Commits

Thomas Tuerk committed 0c06c21

get inlining working again, started working on getting pattern compilation again

  • Participants
  • Parent commits 70c995c

Comments (0)

Files changed (9)

File src/patterns.ml

   in
   List.map get_descr nl
 
+val type_defs_get_constr_families : Ast.l -> type_defs -> t -> const_descr_ref -> constr_family_descr list
 
 let constr_matrix_compile_fun (simp_input: bool) (env : env) (gen : var_name_generator) (m_ty : Types.t) l_org : matrix_compile_fun = fun pL ->
   let ((p : pat), p_id) = matrix_compile_fun_get (Util.option_first (fun p -> Util.option_map (fun (id, _) -> (p, id)) (dest_const_pat p)) pL) in
-  let _ = matrix_compile_fun_check (List.for_all (fun p -> (is_constr_pat p || is_wild_pat p)) pL) in
+  let _ = matrix_compile_fun_check (List.for_all (fun p -> (is_const_pat p || is_wild_pat p)) pL) in
   let loc = Ast.Trans ("constr_matrix_compile_fun", Some l_org) in
 
   let p_ty = annot_to_typ p in
-  let all_ids = get_all_constr_descr loc env p_id in
 
-  (* now build the real argument types and fresh variable names for the arguments *)
+  (* get the family of constructors to match against *)
+  let cfam = begin 
+    let refl = List.map_filter dest_const_pat pL in
+    let cfam_canditates = type_defs_get_constr_families loc env.t_env p_ty p_id.descr in
+    let cfam_ok cfam = List.subset refl cfam.constr_list in
+    matrix_compile_fun_get (Util.option_first (fun cfam -> if cfam_OK cfam then Some cfam else None) cfam_canditates)
+  end in
 
+  (* now build the real argument types and fresh variable names for the arguments *)
   let build_args (id : constr_descr id) =
     let c = id.descr in 
     let subst = Types.TNfmap.from_list2 c.constr_tparams id.instantiation in
   in
   let all_args = List.map build_args all_ids in
 
+
   (* Build top-fun *)
   let top_fun : matrix_compile_top_fun  = fun i eL -> 
      let _ = matrix_compile_fun_check (List.length eL = List.length all_args) in
    [(fun _ _ -> tuple_matrix_compile_fun); 
     (fun _ _ -> bool_matrix_compile_fun false); 
     (fun _ _ -> list_matrix_compile_fun); 
-(*    (           constr_matrix_compile_fun);  *)
+(*    (           constr_matrix_compile_fun);    *)
     (fun _   -> num_matrix_compile_fun false); (fun _   -> num_add_matrix_compile_fun_simple);
     (fun _   -> string_matrix_compile_fun false); 
 (*    (fun _   -> record_matrix_compile_fun) *)]
 
     
 let compile_def t mca env_global (_:Name.t list) env_local (((d, s), l) as org_d : def) =  
-(* TODO: check that union can safely be removed after Scotts change.
-   let env = env_union env_global env_local in *)
  let env = env_global in
  let t' = Util.option_map target_to_ast_target t in
  let cf_opt e = compile_match_exp t mca env e in
   
 let remove_toplevel_match targ mca env_global _ env_local (((d, s), l)) =
   let l_unk = Ast.Trans ("remove_toplevel_match", Some l) in
-
-  (* TODO check 
-  let env = env_union env_global env_local in
-  *)
-
   let env = env_global in
   let aux sk1 sk2 topt sl tnvs class_constraints = begin
     let (_, sk_first_opt, group_nameL) = funcl_aux_seplist_group sl in

File src/target_trans.ml

 				 T.remove_setcomp;
                                  T.remove_set_restr_quant;
                                  T.remove_restr_quant Pattern_syntax.is_var_tup_pat;
-                                 (* TODO: T.do_substitutions Target_hol; *)
+                                 T.do_substitutions Target_hol;
                                  Patterns.compile_exp (Some Target_hol) Patterns.is_hol_pattern_match C.d env]);
                 Pat_macros (fun env ->
                               let module T = T(struct let env = env end) in
                               let module T = T(struct let env = env end) in
                                 [(* TODO: figure out what it does and perhaps add it again    T.hack; *)
                                  (* TODO: add again or implement otherwise                    T.tup_ctor (fun e -> e) Seplist.empty; *)
-                                 (* TODO: add again                                           T.do_substitutions Target_ocaml; *)
+                                 T.do_substitutions Target_ocaml;
                                  T.remove_sets;
                                  T.remove_list_comprehension;
                                  T.remove_quant;
                          T.remove_set_restr_quant;
                          T.remove_restr_quant Pattern_syntax.is_var_wild_tup_pat;
                          T.remove_set_comp_binding;
-                         (* TODO: add again T.do_substitutions Target_isa;*)
+                         T.do_substitutions Target_isa;
                          (* TODO: add again T.sort_record_fields;  *)
                          T.string_lits_isa;
                          Patterns.compile_exp (Some Target_isa) Patterns.is_isabelle_pattern_match C.d env]);
                           T.remove_list_comprehension;
                           T.remove_set_comprehension;
                           T.remove_quant;
-                          (* TODO: add again      T.do_substitutions Target_coq; *)
+                          T.do_substitutions Target_coq; 
                           Patterns.compile_exp (Some Target_coq) Patterns.is_coq_pattern_match C.d env]);
          Pat_macros (fun env ->
                        let module T = T(struct let env = env end) in

File src/trans.ml

         let (subst, x, y) = build_subst params args in
           (Nfmap.insert subst (p.term, Sub(a)), x, y)
 
+
+(* Inline sub [target] bindings *)
+let do_substitutions target e =
+  let l_unk = Ast.Trans("do_substitutions", Some (exp_to_locn e)) in
+  let (f,infix,args) = app_list e in
+    match C.exp_to_term f with
+      | Constant(c_id) ->
+          let cd = c_env_lookup l_unk E.env.c_env c_id.descr in
+          begin            
+            match Targetmap.apply cd.target_rep target with
+              | Some(CR_inline (params,body)) ->
+                  let tsubst = 
+                    Types.TNfmap.from_list2 cd.const_tparams c_id.instantiation
+                  in
+                  let (vsubst, leftover_params, leftover_args) = 
+                    build_subst params args
+                  in
+                  let b = 
+                    C.exp_subst (tsubst,vsubst) 
+                      (fst (alter_init_lskips (fun _ -> (ident_get_first_lskip c_id, None)) body))
+                  in
+                    if params = [] && infix then
+                      begin
+                        match leftover_args with
+                          | (a1,l)::(a2,_)::args ->
+                              Some(List.fold_left 
+                                     (fun e (e',l) -> C.mk_app l e e' None)
+                                     (C.mk_infix l a1 b a2 None)
+                                     args)
+                          | _ -> assert false
+                      end
+                    else if leftover_params = [] then
+                      Some(List.fold_left 
+                             (fun e (e',l) -> C.mk_app l e e' None)
+                             b
+                             leftover_args)
+                    else
+                      Some(C.mk_fun l_unk
+                             None (List.map 
+                                     (fun n -> 
+                                        C.mk_pvar n.locn (Name.add_lskip n.term) (Types.type_subst tsubst n.typ))
+                                     leftover_params) 
+                             None b
+                             None)
+              | _ -> None
+          end
+      | _ -> None
+
+
 (* Replace by something more clever 
 (* Change constructors into tupled constructors *) 
 let rec tup_ctor build_result args e = 

File src/trans.mli

   (** [remove_unit_pats] replaces unit-patterns [()] with wildcard ones [_]. *)
   val remove_unit_pats : pat_macro
 
+  (** [do_substitutions env target] does the inlining of target specific constant definitions *)
+  val do_substitutions : Target.target -> exp macro
+
 (* TODO: add again
 
   (** Warning: HOL specific! Transforms num-patterns of the form [n] or [x + n] into

File src/typecheck.ml

   let add_subst =
     match substitution with
       | None -> (fun c -> c)
-      | Some(ts,(nl, e)) ->
+      | Some(ts,s) ->
           (fun c -> 
-            let s_rep = CR_dummy in
              { c with target_rep = 
                  Targetset.fold
-                   (fun t r -> Targetmap.insert r (t,s_rep))
+                   (fun t r -> Targetmap.insert r (t,CR_inline s))
                    ts 
                    c.target_rep
              })
               context
               ntyps
           in
-          let constr_family = {constr_list = cl; constr_case_fun = None} in
+          let constr_family = {constr_list = cl; constr_case_fun = None; constr_exhaustive = true} in
           let ctxt = {ctxt with all_tdefs = type_defs_add_constr_family l ctxt.all_tdefs type_path constr_family} in 
             (((tn,l),tnvs, Te_variant(sk3,vars), regexp), ctxt)
   end;;

File src/typed_ast.ml

   | P_var_annot of Name.lskips_t * src_t
 
 and const_target_rep =
-  | CR_inline of (exp list -> exp)
-  | CR_target of (exp list -> Output.t)
-  | CR_dummy
+  | CR_rename of Name.t               
+  | CR_inline of ((Name.t,unit) annot list * exp)
 
 and const_descr = { const_binding : Path.t;
                     const_tparams : Types.tnvar list;

File src/typed_ast.mli

         of the P_typ and P_var cases above, but useful as a macro target. *)
 
 and const_target_rep =
-  | CR_inline of (exp list -> exp)
-  | CR_target of (exp list -> Output.t)
-  | CR_dummy
+  | CR_rename of Name.t               
+    (** rename the constant to the given name, but keep Module structure *)
+
+  | CR_inline of ((Name.t,unit) annot list * exp)
+    (** [CR_inline (vars, e)] means inlining the costant with the expression [e] and
+        replacing the variable [vars] inside [e] with the arguments of the constant. *)
 
 (** The description of a top-level definition *)
 and const_descr = 

File src/types.ml

     | Tvar(s) ->
         (match TNfmap.apply substs (Ty s) with
            | Some(t) -> Some(t)
-           | None -> assert false)
+           | None -> None)
     | Tfn(t1,t2) -> 
         begin
           match (type_subst_aux substs t1, type_subst_aux substs t2) with
    constr_list : const_descr_ref list; 
    (** a list of all the constructors *)
 
+   constr_exhaustive : bool;
+   (** is this family of constructors exhaustive, or does a special catch-other case needs adding? *)
+
    constr_case_fun : const_descr_ref option 
    (** the case split function for this constructor list, [None] means that pattern matching is used. *)
 }

File src/types.mli

    constr_list : const_descr_ref list; 
    (** a list of all the constructors *)
 
+   constr_exhaustive : bool;
+   (** is this family of constructors exhaustive, or does a special catch-other case needs adding? *)
+
    constr_case_fun : const_descr_ref option 
    (** the case split function for this constructor list, [None] means that pattern matching is used. *)
 }