diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 18 | ||||
| -rw-r--r-- | library/coqlib.mli | 4 | ||||
| -rw-r--r-- | library/decl_kinds.ml | 11 | ||||
| -rw-r--r-- | library/declaremods.ml | 1024 | ||||
| -rw-r--r-- | library/declaremods.mli | 142 | ||||
| -rw-r--r-- | library/global.ml | 28 | ||||
| -rw-r--r-- | library/global.mli | 29 | ||||
| -rw-r--r-- | library/globnames.mli | 4 | ||||
| -rw-r--r-- | library/goptions.ml | 36 | ||||
| -rw-r--r-- | library/keys.ml | 162 | ||||
| -rw-r--r-- | library/keys.mli | 23 | ||||
| -rw-r--r-- | library/lib.ml | 224 | ||||
| -rw-r--r-- | library/lib.mli | 32 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libobject.ml | 14 | ||||
| -rw-r--r-- | library/libobject.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 642 | ||||
| -rw-r--r-- | library/library.mli | 77 | ||||
| -rw-r--r-- | library/library.mllib | 4 | ||||
| -rw-r--r-- | library/nametab.ml | 86 | ||||
| -rw-r--r-- | library/nametab.mli | 3 | ||||
| -rw-r--r-- | library/states.ml | 8 | ||||
| -rw-r--r-- | library/states.mli | 3 |
23 files changed, 179 insertions, 2399 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index b1e4ef2b00..00ea8b8489 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -89,23 +89,25 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str "cannot find " ++ str s ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".") | l -> anomaly ~label:locstr - (str "ambiguous name " ++ str s ++ str " can represent " ++ - prlist_with_sep pr_comma - (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ + prlist_with_sep pr_comma + (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma DirPath.print dirs ++ str ".") (* For tactics/commands requiring vernacular libraries *) let check_required_library d = let dir = make_dir d in - if Library.library_is_loaded dir then () - else + try + let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in + () + with Not_found -> let in_current_dir = match Lib.current_mp () with | MPfile dp -> DirPath.equal dir dp | _ -> false diff --git a/library/coqlib.mli b/library/coqlib.mli index ab8b18c4fb..10805416d1 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -210,9 +210,9 @@ val build_coq_f_equal2 : GlobRef.t delayed type coq_inversion_data = { inv_eq : GlobRef.t; (** : forall params, args -> Prop *) inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args - -> P args *) + -> P args *) inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> - f params = f args *) + f params = f args *) } val build_coq_inversion_eq_data : coq_inversion_data delayed diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 17746645ee..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type binding_kind = Explicit | Implicit diff --git a/library/declaremods.ml b/library/declaremods.ml deleted file mode 100644 index eea129eae7..0000000000 --- a/library/declaremods.ml +++ /dev/null @@ -1,1024 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util -open Names -open Declarations -open Entries -open Libnames -open Libobject -open Mod_subst - -(** {6 Inlining levels} *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = - | NoInline - | DefaultInline - | InlineAt of int - -type module_kind = Module | ModType | ModAny - -let default_inline () = Some (Flags.get_inline_level ()) - -let inl2intopt = function - | NoInline -> None - | InlineAt i -> Some i - | DefaultInline -> default_inline () - -(** ModSubstObjs : a cache of module substitutive objects - - This table is common to modules and module types. - - For a Module M:=N, the objects of N will be reloaded - with M after substitution. - - For a Module M:SIG:=..., the module M gets its objects from SIG - - Invariants: - - A alias (i.e. a module path inside a Ref constructor) should - never lead to another alias, but rather to a concrete Objs - constructor. - - We will plug later a handler dealing with missing entries in the - cache. Such missing entries may come from inner parts of module - types, which aren't registered by the standard libobject machinery. -*) - -module ModSubstObjs : - sig - val set : ModPath.t -> substitutive_objects -> unit - val get : ModPath.t -> substitutive_objects - val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit - end = - struct - let table = - Summary.ref (MPmap.empty : substitutive_objects MPmap.t) - ~name:"MODULE-SUBSTOBJS" - let missing_handler = ref (fun mp -> assert false) - let set_missing_handler f = (missing_handler := f) - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = - try MPmap.find mp !table with Not_found -> !missing_handler mp - end - -(** Some utilities about substitutive objects : - substitution, expansion *) - -let sobjs_no_functor (mbids,_) = List.is_empty mbids - -let rec subst_aobjs sub = function - | Objs o as objs -> - let o' = subst_objects sub o in - if o == o' then objs else Objs o' - | Ref (mp, sub0) as r -> - let sub0' = join sub0 sub in - if sub0' == sub0 then r else Ref (mp, sub0') - -and subst_sobjs sub (mbids,aobjs as sobjs) = - let aobjs' = subst_aobjs sub aobjs in - if aobjs' == aobjs then sobjs else (mbids, aobjs') - -and subst_objects subst seg = - let subst_one (id,obj as node) = - match obj with - | AtomicObject obj -> - let obj' = Libobject.subst_object (subst,obj) in - if obj' == obj then node else (id, AtomicObject obj') - | ModuleObject sobjs -> - let sobjs' = subst_sobjs subst sobjs in - if sobjs' == sobjs then node else (id, ModuleObject sobjs') - | ModuleTypeObject sobjs -> - let sobjs' = subst_sobjs subst sobjs in - if sobjs' == sobjs then node else (id, ModuleTypeObject sobjs') - | IncludeObject aobjs -> - let aobjs' = subst_aobjs subst aobjs in - if aobjs' == aobjs then node else (id, IncludeObject aobjs') - | ImportObject { export; mp } -> - let mp' = subst_mp subst mp in - if mp'==mp then node else (id, ImportObject { export; mp = mp' }) - | KeepObject _ -> assert false - in - List.Smart.map subst_one seg - -let expand_aobjs = function - | Objs o -> o - | Ref (mp, sub) -> - match ModSubstObjs.get mp with - | (_,Objs o) -> subst_objects sub o - | _ -> assert false (* Invariant : any alias points to concrete objs *) - -let expand_sobjs (_,aobjs) = expand_aobjs aobjs - - -(** {6 ModObjs : a cache of module objects} - - For each module, we also store a cache of - "prefix", "substituted objects", "keep objects". - This is used for instance to implement the "Import" command. - - substituted objects : - roughly the objects above after the substitution - we need to - keep them to call open_object when the module is opened (imported) - - keep objects : - The list of non-substitutive objects - as above, for each of - them we will call open_object when the module is opened - - (Some) Invariants: - * If the module is a functor, it won't appear in this cache. - - * Module objects in substitutive_objects part have empty substituted - objects. - - * Modules which where created with Module M:=mexpr or with - Module M:SIG. ... End M. have the keep list empty. -*) - -type module_objects = Nametab.object_prefix * Lib.lib_objects * Lib.lib_objects - -module ModObjs : - sig - val set : ModPath.t -> module_objects -> unit - val get : ModPath.t -> module_objects (* may raise Not_found *) - val all : unit -> module_objects MPmap.t - end = - struct - let table = - Summary.ref (MPmap.empty : module_objects MPmap.t) - ~name:"MODULE-OBJS" - let set mp objs = (table := MPmap.add mp objs !table) - let get mp = MPmap.find mp !table - let all () = !table - end - - -(** {6 Name management} - - Auxiliary functions to transform full_path and kernel_name given - by Lib into ModPath.t and DirPath.t needed for modules -*) - -let mp_of_kn kn = - let mp,l = KerName.repr kn in - MPdot (mp,l) - -let dir_of_sp sp = - let dir,id = repr_path sp in - add_dirpath_suffix dir id - - -(** {6 Declaration of module substitutive objects} *) - -(** These functions register the visibility of the module and iterates - through its components. They are called by plenty of module functions *) - -let consistency_checks exists dir dirinfo = - if exists then - let globref = - try Nametab.locate_dir (qualid_of_dirpath dir) - with Not_found -> - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " should already exist!") - in - assert (Nametab.GlobDirRef.equal globref dirinfo) - else - if Nametab.exists_dir dir then - user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " already exists") - -let compute_visibility exists i = - if exists then Nametab.Exactly i else Nametab.Until i - -(** Iterate some function [iter_objects] on all components of a module *) - -let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let dirinfo = Nametab.GlobDirRef.DirModule prefix in - consistency_checks exists obj_dir dirinfo; - Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; - ModSubstObjs.set obj_mp sobjs; - (* If we're not a functor, let's iter on the internal components *) - if sobjs_no_functor sobjs then begin - let objs = expand_sobjs sobjs in - ModObjs.set obj_mp (prefix,objs,kobjs); - iter_objects (i+1) prefix objs; - iter_objects (i+1) prefix kobjs - end - -let do_module' exists iter_objects i ((sp,kn),sobjs) = - do_module exists iter_objects i (dir_of_sp sp) (mp_of_kn kn) sobjs [] - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked here via a flag along the substobjs. *) - -(** {6 Declaration of module type substitutive objects} *) - -(** Nota: Interactive modules and module types cannot be recached! - This used to be checked more properly here. *) - -let do_modtype i sp mp sobjs = - if Nametab.exists_modtype sp then - anomaly (pr_path sp ++ str " already exists."); - Nametab.push_modtype (Nametab.Until i) sp mp; - ModSubstObjs.set mp sobjs - -(** {6 Declaration of substitutive objects for Include} *) - -let rec load_object i (name, obj) = - match obj with - | AtomicObject o -> Libobject.load_object i (name, o) - | ModuleObject sobjs -> do_module' false load_objects i (name, sobjs) - | ModuleTypeObject sobjs -> - let (sp,kn) = name in - do_modtype i sp (mp_of_kn kn) sobjs - | IncludeObject aobjs -> load_include i (name, aobjs) - | ImportObject _ -> () - | KeepObject objs -> load_keep i (name, objs) - -and load_objects i prefix objs = - List.iter (fun (id, obj) -> load_object i (Lib.make_oname prefix id, obj)) objs - -and load_include i ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - load_objects i prefix o - -and load_keep i ((sp,kn),kobjs) = - (* Invariant : seg isn't empty *) - let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in - let prefix',sobjs,kobjs0 = - try ModObjs.get obj_mp - with Not_found -> assert false (* a substobjs should already be loaded *) - in - assert Nametab.(eq_op prefix' prefix); - assert (List.is_empty kobjs0); - ModObjs.set obj_mp (prefix,sobjs,kobjs); - load_objects i prefix kobjs - -(** {6 Implementation of Import and Export commands} *) - -let rec really_import_module mp = - (* May raise Not_found for unknown module and for functors *) - let prefix,sobjs,keepobjs = ModObjs.get mp in - open_objects 1 prefix sobjs; - open_objects 1 prefix keepobjs - -and open_object i (name, obj) = - match obj with - | AtomicObject o -> Libobject.open_object i (name, o) - | ModuleObject sobjs -> do_module' true open_objects i (name, sobjs) - | ModuleTypeObject sobjs -> open_modtype i (name, sobjs) - | IncludeObject aobjs -> open_include i (name, aobjs) - | ImportObject { mp; _ } -> open_import i mp - | KeepObject objs -> open_keep i (name, objs) - -and open_objects i prefix objs = - List.iter (fun (id, obj) -> open_object i (Lib.make_oname prefix id, obj)) objs - -and open_modtype i ((sp,kn),_) = - let mp = mp_of_kn kn in - let mp' = - try Nametab.locate_modtype (qualid_of_path sp) - with Not_found -> - anomaly (pr_path sp ++ str " should already exist!"); - in - assert (ModPath.equal mp mp'); - Nametab.push_modtype (Nametab.Exactly i) sp mp - -and open_include i ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - open_objects i prefix o - -and open_import i mp = - if Int.equal i 1 then really_import_module mp - -and open_keep i ((sp,kn),kobjs) = - let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - open_objects i prefix kobjs - -let rec cache_object (name, obj) = - match obj with - | AtomicObject o -> Libobject.cache_object (name, o) - | ModuleObject sobjs -> do_module' false load_objects 1 (name, sobjs) - | ModuleTypeObject sobjs -> - let (sp,kn) = name in - do_modtype 1 sp (mp_of_kn kn) sobjs - | IncludeObject aobjs -> cache_include (name, aobjs) - | ImportObject { mp } -> really_import_module mp - | KeepObject objs -> cache_keep (name, objs) - -and cache_include ((sp,kn), aobjs) = - let obj_dir = Libnames.dirpath sp in - let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in - let o = expand_aobjs aobjs in - load_objects 1 prefix o; - open_objects 1 prefix o - -and cache_keep ((sp,kn),kobjs) = - anomaly (Pp.str "This module should not be cached!") - -(* Adding operations with containers *) - -let add_leaf id obj = - if ModPath.equal (Lib.current_mp ()) ModPath.initial then - user_err Pp.(str "No session module started (use -top dir)"); - let oname = Lib.make_foname id in - cache_object (oname,obj); - Lib.add_entry oname (Lib.Leaf obj); - oname - -let add_leaves id objs = - let oname = Lib.make_foname id in - let add_obj obj = - Lib.add_entry oname (Lib.Leaf obj); - load_object 1 (oname,obj) - in - List.iter add_obj objs; - oname - -(** {6 Handler for missing entries in ModSubstObjs} *) - -(** Since the inner of Module Types are not added by default to - the ModSubstObjs table, we compensate this by explicit traversal - of Module Types inner objects when needed. Quite a hack... *) - -let mp_id mp id = MPdot (mp, Label.of_id id) - -let rec register_mod_objs mp (id,obj) = match obj with - | ModuleObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs - | ModuleTypeObject sobjs -> ModSubstObjs.set (mp_id mp id) sobjs - | IncludeObject aobjs -> - List.iter (register_mod_objs mp) (expand_aobjs aobjs) - | _ -> () - -let handle_missing_substobjs mp = match mp with - | MPdot (mp',l) -> - let objs = expand_sobjs (ModSubstObjs.get mp') in - List.iter (register_mod_objs mp') objs; - ModSubstObjs.get mp - | _ -> - assert false (* Only inner parts of module types should be missing *) - -let () = ModSubstObjs.set_missing_handler handle_missing_substobjs - - - -(** {6 From module expression to substitutive objects} *) - -(** Turn a chain of [MSEapply] into the head ModPath.t and the - list of ModPath.t parameters (deepest param coming first). - The left part of a [MSEapply] must be either [MSEident] or - another [MSEapply]. *) - -let get_applications mexpr = - let rec get params = function - | MEident mp -> mp, params - | MEapply (fexpr, mp) -> get (mp::params) fexpr - | MEwith _ -> user_err Pp.(str "Non-atomic functor application.") - in get [] mexpr - -(** Create the substitution corresponding to some functor applications *) - -let rec compute_subst env mbids sign mp_l inl = - match mbids,mp_l with - | _,[] -> mbids,empty_subst - | [],r -> user_err Pp.(str "Application of a functor with too few arguments.") - | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let mb = Environ.lookup_module mp env in - let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = - if Modops.is_functor mb.mod_type then empty_delta_resolver - else - Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - in - mbid_left,join (map_mbid mbid mp resolver) subst - -(** Create the objects of a "with Module" structure. *) - -let rec replace_module_object idl mp0 objs0 mp1 objs1 = - match idl, objs0 with - | _,[] -> [] - | id::idl,(id',obj)::tail when Id.equal id id' -> - begin match obj with - | ModuleObject sobjs -> - let mp_id = MPdot(mp0, Label.of_id id) in - let objs = match idl with - | [] -> subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 - | _ -> - let objs_id = expand_sobjs sobjs in - replace_module_object idl mp_id objs_id mp1 objs1 - in - (id, ModuleObject ([], Objs objs))::tail - | _ -> assert false - end - | idl,lobj::tail -> lobj::replace_module_object idl mp0 tail mp1 objs1 - -let type_of_mod mp env = function - |true -> (Environ.lookup_module mp env).mod_type - |false -> (Environ.lookup_modtype mp env).mod_type - -let rec get_module_path = function - |MEident mp -> mp - |MEwith (me,_) -> get_module_path me - |MEapply (me,_) -> get_module_path me - -(** Substitutive objects of a module expression (or module type) *) - -let rec get_module_sobjs is_mod env inl = function - |MEident mp -> - begin match ModSubstObjs.get mp with - |(mbids,Objs _) when not (ModPath.is_bound mp) -> - (mbids,Ref (mp, empty_subst)) (* we create an alias *) - |sobjs -> sobjs - end - |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty - |MEwith (mty, WithMod (idl,mp1)) -> - assert (not is_mod); - let sobjs0 = get_module_sobjs is_mod env inl mty in - assert (sobjs_no_functor sobjs0); - (* For now, we expanse everything, to be safe *) - let mp0 = get_module_path mty in - let objs0 = expand_sobjs sobjs0 in - let objs1 = expand_sobjs (ModSubstObjs.get mp1) in - ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) - |MEapply _ as me -> - let mp1, mp_l = get_applications me in - let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in - let typ = type_of_mod mp1 env is_mod in - let mbids_left,subst = compute_subst env mbids typ mp_l inl in - (mbids_left, subst_aobjs subst aobjs) - -let get_functor_sobjs is_mod env inl (params,mexpr) = - let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in - (List.map fst params @ mbids, aobjs) - - -(** {6 Handling of module parameters} *) - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. *) - -let process_module_binding mbid me = - let dir = DirPath.make [MBId.to_id mbid] in - let mp = MPbound mbid in - let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in - let subst = map_mp (get_module_path me) mp empty_delta_resolver in - let sobjs = subst_sobjs subst sobjs in - do_module false load_objects 1 dir mp sobjs [] - -(** Process a declaration of functor parameter(s) (Id1 .. Idn : Typ) - i.e. possibly multiple names with the same module type. - Global environment is updated on the fly. - Objects in these parameters are also loaded. - Output is accumulated on top of [acc] (in reverse order). *) - -let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = - let inl = inl2intopt ann in - let lib_dir = Lib.library_dp() in - let env = Global.env() in - let (mty, _, cst') = interp_modast env ModType typ in - let () = Global.push_context_set true cst' in - let env = Global.env () in - let sobjs = get_module_sobjs false env inl mty in - let mp0 = get_module_path mty in - let fold acc {CAst.v=id} = - let dir = DirPath.make [id] in - let mbid = MBId.make lib_dir id in - let mp = MPbound mbid in - let resolver = Global.add_module_parameter mbid mty inl in - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - do_module false load_objects 1 dir mp sobjs []; - (mbid,mty,inl)::acc - in - let acc = List.fold_left fold acc idl in - (acc, Univ.ContextSet.union cst cst') - -(** Process a list of declarations of functor parameters - (Id11 .. Id1n : Typ1)..(Idk1 .. Idkm : Typk) - Global environment is updated on the fly. - The calls to [interp_modast] should be interleaved with these - env updates, otherwise some "with Definition" could be rejected. - Returns a list of mbids and entries (in reversed order). - - This used to be a [List.concat (List.map ...)], but this should - be more efficient and independent of [List.map] eval order. -*) - -let intern_args interp_modast params = - List.fold_left (intern_arg interp_modast) ([], Univ.ContextSet.empty) params - - -(** {6 Auxiliary functions concerning subtyping checks} *) - -let check_sub mtb sub_mtb_l = - (* The constraints are checked and forgot immediately : *) - ignore (List.fold_right - (fun sub_mtb env -> - Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) env) - sub_mtb_l (Global.env())) - -(** This function checks if the type calculated for the module [mp] is - a subtype of all signatures in [sub_mtb_l]. Uses only the global - environment. *) - -let check_subtypes mp sub_mtb_l = - let mb = - try Global.lookup_module mp with Not_found -> assert false - in - let mtb = Modops.module_type_of_module mb in - check_sub mtb sub_mtb_l - -(** Same for module type [mp] *) - -let check_subtypes_mt mp sub_mtb_l = - let mtb = - try Global.lookup_modtype mp with Not_found -> assert false - in - check_sub mtb sub_mtb_l - -(** Create a params entry. - In [args], the youngest module param now comes first. *) - -let mk_params_entry args = - List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args - -(** Create a functor type struct. - In [args], the youngest module param now comes first. *) - -let mk_funct_type env args seb0 = - List.fold_left - (fun seb (arg_id,arg_t,arg_inl) -> - let mp = MPbound arg_id in - let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in - MoreFunctor(arg_id,arg_t,seb)) - seb0 args - -(** Prepare the module type list for check of subtypes *) - -let build_subtypes interp_modast env mp args mtys = - let (cst, ans) = List.fold_left_map - (fun cst (m,ann) -> - let inl = inl2intopt ann in - let mte, _, cst' = interp_modast env ModType m in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in - cst, { mtb with mod_type = mk_funct_type env args mtb.mod_type }) - Univ.ContextSet.empty mtys - in - (ans, cst) - - -(** {6 Current module information} - - This information is stored by each [start_module] for use - in a later [end_module]. *) - -type current_module_info = { - cur_typ : (module_struct_entry * int option) option; (** type via ":" *) - cur_typs : module_type_body list (** types via "<:" *) -} - -let default_module_info = { cur_typ = None; cur_typs = [] } - -let openmod_info = Summary.ref default_module_info ~name:"MODULE-INFO" - - -(** {6 Current module type information} - - This information is stored by each [start_modtype] for use - in a later [end_modtype]. *) - -let openmodtype_info = - Summary.ref ([] : module_type_body list) ~name:"MODTYPE-INFO" - - -(** {6 Modules : start, end, declare} *) - -module RawModOps = struct - -let start_module interp_modast export id args res fs = - let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let env = Global.env () in - let res_entry_o, subtyps, cst = match res with - | Enforce (res,ann) -> - let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType res in - let env = Environ.push_context_set ~strict:true cst env in - (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some (mte, inl), [], cst - | Check resl -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r resl in - None, typs, cst - in - let () = Global.push_context_set true cst in - openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; - let prefix = Lib.start_module export id mp fs in - Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); - mp - -let end_module () = - let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let substitute, keep, special = Lib.classify_segment lib_stack in - let m_info = !openmod_info in - - (* For sealed modules, we use the substitutive objects of their signatures *) - let sobjs0, keep, special = match m_info.cur_typ with - | None -> ([], Objs substitute), keep, special - | Some (mty, inline) -> - get_module_sobjs false (Global.env()) inline mty, [], [] - in - let id = basename (fst oldoname) 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; - - (* We substitute objects if the module is sealed by a signature *) - let sobjs = - match m_info.cur_typ with - | None -> sobjs - | Some (mty, _) -> - subst_sobjs (map_mp (get_module_path mty) mp resolver) sobjs - in - let node = ModuleObject sobjs in - (* We add the keep objects, if any, and if this isn't a functor *) - let objects = match keep, mbids with - | [], _ | _, _ :: _ -> special@[node] - | _ -> special@[node;KeepObject keep] - in - let newoname = add_leaves id objects in - - (* Name consistency check : start_ vs. end_module, kernel vs. library *) - assert (eq_full_path (fst newoname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd newoname)) mp); - - mp - -let declare_module interp_modast id args res mexpr_o fs = - (* We simulate the beginning of an interactive module, - then we adds the module parameters to the global env. *) - let mp = Global.start_module id in - let arg_entries_r, cst = intern_args interp_modast args in - let params = mk_params_entry arg_entries_r in - let env = Global.env () in - let env = Environ.push_context_set ~strict:true cst env in - let mty_entry_o, subs, inl_res, cst' = match res with - | Enforce (mty,ann) -> - let inl = inl2intopt ann in - let (mte, _, cst) = interp_modast env ModType mty in - let env = Environ.push_context_set ~strict:true cst env in - (* We check immediately that mte is well-formed *) - let _, _, _, cst' = Mod_typing.translate_mse env None inl mte in - let cst = Univ.ContextSet.union cst cst' in - Some mte, [], inl, cst - | Check mtys -> - let typs, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - None, typs, default_inline (), cst - in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let mexpr_entry_o, inl_expr, cst' = match mexpr_o with - | None -> None, default_inline (), Univ.ContextSet.empty - | Some (mexpr,ann) -> - let (mte, _, cst) = interp_modast env Module mexpr in - Some mte, inl2intopt ann, cst - in - let env = Environ.push_context_set ~strict:true cst' env in - let cst = Univ.ContextSet.union cst cst' in - let entry = match mexpr_entry_o, mty_entry_o with - | None, None -> assert false (* No body, no type ... *) - | None, Some typ -> MType (params, typ) - | Some body, otyp -> MExpr (params, body, otyp) - in - let sobjs, mp0 = match entry with - | MType (_,mte) | MExpr (_,_,Some mte) -> - get_functor_sobjs false env inl_res (params,mte), get_module_path mte - | MExpr (_,me,None) -> - get_functor_sobjs true env inl_expr (params,me), get_module_path me - in - (* Undo the simulated interactive building of the module - and declare the module as a whole *) - Summary.unfreeze_summaries fs; - let inl = match inl_expr with - | None -> None - | _ -> inl_res - in - let () = Global.push_context_set true cst in - let mp_env,resolver = Global.add_module id entry inl in - - (* Name consistency check : kernel vs. library *) - assert (ModPath.equal mp (mp_of_kn (Lib.make_kn id))); - assert (ModPath.equal mp mp_env); - - check_subtypes mp subs; - - let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in - ignore (add_leaf id (ModuleObject sobjs)); - mp - -end - -(** {6 Module types : start, end, declare} *) - -module RawModTypeOps = struct - -let start_modtype interp_modast id args mtys fs = - let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let env = Global.env () in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in - openmodtype_info := sub_mty_l; - let prefix = Lib.start_modtype id mp fs in - Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); - mp - -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 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 = add_leaves id (special@[ModuleTypeObject modtypeobjs]) - in - (* Check name consistence : start_ vs. end_modtype, kernel vs. library *) - assert (eq_full_path (fst oname) (fst oldoname)); - assert (ModPath.equal (mp_of_kn (snd oname)) mp); - - mp - -let declare_modtype interp_modast id args mtys (mty,ann) fs = - let inl = inl2intopt ann in - (* We simulate the beginning of an interactive module, - then we adds the module parameters to the global env. *) - let mp = Global.start_modtype id in - let arg_entries_r, cst = intern_args interp_modast args in - let () = Global.push_context_set true cst in - let params = mk_params_entry arg_entries_r in - let env = Global.env () in - let mte, _, cst = interp_modast env ModType mty in - let () = Global.push_context_set true cst in - let env = Global.env () in - (* We check immediately that mte is well-formed *) - let _, _, _, cst = Mod_typing.translate_mse env None inl mte in - let () = Global.push_context_set true cst in - let env = Global.env () in - let entry = params, mte in - let sub_mty_l, cst = build_subtypes interp_modast env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in - let env = Global.env () in - let sobjs = get_functor_sobjs false env inl entry in - let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in - let sobjs = subst_sobjs subst sobjs in - - (* Undo the simulated interactive building of the module type - and declare the module type as a whole *) - Summary.unfreeze_summaries fs; - - (* We enrich the global environment *) - let mp_env = Global.add_modtype id entry inl in - - (* Name consistency check : kernel vs. library *) - assert (ModPath.equal mp_env mp); - - (* Subtyping checks *) - check_subtypes_mt mp sub_mty_l; - - ignore (add_leaf id (ModuleTypeObject sobjs)); - mp - -end - -(** {6 Include} *) - -module RawIncludeOps = struct - -let rec include_subst env mp reso mbids sign inline = match mbids with - | [] -> empty_subst - | mbid::mbids -> - let farg_id, farg_b, fbody_b = Modops.destr_functor sign in - let subst = include_subst env mp reso mbids fbody_b inline in - let mp_delta = - Modops.inline_delta_resolver env inline mp farg_id farg_b reso - in - join (map_mbid mbid mp mp_delta) subst - -let rec decompose_functor mpl typ = - match mpl, typ with - | [], _ -> typ - | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str - | _ -> user_err Pp.(str "Application of a functor with too much arguments.") - -exception NoIncludeSelf - -let type_of_incl env is_mod = function - |MEident mp -> type_of_mod mp env is_mod - |MEapply _ as me -> - let mp0, mp_l = get_applications me in - decompose_functor mp_l (type_of_mod mp0 env is_mod) - |MEwith _ -> raise NoIncludeSelf - -let declare_one_include interp_modast (me_ast,annot) = - let env = Global.env() in - let me, kind, cst = interp_modast env ModAny me_ast in - let () = Global.push_context_set true cst in - let env = Global.env () in - let is_mod = (kind == Module) in - let cur_mp = Lib.current_mp () in - let inl = inl2intopt annot in - let mbids,aobjs = get_module_sobjs is_mod env inl me in - let subst_self = - try - if List.is_empty mbids then raise NoIncludeSelf; - let typ = type_of_incl env is_mod me in - let reso,_ = Safe_typing.delta_of_senv (Global.safe_env ()) in - include_subst env cur_mp reso mbids typ inl - with NoIncludeSelf -> empty_subst - in - let base_mp = get_module_path me in - let resolver = Global.add_include me is_mod inl in - let subst = join subst_self (map_mp base_mp cur_mp resolver) in - let aobjs = subst_aobjs subst aobjs in - ignore (add_leaf (Lib.current_mod_id ()) (IncludeObject aobjs)) - -let declare_include interp me_asts = - List.iter (declare_one_include interp) me_asts - -end - - -(** {6 Module operations handling summary freeze/unfreeze} *) - -let protect_summaries f = - let fs = Summary.freeze_summaries ~marshallable:false in - try f fs - with reraise -> - (* Something wrong: undo the whole process *) - let reraise = CErrors.push reraise in - let () = Summary.unfreeze_summaries fs in - iraise reraise - -let start_module interp export id args res = - protect_summaries (RawModOps.start_module interp export id args res) - -let end_module = RawModOps.end_module - -let declare_module interp id args mtys me_l = - let declare_me fs = match me_l with - | [] -> RawModOps.declare_module interp id args mtys None fs - | [me] -> RawModOps.declare_module interp id args mtys (Some me) fs - | me_l -> - ignore (RawModOps.start_module interp None id args mtys fs); - RawIncludeOps.declare_include interp me_l; - RawModOps.end_module () - in - protect_summaries declare_me - -let start_modtype interp id args mtys = - protect_summaries (RawModTypeOps.start_modtype interp id args mtys) - -let end_modtype = RawModTypeOps.end_modtype - -let declare_modtype interp id args mtys mty_l = - let declare_mt fs = match mty_l with - | [] -> assert false - | [mty] -> RawModTypeOps.declare_modtype interp id args mtys mty fs - | mty_l -> - ignore (RawModTypeOps.start_modtype interp id args mtys fs); - RawIncludeOps.declare_include interp mty_l; - RawModTypeOps.end_modtype () - in - protect_summaries declare_mt - -let declare_include interp me_asts = - protect_summaries (fun _ -> RawIncludeOps.declare_include interp me_asts) - - -(** {6 Libraries} *) - -type library_name = DirPath.t - -(** A library object is made of some substitutive objects - and some "keep" objects. *) - -type library_objects = Lib.lib_objects * Lib.lib_objects - -(** For the native compiler, we cache the library values *) - -let register_library dir cenv (objs:library_objects) digest univ = - let mp = MPfile dir in - let () = - try - (* Is this library already loaded ? *) - ignore(Global.lookup_module mp); - with Not_found -> - (* If not, let's do it now ... *) - let mp' = Global.import cenv univ digest in - if not (ModPath.equal mp mp') then - anomaly (Pp.str "Unexpected disk module name."); - in - let sobjs,keepobjs = objs in - do_module false load_objects 1 dir mp ([],Objs sobjs) keepobjs - -let start_library dir = - let mp = Global.start_library dir in - openmod_info := default_module_info; - Lib.start_compilation dir mp - -let end_library_hook = ref ignore -let append_end_library_hook f = - let old_f = !end_library_hook in - end_library_hook := fun () -> old_f(); f () - -let end_library ?except ~output_native_objects dir = - !end_library_hook(); - let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except ~output_native_objects dir in - let prefix, lib_stack = Lib.end_compilation oname in - assert (ModPath.equal mp (MPfile dir)); - let substitute, keep, _ = Lib.classify_segment lib_stack in - cenv,(substitute,keep),ast - -let import_module export mp = - really_import_module mp; - Lib.add_anonymous_entry (Lib.Leaf (ImportObject { export; mp })) - -(** {6 Iterators} *) - -let iter_all_segments f = - let rec apply_obj prefix (id,obj) = match obj with - | IncludeObject aobjs -> - let objs = expand_aobjs aobjs in - List.iter (apply_obj prefix) objs - | _ -> f (Lib.make_oname prefix id) obj - in - let apply_mod_obj _ (prefix,substobjs,keepobjs) = - List.iter (apply_obj prefix) substobjs; - List.iter (apply_obj prefix) keepobjs - in - let apply_node = function - | sp, Lib.Leaf o -> f sp o - | _ -> () - in - MPmap.iter apply_mod_obj (ModObjs.all ()); - List.iter apply_node (Lib.contents ()) - - -(** {6 Some types used to shorten declaremods.mli} *) - -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** {6 Debug} *) - -let debug_print_modtab _ = - let pr_seg = function - | [] -> str "[]" - | l -> str "[." ++ int (List.length l) ++ str ".]" - in - let pr_modinfo mp (prefix,substobjs,keepobjs) s = - s ++ str (ModPath.to_string mp) ++ (spc ()) - ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs))) - in - let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in - hov 0 modules diff --git a/library/declaremods.mli b/library/declaremods.mli deleted file mode 100644 index ada53dbff0..0000000000 --- a/library/declaremods.mli +++ /dev/null @@ -1,142 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -(** {6 Modules } *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = - | NoInline - | DefaultInline - | InlineAt of int - -(** Kinds of modules *) - -type module_kind = Module | ModType | ModAny - -type 'modast module_interpretor = - Environ.env -> module_kind -> 'modast -> - Entries.module_struct_entry * module_kind * Univ.ContextSet.t - -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) - -val declare_module : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t - -val start_module : - 'modast module_interpretor -> - bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t - -val end_module : unit -> ModPath.t - - - -(** {6 Module types } *) - -(** [declare_modtype interp_modast id fargs typs exprs] - Similar to [declare_module], except that the types could be multiple *) - -val declare_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> - ModPath.t - -val start_modtype : - 'modast module_interpretor -> - Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t - -val end_modtype : unit -> ModPath.t - -(** {6 Libraries i.e. modules on disk } *) - -type library_name = DirPath.t - -type library_objects - -val register_library : - library_name -> - Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.ContextSet.t -> unit - -val start_library : library_name -> unit - -val end_library : - ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> - Safe_typing.compiled_library * library_objects * Safe_typing.native_library - -(** append a function to be executed at end_library *) -val append_end_library_hook : (unit -> unit) -> unit - -(** [really_import_module mp] opens the module [mp] (in a Caml sense). - It modifies Nametab and performs the [open_object] function for - every object of the module. Raises [Not_found] when [mp] is unknown - or when [mp] corresponds to a functor. *) - -val really_import_module : ModPath.t -> unit - -(** [import_module export mp] is a synchronous version of - [really_import_module]. If [export] is [true], the module is also - opened every time the module containing it is. *) - -val import_module : bool -> ModPath.t -> unit - -(** Include *) - -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit - -(** {6 ... } *) -(** [iter_all_segments] iterate over all segments, the modules' - segments first and then the current segment. Modules are presented - in an arbitrary order. The given function is applied to all leaves - (together with their section path). *) - -val iter_all_segments : - (Libobject.object_name -> Libobject.t -> unit) -> unit - - -val debug_print_modtab : unit -> Pp.t - -(** For printing modules, [process_module_binding] adds names of - bound module (and its components) to Nametab. It also loads - objects associated to it. It may raise a [Failure] when the - bound module hasn't an atomic type. *) - -val process_module_binding : - MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/global.ml b/library/global.ml index ca774dbd74..d4262683bb 100644 --- a/library/global.ml +++ b/library/global.ml @@ -71,6 +71,11 @@ let globalize0 f = GlobalSafeEnv.set_safe_env (f (safe_env ())) let globalize f = let res,env = f (safe_env ()) in GlobalSafeEnv.set_safe_env env; res +let globalize0_with_summary fs f = + let env = f (safe_env ()) in + Summary.unfreeze_summaries fs; + GlobalSafeEnv.set_safe_env env + let globalize_with_summary fs f = let res,env = f (safe_env ()) in Summary.unfreeze_summaries fs; @@ -83,24 +88,32 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_section_context c = globalize0 (Safe_typing.push_section_context c) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c) +let set_check_positive c = globalize0 (Safe_typing.set_check_positive c) +let set_check_universes c = globalize0 (Safe_typing.set_check_universes c) let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) -let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) -let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) +let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) +let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (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 open_section () = globalize0 Safe_typing.open_section +let close_section fs = globalize0_with_summary fs Safe_typing.close_section +let sections_are_opened () = Safe_typing.sections_are_opened (safe_env()) + let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) @@ -116,6 +129,7 @@ let add_module_parameter mbid mte inl = (** Queries on the global environment *) let universes () = universes (env()) +let universes_lbound () = universes_lbound (env()) let named_context () = named_context (env()) let named_context_val () = named_context_val (env()) @@ -178,15 +192,19 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r +let is_template_checked r = is_template_checked (env ()) r + +let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r + let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) -let current_dirpath () = +let current_dirpath () = Safe_typing.current_dirpath (safe_env ()) -let with_global f = +let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in push_context_set false ctx; a diff --git a/library/global.mli b/library/global.mli index d034bc4208..db0f87df7e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -22,6 +22,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool val universes : unit -> UGraph.t +val universes_lbound : unit -> Univ.Level.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Constr.named_context @@ -31,6 +32,9 @@ val named_context : unit -> Constr.named_context val set_engagement : Declarations.engagement -> unit val set_indices_matter : bool -> unit val set_typing_flags : Declarations.typing_flags -> unit +val set_check_guarded : bool -> unit +val set_check_positive : bool -> unit +val set_check_universes : bool -> unit val typing_flags : unit -> Declarations.typing_flags val make_sprop_cumulative : unit -> unit val set_allow_sprop : bool -> unit @@ -40,14 +44,16 @@ val sprop_allowed : unit -> bool val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit +val push_section_context : (Name.t array * Univ.UContext.t) -> unit -val export_private_constants : in_section:bool -> +val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a -val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t + Id.t -> Safe_typing.global_declaration -> Constant.t +val add_private_constant : + Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -67,6 +73,17 @@ val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver +(** Sections *) + +val open_section : unit -> unit +(** [poly] is true when the section should be universe polymorphic *) + +val close_section : Summary.frozen -> unit +(** Close the section and reset the global state to the one at the time when + the section what opened. *) + +val sections_are_opened : unit -> bool + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t @@ -88,7 +105,7 @@ val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Opaqueproof.opaque Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -val lookup_pinductive : Constr.pinductive -> +val lookup_pinductive : Constr.pinductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_mind : MutInd.t -> Declarations.mutual_inductive_body val lookup_module : ModPath.t -> Declarations.module_body @@ -133,12 +150,14 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool +val is_template_checked : GlobRef.t -> bool +val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool (** {6 Retroknowledge } *) val register_inline : Constant.t -> unit -val register_inductive : inductive -> CPrimitives.prim_ind -> unit +val register_inductive : inductive -> 'a CPrimitives.prim_ind -> unit (** {6 Oracle } *) diff --git a/library/globnames.mli b/library/globnames.mli index fc0de96e36..48cbb11b66 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -37,7 +37,7 @@ val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t -(** This constr is not safe to be typechecked, universe polymorphism is not +(** This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing *) val printable_constr_of_global : GlobRef.t -> constr @@ -60,6 +60,6 @@ module ExtRefOrdered : sig val hash : t -> int end -type global_reference_or_constr = +type global_reference_or_constr = | IsGlobal of GlobRef.t | IsConstr of constr diff --git a/library/goptions.ml b/library/goptions.ml index c7024ca81d..6e53bed349 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -52,12 +52,12 @@ type 'a table_of_A = { module MakeTable = functor (A : sig - type t + type t type key module Set : CSig.SetS with type elt = t val table : (string * key table_of_A) list ref val encode : Environ.env -> key -> t - val subst : substitution -> t -> t + val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name val title : string @@ -83,30 +83,30 @@ module MakeTable = | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in let load_options i o = if Int.equal i 1 then cache_options o in - let subst_options (subst,(f,p as obj)) = - let p' = A.subst subst p in - if p' == p then obj else - (f,p') - in + let subst_options (subst,(f,p as obj)) = + let p' = A.subst subst p in + if p' == p then obj else + (f,p') + in let inGo : option_mark * A.t -> obj = Libobject.declare_object {(Libobject.default_object nick) with Libobject.load_function = load_options; - Libobject.open_function = load_options; - Libobject.cache_function = cache_options; - Libobject.subst_function = subst_options; - Libobject.classify_function = (fun x -> Substitute x)} - in + Libobject.open_function = load_options; + Libobject.cache_function = cache_options; + Libobject.subst_function = subst_options; + Libobject.classify_function = (fun x -> Substitute x)} + in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) let print_table table_name printer table = Feedback.msg_notice (str table_name ++ - (hov 0 - (if MySet.is_empty table then str " None" ++ fnl () + (hov 0 + (if MySet.is_empty table then str " None" ++ fnl () else MySet.fold - (fun a b -> spc () ++ printer a ++ b) - table (mt ()) ++ str "." ++ fnl ()))) + (fun a b -> spc () ++ printer a ++ b) + table (mt ()) ++ str "." ++ fnl ()))) let table_of_A = { add = (fun env x -> add_option (A.encode env x)); @@ -398,9 +398,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - Feedback.msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in diff --git a/library/keys.ml b/library/keys.ml deleted file mode 100644 index 9964992433..0000000000 --- a/library/keys.ml +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Keys for unification and indexing *) - -open Names -open Constr -open Libobject -open Globnames - -type key = - | KGlob of GlobRef.t - | KLam - | KLet - | KProd - | KSort - | KCase - | KFix - | KCoFix - | KRel - | KInt - -module KeyOrdered = struct - type t = key - - let hash gr = - match gr with - | KGlob gr -> 9 + GlobRef.Ordered.hash gr - | KLam -> 0 - | KLet -> 1 - | KProd -> 2 - | KSort -> 3 - | KCase -> 4 - | KFix -> 5 - | KCoFix -> 6 - | KRel -> 7 - | KInt -> 8 - - let compare gr1 gr2 = - match gr1, gr2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2 - | _, KGlob _ -> -1 - | KGlob _, _ -> 1 - | k, k' -> Int.compare (hash k) (hash k') - - let equal k1 k2 = - match k1, k2 with - | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2 - | _, KGlob _ -> false - | KGlob _, _ -> false - | k, k' -> k == k' -end - -module Keymap = HMap.Make(KeyOrdered) -module Keyset = Keymap.Set - -(* Mapping structure for references to be considered equivalent *) - -let keys = Summary.ref Keymap.empty ~name:"Keys_decl" - -let add_kv k v m = - try Keymap.modify k (fun k' vs -> Keyset.add v vs) m - with Not_found -> Keymap.add k (Keyset.singleton v) m - -let add_keys k v = - keys := add_kv k v (add_kv v k !keys) - -let equiv_keys k k' = - k == k' || KeyOrdered.equal k k' || - try Keyset.mem k' (Keymap.find k !keys) - with Not_found -> false - -(** Registration of keys as an object *) - -let load_keys _ (_,(ref,ref')) = - add_keys ref ref' - -let cache_keys o = - load_keys 1 o - -let subst_key subst k = - match k with - | KGlob gr -> KGlob (subst_global_reference subst gr) - | _ -> k - -let subst_keys (subst,(k,k')) = - (subst_key subst k, subst_key subst k') - -let discharge_key = function - | KGlob (GlobRef.VarRef _ as g) when Lib.is_in_section g -> None - | x -> Some x - -let discharge_keys (_,(k,k')) = - match discharge_key k, discharge_key k' with - | Some x, Some y -> Some (x, y) - | _ -> None - -type key_obj = key * key - -let inKeys : key_obj -> obj = - declare_object @@ superglobal_object "KEYS" - ~cache:cache_keys - ~subst:(Some subst_keys) - ~discharge:discharge_keys - -let declare_equiv_keys ref ref' = - Lib.add_anonymous_leaf (inKeys (ref,ref')) - -let constr_key kind c = - try - let rec aux k = - match kind k with - | Const (c, _) -> KGlob (GlobRef.ConstRef c) - | Ind (i, u) -> KGlob (GlobRef.IndRef i) - | Construct (c,u) -> KGlob (GlobRef.ConstructRef c) - | Var id -> KGlob (GlobRef.VarRef id) - | App (f, _) -> aux f - | Proj (p, _) -> KGlob (GlobRef.ConstRef (Projection.constant p)) - | Cast (p, _, _) -> aux p - | Lambda _ -> KLam - | Prod _ -> KProd - | Case _ -> KCase - | Fix _ -> KFix - | CoFix _ -> KCoFix - | Rel _ -> KRel - | Meta _ -> raise Not_found - | Evar _ -> raise Not_found - | Sort _ -> KSort - | LetIn _ -> KLet - | Int _ -> KInt - in Some (aux c) - with Not_found -> None - -open Pp - -let pr_key pr_global = function - | KGlob gr -> pr_global gr - | KLam -> str"Lambda" - | KLet -> str"Let" - | KProd -> str"Product" - | KSort -> str"Sort" - | KCase -> str"Case" - | KFix -> str"Fix" - | KCoFix -> str"CoFix" - | KRel -> str"Rel" - | KInt -> str"Int" - -let pr_keyset pr_global v = - prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) - -let pr_mapping pr_global k v = - pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v - -let pr_keys pr_global = - Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/library/keys.mli b/library/keys.mli deleted file mode 100644 index a7adf7791b..0000000000 --- a/library/keys.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type key - -val declare_equiv_keys : key -> key -> unit -(** Declare two keys as being equivalent. *) - -val equiv_keys : key -> key -> bool -(** Check equivalence of keys. *) - -val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option -(** Compute the head key of a term. *) - -val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t -(** Pretty-print the mapping *) diff --git a/library/lib.ml b/library/lib.ml index 59b55cc16b..c3c480aee4 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -52,7 +52,7 @@ let subst_atomic_objects subst seg = let subst_one = fun (id,obj as node) -> let obj' = subst_object (subst,obj) in if obj' == obj then node else - (id, obj') + (id, obj') in List.Smart.map subst_one seg @@ -73,11 +73,8 @@ let classify_segment seg = clean ((id,o)::substl, keepl, anticipl) stk | KeepObject _ -> clean (substl, (id,o)::keepl, anticipl) stk - | ImportObject { export } -> - if export then - clean ((id,o)::substl, keepl, anticipl) stk - else - clean acc stk + | ExportObject _ -> + clean ((id,o)::substl, keepl, anticipl) stk | AtomicObject obj -> begin match classify_object obj with | Dispose -> clean acc stk @@ -110,7 +107,6 @@ let segment_of_objects prefix = let initial_prefix = Nametab.{ obj_dir = default_library; obj_mp = ModPath.initial; - obj_sec = DirPath.empty; } type lib_state = { @@ -135,10 +131,10 @@ let library_dp () = let cwd () = !lib_state.path_prefix.Nametab.obj_dir let current_mp () = !lib_state.path_prefix.Nametab.obj_mp -let current_sections () = !lib_state.path_prefix.Nametab.obj_sec +let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env()) -let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) -let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) +let sections_depth () = Section.depth (current_sections()) +let sections_are_opened = Global.sections_are_opened let cwd_except_section () = Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) @@ -172,7 +168,6 @@ let pop_path_prefix () = let op = !lib_state.path_prefix in lib_state := { !lib_state with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir; - obj_sec = pop_dirpath op.obj_sec; } } let find_entry_p p = @@ -285,7 +280,7 @@ let current_mod_id () = let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in - let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in + let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_dir dir @@ -301,15 +296,15 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in - user_err + user_err (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.") let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with | oname,OpenedModule (ty,_,_,fs) -> - if ty == is_type then oname, fs - else error_still_opened (module_kind ty) oname + if ty == is_type then oname, fs + else error_still_opened (module_kind ty) oname | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false with Not_found -> user_err (Pp.str "No opened modules.") @@ -333,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then + if Global.sections_are_opened () then (* XXX not sure if we need this check *) user_err Pp.(str "some sections are already opened"); - let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } @@ -364,7 +359,7 @@ let end_compilation_checks dir = match !lib_state.comp_name with | None -> anomaly (Pp.str "There should be a module name...") | Some m -> - if not (Names.DirPath.equal m dir) then anomaly + if not (Names.DirPath.equal m dir) then anomaly (str "The current open module has name" ++ spc () ++ DirPath.print m ++ spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); in @@ -413,158 +408,25 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind +let instance_from_variable_context = + List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list -type variable_context = variable_info list -type abstr_info = { - abstr_ctx : variable_context; - abstr_subst : Univ.Instance.t; - abstr_uctx : Univ.AUContext.t; -} -type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t - -type secentry = - | Variable of { - id:Names.Id.t; - kind:Decl_kinds.binding_kind; - univs:Univ.ContextSet.t; - } - | Context of Univ.ContextSet.t - -type section_data = { - sec_entry : secentry list; - sec_workl : Opaqueproof.work_list; - sec_abstr : abstr_list; - sec_poly : bool; -} +let extract_worklist info = + let args = instance_from_variable_context info.Section.abstr_ctx in + info.Section.abstr_subst, args -let empty_section_data ~poly = { - sec_entry = []; - sec_workl = (Names.Cmap.empty,Names.Mindmap.empty); - sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty); - sec_poly = poly; -} +let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () -let sectab = - Summary.ref ([] : section_data list) ~name:"section-context" - -let check_same_poly p sec = - if p != sec.sec_poly then - user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") - -let add_section ~poly () = - List.iter (fun tab -> check_same_poly poly tab) !sectab; - sectab := empty_section_data ~poly :: !sectab - -let add_section_variable ~name ~kind ~poly univs = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - List.iter (fun tab -> check_same_poly poly tab) !sectab; - let s = { s with sec_entry = Variable {id=name;kind;univs} :: s.sec_entry } in - sectab := s :: sl - -let add_section_context ctx = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - check_same_poly true s; - let s = { s with sec_entry = Context ctx :: s.sec_entry } in - sectab := s :: sl - -exception PolyFound of bool (* make this a let exception once possible *) -let is_polymorphic_univ u = - try - let open Univ in - List.iter (fun s -> - let vars = s.sec_entry in - List.iter (function - | Variable {univs=(univs,_)} -> - if LSet.mem u univs then raise (PolyFound s.sec_poly) - | Context (univs,_) -> - if LSet.mem u univs then raise (PolyFound true) - ) vars - ) !sectab; - false - with PolyFound b -> b - -let extract_hyps poly (secs,ohyps) = - let rec aux = function - | (Variable {id;kind;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> - let l, r = aux (idl,hyps) in - (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r - | (Variable {univs}::idl,hyps) -> - let l, r = aux (idl,hyps) in - l, if poly then Univ.ContextSet.union r univs else r - | (Context ctx :: idl, hyps) -> - let l, r = aux (idl, hyps) in - l, Univ.ContextSet.union r ctx - | [], _ -> [],Univ.ContextSet.empty - in aux (secs,ohyps) - -let instance_from_variable_context = - List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list - -let name_instance inst = - (* FIXME: this should probably be done at an upper level, by storing the - name information in the section data structure. *) - let map lvl = match Univ.Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - Name (Libnames.qualid_basename qid) - with Not_found -> - (* Best-effort naming from the string representation of the level. - See univNames.ml for a similar hack. *) - Name (Id.of_string_soft (Univ.Level.to_string lvl)) - in - Array.map map (Univ.Instance.to_array inst) - -let add_section_replacement f g poly hyps = - match !sectab with - | [] -> () - | s :: sl -> - let () = check_same_poly poly s in - let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in - let ctx = Univ.ContextSet.to_context ctx in - let inst = Univ.UContext.instance ctx in - let nas = name_instance inst in - let subst, ctx = Univ.abstract_universes nas ctx in - let args = instance_from_variable_context (List.rev sechyps) in - let info = { - abstr_ctx = sechyps; - abstr_subst = subst; - abstr_uctx = ctx; - } in - let s = { s with - sec_workl = f (inst, args) s.sec_workl; - sec_abstr = g info s.sec_abstr; - } in - sectab := s :: sl - -let add_section_kn ~poly kn = - let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f f poly - -let add_section_constant ~poly kn = - let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f poly - -let replacement_context () = (List.hd !sectab).sec_workl +let replacement_context () = + Section.replacement_context (Global.env ()) (sections ()) let section_segment_of_constant con = - Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) + Section.segment_of_constant (Global.env ()) con (sections ()) let section_segment_of_mutual_inductive kn = - Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) + Section.segment_of_inductive (Global.env ()) kn (sections ()) -let empty_segment = { - abstr_ctx = []; - abstr_subst = Univ.Instance.empty; - abstr_uctx = Univ.AUContext.empty; -} +let empty_segment = Section.empty_segment let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c @@ -573,40 +435,36 @@ let section_segment_of_reference = let open GlobRef in function | VarRef _ -> empty_segment let variable_section_segment_of_reference gr = - (section_segment_of_reference gr).abstr_ctx + (section_segment_of_reference gr).Section.abstr_ctx + +let is_in_section ref = + Section.is_in_section (Global.env ()) ref (sections ()) let section_instance = let open GlobRef in function | VarRef id -> - let eq = function - | Variable {id=id'} -> Names.Id.equal id id' - | Context _ -> false - in - if List.exists eq (List.hd !sectab).sec_entry - then Univ.Instance.empty, [||] - else raise Not_found + if is_in_section (VarRef id) then (Univ.Instance.empty, [||]) + else raise Not_found | ConstRef con -> - Names.Cmap.find con (fst (List.hd !sectab).sec_workl) + let data = section_segment_of_constant con in + extract_worklist data | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Names.Mindmap.find kn (snd (List.hd !sectab).sec_workl) - -let is_in_section ref = - try ignore (section_instance ref); true with Not_found -> false + let data = section_segment_of_mutual_inductive kn in + extract_worklist data (*************) (* Sections. *) -let open_section ~poly id = +let open_section id = + let () = Global.open_section () in let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in - let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in if Nametab.exists_dir obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:false in add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); - lib_state := { !lib_state with path_prefix = prefix }; - add_section ~poly () - + lib_state := { !lib_state with path_prefix = prefix } (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) @@ -616,7 +474,7 @@ let discharge_item ((sp,_ as oname),e) = | Leaf lobj -> begin match lobj with | ModuleObject _ | ModuleTypeObject _ | IncludeObject _ | KeepObject _ - | ImportObject _ -> None + | ExportObject _ -> None | AtomicObject obj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,obj)) end @@ -635,7 +493,7 @@ let close_section () = lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); let newdecls = List.map discharge_item secdecls in - Summary.unfreeze_summaries fs; + let () = Global.close_section fs in List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) @@ -693,7 +551,7 @@ let discharge_proj_repr = let _, newpars = Mindmap.find mind (snd modlist) in mind, npars + Array.length newpars) -let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = +let discharge_abstract_universe_context { Section.abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in let ainst = make_abstract_instance auctx in let subst = Instance.append subst ainst in diff --git a/library/lib.mli b/library/lib.mli index fe6bf69ec4..a313a62c2e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool +[@@ocaml.deprecated "Use Global.sections_are_opened"] val sections_depth : unit -> int (** Are we inside an opened module type *) @@ -147,7 +148,7 @@ val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : poly:bool -> Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) @@ -163,40 +164,21 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Constr.named_declaration * Decl_kinds.binding_kind -type variable_context = variable_info list -type abstr_info = private { - abstr_ctx : variable_context; - (** Section variables of this prefix *) - abstr_subst : Univ.Instance.t; - (** Actual names of the abstracted variables *) - abstr_uctx : Univ.AUContext.t; - (** Universe quantification, same length as the substitution *) -} +val section_segment_of_constant : Constant.t -> Section.abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> Section.abstr_info +val section_segment_of_reference : GlobRef.t -> Section.abstr_info -val instance_from_variable_context : variable_context -> Id.t array - -val section_segment_of_constant : Constant.t -> abstr_info -val section_segment_of_mutual_inductive: MutInd.t -> abstr_info -val section_segment_of_reference : GlobRef.t -> abstr_info - -val variable_section_segment_of_reference : GlobRef.t -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit -val add_section_context : Univ.ContextSet.t -> unit -val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit -val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list -val is_polymorphic_univ : Univ.Level.t -> bool - (** {6 Discharge: decrease the section level if in the current section } *) (* XXX Why can't we use the kernel functions ? *) val discharge_proj_repr : Projection.Repr.t -> Projection.Repr.t val discharge_abstract_universe_context : - abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t + Section.abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/libnames.ml b/library/libnames.ml index 485f8837e8..126841c9a5 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -62,7 +62,7 @@ let parse_dir s = if n >= len then dirs else let pos = try - String.index_from s n '.' + String.index_from s n '.' with Not_found -> len in if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path."); diff --git a/library/libobject.ml b/library/libobject.ml index 27e7810e6c..a632a426fd 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -75,7 +75,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ImportObject of { export : bool; mp : ModPath.t } + | ExportObject of { mpl : ModPath.t list } | AtomicObject of obj and objects = (Names.Id.t * t) list @@ -113,12 +113,12 @@ let declare_object_full odecl = and rebuild lobj = infun (odecl.rebuild_function (outfun lobj)) in Hashtbl.add cache_tab na { dyn_cache_function = cacher; - dyn_load_function = loader; + dyn_load_function = loader; dyn_open_function = opener; - dyn_subst_function = substituter; - dyn_classify_function = classifier; - dyn_discharge_function = discharge; - dyn_rebuild_function = rebuild }; + dyn_subst_function = substituter; + dyn_classify_function = classifier; + dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild }; (infun,outfun) let declare_object odecl = fst (declare_object_full odecl) @@ -144,7 +144,7 @@ let load_object i ((_,lobj) as node) = let open_object i ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj -let subst_object ((_,lobj) as node) = +let subst_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj let classify_object lobj = diff --git a/library/libobject.mli b/library/libobject.mli index 3b37db4a6f..146ccc293f 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -112,7 +112,7 @@ and t = | ModuleTypeObject of substitutive_objects | IncludeObject of algebraic_objects | KeepObject of objects - | ImportObject of { export : bool; mp : Names.ModPath.t } + | ExportObject of { mpl : Names.ModPath.t list } | AtomicObject of obj and objects = (Names.Id.t * t) list diff --git a/library/library.ml b/library/library.ml deleted file mode 100644 index 0faef7bf84..0000000000 --- a/library/library.ml +++ /dev/null @@ -1,642 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open CErrors -open Util - -open Names -open Libnames -open Lib -open Libobject - -(************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -let raw_extern_library f = - System.raw_extern_state Coq_config.vo_magic_number f - -let raw_intern_library f = - System.with_magic_number_check - (System.raw_intern_state Coq_config.vo_magic_number) f - -(************************************************************************) -(** Serialized objects loaded on-the-fly *) - -exception Faulty of string - -module Delayed : -sig - -type 'a delayed -val in_delayed : string -> in_channel -> 'a delayed * Digest.t -val fetch_delayed : 'a delayed -> 'a - -end = -struct - -type 'a delayed = { - del_file : string; - del_off : int; - del_digest : Digest.t; -} - -let in_delayed f ch = - let pos = pos_in ch in - let _, digest = System.skip_in_segment f ch in - ({ del_file = f; del_digest = digest; del_off = pos; }, digest) - -(** Fetching a table of opaque terms at position [pos] in file [f], - expecting to find first a copy of [digest]. *) - -let fetch_delayed del = - let { del_digest = digest; del_file = f; del_off = pos; } = del in - try - let ch = raw_intern_library f in - let () = seek_in ch pos in - let obj, _, digest' = System.marshal_in_segment f ch in - let () = close_in ch in - if not (String.equal digest digest') then raise (Faulty f); - obj - with e when CErrors.noncritical e -> raise (Faulty f) - -end - -open Delayed - - -(************************************************************************) -(*s Modules on disk contain the following informations (after the magic - number, and before the digest). *) - -type compilation_unit_name = DirPath.t - -type library_disk = { - md_compiled : Safe_typing.compiled_library; - md_objects : Declaremods.library_objects; -} - -type summary_disk = { - md_name : compilation_unit_name; - md_imports : compilation_unit_name array; - md_deps : (compilation_unit_name * Safe_typing.vodigest) array; -} - -(*s Modules loaded in memory contain the following informations. They are - kept in the global table [libraries_table]. *) - -type library_t = { - library_name : compilation_unit_name; - library_data : library_disk delayed; - library_deps : (compilation_unit_name * Safe_typing.vodigest) array; - library_imports : compilation_unit_name array; - library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.ContextSet.t; -} - -type library_summary = { - libsum_name : compilation_unit_name; - libsum_digests : Safe_typing.vodigest; - libsum_imports : compilation_unit_name array; -} - -module LibraryOrdered = DirPath -module LibraryMap = Map.Make(LibraryOrdered) -module LibraryFilenameMap = Map.Make(LibraryOrdered) - -(* This is a map from names to loaded libraries *) -let libraries_table : library_summary LibraryMap.t ref = - Summary.ref LibraryMap.empty ~name:"LIBRARY" - -(* This is the map of loaded libraries filename *) -(* (not synchronized so as not to be caught in the states on disk) *) -let libraries_filename_table = ref LibraryFilenameMap.empty - -(* These are the _ordered_ sets of loaded, imported and exported libraries *) -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" - -(* various requests to the tables *) - -let find_library dir = - LibraryMap.find dir !libraries_table - -let try_find_library dir = - try find_library dir - with Not_found -> - user_err ~hdr:"Library.find_library" - (str "Unknown library " ++ DirPath.print dir) - -let register_library_filename dir f = - (* Not synchronized: overwrite the previous binding if one existed *) - (* from a previous play of the session *) - libraries_filename_table := - LibraryFilenameMap.add dir f !libraries_filename_table - -let library_full_filename dir = - try LibraryFilenameMap.find dir !libraries_filename_table - with Not_found -> "<unavailable filename>" - -let overwrite_library_filenames f = - let f = - if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in - LibraryMap.iter (fun dir _ -> register_library_filename dir f) - !libraries_table - -let library_is_loaded dir = - try let _ = find_library dir in true - with Not_found -> false - -let library_is_opened dir = - List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list - -let loaded_libraries () = !libraries_loaded_list - -let opened_libraries () = !libraries_imports_list - - (* If a library is loaded several time, then the first occurrence must - be performed first, thus the libraries_loaded_list ... *) - -let register_loaded_library m = - let libname = m.libsum_name in - let link () = - let dirname = Filename.dirname (library_full_filename libname) in - let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in - let f = prefix ^ "cmo" in - let f = Dynlink.adapt_filename f in - if Coq_config.native_compiler then - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f - in - let rec aux = function - | [] -> link (); [libname] - | m'::_ as l when DirPath.equal m' libname -> l - | m'::l' -> m' :: aux l' in - libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := LibraryMap.add libname m !libraries_table - - (* ... while if a library is imported/exported several time, then - only the last occurrence is really needed - though the imported - list may differ from the exported list (consider the sequence - Export A; Export B; Import A which results in A;B for exports but - in B;A for imports) *) - -let rec remember_last_of_each l m = - match l with - | [] -> [m] - | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m - | m'::l' -> m' :: remember_last_of_each l' m - -let register_open_library export m = - libraries_imports_list := remember_last_of_each !libraries_imports_list m; - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(************************************************************************) -(*s Opening libraries *) - -(* [open_library export explicit m] opens library [m] if not already - opened _or_ if explicitly asked to be (re)opened *) - -let open_library export explicit_libs m = - if - (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentioned by the user are always reopen *) - List.exists (fun m' -> DirPath.equal m m') explicit_libs - || not (library_is_opened m) - then begin - register_open_library export m; - Declaremods.really_import_module (MPfile m) - end - else - if export then - libraries_exports_list := remember_last_of_each !libraries_exports_list m - -(* open_libraries recursively open a list of libraries but opens only once - a library that is re-exported many times *) - -let open_libraries export modl = - let to_open_list = - List.fold_left - (fun l m -> - let subimport = - Array.fold_left - (fun l m -> remember_last_of_each l m) - l m.libsum_imports - in remember_last_of_each subimport m.libsum_name) - [] modl in - let explicit = List.map (fun m -> m.libsum_name) modl in - List.iter (open_library export explicit) to_open_list - - -(**********************************************************************) -(* import and export of libraries - synchronous operations *) -(* at the end similar to import and export of modules except that it *) -(* is optimized: when importing several libraries at the same time *) -(* which themselves indirectly imports the very same modules, these *) -(* ones are imported only ones *) - -let open_import_library i (_,(modl,export)) = - if Int.equal i 1 then - (* even if the library is already imported, we re-import it *) - (* if not (library_is_opened dir) then *) - open_libraries export (List.map try_find_library modl) - -let cache_import_library obj = - open_import_library 1 obj - -let subst_import_library (_,o) = o - -let classify_import_library (_,export as obj) = - if export then Substitute obj else Dispose - -let in_import_library : DirPath.t list * bool -> obj = - declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import_library; - open_function = open_import_library; - subst_function = subst_import_library; - classify_function = classify_import_library } - -(************************************************************************) -(** {6 Tables of opaque proof terms} *) - -(** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, - we can quickly load a first half of a .vo file without these opaque - terms, and access them only when a specific command (e.g. Print or - Print Assumptions) needs it. *) - -(** Delayed / available tables of opaque terms *) - -type 'a table_status = - | ToFetch of 'a array delayed - | Fetched of 'a array - -let opaque_tables = - ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t) - -let add_opaque_table dp st = - opaque_tables := LibraryMap.add dp st !opaque_tables - -let access_table what tables dp i = - let t = match LibraryMap.find dp !tables with - | Fetched t -> t - | ToFetch f -> - let dir_path = Names.DirPath.to_string dp in - Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); - let t = - try fetch_delayed f - with Faulty f -> - user_err ~hdr:"Library.access_table" - (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ - str ") is inaccessible or corrupted,\ncannot load some " ++ - str what ++ str " in it.\n") - in - tables := LibraryMap.add dp (Fetched t) !tables; - t - in - assert (i < Array.length t); t.(i) - -let access_opaque_table dp i = - let what = "opaque proofs" in - access_table what opaque_tables dp i - -let indirect_accessor = { - Opaqueproof.access_proof = access_opaque_table; - Opaqueproof.access_discharge = Cooking.cook_constr; -} - -(************************************************************************) -(* Internalise libraries *) - -type seg_sum = summary_disk -type seg_lib = library_disk -type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm array - -let mk_library sd md digests univs = - { - library_name = sd.md_name; - library_data = md; - library_deps = sd.md_deps; - library_imports = sd.md_imports; - library_digests = digests; - library_extra_univs = univs; - } - -let mk_summary m = { - libsum_name = m.library_name; - libsum_imports = m.library_imports; - libsum_digests = m.library_digests; -} - -let intern_from_file f = - let ch = raw_intern_library f in - let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in - let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in - let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in - let _ = System.skip_in_segment f ch in - let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in - close_in ch; - register_library_filename lsd.md_name f; - add_opaque_table lsd.md_name (ToFetch del_opaque); - let open Safe_typing in - match univs with - | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - | Some (uall,true) -> - mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall - | Some (_,false) -> - mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty - -module DPMap = Map.Make(DirPath) - -let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = - (* Look if in the current logical environment *) - try (find_library dir).libsum_digests, (needed, contents) - with Not_found -> - (* Look if already listed and consequently its dependencies too *) - try (DPMap.find dir contents).library_digests, (needed, contents) - with Not_found -> - Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); - (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> lib_resolver dir in - let m = intern_from_file f in - if not (DirPath.equal dir m.library_name) then - user_err ~hdr:"load_physical_library" - (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - DirPath.print m.library_name ++ spc () ++ str "and not library" ++ - spc() ++ DirPath.print dir); - Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f - -and intern_library_deps ~lib_resolver libs dir m from = - let needed, contents = - Array.fold_left (intern_mandatory_library ~lib_resolver dir from) - libs m.library_deps in - (dir :: needed, DPMap.add dir m contents ) - -and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = - let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in - if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err (str "Compiled library " ++ DirPath.print caller ++ - str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ - over library " ++ DirPath.print dir); - libs - -let rec_intern_library ~lib_resolver libs (dir, f) = - let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in - libs - -let native_name_from_filename f = - let ch = raw_intern_library f in - let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in - Nativecode.mod_uid_of_dirpath lmd.md_name - -(**********************************************************************) -(*s [require_library] loads and possibly opens a library. This is a - synchronized operation. It is performed as follows: - - preparation phase: (functions require_library* ) the library and its - dependencies are read from to disk (using intern_* ) - [they are read from disk to ensure that at section/module - discharging time, the physical library referred to outside the - section/module is the one that was used at type-checking time in - the section/module] - - execution phase: (through add_leaf and cache_require) - the library is loaded in the environment and Nametab, the objects are - registered etc, using functions from Declaremods (via load_library, - which recursively loads its dependencies) -*) - -let register_library m = - let l = fetch_delayed m.library_data in - Declaremods.register_library - m.library_name - l.md_compiled - l.md_objects - m.library_digests - m.library_extra_univs; - register_loaded_library (mk_summary m) - -(* Follow the semantics of Anticipate object: - - called at module or module type closing when a Require occurs in - the module or module type - - not called from a library (i.e. a module identified with a file) *) -let load_require _ (_,(needed,modl,_)) = - List.iter register_library needed - -let open_require i (_,(_,modl,export)) = - Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) - export - - (* [needed] is the ordered list of libraries not already loaded *) -let cache_require o = - load_require 1 o; - open_require 1 o - -let discharge_require (_,o) = Some o - -(* open_function is never called from here because an Anticipate object *) - -type require_obj = library_t list * DirPath.t list * bool option - -let in_require : require_obj -> obj = - declare_object {(default_object "REQUIRE") with - cache_function = cache_require; - load_function = load_require; - open_function = (fun _ _ -> assert false); - discharge_function = discharge_require; - classify_function = (fun o -> Anticipate o) } - -(* Require libraries, import them if [export <> None], mark them for export - if [export = Some true] *) - -let warn_require_in_module = - CWarnings.create ~name:"require-in-module" ~category:"deprecated" - (fun () -> strbrk "Require inside a module is" ++ - strbrk " deprecated and strongly discouraged. " ++ - strbrk "You can Require a module at toplevel " ++ - strbrk "and optionally Import it inside another one.") - -let require_library_from_dirpath ~lib_resolver modrefl export = - let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in - let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in - let modrefl = List.map fst modrefl in - if Lib.is_module_or_modtype () then - begin - warn_require_in_module (); - add_anonymous_leaf (in_require (needed,modrefl,None)); - Option.iter (fun exp -> - add_anonymous_leaf (in_import_library (modrefl,exp))) - export - end - else - add_anonymous_leaf (in_require (needed,modrefl,export)); - () - -(* the function called by Vernacentries.vernac_import *) - -let safe_locate_module qid = - try Nametab.locate_module qid - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module" - (pr_qualid qid ++ str " is not a module") - -let import_module export modl = - (* Optimization: libraries in a raw in the list are imported - "globally". If there is non-library in the list; it breaks the - optimization For instance: "Import Arith MyModule Zarith" will - not be optimized (possibly resulting in redefinitions, but - "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" - will have the submodules imported by both Arith and ZArith - imported only once *) - let flush = function - | [] -> () - | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in - let rec aux acc = function - | qid :: l -> - let m,acc = - try Nametab.locate_module qid, acc - with Not_found-> flush acc; safe_locate_module qid, [] in - (match m with - | MPfile dir -> aux (dir::acc) l - | mp -> - flush acc; - try Declaremods.import_module export mp; aux [] l - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"import_module" - (pr_qualid qid ++ str " is not a module")) - | [] -> flush acc - in aux [] modl - -(************************************************************************) -(*s Initializing the compilation of a library. *) - -let load_library_todo f = - let ch = raw_intern_library f in - let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in - let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in - let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let tasks, _, _ = System.marshal_in_segment f ch in - let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in - close_in ch; - if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get tasks, s4 - -(************************************************************************) -(*s [save_library dir] ends library [dir] and save it to the disk. *) - -let current_deps () = - let map name = - let m = try_find_library name in - (name, m.libsum_digests) - in - List.map map !libraries_loaded_list - -let current_reexports () = !libraries_exports_list - -let error_recursively_dependent_library dir = - user_err - (strbrk "Unable to use logical name " ++ DirPath.print dir ++ - strbrk " to save current library because" ++ - strbrk " it already depends on a library of this name.") - -(* We now use two different digests in a .vo file. The first one - only covers half of the file, without the opaque table. It is - used for identifying this version of this library : this digest - is the one leading to "inconsistent assumptions" messages. - The other digest comes at the very end, and covers everything - before it. This one is used for integrity check of the whole - file when loading the opaque table. *) - -(* Security weakness: file might have been changed on disk between - writing the content and computing the checksum... *) - -let save_library_to ?todo ~output_native_objects dir f otab = - let except = match todo with - | None -> - (* XXX *) - (* assert(!Flags.compilation_mode = Flags.BuildVo); *) - assert(Filename.check_suffix f ".vo"); - Future.UUIDSet.empty - | Some (l,_) -> - assert(Filename.check_suffix f ".vio"); - List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) - Future.UUIDSet.empty l in - let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab = - match todo with - | None -> None, None - | Some (tasks, rcbackup) -> - let tasks = - List.map Stateid.(fun (r,b) -> - try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b - with Not_found -> assert b; { r with uuid = -1 }, b) - tasks in - Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false) - in - let sd = { - md_name = dir; - md_deps = Array.of_list (current_deps ()); - md_imports = Array.of_list (current_reexports ()); - } in - let md = { - md_compiled = cenv; - md_objects = seg; - } in - if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then - error_recursively_dependent_library dir; - (* Open the vo file and write the magic number *) - let f' = f in - let ch = raw_extern_library f' in - try - (* Writing vo payload *) - System.marshal_out_segment f' ch (sd : seg_sum); - System.marshal_out_segment f' ch (md : seg_lib); - System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (tasks : 'tasks option); - System.marshal_out_segment f' ch (opaque_table : seg_proofs); - close_out ch; - (* Writing native code files *) - if output_native_objects then - let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - Nativelib.compile_library dir ast fn - with reraise -> - let reraise = CErrors.push reraise in - let () = Feedback.msg_warning (str "Removed file " ++ str f') in - let () = close_out ch in - let () = Sys.remove f' in - iraise reraise - -let save_library_raw f sum lib univs proofs = - let ch = raw_extern_library f in - System.marshal_out_segment f ch (sum : seg_sum); - System.marshal_out_segment f ch (lib : seg_lib); - System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : 'tasks option); - System.marshal_out_segment f ch (proofs : seg_proofs); - close_out ch - -module StringOrd = struct type t = string let compare = String.compare end -module StringSet = Set.Make(StringOrd) - -let get_used_load_paths () = - StringSet.elements - (List.fold_left (fun acc m -> StringSet.add - (Filename.dirname (library_full_filename m)) acc) - StringSet.empty !libraries_loaded_list) - -let _ = Nativelib.get_load_paths := get_used_load_paths diff --git a/library/library.mli b/library/library.mli deleted file mode 100644 index bb6c42e393..0000000000 --- a/library/library.mli +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Libnames - -(** This module provides functions to load, open and save - libraries. Libraries correspond to the subclass of modules that - coincide with a file on disk (the ".vo" files). Libraries on the - disk comes with checksums (obtained with the [Digest] module), which - are checked at loading time to prevent inconsistencies between files - written at various dates. -*) - -(** {6 ... } - Require = load in the environment + open (if the optional boolean - is not [None]); mark also for export if the boolean is [Some true] *) -val require_library_from_dirpath - : lib_resolver:(DirPath.t -> CUnix.physical_path) - -> (DirPath.t * string) list - -> bool option - -> unit - -(** {6 Start the compilation of a library } *) - -(** Segments of a library *) -type seg_sum -type seg_lib -type seg_univ = (* all_cst, finished? *) - Univ.ContextSet.t * bool -type seg_proofs = Opaqueproof.opaque_proofterm array - -(** Open a module (or a library); if the boolean is true then it's also - an export otherwise just a simple import *) -val import_module : bool -> qualid list -> unit - -(** End the compilation of a library and save it to a ".vo" file. - [output_native_objects]: when producing vo objects, also compile the native-code version. *) -val save_library_to : - ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> - output_native_objects:bool -> - DirPath.t -> string -> Opaqueproof.opaquetab -> unit - -val load_library_todo - : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs - -val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit - -(** {6 Interrogate the status of libraries } *) - - (** - Tell if a library is loaded or opened *) -val library_is_loaded : DirPath.t -> bool -val library_is_opened : DirPath.t -> bool - - (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> DirPath.t list -val opened_libraries : unit -> DirPath.t list - - (** - Return the full filename of a loaded library. *) -val library_full_filename : DirPath.t -> string - - (** - Overwrite the filename of all libraries (used when restoring a state) *) -val overwrite_library_filenames : string -> unit - -(** {6 Native compiler. } *) -val native_name_from_filename : string -> string - -(** {6 Opaque accessors} *) -val indirect_accessor : Opaqueproof.indirect_accessor diff --git a/library/library.mllib b/library/library.mllib index 35af5fa43b..a6188f7661 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,4 +1,3 @@ -Decl_kinds Libnames Globnames Libobject @@ -6,10 +5,7 @@ Summary Nametab Global Lib -Declaremods -Library States Kindops Goptions -Keys Coqlib diff --git a/library/nametab.ml b/library/nametab.ml index aed7d08ac1..283da5936c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,12 +18,10 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } let eq_op op1 op2 = DirPath.equal op1.obj_dir op2.obj_dir && - DirPath.equal op1.obj_sec op2.obj_sec && ModPath.equal op1.obj_mp op2.obj_mp (* to this type are mapped DirPath.t's in the nametab *) @@ -130,7 +128,7 @@ struct (* Dictionaries of short names *) type nametree = { path : path_status; - map : nametree ModIdmap.t } + map : nametree ModIdmap.t } let mktree p m = { path=p; map=m } let empty_tree = mktree Nothing ModIdmap.empty @@ -151,34 +149,34 @@ struct let ptab = modify () empty_tree in ModIdmap.add modid ptab tree.map in - let this = + let this = if level <= 0 then - match tree.path with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it - otherwise it may become unaccessible forever *) + match tree.path with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) warn_masking_absolute n; tree.path - | Nothing - | Relative _ -> Relative (uname,o) + | Nothing + | Relative _ -> Relative (uname,o) else tree.path - in - mktree this map + in + mktree this map | [] -> - match tree.path with - | Absolute (uname',o') -> - if E.equal o' o then begin - assert (U.equal uname uname'); - tree - (* we are putting the same thing for the second time :) *) - end - else - (* This is an absolute name, we must keep it otherwise it may - become unaccessible forever *) - (* But ours is also absolute! This is an error! *) - user_err Pp.(str @@ "Cannot mask the absolute name \"" + match tree.path with + | Absolute (uname',o') -> + if E.equal o' o then begin + assert (U.equal uname uname'); + tree + (* we are putting the same thing for the second time :) *) + end + else + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + (* But ours is also absolute! This is an error! *) + user_err Pp.(str @@ "Cannot mask the absolute name \"" ^ U.to_string uname' ^ "\"!") - | Nothing - | Relative _ -> mktree (Absolute (uname,o)) tree.map + | Nothing + | Relative _ -> mktree (Absolute (uname,o)) tree.map let rec push_exactly uname o level tree = function | [] -> @@ -243,7 +241,7 @@ let user_name qid tab = let find uname tab = let id,l = U.repr uname in match search (Id.Map.find id tab) l with - Absolute (_,o) -> o + Absolute (_,o) -> o | _ -> raise Not_found let exists uname tab = @@ -262,9 +260,9 @@ let shortest_qualid ?loc ctx uname tab = | Absolute (u,_) | Relative (u,_) when U.equal u uname && not (is_empty && hidden) -> List.rev pos | _ -> - match dir with - [] -> raise Not_found - | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map) + match dir with + [] -> raise Not_found + | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map) in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in @@ -387,25 +385,25 @@ let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevta let push_xref visibility sp xref = match visibility with | Until _ -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - the_globrevtab := Globrevtab.add xref sp !the_globrevtab + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + the_globrevtab := Globrevtab.add xref sp !the_globrevtab | _ -> - begin - if ExtRefTab.exists sp !the_ccitab then + begin + if ExtRefTab.exists sp !the_ccitab then let open GlobRef in - match ExtRefTab.find sp !the_ccitab with - | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | - TrueGlobal( ConstructRef _) as xref -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - | _ -> - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - else - the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; - end + match ExtRefTab.find sp !the_ccitab with + | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) | + TrueGlobal( ConstructRef _) as xref -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + | _ -> + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + else + the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab; + end let push_cci visibility sp ref = push_xref visibility sp (TrueGlobal ref) - + (* This is for Syntactic Definitions *) let push_syndef visibility sp kn = push_xref visibility sp (SynDef kn) diff --git a/library/nametab.mli b/library/nametab.mli index 6ee22fc283..d603bd51e2 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -74,7 +74,6 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } val eq_op : object_prefix -> object_prefix -> bool @@ -101,7 +100,7 @@ val error_global_not_found : qualid -> 'a object is loaded inside a module -- or - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) - + *) type visibility = Until of int | Exactly of int diff --git a/library/states.ml b/library/states.ml index a73f16957d..0be153d96a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -9,7 +9,6 @@ (************************************************************************) open Util -open System type state = Lib.frozen * Summary.frozen @@ -25,13 +24,6 @@ let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs -let extern_state s = - System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true) - -let intern_state s = - unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s); - Library.overwrite_library_filenames s - (* Rollback. *) let with_state_protection f x = diff --git a/library/states.mli b/library/states.mli index c4f3eae49d..4870f48fc3 100644 --- a/library/states.mli +++ b/library/states.mli @@ -15,9 +15,6 @@ freezing the states of both [Lib] and [Summary]. We provide functions to write and restore state to and from a given file. *) -val intern_state : string -> unit -val extern_state : string -> unit - type state val freeze : marshallable:bool -> state val unfreeze : state -> unit |