diff options
Diffstat (limited to 'library')
| -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 |
4 files changed, 129 insertions, 184 deletions
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 |