diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 5 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 4 | ||||
| -rw-r--r-- | kernel/closure.ml | 14 | ||||
| -rw-r--r-- | kernel/closure.mli | 4 | ||||
| -rw-r--r-- | kernel/cooking.ml | 14 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 59 | ||||
| -rw-r--r-- | kernel/declarations.mli | 40 | ||||
| -rw-r--r-- | kernel/entries.ml | 12 | ||||
| -rw-r--r-- | kernel/entries.mli | 11 | ||||
| -rw-r--r-- | kernel/environ.ml | 30 | ||||
| -rw-r--r-- | kernel/environ.mli | 7 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/inductive.ml | 12 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 732 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 87 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 456 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 17 | ||||
| -rw-r--r-- | kernel/modops.ml | 762 | ||||
| -rw-r--r-- | kernel/modops.mli | 46 | ||||
| -rw-r--r-- | kernel/names.ml | 137 | ||||
| -rw-r--r-- | kernel/names.mli | 54 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 24 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 9 | ||||
| -rw-r--r-- | kernel/reduction.ml | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 502 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 23 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 192 | ||||
| -rw-r--r-- | kernel/term.ml | 9 | ||||
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 10 |
31 files changed, 1790 insertions, 1497 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index a7e8b0b265..e7859962eb 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -723,7 +723,10 @@ let compile_constant_body env body opaque boxed = BCdefined(true, to_patch) else match kind_of_term body with - | Const kn' -> BCallias (get_allias env kn') + | Const kn' -> + (* we use the canonical name of the constant*) + let con= constant_of_kn (canonical_con kn') in + BCallias (get_allias env con) | _ -> let res = compile env body in let to_patch = to_memory res in diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 89264e88b1..4a9c7da2b5 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -304,13 +304,13 @@ let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> sc | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_kn s kn, i)) + | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_ind s kn, i)) let subst_patch s (ri,pos) = match ri with | Reloc_annot a -> let (kn,i) = a.ci.ci_ind in - let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in + let ci = {a.ci with ci_ind = (subst_ind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos) diff --git a/kernel/closure.ml b/kernel/closure.ml index bce564397c..93788ed422 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -196,6 +196,8 @@ let unfold_red kn = type table_key = id_key +let eq_table_key = Names.eq_id_key + type 'a infos = { i_flags : reds; i_repr : 'a infos -> constr -> 'a; @@ -250,18 +252,6 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let rec mind_equiv env (kn1,i1) (kn2,i2) = - let rec equiv kn1 kn2 = - kn1 = kn2 || - match (lookup_mind kn1 env).mind_equiv with - Some kn1' -> equiv kn2 kn1' - | None -> match (lookup_mind kn2 env).mind_equiv with - Some kn2' -> equiv kn2' kn1 - | None -> false in - i1 = i2 && equiv kn1 kn2 - -let mind_equiv_infos info = mind_equiv info.i_env - let create mk_cl flgs env evars = { i_flags = flgs; i_repr = mk_cl; diff --git a/kernel/closure.mli b/kernel/closure.mli index b6ff1fa15d..5cb6fc97c4 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -179,9 +179,7 @@ val whd_stack : (* [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> table_key -> fconstr option -(* [mind_equiv] checks whether two inductive types are intentionally equal *) -val mind_equiv : env -> inductive -> inductive -> bool -val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool +val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index e42a732d38..c971ed2993 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -19,15 +19,15 @@ open Reduction (*s Cooking the constants. *) -type work_list = identifier array Cmap.t * identifier array KNmap.t +type work_list = identifier array Cmap.t * identifier array Mindmap.t let pop_dirpath p = match repr_dirpath p with | [] -> anomaly "dirpath_prefix: empty dirpath" | _::l -> make_dirpath l -let pop_kn kn = - let (mp,dir,l) = Names.repr_kn kn in - Names.make_kn mp (pop_dirpath dir) l +let pop_mind kn = + let (mp,dir,l) = Names.repr_mind kn in + Names.make_mind mp (pop_dirpath dir) l let pop_con con = let (mp,dir,l) = Names.repr_con con in @@ -48,9 +48,9 @@ let share r (cstl,knl) = let f,l = match r with | IndRef (kn,i) -> - mkInd (pop_kn kn,i), KNmap.find kn knl + mkInd (pop_mind kn,i), Mindmap.find kn knl | ConstructRef ((kn,i),j) -> - mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl + mkConstruct ((pop_mind kn,i),j), Mindmap.find kn knl | ConstRef cst -> mkConst (pop_con cst), Cmap.find cst cstl in let c = mkApp (f, Array.map mkVar l) in @@ -69,7 +69,7 @@ let update_case_info ci modlist = with Not_found -> ci -let empty_modlist = (Cmap.empty, KNmap.empty) +let empty_modlist = (Cmap.empty, Mindmap.empty) let expmod_constr modlist c = let rec substrec c = diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 23b1f25347..db35031d93 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,7 +16,7 @@ open Univ (*s Cooking the constants. *) -type work_list = identifier array Cmap.t * identifier array KNmap.t +type work_list = identifier array Cmap.t * identifier array Mindmap.t type recipe = { d_from : constant_body; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c48c01d786..515009798c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -69,7 +69,7 @@ type recarg = let subst_recarg sub r = match r with | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_kn sub kn in + | Imbr (kn,i) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -190,25 +190,25 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } -let subst_arity sub = function -| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) -| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) - +let subst_arity sub arity = + if sub = empty_subst then arity + else match arity with + | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) + | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { - const_hyps = (assert (cb.const_hyps=[]); []); - const_body = Option.map (subst_constr_subst sub) cb.const_body; - const_type = subst_arity sub cb.const_type; - const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) - const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque; - const_inline = cb.const_inline} - + const_hyps = (assert (cb.const_hyps=[]); []); + const_body = Option.map (subst_constr_subst sub) cb.const_body; + const_type = subst_arity sub cb.const_type; + const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) + const_constraints = cb.const_constraints; + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} + let subst_arity sub = function | Monomorphic s -> Monomorphic { @@ -244,8 +244,7 @@ let subst_mind sub mib = mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints ; - mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } + mind_constraints = mib.mind_constraints } (*s Modules: signature component specifications, module types, and @@ -255,8 +254,6 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option - * constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -264,24 +261,26 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * constraints + | SEBapply of struct_expr_body * struct_expr_body * constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = With_module_body of identifier list * module_path - * struct_expr_body option * constraints | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : Retroknowledge.action list} and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : constraints; + typ_delta :delta_resolver} diff --git a/kernel/declarations.mli b/kernel/declarations.mli index c7e27db6be..adf1d14e23 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -171,8 +171,6 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body @@ -185,8 +183,6 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option - * constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -194,24 +190,38 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * constraints + | SEBapply of struct_expr_body * struct_expr_body * constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = With_module_body of identifier list * module_path - * struct_expr_body option * constraints | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + { (*absolute path of the module*) + mod_mp : module_path; + (* Implementation *) + mod_expr : struct_expr_body option; + (* Signature *) + mod_type : struct_expr_body; + (* algebraic structure expression is kept + if it's relevant for extraction *) + mod_type_alg : struct_expr_body option; + (* set of all constraint in the module *) mod_constraints : constraints; - mod_alias : substitution; + (* quotiented set of equivalent constant and inductive name *) + mod_delta : delta_resolver; mod_retroknowledge : Retroknowledge.action list} - + and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + { + (*Path of the module type*) + typ_mp : module_path; + typ_expr : struct_expr_body; + (* algebraic structure expression is kept + if it's relevant for extraction *) + typ_expr_alg : struct_expr_body option ; + typ_constraints : constraints; + (* quotiented set of equivalent constant and inductive name *) + typ_delta :delta_resolver} diff --git a/kernel/entries.ml b/kernel/entries.ml index 26e9a62503..938d1c60aa 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -62,7 +62,8 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool} -type parameter_entry = types*bool +(* type and the inlining flag *) +type parameter_entry = types * bool type constant_entry = | DefinitionEntry of definition_entry @@ -70,7 +71,14 @@ type constant_entry = (*s Modules *) -type module_struct_entry = + +type specification_entry = + SPEconst of constant_entry + | SPEmind of mutual_inductive_entry + | SPEmodule of module_entry + | SPEmodtype of module_struct_entry + +and module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration diff --git a/kernel/entries.mli b/kernel/entries.mli index 291ff0d458..20fbbb8e7d 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type definition_entry = { const_entry_opaque : bool; const_entry_boxed : bool } -type parameter_entry = types*bool (*inline flag*) +type parameter_entry = types * bool (*inline flag*) type constant_entry = | DefinitionEntry of definition_entry @@ -69,7 +69,14 @@ type constant_entry = (*s Modules *) -type module_struct_entry = + +type specification_entry = + SPEconst of constant_entry + | SPEmind of mutual_inductive_entry + | SPEmodule of module_entry + | SPEmodtype of module_struct_entry + +and module_struct_entry = MSEident of module_path | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry | MSEwith of module_struct_entry * with_declaration diff --git a/kernel/environ.ml b/kernel/environ.ml index fb51660b3e..a233d0be19 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -141,7 +141,7 @@ let lookup_constant = lookup_constant let add_constant kn cs env = let new_constants = - Cmap.add kn (cs,ref None) env.env_globals.env_constants in + Cmap_env.add kn (cs,ref None) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in @@ -174,11 +174,9 @@ let evaluable_constant cst env = (* Mutual Inductives *) let lookup_mind = lookup_mind -let scrape_mind = scrape_mind - - + let add_mind kn mib env = - let new_inds = KNmap.add kn mib env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let new_globals = { env.env_globals with env_inductives = new_inds } in @@ -276,30 +274,12 @@ let shallow_add_module mp mb env = env_modules = new_mods } in { env with env_globals = new_globals } -let rec scrape_alias mp env = - try - let mp1 = MPmap.find mp env.env_globals.env_alias in - scrape_alias mp1 env - with - Not_found -> mp - let lookup_module mp env = - let mp = scrape_alias mp env in MPmap.find mp env.env_globals.env_modules -let lookup_modtype ln env = - let mp = scrape_alias ln env in - MPmap.find mp env.env_globals.env_modtypes - -let register_alias mp1 mp2 env = - let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in - let new_globals = - { env.env_globals with - env_alias = new_alias } in - { env with env_globals = new_globals } -let lookup_alias mp env = - MPmap.find mp env.env_globals.env_alias +let lookup_modtype mp env = + MPmap.find mp env.env_globals.env_modtypes (*s Judgments. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 0ae2855286..9401ba6b03 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -142,9 +142,6 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env (* raises [Not_found] if the required path is not found *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body -(* Find the ultimate inductive in the [mind_equiv] chain *) -val scrape_mind : env -> mutual_inductive -> mutual_inductive - (************************************************************************) (*s Modules *) val add_modtype : module_path -> module_type_body -> env -> env @@ -155,10 +152,6 @@ val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : module_path -> env -> module_type_body -val register_alias : module_path -> module_path -> env -> env -val lookup_alias : module_path -> env -> module_path -val scrape_alias : module_path -> env -> module_path - (************************************************************************) (*s Universe constraints *) val set_universes : Univ.universes -> env -> env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index c202d627df..ffb6be771b 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -651,8 +651,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_nparams_rec = nmr; mind_params_ctxt = params; mind_packets = packets; - mind_constraints = cst; - mind_equiv = None; + mind_constraints = cst } (************************************************************************) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 19e4130ffd..8252f2d5a2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -362,20 +362,10 @@ let type_case_branches env (ind,largs) pj c = (************************************************************************) (* Checking the case annotation is relevent *) -let rec inductive_kn_equiv env kn1 kn2 = - match (lookup_mind kn1 env).mind_equiv with - | Some kn1' -> inductive_kn_equiv env kn2 kn1' - | None -> match (lookup_mind kn2 env).mind_equiv with - | Some kn2' -> inductive_kn_equiv env kn2' kn1 - | None -> false - -let inductive_equiv env (kn1,i1) (kn2,i2) = - i1=i2 & inductive_kn_equiv env kn1 kn2 - let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (Closure.mind_equiv env indsp ci.ci_ind) or + not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 238aa3544a..a9d4a246d6 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -13,27 +13,30 @@ open Util open Names open Term -(* WARNING: not every constant in the associative list domain used to exist - in the environment. This allows a simple implementation of the join - operation. However, iterating over the associative list becomes a non-sense -*) -type resolver = (constant * constr option) list - -let make_resolver resolve = resolve - -let apply_opt_resolver resolve kn = - match resolve with - None -> None - | Some resolve -> - try List.assoc kn resolve with Not_found -> None - -type substitution_domain = - MSI of mod_self_id + +type delta_hint = + Inline of constr option + | Equiv of kernel_name + | Prefix_equiv of module_path + +type delta_key = + KN of kernel_name + | MP of module_path + +module Deltamap = Map.Make(struct + type t = delta_key + let compare = Pervasives.compare + end) + +type delta_resolver = delta_hint Deltamap.t + +let empty_delta_resolver = Deltamap.empty + +type substitution_domain = | MBI of mod_bound_id | MPI of module_path let string_of_subst_domain = function - MSI msid -> debug_string_of_msid msid | MBI mbid -> debug_string_of_mbid mbid | MPI mp -> string_of_mp mp @@ -42,48 +45,233 @@ module Umap = Map.Make(struct let compare = Pervasives.compare end) -type substitution = (module_path * resolver option) Umap.t - +type substitution = (module_path * delta_resolver) Umap.t + let empty_subst = Umap.empty -let add_msid msid mp = - Umap.add (MSI msid) (mp,None) + +let string_of_subst_domain = function + | MBI mbid -> debug_string_of_mbid mbid + | MPI mp -> string_of_mp mp + let add_mbid mbid mp resolve = Umap.add (MBI mbid) (mp,resolve) -let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,None) +let add_mp mp1 mp2 resolve = + Umap.add (MPI mp1) (mp2,resolve) -let map_msid msid mp = add_msid msid mp empty_subst let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst -let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst +let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst + +let add_inline_delta_resolver con = + Deltamap.add (KN(user_con con)) (Inline None) + +let add_inline_constr_delta_resolver con cstr = + Deltamap.add (KN(user_con con)) (Inline (Some cstr)) + +let add_constant_delta_resolver con = + Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) + +let add_mind_delta_resolver mind = + Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) + +let add_mp_delta_resolver mp1 mp2 = + Deltamap.add (MP mp1) (Prefix_equiv mp2) + +let mp_in_delta mp = + Deltamap.mem (MP mp) + +let con_in_delta con resolver = +try + match Deltamap.find (KN(user_con con)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let mind_in_delta mind resolver = +try + match Deltamap.find (KN(user_mind mind)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let delta_of_mp resolve mp = + try + match Deltamap.find (MP mp) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly "mod_subst: bad association in delta_resolver" + with + Not_found -> mp + +let delta_of_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> kn + +let remove_mp_delta_resolver resolver mp = + Deltamap.remove (MP mp) resolver + +exception Inline_kn + +let rec find_prefix resolve mp = + let rec sub_mp = function + | MPdot(mp,l) as mp_sup -> + (try + match Deltamap.find (MP mp_sup) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> MPdot(sub_mp mp,l)) + | p -> + match Deltamap.find (MP p) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + in + try + sub_mp mp + with + Not_found -> mp + +let solve_delta_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> raise Inline_kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found | Inline_kn -> + let mp,dir,l = repr_kn kn in + let new_mp = find_prefix resolve mp in + if mp == new_mp then + kn + else + make_kn new_mp dir l + + +let constant_of_delta resolve con = + let kn = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn new_kn + +let constant_of_delta2 resolve con = + let kn = canonical_con con in + let kn1 = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn1 new_kn + +let mind_of_delta resolve mind = + let kn = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn new_kn + +let mind_of_delta2 resolve mind = + let kn = canonical_mind mind in + let kn1 = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn1 new_kn + + + +let inline_of_delta resolver = + let extract key hint l = + match key,hint with + |KN kn, Inline _ -> kn::l + | _,_ -> l + in + Deltamap.fold extract resolver [] -let list_contents sub = - let one_pair uid (mp,_) l = - (string_of_subst_domain uid, string_of_mp mp)::l +exception Not_inline + +let constant_of_delta_with_inline resolve con = + let kn1,kn2 = canonical_con con,user_con con in + try + match Deltamap.find (KN kn2) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> + try match Deltamap.find (KN kn1) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> None + +let string_of_key = function + | KN kn -> string_of_kn kn + | MP mp -> string_of_mp mp + +let string_of_hint = function + | Inline _ -> "inline" + | Equiv kn -> string_of_kn kn + | Prefix_equiv mp -> string_of_mp mp + +let debug_string_of_delta resolve = + let to_string key hint s = + s^", "^(string_of_key key)^"=>"^(string_of_hint hint) + in + Deltamap.fold to_string resolve "" + +let list_contents sub = + let one_pair uid (mp,reso) l = + (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l in Umap.fold one_pair sub [] - + let debug_string_of_subst sub = - let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in + let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]") + (list_contents sub) in "{" ^ String.concat "; " l ^ "}" + +let debug_pr_delta resolve = + str (debug_string_of_delta resolve) let debug_pr_subst sub = let l = list_contents sub in - let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) + let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++ + spc () ++ str "[" ++ str s3 ++ str "]") in str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" - - + + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPself sid -> - let mp',resolve = Umap.find (MSI sid) sub in + | MPfile sid -> + let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve + begin + try + let mp',resolve = Umap.find (MBI bid) sub in + mp',resolve + with Not_found -> + let mp',resolve = Umap.find (MPI mp) sub in + mp',resolve + end | MPdot (mp1,l) as mp2 -> begin try @@ -93,7 +281,6 @@ let subst_mp0 sub mp = (* 's like subst *) let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try Some (aux mp) @@ -104,39 +291,126 @@ let subst_mp sub mp = None -> mp | Some (mp',_) -> mp' - -let subst_kn0 sub kn = +let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with - Some (mp',_) -> - Some (make_kn mp' dir l) - | None -> None + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn + let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> kn' + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + (make_kn mp' dir l) + | None -> kn + +exception No_subst + +type sideconstantsubst = + | User + | Canonical + +let subst_ind sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + mind + with + No_subst -> mind + +let subst_mind0 sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + Some mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + Some mind + with + No_subst -> Some mind let subst_con sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> con,mkConst con - | Some (mp',resolve) -> - let con' = make_con mp' dir l in - match apply_opt_resolver resolve con with - None -> con',mkConst con' - | Some t -> con',t + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None -> begin + match side with + |User -> + let con = constant_of_delta resolve con' in + con,mkConst con + |Canonical -> + let con = constant_of_delta2 resolve con' in + con,mkConst con + end + | Some t -> con',t + with No_subst -> con , mkConst con + let subst_con0 sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> None - | Some (mp',resolve) -> - let con' = make_con mp' dir l in - match apply_opt_resolver resolve con with - None -> Some (mkConst con') - | Some t -> Some t - + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None ->begin + match side with + |User -> + let con = constant_of_delta resolve con' in + Some (mkConst con) + |Canonical -> + let con = constant_of_delta2 resolve con' in + Some (mkConst con) + end + | t -> t + with No_subst -> Some (mkConst con) + (* Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? Does the user mean "Unfold X.t" or does she mean "Unfold y" @@ -220,7 +494,7 @@ let rec map_kn f f' c = | _ -> c let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) + map_kn (subst_mind0 sub) (subst_con0 sub) let rec replace_mp_in_mp mpfrom mpto mp = match mp with @@ -231,233 +505,145 @@ let rec replace_mp_in_mp mpfrom mpto mp = else MPdot (mp1',l) | _ -> mp -let replace_mp_in_con mpfrom mpto kn = - let mp,dir,l = repr_con kn in +let replace_mp_in_kn mpfrom mpto kn = + let mp,dir,l = repr_kn kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn - else make_con mp'' dir l - -exception BothSubstitutionsAreIdentitySubstitutions -exception ChangeDomain of resolver - -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,resolve) = - let mp',resolve' = - match subst_mp0 sub mp with - None -> mp, None - | Some (mp',resolve') -> mp',resolve' in - let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn' - | MPI mp1 -> - let kn' = replace_mp_in_con mp1 mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - let rec changeDom = function - | [] -> [] - | (kn,topt)::r -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid - | MPI mp1 -> mp1 in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in kn, we remove it - from the resolver that we are building*) - changeDom r - else - (kn',topt)::(changeDom r) - in - Some (changeDom res) - in - mp',resolve'' in - let subst = Umap.mapi (apply_subst subst2) subst1 in - (Umap.fold Umap.add subst2 subst) - -let subst_key subst1 subst2 = - let replace_in_key key (mp,resolve) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst1 mp1 with - | None -> None - | Some (mp2,_) -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,resolve) sub - | Some mpi -> Umap.add mpi (mp,resolve) sub + else make_kn mp'' dir l + +let mp_in_key mp key = + let rec mp_rec mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_rec mp2 + | _ -> false + in + match key with + | MP mp1 -> + mp_rec mp1 + | KN kn -> + let mp1,dir,l = repr_kn kn in + mp_rec mp1 + +let subset_prefixed_by mp resolver = + let prefixmp key hint resolv = + if mp_in_key mp key then + Deltamap.add key hint resolv + else + resolv in - Umap.fold replace_in_key subst2 empty_subst - -let update_subst_alias subst1 subst2 = - let subst_inv key (mp,resolve) sub = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub - | MPself msid -> Umap.add (MSI msid) (newmp,None) sub - | _ -> Umap.add (MPI mp) (newmp,None) sub + Deltamap.fold prefixmp resolver empty_delta_resolver + +let subst_dom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match key with + (MP mp) -> + Deltamap.add (MP (subst_mp subst mp)) hint resolver + | (KN kn) -> + Deltamap.add (KN (subst_kn subst kn)) hint resolver in - let subst_mbi = Umap.fold subst_inv subst2 empty_subst in - let alias_subst key (mp,resolve) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst_mbi mp1 with - | None -> None - | Some (mp2,_) -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,resolve) sub - | Some mpi -> Umap.add mpi (mp,resolve) sub + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_mp_delta sub mp key= + match subst_mp0 sub mp with + None -> empty_delta_resolver,mp + | Some (mp',resolve) -> + let mp1 = find_prefix resolve mp' in + let resolve1 = subset_prefixed_by mp1 resolve in + match key with + MP mpk -> + (subst_dom_delta_resolver + (map_mp mp1 mpk empty_delta_resolver) resolve1),mp1 + | _ -> anomaly "Mod_subst: Bad association in resolver" + +let subst_codom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match hint with + Prefix_equiv mp -> + let derived_resolve,mpnew = subst_mp_delta subst mp key in + Deltamap.fold Deltamap.add derived_resolve + (Deltamap.add key (Prefix_equiv mpnew) resolver) + | (Equiv kn) -> + Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver + | Inline None -> + Deltamap.add key hint resolver + | Inline (Some t) -> + Deltamap.add key (Inline (Some (subst_mps subst t))) resolver in - Umap.fold alias_subst subst1 empty_subst - -let update_subst subst1 subst2 = - let subst_inv key (mp,resolve) l = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> ((MBI mbid),newmp,resolve)::l - | MPself msid -> ((MSI msid),newmp,resolve)::l - | _ -> ((MPI mp),newmp,resolve)::l + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_dom_codom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match key,hint with + (MP mp1),Prefix_equiv mp -> + let key = MP (subst_mp subst mp1) in + let derived_resolve,mpnew = subst_mp_delta subst mp key in + Deltamap.fold Deltamap.add derived_resolve + (Deltamap.add key (Prefix_equiv mpnew) resolver) + | (KN kn1),(Equiv kn) -> + let key = KN (subst_kn subst kn1) in + Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver + | (KN kn),Inline None -> + let key = KN (subst_kn subst kn) in + Deltamap.add key hint resolver + | (KN kn),Inline (Some t) -> + let key = KN (subst_kn subst kn) in + Deltamap.add key (Inline (Some (subst_mps subst t))) resolver + | _,_ -> anomaly "Mod_subst: Bad association in resolver" in - let subst_mbi = Umap.fold subst_inv subst2 [] in - let alias_subst key (mp,resolve) sub= - let newsetkey = - match key with - | MPI mp1 -> - let compute_set_newkey l (k,mp',resolve) = - let mp_from_key = match k with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l - in - begin - match List.fold_left compute_set_newkey [] subst_mbi with - | [] -> None - | l -> Some (l) - end - | _ -> None + Deltamap.fold apply_subst resolver empty_delta_resolver + +let update_delta_resolver resolver1 resolver2 = + let apply_res key hint res = + try + match hint with + Prefix_equiv mp -> + let new_hint = + Prefix_equiv (find_prefix resolver2 mp) + in Deltamap.add key new_hint res + | Equiv kn -> + let new_hint = + Equiv (solve_delta_kn resolver2 kn) + in Deltamap.add key new_hint res + | _ -> Deltamap.add key hint res + with not_found -> + Deltamap.add key hint res in - match newsetkey with - | None -> sub - | Some l -> - List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) - sub l - in - Umap.fold alias_subst subst1 empty_subst + Deltamap.fold apply_res resolver1 empty_delta_resolver + +let add_delta_resolver resolver1 resolver2 = + if resolver1 == resolver2 then + resolver2 + else if resolver2 = empty_delta_resolver then + resolver1 + else + Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) + resolver2 -let join_alias (subst1 : substitution) (subst2 : substitution) = +let join (subst1 : substitution) (subst2 : substitution) = let apply_subst (sub : substitution) key (mp,resolve) = let mp',resolve' = match subst_mp0 sub mp with None -> mp, None - | Some (mp',resolve') -> mp',resolve' in - let resolve'' : resolver option = - try - let res = - match resolve with - Some res -> res - | None -> - match resolve' with - None -> raise BothSubstitutionsAreIdentitySubstitutions - | Some res -> raise (ChangeDomain res) - in - Some - (List.map - (fun (kn,topt) -> - kn, - match topt with - None -> - (match key with - MSI msid -> - let kn' = replace_mp_in_con (MPself msid) mp kn in - apply_opt_resolver resolve' kn' - | MBI mbid -> - let kn' = replace_mp_in_con (MPbound mbid) mp kn in - apply_opt_resolver resolve' kn' - | MPI mp1 -> - let kn' = replace_mp_in_con mp1 mp kn in - apply_opt_resolver resolve' kn') - | Some t -> Some (subst_mps sub t)) res) - with - BothSubstitutionsAreIdentitySubstitutions -> None - | ChangeDomain res -> - let rec changeDom = function - | [] -> [] - | (kn,topt)::r -> - let key' = - match key with - MSI msid -> MPself msid - | MBI mbid -> MPbound mbid - | MPI mp1 -> mp1 in - let kn' = replace_mp_in_con mp key' kn in - if kn==kn' then - (*the key does not appear in kn, we remove it - from the resolver that we are building*) - changeDom r - else - (kn',topt)::(changeDom r) - in - Some (changeDom res) + | Some (mp',resolve') -> mp' + ,Some resolve' in + let resolve'' : delta_resolver = + match resolve' with + Some res -> + add_delta_resolver + (subst_dom_codom_delta_resolver sub resolve) + res + | None -> + subst_codom_delta_resolver sub resolve in mp',resolve'' in - Umap.mapi (apply_subst subst2) subst1 + let subst = Umap.mapi (apply_subst subst2) subst1 in + (Umap.fold Umap.add subst2 subst) -let remove_alias subst = - let rec remove key (mp,resolve) sub = - match key with - MPI _ -> sub - | _ -> Umap.add key (mp,resolve) sub - in - Umap.fold remove subst empty_subst let rec occur_in_path uid path = match uid,path with - | MSI sid,MPself sid' -> sid = sid' | MBI bid,MPbound bid' -> bid = bid' | _,MPdot (mp1,_) -> occur_in_path uid mp1 | _ -> false @@ -471,7 +657,7 @@ let occur_uid uid sub = false with Exit -> true -let occur_msid uid = occur_uid (MSI uid) + let occur_mbid uid = occur_uid (MBI uid) type 'a lazy_subst = diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index d30168a1bf..a948d1647f 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -13,26 +13,74 @@ open Names open Term -type resolver +(* A delta_resolver maps name (constant, inductive, module_path) + to canonical name *) +type delta_resolver + type substitution -val make_resolver : (constant * constr option) list -> resolver +val empty_delta_resolver : delta_resolver + +val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver + +val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver + -> delta_resolver + +val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver + +val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver + +val add_mp_delta_resolver : module_path -> module_path -> delta_resolver + -> delta_resolver + +val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver + +(* Apply the substitution on the domain of the resolver *) +val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver + +(* Apply the substitution on the codomain of the resolver *) +val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver + +val subst_dom_codom_delta_resolver : + substitution -> delta_resolver -> delta_resolver + +(* *_of_delta return the associated name of arg2 in arg1 *) +val constant_of_delta : delta_resolver -> constant -> constant + +val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive + +val delta_of_mp : delta_resolver -> module_path -> module_path + +(* Extract the set of inlined constant in the resolver *) +val inline_of_delta : delta_resolver -> kernel_name list + +(* remove_mp is used for the computation of a resolver induced by Include P *) +val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver + + +(* mem tests *) +val mp_in_delta : module_path -> delta_resolver -> bool + +val con_in_delta : constant -> delta_resolver -> bool + +val mind_in_delta : mutual_inductive -> delta_resolver -> bool + +(*substitution*) val empty_subst : substitution -val add_msid : - mod_self_id -> module_path -> substitution -> substitution +(* add_* add [arg2/arg1]{arg3} to the substitution with no + sequential composition *) val add_mbid : - mod_bound_id -> module_path -> resolver option -> substitution -> substitution + mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution val add_mp : - module_path -> module_path -> substitution -> substitution + module_path -> module_path -> delta_resolver -> substitution -> substitution -val map_msid : - mod_self_id -> module_path -> substitution +(* map_* create a new substitution [arg2/arg1]{arg3} *) val map_mbid : - mod_bound_id -> module_path -> resolver option -> substitution + mod_bound_id -> module_path -> delta_resolver -> substitution val map_mp : - module_path -> module_path -> substitution + module_path -> module_path -> delta_resolver -> substitution (* sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -47,6 +95,8 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted (*i debugging *) val debug_string_of_subst : substitution -> string val debug_pr_subst : substitution -> Pp.std_ppcmds +val debug_string_of_delta : delta_resolver -> string +val debug_pr_delta : delta_resolver -> Pp.std_ppcmds (*i*) (* [subst_mp sub mp] guarantees that whenever the result of the @@ -56,7 +106,10 @@ val debug_pr_subst : substitution -> Pp.std_ppcmds val subst_mp : substitution -> module_path -> module_path -val subst_kn : +val subst_ind : + substitution -> mutual_inductive -> mutual_inductive + +val subst_kn : substitution -> kernel_name -> kernel_name val subst_con : @@ -71,7 +124,7 @@ val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference (* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) -val replace_mp_in_con : module_path -> module_path -> constant -> constant +val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name (* [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) @@ -80,15 +133,5 @@ val subst_mps : substitution -> constr -> constr (* [occur_*id id sub] returns true iff [id] occurs in [sub] on either side *) -val occur_msid : mod_self_id -> substitution -> bool val occur_mbid : mod_bound_id -> substitution -> bool -val update_subst_alias : substitution -> substitution -> substitution - -val update_subst : substitution -> substitution -> substitution - -val subst_key : substitution -> substitution -> substitution - -val join_alias : substitution -> substitution -> substitution - -val remove_alias : substitution -> substitution diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 3d55fb69a2..48928470a7 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -37,52 +37,32 @@ let rec list_fold_map2 f e = function let e'',t1',t2' = list_fold_map2 f e' t in e'',h1'::t1',h2'::t2' +let discr_resolver env mtb = + match mtb.typ_expr with + SEBstruct _ -> + mtb.typ_delta + | _ -> (*case mp is a functor *) + empty_delta_resolver + let rec rebuild_mp mp l = match l with []-> mp - | i::r -> rebuild_mp (MPdot(mp,i)) r - -let type_of_struct env b meb = - let rec aux env = function - | SEBfunctor (mp,mtb,body) -> - let env = add_module (MPbound mp) (module_body_of_type mtb) env in - SEBfunctor(mp,mtb, aux env body) - | SEBident mp -> - strengthen env (lookup_modtype mp env).typ_expr mp - | SEBapply _ as mtb -> eval_struct env mtb - | str -> str - in - if b then - Some (aux env meb) - else - None - -let rec bounded_str_expr = function - | SEBfunctor (mp,mtb,body) -> bounded_str_expr body - | SEBident mp -> (check_bound_mp mp) - | SEBapply (f,a,_)->(bounded_str_expr f) - | _ -> false - -let return_opt_type mp env mtb = - if (check_bound_mp mp) then - Some (strengthen env mtb.typ_expr mp) - else - None - -let rec check_with env mtb with_decl = + | i::r -> rebuild_mp (MPdot(mp,i)) r + +let rec check_with env sign with_decl alg_sign mp equiv = match with_decl with | With_Definition (id,_) -> - let cb = check_with_aux_def env mtb with_decl in - SEBwith(mtb,With_definition_body(id,cb)),empty_subst - | With_Module (id,mp) -> - let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in - SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub - -and check_with_aux_def env mtb with_decl = - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> - msid,sig_b - | _ -> error_signature_expected mtb + let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in + sign,Some (SEBwith(alg_sign,With_definition_body(id,cb))),equiv,cst + | With_Module (id,mp1) -> + let sign,equiv,cst = + check_with_aux_mod env sign with_decl mp equiv in + sign,Some (SEBwith(alg_sign,With_module_body(id,mp1))),equiv,cst + +and check_with_aux_def env sign with_decl mp equiv = + let sig_b = match sign with + | SEBstruct(sig_b) -> sig_b + | _ -> error_signature_expected sign in let id,idl = match with_decl with | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl @@ -92,7 +72,7 @@ and check_with_aux_def env mtb with_decl = try let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in - let env' = Modops.add_signature (MPself msid) before env in + let env' = Modops.add_signature mp before equiv env in match with_decl with | With_Definition ([],_) -> assert false | With_Definition ([id],c) -> @@ -116,7 +96,7 @@ and check_with_aux_def env mtb with_decl = const_body_code = Cemitcodes.from_val (compile_constant_body env' body false false); const_constraints = cst} in - cb' + SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst | Some b -> let cst1 = Reduction.conv env' c (Declarations.force b) in let cst = Constraint.union cb.const_constraints cst1 in @@ -126,9 +106,9 @@ and check_with_aux_def env mtb with_decl = const_body_code = Cemitcodes.from_val (compile_constant_body env' body false false); const_constraints = cst} in - cb' + SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst end - | With_Definition (_::_,_) -> + | With_Definition (_::_,c) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -136,10 +116,14 @@ and check_with_aux_def env mtb with_decl = begin match old.mod_expr with | None -> - let new_with_decl = match with_decl with - With_Definition (_,c) -> With_Definition (idl,c) - | With_Module (_,c) -> With_Module (idl,c) in - check_with_aux_def env' (type_of_mb env old) new_with_decl + let new_with_decl = With_Definition (idl,c) in + let sign,cb,cst = + check_with_aux_def env' old.mod_type new_with_decl + (MPdot(mp,l)) old.mod_delta in + let new_spec = SFBmodule({old with + mod_type = sign; + mod_type_alg = None}) in + SEBstruct(before@((l,new_spec)::after)),cb,cst | Some msb -> error_a_generative_module_expected l end @@ -148,11 +132,10 @@ and check_with_aux_def env mtb with_decl = Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl now = - let initmsid,msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in - msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) - | _ -> error_signature_expected mtb +and check_with_aux_mod env sign with_decl mp equiv = + let sig_b = match sign with + | SEBstruct(sig_b) ->sig_b + | _ -> error_signature_expected sign in let id,idl = match with_decl with | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl @@ -163,172 +146,234 @@ and check_with_aux_mod env mtb with_decl now = let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in let rec mp_rec = function - | [] -> MPself initmsid + | [] -> mp | i::r -> MPdot(mp_rec r,label_of_id i) in - let env' = Modops.add_signature (MPself msid) before env in + let env' = Modops.add_signature mp before equiv env in match with_decl with | With_Module ([],_) -> assert false - | With_Module ([id], mp) -> - let old,alias = match spec with - SFBmodule msb -> Some msb,None - | SFBalias (mp',_,cst) -> None,Some (mp',cst) + | With_Module ([id], mp1) -> + let old = match spec with + SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) in - let mtb' = lookup_modtype mp env' in + let mb_mp1 = (lookup_module mp1 env) in + let mtb_mp1 = + module_type_of_module env' None mb_mp1 in let cst = - match old,alias with - Some msb,None -> + match old.mod_expr with + None -> begin try Constraint.union - (check_subtypes env' mtb' (module_type_of_module None msb)) - msb.mod_constraints + (check_subtypes env' mtb_mp1 + (module_type_of_module env' None old)) + old.mod_constraints with Failure _ -> error_with_incorrect (label_of_id id) end - | None,Some (mp',None) -> - check_modpath_equiv env' mp mp'; - Constraint.empty - | None,Some (mp',Some cst) -> - check_modpath_equiv env' mp mp'; - cst - | _,_ -> - anomaly "Mod_typing:no implementation and no alias" + | Some (SEBident(mp')) -> + check_modpath_equiv env' mp1 mp'; + old.mod_constraints + | _ -> error_a_generative_module_expected l + in + let new_mb = strengthen_and_subst_mb mb_mp1 + (MPdot(mp,l)) env false in + let new_spec = SFBmodule {new_mb with + mod_mp = MPdot(mp,l); + mod_expr = Some (SEBident mp1); + mod_constraints = cst} in + (* we propagate the new equality in the rest of the signature + with the identity substitution accompagned by the new resolver*) + let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in + SEBstruct(before@(l,new_spec)::subst_signature id_subst after), + add_delta_resolver equiv new_mb.mod_delta,cst + | With_Module (idc,mp1) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) in - if now then - let mp' = scrape_alias mp env' in - let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in - let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in - cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb') - else - cst,empty_subst,(return_opt_type mp env' mtb') - | With_Module (_::_,mp) -> - let old,alias = match spec with - SFBmodule msb -> Some msb, None - | SFBalias (mpold,typ_opt,cst)->None, Some mpold - | _ -> error_not_a_module (string_of_label l) - in begin - if alias = None then - let old = Option.get old in - match old.mod_expr with - None -> - let new_with_decl = match with_decl with - With_Definition (_,c) -> - With_Definition (idl,c) - | With_Module (_,c) -> With_Module (idl,c) in - let cst,_,typ_opt = - check_with_aux_mod env' - (type_of_mb env' old) new_with_decl false in - if now then - let mtb' = lookup_modtype mp env' in - let mp' = scrape_alias mp env' in - let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in - let up_subst = update_subst - sub (map_mp (mp_rec (List.rev (id::idl))) mp') in - cst, - (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst), - typ_opt - else - cst,empty_subst,typ_opt - | Some msb -> - error_a_generative_module_expected l - else - let mpold = Option.get alias in - let mpnew = rebuild_mp mpold (List.map label_of_id idl) in - check_modpath_equiv env' mpnew mp; - let mtb' = lookup_modtype mp env' in - Constraint.empty,empty_subst,(return_opt_type mp env' mtb') + match old.mod_expr with + None -> + let new_with_decl = With_Module (idl,mp1) in + let sign,equiv',cst = + check_with_aux_mod env' + old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in + let new_equiv = add_delta_resolver equiv equiv' in + let new_spec = SFBmodule {old with + mod_type = sign; + mod_type_alg = None; + mod_delta = equiv'} + in + let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in + SEBstruct(before@(l,new_spec)::subst_signature id_subst after), + new_equiv,cst + | Some (SEBident(mp')) -> + let mpnew = rebuild_mp mp' (List.map label_of_id idl) in + check_modpath_equiv env' mpnew mp; + SEBstruct(before@(l,spec)::after) + ,equiv,Constraint.empty + | _ -> + error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" + | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and translate_module env me = +and translate_module env mp me = match me.mod_entry_expr, me.mod_entry_type with | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" | None, Some mte -> - let mtb,sub = translate_struct_entry env mte in - { mod_expr = None; - mod_type = Some mtb; - mod_alias = sub; - mod_constraints = Constraint.empty; - mod_retroknowledge = []} - | Some mexpr, _ -> - let meb,sub1 = translate_struct_entry env mexpr in - let mod_typ,sub,cst = + let mtb = translate_module_type env mp mte in + { mod_mp = mp; + mod_expr = None; + mod_type = mtb.typ_expr; + mod_type_alg = mtb.typ_expr_alg; + mod_delta = mtb.typ_delta; + mod_constraints = mtb.typ_constraints; + mod_retroknowledge = []} + | Some mexpr, _ -> + let sign,alg_implem,resolver,cst1 = + translate_struct_module_entry env mp mexpr in + let sign,alg1,resolver,cst2 = match me.mod_entry_type with | None -> - (type_of_struct env (bounded_str_expr meb) meb) - ,sub1,Constraint.empty + sign,None,resolver,Constraint.empty | Some mte -> - let mtb2,sub2 = translate_struct_entry env mte in + let mtb = translate_module_type env mp mte in let cst = check_subtypes env - {typ_expr = meb; - typ_strength = None; - typ_alias = sub1;} - {typ_expr = mtb2; - typ_strength = None; - typ_alias = sub2;} + {typ_mp = mp; + typ_expr = sign; + typ_expr_alg = None; + typ_constraints = Constraint.empty; + typ_delta = resolver;} + mtb in - Some mtb2,sub2,cst + mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst in - { mod_type = mod_typ; - mod_expr = Some meb; - mod_constraints = cst; - mod_alias = sub; - mod_retroknowledge = []} (* spiwack: not so sure about that. It may - cause a bug when closing nested modules. - If it does, I don't really know how to - fix the bug.*) - - -and translate_struct_entry env mse = match mse with - | MSEident mp -> - let mtb = lookup_modtype mp env in - SEBident mp,mtb.typ_alias + { mod_mp = mp; + mod_type = sign; + mod_expr = Some alg_implem; + mod_type_alg = alg1; + mod_constraints = Univ.Constraint.union cst1 cst2; + mod_delta = resolver; + mod_retroknowledge = []} + (* spiwack: not so sure about that. It may + cause a bug when closing nested modules. + If it does, I don't really know how to + fix the bug.*) + + +and translate_struct_module_entry env mp mse = match mse with + | MSEident mp1 -> + let mb = lookup_module mp1 env in + let mb' = strengthen_and_subst_mb mb mp env false in + mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty | MSEfunctor (arg_id, arg_e, body_expr) -> - let arg_b,sub = translate_struct_entry env arg_e in - let mtb = - {typ_expr = arg_b; - typ_strength = None; - typ_alias = sub} in - let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in - let body_b,sub = translate_struct_entry env' body_expr in - SEBfunctor (arg_id, mtb, body_b),sub + let mtb = translate_module_type env (MPbound arg_id) arg_e in + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) + env in + let sign,alg,resolver,cst = translate_struct_module_entry env' + mp body_expr in + SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver, + Univ.Constraint.union cst mtb.typ_constraints | MSEapply (fexpr,mexpr) -> - let feb,sub1 = translate_struct_entry env fexpr in - let feb'= eval_struct env feb - in - let farg_id, farg_b, fbody_b = destr_functor env feb' in - let mtb,mp = + let sign,alg,resolver,cst1 = translate_struct_module_entry env mp fexpr in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mtb,mp1 = try - let mp = scrape_alias (path_of_mexpr mexpr) env in - lookup_modtype mp env,mp + let mp1 = path_of_mexpr mexpr in + let mtb = module_type_of_module env None (lookup_module mp1 env) in + mtb,mp1 with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in - let meb,sub2= translate_struct_entry env (MSEident mp) in - if sub1 = empty_subst then - let cst = check_subtypes env mtb farg_b in - SEBapply(feb,meb,cst),sub1 - else - let sub2 = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> - join_alias - (subst_key (map_msid msid mp) sub2) - (map_msid msid mp) - | _ -> sub2 in - let sub3 = join_alias sub1 (map_mbid farg_id mp None) in - let sub4 = update_subst sub2 sub3 in - let cst = check_subtypes env mtb farg_b in - SEBapply(feb,meb,cst),(join sub3 sub4) + let cst = check_subtypes env mtb farg_b in + let mp_delta = discr_resolver env mtb in + let mp_delta = complete_inline_delta_resolver env mp1 + farg_id farg_b mp_delta in + let subst = map_mbid farg_id mp1 mp_delta in + (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst), + (subst_codom_delta_resolver subst resolver), + Univ.Constraint.union cst1 cst | MSEwith(mte, with_decl) -> - let mtb,sub1 = translate_struct_entry env mte in - let mtb',sub2 = check_with env mtb with_decl in - mtb',join sub1 sub2 - + let sign,alg,resolve,cst1 = translate_struct_module_entry env mp mte in + let sign,alg,resolve,cst2 = check_with env sign with_decl alg mp resolve in + sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2 + +and translate_struct_type_entry env mse = match mse with + | MSEident mp1 -> + let mtb = lookup_modtype mp1 env in + mtb.typ_expr, + Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty + | MSEfunctor (arg_id, arg_e, body_expr) -> + let mtb = translate_module_type env (MPbound arg_id) arg_e in + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env' + body_expr in + SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from, + Univ.Constraint.union cst mtb.typ_constraints + | MSEapply (fexpr,mexpr) -> + let sign,alg,resolve,mp_from,cst1 = translate_struct_type_entry env fexpr in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mtb,mp1 = + try + let mp1 = path_of_mexpr mexpr in + let mtb = module_type_of_module env None (lookup_module mp1 env) in + mtb,mp1 + with + | Not_path -> error_application_to_not_path mexpr + (* place for nondep_supertype *) in + let cst2 = check_subtypes env mtb farg_b in + let mp_delta = discr_resolver env mtb in + let mp_delta = complete_inline_delta_resolver env mp1 + farg_id farg_b mp_delta in + let subst = map_mbid farg_id mp1 mp_delta in + (subst_struct_expr subst fbody_b),None, + (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2 + | MSEwith(mte, with_decl) -> + let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in + let sign,alg,resolve,cst1 = + check_with env sign with_decl (Option.get alg) mp_from resolve in + sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1 + +and translate_module_type env mp mte = + let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env mte in + subst_modtype_and_resolver + {typ_mp = mp_from; + typ_expr = sign; + typ_expr_alg = alg; + typ_constraints = cst; + typ_delta = resolve} mp env + +let rec translate_struct_include_module_entry env mp mse = match mse with + | MSEident mp1 -> + let mb = lookup_module mp1 env in + let mb' = strengthen_and_subst_mb mb mp env true in + mb'.mod_type, mb'.mod_delta,Univ.Constraint.empty + | MSEapply (fexpr,mexpr) -> + let sign,resolver,cst1 = + translate_struct_include_module_entry env mp fexpr in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mtb,mp1 = + try + let mp1 = path_of_mexpr mexpr in + let mtb = module_type_of_module env None (lookup_module mp1 env) in + mtb,mp1 + with + | Not_path -> error_application_to_not_path mexpr + (* place for nondep_supertype *) in + let cst = check_subtypes env mtb farg_b in + let mp_delta = discr_resolver env mtb in + let mp_delta = complete_inline_delta_resolver env mp1 + farg_id farg_b mp_delta in + let subst = map_mbid farg_id mp1 mp_delta in + (subst_struct_expr subst fbody_b), + (subst_codom_delta_resolver subst resolver), + Univ.Constraint.union cst1 cst + | _ -> error ("You cannot Include a high-order structure.") + let rec add_struct_expr_constraints env = function | SEBident _ -> env @@ -337,7 +382,7 @@ let rec add_struct_expr_constraints env = function add_struct_expr_constraints (add_modtype_constraints env mtb) meb - | SEBstruct (_,structure_body) -> + | SEBstruct (structure_body) -> List.fold_left (fun env (l,item) -> add_struct_elem_constraints env item) env @@ -351,16 +396,13 @@ let rec add_struct_expr_constraints env = function | SEBwith(meb,With_definition_body(_,cb))-> Environ.add_constraints cb.const_constraints (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,_,cst))-> - Environ.add_constraints cst - (add_struct_expr_constraints env meb) - -and add_struct_elem_constraints env = function + | SEBwith(meb,With_module_body(_,_))-> + add_struct_expr_constraints env meb + +and add_struct_elem_constraints env = function | SFBconst cb -> Environ.add_constraints cb.const_constraints env | SFBmind mib -> Environ.add_constraints mib.mind_constraints env | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,_,None) -> env | SFBmodtype mtb -> add_modtype_constraints env mtb and add_module_constraints env mb = @@ -368,15 +410,14 @@ and add_module_constraints env mb = | None -> env | Some meb -> add_struct_expr_constraints env meb in - let env = match mb.mod_type with - | None -> env - | Some mtb -> - add_struct_expr_constraints env mtb + let env = + add_struct_expr_constraints env mb.mod_type in Environ.add_constraints mb.mod_constraints env and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb.typ_expr + Environ.add_constraints mtb.typ_constraints + (add_struct_expr_constraints env mtb.typ_expr) let rec struct_expr_constraints cst = function @@ -386,7 +427,7 @@ let rec struct_expr_constraints cst = function struct_expr_constraints (modtype_constraints cst mtb) meb - | SEBstruct (_,structure_body) -> + | SEBstruct (structure_body) -> List.fold_left (fun cst (l,item) -> struct_elem_constraints cst item) cst @@ -399,28 +440,25 @@ let rec struct_expr_constraints cst = function | SEBwith(meb,With_definition_body(_,cb))-> struct_expr_constraints (Univ.Constraint.union cb.const_constraints cst) meb - | SEBwith(meb,With_module_body(_,_,_,cst1))-> - struct_expr_constraints (Univ.Constraint.union cst1 cst) meb - -and struct_elem_constraints cst = function + | SEBwith(meb,With_module_body(_,_))-> + struct_expr_constraints cst meb + +and struct_elem_constraints cst = function | SFBconst cb -> cst | SFBmind mib -> cst | SFBmodule mb -> module_constraints cst mb - | SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst - | SFBalias (mp,_,None) -> cst | SFBmodtype mtb -> modtype_constraints cst mtb and module_constraints cst mb = let cst = match mb.mod_expr with | None -> cst | Some meb -> struct_expr_constraints cst meb in - let cst = match mb.mod_type with - | None -> cst - | Some mtb -> struct_expr_constraints cst mtb in + let cst = + struct_expr_constraints cst mb.mod_type in Univ.Constraint.union mb.mod_constraints cst and modtype_constraints cst mtb = - struct_expr_constraints cst mtb.typ_expr + struct_expr_constraints (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 1fadec2ad9..746a80e151 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -13,13 +13,24 @@ open Declarations open Environ open Entries open Mod_subst +open Names (*i*) -val translate_module : env -> module_entry -> module_body +val translate_module : env -> module_path -> module_entry + -> module_body -val translate_struct_entry : env -> module_struct_entry -> - struct_expr_body * substitution +val translate_module_type : env -> module_path -> module_struct_entry -> + module_type_body + +val translate_struct_module_entry : env -> module_path -> module_struct_entry -> + struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints + +val translate_struct_type_entry : env -> module_struct_entry -> + struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints + +val translate_struct_include_module_entry : env -> module_path + -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints val add_modtype_constraints : env -> module_type_body -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 3f38cc2f7c..8193c02e53 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -22,7 +22,7 @@ open Mod_subst -let error_existing_label l = +let error_existing_label l = error ("The label "^string_of_label l^" is already declared.") let error_declaration_not_path _ = error "Declaration is not a path." @@ -39,31 +39,31 @@ let error_not_match l _ = error ("Signature components for label "^string_of_lab let error_no_such_label l = error ("No such label "^string_of_label l^".") -let error_incompatible_labels l l' = +let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") -let error_result_must_be_signature () = +let error_result_must_be_signature () = error "The result module type must be a signature." let error_signature_expected mtb = error "Signature expected." -let error_no_module_to_end _ = +let error_no_module_to_end _ = error "No open module to end." let error_no_modtype_to_end _ = error "No open module type to end." -let error_not_a_modtype_loc loc s = +let error_not_a_modtype_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) -let error_not_a_module_loc loc s = +let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) let error_not_a_module s = error_not_a_module_loc dummy_loc s -let error_not_a_constant l = +let error_not_a_constant l = error ("\""^(string_of_label l)^"\" is not a constant.") let error_with_incorrect l = @@ -74,28 +74,17 @@ let error_a_generative_module_expected l = "component of generative modules can be changed using the \"with\" " ^ "construct.") -let error_local_context lo = +let error_local_context lo = match lo with - None -> + None -> error ("The local context is not empty.") | (Some l) -> error ("The local context of the component "^ (string_of_label l)^" is not empty.") -let error_no_such_label_sub l l1 l2 = - error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".") - - - -let rec list_split_assoc k rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail - -let path_of_seb = function - | SEBident mp -> mp - | _ -> anomaly "Modops: evaluation failed." +let error_no_such_label_sub l l1 = + error ("The field "^(string_of_label l)^" is missing in "^l1^".") let destr_functor env mtb = @@ -104,123 +93,126 @@ let destr_functor env mtb = (arg_id,arg_t,body_t) | _ -> error_not_a_functor mtb -(* the constraints are not important here *) +let is_functor = function + | SEBfunctor (arg_id,arg_t,body_t) -> true + | _ -> false -let module_body_of_type mtb = - { mod_type = Some mtb.typ_expr; +let module_body_of_type mp mtb = + { mod_mp = mp; + mod_type = mtb.typ_expr; + mod_type_alg = mtb.typ_expr_alg; mod_expr = None; - mod_constraints = Constraint.empty; - mod_alias = mtb.typ_alias; + mod_constraints = mtb.typ_constraints; + mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let module_type_of_module mp mb = - let mp1,expr = - (match mb.mod_type with - | Some expr -> mp,expr - | None -> (match mb.mod_expr with - | Some (SEBident mp') ->(Some mp'),(SEBident mp') - | Some expr -> mp,expr - | None -> - anomaly "Modops: empty expr and type")) in - {typ_expr = expr; - typ_alias = mb.mod_alias; - typ_strength = mp1 - } - -let rec check_modpath_equiv env mp1 mp2 = +let check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else - let mp1 = scrape_alias mp1 env in - let mp2 = scrape_alias mp2 env in - if mp1=mp2 then () - else - error_not_equal mp1 mp2 - + let mb1=lookup_module mp1 env in + let mb2=lookup_module mp2 env in + if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) + then () + else error_not_equal mp1 mp2 + let rec subst_with_body sub = function - | With_module_body(id,mp,typ_opt,cst) -> - With_module_body(id,subst_mp sub mp,Option.smartmap - (subst_struct_expr sub) typ_opt,cst) + | With_module_body(id,mp) -> + With_module_body(id,subst_mp sub mp) | With_definition_body(id,cb) -> With_definition_body( id,subst_const_body sub cb) -and subst_modtype sub mtb = - let typ_expr' = subst_struct_expr sub mtb.typ_expr in - let sub_mtb = join_alias mtb.typ_alias sub in - if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then - mtb +and subst_modtype sub do_delta mtb= + let mp = subst_mp sub mtb.typ_mp in + let sub = add_mp mtb.typ_mp mp empty_delta_resolver sub in + let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in + let typ_alg' = + Option.smartmap + (subst_struct_expr sub (fun x -> x)) mtb.typ_expr_alg in + let mtb_delta = do_delta mtb.typ_delta in + if typ_expr'==mtb.typ_expr && + typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then + mtb else - { mtb with - typ_expr = typ_expr'; - typ_alias = sub_mtb} - -and subst_structure sub sign = - let subst_body = function - SFBconst cb -> + {mtb with + typ_mp = mp; + typ_expr = typ_expr'; + typ_expr_alg = typ_alg'; + typ_delta = mtb_delta} + +and subst_structure sub do_delta sign = + let subst_body = function + SFBconst cb -> SFBconst (subst_const_body sub cb) - | SFBmind mib -> + | SFBmind mib -> SFBmind (subst_mind sub mib) - | SFBmodule mb -> - SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> - SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,typ_opt,cst) -> - SFBalias (subst_mp sub mp,Option.smartmap - (subst_struct_expr sub) typ_opt,cst) + | SFBmodule mb -> + SFBmodule (subst_module sub do_delta mb) + | SFBmodtype mtb -> + SFBmodtype (subst_modtype sub do_delta mtb) in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = - let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in - (* This is similar to the previous case. In this case we have - a module M in a signature that is knows to be equivalent to a module M' - (because the signature is "K with Module M := M'") and we are substituting - M' with some M''. *) - let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in - let mb_alias = update_subst sub mb.mod_alias in - let mb_alias = if mb_alias = empty_subst then - join_alias mb.mod_alias sub - else - join mb_alias (join_alias mb.mod_alias sub) - in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mb_alias == mb.mod_alias +and subst_module sub do_delta mb = + let mp = subst_mp sub mb.mod_mp in + let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then + add_mp mb.mod_mp mp + empty_delta_resolver sub else sub in + let id_delta = (fun x -> x) in + let mtb',me' = + let mtb = subst_struct_expr sub do_delta mb.mod_type in + match mb.mod_expr with + None -> mtb,None + | Some me -> if me==mb.mod_type then + mtb,Some mtb + else mtb,Option.smartmap + (subst_struct_expr sub id_delta) mb.mod_expr + in + let typ_alg' = Option.smartmap + (subst_struct_expr sub id_delta) mb.mod_type_alg in + let mb_delta = do_delta mb.mod_delta in + if mtb'==mb.mod_type && mb.mod_expr == me' + && mb_delta == mb.mod_delta && mp == mb.mod_mp then mb else - { mod_expr = me'; - mod_type=mtb'; - mod_constraints=mb.mod_constraints; - mod_alias = mb_alias; - mod_retroknowledge=mb.mod_retroknowledge} - - -and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (msid, mtb, meb') -> - SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') - | SEBstruct (msid,str)-> - SEBstruct(msid, subst_structure sub str) + { mb with + mod_mp = mp; + mod_expr = me'; + mod_type_alg = typ_alg'; + mod_type=mtb'; + mod_delta = mb_delta} + +and subst_struct_expr sub do_delta = function + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (mbid, mtb, meb') -> + SEBfunctor(mbid,subst_modtype sub do_delta mtb + ,subst_struct_expr sub do_delta meb') + | SEBstruct (str)-> + SEBstruct( subst_structure sub do_delta str) | SEBapply (meb1,meb2,cst)-> - SEBapply(subst_struct_expr sub meb1, - subst_struct_expr sub meb2, + SEBapply(subst_struct_expr sub do_delta meb1, + subst_struct_expr sub do_delta meb2, cst) - | SEBwith (meb,wdb)-> - SEBwith(subst_struct_expr sub meb, + | SEBwith (meb,wdb)-> + SEBwith(subst_struct_expr sub do_delta meb, subst_with_body sub wdb) +let subst_signature subst = + subst_structure subst + (fun resolver -> subst_codom_delta_resolver subst resolver) -let subst_signature_msid msid mp = - subst_structure (map_msid msid mp) +let subst_struct_expr subst = + subst_struct_expr subst + (fun resolver -> subst_codom_delta_resolver subst resolver) -(* spiwack: here comes the function which takes care of importing +(* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge msid mp = - let subst = add_msid msid mp empty_subst in - let subst_and_perform rkaction env = +let add_retroknowledge mp = + let perform rkaction env = match rkaction with | Retroknowledge.RKRegister (f, e) -> - Environ.register env f - (match e with - | Const kn -> kind_of_term (subst_mps subst (mkConst kn)) - | Ind ind -> kind_of_term (subst_mps subst (mkInd ind)) + Environ.register env f + (match e with + | Const kn -> kind_of_term (mkConst kn) + | Ind ind -> kind_of_term (mkInd ind) | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term") in fun lclrk env -> @@ -229,305 +221,283 @@ let add_retroknowledge msid mp = int31 type registration absolutely needs int31 bits to be registered. Since the local_retroknowledge is stored in reverse order (each new registration is added at the top of the list) we need a fold_right - for things to go right (the pun is not intented). So we lose + for things to go right (the pun is not intented). So we lose tail recursivity, but the world will have exploded before any module imports 10 000 retroknowledge registration.*) - List.fold_right subst_and_perform lclrk env + List.fold_right perform lclrk env +let rec add_signature mp sign resolver env = + let add_one env (l,elem) = + let kn = make_kn mp empty_dirpath l in + let con = constant_of_kn kn in + let mind = mind_of_kn kn in + match elem with + | SFBconst cb -> + let con = constant_of_delta resolver con in + Environ.add_constant con cb env + | SFBmind mib -> + let mind = mind_of_delta resolver mind in + Environ.add_mind mind mib env + | SFBmodule mb -> add_module mb env + (* adds components as well *) + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env + in + List.fold_left add_one env sign +and add_module mb env = + let mp = mb.mod_mp in + let env = Environ.shallow_add_module mp mb env in + match mb.mod_type with + | SEBstruct (sign) -> + add_retroknowledge mp mb.mod_retroknowledge + (add_signature mp sign mb.mod_delta env) + | SEBfunctor _ -> env + | _ -> anomaly "Modops:the evaluation of the structure failed " -let strengthen_const env mp l cb = +let strengthen_const env mp_from l cb resolver = match cb.const_opaque, cb.const_body with | false, Some _ -> cb - | true, Some _ + | true, Some _ | _, None -> - let const = mkConst (make_con mp empty_dirpath l) in + let con = make_con mp_from empty_dirpath l in + let con = constant_of_delta resolver con in + let const = mkConst con in let const_subs = Some (Declarations.from_val const) in - {cb with + {cb with const_body = const_subs; const_opaque = false; const_body_code = Cemitcodes.from_val (compile_constant_body env const_subs false false) } - -let strengthen_mind env mp l mib = match mib.mind_equiv with - | Some _ -> mib - | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} - - -let rec eval_struct env = function - | SEBident mp -> - begin - let mtb =lookup_modtype mp env in - match mtb.typ_expr,mtb.typ_strength with - mtb,None -> eval_struct env mtb - | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) - end - | SEBapply (seb1,seb2,_) -> - let svb1 = eval_struct env seb1 in - let farg_id, farg_b, fbody_b = destr_functor env svb1 in - let mp = path_of_seb seb2 in - let mp = scrape_alias mp env in - let sub_alias = (lookup_modtype mp env).typ_alias in - let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> - join_alias - (subst_key (map_msid msid mp) sub_alias) - (map_msid msid mp) - | _ -> sub_alias in - let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in - let sub_alias1 = update_subst sub_alias - (map_mbid farg_id mp (Some resolve)) in - eval_struct env (subst_struct_expr - (join sub_alias1 - (map_mbid farg_id mp (Some resolve))) fbody_b) - | SEBwith (mtb,(With_definition_body _ as wdb)) -> - let mtb',_ = merge_with env mtb wdb empty_subst in - mtb' - | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) -> - let alias_in_mp = - (lookup_modtype mp env).typ_alias in - let alias_in_mp = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp - | _ -> alias_in_mp in - let mtb',_ = merge_with env mtb wdb alias_in_mp in - mtb' -(* | SEBfunctor(mbid,mtb,body) -> - let env = add_module (MPbound mbid) (module_body_of_type mtb) env in - SEBfunctor(mbid,mtb,eval_struct env body) *) - | mtb -> mtb - -and type_of_mb env mb = - match mb.mod_type,mb.mod_expr with - None,Some b -> eval_struct env b - | Some t, _ -> eval_struct env t - | _,_ -> anomaly - "Modops: empty type and empty expr" - -and merge_with env mtb with_decl alias= - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> msid,sig_b - | _ -> error_signature_expected mtb - in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false - in - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc l [] sig_b in - let before = List.rev rev_before in - let rec mp_rec = function - | [] -> MPself msid - | i::r -> MPdot(mp_rec r,label_of_id i) - in - let env' = add_signature (MPself msid) before env in - let new_spec,subst = match with_decl with - | With_definition_body ([],_) - | With_module_body ([],_,_,_) -> assert false - | With_definition_body ([id],c) -> - SFBconst c,None - | With_module_body ([id], mp,typ_opt,cst) -> - let mp' = scrape_alias mp env' in - let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in - SFBalias (mp,typ_opt,Some cst), - Some(join (map_mp (mp_rec [id]) mp') new_alias) - | With_definition_body (_::_,_) - | With_module_body (_::_,_,_,_) -> - let old,aliasold = match spec with - SFBmodule msb -> Some msb, None - | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst) - | _ -> error_not_a_module (string_of_label l) - in - if aliasold = None then - let old = Option.get old in - let new_with_decl,subst1 = - match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,typ_opt,cst) -> - let mp' = scrape_alias mp env' in - With_module_body (idl,mp,typ_opt,cst), - Some(map_mp (mp_rec (List.rev idc)) mp') - in - let subst = match subst1 with - | None -> None - | Some s -> Some (join s (update_subst alias s)) in - let modtype,subst_msb = - merge_with env' (type_of_mb env' old) new_with_decl alias in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_constraints = old.mod_constraints; - mod_alias = begin - match subst_msb with - |None -> empty_subst - |Some s -> s - end; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb),subst + + +let rec strengthen_mod env mp_from mp_to mb = + assert(mp_from = mb.mod_mp); + if mp_in_delta mb.mod_mp mb.mod_delta then + mb + else + match mb.mod_type with + | SEBstruct (sign) -> + let resolve_out,sign_out = + strengthen_sig env mp_from sign mp_to mb.mod_delta in + { mb with + mod_expr = Some (SEBident mp_to); + mod_type = SEBstruct(sign_out); + mod_type_alg = mb.mod_type_alg; + mod_constraints = mb.mod_constraints; + mod_delta = add_mp_delta_resolver mp_from mp_to + (add_delta_resolver mb.mod_delta resolve_out); + mod_retroknowledge = mb.mod_retroknowledge} + | SEBfunctor _ -> mb + | _ -> anomaly "Modops:the evaluation of the structure failed " + +and strengthen_sig env mp_from sign mp_to resolver = + match sign with + | [] -> empty_delta_resolver,[] + | (l,SFBconst cb) :: rest -> + let item' = + l,SFBconst (strengthen_const env mp_from l cb resolver) in + let resolve_out,rest' = + strengthen_sig env mp_from rest mp_to resolver in + resolve_out,item'::rest' + | (_,SFBmind _ as item):: rest -> + let resolve_out,rest' = + strengthen_sig env mp_from rest mp_to resolver in + resolve_out,item::rest' + | (l,SFBmodule mb) :: rest -> + let mp_from' = MPdot (mp_from,l) in + let mp_to' = MPdot(mp_to,l) in + let mb_out = + strengthen_mod env mp_from' mp_to' mb in + let item' = l,SFBmodule (mb_out) in + let env' = add_module mb_out env in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + add_delta_resolver resolve_out mb.mod_delta, + item':: rest' + | (l,SFBmodtype mty as item) :: rest -> + let env' = add_modtype + (MPdot(mp_from,l)) mty env + in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + resolve_out,item::rest' + +let strengthen env mtb mp = + if mp_in_delta mtb.typ_mp mtb.typ_delta then + (* in this case mtb has already been strengthened*) + mtb + else + match mtb.typ_expr with + | SEBstruct (sign) -> + let resolve_out,sign_out = + strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in + {mtb with + typ_expr = SEBstruct(sign_out); + typ_delta = add_delta_resolver mtb.typ_delta + (add_mp_delta_resolver mtb.typ_mp mp resolve_out)} + | SEBfunctor _ -> mtb + | _ -> anomaly "Modops:the evaluation of the structure failed " + +let module_type_of_module env mp mb = + match mp with + Some mp -> + strengthen env { + typ_mp = mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} mp + + | None -> + {typ_mp = mb.mod_mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} + +let complete_inline_delta_resolver env mp mbid mtb delta = + let constants = inline_of_delta mtb.typ_delta in + let rec make_inline delta = function + | [] -> delta + | kn::r -> + let kn = replace_mp_in_kn (MPbound mbid) mp kn in + let con = constant_of_kn kn in + let con' = constant_of_delta delta con in + let constant = lookup_constant con' env in + if (not constant.Declarations.const_opaque) then + let constr = Option.map Declarations.force + constant.Declarations.const_body in + if constr = None then + (make_inline delta r) else - let mpold,typ_opt,cst = Option.get aliasold in - SFBalias (mpold,typ_opt,cst),None - in - SEBstruct(msid, before@(l,new_spec):: - (Option.fold_right subst_structure subst after)),subst - with - Not_found -> error_no_such_label l - -and add_signature mp sign env = - let add_one env (l,elem) = - let kn = make_kn mp empty_dirpath l in - let con = make_con mp empty_dirpath l in - match elem with - | SFBconst cb -> Environ.add_constant con cb env - | SFBmind mib -> Environ.add_mind kn mib env - | SFBmodule mb -> - add_module (MPdot (mp,l)) mb env - (* adds components as well *) - | SFBalias (mp1,_,cst) -> - Environ.register_alias (MPdot(mp,l)) mp1 env - | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) - mtb env + add_inline_constr_delta_resolver con (Option.get constr) + (make_inline delta r) + else + (make_inline delta r) in - List.fold_left add_one env sign - -and add_module mp mb env = - let env = Environ.shallow_add_module mp mb env in - let env = - Environ.add_modtype mp (module_type_of_module (Some mp) mb) env - in - let mod_typ = type_of_mb env mb in - match mod_typ with - | SEBstruct (msid,sign) -> - add_retroknowledge msid mp (mb.mod_retroknowledge) - (add_signature mp (subst_signature_msid msid mp sign) env) - | SEBfunctor _ -> env - | _ -> anomaly "Modops:the evaluation of the structure failed " - - - -and constants_of_specification env mp sign = - let aux (env,res) (l,elem) = - match elem with - | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SFBmind _ -> env,res - | SFBmodule mb -> - let new_env = add_module (MPdot (mp,l)) mb env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (type_of_mb env mb)) @ res - | SFBalias (mp1,typ_opt,cst) -> - let new_env = register_alias (MPdot (mp,l)) mp1 env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (eval_struct env (SEBident mp1))) @ res - | SFBmodtype mtb -> - (* module type dans un module type. - Il faut au moins mettre mtb dans l'environnement (avec le bon - kn pour pouvoir continuer aller deplier les modules utilisant ce - mtb - ex: - Module Type T1. - Module Type T2. - .... - End T2. - ..... - Declare Module M : T2. - End T2 - si on ne rajoute pas T2 dans l'environement de typage - on va exploser au moment du Declare Module - *) - let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in - new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res - in - snd (List.fold_left aux (env,[]) sign) - -and constants_of_modtype env mp modtype = - match (eval_struct env modtype) with - SEBstruct (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | SEBfunctor _ -> [] - | _ -> anomaly "Modops:the evaluation of the structure failed " - -(* returns a resolver for kn that maps mbid to mp. We only keep - constants that have the inline flag *) -and resolver_of_environment mbid modtype mp alias env = - let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in - let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in - let rec make_resolve = function - | [] -> [] - | (con,expecteddef)::r -> - let con' = replace_mp_in_con (MPbound mbid) mp con in - let con',_ = subst_con alias con' in - (* let con' = replace_mp_in_con (MPbound mbid) mp con' in *) - try - if expecteddef.Declarations.const_inline then - let constant = lookup_constant con' env in - if (not constant.Declarations.const_opaque) then - let constr = Option.map Declarations.force - constant.Declarations.const_body in - (con,constr)::(make_resolve r) - else make_resolve r - else make_resolve r - with Not_found -> error_no_such_label (con_label con') - in - let resolve = make_resolve constants in - Mod_subst.make_resolver resolve - - -and strengthen_mtb env mp mtb = - let mtb1 = eval_struct env mtb in - match mtb1 with - | SEBfunctor _ -> mtb1 - | SEBstruct (msid,sign) -> - SEBstruct (msid,strengthen_sig env msid sign mp) - | _ -> anomaly "Modops:the evaluation of the structure failed " - -and strengthen_mod env mp mb = - let mod_typ = type_of_mb env mb in - { mod_expr = mb.mod_expr; - mod_type = Some (strengthen_mtb env mp mod_typ); - mod_constraints = mb.mod_constraints; - mod_alias = mb.mod_alias; - mod_retroknowledge = mb.mod_retroknowledge} - -and strengthen_sig env msid sign mp = match sign with - | [] -> [] - | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const env mp l cb) in - let rest' = strengthen_sig env msid rest mp in + make_inline delta constants + +let rec strengthen_and_subst_mod + mb subst env mp_from mp_to env resolver = + match mb.mod_type with + SEBstruct(str) -> + let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in + if mb_is_an_alias then + subst_module subst + (fun resolver -> subst_dom_delta_resolver subst resolver) mb + else + let resolver,new_sig = + strengthen_and_subst_struct str subst env + mp_from mp_from mp_to false false mb.mod_delta + in + {mb with + mod_mp = mp_to; + mod_expr = Some (SEBident mp_from); + mod_type = SEBstruct(new_sig); + mod_delta = add_mp_delta_resolver mp_to mp_from resolver} + | SEBfunctor(arg_id,arg_b,body) -> + subst_module subst + (fun resolver -> subst_dom_delta_resolver subst resolver) mb + | _ -> anomaly "Modops:the evaluation of the structure failed " + +and strengthen_and_subst_struct + str subst env mp_alias mp_from mp_to alias incl resolver = + match str with + | [] -> empty_delta_resolver,[] + | (l,SFBconst cb) :: rest -> + let item' = if alias then + l,SFBconst (subst_const_body subst cb) + else + l,SFBconst (strengthen_const env mp_from l + (subst_const_body subst cb) resolver) + in + let con = make_con mp_from empty_dirpath l in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env + mp_alias mp_from mp_to alias incl resolver in + if incl && not (con_in_delta con resolver) then + (add_constant_delta_resolver + (make_con_equiv mp_to mp_alias empty_dirpath l) resolve_out), item'::rest' - | (l,SFBmind mib) :: rest -> - let item' = l,SFBmind (strengthen_mind env mp l mib) in - let rest' = strengthen_sig env msid rest mp in + else + resolve_out,item'::rest' + | (l,SFBmind mib) :: rest -> + let item' = l,SFBmind (subst_mind subst mib) in + let mind = make_mind mp_from empty_dirpath l in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env + mp_alias mp_from mp_to alias incl resolver in + if incl && not (mind_in_delta mind resolver) then + (add_mind_delta_resolver + (make_mind_equiv mp_to mp_alias empty_dirpath l) resolve_out), item'::rest' - | (l,SFBmodule mb) :: rest -> - let mp' = MPdot (mp,l) in - let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) mb env in - let rest' = strengthen_sig env' msid rest mp in + else + resolve_out,item'::rest' + | (l,SFBmodule mb) :: rest -> + let mp_from' = MPdot (mp_from,l) in + let mp_to' = MPdot(mp_to,l) in + let mb_out = if alias then + subst_module subst + (fun resolver -> subst_dom_delta_resolver subst resolver) mb + else + strengthen_and_subst_mod + mb subst env mp_from' mp_to' env resolver + in + let item' = l,SFBmodule (mb_out) in + let env' = add_module mb_out env in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env' + mp_alias mp_from mp_to alias incl resolver in + add_delta_resolver resolve_out mb_out.mod_delta, item':: rest' - | ((l,SFBalias (mp1,_,cst)) as item) :: rest -> - let env' = register_alias (MPdot(MPself msid,l)) mp1 env in - let rest' = strengthen_sig env' msid rest mp in - item::rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot((MPself msid),l)) - mty - env - in - let rest' = strengthen_sig env' msid rest mp in - item::rest' - - -let strengthen env mtb mp = strengthen_mtb env mp mtb - - -let update_subst env mb mp = - match type_of_mb env mb with - | SEBstruct(msid,str) -> false, join_alias - (subst_key (map_msid msid mp) mb.mod_alias) - (map_msid msid mp) - | _ -> true, mb.mod_alias + | (l,SFBmodtype mty) :: rest -> + let mp_from' = MPdot (mp_from,l) in + let mp_to' = MPdot(mp_to,l) in + let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in + let mty = subst_modtype subst' + (fun resolver -> subst_dom_codom_delta_resolver subst' resolver) mty in + let env' = add_modtype mp_from' mty env in + let resolve_out,rest' = strengthen_and_subst_struct rest subst env' + mp_alias mp_from mp_to alias incl resolver in + (add_mp_delta_resolver + mp_to' mp_to' resolve_out),(l,SFBmodtype mty)::rest' + +let strengthen_and_subst_mb mb mp env include_b = + match mb.mod_type with + SEBstruct str -> + let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in + (*if mb is an alias then the strengthening is useless + (i.e. it is already done)*) + let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in + let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in + let resolver = + add_mp_delta_resolver mp mp_alias + (subst_dom_delta_resolver subst_resolver mb.mod_delta) in + let subst = map_mp mb.mod_mp mp resolver in + let resolver = if mb_is_an_alias && include_b then + remove_mp_delta_resolver mb.mod_delta mb.mod_mp + else mb.mod_delta in + let resolver,new_sig = + strengthen_and_subst_struct str subst env + mp_alias mb.mod_mp mp mb_is_an_alias include_b resolver + in + {mb with + mod_mp = mp; + mod_type = SEBstruct(new_sig); + mod_expr = Some (SEBident mb.mod_mp); + mod_delta = if include_b then resolver + else add_mp_delta_resolver mp mp_alias resolver} + | SEBfunctor(arg_id,argb,body) -> + let subst = map_mp mb.mod_mp mp empty_delta_resolver in + subst_module subst + (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mb + | _ -> anomaly "Modops:the evaluation of the structure failed " + + +let subst_modtype_and_resolver mtb mp env = + let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in + let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in + let full_subst = (map_mp mtb.typ_mp mp new_delta) in + subst_modtype full_subst + (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mtb diff --git a/kernel/modops.mli b/kernel/modops.mli index 4cd72a2ef5..44d29ee3e4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -20,46 +20,38 @@ open Mod_subst (* Various operations on modules and module types *) -(* make the environment entry out of type *) -val module_body_of_type : module_type_body -> module_body -val module_type_of_module : module_path option -> module_body -> +val module_body_of_type : module_path -> module_type_body -> module_body + +val module_type_of_module : env -> module_path option -> module_body -> module_type_body val destr_functor : env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body -val subst_modtype : substitution -> module_type_body -> module_type_body -val subst_structure : substitution -> structure_body -> structure_body - val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body -val subst_signature_msid : - mod_self_id -> module_path -> - structure_body -> structure_body - -val subst_structure : substitution -> structure_body -> structure_body - -(* Evaluation functions *) -val eval_struct : env -> struct_expr_body -> struct_expr_body - -val type_of_mb : env -> module_body -> struct_expr_body +val subst_signature : substitution -> structure_body -> structure_body -(* [add_signature mp sign env] assumes that the substitution [msid] - $\mapsto$ [mp] has already been performed (or is not necessary, like - when [mp = MPself msid]) *) val add_signature : - module_path -> structure_body -> env -> env + module_path -> structure_body -> delta_resolver -> env -> env (* adds a module and its components, but not the constraints *) -val add_module : - module_path -> module_body -> env -> env +val add_module : module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val strengthen : env -> module_type_body -> module_path -> module_type_body -val update_subst : env -> module_body -> module_path -> bool * substitution +val complete_inline_delta_resolver : + env -> module_path -> mod_bound_id -> module_type_body -> + delta_resolver -> delta_resolver + +val strengthen_and_subst_mb : module_body -> module_path -> env -> bool + -> module_body + +val subst_modtype_and_resolver : module_type_body -> module_path -> env -> + module_type_body val error_existing_label : label -> 'a @@ -102,9 +94,7 @@ val error_a_generative_module_expected : label -> 'a val error_local_context : label option -> 'a -val error_no_such_label_sub : label->string->string->'a +val error_no_such_label_sub : label->string->'a + -val resolver_of_environment : - mod_bound_id -> module_type_body -> module_path -> substitution - -> env -> resolver diff --git a/kernel/names.ml b/kernel/names.ml index 0d61a29aa5..06ca87b4da 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -108,7 +108,7 @@ module Labmap = Idmap type module_path = | MPfile of dir_path | MPbound of mod_bound_id - | MPself of mod_self_id + (* | MPapp of module_path * module_path *) | MPdot of module_path * label let rec check_bound_mp = function @@ -119,7 +119,9 @@ let rec check_bound_mp = function let rec string_of_mp = function | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")" | MPbound uid -> string_of_uid uid - | MPself uid -> string_of_uid uid + (* | MPapp (mp1,mp2) -> + "("^string_of_mp mp ^ " " ^ + string_of_mp mp^")"*) | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l (* we compare labels first if both are MPdots *) @@ -172,6 +174,28 @@ let kn_ord kn1 kn2 = else MPord.compare mp1 mp2 +(* a constant name is a kernel name couple (kn1,kn2) + where kn1 corresponds to the name used at toplevel + (i.e. what the user see) + and kn2 corresponds to the canonical kernel name + i.e. in the environment we have + kn1 \rhd_{\delta}^* kn2 \rhd_{\delta} t *) +type constant = kernel_name*kernel_name + +(* For the environment we distinguish constants by their + user part*) +module User_ord = struct + type t = kernel_name*kernel_name + let compare x y= kn_ord (fst x) (fst y) +end + +(* For other uses (ex: non-logical things) it is enough + to deal with the canonical part *) +module Canonical_ord = struct + type t = kernel_name*kernel_name + let compare x y= kn_ord (snd x) (snd y) +end + module KNord = struct type t = kernel_name @@ -181,47 +205,89 @@ end module KNmap = Map.Make(KNord) module KNpred = Predicate.Make(KNord) module KNset = Set.Make(KNord) -module Cmap = KNmap -module Cpred = KNpred -module Cset = KNset + +module Cmap = Map.Make(Canonical_ord) +module Cmap_env = Map.Make(User_ord) +module Cpred = Predicate.Make(Canonical_ord) +module Cset = Set.Make(Canonical_ord) +module Cset_env = Set.Make(User_ord) + +module Mindmap = Map.Make(Canonical_ord) +module Mindset = Set.Make(Canonical_ord) +module Mindmap_env = Map.Make(User_ord) let default_module_name = "If you see this, it's a bug" let initial_dir = make_dirpath [default_module_name] let initial_msid = (make_msid initial_dir "If you see this, it's a bug") -let initial_path = MPself initial_msid +let initial_path = MPfile initial_dir type variable = identifier -type constant = kernel_name -type mutual_inductive = kernel_name + +(* The same thing is done for mutual inductive names + it replaces also the old mind_equiv field of mutual + inductive types*) +type mutual_inductive = kernel_name*kernel_name type inductive = mutual_inductive * int type constructor = inductive * int -let constant_of_kn kn = kn -let make_con mp dir l = (mp,dir,l) -let repr_con con = con -let string_of_con = string_of_kn -let con_label = label -let pr_con = pr_kn -let con_modpath = modpath - -let mind_modpath = modpath +let constant_of_kn kn = (kn,kn) +let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) +let make_con mp dir l = ((mp,dir,l),(mp,dir,l)) +let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let canonical_con con = snd con +let user_con con = fst con +let repr_con con = fst con +let string_of_con con = string_of_kn (fst con) +let con_label con = label (fst con) +let pr_con con = pr_kn (fst con) +let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++ str ")" +let eq_constant (_,kn1) (_,kn2) = kn1=kn2 +let debug_string_of_con con = string_of_kn (fst con)^"'"^string_of_kn (snd con) + +let con_modpath con = modpath (fst con) + +let mind_modpath mind = modpath (fst mind) let ind_modpath ind = mind_modpath (fst ind) let constr_modpath c = ind_modpath (fst c) + +let mind_of_kn kn = (kn,kn) +let mind_of_kn_equiv kn1 kn2 = (kn1,kn2) +let make_mind mp dir l = ((mp,dir,l),(mp,dir,l)) +let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let canonical_mind mind = snd mind +let user_mind mind = fst mind +let repr_mind mind = fst mind +let string_of_mind mind = string_of_kn (fst mind) +let mind_label mind= label (fst mind) +let pr_mind mind = pr_kn (fst mind) +let debug_pr_mind mind = str "("++ pr_kn (fst mind) ++ str ","++ pr_kn (snd mind)++ str ")" +let eq_mind (_,kn1) (_,kn2) = kn1=kn2 +let debug_string_of_mind mind = string_of_kn (fst mind)^"'"^string_of_kn (snd mind) + let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) let inductive_of_constructor (ind,i) = ind let index_of_constructor (ind,i) = i +let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2 +let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2 module InductiveOrdered = struct type t = inductive let compare (spx,ix) (spy,iy) = - let c = ix - iy in if c = 0 then KNord.compare spx spy else c + let c = ix - iy in if c = 0 then Canonical_ord.compare spx spy else c +end + +module InductiveOrdered_env = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then User_ord.compare spx spy else c end module Indmap = Map.Make(InductiveOrdered) +module Indmap_env = Map.Make(InductiveOrdered_env) module ConstructorOrdered = struct type t = constructor @@ -229,13 +295,24 @@ module ConstructorOrdered = struct let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c end +module ConstructorOrdered_env = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered_env.compare indx indy else c +end + module Constrmap = Map.Make(ConstructorOrdered) +module Constrmap_env = Map.Make(ConstructorOrdered_env) (* Better to have it here that in closure, since used in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of constant +let eq_egr e1 e2 = match e1,e2 with + EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2 + | _,_ -> e1 = e2 + (* Hash-consing of name objects *) module Hname = Hashcons.Make( struct @@ -281,24 +358,24 @@ module Hmod = Hashcons.Make( let rec hash_sub (hdir,huniqid,hstr as hfuns) = function | MPfile dir -> MPfile (hdir dir) | MPbound m -> MPbound (huniqid m) - | MPself m -> MPself (huniqid m) | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l) let rec equal d1 d2 = match (d1,d2) with | MPfile dir1, MPfile dir2 -> dir1 == dir2 | MPbound m1, MPbound m2 -> m1 == m2 - | MPself m1, MPself m2 -> m1 == m2 | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2 | _ -> false let hash = Hashtbl.hash end) -module Hkn = Hashcons.Make( - struct - type t = kernel_name + +module Hcn = Hashcons.Make( + struct + type t = kernel_name*kernel_name type u = (module_path -> module_path) * (dir_path -> dir_path) * (string -> string) - let hash_sub (hmod,hdir,hstr) (md,dir,l) = (hmod md, hdir dir, hstr l) - let equal (mod1,dir1,l1) (mod2,dir2,l2) = + let hash_sub (hmod,hdir,hstr) ((md,dir,l),(mde,dire,le)) = + ((hmod md, hdir dir, hstr l),(hmod mde, hdir dire, hstr le)) + let equal ((mod1,dir1,l1),_) ((mod2,dir2,l2),_) = mod1 == mod2 && dir1 == dir2 && l1 == l2 let hash = Hashtbl.hash end) @@ -310,8 +387,9 @@ let hcons_names () = let hdir = Hashcons.simple_hcons Hdir.f hident in let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in - let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in - (hkn,hkn,hdir,hname,hident,hstring) + let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in + let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in + (hcn,hmind,hdir,hname,hident,hstring) (*******) @@ -335,3 +413,8 @@ type inv_rel_key = int (* index in the [rel_context] part of environment type id_key = inv_rel_key tableKey +let eq_id_key ik1 ik2 = + match ik1,ik2 with + ConstKey (_,kn1), + ConstKey (_,kn2) -> kn1=kn2 + | a,b -> a=b diff --git a/kernel/names.mli b/kernel/names.mli index fb3b5c81b5..e42f8ea71b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -80,9 +80,9 @@ module Labmap : Map.S with type key = label type module_path = | MPfile of dir_path | MPbound of mod_bound_id - | MPself of mod_self_id + (* | MPapp of module_path * module_path very soon *) | MPdot of module_path * label -(*i | MPapply of module_path * module_path in the future (maybe) i*) + val check_bound_mp : module_path -> bool @@ -122,25 +122,64 @@ module KNmap : Map.S with type key = kernel_name type variable = identifier type constant -type mutual_inductive = kernel_name +type mutual_inductive (* Beware: first inductive has index 0 *) type inductive = mutual_inductive * int (* Beware: first constructor has index 1 *) type constructor = inductive * int +(* *_env modules consider an order on user part of names + the others consider an order on canonical part of names*) module Cmap : Map.S with type key = constant +module Cmap_env : Map.S with type key = constant module Cpred : Predicate.S with type elt = constant module Cset : Set.S with type elt = constant +module Cset_env : Set.S with type elt = constant +module Mindmap : Map.S with type key = mutual_inductive +module Mindmap_env : Map.S with type key = mutual_inductive +module Mindset : Set.S with type elt = mutual_inductive module Indmap : Map.S with type key = inductive module Constrmap : Map.S with type key = constructor +module Indmap_env : Map.S with type key = inductive +module Constrmap_env : Map.S with type key = constructor val constant_of_kn : kernel_name -> constant +val constant_of_kn_equiv : kernel_name -> kernel_name -> constant val make_con : module_path -> dir_path -> label -> constant +val make_con_equiv : module_path -> module_path -> dir_path + -> label -> constant +val user_con : constant -> kernel_name +val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * dir_path * label +val eq_constant : constant -> constant -> bool + val string_of_con : constant -> string val con_label : constant -> label val con_modpath : constant -> module_path val pr_con : constant -> Pp.std_ppcmds +val debug_pr_con : constant -> Pp.std_ppcmds +val debug_string_of_con : constant -> string + + + +val mind_of_kn : kernel_name -> mutual_inductive +val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive +val make_mind : module_path -> dir_path -> label -> mutual_inductive +val make_mind_equiv : module_path -> module_path -> dir_path + -> label -> mutual_inductive +val user_mind : mutual_inductive -> kernel_name +val canonical_mind : mutual_inductive -> kernel_name +val repr_mind : mutual_inductive -> module_path * dir_path * label +val eq_mind : mutual_inductive -> mutual_inductive -> bool + +val string_of_mind : mutual_inductive -> string +val mind_label : mutual_inductive -> label +val mind_modpath : mutual_inductive -> module_path +val pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_string_of_mind : mutual_inductive -> string + + val mind_modpath : mutual_inductive -> module_path val ind_modpath : inductive -> module_path @@ -150,16 +189,21 @@ val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int +val eq_ind : inductive -> inductive -> bool +val eq_constructor : constructor -> constructor -> bool (* Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of constant +val eq_egr : evaluable_global_reference -> evaluable_global_reference + -> bool + (* Hash-consing *) val hcons_names : unit -> (constant -> constant) * - (kernel_name -> kernel_name) * (dir_path -> dir_path) * + (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * (string -> string) @@ -182,3 +226,5 @@ type inv_rel_key = int (* index in the [rel_context] part of environment of de Bruijn indice *) type id_key = inv_rel_key tableKey + +val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 4216722015..b58951e983 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -23,11 +23,10 @@ type key = int option ref type constant_key = constant_body * key type globals = { - env_constants : constant_key Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_key Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; @@ -58,11 +57,10 @@ let empty_named_context_val = [],[] let empty_env = { env_globals = { - env_constants = Cmap.empty; - env_inductives = KNmap.empty; + env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty; - env_alias = MPmap.empty }; + env_modtypes = MPmap.empty}; env_named_context = empty_named_context; env_named_vals = []; env_rel_context = empty_rel_context; @@ -123,16 +121,12 @@ let env_of_named id env = env (* Global constants *) let lookup_constant_key kn env = - Cmap.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.env_constants let lookup_constant kn env = - fst (Cmap.find kn env.env_globals.env_constants) + fst (Cmap_env.find kn env.env_globals.env_constants) (* Mutual Inductives *) let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives + Mindmap_env.find kn env.env_globals.env_inductives -let rec scrape_mind env kn = - match (lookup_mind kn env).mind_equiv with - | None -> kn - | Some kn' -> scrape_mind env kn' diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index abbf9b1b53..718132b327 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -23,11 +23,10 @@ type key = int option ref type constant_key = constant_body * key type globals = { - env_constants : constant_key Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_key Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; @@ -80,5 +79,3 @@ val lookup_constant : constant -> env -> constant_body (* Mutual Inductives *) val lookup_mind : mutual_inductive -> env -> mutual_inductive_body -(* Find the ultimate inductive in the [mind_equiv] chain *) -val scrape_mind : env -> mutual_inductive -> mutual_inductive diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0a404fff31..92386c4d36 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -274,7 +274,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if fl1 = fl2 + if eq_table_key fl1 fl2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible with NotConvertible -> @@ -325,13 +325,13 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd ind1, FInd ind2) -> - if mind_equiv_infos (snd infos) ind1 ind2 + if eq_ind ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> - if j1 = j2 && mind_equiv_infos (snd infos) ind1 ind2 + if j1 = j2 && eq_ind ind1 ind2 then convert_stacks infos lft1 lft2 v1 v2 cuniv else raise NotConvertible @@ -377,7 +377,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv = and convert_stacks infos lft1 lft2 stk1 stk2 cuniv = compare_stacks (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c) - (mind_equiv_infos (snd infos)) + (eq_ind) lft1 stk1 lft2 stk2 cuniv and convert_vect infos lft1 lft2 v1 v2 cuniv = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e73689bc8c..b0dc6dd8a0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -35,13 +35,12 @@ type modvariant = | LIBRARY of dir_path type module_info = - { msid : mod_self_id; - modpath : module_path; - seed : dir_path; (* the "seed" of unique identifier generator *) - label : label; - variant : modvariant; - alias_subst : substitution} - + {modpath : module_path; + label : label; + variant : modvariant; + resolver : delta_resolver; + resolver_of_param : delta_resolver;} + let check_label l labset = if Labset.mem l labset then error_existing_label l @@ -80,12 +79,11 @@ let rec empty_environment = { old = empty_environment; env = empty_env; modinfo = { - msid = initial_msid; modpath = initial_path; - seed = initial_dir; label = mk_label "_"; variant = NONE; - alias_subst = empty_subst}; + resolver = empty_delta_resolver; + resolver_of_param = empty_delta_resolver}; labset = Labset.empty; revstruct = []; univ = Univ.Constraint.empty; @@ -215,9 +213,16 @@ let add_constant dir l decl senv = in let senv' = add_constraints cb.const_constraints senv in let env'' = Environ.add_constant kn cb senv'.env in + let resolver = + if cb.const_inline then + add_inline_delta_resolver kn senv'.modinfo.resolver + else + senv'.modinfo.resolver + in kn, { old = senv'.old; env = env''; - modinfo = senv'.modinfo; + modinfo = {senv'.modinfo with + resolver = resolver}; labset = Labset.add l senv'.labset; revstruct = (l,SFBconst cb)::senv'.revstruct; univ = senv'.univ; @@ -242,7 +247,7 @@ let add_mind dir l mie senv = all labels *) let mib = translate_mind senv.env mie in let senv' = add_constraints mib.mind_constraints senv in - let kn = make_kn senv.modinfo.modpath dir l in + let kn = make_mind senv.modinfo.modpath dir l in let env'' = Environ.add_mind kn mib senv'.env in kn, { old = senv'.old; env = env''; @@ -259,118 +264,82 @@ let add_mind dir l mie senv = let add_modtype l mte senv = check_label l senv.labset; - let mtb_expr,sub = translate_struct_entry senv.env mte in - let mtb = { typ_expr = mtb_expr; - typ_strength = None; - typ_alias = sub} in - let senv' = add_constraints - (struct_expr_constraints mtb_expr) senv in let mp = MPdot(senv.modinfo.modpath, l) in - let env'' = Environ.add_modtype mp mtb senv'.env in - mp, { old = senv'.old; - env = env''; - modinfo = senv'.modinfo; - labset = Labset.add l senv'.labset; - revstruct = (l,SFBmodtype mtb)::senv'.revstruct; - univ = senv'.univ; - engagement = senv'.engagement; - imports = senv'.imports; - loads = senv'.loads; - local_retroknowledge = senv'.local_retroknowledge } + let mtb = translate_module_type senv.env mp mte in + let senv' = add_constraints mtb.typ_constraints senv in + let env'' = Environ.add_modtype mp mtb senv'.env in + mp, { old = senv'.old; + env = env''; + modinfo = senv'.modinfo; + labset = Labset.add l senv'.labset; + revstruct = (l,SFBmodtype mtb)::senv'.revstruct; + univ = senv'.univ; + engagement = senv'.engagement; + imports = senv'.imports; + loads = senv'.loads; + local_retroknowledge = senv'.local_retroknowledge } (* full_add_module adds module with universes and constraints *) -let full_add_module mp mb senv = - let senv = add_constraints (module_constraints mb) senv in - let env = Modops.add_module mp mb senv.env in +let full_add_module mb senv = + let senv = add_constraints mb.mod_constraints senv in + let env = Modops.add_module mb senv.env in {senv with env = env} (* Insertion of modules *) let add_module l me senv = check_label l senv.labset; - let mb = translate_module senv.env me in let mp = MPdot(senv.modinfo.modpath, l) in - let senv' = full_add_module mp mb senv in - let is_functor,sub = Modops.update_subst senv'.env mb mp in - mp, { old = senv'.old; - env = senv'.env; - modinfo = - if is_functor then - senv'.modinfo - else - {senv'.modinfo with - alias_subst = join senv'.modinfo.alias_subst sub}; - labset = Labset.add l senv'.labset; - revstruct = (l,SFBmodule mb)::senv'.revstruct; - univ = senv'.univ; - engagement = senv'.engagement; - imports = senv'.imports; - loads = senv'.loads; - local_retroknowledge = senv'.local_retroknowledge } - -let add_alias l mp senv = - check_label l senv.labset; - let mp' = MPdot(senv.modinfo.modpath, l) in - let mp1 = scrape_alias mp senv.env in - let typ_opt = - if check_bound_mp mp then - Some (strengthen senv.env - (lookup_modtype mp senv.env).typ_expr mp) - else - None + let mb = translate_module senv.env mp me in + let senv' = full_add_module mb senv in + let modinfo = match mb.mod_type with + SEBstruct _ -> + { senv'.modinfo with + resolver = + add_delta_resolver mb.mod_delta senv'.modinfo.resolver} + | _ -> senv'.modinfo in - (* we get all updated alias substitution {mp1.K\M} that comes from mp1 *) - let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in - (* transformation of {mp1.K\M} to {mp.K\M}*) - let sub = update_subst sub (map_mp mp' mp1) in - (* transformation of {mp.K\M} to {mp.K\M'} where M'=M{mp1\mp'}*) - let sub = join_alias sub (map_mp mp' mp1) in - (* we add the alias substitution *) - let sub = add_mp mp' mp1 sub in - let env' = register_alias mp' mp senv.env in - mp', { old = senv.old; - env = env'; - modinfo = { senv.modinfo with - alias_subst = join - senv.modinfo.alias_subst sub}; - labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct; - univ = senv.univ; - engagement = senv.engagement; - imports = senv.imports; - loads = senv.loads; - local_retroknowledge = senv.local_retroknowledge } - + mp,mb.mod_delta, + { old = senv'.old; + env = senv'.env; + modinfo = modinfo; + labset = Labset.add l senv'.labset; + revstruct = (l,SFBmodule mb)::senv'.revstruct; + univ = senv'.univ; + engagement = senv'.engagement; + imports = senv'.imports; + loads = senv'.loads; + local_retroknowledge = senv'.local_retroknowledge } + (* Interactive modules *) let start_module l senv = check_label l senv.labset; - let msid = make_msid senv.modinfo.seed (string_of_label l) in - let mp = MPself msid in - let modinfo = { msid = msid; - modpath = mp; - seed = senv.modinfo.seed; - label = l; - variant = STRUCT []; - alias_subst = empty_subst} - in - mp, { old = senv; - env = senv.env; - modinfo = modinfo; - labset = Labset.empty; - revstruct = []; - univ = Univ.Constraint.empty; - engagement = None; - imports = senv.imports; - loads = []; - (* spiwack : not sure, but I hope it's correct *) - local_retroknowledge = [] } + let mp = MPdot(senv.modinfo.modpath, l) in + let modinfo = { modpath = mp; + label = l; + variant = STRUCT []; + resolver = empty_delta_resolver; + resolver_of_param = empty_delta_resolver} + in + mp, { old = senv; + env = senv.env; + modinfo = modinfo; + labset = Labset.empty; + revstruct = []; + univ = Univ.Constraint.empty; + engagement = None; + imports = senv.imports; + loads = []; + (* spiwack : not sure, but I hope it's correct *) + local_retroknowledge = [] } let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in - let restype = Option.map (translate_struct_entry senv.env) restype in + let mp = senv.modinfo.modpath in + let restype = Option.map (translate_module_type senv.env mp) restype in let params,is_functor = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () @@ -386,83 +355,107 @@ let end_module l restype senv = params in let auto_tb = - SEBstruct (modinfo.msid, List.rev senv.revstruct) + SEBstruct (List.rev senv.revstruct) in - let mod_typ,subst,cst = + let mexpr,mod_typ,mod_typ_alg,resolver,cst = match restype with - | None -> None,modinfo.alias_subst,Constraint.empty - | Some (res_tb,subst) -> - let cst = check_subtypes senv.env - {typ_expr = auto_tb; - typ_strength = None; - typ_alias = modinfo.alias_subst} - {typ_expr = res_tb; - typ_strength = None; - typ_alias = subst} in - let mtb = functorize_struct res_tb in - Some mtb,subst,cst + | None -> let mexpr = functorize_struct auto_tb in + mexpr,mexpr,None,modinfo.resolver,Constraint.empty + | Some mtb -> + let auto_mtb = { + typ_mp = senv.modinfo.modpath; + typ_expr = auto_tb; + typ_expr_alg = None; + typ_constraints = Constraint.empty; + typ_delta = empty_delta_resolver} in + let cst = check_subtypes senv.env auto_mtb + mtb in + let mod_typ = functorize_struct mtb.typ_expr in + let mexpr = functorize_struct auto_tb in + let typ_alg = + Option.map functorize_struct mtb.typ_expr_alg in + mexpr,mod_typ,typ_alg,mtb.typ_delta,cst in - let mexpr = functorize_struct auto_tb in let cst = Constraint.union cst senv.univ in let mb = - { mod_expr = Some mexpr; + { mod_mp = mp; + mod_expr = Some mexpr; mod_type = mod_typ; + mod_type_alg = mod_typ_alg; mod_constraints = cst; - mod_alias = subst; + mod_delta = resolver; mod_retroknowledge = senv.local_retroknowledge } in - let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in let newenv = set_engagement_opt senv.engagement newenv in let senv'= {senv with env=newenv} in let senv' = List.fold_left - (fun env (mp,mb) -> full_add_module mp mb env) + (fun env (_,mb) -> full_add_module mb env) senv' (List.rev senv'.loads) in let newenv = Environ.add_constraints cst senv'.env in let newenv = - Modops.add_module mp mb newenv - in - let is_functor,subst = Modops.update_subst newenv mb mp in - let newmodinfo = - if is_functor then - oldsenv.modinfo - else - { oldsenv.modinfo with - alias_subst = join - oldsenv.modinfo.alias_subst - subst }; + Modops.add_module mb newenv in + let modinfo = match mb.mod_type with + SEBstruct _ -> + { oldsenv.modinfo with + resolver = + add_delta_resolver resolver oldsenv.modinfo.resolver} + | _ -> oldsenv.modinfo in - mp, { old = oldsenv.old; - env = newenv; - modinfo = newmodinfo; - labset = Labset.add l oldsenv.labset; - revstruct = (l,SFBmodule mb)::oldsenv.revstruct; - univ = Univ.Constraint.union senv'.univ oldsenv.univ; - (* engagement is propagated to the upper level *) - engagement = senv'.engagement; - imports = senv'.imports; - loads = senv'.loads@oldsenv.loads; - local_retroknowledge = senv'.local_retroknowledge@oldsenv.local_retroknowledge } + mp,resolver,{ old = oldsenv.old; + env = newenv; + modinfo = modinfo; + labset = Labset.add l oldsenv.labset; + revstruct = (l,SFBmodule mb)::oldsenv.revstruct; + univ = Univ.Constraint.union senv'.univ oldsenv.univ; + (* engagement is propagated to the upper level *) + engagement = senv'.engagement; + imports = senv'.imports; + loads = senv'.loads@oldsenv.loads; + local_retroknowledge = + senv'.local_retroknowledge@oldsenv.local_retroknowledge } (* Include for module and module type*) - let add_include me senv = - let struct_expr,_ = translate_struct_entry senv.env me in - let senv = add_constraints (struct_expr_constraints struct_expr) senv in - let msid,str = match (eval_struct senv.env struct_expr) with - | SEBstruct(msid,str_l) -> msid,str_l - | _ -> error ("You cannot Include a higher-order Module or Module Type.") + let add_include me is_module senv = + let sign,cst,resolver = + if is_module then + let sign,resolver,cst = + translate_struct_include_module_entry senv.env + senv.modinfo.modpath me in + sign,cst,resolver + else + let mtb = + translate_module_type senv.env + senv.modinfo.modpath me in + mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta in + let senv = add_constraints cst senv in let mp_sup = senv.modinfo.modpath in - let str1 = subst_signature_msid msid mp_sup str in + let str = match sign with + | SEBstruct(str_l) -> + str_l + | _ -> error ("You cannot Include a high-order structure.") + in + let senv = + {senv + with modinfo = + {senv.modinfo + with resolver = + add_delta_resolver resolver senv.modinfo.resolver}} + in let add senv (l,elem) = check_label l senv.labset; match elem with | SFBconst cb -> - let con = make_con mp_sup empty_dirpath l in + let kn = make_kn mp_sup empty_dirpath l in + let con = constant_of_kn_equiv kn + (canonical_con + (constant_of_delta resolver (constant_of_kn kn))) + in let senv' = add_constraints cb.const_constraints senv in let env'' = Environ.add_constant con cb senv'.env in { old = senv'.old; @@ -475,11 +468,14 @@ let end_module l restype senv = imports = senv'.imports; loads = senv'.loads ; local_retroknowledge = senv'.local_retroknowledge } - | SFBmind mib -> let kn = make_kn mp_sup empty_dirpath l in + let mind = mind_of_kn_equiv kn + (canonical_mind + (mind_of_delta resolver (mind_of_kn kn))) + in let senv' = add_constraints mib.mind_constraints senv in - let env'' = Environ.add_mind kn mib senv'.env in + let env'' = Environ.add_mind mind mib senv'.env in { old = senv'.old; env = env''; modinfo = senv'.modinfo; @@ -492,17 +488,10 @@ let end_module l restype senv = local_retroknowledge = senv'.local_retroknowledge } | SFBmodule mb -> - let mp = MPdot(senv.modinfo.modpath, l) in - let is_functor,sub = Modops.update_subst senv.env mb mp in - let senv' = full_add_module mp mb senv in + let senv' = full_add_module mb senv in { old = senv'.old; env = senv'.env; - modinfo = - if is_functor then - senv'.modinfo - else - {senv'.modinfo with - alias_subst = join senv'.modinfo.alias_subst sub}; + modinfo = senv'.modinfo; labset = Labset.add l senv'.labset; revstruct = (l,SFBmodule mb)::senv'.revstruct; univ = senv'.univ; @@ -510,87 +499,69 @@ let end_module l restype senv = imports = senv'.imports; loads = senv'.loads; local_retroknowledge = senv'.local_retroknowledge } - | SFBalias (mp',typ_opt,cst) -> - let env' = Option.fold_right - Environ.add_constraints cst senv.env in - let mp = MPdot(senv.modinfo.modpath, l) in - let mp1 = scrape_alias mp' senv.env in - let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in - let sub = update_subst sub (map_mp mp mp1) in - let sub = join_alias sub (map_mp mp mp1) in - let sub = add_mp mp mp1 sub in - let env' = register_alias mp mp' env' in - { old = senv.old; - env = env'; - modinfo = { senv.modinfo with - alias_subst = join - senv.modinfo.alias_subst sub}; - labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct; - univ = senv.univ; - engagement = senv.engagement; - imports = senv.imports; - loads = senv.loads; - local_retroknowledge = senv.local_retroknowledge } | SFBmodtype mtb -> - let env' = add_modtype_constraints senv.env mtb in + let senv' = add_constraints mtb.typ_constraints senv in let mp = MPdot(senv.modinfo.modpath, l) in - let env'' = Environ.add_modtype mp mtb env' in + let env' = Environ.add_modtype mp mtb senv'.env in { old = senv.old; - env = env''; - modinfo = senv.modinfo; + env = env'; + modinfo = senv'.modinfo; labset = Labset.add l senv.labset; - revstruct = (l,SFBmodtype mtb)::senv.revstruct; - univ = senv.univ; - engagement = senv.engagement; - imports = senv.imports; - loads = senv.loads; - local_retroknowledge = senv.local_retroknowledge } + revstruct = (l,SFBmodtype mtb)::senv'.revstruct; + univ = senv'.univ; + engagement = senv'.engagement; + imports = senv'.imports; + loads = senv'.loads; + local_retroknowledge = senv'.local_retroknowledge } in - List.fold_left add senv str1 + resolver,(List.fold_left add senv str) (* Adding parameters to modules or module types *) let add_module_parameter mbid mte senv = if senv.revstruct <> [] or senv.loads <> [] then anomaly "Cannot add a module parameter to a non empty module"; - let mtb_expr,sub = translate_struct_entry senv.env mte in - let mtb = {typ_expr = mtb_expr; - typ_strength = None; - typ_alias = sub} in - let senv = full_add_module (MPbound mbid) (module_body_of_type mtb) senv + let mtb = translate_module_type senv.env (MPbound mbid) mte in + let senv = + full_add_module (module_body_of_type (MPbound mbid) mtb) senv in let new_variant = match senv.modinfo.variant with | STRUCT params -> STRUCT ((mbid,mtb) :: params) | SIG params -> SIG ((mbid,mtb) :: params) | _ -> - anomaly "Module parameters can only be added to modules or signatures" + anomaly "Module parameters can only be added to modules or signatures" in - { old = senv.old; - env = senv.env; - modinfo = { senv.modinfo with variant = new_variant }; - labset = senv.labset; - revstruct = []; - univ = senv.univ; - engagement = senv.engagement; - imports = senv.imports; - loads = []; - local_retroknowledge = senv.local_retroknowledge } - + + let resolver_of_param = match mtb.typ_expr with + SEBstruct _ -> mtb.typ_delta + | _ -> empty_delta_resolver + in + mtb.typ_delta, { old = senv.old; + env = senv.env; + modinfo = { senv.modinfo with + variant = new_variant; + resolver_of_param = add_delta_resolver + resolver_of_param senv.modinfo.resolver_of_param}; + labset = senv.labset; + revstruct = []; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = []; + local_retroknowledge = senv.local_retroknowledge } + (* Interactive module types *) let start_modtype l senv = check_label l senv.labset; - let msid = make_msid senv.modinfo.seed (string_of_label l) in - let mp = MPself msid in - let modinfo = { msid = msid; - modpath = mp; - seed = senv.modinfo.seed; - label = l; - variant = SIG []; - alias_subst = empty_subst } - in + let mp = MPdot(senv.modinfo.modpath, l) in + let modinfo = { modpath = mp; + label = l; + variant = SIG []; + resolver = empty_delta_resolver; + resolver_of_param = empty_delta_resolver} + in mp, { old = senv; env = senv.env; modinfo = modinfo; @@ -614,7 +585,7 @@ let end_modtype l senv = if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; let auto_tb = - SEBstruct (modinfo.msid, List.rev senv.revstruct) + SEBstruct (List.rev senv.revstruct) in let mtb_expr = List.fold_left @@ -625,42 +596,39 @@ let end_modtype l senv = in let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in - (* since universes constraints cannot be stored in the modtype, - they are propagated to the upper level *) let newenv = Environ.add_constraints senv.univ newenv in let newenv = set_engagement_opt senv.engagement newenv in let senv = {senv with env=newenv} in let senv = List.fold_left - (fun env (mp,mb) -> full_add_module mp mb env) + (fun env (mp,mb) -> full_add_module mb env) senv (List.rev senv.loads) in - let subst = senv.modinfo.alias_subst in - let mtb = {typ_expr = mtb_expr; - typ_strength = None; - typ_alias = subst} in + let mtb = {typ_mp = mp; + typ_expr = mtb_expr; + typ_expr_alg = None; + typ_constraints = senv.univ; + typ_delta = senv.modinfo.resolver} in let newenv = Environ.add_modtype mp mtb senv.env in mp, { old = oldsenv.old; env = newenv; - modinfo = oldsenv.modinfo; - labset = Labset.add l oldsenv.labset; - revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; - univ = Univ.Constraint.union senv.univ oldsenv.univ; - engagement = senv.engagement; - imports = senv.imports; - loads = senv.loads@oldsenv.loads; - (* spiwack : if there is a bug with retroknowledge in nested modules - it's likely to come from here *) - local_retroknowledge = - senv.local_retroknowledge@oldsenv.local_retroknowledge} - + modinfo = oldsenv.modinfo; + labset = Labset.add l oldsenv.labset; + revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; + univ = Univ.Constraint.union senv.univ oldsenv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads@oldsenv.loads; + (* spiwack : if there is a bug with retroknowledge in nested modules + it's likely to come from here *) + local_retroknowledge = + senv.local_retroknowledge@oldsenv.local_retroknowledge} let current_modpath senv = senv.modinfo.modpath -let current_msid senv = senv.modinfo.msid - +let delta_of_senv senv = senv.modinfo.resolver,senv.modinfo.resolver_of_param (* Check that the engagement expected by a library matches the initial one *) let check_engagement env c = @@ -685,7 +653,7 @@ type compiled_library = let is_empty senv = senv.revstruct = [] && - senv.modinfo.msid = initial_msid && + senv.modinfo.modpath = initial_path && senv.modinfo.variant = NONE let start_library dir senv = @@ -697,14 +665,12 @@ let start_library dir senv = | hd::tl -> make_dirpath tl, label_of_id hd in - let msid = make_msid dir_path (string_of_label l) in - let mp = MPself msid in - let modinfo = { msid = msid; - modpath = mp; - seed = dir; - label = l; - variant = LIBRARY dir; - alias_subst = empty_subst } + let mp = MPfile dir in + let modinfo = {modpath = mp; + label = l; + variant = LIBRARY dir; + resolver = empty_delta_resolver; + resolver_of_param = empty_delta_resolver} in mp, { old = senv; env = senv.env; @@ -731,14 +697,18 @@ let export senv dir = end; (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then (* error_export_simple *) (); *) - let mb = - { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct)); - mod_type = None; + let str = SEBstruct (List.rev senv.revstruct) in + let mp = senv.modinfo.modpath in + let mb = + { mod_mp = mp; + mod_expr = Some str; + mod_type = str; + mod_type_alg = None; mod_constraints = senv.univ; - mod_alias = senv.modinfo.alias_subst; + mod_delta = senv.modinfo.resolver; mod_retroknowledge = senv.local_retroknowledge} in - modinfo.msid, (dir,mb,senv.imports,engagement senv.env) + mp, (dir,mb,senv.imports,engagement senv.env) let check_imports senv needed = @@ -775,9 +745,13 @@ let import (dp,mb,depends,engmt) digest senv = let mp = MPfile dp in let env = senv.env in let env = Environ.add_constraints mb.mod_constraints env in - let env = Modops.add_module mp mb env in + let env = Modops.add_module mb env in mp, { senv with env = env; + modinfo = + {senv.modinfo with + resolver = + add_delta_resolver mb.mod_delta senv.modinfo.resolver}; imports = (dp,digest)::senv.imports; loads = (mp,mb)::senv.loads } @@ -785,14 +759,14 @@ let import (dp,mb,depends,engmt) digest senv = (* Remove the body of opaque constants in modules *) let rec lighten_module mb = { mb with - mod_expr = Option.map lighten_modexpr mb.mod_expr; - mod_type = Option.map lighten_modexpr mb.mod_type; + mod_expr = None; + mod_type = lighten_modexpr mb.mod_type; } and lighten_struct struc = let lighten_body (l,body) = (l,match body with | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x + | (SFBconst _ | SFBmind _ ) as x -> x | SFBmodule m -> SFBmodule (lighten_module m) | SFBmodtype m -> SFBmodtype ({m with @@ -807,8 +781,8 @@ and lighten_modexpr = function typ_expr = lighten_modexpr mty.typ_expr}), lighten_modexpr mexpr) | SEBident mp as x -> x - | SEBstruct (msid, struc) -> - SEBstruct (msid, lighten_struct struc) + | SEBstruct (struc) -> + SEBstruct (lighten_struct struc) | SEBapply (mexpr,marg,u) -> SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) | SEBwith (seb,wdcl) -> diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index ac1e3863ad..f011d42b7f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -13,6 +13,7 @@ open Names open Term open Declarations open Entries +open Mod_subst (*i*) (*s Safe environments. Since we are now able to type terms, we can @@ -55,12 +56,8 @@ val add_mind : (* Adding a module *) val add_module : label -> module_entry -> safe_environment - -> module_path * safe_environment + -> module_path * delta_resolver * safe_environment -(* Adding a module alias*) -val add_alias : - label -> module_path -> safe_environment - -> module_path * safe_environment (* Adding a module type *) val add_modtype : label -> module_struct_entry -> safe_environment @@ -77,12 +74,13 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : label -> safe_environment -> module_path * safe_environment + val end_module : - label -> module_struct_entry option - -> safe_environment -> module_path * safe_environment + label -> module_struct_entry option + -> safe_environment -> module_path * delta_resolver * safe_environment val add_module_parameter : - mod_bound_id -> module_struct_entry -> safe_environment -> safe_environment + mod_bound_id -> module_struct_entry -> safe_environment -> delta_resolver * safe_environment val start_modtype : label -> safe_environment -> module_path * safe_environment @@ -91,12 +89,11 @@ val end_modtype : label -> safe_environment -> module_path * safe_environment val add_include : - module_struct_entry -> safe_environment -> safe_environment + module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment val current_modpath : safe_environment -> module_path -val current_msid : safe_environment -> mod_self_id - - +val delta_of_senv : safe_environment -> delta_resolver*delta_resolver + (* Loading and saving compilation units *) (* exporting and importing modules *) @@ -106,7 +103,7 @@ val start_library : dir_path -> safe_environment -> module_path * safe_environment val export : safe_environment -> dir_path - -> mod_self_id * compiled_library + -> module_path * compiled_library val import : compiled_library -> Digest.t -> safe_environment -> module_path * safe_environment diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 861dc9a3fd..41f4c640ce 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -33,7 +33,6 @@ type namedobject = | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) @@ -61,10 +60,9 @@ let make_label_map mp list = match e with | SFBconst cb -> add_map (Constant cb) | SFBmind mib -> - add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map + add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt)) in List.fold_right add_one list Labmap.empty @@ -75,15 +73,18 @@ let check_conv_error error cst f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive cst env msid1 l info1 mib2 spec2 = - let kn = make_kn (MPself msid1) empty_dirpath l in + +let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= + let kn1 = make_mind mp1 empty_dirpath l in + let kn2 = make_mind mp2 empty_dirpath l in let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in let mib1 = match info1 with - | IndType ((_,0), mib) -> mib + | IndType ((_,0), mib) -> subst_mind subst1 mib | _ -> error () in + let mib2 = subst_mind subst2 mib2 in let check_inductive_type cst env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -141,8 +142,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = array_fold_left2 (fun cst t1 t2 -> check_conv cst conv env t1 t2) cst - (arities_of_specif kn (mib1,p1)) - (arities_of_specif kn (mib2,p2)) + (arities_of_specif kn1 (mib1,p1)) + (arities_of_specif kn1 (mib2,p2)) in let check f = if f mib1 <> f mib2 then error () in check (fun mib -> mib.mind_finite); @@ -158,16 +159,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - begin - match mib2.mind_equiv with - | None -> () - | Some kn2' -> - let kn2 = scrape_mind env kn2' in - let kn1 = match mib1.mind_equiv with - None -> kn - | Some kn1' -> scrape_mind env kn1' - in - if kn1 <> kn2 then error () + begin + match mind_of_delta reso2 kn2 with + | kn2' when kn2=kn2' -> () + | kn2' -> + if not (eq_mind (mind_of_delta reso1 kn1) kn2') then + error () end; (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record); @@ -194,7 +191,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = in cst -let check_constant cst env msid1 l info1 cb2 spec2 = + +let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -245,13 +243,15 @@ let check_constant cst env msid1 l info1 cb2 spec2 = in match info1 with - | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*Start by checking types*) + | Constant cb1 -> + assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking types*) + let cb1 = subst_const_body subst1 cb1 in + let cb2 = subst_const_body subst2 cb2 in let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = check_type cst env typ1 typ2 in - let con = make_con (MPself msid1) empty_dirpath l in + let con = make_con mp1 empty_dirpath l in let cst = if cb2.const_opaque then match cb2.const_body with @@ -264,7 +264,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = begin match (kind_of_term c) with Const n -> - let cb = lookup_constant n env in + let cb = subst_const_body subst1 + (lookup_constant n env) in (match cb.const_opaque, cb.const_body with | true, Some lc1 -> @@ -311,28 +312,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = check_conv cst conv env ty1 ty2 | _ -> error () -let rec check_modules cst env msid1 l msb1 msb2 alias = - let mp = (MPdot(MPself msid1,l)) in - let mty1 = module_type_of_module (Some mp) msb1 in - let alias1,struct_expr = match eval_struct env mty1.typ_expr with - | SEBstruct (msid,sign) as str -> - update_subst alias (map_msid msid mp),str - | _ as str -> empty_subst,str in - let mty1 = {mty1 with - typ_expr = struct_expr; - typ_alias = join alias1 mty1.typ_alias } in - let mty2 = module_type_of_module None msb2 in - let cst = check_modtypes cst env mty1 mty2 false in +let rec check_modules cst env msb1 msb2 subst1 subst2 = + let mty1 = module_type_of_module env None msb1 in + let mty2 = module_type_of_module env None msb2 in + let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in cst - -and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = - let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env in - let sig1 = subst_structure alias sig1 in - let alias1 = update_subst alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias1 sig2' in - let sig2 = subst_signature_msid msid2 mp1 sig2 in +and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = @@ -340,38 +326,19 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = Labmap.find l map1 with Not_found -> error_no_such_label_sub l - (string_of_msid msid1) (string_of_msid msid2) + (string_of_mp mp1) in match spec2 with | SFBconst cb2 -> - check_constant cst env msid1 l info1 cb2 spec2 + check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive cst env msid1 l info1 mib2 spec2 + check_inductive cst env + mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules cst env msid1 l msb msb2 alias - | Alias (mp,typ_opt) ->let msb = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb2 alias - | _ -> error_not_match l spec2 - end - | SFBalias (mp,typ_opt,_) -> - begin - match info1 with - | Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst - | Module msb -> - let msb1 = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb1 alias + | Module msb -> check_modules cst env msb msb2 + subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> @@ -380,50 +347,69 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - check_modtypes cst env mtb1 mtb2 true + let env = add_module (module_body_of_type mtb2.typ_mp mtb2) + (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in + check_modtypes cst env mtb1 mtb2 subst1 subst2 true in List.fold_left check_one_body cst sig2 - -and check_modtypes cst env mtb1 mtb2 equiv = - if mtb1==mtb2 then cst else (* just in case :) *) - let mtb1',mtb2'= - (match mtb1.typ_strength with - None -> eval_struct env mtb1.typ_expr, - eval_struct env mtb2.typ_expr - | Some mp -> strengthen env mtb1.typ_expr mp, - eval_struct env mtb2.typ_expr) in - let rec check_structure cst env str1 str2 equiv = - match str1, str2 with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - let cst = check_signatures cst env - (msid1,list1) mtb1.typ_alias (msid2,list2) in - if equiv then - check_signatures cst env - (msid2,list2) mtb2.typ_alias (msid1,list1) - else - cst +and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 then cst else + let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in + let rec check_structure cst env str1 str2 equiv subst1 subst2 = + match str1,str2 with + | SEBstruct (list1), + SEBstruct (list2) -> + if equiv then + let subst2 = + add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in + Univ.Constraint.union + (check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta) + (check_signatures cst env + mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 + mtb2.typ_delta mtb1.typ_delta) + else + check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta | SEBfunctor (arg_id1,arg_t1,body_t1), SEBfunctor (arg_id2,arg_t2,body_t2) -> - let cst = check_modtypes cst env arg_t2 arg_t1 equiv in + let subst1 = + (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in + let cst = check_modtypes cst env + arg_t2 arg_t1 subst2 subst1 + equiv in (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + let env = add_module + (module_body_of_type (MPbound arg_id2) arg_t2) env in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_struct_expr - (map_mbid arg_id1 (MPbound arg_id2) None) - body_t1 + let subst1 = + (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in + let env = match body_t1 with + SEBstruct str -> + add_module {mod_mp = mtb1.typ_mp; + mod_expr = None; + mod_type = subst_struct_expr subst1 body_t1; + mod_type_alg= None; + mod_constraints=mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + | _ -> env in - check_structure cst env (eval_struct env body_t1') - (eval_struct env body_t2) equiv + check_structure cst env body_t1 body_t2 equiv + subst1 + subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 in if mtb1'== mtb2' then cst - else check_structure cst env mtb1' mtb2' equiv + else check_structure cst env mtb1' mtb2' equiv subst1 subst2 let check_subtypes env sup super = - check_modtypes Constraint.empty env sup super false + let env = add_module + (module_body_of_type sup.typ_mp sup) env in + check_modtypes Constraint.empty env + (strengthen env sup sup.typ_mp) super empty_subst + (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false + diff --git a/kernel/term.ml b/kernel/term.ml index 68ea2ed3fe..685656592f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -184,7 +184,7 @@ module Hconstr = type t = constr type u = (constr -> constr) * ((sorts -> sorts) * (constant -> constant) * - (kernel_name -> kernel_name) * (name -> name) * + (mutual_inductive -> mutual_inductive) * (name -> name) * (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term @@ -609,6 +609,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with application associativity, binders name and Cases annotations are not taken into account *) + let compare_constr f t1 t2 = match kind_of_term t1, kind_of_term t2 with | Rel n1, Rel n2 -> n1 = n2 @@ -630,9 +631,9 @@ let compare_constr f t1 t2 = f h1 h2 & List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> c1 = c2 - | Ind c1, Ind c2 -> c1 = c2 - | Construct c1, Construct c2 -> c1 = c2 + | Const c1, Const c2 -> eq_constant c1 c2 + | Ind c1, Ind c2 -> eq_ind c1 c2 + | Construct c1, Construct c2 -> eq_constructor c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> diff --git a/kernel/term.mli b/kernel/term.mli index 5929250db4..0de8316689 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -595,7 +595,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val hcons_constr: (constant -> constant) * - (kernel_name -> kernel_name) * + (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) * (name -> name) * (identifier -> identifier) * diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 0dd119f7bb..a35d1d88ec 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -83,7 +83,7 @@ and conv_whd pb k whd1 whd2 cu = and conv_atom pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind (kn1,i1), Aind(kn2,i2) -> - if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 then conv_stack k stk1 stk2 cu else raise NotConvertible @@ -94,7 +94,7 @@ and conv_atom pb k a1 stk1 a2 stk2 cu = | Aiddef(ik1,v1), Aiddef(ik2,v2) -> begin try - if ik1 = ik2 && compare_stack stk1 stk2 then + if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack k stk1 stk2 cu else raise NotConvertible with NotConvertible -> @@ -191,11 +191,11 @@ let rec conv_eq pb t1 t2 cu = if e1 = e2 then conv_eq_vect l1 l2 cu else raise NotConvertible | Const c1, Const c2 -> - if c1 = c2 then cu else raise NotConvertible + if eq_constant c1 c2 then cu else raise NotConvertible | Ind c1, Ind c2 -> - if c1 = c2 then cu else raise NotConvertible + if eq_ind c1 c2 then cu else raise NotConvertible | Construct c1, Construct c2 -> - if c1 = c2 then cu else raise NotConvertible + if eq_constructor c1 c2 then cu else raise NotConvertible | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> let pcu = conv_eq CONV p1 p2 cu in let ccu = conv_eq CONV c1 c2 pcu in |