diff options
| -rw-r--r-- | kernel/environ.ml | 16 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 36 | ||||
| -rw-r--r-- | kernel/modops.mli | 12 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 1121 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 141 | ||||
| -rw-r--r-- | library/declaremods.ml | 39 | ||||
| -rw-r--r-- | library/global.ml | 149 | ||||
| -rw-r--r-- | library/global.mli | 121 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 19 |
13 files changed, 776 insertions, 893 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a3e51aa1..8a4871a1d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,18 +275,16 @@ let keep_hyps env needed = (* Modules *) -let add_modtype ln mtb env = - let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in - let new_globals = - { env.env_globals with - env_modtypes = new_modtypes } in +let add_modtype mtb env = + let mp = mtb.typ_mp in + let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in + let new_globals = { env.env_globals with env_modtypes = new_modtypes } in { env with env_globals = new_globals } -let shallow_add_module mp mb env = +let shallow_add_module mb env = + let mp = mb.mod_mp in let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = - { env.env_globals with - env_modules = new_mods } in + let new_globals = { env.env_globals with env_modules = new_mods } in { env with env_globals = new_globals } let lookup_module mp env = diff --git a/kernel/environ.mli b/kernel/environ.mli index ffa3ceb87..0dcc291b5 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -143,10 +143,10 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body (** {5 Modules } *) -val add_modtype : module_path -> module_type_body -> env -> env +val add_modtype : module_type_body -> env -> env (** [shallow_add_module] does not add module components *) -val shallow_add_module : module_path -> module_body -> env -> env +val shallow_add_module : module_body -> env -> env val lookup_module : module_path -> env -> module_body val lookup_modtype : module_path -> env -> module_type_body diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 67db4e806..befa822ce 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -353,7 +353,7 @@ let rec translate_struct_include_module_entry env mp inl = function | MSEapply (fexpr,mexpr) -> let ftrans = translate_struct_include_module_entry env mp inl fexpr in translate_apply env inl ftrans mexpr (fun _ _ _ -> None) - | _ -> error ("You cannot Include a high-order structure.") + | _ -> Modops.error_higher_order_include () let rec add_struct_expr_constraints env = function | SEBident _ -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 5f79c5363..d431fdfdd 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -54,15 +54,13 @@ type module_typing_error = | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body - | NoModuleToEnd - | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string | NotAConstant of Label.t | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t - | NonEmptyLocalContect of Label.t option | LabelMissing of Label.t * string + | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -93,12 +91,6 @@ let error_incompatible_labels l l' = let error_signature_expected mtb = raise (ModuleTypingError (SignatureExpected mtb)) -let error_no_module_to_end _ = - raise (ModuleTypingError NoModuleToEnd) - -let error_no_modtype_to_end _ = - raise (ModuleTypingError NoModuleTypeToEnd) - let error_not_a_module s = raise (ModuleTypingError (NotAModule s)) @@ -111,13 +103,11 @@ let error_incorrect_with_constraint l = let error_generative_module_expected l = raise (ModuleTypingError (GenerativeModuleExpected l)) -let error_non_empty_local_context lo = - raise (ModuleTypingError (NonEmptyLocalContect lo)) - let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) -(************************) +let error_higher_order_include () = + raise (ModuleTypingError HigherOrderInclude) let destr_functor mtb = match mtb with @@ -267,19 +257,21 @@ let rec add_signature mp sign resolver env = | SFBmind mib -> Environ.add_mind (mind_of_delta_kn resolver kn) mib env | SFBmodule mb -> add_module mb env (* adds components as well *) - | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env + | SFBmodtype mtb -> Environ.add_modtype mtb env in List.fold_left add_one env sign -and add_module mb env = +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 ~label:"Modops" (Pp.str "the evaluation of the structure failed ") + let env = Environ.shallow_add_module 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 ~label:"Modops" + (Pp.str "the evaluation of the structure failed ") let strengthen_const mp_from l cb resolver = match cb.const_body with diff --git a/kernel/modops.mli b/kernel/modops.mli index c0943233b..ea92c45ea 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -87,15 +87,13 @@ type module_typing_error = | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body - | NoModuleToEnd - | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string | NotAConstant of Label.t | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t - | NonEmptyLocalContect of Label.t option | LabelMissing of Label.t * string + | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -115,10 +113,6 @@ val error_no_such_label : Label.t -> 'a val error_signature_expected : struct_expr_body -> 'a -val error_no_module_to_end : unit -> 'a - -val error_no_modtype_to_end : unit -> 'a - val error_not_a_module : string -> 'a val error_not_a_constant : Label.t -> 'a @@ -127,6 +121,6 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a -val error_non_empty_local_context : Label.t option -> 'a - val error_no_such_label_sub : Label.t->string->'a + +val error_higher_order_include : unit -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d95e9fe73..c7711b137 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -25,13 +25,13 @@ [,] |- push_named_assum(a,T): - + E[Delta,Gamma] |-_G ------------------------ E[Delta,Gamma,a:T] |-_G' push_named_def(a,t,T): - + E[Delta,Gamma] |-_G --------------------------- E[Delta,Gamma,a:=t:T] |-_G' @@ -57,56 +57,117 @@ etc. *) -open Errors open Util open Names -open Univ open Declarations -open Environ -open Entries -open Typeops -open Modops -open Subtyping -open Mod_typing -open Mod_subst +(** {6 Safe environments } + + Fields of [safe_environment] : + + - [env] : the underlying environment (cf Environ) + - [modpath] : the current module name + - [modvariant] : + * NONE before coqtop initialization (or when -notop is used) + * LIBRARY at toplevel of a compilation or a regular coqtop session + * STRUCT (params,oldsenv) : inside a local module, with + module parameters [params] and earlier environment [oldsenv] + * SIG (params,oldsenv) : same for a local module type + - [modresolver] : delta_resolver concerning the module content + - [paramresolver] : delta_resolver concerning the module parameters + - [revstruct] : current module content, most recent declarations first + - [modlabels] and [objlabels] : names defined in the current module, + either for modules/modtypes or for constants/inductives. + These fields could be deduced from [revstruct], but they allow faster + name freshness checks. + - [univ] and [future_cst] : current and future universe constraints + - [engagement] : are we Set-impredicative ? + - [imports] : names and digests of Require'd libraries since big-bang. + This field will only grow + - [loads] : list of libraries Require'd inside the current module. + They will be propagated to the upper module level when + the current module ends. + - [local_retroknowledge] -type modvariant = - | NONE - | SIG of (* funsig params *) (MBId.t * module_type_body) list - | STRUCT of (* functor params *) (MBId.t * module_type_body) list - | LIBRARY of DirPath.t - -type module_info = - {modpath : module_path; - label : Label.t; - variant : modvariant; - resolver : delta_resolver; - resolver_of_param : delta_resolver;} - -let set_engagement_opt oeng env = - match oeng with - Some eng -> set_engagement eng env - | _ -> env +*) type library_info = DirPath.t * Digest.t +(** Functor and funsig parameters, most recent first *) +type module_parameters = (MBId.t * module_type_body) list + type safe_environment = - { old : safe_environment; - env : env; - modinfo : module_info; - modlabels : Label.Set.t; - objlabels : Label.Set.t; - revstruct : structure_body; - univ : Univ.constraints; - future_cst : Univ.constraints Future.computation list; - engagement : engagement option; - imports : library_info list; - loads : (module_path * module_body) list; - local_retroknowledge : Retroknowledge.action list} + { env : Environ.env; + modpath : module_path; + modvariant : modvariant; + modresolver : Mod_subst.delta_resolver; + paramresolver : Mod_subst.delta_resolver; + revstruct : structure_body; + modlabels : Label.Set.t; + objlabels : Label.Set.t; + univ : Univ.constraints; + future_cst : Univ.constraints Future.computation list; + engagement : engagement option; + imports : library_info list; + loads : (module_path * module_body) list; + local_retroknowledge : Retroknowledge.action list} + +and modvariant = + | NONE + | LIBRARY + | SIG of module_parameters * safe_environment (** saved env *) + | STRUCT of module_parameters * safe_environment (** saved env *) + +let empty_environment = + { env = Environ.empty_env; + modpath = initial_path; + modvariant = NONE; + modresolver = Mod_subst.empty_delta_resolver; + paramresolver = Mod_subst.empty_delta_resolver; + revstruct = []; + modlabels = Label.Set.empty; + objlabels = Label.Set.empty; + future_cst = []; + univ = Univ.empty_constraint; + engagement = None; + imports = []; + loads = []; + local_retroknowledge = [] } + +let is_initial senv = + match senv.revstruct, senv.modvariant with + | [], NONE -> ModPath.equal senv.modpath initial_path + | _ -> false + +let delta_of_senv senv = senv.modresolver,senv.paramresolver + +(** The safe_environment state monad *) + +type safe_transformer0 = safe_environment -> safe_environment +type 'a safe_transformer = safe_environment -> 'a * safe_environment + + +(** {6 Engagement } *) + +let set_engagement_opt env = function + | Some c -> Environ.set_engagement c env + | None -> env + +let set_engagement c senv = + { senv with + env = Environ.set_engagement c senv.env; + engagement = Some c } + +(** Check that the engagement [c] expected by a library matches + the current (initial) one *) +let check_engagement env c = + match Environ.engagement env, c with + | None, Some ImpredicativeSet -> + Errors.error "Needs option -impredicative-set." + | _ -> () -let exists_modlabel l senv = Label.Set.mem l senv.modlabels -let exists_objlabel l senv = Label.Set.mem l senv.objlabels + +(** {6 Stm machinery } *) (* type to be maintained isomorphic to Entries.side_effects *) (* XXX ideally this function obtains a valid side effect that @@ -129,11 +190,11 @@ let add_constraints cst senv = env = Environ.add_constraints cst senv.env; univ = Univ.union_constraints cst senv.univ } -let is_curmod_library senv = - match senv.modinfo.variant with LIBRARY _ -> true | _ -> false +let is_curmod_library senv = + match senv.modvariant with LIBRARY -> true | _ -> false let join_safe_environment e = - join_structure_body e.revstruct; + Modops.join_structure_body e.revstruct; List.fold_left (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst @@ -142,27 +203,125 @@ let join_safe_environment e = (* this is there to explore the opaque pre-env structure but is * not part of the trusted code base *) let prune_env env = - let env = Environ.pre_env env in + let open Pre_env in let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in let prune_globals glob = - {glob with Pre_env.env_constants = - Cmap_env.map prune_ckey glob.Pre_env.env_constants } in - Environ.env_of_pre_env - {env with Pre_env.env_globals = prune_globals env.Pre_env.env_globals} + { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants } + in + let env = Environ.pre_env env in + Environ.env_of_pre_env {env with env_globals = prune_globals env.env_globals} let prune_safe_environment e = - let e = {e with revstruct = prune_structure_body e.revstruct; - future_cst = []; - env = prune_env e.env} in - {e with old = e} + { e with + modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE); + revstruct = Modops.prune_structure_body e.revstruct; + future_cst = []; + env = prune_env e.env } + + +(** {6 Various checks } *) + +let exists_modlabel l senv = Label.Set.mem l senv.modlabels +let exists_objlabel l senv = Label.Set.mem l senv.objlabels let check_modlabel l senv = - if exists_modlabel l senv then error_existing_label l + if exists_modlabel l senv then Modops.error_existing_label l + let check_objlabel l senv = - if exists_objlabel l senv then error_existing_label l + if exists_objlabel l senv then Modops.error_existing_label l let check_objlabels ls senv = Label.Set.iter (fun l -> check_objlabel l senv) ls +(** Are we closing the right module / modtype ? + No user error here, since the opening/ending coherence + is now verified in [vernac_end_segment] *) + +let check_current_label lab = function + | MPdot (_,l) -> assert (Label.equal lab l) + | _ -> assert false + +let check_struct = function + | STRUCT (params,oldsenv) -> params, oldsenv + | NONE | LIBRARY | SIG _ -> assert false + +let check_sig = function + | SIG (params,oldsenv) -> params, oldsenv + | NONE | LIBRARY | STRUCT _ -> assert false + +let check_current_library dir senv = match senv.modvariant with + | LIBRARY -> assert (ModPath.equal senv.modpath (MPfile dir)) + | NONE | STRUCT _ | SIG _ -> assert false (* cf Lib.end_compilation *) + +(** When operating on modules, we're normally outside sections *) + +let check_empty_context senv = + assert (Environ.empty_context senv.env) + +(** When adding a parameter to the current module/modtype, + it must have been freshly started *) + +let check_empty_struct senv = + assert (List.is_empty senv.revstruct + && List.is_empty senv.loads) + +(** When starting a library, the current environment should be initial + i.e. only composed of Require's *) + +let check_initial senv = assert (is_initial senv) + +(** When loading a library, its dependencies should be already there, + with the correct digests. *) + +let check_imports current_libs needed = + let check (id,stamp) = + try + let actual_stamp = List.assoc id current_libs in + if not (String.equal stamp actual_stamp) then + Errors.error + ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") + with Not_found -> + Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + in + Array.iter check needed + + +(** {6 Insertion of section variables} *) + +(** They are now typed before being added to the environment. + Same as push_named, but check that the variable is not already + there. Should *not* be done in Environ because tactics add temporary + hypothesis many many times, and the check performed here would + cost too much. *) + +let safe_push_named (id,_,_ as d) env = + let _ = + try + let _ = Environ.lookup_named id env in + Errors.error ("Identifier "^Id.to_string id^" already defined.") + with Not_found -> () in + Environ.push_named d env + +let push_named_def (id,de) senv = + let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in + (* XXX for now we force *) + let c = match c with + | Def c -> Lazyconstr.force c + | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c) + | _ -> assert false in + let cst = Future.join cst in + let senv' = add_constraints (Now cst) senv in + let env'' = safe_push_named (id,Some c,typ) senv'.env in + (cst, {senv' with env=env''}) + +let push_named_assum (id,t) senv = + let (t,cst) = Term_typing.translate_local_assum senv.env t in + let senv' = add_constraints (Now cst) senv in + let env'' = safe_push_named (id,None,t) senv'.env in + (cst, {senv' with env=env''}) + + +(** {6 Insertion of new declarations to current environment } *) + let labels_of_mib mib = let add,get = let labels = ref Label.Set.empty in @@ -176,43 +335,23 @@ let labels_of_mib mib = Array.iter visit_mip mib.mind_packets; get () -(* a small hack to avoid variants and an unused case in all functions *) -let rec empty_environment = - { old = empty_environment; - env = empty_env; - modinfo = { - modpath = initial_path; - label = Label.make "_"; - variant = NONE; - resolver = empty_delta_resolver; - resolver_of_param = empty_delta_resolver}; - modlabels = Label.Set.empty; - objlabels = Label.Set.empty; - revstruct = []; - future_cst = []; - univ = Univ.empty_constraint; - engagement = None; - imports = []; - loads = []; - local_retroknowledge = [] } - let constraints_of_sfb = function | SFBmind mib -> Now mib.mind_constraints | SFBmodtype mtb -> Now mtb.typ_constraints | SFBmodule mb -> Now mb.mod_constraints - | SFBconst cb -> + | SFBconst cb -> match Future.peek_val cb.const_constraints with | Some c -> Now c | None -> Later cb.const_constraints -(* A generic function for adding a new field in a same environment. - It also performs the corresponding [add_constraints]. *) +(** A generic function for adding a new field in a same environment. + It also performs the corresponding [add_constraints]. *) type generic_name = | C of constant | I of mutual_inductive - | MT of module_path - | M + | M (** name already known, cf the mod_mp field *) + | MT (** name already known, cf the typ_mp field *) let add_field ((l,sfb) as field) gn senv = let mlabs,olabs = match sfb with @@ -228,98 +367,32 @@ let add_field ((l,sfb) as field) gn senv = let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env | SFBmind mib, I mind -> Environ.add_mind mind mib senv.env - | SFBmodtype mtb, MT mp -> Environ.add_modtype mp mtb senv.env + | SFBmodtype mtb, MT -> Environ.add_modtype mtb senv.env | SFBmodule mb, M -> Modops.add_module mb senv.env | _ -> assert false in { senv with env = env'; + revstruct = field :: senv.revstruct; modlabels = Label.Set.union mlabs senv.modlabels; - objlabels = Label.Set.union olabs senv.objlabels; - revstruct = field :: senv.revstruct } + objlabels = Label.Set.union olabs senv.objlabels } -(* Applying a certain function to the resolver of a safe environment *) +(** Applying a certain function to the resolver of a safe environment *) -let update_resolver f senv = - let mi = senv.modinfo in - { senv with modinfo = { mi with resolver = f mi.resolver }} +let update_resolver f senv = { senv with modresolver = f senv.modresolver } - -(* universal lifting, used for the "get" operations mostly *) -let retroknowledge f senv = - Environ.retroknowledge f (env_of_senv senv) - -let register senv field value by_clause = - (* todo : value closed, by_clause safe, by_clause of the proper type*) - (* spiwack : updates the safe_env with the information that the register - action has to be performed (again) when the environement is imported *) - {senv with - env = Environ.register senv.env field value; - local_retroknowledge = - Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge - } - -(* spiwack : currently unused *) -let unregister senv field = - (*spiwack: todo: do things properly or delete *) - {senv with env = Environ.unregister senv.env field} -(* /spiwack *) - - - - - - - - - - -(* Insertion of section variables. They are now typed before being - added to the environment. *) - -(* Same as push_named, but check that the variable is not already - there. Should *not* be done in Environ because tactics add temporary - hypothesis many many times, and the check performed here would - cost too much. *) -let safe_push_named (id,_,_ as d) env = - let _ = - try - let _ = lookup_named id env in - error ("Identifier "^Id.to_string id^" already defined.") - with Not_found -> () in - Environ.push_named d env - -let push_named_def (id,de) senv = - let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in - (* XXX for now we force *) - let c = match c with - | Def c -> Lazyconstr.force c - | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c) - | _ -> assert false in - let cst = Future.join cst in - let senv' = add_constraints (Now cst) senv in - let env'' = safe_push_named (id,Some c,typ) senv'.env in - (cst, {senv' with env=env''}) - -let push_named_assum (id,t) senv = - let (t,cst) = Term_typing.translate_local_assum senv.env t in - let senv' = add_constraints (Now cst) senv in - let env'' = safe_push_named (id,None,t) senv'.env in - (cst, {senv' with env=env''}) - - -(* Insertion of constants and parameters in environment. *) +(** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of constant_entry + | ConstantEntry of Entries.constant_entry | GlobalRecipe of Cooking.recipe let add_constant dir l decl senv = - let kn = make_con senv.modinfo.modpath dir l in + let kn = make_con senv.modpath dir l in let cb = match decl with | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce | GlobalRecipe r -> - let cb = Term_typing.translate_recipe senv.env kn r in + let cb = Term_typing.translate_recipe senv.env kn r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb in let cb = match cb.const_body with @@ -333,362 +406,271 @@ let add_constant dir l decl senv = let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> - update_resolver (add_inline_delta_resolver (user_con kn) (lev,None)) senv' + update_resolver + (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' | _ -> senv' in kn, senv'' -(* Insertion of inductive types. *) +(** Insertion of inductive types *) + +let check_mind mie lab = + let open Entries in + match mie.mind_entry_inds with + | [] -> assert false (* empty inductive entry *) + | oie::_ -> + (* The label and the first inductive type name should match *) + assert (Id.equal (Label.to_id lab) oie.mind_entry_typename) let add_mind dir l mie senv = - let () = match mie.mind_entry_inds with - | [] -> - anomaly (Pp.str "empty inductive types declaration") - (* this test is repeated by translate_mind *) - | _ -> () - in - let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in - if not (Label.equal l (Label.of_id id)) then - anomaly (Pp.str "the label of inductive packet and its first inductive \ - type do not match"); - let kn = make_mind senv.modinfo.modpath dir l in + let () = check_mind mie l in + let kn = make_mind senv.modpath dir l in let mib = Term_typing.translate_mind senv.env kn mie in - let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib + let mib = + match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib in - let senv' = add_field (l,SFBmind mib) (I kn) senv in - kn, senv' + kn, add_field (l,SFBmind mib) (I kn) senv -(* Insertion of module types *) +(** Insertion of module types *) let add_modtype l mte inl senv = - let mp = MPdot(senv.modinfo.modpath, l) in - let mtb = translate_module_type senv.env mp inl mte in - let senv' = add_field (l,SFBmodtype mtb) (MT mp) senv in + let mp = MPdot(senv.modpath, l) in + let mtb = Mod_typing.translate_module_type senv.env mp inl mte in + let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' -(* full_add_module adds module with universes and constraints *) +(** full_add_module adds module with universes and constraints *) + let full_add_module mb senv = let senv = add_constraints (Now mb.mod_constraints) senv in { senv with env = Modops.add_module mb senv.env } -(* Insertion of modules *) +(** Insertion of modules *) let add_module l me inl senv = - let mp = MPdot(senv.modinfo.modpath, l) in - let mb = translate_module senv.env mp inl me in + let mp = MPdot(senv.modpath, l) in + let mb = Mod_typing.translate_module senv.env mp inl me in let senv' = add_field (l,SFBmodule mb) M senv in let senv'' = match mb.mod_type with - | SEBstruct _ -> update_resolver (add_delta_resolver mb.mod_delta) senv' + | SEBstruct _ -> + update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv' | _ -> senv' in - mp,mb.mod_delta,senv'' + (mp,mb.mod_delta),senv'' -(* Interactive modules *) + +(** {6 Starting / ending interactive modules and module types } *) let start_module l senv = - check_modlabel l senv; - 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; - modlabels = Label.Set.empty; - objlabels = Label.Set.empty; - revstruct = []; - univ = Univ.empty_constraint; - future_cst = []; - engagement = None; - imports = senv.imports; - loads = []; - (* spiwack : not sure, but I hope it's correct *) - local_retroknowledge = [] } + let () = check_modlabel l senv in + let () = check_empty_context senv in + let mp = MPdot(senv.modpath, l) in + mp, + { empty_environment with + env = senv.env; + modpath = mp; + modvariant = STRUCT ([],senv); + imports = senv.imports } -let end_module l restype senv = - let oldsenv = senv.old in - let modinfo = senv.modinfo in - let mp = senv.modinfo.modpath in - let restype = - Option.map - (fun (res,inl) -> translate_module_type senv.env mp inl res) restype in - let params,is_functor = - match modinfo.variant with - | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () - | STRUCT params -> params, (List.length params > 0) - in - if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_non_empty_local_context None; - let functorize_struct tb = - List.fold_left - (fun mtb (arg_id,arg_b) -> - SEBfunctor(arg_id,arg_b,mtb)) - tb - params - in - let auto_tb = - SEBstruct (List.rev senv.revstruct) - in - let mexpr,mod_typ,mod_typ_alg,resolver,cst = - match restype with - | None -> let mexpr = functorize_struct auto_tb in - mexpr,mexpr,None,modinfo.resolver,empty_constraint - | Some mtb -> - let auto_mtb = { - typ_mp = senv.modinfo.modpath; - typ_expr = auto_tb; - typ_expr_alg = None; - typ_constraints = empty_constraint; - 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 cst = union_constraints cst senv.univ in - let mb = - { mod_mp = mp; - mod_expr = Some mexpr; - mod_type = mod_typ; - mod_type_alg = mod_typ_alg; - mod_constraints = cst; - mod_delta = resolver; - mod_retroknowledge = senv.local_retroknowledge } - 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 (_,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 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,resolver,{ old = oldsenv.old; - env = newenv; - modinfo = modinfo; - modlabels = Label.Set.add l oldsenv.modlabels; - objlabels = oldsenv.objlabels; - revstruct = (l,SFBmodule mb)::oldsenv.revstruct; - univ = Univ.union_constraints senv'.univ oldsenv.univ; - future_cst = senv'.future_cst @ oldsenv.future_cst; - (* 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 is_module inl senv = - let sign,cst,resolver = - if is_module then - let sign,_,resolver,cst = - translate_struct_include_module_entry senv.env - senv.modinfo.modpath inl me in - sign,cst,resolver - else - let mtb = - translate_module_type senv.env - senv.modinfo.modpath inl me in - mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta - in - let senv = add_constraints (Now cst) senv in - let mp_sup = senv.modinfo.modpath in - (* Include Self support *) - let rec compute_sign sign mb resolver senv = - match sign with - | SEBfunctor(mbid,mtb,str) -> - let cst_sub = check_subtypes senv.env mb mtb in - let senv = add_constraints (Now cst_sub) senv in - let mpsup_delta = - inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta - in - let subst = map_mbid mbid mp_sup mpsup_delta in - let resolver = subst_codom_delta_resolver subst resolver in - (compute_sign - (subst_struct_expr subst str) mb resolver senv) - | str -> resolver,str,senv - in - let resolver,sign,senv = compute_sign sign {typ_mp = mp_sup; - typ_expr = SEBstruct (List.rev senv.revstruct); - typ_expr_alg = None; - typ_constraints = empty_constraint; - typ_delta = senv.modinfo.resolver} resolver senv - in - let str = match sign with - | SEBstruct(str_l) -> str_l - | _ -> error ("You cannot Include a higher-order structure.") - in - let senv = update_resolver (add_delta_resolver resolver) senv - in - let add senv ((l,elem) as field) = - let new_name = match elem with - | SFBconst _ -> - C (constant_of_delta_kn resolver (KerName.make2 mp_sup l)) - | SFBmind _ -> - I (mind_of_delta_kn resolver (KerName.make2 mp_sup l)) - | SFBmodule _ -> M - | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l)) - in - add_field field new_name senv - in - resolver,(List.fold_left add senv str) - -(* Adding parameters to modules or module types *) +let start_modtype l senv = + let () = check_modlabel l senv in + let () = check_empty_context senv in + let mp = MPdot(senv.modpath, l) in + mp, + { empty_environment with + env = senv.env; + modpath = mp; + modvariant = SIG ([], senv); + imports = senv.imports } + +(** Adding parameters to the current module or module type. + This module should have been freshly started. *) let add_module_parameter mbid mte inl senv = - let () = match senv.revstruct, senv.loads with - | [], _ :: _ | _ :: _, [] -> - anomaly (Pp.str "Cannot add a module parameter to a non empty module") - | _ -> () - in + let () = check_empty_struct senv in let mp = MPbound mbid in - let mtb = translate_module_type senv.env mp inl mte in - let senv = full_add_module (module_body_of_type mp mtb) senv + let mtb = Mod_typing.translate_module_type senv.env mp inl mte in + let senv = full_add_module (Modops.module_body_of_type mp mtb) senv in + let new_variant = match senv.modvariant with + | STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv) + | SIG (params,oldenv) -> SIG ((mbid,mtb) :: params, oldenv) + | _ -> assert false in - let new_variant = match senv.modinfo.variant with - | STRUCT params -> STRUCT ((mbid,mtb) :: params) - | SIG params -> SIG ((mbid,mtb) :: params) - | _ -> - let msg = "Module parameters can only be added to modules or signatures" - in anomaly (Pp.str msg) + let new_paramresolver = match mtb.typ_expr with + | SEBstruct _ -> + Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver + | _ -> senv.paramresolver in + mtb.typ_delta, + { senv with + modvariant = new_variant; + paramresolver = new_paramresolver } + +let functorize_struct params seb0 = + List.fold_left + (fun seb (arg_id,arg_b) -> SEBfunctor(arg_id,arg_b,seb)) + seb0 params + +let propagate_loads senv = + List.fold_left + (fun env (_,mb) -> full_add_module mb env) + senv + (List.rev senv.loads) + +(** Build the module body of the current module, taking in account + a possible return type (_:T) *) + +let build_module_body params restype senv = + let mp = senv.modpath in + let mexpr = SEBstruct (List.rev senv.revstruct) in + let mexpr' = functorize_struct params mexpr in + match restype with + | None -> + { mod_mp = mp; + mod_expr = Some mexpr'; + mod_type = mexpr'; + mod_type_alg = None; + mod_constraints = senv.univ; + mod_delta = senv.modresolver; + mod_retroknowledge = senv.local_retroknowledge } + | Some (res,inl) -> + let res_mtb = Mod_typing.translate_module_type senv.env mp inl res in + let auto_mtb = { + typ_mp = mp; + typ_expr = mexpr; + typ_expr_alg = None; + typ_constraints = Univ.empty_constraint; + typ_delta = Mod_subst.empty_delta_resolver} in + let cst = Subtyping.check_subtypes senv.env auto_mtb res_mtb in + { mod_mp = mp; + mod_expr = Some mexpr'; + mod_type = functorize_struct params res_mtb.typ_expr; + mod_type_alg = + Option.map (functorize_struct params) res_mtb.typ_expr_alg; + mod_constraints = Univ.union_constraints cst senv.univ; + mod_delta = res_mtb.typ_delta; + mod_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}; - modlabels = senv.modlabels; - objlabels = senv.objlabels; - revstruct = []; - univ = senv.univ; - future_cst = senv.future_cst; - engagement = senv.engagement; - imports = senv.imports; - loads = []; - local_retroknowledge = senv.local_retroknowledge } - - -(* Interactive module types *) +(** Returning back to the old pre-interactive-module environment, + with one extra component and some updated fields + (constraints, imports, etc) *) + +let propagate_senv newdef newenv newresolver senv oldsenv = + { oldsenv with + env = newenv; + modresolver = newresolver; + revstruct = newdef::oldsenv.revstruct; + modlabels = Label.Set.add (fst newdef) oldsenv.modlabels; + univ = Univ.union_constraints senv.univ oldsenv.univ; + future_cst = senv.future_cst @ oldsenv.future_cst; + (* 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 } -let start_modtype l senv = - check_modlabel l senv; - 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; - modlabels = Label.Set.empty; - objlabels = Label.Set.empty; - revstruct = []; - univ = Univ.empty_constraint; - future_cst = []; - engagement = None; - imports = senv.imports; - loads = [] ; - (* spiwack: not 100% sure, but I think it should be like that *) - local_retroknowledge = []} +let end_module l restype senv = + let mp = senv.modpath in + let params, oldsenv = check_struct senv.modvariant in + let () = check_current_label l mp in + let () = check_empty_context senv in + let mbids = List.rev_map fst params in + let mb = build_module_body params restype senv in + let newenv = oldsenv.env in + let newenv = set_engagement_opt newenv senv.engagement in + let senv'= propagate_loads {senv with env=newenv} in + let newenv = Environ.add_constraints mb.mod_constraints senv'.env in + let newenv = Modops.add_module mb newenv in + let newresolver = match mb.mod_type with + | SEBstruct _ -> + Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver + | _ -> oldsenv.modresolver + in + (mp,mbids,mb.mod_delta), + propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv let end_modtype l senv = - let oldsenv = senv.old in - let modinfo = senv.modinfo in - let params = - match modinfo.variant with - | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end () - | SIG params -> params - in - if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_non_empty_local_context None; - let auto_tb = - SEBstruct (List.rev senv.revstruct) - in - let mtb_expr = - List.fold_left - (fun mtb (arg_id,arg_b) -> - SEBfunctor(arg_id,arg_b,mtb)) - auto_tb - params - in - let mp = MPdot (oldsenv.modinfo.modpath, l) in + let mp = senv.modpath in + let params, oldsenv = check_sig senv.modvariant in + let () = check_current_label l mp in + let () = check_empty_context senv in + let mbids = List.rev_map fst params in + let auto_tb = SEBstruct (List.rev senv.revstruct) in let newenv = oldsenv.env in - 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 mb env) - senv - (List.rev senv.loads) - 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; - modlabels = Label.Set.add l oldsenv.modlabels; - objlabels = oldsenv.objlabels; - revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; - univ = Univ.union_constraints senv.univ oldsenv.univ; - future_cst = senv.future_cst @ oldsenv.future_cst; - 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 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 = - match Environ.engagement env, c with - | Some ImpredicativeSet, Some ImpredicativeSet -> () - | _, None -> () - | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set." - -let set_engagement c senv = - {senv with - env = Environ.set_engagement c senv.env; - engagement = Some c } - -(* Libraries = Compiled modules *) + let newenv = Environ.add_constraints senv.univ newenv in + let newenv = set_engagement_opt newenv senv.engagement in + let senv' = propagate_loads {senv with env=newenv} in + let mtb = + { typ_mp = mp; + typ_expr = functorize_struct params auto_tb; + typ_expr_alg = None; + typ_constraints = senv'.univ; + typ_delta = senv.modresolver } + in + let newenv = Environ.add_modtype mtb senv'.env in + let newresolver = oldsenv.modresolver in + (mp,mbids), + propagate_senv (l,SFBmodtype mtb) newenv newresolver senv' oldsenv + +(** {6 Inclusion of module or module type } *) + +let add_include me is_module inl senv = + let mp_sup = senv.modpath in + let sign,cst,resolver = + if is_module then + let sign,_,resolver,cst = + Mod_typing.translate_struct_include_module_entry senv.env mp_sup inl me + in + sign,cst,resolver + else + let mtb = Mod_typing.translate_module_type senv.env mp_sup inl me in + mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta + in + let senv = add_constraints (Now cst) senv in + (* Include Self support *) + let rec compute_sign sign mb resolver senv = + match sign with + | SEBfunctor(mbid,mtb,str) -> + let cst_sub = Subtyping.check_subtypes senv.env mb mtb in + let senv = add_constraints (Now cst_sub) senv in + let mpsup_delta = + Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta + in + let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in + let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in + compute_sign (Modops.subst_struct_expr subst str) mb resolver senv + | str -> resolver,str,senv + in + let resolver,sign,senv = + let mtb = + { typ_mp = mp_sup; + typ_expr = SEBstruct (List.rev senv.revstruct); + typ_expr_alg = None; + typ_constraints = Univ.empty_constraint; + typ_delta = senv.modresolver } in + compute_sign sign mtb resolver senv + in + let str = match sign with + | SEBstruct str_l -> str_l + | _ -> Modops.error_higher_order_include () + in + let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv + in + let add senv ((l,elem) as field) = + let new_name = match elem with + | SFBconst _ -> + C (Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp_sup l)) + | SFBmind _ -> + I (Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp_sup l)) + | SFBmodule _ -> M + | SFBmodtype _ -> MT + in + add_field field new_name senv + in + resolver, List.fold_left add senv str + +(** {6 Libraries, i.e. compiled modules } *) type compiled_library = { comp_name : DirPath.t; @@ -700,154 +682,135 @@ type compiled_library = { type native_library = Nativecode.global list -let join_compiled_library l = join_module_body l.comp_mod - -(* We check that only initial state Require's were performed before - [start_library] was called *) - -let is_empty senv = match senv.revstruct, senv.modinfo.variant with - | [], NONE -> mp_eq senv.modinfo.modpath initial_path - | _ -> false +let join_compiled_library l = Modops.join_module_body l.comp_mod let start_library dir senv = - if not (is_empty senv) then - anomaly ~label:"Safe_typing.start_library" (Pp.str "environment should be empty"); - let dir_path,l = - match (DirPath.repr dir) with - [] -> anomaly (Pp.str "Empty dirpath in Safe_typing.start_library") - | hd::tl -> - DirPath.make tl, Label.of_id hd - in + check_initial senv; + assert (not (DirPath.is_empty dir)); 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; - modinfo = modinfo; - modlabels = Label.Set.empty; - objlabels = Label.Set.empty; - revstruct = []; - univ = Univ.empty_constraint; - future_cst = []; - engagement = None; - imports = senv.imports; - loads = []; - local_retroknowledge = [] } + mp, + { empty_environment with + env = senv.env; + modpath = mp; + modvariant = LIBRARY; + imports = senv.imports } let export senv dir = - let senv = + let senv = try join_safe_environment senv - with e -> Errors.errorlabstrm "future" (Errors.print e) in - let modinfo = senv.modinfo in - begin - match modinfo.variant with - | LIBRARY dp -> - if not (DirPath.equal dir dp) then - anomaly (Pp.str "We are not exporting the right library!") - | _ -> - anomaly (Pp.str "We are not exporting the library") - end; - (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then - (* error_export_simple *) (); *) - let str = SEBstruct (List.rev senv.revstruct) in - let mp = senv.modinfo.modpath in - let mb = + with e -> Errors.errorlabstrm "future" (Errors.print e) + in + let () = check_current_library dir senv in + let mp = senv.modpath in + let str = SEBstruct (List.rev senv.revstruct) in + let mb = { mod_mp = mp; mod_expr = Some str; mod_type = str; mod_type_alg = None; mod_constraints = senv.univ; - mod_delta = senv.modinfo.resolver; + mod_delta = senv.modresolver; mod_retroknowledge = senv.local_retroknowledge } in let ast, values = if !Flags.no_native_compiler then [], [||] - else let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in - Nativecode.update_locations upds; - ast, values + else + let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in + Nativecode.update_locations upds; + ast, values in let lib = { comp_name = dir; comp_mod = mb; comp_deps = Array.of_list senv.imports; - comp_enga = engagement senv.env; + comp_enga = Environ.engagement senv.env; comp_natsymbs = values } in mp, lib, ast -let check_imports senv needed = - let imports = senv.imports in - let check (id,stamp) = - try - let actual_stamp = List.assoc id imports in - if not (String.equal stamp actual_stamp) then - error - ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") - with Not_found -> - error ("Reference to unknown module "^(DirPath.to_string id)^".") - in - Array.iter check needed - - - -(* we have an inefficiency: Since loaded files are added to the -environment every time a module is closed, their components are -calculated many times. Thic could be avoided in several ways: - -1 - for each file create a dummy environment containing only this -file's components, merge this environment with the global -environment, and store for the future (instead of just its type) - -2 - create "persistent modules" environment table in Environ add put -loaded by side-effect once and for all (like it is done in OCaml). -Would this be correct with respect to undo's and stuff ? -*) - let import lib digest senv = - check_imports senv lib.comp_deps; + check_imports senv.imports lib.comp_deps; check_engagement senv.env lib.comp_enga; let mp = MPfile lib.comp_name in let mb = lib.comp_mod in - let env = senv.env in - let env = Environ.add_constraints mb.mod_constraints env in - let env = Modops.add_module mb env in - let reso = add_delta_resolver mb.mod_delta senv.modinfo.resolver in - let senv = { senv with - env = env; - modinfo = { senv.modinfo with resolver = reso }; + let env = Environ.add_constraints mb.mod_constraints senv.env in + (mp, lib.comp_natsymbs), + { senv with + env = Modops.add_module mb env; + modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; imports = (lib.comp_name,digest)::senv.imports; loads = (mp,mb)::senv.loads } - in - mp, senv, lib.comp_natsymbs -type judgment = unsafe_judgment -let j_val j = j.uj_val -let j_type j = j.uj_type +(** {6 Safe typing } *) + +type judgment = Environ.unsafe_judgment -let safe_infer senv = infer (env_of_senv senv) +let j_val j = j.Environ.uj_val +let j_type j = j.Environ.uj_type + +let safe_infer senv = Typeops.infer (env_of_senv senv) let typing senv = Typeops.typing (env_of_senv senv) + +(** {6 Retroknowledge / native compiler } *) + +(** universal lifting, used for the "get" operations mostly *) +let retroknowledge f senv = + Environ.retroknowledge f (env_of_senv senv) + +let register field value by_clause senv = + (* todo : value closed, by_clause safe, by_clause of the proper type*) + (* spiwack : updates the safe_env with the information that the register + action has to be performed (again) when the environement is imported *) + { senv with + env = Environ.register senv.env field value; + local_retroknowledge = + Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge + } + +(* spiwack : currently unused *) +let unregister field senv = + (*spiwack: todo: do things properly or delete *) + { senv with env = Environ.unregister senv.env field} +(* /spiwack *) + (* This function serves only for inlining constants in native compiler for now, but it is meant to become a replacement for environ.register *) let register_inline kn senv = + let open Environ in + let open Pre_env in if not (evaluable_constant kn senv.env) then Errors.error "Register inline: an evaluable constant is expected"; let env = pre_env senv.env in - let (cb,r) = Cmap_env.find kn env.Pre_env.env_globals.Pre_env.env_constants in - let cb = {cb with const_inline_code = true} in - let new_constants = - Cmap_env.add kn (cb,r) env.Pre_env.env_globals.Pre_env.env_constants - in - let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in - let env = { env with Pre_env.env_globals = new_globals } in + let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in + let cb = {cb with const_inline_code = true} in + let new_constants = Cmap_env.add kn (cb,r) env.env_globals.env_constants in + let new_globals = { env.env_globals with env_constants = new_constants } in + let env = { env with env_globals = new_globals } in { senv with env = env_of_pre_env env } let add_constraints c = add_constraints (Now c) + +(* NB: The next old comment probably refers to [propagate_loads] above. + When a Require is done inside a module, we'll redo this require + at the upper level after the module is ended, and so on. + This is probably not a big deal anyway, since these Require's + inside modules should be pretty rare. Maybe someday we could + brutally forbid this tricky "feature"... *) + +(* we have an inefficiency: Since loaded files are added to the +environment every time a module is closed, their components are +calculated many times. This could be avoided in several ways: + +1 - for each file create a dummy environment containing only this +file's components, merge this environment with the global +environment, and store for the future (instead of just its type) + +2 - create "persistent modules" environment table in Environ add put +loaded by side-effect once and for all (like it is done in OCaml). +Would this be correct with respect to undo's and stuff ? +*) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index e9716930b..3d67f6c07 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -7,29 +7,35 @@ (************************************************************************) open Names -open Term -open Declarations -open Entries -open Mod_subst (** {6 Safe environments } *) -(** Since we are now able to type terms, we can - define an abstract type of safe environments, where objects are - typed before being added. +(** Since we are now able to type terms, we can define an abstract type + of safe environments, where objects are typed before being added. - We also add [open_structure] and [close_section], [close_module] to - provide functionnality for sections and interactive modules + We also provide functionality for modules : [start_module], [end_module], + etc. *) type safe_environment +val empty_environment : safe_environment + +val is_initial : safe_environment -> bool + val env_of_safe_env : safe_environment -> Environ.env -val sideff_of_con : safe_environment -> constant -> side_effect +(** The safe_environment state monad *) + +type safe_transformer0 = safe_environment -> safe_environment +type 'a safe_transformer = safe_environment -> 'a * safe_environment -val is_curmod_library : safe_environment -> bool +(** {6 Stm machinery } *) + +val sideff_of_con : safe_environment -> constant -> Declarations.side_effect + +val is_curmod_library : safe_environment -> bool (* safe_environment has functional data affected by lazy computations, * thus this function returns a new safe_environment *) @@ -37,117 +43,112 @@ val join_safe_environment : safe_environment -> safe_environment (* future computations are just dropped by this function *) val prune_safe_environment : safe_environment -> safe_environment -val empty_environment : safe_environment -val is_empty : safe_environment -> bool +(** {6 Enriching a safe environment } *) + +(** Insertion of local declarations (Local or Variables) *) -(** Adding and removing local declarations (Local or Variables) *) val push_named_assum : - Id.t * types -> safe_environment -> - Univ.constraints * safe_environment + Id.t * Term.types -> Univ.constraints safe_transformer val push_named_def : - Id.t * definition_entry -> safe_environment -> - Univ.constraints * safe_environment + Id.t * Entries.definition_entry -> Univ.constraints safe_transformer + +(** Insertion of global axioms or definitions *) -(** Adding global axioms or definitions *) type global_declaration = - | ConstantEntry of constant_entry + | ConstantEntry of Entries.constant_entry | GlobalRecipe of Cooking.recipe val add_constant : - DirPath.t -> Label.t -> global_declaration -> safe_environment -> - constant * safe_environment + DirPath.t -> Label.t -> global_declaration -> constant safe_transformer (** Adding an inductive type *) + val add_mind : - DirPath.t -> Label.t -> mutual_inductive_entry -> safe_environment -> - mutual_inductive * safe_environment + DirPath.t -> Label.t -> Entries.mutual_inductive_entry -> + mutual_inductive safe_transformer -(** Adding a module *) -val add_module : - Label.t -> module_entry -> inline -> safe_environment - -> module_path * delta_resolver * safe_environment +(** Adding a module or a module type *) -(** Adding a module type *) +val add_module : + Label.t -> Entries.module_entry -> Declarations.inline -> + (module_path * Mod_subst.delta_resolver) safe_transformer val add_modtype : - Label.t -> module_struct_entry -> inline -> safe_environment - -> module_path * safe_environment + Label.t -> Entries.module_struct_entry -> Declarations.inline -> + module_path safe_transformer (** Adding universe constraints *) -val add_constraints : - Univ.constraints -> safe_environment -> safe_environment -(** Settin the strongly constructive or classical logical engagement *) -val set_engagement : engagement -> safe_environment -> safe_environment +val add_constraints : Univ.constraints -> safe_transformer0 + +(** Setting the Set-impredicative engagement *) +val set_engagement : Declarations.engagement -> safe_transformer0 (** {6 Interactive module functions } *) -val start_module : - Label.t -> safe_environment -> module_path * safe_environment +val start_module : Label.t -> module_path safe_transformer -val end_module : - Label.t -> (module_struct_entry * inline) option - -> safe_environment -> module_path * delta_resolver * safe_environment +val start_modtype : Label.t -> module_path safe_transformer val add_module_parameter : - MBId.t -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment + MBId.t -> Entries.module_struct_entry -> Declarations.inline -> + Mod_subst.delta_resolver safe_transformer -val start_modtype : - Label.t -> safe_environment -> module_path * safe_environment +val end_module : + Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> + (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer -val end_modtype : - Label.t -> safe_environment -> module_path * safe_environment +val end_modtype : Label.t -> (module_path * MBId.t list) safe_transformer val add_include : - module_struct_entry -> bool -> inline -> safe_environment -> - delta_resolver * safe_environment + Entries.module_struct_entry -> bool -> Declarations.inline -> + Mod_subst.delta_resolver safe_transformer -val delta_of_senv : safe_environment -> delta_resolver*delta_resolver +(** {6 Libraries : loading and saving compilation units } *) -(** Loading and saving compilation units *) - -(** exporting and importing modules *) type compiled_library type native_library = Nativecode.global list -val start_library : DirPath.t -> safe_environment - -> module_path * safe_environment +val start_library : DirPath.t -> module_path safe_transformer -val export : safe_environment -> DirPath.t - -> module_path * compiled_library * native_library +val export : safe_environment -> DirPath.t -> + module_path * compiled_library * native_library -val import : compiled_library -> Digest.t -> safe_environment - -> module_path * safe_environment * Nativecode.symbol array +val import : compiled_library -> Digest.t -> + (module_path * Nativecode.symbol array) safe_transformer val join_compiled_library : compiled_library -> unit -(** {6 Typing judgments } *) +(** {6 Safe typing judgments } *) type judgment -val j_val : judgment -> constr -val j_type : judgment -> constr +val j_val : judgment -> Term.constr +val j_type : judgment -> Term.constr -(** Safe typing of a term returning a typing judgment and universe - constraints to be added to the environment for the judgment to - hold. It is guaranteed that the constraints are satisfiable +(** The safe typing of a term returns a typing judgment and some universe + constraints (to be added to the environment for the judgment to + hold). It is guaranteed that the constraints are satisfiable. *) -val safe_infer : safe_environment -> constr -> judgment * Univ.constraints +val safe_infer : safe_environment -> Term.constr -> judgment * Univ.constraints -val typing : safe_environment -> constr -> judgment +val typing : safe_environment -> Term.constr -> judgment -(** {7 Query } *) +(** {6 Queries } *) val exists_objlabel : Label.t -> safe_environment -> bool -(*spiwack: safe retroknowledge functionalities *) +val delta_of_senv : + safe_environment -> Mod_subst.delta_resolver * Mod_subst.delta_resolver + +(** {6 Retroknowledge / Native compiler } *) open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a -val register : safe_environment -> field -> Retroknowledge.entry -> constr - -> safe_environment +val register : + field -> Retroknowledge.entry -> Term.constr -> safe_transformer0 -val register_inline : constant -> safe_environment -> safe_environment +val register_inline : constant -> safe_transformer0 diff --git a/library/declaremods.ml b/library/declaremods.ml index 0dfee9787..5c0700606 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -553,17 +553,11 @@ let build_subtypes interp_modast env mp args mtys = in a later [end_module]. *) type current_module_info = { - cur_mp : module_path; (** current started interactive module (if any) *) - cur_args : MBId.t list; (** its arguments *) cur_typ : (module_struct_entry * int option) option; (** type via ":" *) cur_typs : module_type_body list (** types via "<:" *) } -let default_module_info = - { cur_mp = MPfile DirPath.initial; - cur_args = []; - cur_typ = None; - cur_typs = [] } +let default_module_info = { cur_typ = None; cur_typs = [] } let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" @@ -574,8 +568,7 @@ let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" in a later [end_modtype]. *) let openmodtype_info = - Summary.ref ([],[] : MBId.t list * module_type_body list) - ~name:"MODTYPE-INFO" + Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" (** {6 Modules : start, end, declare} *) @@ -595,12 +588,7 @@ let start_module interp_modast export id args res fs = | Check resl -> None, build_subtypes interp_modast env mp arg_entries_r resl in - let mbids = List.rev_map fst arg_entries_r in - openmod_info:= - { cur_mp = mp; - cur_args = mbids; - cur_typ = res_entry_o; - cur_typs = subtyps }; + openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); Lib.add_frozen_state (); mp @@ -611,14 +599,14 @@ let end_module () = let m_info = !openmod_info in (* For sealed modules, we use the substitutive objects of their signatures *) - let sobjs, keep, special = match m_info.cur_typ with - | None -> (m_info.cur_args, Objs substitute), keep, special + let sobjs0, keep, special = match m_info.cur_typ with + | None -> ([], Objs substitute), keep, special | Some (mty, inline) -> - let (mbids,aobjs) = get_module_sobjs false (Global.env()) inline mty - in (m_info.cur_args@mbids,aobjs), [], [] + get_module_sobjs false (Global.env()) inline mty, [], [] in let id = basename (fst oldoname) in - let mp,resolver = Global.end_module fs id m_info.cur_typ in + let mp,mbids,resolver = Global.end_module fs id m_info.cur_typ in + let sobjs = let (ms,objs) = sobjs0 in (mbids@ms,objs) in check_subtypes mp m_info.cur_typs; @@ -631,7 +619,7 @@ let end_module () = in let node = in_module sobjs in (* We add the keep objects, if any, and if this isn't a functor *) - let objects = match keep, m_info.cur_args with + let objects = match keep, mbids with | [], _ | _, _ :: _ -> special@[node] | _ -> special@[node;in_modkeep keep] in @@ -705,8 +693,7 @@ let start_modtype interp_modast id args mtys fs = let arg_entries_r = intern_args interp_modast args in let env = Global.env () in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in - let mbids = List.rev_map fst arg_entries_r in - openmodtype_info := mbids, sub_mty_l; + openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); Lib.add_frozen_state (); mp @@ -715,8 +702,8 @@ let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in let id = basename (fst oldoname) in let substitute, _, special = Lib.classify_segment lib_stack in - let mbids, sub_mty_l = !openmodtype_info in - let mp = Global.end_modtype fs id in + let sub_mty_l = !openmodtype_info in + let mp, mbids = Global.end_modtype fs id in let modtypeobjs = (mbids, Objs substitute) in check_subtypes_mt mp sub_mty_l; let oname = Lib.add_leaves id (special@[in_modtype modtypeobjs]) @@ -901,7 +888,7 @@ let get_library_symbols_tbl dir = Dirmap.find dir !library_values let start_library dir = let mp = Global.start_library dir in - openmod_info := { default_module_info with cur_mp = mp }; + openmod_info := default_module_info; Lib.start_compilation dir mp; Lib.add_frozen_state () diff --git a/library/global.ml b/library/global.ml index 22b69e4f2..fd6cce46f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -9,20 +9,19 @@ open Names open Term open Environ -open Safe_typing -(* We introduce here the global environment of the system, and we declare it - as a synchronized table. *) +(** We introduce here the global environment of the system, + and we declare it as a synchronized table. *) module GlobalSafeEnv : sig - val safe_env : unit -> safe_environment - val set_safe_env : safe_environment -> unit + val safe_env : unit -> Safe_typing.safe_environment + val set_safe_env : Safe_typing.safe_environment -> unit val join_safe_environment : unit -> unit end = struct -let global_env = ref empty_environment +let global_env = ref Safe_typing.empty_environment let join_safe_environment () = global_env := Safe_typing.join_safe_environment !global_env @@ -37,7 +36,7 @@ let () = | `No -> !global_env | `Shallow -> prune_safe_environment !global_env); unfreeze_function = (fun fr -> global_env := fr); - init_function = (fun () -> global_env := empty_environment) } + init_function = (fun () -> global_env := Safe_typing.empty_environment) } let assert_not_parsing () = if !Flags.we_are_parsing then @@ -50,89 +49,57 @@ let set_safe_env e = global_env := e end -open GlobalSafeEnv -let safe_env = safe_env -let join_safe_environment = join_safe_environment +let safe_env = GlobalSafeEnv.safe_env +let join_safe_environment = GlobalSafeEnv.join_safe_environment -let env () = env_of_safe_env (safe_env ()) +let env () = Safe_typing.env_of_safe_env (safe_env ()) -let env_is_empty () = is_empty (safe_env ()) +let env_is_initial () = Safe_typing.is_initial (safe_env ()) -(* Then we export the functions of [Typing] on that environment. *) - -let universes () = universes (env()) -let named_context () = named_context (env()) -let named_context_val () = named_context_val (env()) - -let push_named_assum a = - let (cst,env) = push_named_assum a (safe_env ()) in - set_safe_env env; - cst -let push_named_def d = - let (cst,env) = push_named_def d (safe_env ()) in - set_safe_env env; - cst +(** Turn ops over the safe_environment state monad to ops on the global env *) +let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) -let add_thing add dir id thing = - let kn, newenv = add dir (Label.of_id id) thing (safe_env ()) in - set_safe_env newenv; - kn +let globalize f = + let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res -let add_constant = add_thing add_constant -let add_mind = add_thing add_mind -let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y +let globalize_with_summary fs f = + let res,env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env; + res +(** [Safe_typing] operations, now operating on the global environment *) -let add_module id me inl = - let l = Label.of_id id in - let mp,resolve,new_env = add_module l me inl (safe_env ()) in - set_safe_env new_env; - mp,resolve - +let i2l = Label.of_id -let add_constraints c = set_safe_env (add_constraints c (safe_env ())) +let push_named_assum a = globalize (Safe_typing.push_named_assum a) +let push_named_def d = globalize (Safe_typing.push_named_def d) +let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) +let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) +let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) +let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) +let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) -let set_engagement c = set_safe_env (set_engagement c (safe_env ())) - -let add_include me is_module inl = - let resolve,newenv = add_include me is_module inl (safe_env ()) in - set_safe_env newenv; - resolve - -let start_module id = - let l = Label.of_id id in - let mp,newenv = start_module l (safe_env ()) in - set_safe_env newenv; - mp +let start_module id = globalize (Safe_typing.start_module (i2l id)) +let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) let end_module fs id mtyo = - let l = Label.of_id id in - let mp,resolve,newenv = end_module l mtyo (safe_env ()) in - Summary.unfreeze_summaries fs; - set_safe_env newenv; - mp,resolve + globalize_with_summary fs (Safe_typing.end_module (i2l id) mtyo) +let end_modtype fs id = + globalize_with_summary fs (Safe_typing.end_modtype (i2l id)) let add_module_parameter mbid mte inl = - let resolve,newenv = add_module_parameter mbid mte inl (safe_env ()) in - set_safe_env newenv; - resolve + globalize (Safe_typing.add_module_parameter mbid mte inl) +(** Queries on the global environment *) -let start_modtype id = - let l = Label.of_id id in - let mp,newenv = start_modtype l (safe_env ()) in - set_safe_env newenv; - mp - -let end_modtype fs id = - let l = Label.of_id id in - let kn,newenv = end_modtype l (safe_env ()) in - Summary.unfreeze_summaries fs; - set_safe_env newenv; - kn - +let universes () = universes (env()) +let named_context () = named_context (env()) +let named_context_val () = named_context_val (env()) let lookup_named id = lookup_named id (env()) let lookup_constant kn = lookup_constant kn (env()) @@ -142,35 +109,32 @@ let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) let lookup_modtype kn = lookup_modtype kn (env()) +let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) + +(** Operations on kernel names *) + let constant_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv (safe_env ())) in + let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ()) + in (* TODO : are resolver and resolver_param orthogonal ? the effect of resolver is lost if resolver_param isn't trivial at that spot. *) Mod_subst.constant_of_deltas_kn resolver_param resolver kn let mind_of_delta_kn kn = - let resolver,resolver_param = (delta_of_senv (safe_env ())) in + let resolver,resolver_param = Safe_typing.delta_of_senv (safe_env ()) + in (* TODO idem *) Mod_subst.mind_of_deltas_kn resolver_param resolver kn -let exists_objlabel id = exists_objlabel id (safe_env ()) - -let start_library dir = - let mp,newenv = start_library dir (safe_env ()) in - set_safe_env newenv; - mp - -let export s = export (safe_env ()) s - -let import cenv digest = - let mp,newenv,values = import cenv digest (safe_env ()) in - set_safe_env newenv; - mp, values +(** Operations on libraries *) +let start_library dir = globalize (Safe_typing.start_library dir) +let export s = Safe_typing.export (safe_env ()) s +let import cenv digest = globalize (Safe_typing.import cenv digest) -(*s Function to get an environment from the constants part of the global +(** Function to get an environment from the constants part of the global environment and a given context. *) let env_of_context hyps = @@ -194,9 +158,6 @@ let type_of_global t = type_of_reference (env ()) t (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = - let entry = kind_of_term value in - let senv = Safe_typing.register (safe_env ()) field entry by_clause in - set_safe_env senv + globalize0 (Safe_typing.register field (kind_of_term value) by_clause) -let register_inline c = - set_safe_env (Safe_typing.register_inline c (safe_env ())) +let register_inline c = globalize0 (Safe_typing.register_inline c) diff --git a/library/global.mli b/library/global.mli index a5ca92013..1bc745bb7 100644 --- a/library/global.mli +++ b/library/global.mli @@ -7,104 +7,101 @@ (************************************************************************) open Names -open Univ -open Term -open Context -open Declarations -open Entries -open Indtypes -open Mod_subst -open Safe_typing - -(** This module defines the global environment of Coq. The functions + +(** This module defines the global environment of Coq. The functions below are exactly the same as the ones in [Safe_typing], operating on that global environment. [add_*] functions perform name verification, i.e. check that the name given as argument match those provided by [Safe_typing]. *) - - -val safe_env : unit -> safe_environment +val safe_env : unit -> Safe_typing.safe_environment val env : unit -> Environ.env -val env_is_empty : unit -> bool +val env_is_initial : unit -> bool -val universes : unit -> universes +val universes : unit -> Univ.universes val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Context.named_context -val env_is_empty : unit -> bool +(** {6 Enriching the global environment } *) -(** {6 Extending env with variables and local definitions } *) -val push_named_assum : (Id.t * types) -> Univ.constraints -val push_named_def : (Id.t * definition_entry) -> Univ.constraints +(** Changing the (im)predicativity of the system *) +val set_engagement : Declarations.engagement -> unit -(** {6 ... } *) -(** Adding constants, inductives, modules and module types. All these - functions verify that given names match those generated by kernel *) +(** Extra universe constraints *) +val add_constraints : Univ.constraints -> unit -val add_constant : - DirPath.t -> Id.t -> global_declaration -> constant -val add_mind : - DirPath.t -> Id.t -> mutual_inductive_entry -> mutual_inductive - -val add_module : - Id.t -> module_entry -> inline -> module_path * delta_resolver -val add_modtype : - Id.t -> module_struct_entry -> inline -> module_path -val add_include : - module_struct_entry -> bool -> inline -> delta_resolver +(** Variables, Local definitions, constants, inductive types *) -val add_constraints : constraints -> unit +val push_named_assum : (Id.t * Term.types) -> Univ.constraints +val push_named_def : (Id.t * Entries.definition_entry) -> Univ.constraints +val add_constant : + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant +val add_mind : + DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive -val set_engagement : engagement -> unit +(** Non-interactive modules and module types *) -(** {6 Interactive modules and module types } - Both [start_*] functions take the [DirPath.t] argument to create a - [mod_self_id]. This should be the name of the compilation unit. *) +val add_module : + Id.t -> Entries.module_entry -> Declarations.inline -> + module_path * Mod_subst.delta_resolver +val add_modtype : + Id.t -> Entries.module_struct_entry -> Declarations.inline -> module_path +val add_include : + Entries.module_struct_entry -> bool -> Declarations.inline -> + Mod_subst.delta_resolver -(** [start_*] functions return the [module_path] valid for components - of the started module / module type *) +(** Interactive modules and module types *) val start_module : Id.t -> module_path +val start_modtype : Id.t -> module_path -val end_module : Summary.frozen ->Id.t -> - (module_struct_entry * inline) option -> module_path * delta_resolver - -val add_module_parameter : - MBId.t -> module_struct_entry -> inline -> delta_resolver +val end_module : Summary.frozen -> Id.t -> + (Entries.module_struct_entry * Declarations.inline) option -> + module_path * MBId.t list * Mod_subst.delta_resolver -val start_modtype : Id.t -> module_path -val end_modtype : Summary.frozen -> Id.t -> module_path +val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list +val add_module_parameter : + MBId.t -> Entries.module_struct_entry -> Declarations.inline -> + Mod_subst.delta_resolver + +(** {6 Queries in the global environment } *) + +val lookup_named : variable -> Context.named_declaration +val lookup_constant : constant -> Declarations.constant_body +val lookup_inductive : inductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body +val lookup_module : module_path -> Declarations.module_body +val lookup_modtype : module_path -> Declarations.module_type_body +val exists_objlabel : Label.t -> bool -(** Queries *) -val lookup_named : variable -> named_declaration -val lookup_constant : constant -> constant_body -val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body -val lookup_mind : mutual_inductive -> mutual_inductive_body -val lookup_module : module_path -> module_body -val lookup_modtype : module_path -> module_type_body val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive -val exists_objlabel : Label.t -> bool -(** Compiled modules *) +(** {6 Compiled libraries } *) + val start_library : DirPath.t -> module_path -val export : DirPath.t -> module_path * compiled_library * native_library -val import : compiled_library -> Digest.t -> +val export : DirPath.t -> + module_path * Safe_typing.compiled_library * Safe_typing.native_library +val import : Safe_typing.compiled_library -> Digest.t -> module_path * Nativecode.symbol array -(** {6 ... } *) +(** {6 Misc } *) + (** Function to get an environment from the constants part of the global * environment and a given context. *) -val type_of_global : Globnames.global_reference -> types +val type_of_global : Globnames.global_reference -> Term.types val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : unit -> unit -(** spiwack: register/unregister function for retroknowledge *) -val register : Retroknowledge.field -> constr -> constr -> unit + +(** {6 Retroknowledge } *) + +val register : + Retroknowledge.field -> Term.constr -> Term.constr -> unit val register_inline : constant -> unit diff --git a/library/lib.ml b/library/lib.ml index 379d0e8ad..159ac2d6d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -220,7 +220,7 @@ let add_anonymous_entry node = let add_leaf id obj = let (path, _) = current_prefix () in - if Names.mp_eq path Names.initial_path then + if Names.ModPath.equal path Names.initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -296,7 +296,7 @@ let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedModule (ty,_,_,fs) -> - if Pervasives.(=) ty is_type then oname, fs + if ty == is_type then oname, fs else error_still_opened (module_kind ty) oname | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 26e3081bb..c0b47f0c1 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -395,8 +395,9 @@ let init arglist = (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; Syntax_def.set_compat_notations (not !no_compat_ntn); - if (not !batch_mode|| List.is_empty !compile_list) && Global.env_is_empty() then - Option.iter Declaremods.start_library !toplevel_name; + if (not !batch_mode || List.is_empty !compile_list) + && Global.env_is_initial () + then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 756df0053..9a2d03891 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -683,12 +683,6 @@ let explain_incompatible_labels l l' = let explain_signature_expected mtb = str "Signature expected." -let explain_no_module_to_end () = - str "No open module to end." - -let explain_no_module_type_to_end () = - str "No open module type to end." - let explain_not_a_module s = quote (str s) ++ str " is not a module." @@ -706,16 +700,13 @@ let explain_generative_module_expected l = str "The module " ++ str (Label.to_string l) ++ strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct." -let explain_non_empty_local_context = function - | None -> str "The local context is not empty." - | Some l -> - str "The local context of the component " ++ - str (Label.to_string l) ++ str " is not empty." - let explain_label_missing l s = str "The field " ++ str (Label.to_string l) ++ str " is missing in " ++ str s ++ str "." +let explain_higher_order_include () = + str "You cannot Include a higher-order structure." + let explain_module_error = function | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l @@ -726,15 +717,13 @@ let explain_module_error = function | NoSuchLabel l -> explain_no_such_label l | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 | SignatureExpected mtb -> explain_signature_expected mtb - | NoModuleToEnd -> explain_no_module_to_end () - | NoModuleTypeToEnd -> explain_no_module_type_to_end () | NotAModule s -> explain_not_a_module s | NotAModuleType s -> explain_not_a_module_type s | NotAConstant l -> explain_not_a_constant l | IncorrectWithConstraint l -> explain_incorrect_label_constraint l | GenerativeModuleExpected l -> explain_generative_module_expected l - | NonEmptyLocalContect lopt -> explain_non_empty_local_context lopt | LabelMissing (l,s) -> explain_label_missing l s + | HigherOrderInclude -> explain_higher_order_include () (* Module internalization errors *) |