diff options
| -rw-r--r-- | plugins/extraction/extraction.ml | 100 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 48 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 19 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3923.v | 33 |
4 files changed, 111 insertions, 89 deletions
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/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 diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v new file mode 100644 index 000000000..0aa029e73 --- /dev/null +++ b/test-suite/bugs/closed/3923.v @@ -0,0 +1,33 @@ +Module Type TRIVIAL. +Parameter t:Type. +End TRIVIAL. + +Module MkStore (Key : TRIVIAL). + +Module St : TRIVIAL. +Definition t := unit. +End St. + +End MkStore. + + + +Module Type CERTRUNTIMETYPES (B : TRIVIAL). + +Parameter cert_fieldstore : Type. +Parameter empty_fieldstore : cert_fieldstore. + +End CERTRUNTIMETYPES. + + + +Module MkCertRuntimeTypes (B : TRIVIAL) : CERTRUNTIMETYPES B. + +Module FieldStore := MkStore B. + +Definition cert_fieldstore := FieldStore.St.t. +Axiom empty_fieldstore : cert_fieldstore. + +End MkCertRuntimeTypes. + +Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) |