diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/common.ml | 5 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 100 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 90 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 2 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 5 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 48 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 19 |
9 files changed, 180 insertions, 101 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 97f856944..8cf3b8194 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -171,10 +171,7 @@ let push_vars ids (db,avoid) = let ids',avoid' = rename_vars avoid ids in ids', (ids' @ db, avoid') -let get_db_name n (db,_) = - let id = List.nth db (pred n) in - if Id.equal id dummy_name then Id.of_string "__" else id - +let get_db_name n (db,_) = List.nth db (pred n) (*S Renamings of global objects. *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f4d14af62..2dc2420c4 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -201,36 +201,6 @@ let parse_ind_args si args relmax = | _ -> parse (i+1) (j+1) s) in parse 1 1 si -let oib_equal o1 o2 = - Id.equal o1.mind_typename o2.mind_typename && - List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && - begin - match o1.mind_arity, o2.mind_arity with - | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> - eq_constr c1 c2 && Sorts.equal s1 s2 - | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in - List.equal eq p1.template_param_levels p2.template_param_levels && - Univ.Universe.equal p1.template_level p2.template_level - | _, _ -> false - end && - Array.equal Id.equal o1.mind_consnames o2.mind_consnames - -let eq_record x y = - Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y - -let mib_equal m1 m2 = - Array.equal oib_equal m1.mind_packets m1.mind_packets && - eq_record m1.mind_record m2.mind_record && - (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite && - Int.equal m1.mind_ntypes m2.mind_ntypes && - List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && - Int.equal m1.mind_nparams m2.mind_nparams && - Int.equal m1.mind_nparams_rec m2.mind_nparams_rec && - List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && - (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *) - (* m1.mind_universes = m2.mind_universes *) - (*S Extraction of a type. *) (* [extract_type env db c args] is used to produce an ML type from the @@ -360,14 +330,9 @@ and extract_type_scheme env db c p = and extract_ind env kn = (* kn is supposed to be in long form *) let mib = Environ.lookup_mind kn env in - try - (* For a same kn, we can get various bodies due to module substitutions. - We hence check that the mib has not changed from recording - time to retrieving time. Ideally we should also check the env. *) - let (mib0,ml_ind) = lookup_ind kn in - if not (mib_equal mib mib0) then raise Not_found; - ml_ind - with Not_found -> + match lookup_ind kn mib with + | Some ml_ind -> ml_ind + | None -> (* First, if this inductive is aliased via a Module, we process the original inductive if possible. When at toplevel of the monolithic case, we cannot do much @@ -523,28 +488,25 @@ and extract_type_cons env db dbmap c i = (*s Recording the ML type abbreviation of a Coq type scheme constant. *) and mlt_env env r = match r with + | IndRef _ | ConstructRef _ | VarRef _ -> None | ConstRef kn -> - (try - if not (visible_con kn) then raise Not_found; - match lookup_term kn with - | Dtype (_,vl,mlt) -> Some mlt + let cb = Environ.lookup_constant kn env in + match cb.const_body with + | Undef _ | OpaqueDef _ -> None + | Def l_body -> + match lookup_typedef kn cb with + | Some _ as o -> o + | None -> + let typ = Typeops.type_of_constant_type env cb.const_type + (* FIXME not sure if we should instantiate univs here *) in + match flag_of_type env typ with + | Info,TypeScheme -> + let body = Mod_subst.force_constr l_body in + let s = type_sign env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db body (List.length s) + in add_typedef kn cb t; Some t | _ -> None - with Not_found -> - let cb = Environ.lookup_constant kn env in - let typ = Typeops.type_of_constant_type env cb.const_type - (* FIXME not sure if we should instantiate univs here *) in - match cb.const_body with - | Undef _ | OpaqueDef _ -> None - | Def l_body -> - (match flag_of_type env typ with - | Info,TypeScheme -> - let body = Mod_subst.force_constr l_body in - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) - in add_term kn (Dtype (r, vl, t)); Some t - | _ -> None)) - | _ -> None and expand env = type_expand (mlt_env env) and type2signature env = type_to_signature (mlt_env env) @@ -555,16 +517,18 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) (*s Extraction of the type of a constant. *) let record_constant_type env kn opt_typ = - try - if not (visible_con kn) then raise Not_found; - lookup_type kn - with Not_found -> - let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type - | Some typ -> typ - in let mlt = extract_type env [] 1 typ [] - in let schema = (type_maxvar mlt, mlt) - in add_type kn schema; schema + let cb = lookup_constant kn env in + match lookup_cst_type kn cb with + | Some schema -> schema + | None -> + let typ = match opt_typ with + | None -> Typeops.type_of_constant_type env cb.const_type + | Some typ -> typ + in + let mlt = extract_type env [] 1 typ [] in + let schema = (type_maxvar mlt, mlt) in + let () = add_cst_type kn cb schema in + schema (*S Extraction of a term. *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 00259750d..da7a4265e 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -143,7 +143,11 @@ let rec pp_expr par env args = and apply2 st = pp_apply2 st par args in function | MLrel n -> - let id = get_db_name n env in apply (pr_id id) + let id = get_db_name n env in + (* Try to survive to the occurrence of a Dummy rel. + TODO: we should get rid of this hack (cf. #592) *) + let id = if Id.equal id dummy_name then Id.of_string "__" else id in + apply (pr_id id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index bfd0794de..62724f211 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -511,6 +511,70 @@ let nb_occur_match = | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0 in nb 1 +(* Replace unused variables by _ *) + +let dump_unused_vars a = + let rec ren env a = match a with + | MLrel i -> + let () = (List.nth env (i-1)) := true in a + + | MLlam (id,b) -> + let occ_id = ref false in + let b' = ren (occ_id::env) b in + if !occ_id then if b' == b then a else MLlam(id,b') + else MLlam(Dummy,b') + + | MLletin (id,b,c) -> + let occ_id = ref false in + let b' = ren env b in + let c' = ren (occ_id::env) c in + if !occ_id then + if b' == b && c' == c then a else MLletin(id,b',c') + else + (* 'let' without occurrence: shouldn't happen after simpl *) + MLletin(Dummy,b',c') + + | MLcase (t,e,br) -> + let e' = ren env e in + let br' = Array.smartmap (ren_branch env) br in + if e' == e && br' == br then a else MLcase (t,e',br') + + | MLfix (i,ids,v) -> + let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in + let v' = Array.smartmap (ren env') v in + if v' == v then a else MLfix (i,ids,v') + + | MLapp (b,l) -> + let b' = ren env b and l' = List.smartmap (ren env) l in + if b' == b && l' == l then a else MLapp (b',l') + + | MLcons(t,r,l) -> + let l' = List.smartmap (ren env) l in + if l' == l then a else MLcons (t,r,l') + + | MLtuple l -> + let l' = List.smartmap (ren env) l in + if l' == l then a else MLtuple l' + + | MLmagic b -> + let b' = ren env b in + if b' == b then a else MLmagic b' + + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a + + and ren_branch env ((ids,p,b) as tr) = + let occs = List.map (fun _ -> ref false) ids in + let b' = ren (List.rev_append occs env) b in + let ids' = + List.map2 + (fun id occ -> if !occ then id else Dummy) + ids occs + in + if b' == b && List.equal eq_ml_ident ids ids' then tr + else (ids',p,b') + in + ren [] a + (*s Lifting on terms. [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *) @@ -949,9 +1013,20 @@ let expand_linear_let o id e = (* Some beta-iota reductions + simplifications. *) +let rec unmagic = function MLmagic e -> unmagic e | e -> e +let is_magic = function MLmagic _ -> true | _ -> false +let magic_hd a = match a with + | MLmagic _ :: _ -> a + | e :: a -> MLmagic e :: a + | [] -> assert false + let rec simpl o = function | MLapp (f, []) -> simpl o f - | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) + | MLapp (MLapp(f,a),a') -> simpl o (MLapp(f,a@a')) + | MLapp (f, a) -> + (* When the head of the application is magic, no need for magic on args *) + let a = if is_magic f then List.map unmagic a else a in + simpl_app o (List.map (simpl o) a) (simpl o f) | MLcase (typ,e,br) -> let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in simpl_case o typ br (simpl o e) @@ -971,12 +1046,18 @@ let rec simpl o = function if ast_occurs_itvl 1 n c.(i) then MLfix (i, ids, Array.map (simpl o) c) else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *) + | MLmagic(MLmagic _ as e) -> simpl o e + | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l)) + | MLmagic(MLletin(id,c,e)) -> simpl o (MLletin(id,c,MLmagic e)) + | MLmagic(MLcase(typ,e,br)) -> + let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in + simpl o (MLcase(typ,e,br')) + | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a (* invariant : list [a] of arguments is non-empty *) and simpl_app o a = function - | MLapp (f',a') -> simpl_app o (a'@a) f' | MLlam (Dummy,t) -> simpl o (MLapp (ast_pop t, List.tl a)) | MLlam (id,t) -> (* Beta redex *) @@ -989,8 +1070,9 @@ and simpl_app o a = function simpl o (MLletin (id, List.hd a, MLapp (t, a')))) | MLmagic (MLlam (id,t)) -> (* When we've at least one argument, we permute the magic - and the lambda, to simplify things a bit (see #2795) *) - simpl_app o a (MLlam (id,MLmagic t)) + and the lambda, to simplify things a bit (see #2795). + Alas, the 1st argument must also be magic then. *) + simpl_app o (magic_hd a) (MLlam (id,MLmagic t)) | MLletin (id,e1,e2) when o.opt_let_app -> (* Application of a letin: we push arguments inside *) MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index c380dfb3e..c07cee713 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -111,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast +val dump_unused_vars : ml_ast -> ml_ast + val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index e8383bda5..c3dc286cd 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -269,7 +269,7 @@ let rec optim_se top to_appear s = function let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - let d = match optimize_fix a with + let d = match dump_unused_vars (optimize_fix a) with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) | a -> Dterm (r, a, t) @@ -283,7 +283,8 @@ let rec optim_se top to_appear s = function if inline rv.(i) fake_body then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s done; - (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + let av' = Array.map dump_unused_vars av in + (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} in (l,SEmodule m) :: (optim_se top to_appear s lse) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 6ff4c25ec..8c86c7711 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -178,7 +178,11 @@ let rec pp_expr par env args = and apply2 st = pp_apply2 st par args in function | MLrel n -> - let id = get_db_name n env in apply (pr_id id) + let id = get_db_name n env in + (* Try to survive to the occurrence of a Dummy rel. + TODO: we should get rid of this hack (cf. #592) *) + let id = if Id.equal id dummy_name then Id.of_string "__" else id in + apply (pr_id id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 63d792e36..9feaea8cd 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -72,8 +72,6 @@ let mp_length mp = | _ -> 1 in len mp -let visible_con kn = at_toplevel (base_mp (con_modpath kn)) - let rec prefixes_mp mp = match mp with | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') | _ -> MPset.singleton mp @@ -105,17 +103,30 @@ let labels_of_ref r = (* Theses tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) -(*s Constants tables. *) +(* We use [constant_body] (resp. [mutual_inductive_body]) as checksum + to ensure that the table contents aren't outdated. *) -let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t) -let init_terms () = terms := Cmap_env.empty -let add_term kn d = terms := Cmap_env.add kn d !terms -let lookup_term kn = Cmap_env.find kn !terms +(*s Constants tables. *) -let types = ref (Cmap_env.empty : ml_schema Cmap_env.t) -let init_types () = types := Cmap_env.empty -let add_type kn s = types := Cmap_env.add kn s !types -let lookup_type kn = Cmap_env.find kn !types +let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let init_typedefs () = typedefs := Cmap_env.empty +let add_typedef kn cb t = + typedefs := Cmap_env.add kn (cb,t) !typedefs +let lookup_typedef kn cb = + try + let (cb0,t) = Cmap_env.find kn !typedefs in + if cb0 == cb then Some t else None + with Not_found -> None + +let cst_types = + ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) +let init_cst_types () = cst_types := Cmap_env.empty +let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types +let lookup_cst_type kn cb = + try + let (cb0,s) = Cmap_env.find kn !cst_types in + if cb0 == cb then Some s else None + with Not_found -> None (*s Inductives table. *) @@ -124,7 +135,14 @@ let inductives = let init_inductives () = inductives := Mindmap_env.empty let add_ind kn mib ml_ind = inductives := Mindmap_env.add kn (mib,ml_ind) !inductives -let lookup_ind kn = Mindmap_env.find kn !inductives +let lookup_ind kn mib = + try + let (mib0,ml_ind) = Mindmap_env.find kn !inductives in + if mib == mib0 then Some ml_ind + else None + with Not_found -> None + +let unsafe_lookup_ind kn = snd (Mindmap_env.find kn !inductives) let inductive_kinds = ref (Mindmap_env.empty : inductive_kind Mindmap_env.t) @@ -244,10 +262,10 @@ let safe_basename_of_global r = | ConstRef kn -> Label.to_id (con_label kn) | IndRef (kn,0) -> Label.to_id (mind_label kn) | IndRef (kn,i) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) | ConstructRef ((kn,i),j) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) | VarRef _ -> assert false @@ -876,6 +894,6 @@ let extract_inductive r s l optstr = (*s Tables synchronization. *) let reset_tables () = - init_terms (); init_types (); init_inductives (); + init_typedefs (); init_cst_types (); init_inductives (); init_inductive_kinds (); init_recursors (); init_projs (); init_axioms (); init_opaques (); reset_modfile () diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a6734dae8..916cf3ad6 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -55,7 +55,6 @@ val string_of_modfile : module_path -> string val file_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool -val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : @@ -65,14 +64,22 @@ val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) -val add_term : constant -> ml_decl -> unit -val lookup_term : constant -> ml_decl +(* For avoiding repeated extraction of the same constant or inductive, + we use cache functions below. Indexing by constant name isn't enough, + due to modules we could have a same constant name but different + content. So we check that the [constant_body] hasn't changed from + recording time to retrieving time. Same for inductive : we store + [mutual_inductive_body] as checksum. In both case, we should ideally + also check the env *) -val add_type : constant -> ml_schema -> unit -val lookup_type : constant -> ml_schema +val add_typedef : constant -> constant_body -> ml_type -> unit +val lookup_typedef : constant -> constant_body -> ml_type option + +val add_cst_type : constant -> constant_body -> ml_schema -> unit +val lookup_cst_type : constant -> constant_body -> ml_schema option val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind +val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option val add_inductive_kind : mutual_inductive -> inductive_kind -> unit val is_coinductive : global_reference -> bool |