From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 2 Aug 2002 17:17:42 +0000 Subject: Modules dans COQ\!\!\!\! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 179 ++++++++------ library/declare.mli | 20 +- library/declaremods.ml | 630 ++++++++++++++++++++++++++++++++++++++++++++++++ library/declaremods.mli | 85 +++++++ library/global.ml | 85 ++++++- library/global.mli | 67 ++++- library/goptions.ml | 41 ++-- library/goptions.mli | 2 + library/impargs.ml | 130 +++++----- library/impargs.mli | 1 + library/lib.ml | 447 ++++++++++++++++++++++++++-------- library/lib.mli | 107 ++++++-- library/libnames.ml | 212 ++++++++++++++++ library/libnames.mli | 118 +++++++++ library/libobject.ml | 98 ++++++-- library/libobject.mli | 93 +++++-- library/library.ml | 502 +++++++++++++++++++------------------- library/library.mli | 68 +++--- library/nameops.ml | 85 +------ library/nameops.mli | 36 +-- library/nametab.ml | 409 +++++++++++++++++-------------- library/nametab.mli | 111 +++++---- library/summary.ml | 22 +- library/summary.mli | 3 + 24 files changed, 2596 insertions(+), 955 deletions(-) create mode 100644 library/declaremods.ml create mode 100644 library/declaremods.mli create mode 100644 library/libnames.ml create mode 100644 library/libnames.mli (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index fc80cfda9..31af6dbbb 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -11,10 +11,12 @@ open Pp open Util open Names +open Libnames open Nameops open Term open Sign open Declarations +open Entries open Inductive open Indtypes open Reduction @@ -91,7 +93,7 @@ let _ = Summary.declare_summary "VARIABLE" Summary.init_function = (fun () -> vartab := Idmap.empty); Summary.survive_section = false } -let cache_variable (sp,(id,(p,d,strength))) = +let cache_variable ((sp,_),(id,(p,d,strength))) = (* Constr raisonne sur les noms courts *) if Idmap.mem id !vartab then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); @@ -100,17 +102,13 @@ let cache_variable (sp,(id,(p,d,strength))) = | SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in let vd = (bd,ty,cst) in - Nametab.push 0 (restrict_path 0 sp) (VarRef id); + Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); vartab := Idmap.add id (p,vd,strength) !vartab let (in_variable, out_variable) = - let od = { + declare_object { (default_object "VARIABLE") with cache_function = cache_variable; - load_function = (fun _ -> ()); - open_function = (fun _ -> ()); - export_function = (fun x -> Some x) } - in - declare_object ("VARIABLE", od) + classify_function = (fun _ -> Dispose) } let declare_variable id obj = let sp = add_leaf id (in_variable (id,obj)) in @@ -119,7 +117,7 @@ let declare_variable id obj = (* Globals: constants and parameters *) -type constant_declaration = global_declaration * strength +type constant_declaration = constant_entry * strength let csttab = ref (Spmap.empty : strength Spmap.t) @@ -129,90 +127,101 @@ let _ = Summary.declare_summary "CONSTANT" Summary.init_function = (fun () -> csttab := Spmap.empty); Summary.survive_section = false } -let cache_constant (sp,(cdt,stre)) = +let cache_constant ((sp,kn),(cdt,stre)) = (if Idmap.mem (basename sp) !vartab then errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists")); (if Nametab.exists_cci sp then let (_,id) = repr_path sp in errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - Global.add_constant sp cdt; + let _,dir,_ = repr_kn kn in + let kn' = Global.add_constant dir (basename sp) cdt in + if kn' <> kn then + anomaly "Kernel and Library names do not match"; (match stre with | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) -> (* Only qualifications including the sections segment from the current section to the discharge section is available for Remark & Fact *) - Nametab.push (n-Lib.sections_depth()) sp (ConstRef sp) + Nametab.push (Nametab.Until ((*n-Lib.sections_depth()+*)1)) sp (ConstRef kn) | (NeverDischarge| DischargeAt _) -> (* All qualifications of Theorem, Lemma & Definition are visible *) - Nametab.push 0 sp (ConstRef sp) + Nametab.push (Nametab.Until 1) sp (ConstRef kn) | NotDeclare -> assert false); csttab := Spmap.add sp stre !csttab (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant (sp,(ce,stre)) = +let load_constant i ((sp,kn),(ce,stre)) = (if Nametab.exists_cci sp then let (_,id) = repr_path sp in errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); csttab := Spmap.add sp stre !csttab; - Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp) + Nametab.push (Nametab.Until ((*depth_of_strength stre + *)i)) sp (ConstRef kn) (* Opening means making the name without its module qualification available *) -let open_constant (sp,(_,stre)) = +let open_constant i ((sp,kn),(_,stre)) = let n = depth_of_strength stre in - Nametab.push n (restrict_path n sp) (ConstRef sp) + Nametab.push (Nametab.Exactly (i(*+n*))) sp (ConstRef kn) (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ParameterEntry mkProp +let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) + +let dummy_constant (ce,stre) = dummy_constant_entry,stre -let export_constant (ce,stre) = Some (dummy_constant_entry,stre) +let export_constant cst = Some (dummy_constant cst) + +let classify_constant (_,cst) = Substitute (dummy_constant cst) let (in_constant, out_constant) = - let od = { + declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; + classify_function = classify_constant; + subst_function = ident_subst_function; export_function = export_constant } - in - declare_object ("CONSTANT", od) let hcons_constant_declaration = function - | (ConstantEntry ce, stre) -> - (ConstantEntry + | (DefinitionEntry ce, stre) -> + (DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = option_app hcons1_constr ce.const_entry_type; const_entry_opaque = ce.const_entry_opaque }, stre) | cd -> cd -let declare_constant id cd = +let declare_constant id (cd,stre) = (* let cd = hcons_constant_declaration cd in *) - let sp = add_leaf id (in_constant cd) in - if is_implicit_args() then declare_constant_implicits sp; - sp + let oname = add_leaf id (in_constant (ConstantEntry cd,stre)) in + if is_implicit_args() then declare_constant_implicits (snd oname); + oname -let redeclare_constant sp (cd,stre) = - add_absolutely_named_leaf sp (in_constant (GlobalRecipe cd,stre)); - if is_implicit_args() then declare_constant_implicits sp +let redeclare_constant id (cd,stre) = + let _,kn = add_leaf id (in_constant (GlobalRecipe cd,stre)) in + if is_implicit_args() then declare_constant_implicits kn (* Inductives. *) -let inductive_names sp mie = +let inductive_names sp kn mie = let (dp,_) = repr_path sp in let names, _ = List.fold_left (fun (names, n) ind -> - let indsp = (sp,n) in + let ind_p = (kn,n) in let names, _ = List.fold_left - (fun (names, p) id -> - let sp = Names.make_path dp id in - ((sp, ConstructRef (indsp,p)) :: names, p+1)) + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, ConstructRef (ind_p,p)) :: names, p+1)) (names, 1) ind.mind_entry_consnames in - let sp = Names.make_path dp ind.mind_entry_typename in - ((sp, IndRef indsp) :: names, n+1)) + let sp = Libnames.make_path dp ind.mind_entry_typename + in + ((sp, IndRef ind_p) :: names, n+1)) ([], 0) mie.mind_entry_inds in names + let check_exists_inductive (sp,_) = (if Idmap.mem (basename sp) !vartab then errorlabstrm "cache_inductive" @@ -221,22 +230,27 @@ let check_exists_inductive (sp,_) = let (_,id) = repr_path sp in errorlabstrm "cache_inductive" (pr_id id ++ str " already exists") -let cache_inductive (sp,mie) = - let names = inductive_names sp mie in +let cache_inductive ((sp,kn),mie) = + let names = inductive_names sp kn mie in List.iter check_exists_inductive names; - Global.add_mind sp mie; + let _,dir,_ = repr_kn kn in + let kn' = Global.add_mind dir (basename sp) mie in + if kn' <> kn then + anomaly "Kernel and Library names do not match"; + List.iter - (fun (sp, ref) -> Nametab.push 0 sp ref) + (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let load_inductive (sp,mie) = - let names = inductive_names sp mie in +let load_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in List.iter check_exists_inductive names; - List.iter (fun (sp, ref) -> Nametab.push 1 sp ref) names + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names -let open_inductive (sp,mie) = - let names = inductive_names sp mie in - List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names +let open_inductive i ((sp,kn),mie) = + let names = inductive_names sp kn mie in +(* List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names*) + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names let dummy_one_inductive_entry mie = { mind_entry_params = []; @@ -254,28 +268,28 @@ let dummy_inductive_entry m = { let export_inductive x = Some (dummy_inductive_entry x) let (in_inductive, out_inductive) = - let od = { + declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; + classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); + subst_function = ident_subst_function; export_function = export_inductive } - in - declare_object ("INDUCTIVE", od) let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in - let sp = add_leaf id (in_inductive mie) in - if is_implicit_args() then declare_mib_implicits sp; - sp + let oname = add_leaf id (in_inductive mie) in + if is_implicit_args() then declare_mib_implicits (snd oname); + oname (*s Test and access functions. *) let is_constant sp = - try let _ = Global.lookup_constant sp in true with Not_found -> false + try let _ = Spmap.find sp !csttab in true with Not_found -> false let constant_strength sp = Spmap.find sp !csttab @@ -291,7 +305,7 @@ let variable_strength id = let (_,_,str) = Idmap.find id !vartab in str let find_section_variable id = - let (p,_,_) = Idmap.find id !vartab in Names.make_path p id + let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id (* Global references. *) @@ -353,12 +367,14 @@ let construct_qualified_reference qid = let ref = Nametab.locate qid in constr_of_reference ref -let construct_reference env id = - try - mkVar (let _ = Environ.lookup_named id env in id) - with Not_found -> - let ref = Nametab.sp_of_id id in - constr_of_reference ref +let construct_reference ctx_opt id = + match ctx_opt with + | None -> construct_qualified_reference (make_short_qualid id) + | Some ctx -> + try + mkVar (let _ = Sign.lookup_named id ctx in id) + with Not_found -> + construct_qualified_reference (make_short_qualid id) let global_qualified_reference qid = construct_qualified_reference qid @@ -370,36 +386,42 @@ let global_reference_in_absolute_module dir id = constr_of_reference (Nametab.locate_in_absolute_module dir id) let global_reference id = - construct_reference (Global.env()) id - -let dirpath sp = let (p,_) = repr_path sp in p - -let dirpath_of_global = function - | VarRef id -> empty_dirpath - | ConstRef sp -> dirpath sp - | IndRef (sp,_) -> dirpath sp - | ConstructRef ((sp,_),_) -> dirpath sp + construct_qualified_reference (make_short_qualid id) let is_section_variable = function | VarRef _ -> true | _ -> false +(* TODO temporary hack!!! *) +let rec is_imported_modpath = function + | MPfile dp -> dp <> (Lib.module_dp ()) +(* | MPdot (mp,_) -> is_imported_modpath mp *) + | _ -> false + +let is_imported_ref = function + | VarRef _ -> false + | ConstRef kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) +(* | ModTypeRef ln *) -> + let (mp,_,_) = repr_kn kn in is_imported_modpath mp +(* | ModRef mp -> + is_imported_modpath mp +*) let is_global id = try - let osp = Nametab.locate (make_short_qualid id) in - (* Compatibilité V6.3: Les variables de section ne sont pas globales - not (is_section_variable osp) && *) - is_dirpath_prefix_of (dirpath_of_global osp) (Lib.cwd()) + let ref = Nametab.locate (make_short_qualid id) in + not (is_imported_ref ref) with Not_found -> false -let strength_of_global = function - | ConstRef sp -> constant_strength sp +let strength_of_global ref = match ref with + | ConstRef kn -> constant_strength (full_name ref) | VarRef id -> variable_strength id | IndRef _ | ConstructRef _ -> NeverDischarge let library_part ref = - let sp = Nametab.sp_of_global (Global.env ()) ref in + let sp = Nametab.sp_of_global None ref in let dir,_ = repr_path sp in match strength_of_global ref with | DischargeAt (dp,n) -> @@ -412,3 +434,4 @@ let library_part ref = (* Theorem/Lemma outside its outer section of definition *) dir | NotDeclare -> assert false + diff --git a/library/declare.mli b/library/declare.mli index 07b9d98b6..273a2b344 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -10,9 +10,11 @@ (*i*) open Names +open Libnames open Term open Sign open Declarations +open Entries open Indtypes open Safe_typing open Library @@ -34,16 +36,16 @@ type section_variable_entry = type variable_declaration = dir_path * section_variable_entry * strength -val declare_variable : variable -> variable_declaration -> section_path +val declare_variable : variable -> variable_declaration -> object_name -type constant_declaration = global_declaration * strength +type constant_declaration = constant_entry * strength (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> constant +val declare_constant : identifier -> constant_declaration -> object_name -val redeclare_constant : constant -> Cooking.recipe * strength -> unit +val redeclare_constant : identifier -> Cooking.recipe * strength -> unit (* val declare_parameter : identifier -> constr -> constant @@ -52,7 +54,7 @@ val declare_parameter : identifier -> constr -> constant (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block *) -val declare_mind : mutual_inductive_entry -> mutual_inductive +val declare_mind : mutual_inductive_entry -> object_name val out_inductive : Libobject.obj -> mutual_inductive_entry @@ -65,7 +67,7 @@ val strength_min : strength * strength -> strength (*s Corresponding test and access functions. *) val is_constant : section_path -> bool -val constant_strength : constant -> strength +val constant_strength : section_path -> strength val out_variable : Libobject.obj -> identifier * variable_declaration val get_variable : variable -> named_declaration * strength @@ -86,11 +88,11 @@ val constr_of_reference : global_reference -> constr raise [Not_found] if not a global *) val reference_of_constr : constr -> global_reference -val global_qualified_reference : Nametab.qualid -> constr +val global_qualified_reference : qualid -> constr val global_absolute_reference : section_path -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -val construct_qualified_reference : Nametab.qualid -> constr +val construct_qualified_reference : qualid -> constr val construct_absolute_reference : section_path -> constr (* This should eventually disappear *) @@ -98,7 +100,7 @@ val construct_absolute_reference : section_path -> constr the name [id] in the global environment. It looks also for variables in a given environment instead of looking in the current global environment. *) val global_reference : identifier -> constr -val construct_reference : Environ.env -> identifier -> constr +val construct_reference : Sign.named_context option -> identifier -> constr val is_global : identifier -> bool diff --git a/library/declaremods.ml b/library/declaremods.ml new file mode 100644 index 000000000..76ed46619 --- /dev/null +++ b/library/declaremods.ml @@ -0,0 +1,630 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + !modtab_substobjs, + !modtab_objects, + !openmod_info); + Summary.unfreeze_function = (fun (sobjs,objs,info) -> + modtab_substobjs := sobjs; + modtab_objects := objs; + openmod_info := info); + Summary.init_function = (fun () -> + modtab_substobjs := MPmap.empty; + modtab_objects := MPmap.empty; + openmod_info := ([],None)); + Summary.survive_section = false } + +(* auxiliary functions to transform section_path and kernel_name given + by Lib into module_path and dir_path needed for modules *) + +let mp_of_kn kn = + let mp,sec,l = repr_kn kn in + if sec=empty_dirpath then + MPdot (mp,l) + else + anomaly ("Non-empty section in module name!" ^ string_of_kn kn) + +let dir_of_sp sp = + let dir,id = repr_path sp in + extend_dirpath dir id + +let msid_of_mp = function + MPself msid -> msid + | _ -> anomaly "'Self' module path expected!" + +let msid_of_prefix (_,(mp,sec)) = + if sec=empty_dirpath then + msid_of_mp mp + else + anomaly ("Non-empty section in module name!" ^ + string_of_mp mp ^ "." ^ string_of_dirpath sec) + +(* This function registers the visibility of the module and iterates + through its components. It is called by plenty module functions *) + +let do_module exists what iter_objects i dir mp substobjs objects = + let prefix = (dir,(mp,empty_dirpath)) in + let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let vis = + if exists then + if + try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo + with Not_found -> false + then + Nametab.Exactly i + else + errorlabstrm (what^"_module") + (pr_dirpath dir ++ str " should already exist!") + else + if Nametab.exists_dir dir then + errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") + else + Nametab.Until i + in + Nametab.push_dir vis dir dirinfo; + modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; + match objects with + Some seg -> + modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects; + iter_objects (i+1) prefix seg + | None -> () + + +let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted = + let dir,mp = dir_of_sp sp, mp_of_kn kn in + do_module exists what iter_objects i dir mp substobjs substituted + +(* Interactive modules and module types cannot be recached! cache_mod* + functions can be called only once (and "end_mod*" set the flag to + false then) +*) + +let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = + let _ = match entry with + | None -> + anomaly "You must not recache interactive modules!" + | Some me -> + let mp = Global.add_module (basename sp) me in + if mp <> mp_of_kn kn then + anomaly "Kernel and Library names do not match" + in + conv_names_do_module false "cache" load_objects 1 oname substobjs substituted + + +(* TODO: This check is not essential *) +let check_empty s = function + | None -> () + | Some _ -> + anomaly ("We should never have full info in " ^ s^"!") + + +(* When this function is called the module itself is already in the + environment. This function loads its objects only *) + +let load_module i (oname,(entry,substobjs,substituted)) = + (* TODO: This check is not essential *) + check_empty "load_module" entry; + conv_names_do_module false "load" load_objects i oname substobjs substituted + + +let open_module i (oname,(entry,substobjs,substituted)) = + (* TODO: This check is not essential *) + check_empty "open_module" entry; + conv_names_do_module true "open" open_objects i oname substobjs substituted + + +let subst_substobjs dir mp (subst,mbids,msid,objs) = + match mbids with + | [] -> + let prefix = dir,(mp,empty_dirpath) in + Some (subst_objects prefix (add_msid msid mp subst) objs) + | _ -> None + + +let subst_module ((sp,kn),subst,(entry,substobjs,_)) = + check_empty "subst_module" entry; + let dir,mp = dir_of_sp sp, mp_of_kn kn in + let (sub,mbids,msid,objs) = substobjs in + let subst' = join sub subst in + (* substitutive_objects get the new substitution *) + let substobjs = (subst',mbids,msid,objs) in + (* if we are not a functor - calculate substitued. + We add "msid |-> mp" to the substitution *) + let substituted = subst_substobjs dir mp substobjs + in + (None,substobjs,substituted) + + +let classify_module (_,(_,substobjs,_)) = + Substitute (None,substobjs,None) + +let (in_module,out_module) = + declare_object {(default_object "MODULE") with + cache_function = cache_module; + load_function = load_module; + open_function = open_module; + subst_function = subst_module; + classify_function = classify_module; + export_function = (fun _ -> anomaly "No modules in sections!") } + + +let cache_keep _ = anomaly "This module should not be cached!" + +let load_keep i ((sp,kn),seg) = + let mp = mp_of_kn kn in + let prefix = dir_of_sp sp, (mp,empty_dirpath) in + begin + try + let prefix',objects = MPmap.find mp !modtab_objects in + if prefix' <> prefix then + anomaly "Two different modules with the same path!"; + modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects; + with + Not_found -> anomaly "Keep objects before substitutive" + end; + load_objects i prefix seg + +let open_keep i ((sp,kn),seg) = + let dirpath,mp = dir_of_sp sp, mp_of_kn kn in + open_objects i (dirpath,(mp,empty_dirpath)) seg + +let (in_modkeep,out_modkeep) = + declare_object {(default_object "MODULE KEEP OBJECTS") with + cache_function = cache_keep; + load_function = load_keep; + open_function = open_keep; + export_function = (fun _ -> anomaly "No modules in sections!") } + +(* we remember objects for a module type. In case of a declaration: + Module M:SIG:=... + The module M gets its objects from SIG +*) +let modtypetab = + ref (KNmap.empty : substitutive_objects KNmap.t) + +(* currently started interactive module type. We remember its arguments + if it is a functor type *) +let openmodtype_info = + ref ([] : mod_bound_id list) + +let _ = Summary.declare_summary "MODTYPE-INFO" + { Summary.freeze_function = (fun () -> + !modtypetab,!openmodtype_info); + Summary.unfreeze_function = (fun ft -> + modtypetab := fst ft; + openmodtype_info := snd ft); + Summary.init_function = (fun () -> + modtypetab := KNmap.empty; + openmodtype_info := []); + Summary.survive_section = true } + + + + +let cache_modtype ((sp,kn),(entry,modtypeobjs)) = + let _ = + match entry with + | None -> + anomaly "You must not recache interactive module types!" + | Some mte -> + let kn' = Global.add_modtype (basename sp) mte in + if kn' <> kn then + anomaly "Kernel and Library names do not match" + in + + if Nametab.exists_modtype sp then + errorlabstrm "cache_modtype" + (pr_sp sp ++ str " already exists") ; + + Nametab.push_modtype (Nametab.Until 1) sp kn; + + modtypetab := KNmap.add kn modtypeobjs !modtypetab + + +let load_modtype i ((sp,kn),(entry,modtypeobjs)) = + check_empty "load_modtype" entry; + + if Nametab.exists_modtype sp then + errorlabstrm "cache_modtype" + (pr_sp sp ++ str " already exists") ; + + Nametab.push_modtype (Nametab.Until i) sp kn; + + modtypetab := KNmap.add kn modtypeobjs !modtypetab + + +let open_modtype i ((sp,kn),(entry,_)) = + check_empty "open_modtype" entry; + + if + try Nametab.locate_modtype (qualid_of_sp sp) <> kn + with Not_found -> true + then + errorlabstrm ("open_modtype") + (pr_sp sp ++ str " should already exist!"); + + Nametab.push_modtype (Nametab.Exactly i) sp kn + + +let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = + check_empty "subst_modtype" entry; + (entry,(join subs subst,mbids,msid,objs)) + + +let classify_modtype (_,(_,substobjs)) = + Substitute (None,substobjs) + + +let (in_modtype,out_modtype) = + declare_object {(default_object "MODULE TYPE") with + cache_function = cache_modtype; + load_function = load_modtype; + subst_function = subst_modtype; + classify_function = classify_modtype; + export_function = in_some } + + + +let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = + (subst, mbids1@mbids2, msid, lib_stack) + + +let rec get_modtype_substobjs = function + MTEident ln -> KNmap.find ln !modtypetab + | MTEfunsig (mbid,_,mte) -> + let (subst, mbids, msid, objs) = get_modtype_substobjs mte in + (subst, mbid::mbids, msid, objs) + | MTEsig (msid,_) -> (empty_subst, [], msid, []) + (* this is plainly wrong, but it is hard to do otherwise... *) + +(* push names of bound modules (and their components) to Nametab *) +(* add objects associated to them *) +let process_module_bindings argids args = + let process_arg id (mbid,mty) = + let dir = make_dirpath [id] in + let mp = MPbound mbid in + let substobjs = get_modtype_substobjs mty in + let substituted = subst_substobjs dir mp substobjs in + do_module false "begin" load_objects 1 dir mp substobjs substituted + in + List.iter2 process_arg argids args + +(* +(* this function removes keep objects from submodules *) +let rec kill_keep objs = + let kill = function + | (oname,Leaf obj) as node -> + if object_tag obj = "MODULE" then + let (entry,substobjs,substitute) = out_module obj in + match substitute,keep with + | [],[] -> node + | _ -> oname, Leaf (in_module (entry,(substobjs,[],[]))) + else + node + | _ -> anomaly "kill_keep expects Leafs only!" + in + match objs with + | [] -> objs + | h::tl -> let h'=kill h and tl'=kill_keep tl in + if h==h' && tl==tl' then + objs + else + h'::tl' +*) + +let start_module id argids args res_o = + let mp = Global.start_module (Lib.module_dp()) id args res_o in + let mbids = List.map fst args in + let fs = Summary.freeze_summaries () in + process_module_bindings argids args; + openmod_info:=(mbids,res_o); + Lib.start_module id mp fs; + Lib.add_frozen_state () + + +let end_module id = + + let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in + let mp = Global.end_module id in + let substitute, keep, special = Lib.classify_objects lib_stack in + + let dir = fst oldprefix in + let msid = msid_of_prefix oldprefix in + let mbids, res_o = !openmod_info in + + Summary.unfreeze_other_summaries fs; + + let substobjs = match res_o with + | None -> + empty_subst, mbids, msid, substitute + | Some (MTEident ln) -> + abstract_substobjs mbids (KNmap.find ln (!modtypetab)) + | Some (MTEsig (msid,_)) -> + todo "Anonymous signatures not supported"; + empty_subst, mbids, msid, [] + | Some (MTEfunsig _) -> + anomaly "Funsig cannot be here..." + in + let substituted = subst_substobjs dir mp substobjs in + let node = in_module (None,substobjs,substituted) in + let objects = + if keep = [] then + special@[node] + else + special@[node;in_modkeep keep] + in + let newoname = Lib.add_leaves id objects in + + if (fst newoname) <> (fst oldoname) then + anomaly "Names generated on start_ and end_module do not match"; + if mp_of_kn (snd newoname) <> mp then + anomaly "Kernel and Library names do not match"; + + Lib.add_frozen_state () (* to prevent recaching *) + + + +let module_objects mp = + let prefix,objects = MPmap.find mp !modtab_objects in + segment_of_objects prefix objects + + +type library_name = dir_path + +(* The first two will form a substitutive_objects, the last one is keep *) +type library_objects = + mod_self_id * lib_objects * lib_objects + + +(* The library_cache here is needed to avoid recalculations of + substituted modules object during "reloading" of libraries *) +let library_cache = Hashtbl.create 17 + + +let register_library dir cenv objs digest = + let mp = MPfile dir in + let prefix = dir, (mp, empty_dirpath) in + let substobjs, objects = + try + ignore(Global.lookup_module mp); + (* if it's in the environment, the cached objects should be correct *) + Hashtbl.find library_cache dir + with + Not_found -> + if mp <> Global.import cenv digest then + anomaly "Unexpected disk module name"; + let msid,substitute,keep = objs in + let substobjs = empty_subst, [], msid, substitute in + let substituted = subst_substobjs dir mp substobjs in + let objects = option_app (fun seg -> seg@keep) substituted in + let modobjs = substobjs, objects in + Hashtbl.add library_cache dir modobjs; + modobjs + in + do_module false "register_compilation" load_objects 1 dir mp substobjs objects + + +let start_library dir = + let mp = Global.start_library dir in + openmod_info:=[],None; + Lib.start_compilation dir mp; + Lib.add_frozen_state () + + +let export_library dir = + let cenv = Global.export dir in + let prefix, lib_stack = Lib.end_compilation dir in + let msid = msid_of_prefix prefix in + let substitute, keep, _ = Lib.classify_objects lib_stack in + cenv,(msid,substitute,keep) + + + +let import_module mp = + let prefix,objects = MPmap.find mp !modtab_objects in + open_objects 1 prefix objects + + +let start_modtype id argids args = + let mp = Global.start_modtype (Lib.module_dp()) id args in + let fs= Summary.freeze_summaries () in + process_module_bindings argids args; + openmodtype_info := (List.map fst args); + Lib.start_modtype id mp fs; + Lib.add_frozen_state () + + +let end_modtype id = + + let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in + let ln = Global.end_modtype id in + let substitute, _, special = Lib.classify_objects lib_stack in + + let msid = msid_of_prefix prefix in + let mbids = !openmodtype_info in + + Summary.unfreeze_other_summaries fs; + + let modtypeobjs = empty_subst, mbids, msid, substitute in + + let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in + if fst oname <> fst oldoname then + anomaly + "Section paths generated on start_ and end_modtype do not match"; + if snd oname <> ln then + anomaly + "Kernel and Library names do not match"; + + Lib.add_frozen_state ()(* to prevent recaching *) + + +let declare_modtype id mte = + let substobjs = get_modtype_substobjs mte in + ignore (add_leaf id (in_modtype (Some mte, substobjs))) + + + +let rec get_module_substobjs = function + MEident mp -> MPmap.find mp !modtab_substobjs + | MEfunctor (mbid,_,mexpr) -> + let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + (subst, mbid::mbids, msid, objs) + | MEstruct (msid,_) -> + (empty_subst, [], msid, []) + | MEapply (mexpr, MEident mp) -> + let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + (match mbids with + | mbid::mbids -> + (add_mbid mbid mp subst, mbids, msid, objs) + | [] -> anomaly "Too few arguments in functor") + | MEapply (_,_) -> + anomaly "The argument of a module application must be a path!" + + +let declare_module id me = + let substobjs = + match me with + | {mod_entry_type = Some mte} -> get_modtype_substobjs mte + | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr + | _ -> anomaly "declare_module: No type, no body ..." + in + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module (Some me, substobjs, substituted))) + + +(*s Iterators. *) + +let fold_all_segments insec f x = + let acc' = + MPmap.fold + (fun _ (prefix,objects) acc -> + let apply_obj acc (id,obj) = f acc (make_oname prefix id) obj in + List.fold_left apply_obj acc objects) + !modtab_objects x + in + let rec apply_node acc = function + | sp, Leaf o -> f acc sp o + | _, ClosedSection (_,_,seg) -> + if insec then List.fold_left apply_node acc seg else acc + | _ -> acc + in + List.fold_left apply_node acc' (Lib.contents_after None) + +let iter_all_segments insec f = + let _ = + MPmap.iter + (fun _ (prefix,objects) -> + let apply_obj (id,obj) = f (make_oname prefix id) obj in + List.iter apply_obj objects) + !modtab_objects + in + let rec apply_node = function + | sp, Leaf o -> f sp o + | _, ClosedSection (_,_,seg) -> if insec then List.iter apply_node seg + | _ -> () + in + List.iter apply_node (Lib.contents_after None) + + + +let debug_print_modtab _ = + let pr_seg = function + | [] -> str "[]" + | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") + in + let pr_modinfo mp (prefix,objects) s = + s ++ str (string_of_mp mp) ++ (spc ()) + ++ (pr_seg (segment_of_objects prefix objects)) + in + let modules = MPmap.fold pr_modinfo !modtab_objects (mt ()) in + hov 0 modules + + diff --git a/library/declaremods.mli b/library/declaremods.mli new file mode 100644 index 000000000..17db827e8 --- /dev/null +++ b/library/declaremods.mli @@ -0,0 +1,85 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* module_entry -> unit + +val start_module : + identifier -> identifier list -> (mod_bound_id * module_type_entry) list + -> module_type_entry option -> unit +val end_module : identifier -> unit + + + +(*s Module types *) + +val declare_modtype : identifier -> module_type_entry -> unit + +val start_modtype : + identifier -> identifier list -> (mod_bound_id * module_type_entry) list + -> unit +val end_modtype : identifier -> unit + + +(*s Objects of a module. They come in two lists: the substitutive ones + and the other *) + +val module_objects : module_path -> library_segment + + +(*s Libraries i.e. modules on disk *) + +type library_name = dir_path + +type library_objects + +val register_library : + library_name -> + Safe_typing.compiled_library -> library_objects -> Digest.t -> unit + +val start_library : library_name -> unit + +val export_library : + library_name -> Safe_typing.compiled_library * library_objects + + +(* [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. *) + +val import_module : module_path -> unit + + +(*s [fold_all_segments] and [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). The boolean indicates if we must enter closed sections. *) + +val fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a +val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit + + +val debug_print_modtab : unit -> Pp.std_ppcmds + +(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*) diff --git a/library/global.ml b/library/global.ml index db0e5f470..cdebc52f5 100644 --- a/library/global.ml +++ b/library/global.ml @@ -26,7 +26,7 @@ let safe_env () = !global_env let env () = env_of_safe_env !global_env let _ = - declare_summary "Global environment" + declare_global_environment { freeze_function = (fun () -> !global_env); unfreeze_function = (fun fr -> global_env := fr); init_function = (fun () -> global_env := empty_environment); @@ -46,17 +46,81 @@ let push_named_def d = global_env := env; cst -let add_constant sp ce = global_env := add_constant sp ce !global_env -let add_mind sp mie = global_env := add_mind sp mie !global_env +(*let add_thing add kn thing = + let _,dir,l = repr_kn kn in + let kn',newenv = add dir l thing !global_env in + if kn = kn' then + global_env := newenv + else + anomaly "Kernel names do not match." +*) + +let add_thing add dir id thing = + let kn, newenv = add dir (label_of_id id) thing !global_env in + global_env := newenv; + kn + +let add_constant = add_thing add_constant +let add_mind = add_thing add_mind +let add_modtype = add_thing (fun _ -> add_modtype) () +let add_module = add_thing (fun _ -> add_module) () + let add_constraints c = global_env := add_constraints c !global_env + + +let start_module dir id params mtyo = + let l = label_of_id id in + let mp,newenv = start_module dir l params mtyo !global_env in + global_env := newenv; + mp + +let end_module id = + let l = label_of_id id in + let mp,newenv = end_module l !global_env in + global_env := newenv; + mp + + +let start_modtype dir id params = + let l = label_of_id id in + let mp,newenv = start_modtype dir l params !global_env in + global_env := newenv; + mp + +let end_modtype id = + let l = label_of_id id in + let kn,newenv = end_modtype l !global_env in + global_env := newenv; + kn + + + + let lookup_named id = lookup_named id (env()) -let lookup_constant sp = lookup_constant sp (env()) +let lookup_constant kn = lookup_constant kn (env()) let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind -let lookup_mind sp = lookup_mind sp (env()) +let lookup_mind kn = lookup_mind kn (env()) + +let lookup_module mp = lookup_module mp (env()) +let lookup_modtype kn = lookup_modtype kn (env()) + + + + +let start_library dir = + let mp,newenv = start_library dir !global_env in + global_env := newenv; + mp + +let export s = snd (export !global_env s) + +let import cenv digest = + let mp,newenv = import cenv digest !global_env in + global_env := newenv; + mp + -let export s = export !global_env s -let import cenv = global_env := import cenv !global_env (*s Function to get an environment from the constants part of the global environment and a given context. *) @@ -64,7 +128,7 @@ let import cenv = global_env := import cenv !global_env let env_of_context hyps = reset_with_named_context hyps (env()) -open Nametab +open Libnames let type_of_reference env = function | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t @@ -73,3 +137,8 @@ let type_of_reference env = function | ConstructRef cstr -> Inductive.type_of_constructor env cstr let type_of_global t = type_of_reference (env ()) t + + +(*let get_kn dp l = + make_kn (current_modpath !global_env) dp l +*) diff --git a/library/global.mli b/library/global.mli index 48e90d12e..4a215167a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -13,13 +13,18 @@ open Names open Univ open Term open Declarations +open Entries open Indtypes open Safe_typing -(*i*) + (*i*) + +(* This module defines the global environment of Coq. The functions + below are exactly the same as the ones in [Safe_typing], operating on + that global environment. [add_*] functions perform name verification, + i.e. check that the name given as argument match those provided by + [Safe_typing]. *) + -(* This module defines the global environment of Coq. - The functions below are exactly the same as the ones in [Typing], - operating on that global environment. *) val safe_env : unit -> safe_environment val env : unit -> Environ.env @@ -27,26 +32,62 @@ val env : unit -> Environ.env val universes : unit -> universes val named_context : unit -> Sign.named_context -(* Extending env with variables, constants and inductives *) +(*s Extending env with variables and local definitions *) val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints -val add_constant : constant -> global_declaration -> unit -val add_mind : mutual_inductive -> mutual_inductive_entry -> unit +(*s Adding constants, inductives, modules and module types. All these + functions verify that given names match those generated by kernel *) + +val add_constant : + dir_path -> identifier -> global_declaration -> kernel_name +val add_mind : + dir_path -> identifier -> mutual_inductive_entry -> kernel_name + +val add_module : identifier -> module_entry -> module_path +val add_modtype : identifier -> module_type_entry -> kernel_name + val add_constraints : constraints -> unit +(*s Interactive modules and module types *) +(* Both [start_*] functions take the [dir_path] argument to create a + [mod_self_id]. This should be the name of the compilation unit. *) + +(* [start_*] functions return the [module_path] valid for components + of the started module / module type *) + +val start_module : + dir_path -> identifier -> (mod_bound_id * module_type_entry) list + -> module_type_entry option + -> module_path + +val end_module : + identifier -> module_path + +val start_modtype : + dir_path -> identifier -> (mod_bound_id * module_type_entry) list + -> module_path + +val end_modtype : + identifier -> kernel_name + + (* Queries *) val lookup_named : variable -> named_declaration val lookup_constant : constant -> constant_body val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body val lookup_mind : mutual_inductive -> mutual_inductive_body +val lookup_module : module_path -> module_body +val lookup_modtype : kernel_name -> module_type_body -(* Modules *) -val export : dir_path -> Environ.compiled_env -val import : Environ.compiled_env -> unit +(* Compiled modules *) +val start_library : dir_path -> module_path +val export : dir_path -> compiled_library +val import : compiled_library -> Digest.t -> module_path (*s Function to get an environment from the constants part of the global - environment and a given context. *) - -val type_of_global : Nametab.global_reference -> types + * environment and a given context. *) + +val type_of_global : Libnames.global_reference -> types val env_of_context : Sign.named_context -> Environ.env + diff --git a/library/goptions.ml b/library/goptions.ml index b4056472b..4d505b5aa 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -14,6 +14,7 @@ open Pp open Util open Libobject open Names +open Libnames open Term open Nametab @@ -55,6 +56,7 @@ module MakeTable = type key val table : (string * key table_of_A) list ref val encode : key -> t + val subst : substitution -> t -> t val printer : t -> std_ppcmds val key : option_name val title : string @@ -66,10 +68,10 @@ module MakeTable = | GOadd | GOrmv - let kn = nickname A.key + let nick = nickname A.key let _ = - if List.mem_assoc kn !A.table then + if List.mem_assoc nick !A.table then error "Sorry, this table name is already used" module MyType = struct type t = A.t let compare = Pervasives.compare end @@ -82,7 +84,7 @@ module MakeTable = let freeze () = !t in let unfreeze c = t := c in let init () = t := MySet.empty in - Summary.declare_summary kn + Summary.declare_summary nick { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; Summary.init_function = init; @@ -90,17 +92,25 @@ module MakeTable = let (add_option,remove_option) = if A.synchronous then - let load_options _ = () in let cache_options (_,(f,p)) = match f with | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in - let export_options fp = Some fp in + let load_options i o = if 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 export_options fp = Some fp in let (inGo,outGo) = - Libobject.declare_object (kn, - { Libobject.load_function = load_options; - Libobject.open_function = cache_options; + Libobject.declare_object {(Libobject.default_object nick) with + Libobject.load_function = load_options; + Libobject.open_function = load_options; Libobject.cache_function = cache_options; - Libobject.export_function = export_options}) in + Libobject.subst_function = subst_options; + Libobject.classify_function = (fun (_,x) -> Substitute x); + Libobject.export_function = export_options} + in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) else @@ -126,7 +136,7 @@ module MakeTable = method print = print_table A.title A.printer !t end - let _ = A.table := (kn,new table_of_A ())::!A.table + let _ = A.table := (nick,new table_of_A ())::!A.table let active c = MySet.mem c !t let elements () = MySet.elements !t end @@ -149,6 +159,7 @@ struct type key = string let table = string_table let encode x = x + let subst _ x = x let printer = str let key = A.key let title = A.title @@ -167,6 +178,7 @@ module type RefConvertArg = sig type t val encode : qualid located -> t + val subst : substitution -> t -> t val printer : t -> std_ppcmds val key : option_name val title : string @@ -180,6 +192,7 @@ struct type key = qualid located let table = ref_table let encode = A.encode + let subst = A.subst let printer = A.printer let key = A.key let title = A.title @@ -228,11 +241,9 @@ let declare_option cast uncast check_key key; let write = if sync then let (decl_obj,_) = - declare_object ((nickname key), - {load_function = (fun _ -> ()); - open_function = (fun _ -> ()); + declare_object {(default_object (nickname key)) with cache_function = (fun (_,v) -> write v); - export_function = (fun x -> None)}) + classify_function = (fun _ -> Dispose)} in let _ = declare_summary (nickname key) {freeze_function = read; @@ -298,7 +309,7 @@ let msg_option_value (name,v) = | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s - | IdentValue r -> pr_global_env (Global.env()) r + | IdentValue r -> pr_global_env None r let print_option_value key = let (name,(_,read,_)) = get_option key in diff --git a/library/goptions.mli b/library/goptions.mli index d43a4283e..28da69ea6 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -56,6 +56,7 @@ open Pp open Util open Names +open Libnames open Term open Nametab (*i*) @@ -107,6 +108,7 @@ module MakeRefTable : (A : sig type t val encode : qualid located -> t + val subst : substitution -> t -> t val printer : t -> std_ppcmds val key : option_name val title : string diff --git a/library/impargs.ml b/library/impargs.ml index af6bfd6b7..14a93123b 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -10,6 +10,7 @@ open Util open Names +open Libnames open Term open Reduction open Declarations @@ -92,31 +93,35 @@ let list_of_implicits = function (*s Constants. *) -let constants_table = ref Spmap.empty +let constants_table = ref KNmap.empty -let compute_constant_implicits sp = +let compute_constant_implicits kn = let env = Global.env () in - let cb = lookup_constant sp env in + let cb = lookup_constant kn env in auto_implicits env (body_of_type cb.const_type) -let cache_constant_implicits (_,(sp,imps)) = - constants_table := Spmap.add sp imps !constants_table +let cache_constant_implicits (_,(kn,imps)) = + constants_table := KNmap.add kn imps !constants_table + +let subst_constant_implicits (_,subst,(kn,imps as obj)) = + let kn' = subst_kn subst kn in + if kn' == kn then obj else + kn',imps let (in_constant_implicits, _) = - let od = { + declare_object {(default_object "CONSTANT-IMPLICITS") with cache_function = cache_constant_implicits; - load_function = cache_constant_implicits; - open_function = (fun _ -> ()); + load_function = (fun _ -> cache_constant_implicits); + subst_function = subst_constant_implicits; + classify_function = (fun (_,x) -> Substitute x); export_function = (fun x -> Some x) } - in - declare_object ("CONSTANT-IMPLICITS", od) -let declare_constant_implicits sp = - let imps = compute_constant_implicits sp in - add_anonymous_leaf (in_constant_implicits (sp,imps)) +let declare_constant_implicits kn = + let imps = compute_constant_implicits kn in + add_anonymous_leaf (in_constant_implicits (kn,imps)) let constant_implicits sp = - try Spmap.find sp !constants_table with Not_found -> No_impl + try KNmap.find sp !constants_table with Not_found -> No_impl let constant_implicits_list sp = list_of_implicits (constant_implicits sp) @@ -151,30 +156,40 @@ let constructors_table = ref Constrmap.empty let cache_inductive_implicits (_,(indp,imps)) = inductives_table := Indmap.add indp imps !inductives_table +let subst_inductive_implicits (_,subst,((kn,i),imps as obj)) = + let kn' = subst_kn subst kn in + if kn' == kn then obj else + (kn',i),imps + let (in_inductive_implicits, _) = - let od = { + declare_object {(default_object "INDUCTIVE-IMPLICITS") with cache_function = cache_inductive_implicits; - load_function = cache_inductive_implicits; - open_function = (fun _ -> ()); - export_function = (fun x -> Some x) } - in - declare_object ("INDUCTIVE-IMPLICITS", od) + load_function = (fun _ -> cache_inductive_implicits); + subst_function = subst_inductive_implicits; + classify_function = (fun (_,x) -> Substitute x); + export_function = (fun x -> Some x) } let cache_constructor_implicits (_,(consp,imps)) = constructors_table := Constrmap.add consp imps !constructors_table +let subst_constructor_implicits (_,subst,(((kn,i),j),imps as obj)) = + let kn' = subst_kn subst kn in + if kn' == kn then obj else + ((kn',i),j),imps + + let (in_constructor_implicits, _) = - let od = { + declare_object {(default_object "CONSTRUCTOR-IMPLICITS") with cache_function = cache_constructor_implicits; - load_function = cache_constructor_implicits; - open_function = (fun _ -> ()); - export_function = (fun x -> Some x) } - in - declare_object ("CONSTRUCTOR-IMPLICITS", od) + load_function = (fun _ -> cache_constructor_implicits); + subst_function = subst_constructor_implicits; + classify_function = (fun (_,x) -> Substitute x); + export_function = (fun x -> Some x) } -let compute_mib_implicits sp = + +let compute_mib_implicits kn = let env = Global.env () in - let mib = lookup_mind sp env in + let mib = lookup_mind kn env in let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) @@ -188,10 +203,10 @@ let compute_mib_implicits sp = in Array.map imps_one_inductive mib.mind_packets -let cache_mib_implicits (_,(sp,mibimps)) = +let cache_mib_implicits (_,(kn,mibimps)) = Array.iteri (fun i (imps,v) -> - let indp = (sp,i) in + let indp = (kn,i) in inductives_table := Indmap.add indp imps !inductives_table; Array.iteri (fun j imps -> @@ -199,18 +214,22 @@ let cache_mib_implicits (_,(sp,mibimps)) = Constrmap.add (indp,succ j) imps !constructors_table) v) mibimps +let subst_mib_implicits (_,subst,(kn,mibimps as obj)) = + let kn' = subst_kn subst kn in + if kn' == kn then obj else + kn',mibimps + let (in_mib_implicits, _) = - let od = { + declare_object {(default_object "MIB-IMPLICITS") with cache_function = cache_mib_implicits; - load_function = cache_mib_implicits; - open_function = (fun _ -> ()); - export_function = (fun x -> Some x) } - in - declare_object ("MIB-IMPLICITS", od) + load_function = (fun _ -> cache_mib_implicits); + subst_function = subst_mib_implicits; + classify_function = (fun (_,x) -> Substitute x); + export_function = (fun x -> Some x) } -let declare_mib_implicits sp = - let imps = compute_mib_implicits sp in - add_anonymous_leaf (in_mib_implicits (sp,imps)) +let declare_mib_implicits kn = + let imps = compute_mib_implicits kn in + add_anonymous_leaf (in_mib_implicits (kn,imps)) let inductive_implicits indp = try Indmap.find indp !inductives_table with Not_found -> No_impl @@ -237,13 +256,12 @@ let cache_var_implicits (_,(id,imps)) = var_table := Idmap.add id imps !var_table let (in_var_implicits, _) = - let od = { + declare_object {(default_object "VARIABLE-IMPLICITS") with cache_function = cache_var_implicits; - load_function = cache_var_implicits; - open_function = (fun _ -> ()); - export_function = (fun x -> Some x) } - in - declare_object ("VARIABLE-IMPLICITS", od) + load_function = (fun _ -> cache_var_implicits); + export_function = (fun x -> Some x) } + + let declare_var_implicits id = let imps = compute_var_implicits id in @@ -255,16 +273,16 @@ let implicits_of_var id = (*s Implicits of a global reference. *) let declare_implicits = function - | VarRef sp -> - declare_var_implicits sp - | ConstRef sp -> - declare_constant_implicits sp - | IndRef ((sp,i) as indp) -> - let mib_imps = compute_mib_implicits sp in + | VarRef id -> + declare_var_implicits id + | ConstRef kn -> + declare_constant_implicits kn + | IndRef ((kn,i) as indp) -> + let mib_imps = compute_mib_implicits kn in let imps = fst mib_imps.(i) in add_anonymous_leaf (in_inductive_implicits (indp, imps)) - | ConstructRef (((sp,i),j) as consp) -> - let mib_imps = compute_mib_implicits sp in + | ConstructRef (((kn,i),j) as consp) -> + let mib_imps = compute_mib_implicits kn in let imps = (snd mib_imps.(i)).(j-1) in add_anonymous_leaf (in_constructor_implicits (consp, imps)) @@ -296,7 +314,7 @@ let declare_manual_implicits r l = (*s Tests if declared implicit *) let is_implicit_constant sp = - try let _ = Spmap.find sp !constants_table in true with Not_found -> false + try let _ = KNmap.find sp !constants_table in true with Not_found -> false let is_implicit_inductive_definition indp = try let _ = Indmap.find indp !inductives_table in true @@ -313,13 +331,13 @@ let implicits_of_global = function (*s Registration as global tables and rollback. *) -type frozen_t = implicits Spmap.t +type frozen_t = implicits KNmap.t * implicits Indmap.t * implicits Constrmap.t * implicits Idmap.t let init () = - constants_table := Spmap.empty; + constants_table := KNmap.empty; inductives_table := Indmap.empty; constructors_table := Constrmap.empty; var_table := Idmap.empty diff --git a/library/impargs.mli b/library/impargs.mli index 022a38230..751d96844 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Term open Environ open Nametab diff --git a/library/lib.ml b/library/lib.ml index 8eaba772e..286133305 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -11,23 +11,102 @@ open Pp open Util open Names +open Libnames open Nameops open Libobject open Summary + type node = | Leaf of obj - | Module of dir_path - | OpenedSection of dir_path * Summary.frozen + | CompilingModule of object_prefix + | OpenedModule of object_prefix * Summary.frozen + | OpenedModtype of object_prefix * Summary.frozen + | OpenedSection of object_prefix * Summary.frozen (* bool is to tell if the section must be opened automatically *) | ClosedSection of bool * dir_path * library_segment | FrozenState of Summary.frozen -and library_entry = section_path * node +and library_entry = object_name * node and library_segment = library_entry list +type lib_objects = (identifier * obj) list + +let rec iter_leaves f i seg = + match seg with + | [] -> () + | (oname ,Leaf obj)::segtl -> + f i (oname,obj); + iter_leaves f i segtl + | _ -> anomaly "We should have leaves only here" + + +let open_segment = iter_leaves open_object + +let load_segment = iter_leaves load_object + +let change_kns mp seg = + let subst_one = function + | ((sp,kn),(Leaf obj as lobj)) -> + let kn' = make_kn mp empty_dirpath (label kn) in + ((sp,kn'),lobj) + | _ -> anomaly "We should have leaves only here" + in + List.map subst_one seg + +let subst_segment (dirpath,(mp,dir)) subst seg = + let subst_one = function + | ((sp,kn),Leaf obj) -> + let sp' = make_path dirpath (basename sp) in + let kn' = make_kn mp dir (label kn) in + let oname' = sp',kn' in + let obj' = subst_object (oname',subst,obj) in + (oname', Leaf obj') + | _ -> anomaly "We should have leaves only here" + in + List.map subst_one seg + + +let iter_objects f i prefix = + List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) + +let load_objects = iter_objects load_object +let open_objects = iter_objects open_object + +let subst_objects prefix subst seg = + let subst_one = fun (id,obj as node) -> + let obj' = subst_object (make_oname prefix id, subst, obj) in + if obj' == obj then node else + (id, obj') + in + list_smartmap subst_one seg + +let classify_objects seg = + let rec clean ((substl,keepl,anticipl) as acc) = function + | (_,CompilingModule _) :: _ | [] -> acc + | ((sp,kn as oname),Leaf o) as node :: stk -> + let id = id_of_label (label kn) in + (match classify_object (oname,o) with + | Dispose -> clean acc stk + | Keep o' -> + clean (substl, (id,o')::keepl, anticipl) stk + | Substitute o' -> + clean ((id,o')::substl, keepl, anticipl) stk + | Anticipate o' -> + clean (substl, keepl, o'::anticipl) stk) + | (oname,ClosedSection _ as item) :: stk -> clean acc stk + | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedModule _) :: _ -> error "there are still opened modules" + | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,FrozenState _) :: stk -> clean acc stk + in + clean ([],[],[]) (List.rev seg) + + +let segment_of_objects prefix = + List.map (fun (id,obj) -> (make_oname prefix id, Leaf obj)) (* We keep trace of operations in the stack [lib_stk]. [path_prefix] is the current path of sections, where sections are stored in @@ -36,31 +115,44 @@ and library_segment = library_entry list sections, but on the contrary there are many constructions of section paths based on the library path. *) +let initial_prefix = default_module,(initial_path,empty_dirpath) + let lib_stk = ref ([] : library_segment) -let module_name = ref None -let path_prefix = ref (default_module : dir_path) +let comp_name = ref None +let path_prefix = ref initial_prefix -let module_sp () = - match !module_name with Some m -> m | None -> default_module +let module_dp () = + match !comp_name with Some m -> m | None -> default_module let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir + | (sp, OpenedModule (dir,_)) :: _ -> dir + | (sp, OpenedModtype (dir,_)) :: _ -> dir + | (sp, CompilingModule dir) :: _ -> dir | _::l -> recalc l - | [] -> module_sp () + | [] -> initial_prefix in path_prefix := recalc !lib_stk -let pop_path_prefix () = path_prefix := fst (split_dirpath !path_prefix) +let pop_path_prefix () = + let dir,(mp,sec) = !path_prefix in + path_prefix := fst (split_dirpath dir), (mp, fst (split_dirpath sec)) + +let make_path id = Libnames.make_path (fst !path_prefix) id -let make_path id = Names.make_path !path_prefix id +let make_kn id = + let mp,dir = snd !path_prefix in + Names.make_kn mp dir (label_of_id id) + +let make_oname id = make_path id, make_kn id let sections_depth () = - List.length (repr_dirpath !path_prefix) - - List.length (repr_dirpath (module_sp ())) + List.length (repr_dirpath (snd (snd !path_prefix))) -let cwd () = !path_prefix +let cwd () = fst !path_prefix +let current_prefix () = snd !path_prefix let find_entry_p p = let rec find = function @@ -70,12 +162,17 @@ let find_entry_p p = find !lib_stk let split_lib sp = - let rec findrec after = function - | ((sp',obj) as hd)::before -> - if sp = sp' then (after,hd,before) else findrec (hd::after) before + let rec collect after equal = function + | ((sp',_) as hd)::before -> + if sp = sp' then collect after (hd::equal) before else after,equal,hd::before + | [] -> after,equal,[] + in + let rec findeq after = function + | ((sp',_) as hd)::before -> + if sp = sp' then collect after [hd] before else findeq (hd::after) before | [] -> error "no such entry" in - findrec [] !lib_stk + findeq [] !lib_stk (* Adding operations. *) @@ -87,119 +184,267 @@ let anonymous_id = fun () -> incr n; id_of_string ("_" ^ (string_of_int !n)) let add_anonymous_entry node = - let sp = make_path (anonymous_id()) in - add_entry sp node; - sp + let id = anonymous_id () in + let name = make_oname id in + add_entry name node; + name let add_absolutely_named_leaf sp obj = cache_object (sp,obj); add_entry sp (Leaf obj) let add_leaf id obj = - let sp = make_path id in - cache_object (sp,obj); - add_entry sp (Leaf obj); - sp + let oname = make_oname id in + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname + +let add_leaves id objs = + let oname = make_oname id in + let add_obj obj = + add_entry oname (Leaf obj); + load_object 1 (oname,obj) + in + List.iter add_obj objs; + oname let add_anonymous_leaf obj = - let sp = make_path (anonymous_id()) in - cache_object (sp,obj); - add_entry sp (Leaf obj) + let id = anonymous_id () in + let oname = make_oname id in + cache_object (oname,obj); + add_entry oname (Leaf obj) let add_frozen_state () = let _ = add_anonymous_entry (FrozenState (freeze_summaries())) in () +(* Modules. *) + +let is_something_opened = function + (_,OpenedSection _) -> true + | (_,OpenedModule _) -> true + | (_,OpenedModtype _) -> true + | _ -> false + +let classify_segment seg = + let rec clean ((substl,keepl,anticipl) as acc) = function + | (_,CompilingModule _) :: _ | [] -> acc + | (oname,Leaf o) as node :: stk -> + (match classify_object (oname,o) with + | Dispose -> clean acc stk + | Keep o' -> + clean (substl, (oname,Leaf o')::keepl, anticipl) stk + | Substitute o' -> + clean ((oname,Leaf o')::substl, keepl, anticipl) stk + | Anticipate o' -> + clean (substl, keepl, (oname,Leaf o')::anticipl) stk) + | (oname,ClosedSection _ as item) :: stk -> clean acc stk + | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedModule _) :: _ -> error "there are still opened modules" + | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,FrozenState _) :: stk -> clean acc stk + in + clean ([],[],[]) (List.rev seg) + +let export_segment seg = + let rec clean acc = function + | (_,CompilingModule _) :: _ | [] -> acc + | (oname,Leaf o) as node :: stk -> + (match export_object o with + | None -> clean acc stk + | Some o' -> clean ((oname,Leaf o') :: acc) stk) + | (oname,ClosedSection _ as item) :: stk -> clean (item :: acc) stk + | (_,OpenedSection _) :: _ -> error "there are still opened sections" + | (_,OpenedModule _) :: _ -> error "there are still opened modules" + | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,FrozenState _) :: stk -> clean acc stk + in + clean [] seg + + +let start_module id mp nametab = + let dir = extend_dirpath (fst !path_prefix) id in + let prefix = dir,(mp,empty_dirpath) in + let oname = make_path id, make_kn id in + if Nametab.exists_module dir then + errorlabstrm "open_module" (pr_id id ++ str " already exists") ; + add_entry oname (OpenedModule (prefix,nametab)); + path_prefix := prefix +(* add_frozen_state () must be called in declaremods *) + +let end_module id = + let oname,nametab = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,nametab) -> + let sp = fst oname in + let id' = basename sp in + if id<>id' then error "this is not the last opened module"; + oname,nametab + | _,OpenedModtype _ -> + error "there are some open module types" + | _,OpenedSection _ -> + error "there are some open sections" + | _ -> assert false + with Not_found -> + error "no opened modules" + in + let (after,_,before) = split_lib oname in + lib_stk := before; + let prefix = !path_prefix in + recalc_path_prefix (); + (* add_frozen_state must be called after processing the module, + because we cannot recache interactive modules *) + (oname, prefix, nametab,after) + +let start_modtype id mp nametab = + let dir = extend_dirpath (fst !path_prefix) id in + let prefix = dir,(mp,empty_dirpath) in + let sp = make_path id in + let name = sp, make_kn id in + if Nametab.exists_cci sp then + errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ; + add_entry name (OpenedModtype (prefix,nametab)); + path_prefix := prefix + +let end_modtype id = + let sp,nametab = + try match find_entry_p is_something_opened with + | sp,OpenedModtype (_,nametab) -> + let id' = basename (fst sp) in + if id<>id' then error "this is not the last opened module"; + sp,nametab + | _,OpenedModule _ -> + error "there are some open modules" + | _,OpenedSection _ -> + error "there are some open sections" + | _ -> assert false + with Not_found -> + error "no opened module types" + in + let (after,_,before) = split_lib sp in + lib_stk := before; + let dir = !path_prefix in + recalc_path_prefix (); + (* add_frozen_state must be called after processing the module type. + This is because we cannot recache interactive module types *) + (sp,dir,nametab,after) + + + let contents_after = function | None -> !lib_stk | Some sp -> let (after,_,_) = split_lib sp in after (* Modules. *) -let check_for_module () = +let check_for_comp_unit () = let is_decl = function (_,FrozenState _) -> false | _ -> true in try let _ = find_entry_p is_decl in - error "a module can not be started after some declarations" + error "a module cannot be started after some declarations" with Not_found -> () (* TODO: use check_for_module ? *) -let start_module s = - if !module_name <> None then - error "a module is already started"; - if !path_prefix <> default_module then +let start_compilation s mp = + if !comp_name <> None then + error "compilation unit is already started"; + if snd (snd (!path_prefix)) <> empty_dirpath then error "some sections are already opened"; - module_name := Some s; - let _ = add_anonymous_entry (Module s) in - path_prefix := s - -let end_module s = - match !module_name with - | None -> error "no module declared" - | Some m -> - let (_,bm) = split_dirpath m in - if bm <> s then - error ("The current open module has basename "^(string_of_id bm)); - m + let prefix = s, (mp, empty_dirpath) in + let _ = add_anonymous_entry (CompilingModule prefix) in + comp_name := Some s; + path_prefix := prefix + +let end_compilation dir = + let _ = + try match find_entry_p is_something_opened with + | _, OpenedSection _ -> error "There are some open sections" + | _, OpenedModule _ -> error "There are some open modules" + | _, OpenedModtype _ -> error "There are some open module types" + | _ -> assert false + with + Not_found -> () + in + let module_p = + function (_,CompilingModule _) -> true | x -> is_something_opened x + in + let oname = + try match find_entry_p module_p with + (oname, CompilingModule prefix) -> oname + | _ -> assert false + with + Not_found -> anomaly "No module declared" + in + let _ = match !comp_name with + | None -> anomaly "There should be a module name..." + | Some m -> + if m <> dir then anomaly + ("The current open module has name "^ (string_of_dirpath m) ^ + " and not " ^ (string_of_dirpath m)); + in + let (after,_,before) = split_lib oname in + !path_prefix,after + +(* Returns true if we are inside an opened module type *) +let is_specification () = + let opened_p = function + | _, OpenedModtype _ -> true + | _ -> false + in + try + let _ = find_entry_p opened_p in true + with + Not_found -> false + +(* Returns the most recent OpenedThing node *) +let what_is_opened () = find_entry_p is_something_opened (* Sections. *) let open_section id = - let dir = extend_dirpath !path_prefix id in - let sp = make_path id in + let olddir,(mp,oldsec) = !path_prefix in + let dir = extend_dirpath olddir id in + let prefix = dir, (mp, extend_dirpath oldsec id) in + let name = make_path id, make_kn id (* this makes little sense however *) in if Nametab.exists_section dir then errorlabstrm "open_section" (pr_id id ++ str " already exists"); let sum = freeze_summaries() in - add_entry sp (OpenedSection (dir, sum)); + add_entry name (OpenedSection (prefix, sum)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_section dir; - path_prefix := dir; - sp - -let is_opened_section = function (_,OpenedSection _) -> true | _ -> false + Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); + path_prefix := prefix; + prefix let sections_are_opened () = - try let _ = find_entry_p is_opened_section in true + try + match find_entry_p is_something_opened with + | (_,OpenedSection _) -> true + | (_,OpenedModule _) -> false + | _ -> false with Not_found -> false -let export_segment seg = - let rec clean acc = function - | (_,Module _) :: _ | [] -> acc - | (sp,Leaf o) as node :: stk -> - (match export_object o with - | None -> clean acc stk - | Some o' -> clean ((sp,Leaf o') :: acc) stk) - | (sp,ClosedSection _ as item) :: stk -> clean (item :: acc) stk - | (_,OpenedSection _) :: _ -> error "there are still opened sections" - | (_,FrozenState _) :: stk -> clean acc stk - in - clean [] seg - (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) let close_section ~export id = - let sp,dir,fs = - try match find_entry_p is_opened_section with - | sp,OpenedSection (dir,fs) -> - if id<>snd(split_dirpath dir) then + let oname,fs = + try match find_entry_p is_something_opened with + | oname,OpenedSection (_,fs) -> + if id <> basename (fst oname) then error "this is not the last opened section"; - (sp,dir,fs) - | _ -> assert false + (oname,fs) + | _ -> assert false with Not_found -> error "no opened section" in - let (after,_,before) = split_lib sp in + let (after,_,before) = split_lib oname in lib_stk := before; + let prefix = !path_prefix in pop_path_prefix (); - let closed_sec = ClosedSection (export, dir, export_segment after) in - add_entry (make_path id) closed_sec; - (dir,after,fs) - -(* The following function exports the whole library segment, that will be - saved as a module. Objects are presented in chronological order, and - frozen states are removed. *) - -let export_module s = - export_segment !lib_stk + let closed_sec = + ClosedSection (export, (fst prefix), export_segment after) + in + let name = make_path id, make_kn id in + add_entry name closed_sec; + (prefix, after, fs) (* Backtracking. *) @@ -207,6 +452,7 @@ let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) | _ -> () + let recache_context ctx = List.iter recache_decl ctx @@ -226,21 +472,16 @@ let reset_to sp = let reset_name id = let (sp,_) = try - find_entry_p (fun (sp,_) -> let (_,spi) = repr_path sp in id = spi) + find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) with Not_found -> error (string_of_id id ^ ": no such entry") in reset_to sp let point_obj = - let (f,_) = - declare_object - ("DOT", - {cache_function = (fun _ -> ()); - load_function = (fun _ -> ()); - open_function = (fun _ -> ()); - export_function = (fun _ -> None) }) in - f() + let (f,_) = declare_object {(default_object "DOT") with + classify_function = (fun _ -> Dispose)} in + f() let mark_end_of_command () = match !lib_stk with @@ -258,41 +499,41 @@ let back n = reset_to (back_stk n !lib_stk) (* [dir] is a section dir if [module] < [dir] <= [path_prefix] *) let is_section_p sp = - not (is_dirpath_prefix_of sp (module_sp ())) - & (is_dirpath_prefix_of sp !path_prefix) + not (is_dirpath_prefix_of sp (module_dp ())) + & (is_dirpath_prefix_of sp (fst !path_prefix)) (* State and initialization. *) type frozen = dir_path option * library_segment -let freeze () = (!module_name, !lib_stk) +let freeze () = (!comp_name, !lib_stk) let unfreeze (mn,stk) = - module_name := mn; + comp_name := mn; lib_stk := stk; recalc_path_prefix () let init () = lib_stk := []; add_frozen_state (); - module_name := None; - path_prefix := make_dirpath []; + comp_name := None; + path_prefix := initial_prefix; init_summaries() (* Initial state. *) -let initial_state = ref (None : section_path option) +let initial_state = ref None let declare_initial_state () = - let sp = add_anonymous_entry (FrozenState (freeze_summaries())) in - initial_state := Some sp + let name = add_anonymous_entry (FrozenState (freeze_summaries())) in + initial_state := Some name let reset_initial () = match !initial_state with | None -> init () | Some sp -> begin match split_lib sp with - | (_,(_,FrozenState fs as hd),before) -> + | (_,[_,FrozenState fs as hd],before) -> lib_stk := hd::before; recalc_path_prefix (); unfreeze_summaries fs diff --git a/library/lib.mli b/library/lib.mli index b86c08f72..90f111c4b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames open Libobject open Summary (*i*) @@ -20,53 +21,127 @@ open Summary type node = | Leaf of obj - | Module of dir_path - | OpenedSection of dir_path * Summary.frozen + | CompilingModule of object_prefix + | OpenedModule of object_prefix * Summary.frozen + | OpenedModtype of object_prefix * Summary.frozen + | OpenedSection of object_prefix * Summary.frozen | ClosedSection of bool * dir_path * library_segment | FrozenState of Summary.frozen -and library_entry = section_path * node +and library_entry = object_name * node and library_segment = library_entry list +type lib_objects = (identifier * obj) list -(*s Adding operations (which calls the [cache] method, and getting the +(*s These functions iterate (or map) object functions. + + [subst_segment prefix subst seg] makes an assumption that all + objects in [seg] have the same prefix. This prefix is universally + changed to [prefix]. + + [classify_segment seg] divides segment into objects which responded + with [Substitute], [Keep], [Anticipate] respectively, to the + [classify_object] function. The order of each returned list is the + same as in the input list. + + [change_kns mp lib] only changes the prefix of the [kernel_name] + part of the [object_name] of every object to [(mp,empty_dirpath)]. + The [section_path] part of the [object_name] and the object itself + are unchanged. +*) + + +val open_segment : int -> library_segment -> unit +val load_segment : int -> library_segment -> unit +val subst_segment : + object_prefix -> substitution -> library_segment -> library_segment +val classify_segment : + library_segment -> library_segment * library_segment * library_segment +val change_kns : module_path -> library_segment -> library_segment + + + +val open_objects : int -> object_prefix -> lib_objects -> unit +val load_objects : int -> object_prefix -> lib_objects -> unit +val subst_objects : + object_prefix -> substitution -> lib_objects -> lib_objects +val classify_objects : + library_segment -> lib_objects * lib_objects * obj list + +val segment_of_objects : + object_prefix -> lib_objects -> library_segment + +(*s Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : identifier -> obj -> section_path -val add_absolutely_named_leaf : section_path -> obj -> unit +val add_leaf : identifier -> obj -> object_name +val add_absolutely_named_leaf : object_name -> obj -> unit val add_anonymous_leaf : obj -> unit + +(* this operation adds all objects with the same name and calls load_object + for each of them *) +val add_leaves : identifier -> obj list -> object_name + val add_frozen_state : unit -> unit val mark_end_of_command : unit -> unit (*s The function [contents_after] returns the current library segment, - starting from a given section path. If not given, the entire segment - is returned. *) + starting from a given section path. If not given, the entire segment + is returned. *) -val contents_after : section_path option -> library_segment +val contents_after : object_name option -> library_segment +(* Returns true if we are inside an opened module type *) +val is_specification : unit -> bool + +(* Returns the most recent OpenedThing node *) +val what_is_opened : unit -> library_entry (*s Opening and closing a section. *) -val open_section : identifier -> section_path -val close_section : - export:bool -> identifier -> dir_path * library_segment * Summary.frozen +val open_section : identifier -> object_prefix + +val close_section : export:bool -> identifier -> + object_prefix * library_segment * Summary.frozen + val sections_are_opened : unit -> bool val make_path : identifier -> section_path +val make_kn : identifier -> kernel_name + val cwd : unit -> dir_path val sections_depth : unit -> int val is_section_p : dir_path -> bool -val start_module : dir_path -> unit -val end_module : module_ident -> dir_path -val export_module : dir_path -> library_segment +(*s Compilation units *) + +val start_compilation : dir_path -> module_path -> unit +val end_compilation : dir_path -> object_prefix * library_segment + +val module_dp : unit -> dir_path +(*s Modules and module types *) + +val start_module : module_ident -> module_path -> Summary.frozen -> unit +val end_module : module_ident + -> object_name * object_prefix * Summary.frozen * library_segment + +val start_modtype : module_ident -> module_path -> Summary.frozen -> unit +val end_modtype : module_ident + -> object_name * object_prefix * Summary.frozen * library_segment + +(* Lib.add_frozen_state must be called after all of the above functions *) + +val current_prefix : unit -> module_path * dir_path (*s Backtracking (undo). *) -val reset_to : section_path -> unit +val reset_to : object_name -> unit val reset_name : identifier -> unit + +(* [back n] resets to the place corresponding to the $n$-th call of + [mark_end_of_command] (counting backwards) *) val back : int -> unit (*s We can get and set the state of the operations (used in [States]). *) diff --git a/library/libnames.ml b/library/libnames.ml new file mode 100644 index 000000000..d5e9c8dc7 --- /dev/null +++ b/library/libnames.ml @@ -0,0 +1,212 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ref + | ConstRef kn -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstRef kn' + | IndRef (kn,i) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + IndRef(kn',i) + | ConstructRef ((kn,i),j) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstructRef ((kn',i),j) + + +(**********************************************) + +let pr_dirpath sl = (str (string_of_dirpath sl)) + +(*s Operations on dirpaths *) + +(* Pop the last n module idents *) +let extract_dirpath_prefix n dir = + let (_,dir') = list_chop n (repr_dirpath dir) in + make_dirpath dir' + +let dirpath_prefix p = match repr_dirpath p with + | [] -> anomaly "dirpath_prefix: empty dirpath" + | _::l -> make_dirpath l + +let is_dirpath_prefix_of d1 d2 = + list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + +(* To know how qualified a name should be to be understood in the current env*) +let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) + +let split_dirpath d = + let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) + +let extend_dirpath p id = make_dirpath (id :: repr_dirpath p) + + +(* +let path_of_constructor env ((sp,tyi),ind) = + let mib = Environ.lookup_mind sp env in + let mip = mib.mind_packets.(tyi) in + let (pa,_) = repr_path sp in + Names.make_path pa (mip.mind_consnames.(ind-1)) + +let path_of_inductive env (sp,tyi) = + if tyi = 0 then sp + else + let mib = Environ.lookup_mind sp env in + let mip = mib.mind_packets.(tyi) in + let (pa,_) = repr_path sp in + Names.make_path pa (mip.mind_typename) +*) +(* parsing *) +let parse_dir s = + let len = String.length s in + let rec decoupe_dirs dirs n = + if n>=len then dirs else + let pos = + try + String.index_from s n '.' + with Not_found -> len + in + let dir = String.sub s n (pos-n) in + decoupe_dirs ((id_of_string dir)::dirs) (pos+1) + in + decoupe_dirs [] 0 + +let dirpath_of_string s = + match parse_dir s with + [] -> invalid_arg "dirpath_of_string" + | dir -> make_dirpath dir + + +(*s Section paths are absolute names *) + +type section_path = { + dirpath : dir_path ; + basename : identifier } + +let make_path pa id = { dirpath = pa; basename = id } +let repr_path { dirpath = pa; basename = id } = (pa,id) + +(* parsing and printing of section paths *) +let string_of_path sp = + let (sl,id) = repr_path sp in + if repr_dirpath sl = [] then string_of_id id + else (string_of_dirpath sl) ^ "." ^ (string_of_id id) + +let sp_ord sp1 sp2 = + let (p1,id1) = repr_path sp1 + and (p2,id2) = repr_path sp2 in + let p_bit = compare p1 p2 in + if p_bit = 0 then id_ord id1 id2 else p_bit + +module SpOrdered = + struct + type t = section_path + let compare = sp_ord + end + +module Spset = Set.Make(SpOrdered) +module Sppred = Predicate.Make(SpOrdered) +module Spmap = Map.Make(SpOrdered) + +let dirpath sp = let (p,_) = repr_path sp in p +let basename sp = let (_,id) = repr_path sp in id + +let path_of_string s = + try + let dir, id = split_dirpath (dirpath_of_string s) in + make_path dir id + with + | Invalid_argument _ -> invalid_arg "path_of_string" + +let pr_sp sp = str (string_of_path sp) + +let restrict_path n sp = + let dir, s = repr_path sp in + let (dir',_) = list_chop n (repr_dirpath dir) in + make_path (make_dirpath dir') s + +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of kernel_name + +let subst_ext subst glref = match glref with + | TrueGlobal ref -> + let ref' = subst_global subst ref in + if ref' == ref then glref else + TrueGlobal ref' + | SyntacticDef kn -> + let kn' = subst_kn subst kn in + if kn' == kn then glref else + SyntacticDef kn' + +let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) + +let decode_kn kn = + let mp,sec_dir,l = repr_kn kn in + match mp,(repr_dirpath sec_dir) with + MPfile dir,[] -> (dir,id_of_label l) + | _ , [] -> anomaly "MPfile expected!" + | _ -> anomaly "Section part should be empty!" + +(*s qualified names *) +type qualid = section_path + +let make_qualid = make_path +let repr_qualid = repr_path + +let string_of_qualid = string_of_path +let pr_qualid = pr_sp + +let qualid_of_string = path_of_string + +let qualid_of_sp sp = sp +let make_short_qualid id = make_qualid empty_dirpath id +let qualid_of_dirpath dir = + let (l,a) = split_dirpath dir in + make_qualid l a + +type object_name = section_path * kernel_name + +type object_prefix = dir_path * (module_path * dir_path) + +let make_oname (dirpath,(mp,dir)) id = + make_path dirpath id, make_kn mp dir (label_of_id id) + +(* to this type are mapped dir_path's in the nametab *) +type global_dir_reference = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + | DirClosedSection of dir_path + (* this won't last long I hope! *) + +(* | ModRef mp -> + let mp' = subst_modpath subst mp in if mp==mp' then ref else + ModRef mp' + | ModTypeRef kn -> + let kn' = subst_kernel_name subst kn in if kn==kn' then ref else + ModTypeRef kn' +*) + +type strength = + | NotDeclare + | DischargeAt of dir_path * int + | NeverDischarge diff --git a/library/libnames.mli b/library/libnames.mli new file mode 100644 index 000000000..915cdf3d2 --- /dev/null +++ b/library/libnames.mli @@ -0,0 +1,118 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference -> global_reference + +(* dirpaths *) +val pr_dirpath : dir_path -> Pp.std_ppcmds + +val dirpath_of_string : string -> dir_path + +(* Give the immediate prefix of a [dir_path] *) +val dirpath_prefix : dir_path -> dir_path + +(* Give the immediate prefix and basename of a [dir_path] *) +val split_dirpath : dir_path -> dir_path * identifier + +val extend_dirpath : dir_path -> module_ident -> dir_path +val add_dirpath_prefix : module_ident -> dir_path -> dir_path + +val extract_dirpath_prefix : int -> dir_path -> dir_path +val is_dirpath_prefix_of : dir_path -> dir_path -> bool + +(*s Section paths are {\em absolute} names *) +type section_path + +(* Constructors of [section_path] *) +val make_path : dir_path -> identifier -> section_path + +(* Destructors of [section_path] *) +val repr_path : section_path -> dir_path * identifier +val dirpath : section_path -> dir_path +val basename : section_path -> identifier + +(* Parsing and printing of section path as ["coq_root.module.id"] *) +val path_of_string : string -> section_path +val string_of_path : section_path -> string +val pr_sp : section_path -> std_ppcmds + +module Sppred : Predicate.S with type elt = section_path +module Spmap : Map.S with type key = section_path + +val restrict_path : int -> section_path -> section_path + +type extended_global_reference = + | TrueGlobal of global_reference + | SyntacticDef of kernel_name + +val subst_ext : + substitution -> extended_global_reference -> extended_global_reference + +(*s Temporary function to brutally form kernel names from section paths *) + +val encode_kn : dir_path -> identifier -> kernel_name +val decode_kn : kernel_name -> dir_path * identifier + + +(*s A [qualid] is a partially qualified ident; it includes fully + qualified names (= absolute names) and all intermediate partial + qualifications of absolute names, including single identifiers *) +type qualid + +val make_qualid : dir_path -> identifier -> qualid +val repr_qualid : qualid -> dir_path * identifier + +val string_of_qualid : qualid -> string +val pr_qualid : qualid -> std_ppcmds + +val qualid_of_string : string -> qualid + +(* Turns an absolute name into a qualified name denoting the same name *) +val qualid_of_sp : section_path -> qualid + +val qualid_of_dirpath : dir_path -> qualid + +val make_short_qualid : identifier -> qualid + +(* Both names are passed to objects: a "semantic" kernel_name, which + can be substituted and a "syntactic" section_path which can be printed +*) + +type object_name = section_path * kernel_name + +type object_prefix = dir_path * (module_path * dir_path) + +val make_oname : object_prefix -> identifier -> object_name + +(* to this type are mapped dir_path's in the nametab *) +type global_dir_reference = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + | DirClosedSection of dir_path + (* this won't last long I hope! *) + +type strength = + | NotDeclare + | DischargeAt of dir_path * int + | NeverDischarge diff --git a/library/libobject.ml b/library/libobject.ml index bbd8615be..2049e8e04 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -10,6 +10,7 @@ open Util open Names +open Libnames (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -23,18 +24,53 @@ let relax_flag = ref false;; let relax b = relax_flag := b;; +type 'a substitutivity = + Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a + + type 'a object_declaration = { - cache_function : section_path * 'a -> unit; - load_function : section_path * 'a -> unit; - open_function : section_path * 'a -> unit; + object_name : string; + cache_function : object_name * 'a -> unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : object_name * 'a -> 'a substitutivity; + subst_function : object_name * substitution * 'a -> 'a; export_function : 'a -> 'a option } +let yell s = anomaly s + +let default_object s = { + object_name = s; + cache_function = (fun _ -> ()); + load_function = (fun _ _ -> ()); + open_function = (fun _ _ -> ()); + subst_function = (fun _ -> + yell ("The object "^s^" does not know how to substitute!")); + classify_function = (fun (_,obj) -> Keep obj); + export_function = (fun _ -> None)} + + +(* The suggested object declaration is the following: + + declare_object { (default_object "MY OBJECT") with + cache_function = fun (sp,a) -> Mytbl.add sp a} + + and the listed functions are only those which definitions accually + differ from the default. + + This helps introducing new functions in objects. +*) + +let ident_subst_function (_,_,a) = a + type obj = Dyn.t (* persistent dynamic objects *) type dynamic_object_declaration = { - dyn_cache_function : section_path * obj -> unit; - dyn_load_function : section_path * obj -> unit; - dyn_open_function : section_path * obj -> unit; + dyn_cache_function : object_name * obj -> unit; + dyn_load_function : int -> object_name * obj -> unit; + dyn_open_function : int -> object_name * obj -> unit; + dyn_subst_function : object_name * substitution * obj -> obj; + dyn_classify_function : object_name * obj -> obj substitutivity; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -42,23 +78,43 @@ let object_tag lobj = Dyn.tag lobj let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) -let declare_object (na,odecl) = +let declare_object odecl = + let na = odecl.object_name in let (infun,outfun) = Dyn.create na in - let cacher (spopt,lobj) = - if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj) + let cacher (oname,lobj) = + if Dyn.tag lobj = na then odecl.cache_function (oname,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the cachefun" - and loader (spopt,lobj) = - if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj) + and loader i (oname,lobj) = + if Dyn.tag lobj = na then odecl.load_function i (oname,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the loadfun" - and opener (spopt,lobj) = - if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj) + and opener i (oname,lobj) = + if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the openfun" + and substituter (oname,sub,lobj) = + if Dyn.tag lobj = na then + infun (odecl.subst_function (oname,sub,outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the substfun" + and classifier (spopt,lobj) = + if Dyn.tag lobj = na then + match odecl.classify_function (spopt,outfun lobj) with + | Dispose -> Dispose + | Substitute obj -> Substitute (infun obj) + | Keep obj -> Keep (infun obj) + | Anticipate (obj) -> Anticipate (infun obj) + else + anomaly "somehow we got the wrong dynamic object in the classifyfun" and exporter lobj = - option_app infun (odecl.export_function (outfun lobj)) + if Dyn.tag lobj = na then + option_app infun (odecl.export_function (outfun lobj)) + else + anomaly "somehow we got the wrong dynamic object in the exportfun" + in Hashtbl.add cache_tab na { dyn_cache_function = cacher; dyn_load_function = loader; dyn_open_function = opener; + dyn_subst_function = substituter; + dyn_classify_function = classifier; dyn_export_function = exporter }; (infun,outfun) @@ -85,11 +141,17 @@ let apply_dyn_fun deflt f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj -let load_object ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_load_function node) lobj +let load_object i ((_,lobj) as node) = + apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj + +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) = + apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj -let open_object ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_open_function node) lobj +let classify_object ((_,lobj) as node) = + apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 017650e76..1c1209019 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -10,37 +10,96 @@ (*i*) open Names +open Libnames (*i*) -(* [Libobject] declares persistent objects, given with three methods: - a caching function specifying how to add the object in the current - scope of theory modules; - a loading function, specifying what to do when the object is loaded - from the disk; - an opening function, specifying what to do when the module containing - the object is opened; - a specification function, to extract its specification when writing - the specification of a module to the disk (.vi) *) +(* [Libobject] declares persistent objects, given with methods: + + * a caching function specifying how to add the object in the current + scope; + If the object wishes to register its visibility in the Nametab, + it should do so for all possible sufixes. + + * a loading function, specifying what to do when the module + containing the object is loaded; + If the object wishes to register its visibility in the Nametab, + it should do so for all sufixes no shorter then the "int" argument + + * an opening function, specifying what to do when the module + containing the object is opened (imported); + If the object wishes to register its visibility in the Nametab, + it should do so for the sufix of the length the "int" argument + + * a classification function, specyfying what to do with the object, + when the current module (containing the object) is ended; + The possibilities are: + Dispose - the object dies at the end of the module + Substitue - meaning the object is substitutive and + the module name must be updated + Keep - the object is not substitutive, but survives module + closing + Anticipate - this is for objects which have to be explicitely + managed by the end_module function (like Require + and Read markers) + + The classification function is also an occasion for a cleanup + (if this function returns Keep or Substitute of some object, the + cache method is never called for it) + + * a substitution function, performing the substitution; + this function should be declared for substitutive objects + only (see obove) + + * an export function, to enable optional writing of its contents + to disk (.vo). This function is also the oportunity to remove + redundant information in order to keep .vo size small + + The export function is a little obsolete and will be removed + in the near future... + +*) + +type 'a substitutivity = + Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a type 'a object_declaration = { - cache_function : section_path * 'a -> unit; - load_function : section_path * 'a -> unit; - open_function : section_path * 'a -> unit; + object_name : string; + cache_function : object_name * 'a -> unit; + load_function : int -> object_name * 'a -> unit; + open_function : int -> object_name * 'a -> unit; + classify_function : object_name * 'a -> 'a substitutivity; + subst_function : object_name * substitution * 'a -> 'a; export_function : 'a -> 'a option } -(*s Given an object name and a declaration, the function [declare_object] +(* The default object is a "Keep" object with empty methods. + Object creators are advised to use the construction + [{(default_object "MY_OBJECT") with + cache_function = ... + }] + and specify only these functions which are not empty/meaningless + +*) + +val default_object : string -> 'a object_declaration + +(* the identity substitution function *) +val ident_subst_function : object_name * substitution * 'a -> 'a + +(*s Given an object declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) type obj val declare_object : - (string * 'a object_declaration) -> ('a -> obj) * (obj -> 'a) + 'a object_declaration -> ('a -> obj) * (obj -> 'a) val object_tag : obj -> string -val cache_object : section_path * obj -> unit -val load_object : section_path * obj -> unit -val open_object : section_path * obj -> unit +val cache_object : object_name * obj -> unit +val load_object : int -> object_name * obj -> unit +val open_object : int -> object_name * obj -> unit +val subst_object : object_name * substitution * obj -> obj +val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index 93ab76371..8dd3c5432 100644 --- a/library/library.ml +++ b/library/library.ml @@ -12,13 +12,16 @@ open Pp open Util open Names +open Libnames open Nameops -open Environ +open Safe_typing open Libobject open Lib open Nametab +open Declaremods -(*s Load path. *) +(*************************************************************************) +(*s Load path. Mapping from physical to logical paths etc.*) type logical_path = dir_path @@ -54,6 +57,7 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p + let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in match list_filter2 (fun p d -> p = phys_dir) !load_path with @@ -75,7 +79,7 @@ let add_load_path_entry (phys_path,coq_path) = && coq_path = Nameops.default_root_prefix) then begin - (* Assume the user is concerned by module naming *) + (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then (Options.if_verbose warning (phys_path^" was previously bound to " ^(string_of_dirpath dir) @@ -95,31 +99,32 @@ let load_path_of_logical_path dir = let get_full_load_path () = List.combine (fst !load_path) (snd !load_path) +(***********************************************************************) (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) type compilation_unit_name = dir_path -type module_disk = { +type library_disk = { md_name : compilation_unit_name; - md_compiled_env : compiled_env; - md_declarations : library_segment; + md_compiled : compiled_library; + md_objects : library_objects; md_deps : (compilation_unit_name * Digest.t) list; md_imports : compilation_unit_name list } (*s Modules loaded in memory contain the following informations. They are - kept in the global table [modules_table]. *) - -type module_t = { - module_name : compilation_unit_name; - module_filename : System.physical_path; - module_compiled_env : compiled_env; - module_declarations : library_segment; - module_deps : (compilation_unit_name * Digest.t) list; - module_imports : compilation_unit_name list; - module_digest : Digest.t } - -module CompUnitOrdered = + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_filename : System.physical_path; + library_compiled : compiled_library; + library_objects : library_objects; + library_deps : (compilation_unit_name * Digest.t) list; + library_imports : compilation_unit_name list; + library_digest : Digest.t } + +module CompilingModuleOrdered = struct type t = dir_path let compare d1 d2 = @@ -127,33 +132,33 @@ module CompUnitOrdered = (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) end -module CompUnitmap = Map.Make(CompUnitOrdered) +module CompilingModulemap = Map.Make(CompilingModuleOrdered) -(* This is a map from names to modules *) -let modules_table = ref CompUnitmap.empty +(* This is a map from names to libraries *) +let libraries_table = ref CompilingModulemap.empty -(* These are the _ordered_ lists of loaded, imported and exported modules *) -let modules_loaded_list = ref [] -let modules_imports_list = ref [] -let modules_exports_list = ref [] +(* These are the _ordered_ lists of loaded, imported and exported libraries *) +let libraries_loaded_list = ref [] +let libraries_imports_list = ref [] +let libraries_exports_list = ref [] let freeze () = - !modules_table, - !modules_loaded_list, - !modules_imports_list, - !modules_exports_list + !libraries_table, + !libraries_loaded_list, + !libraries_imports_list, + !libraries_exports_list let unfreeze (mt,mo,mi,me) = - modules_table := mt; - modules_loaded_list := mo; - modules_imports_list := mi; - modules_exports_list := me + libraries_table := mt; + libraries_loaded_list := mo; + libraries_imports_list := mi; + libraries_exports_list := me let init () = - modules_table := CompUnitmap.empty; - modules_loaded_list := []; - modules_imports_list := []; - modules_exports_list := [] + libraries_table := CompilingModulemap.empty; + libraries_loaded_list := []; + libraries_imports_list := []; + libraries_exports_list := [] let _ = Summary.declare_summary "MODULES" @@ -162,40 +167,42 @@ let _ = Summary.init_function = init; Summary.survive_section = false } -let find_module s = +let find_library s = try - CompUnitmap.find s !modules_table + CompilingModulemap.find s !libraries_table with Not_found -> - error ("Unknown module " ^ (string_of_dirpath s)) + error ("Unknown library " ^ (string_of_dirpath s)) -let module_is_loaded dir = - try let _ = CompUnitmap.find dir !modules_table in true +let library_full_filename m = (find_library m).library_filename + +let library_is_loaded dir = + try let _ = CompilingModulemap.find dir !libraries_table in true with Not_found -> false -let module_is_opened dir = - List.exists (fun m -> m.module_name = dir) !modules_imports_list +let library_is_opened dir = + List.exists (fun m -> m.library_name = dir) !libraries_imports_list -let module_is_exported dir = - List.exists (fun m -> m.module_name = dir) !modules_exports_list +let library_is_exported dir = + List.exists (fun m -> m.library_name = dir) !libraries_exports_list -let loaded_modules () = - List.map (fun m -> m.module_name) !modules_loaded_list +let loaded_libraries () = + List.map (fun m -> m.library_name) !libraries_loaded_list -let opened_modules () = - List.map (fun m -> m.module_name) !modules_imports_list +let opened_libraries () = + List.map (fun m -> m.library_name) !libraries_imports_list - (* If a module is loaded several time, then the first occurrence must - be performed first, thus the modules_loaded_list ... *) + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) -let register_loaded_module m = +let register_loaded_library m = let rec aux = function | [] -> [m] - | m'::_ as l when m'.module_name = m.module_name -> l + | m'::_ as l when m'.library_name = m.library_name -> l | m'::l' -> m' :: aux l' in - modules_loaded_list := aux !modules_loaded_list; - modules_table := CompUnitmap.add m.module_name m !modules_table + libraries_loaded_list := aux !libraries_loaded_list; + libraries_table := CompilingModulemap.add m.library_name m !libraries_table - (* ... while if a module is imported/exported several time, then + (* ... 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 @@ -204,87 +211,89 @@ let register_loaded_module m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when m'.module_name = m.module_name -> remember_last_of_each l' m + | m'::l' when m'.library_name = m.library_name -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m -let register_open_module export m = - modules_imports_list := remember_last_of_each !modules_imports_list m; +let register_open_library export m = + libraries_imports_list := remember_last_of_each !libraries_imports_list m; if export then - modules_exports_list := remember_last_of_each !modules_exports_list m - -let compunit_cache = ref CompUnitmap.empty - -let module_segment = function - | None -> contents_after None - | Some m -> (find_module m).module_declarations - -let module_full_filename m = (find_module m).module_filename - -let vo_magic_number = 0703 (* V7.3 *) + libraries_exports_list := remember_last_of_each !libraries_exports_list m -let (raw_extern_module, raw_intern_module) = - System.raw_extern_intern vo_magic_number ".vo" +(************************************************************************) +(*s Operations on library objects and opening *) -let segment_rec_iter f = +(*let segment_rec_iter f = let rec apply = function | sp,Leaf obj -> f (sp,obj) | _,OpenedSection _ -> assert false | _,ClosedSection (_,_,seg) -> iter seg - | _,(FrozenState _ | Module _) -> () + | _,(FrozenState _ | CompilingModule _ + | OpenedModule _ | OpenedModtype _) -> () and iter seg = List.iter apply seg in iter -let segment_iter f = +let segment_iter i v f = let rec apply = function - | sp,Leaf obj -> f (sp,obj) + | sp,Leaf obj -> f (i,sp,obj) | _,OpenedSection _ -> assert false | sp,ClosedSection (export,dir,seg) -> - push_section dir; + push_dir v dir (DirClosedSection dir); if export then iter seg - | _,(FrozenState _ | Module _) -> () + | _,(FrozenState _ | CompilingModule _ + | OpenedModule _ | OpenedModtype _) -> () and iter seg = List.iter apply seg in iter +*) -(*s [open_module s] opens a module. The module [s] and all modules needed by +(*s [open_library s] opens a library. The library [s] and all libraries needed by [s] are assumed to be already loaded. When opening [s] we recursively open - all the modules needed by [s] and tagged [exported]. *) + all the libraries needed by [s] and tagged [exported]. *) -let open_objects decls = - segment_iter open_object decls +(*let open_objects i decls = + segment_iter i (Exactly i) open_object decls*) -let open_module export m = - if not (module_is_opened m.module_name) then - (register_open_module export m; - open_objects m.module_declarations) +let open_library export m = + if not (library_is_opened m.library_name) then begin + register_open_library export m; + Declaremods.import_module (MPfile m.library_name) + end else if export then - modules_exports_list := remember_last_of_each !modules_exports_list m + libraries_exports_list := remember_last_of_each !libraries_exports_list m -let open_modules export modl = +let open_libraries export modl = let to_open_list = List.fold_left (fun l m -> let subimport = List.fold_left - (fun l m -> remember_last_of_each l (find_module m)) - [] m.module_imports + (fun l m -> remember_last_of_each l (find_library m)) + [] m.library_imports in remember_last_of_each subimport m) [] modl in - List.iter (open_module export) to_open_list + List.iter (open_library export) to_open_list -(*s [load_module s] loads the module [s] from the disk, and [find_module s] - returns the module of name [s], loading it if necessary. - The boolean [doexp] specifies if we open the modules which are declared + +(************************************************************************) +(*s Loading from disk to cache (preparation phase) *) + +let compunit_cache = ref CompilingModulemap.empty + +let vo_magic_number = 0703 (* V7.3 *) + +let (raw_extern_library, raw_intern_library) = + System.raw_extern_intern vo_magic_number ".vo" + +(*s [load_library s] loads the library [s] from the disk, and [find_library s] + returns the library of name [s], loading it if necessary. + The boolean [doexp] specifies if we open the libraries which are declared exported in the dependencies (it is [true] at the highest level; then same value as for caller is reused in recursive loadings). *) -let load_objects decls = - segment_iter load_object decls - exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -292,8 +301,8 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Look if loaded in current environment *) try - let m = CompUnitmap.find dir !modules_table in - (dir, m.module_filename) + let m = CompilingModulemap.find dir !libraries_table in + (dir, m.library_filename) with Not_found -> (* Look if in loadpath *) try @@ -313,112 +322,94 @@ let with_magic_number_check f a = spc () ++ str"It is corrupted" ++ spc () ++ str"or was compiled with another version of Coq.") -let rec load_module dir = - try - (* Look if loaded in current env (and consequently its dependencies) *) - CompUnitmap.find dir !modules_table - with Not_found -> - (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let m = - try CompUnitmap.find dir !compunit_cache - with Not_found -> - anomaly ((string_of_dirpath dir)^" should be in cache") - in - List.iter (fun (dir,_) -> ignore (load_module dir)) m.module_deps; - Global.import m.module_compiled_env; - load_objects m.module_declarations; - register_loaded_module m; - Nametab.push_loaded_library m.module_name; - m - -let mk_module md f digest = { - module_name = md.md_name; - module_filename = f; - module_compiled_env = md.md_compiled_env; - module_declarations = md.md_declarations; - module_deps = md.md_deps; - module_imports = md.md_imports; - module_digest = digest } +let mk_library md f digest = { + library_name = md.md_name; + library_filename = f; + library_compiled = md.md_compiled; + library_objects = md.md_objects; + library_deps = md.md_deps; + library_imports = md.md_imports; + library_digest = digest } let intern_from_file f = - let ch = with_magic_number_check raw_intern_module f in + let ch = with_magic_number_check raw_intern_library f in let md = System.marshal_in ch in let digest = System.marshal_in ch in close_in ch; - mk_module md f digest + mk_library md f digest -let rec intern_module (dir, f) = +let rec intern_library (dir, f) = try (* Look if in the current logical environment *) - CompUnitmap.find dir !modules_table + CompilingModulemap.find dir !libraries_table with Not_found -> try (* Look if already loaded in cache and consequently its dependencies *) - CompUnitmap.find dir !compunit_cache + CompilingModulemap.find dir !compunit_cache with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in - if dir <> m.module_name then - errorlabstrm "load_physical_module" - (str ("The file " ^ f ^ " contains module") ++ spc () ++ - pr_dirpath m.module_name ++ spc () ++ str "and not module" ++ + if dir <> m.library_name then + errorlabstrm "load_physical_library" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); - compunit_cache := CompUnitmap.add dir m !compunit_cache; - List.iter (intern_mandatory_module dir) m.module_deps; + compunit_cache := CompilingModulemap.add dir m !compunit_cache; + List.iter (intern_mandatory_library dir) m.library_deps; m -and intern_mandatory_module caller (dir,d) = - let m = intern_absolute_module_from dir in - if d <> m.module_digest then - error ("compiled module "^(string_of_dirpath caller)^ - " makes inconsistent assumptions over module " +and intern_mandatory_library caller (dir,d) = + let m = intern_absolute_library_from dir in + if d <> m.library_digest then + error ("compiled library "^(string_of_dirpath caller)^ + " makes inconsistent assumptions over library " ^(string_of_dirpath dir)) -and intern_absolute_module_from dir = +and intern_absolute_library_from dir = try - intern_module (locate_absolute_library dir) + intern_library (locate_absolute_library dir) with | LibUnmappedDir -> let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in - errorlabstrm "load_absolute_module_from" + errorlabstrm "load_absolute_library_from" (str ("Cannot load "^dir^":") ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) | LibNotFound -> - errorlabstrm "load_absolute_module_from" - (str"Cannot find module " ++ pr_dirpath dir ++ str" in loadpath") + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_dirpath dir ++ str" in loadpath") | e -> raise e -let rec_intern_module mref = let _ = intern_module mref in () +let rec_intern_library mref = let _ = intern_library mref in () -let check_module_short_name f dir = function +let check_library_short_name f dir = function | Some id when id <> snd (split_dirpath dir) -> - errorlabstrm "check_module_short_name" - (str ("The file " ^ f ^ " contains module") ++ spc () ++ - pr_dirpath dir ++ spc () ++ str "and not module" ++ spc () ++ + errorlabstrm "check_library_short_name" + (str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ pr_id id) | _ -> () let rec_intern_by_filename_only id f = let m = intern_from_file f in (* Only the base name is expected to match *) - check_module_short_name f m.module_name id; - (* We check no other file containing same module is loaded *) + check_library_short_name f m.library_name id; + (* We check no other file containing same library is loaded *) try - let m' = CompUnitmap.find m.module_name !modules_table in + let m' = CompilingModulemap.find m.library_name !libraries_table in Options.if_verbose warning - ((string_of_dirpath m.module_name)^" is already loaded from file "^ - m'.module_filename); - m.module_name + ((string_of_dirpath m.library_name)^" is already loaded from file "^ + m'.library_filename); + m.library_name with Not_found -> - compunit_cache := CompUnitmap.add m.module_name m !compunit_cache; - List.iter (intern_mandatory_module m.module_name) m.module_deps; - m.module_name + compunit_cache := CompilingModulemap.add m.library_name m !compunit_cache; + List.iter (intern_mandatory_library m.library_name) m.library_deps; + m.library_name let locate_qualified_library qid = (* Look if loaded in current environment *) try let dir = Nametab.locate_loaded_library qid in - (LibLoaded, dir, module_full_filename dir) + (LibLoaded, dir, library_full_filename dir) with Not_found -> (* Look if in loadpath *) try @@ -438,7 +429,7 @@ let locate_qualified_library qid = let rec_intern_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library qid in - rec_intern_module (dir,f); + rec_intern_library (dir,f); dir with | LibUnmappedDir -> @@ -449,42 +440,79 @@ let rec_intern_qualified_library (loc,qid) = fnl ()) | LibNotFound -> user_err_loc (loc, "rec_intern_qualified_library", - str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath") + str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") -let rec_intern_module_from_file idopt f = - (* A name is specified, we have to check it contains module id *) +let rec_intern_library_from_file idopt f = + (* A name is specified, we have to check it contains library id *) let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in rec_intern_by_filename_only idopt f -(*s [require_module] loads and opens a module. This is a synchronized - operation. *) +(**********************************************************************) +(*s [require_library] loads and 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 to the compunit_cache + (using intern_* ) -type module_reference = dir_path list * bool option + 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 string_of_module (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) + + The [read_library] operation is very similar, but has does not "open" + the library +*) + +type library_reference = dir_path list * bool option + +let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) + +let rec load_library dir = + try + (* Look if loaded in current env (and consequently its dependencies) *) + CompilingModulemap.find dir !libraries_table + with Not_found -> + (* [dir] is an absolute name matching [f] which must be in loadpath *) + let m = + try CompilingModulemap.find dir !compunit_cache + with Not_found -> + anomaly ((string_of_dirpath dir)^" should be in cache") + in + List.iter (fun (dir,_) -> ignore (load_library dir)) m.library_deps; + Declaremods.register_library + m.library_name + m.library_compiled + m.library_objects + m.library_digest; + register_loaded_library m; + m let cache_require (_,(modl,export)) = - let ml = list_map_left load_module modl in + let ml = list_map_left load_library modl in match export with | None -> () - | Some export -> open_modules export ml + | Some export -> open_libraries export ml + +let load_require _ (_,(modl,_)) = + ignore(list_map_left load_library modl) (* keeps the require marker for closed section replay but removes OS dependent fields from .vo files for cross-platform compatibility *) let export_require (l,e) = Some (l,e) let (in_require, out_require) = - declare_object - ("REQUIRE", - { cache_function = cache_require; - load_function = (fun _ -> ()); - open_function = (fun _ -> ()); - export_function = export_require }) + declare_object {(default_object "REQUIRE") with + cache_function = cache_require; + load_function = load_require; + export_function = export_require; + classify_function = (fun (_,o) -> Anticipate o) } -let require_module spec qidl export = +let require_library spec qidl export = (* if sections_are_opened () && Options.verbose () then - warning ("Objets of "^(string_of_module modref)^ + warning ("Objets of "^(string_of_library modref)^ " not surviving sections (e.g. Grammar \nand Hints)\n"^ "will be removed at the end of the section"); *) @@ -492,53 +520,67 @@ let require_module spec qidl export = add_anonymous_leaf (in_require (modrefl,Some export)); add_frozen_state () -let require_module_from_file spec idopt file export = - let modref = rec_intern_module_from_file idopt file in +let require_library_from_file spec idopt file export = + let modref = rec_intern_library_from_file idopt file in add_anonymous_leaf (in_require ([modref],Some export)); add_frozen_state () -let import_module export (loc,qid) = - let modref = - try - Nametab.locate_loaded_library qid - with Not_found -> - user_err_loc - (loc,"import_module", - str ((Nametab.string_of_qualid qid)^" not loaded")) in - add_anonymous_leaf (in_require ([modref],Some export)) - -let read_module qid = +let export_library (loc,qid) = + try + match Nametab.locate_module qid with + MPfile dir -> + add_anonymous_leaf (in_require ([dir],Some true)) + | _ -> + raise Not_found + with + Not_found -> + user_err_loc + (loc,"export_library", + str ((string_of_qualid qid)^" is not a loaded library")) + +let read_library qid = let modref = rec_intern_qualified_library qid in add_anonymous_leaf (in_require ([modref],None)); add_frozen_state () -let read_module_from_file f = +let read_library_from_file f = let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in let modref = rec_intern_by_filename_only None f in add_anonymous_leaf (in_require ([modref],None)); add_frozen_state () -let reload_module (modrefl, export) = +let reload_library (modrefl, export) = add_anonymous_leaf (in_require (modrefl,export)); add_frozen_state () -(*s [save_module s] saves the module [m] to the disk. *) + +(***********************************************************************) +(*s [save_library s] saves the library [m] to the disk. *) + +let start_library f = + let _,longf = + System.find_file_in_path (get_load_path ()) (f^".v") in + let ldir0 = find_logical_path (Filename.dirname longf) in + let id = id_of_string (Filename.basename f) in + let ldir = extend_dirpath ldir0 id in + Declaremods.start_library ldir; + ldir,longf let current_deps () = - List.map (fun m -> (m.module_name, m.module_digest)) !modules_loaded_list + List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list let current_reexports () = - List.map (fun m -> m.module_name) !modules_exports_list + List.map (fun m -> m.library_name) !libraries_exports_list -let save_module_to s f = - let seg = export_module s in +let save_library_to s f = + let cenv, seg = Declaremods.export_library s in let md = { md_name = s; - md_compiled_env = Global.export s; - md_declarations = seg; + md_compiled = cenv; + md_objects = seg; md_deps = current_deps (); md_imports = current_reexports () } in - let (f',ch) = raw_extern_module f in + let (f',ch) = raw_extern_library f in try System.marshal_out ch md; flush ch; @@ -547,62 +589,38 @@ let save_module_to s f = close_out ch with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) -(*s Iterators. *) - -let fold_all_segments insec f x = - let rec apply acc = function - | sp, Leaf o -> f acc sp o - | _, ClosedSection (_,_,seg) -> - if insec then List.fold_left apply acc seg else acc - | _ -> acc - in - let acc' = - CompUnitmap.fold - (fun _ m acc -> List.fold_left apply acc m.module_declarations) - !modules_table x - in - List.fold_left apply acc' (Lib.contents_after None) - -let iter_all_segments insec f = - let rec apply = function - | sp, Leaf o -> f sp o - | _, ClosedSection (_,_,seg) -> if insec then List.iter apply seg - | _ -> () - in - CompUnitmap.iter - (fun _ m -> List.iter apply m.module_declarations) !modules_table; - List.iter apply (Lib.contents_after None) - -(*s Pretty-printing of modules state. *) - -let fmt_modules_state () = - let opened = opened_modules () - and loaded = loaded_modules () in +(*s Pretty-printing of libraries state. *) + +let fmt_libraries_state () = + let opened = opened_libraries () + and loaded = loaded_libraries () in (str "Imported (open) Modules: " ++ prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++ str "Loaded Modules: " ++ prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ()) + (*s For tactics/commands requiring vernacular libraries *) -let check_required_module d = +let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in - if not (module_is_loaded dir) then + if not (library_is_loaded dir) then (* Loading silently ... let m, prefix = list_sep_last d' in - read_module + read_library (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) - error ("Module "^(list_last d)^" has to be required first") + error ("Library "^(list_last d)^" has to be required first") + -(*s Display the memory use of a module. *) +(*s Display the memory use of a library. *) open Printf let mem s = - let m = find_module s in + let m = find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (size_kb m) (size_kb m.module_compiled_env) - (size_kb m.module_declarations))) + (size_kb m) (size_kb m.library_compiled) + (size_kb m.library_objects))) diff --git a/library/library.mli b/library/library.mli index dc34ec72e..43d73d241 100644 --- a/library/library.mli +++ b/library/library.mli @@ -11,61 +11,59 @@ (*i*) open Util open Names +open Libnames open Libobject (*i*) (*s This module is the heart of the library. It provides low level functions to - load, open and save modules. Modules are saved onto the disk with checksums + load, open and save libraries. Modules are saved onto the disk with checksums (obtained with the [Digest] module), which are checked at loading time to prevent inconsistencies between files written at various dates. It also provides a high level function [require] which corresponds to the vernacular command [Require]. *) -val read_module : Nametab.qualid located -> unit -val read_module_from_file : System.physical_path -> unit -val import_module : bool -> Nametab.qualid located -> unit +val read_library : qualid located -> unit -val module_is_loaded : dir_path -> bool -val module_is_opened : dir_path -> bool +val read_library_from_file : System.physical_path -> unit -val loaded_modules : unit -> dir_path list -val opened_modules : unit -> dir_path list +val export_library : qualid located -> unit -val fmt_modules_state : unit -> Pp.std_ppcmds +val library_is_loaded : dir_path -> bool +val library_is_opened : dir_path -> bool -(*s Require. The command [require_module spec m file export] loads and opens - a module [m]. [file] specifies the filename, if not [None]. [spec] +val loaded_libraries : unit -> dir_path list +val opened_libraries : unit -> dir_path list + +val fmt_libraries_state : unit -> Pp.std_ppcmds + +(*s Require. The command [require_library spec m file export] loads and opens + a library [m]. [file] specifies the filename, if not [None]. [spec] specifies to look for a specification ([true]) or for an implementation - ([false]), if not [None]. And [export] specifies if the module must be + ([false]), if not [None]. And [export] specifies if the library must be exported. *) -val require_module : - bool option -> Nametab.qualid located list -> bool -> unit +val require_library : + bool option -> qualid located list -> bool -> unit -val require_module_from_file : +val require_library_from_file : bool option -> identifier option -> string -> bool -> unit -(*s [save_module_to s f] saves the current environment as a module [s] +(*s [save_library_to s f] saves the current environment as a library [s] in the file [f]. *) -val save_module_to : dir_path -> string -> unit +val start_library : string -> dir_path * string +val save_library_to : dir_path -> string -> unit -(*s [module_segment m] returns the segment of the loaded module - [m]; if not given, the segment of the current module is returned +(*s [library_segment m] returns the segment of the loaded library + [m]; if not given, the segment of the current library is returned (which is then the same as [Lib.contents_after None]). - [module_full_filename] returns the full filename of a loaded module. *) +*) +(*val library_segment : dir_path option -> Lib.library_segment*) -val module_segment : dir_path option -> Lib.library_segment -val module_full_filename : dir_path -> string +(* [library_full_filename] returns the full filename of a loaded library. *) -(*s [fold_all_segments] and [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). The boolean indicates if we must enter closed sections. *) +val library_full_filename : dir_path -> string -val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a -val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit (*s Global load path *) type logical_path = dir_path @@ -82,16 +80,16 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - Nametab.qualid -> library_location * dir_path * System.physical_path + qualid -> library_location * dir_path * System.physical_path -val check_required_module : string list -> unit -(*s Displays the memory use of a module. *) +val check_required_library : string list -> unit +(*s Displays the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds (* For discharge *) -type module_reference +type library_reference -val out_require : Libobject.obj -> module_reference -val reload_module : module_reference -> unit +val out_require : Libobject.obj -> library_reference +val reload_library : library_reference -> unit diff --git a/library/nameops.ml b/library/nameops.ml index ecbe07e77..0fd9ec0d1 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -143,12 +143,7 @@ let next_name_away name l = | Name str -> next_ident_away str l | Anonymous -> id_of_string "_" -(**********************************************) - -let pr_dirpath sl = (str (string_of_dirpath sl)) - -(* Operations on dirpaths *) -let empty_dirpath = make_dirpath [] +let pr_lab l = str (string_of_label l) let default_module_name = id_of_string "Top" let default_module = make_dirpath [default_module_name] @@ -157,81 +152,3 @@ let default_module = make_dirpath [default_module_name] let coq_root = id_of_string "Coq" let default_root_prefix = make_dirpath [] -let restrict_path n sp = - let dir, s = repr_path sp in - let (dir',_) = list_chop n (repr_dirpath dir) in - Names.make_path (make_dirpath dir') s - -(* Pop the last n module idents *) -let extract_dirpath_prefix n dir = - let (_,dir') = list_chop n (repr_dirpath dir) in - make_dirpath dir' - -let dirpath_prefix p = match repr_dirpath p with - | [] -> anomaly "dirpath_prefix: empty dirpath" - | _::l -> make_dirpath l - -let is_dirpath_prefix_of d1 d2 = - list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) - -(* To know how qualified a name should be to be understood in the current env*) -let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) - -let split_dirpath d = - let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) - -let extend_dirpath p id = make_dirpath (id :: repr_dirpath p) - - -(* Section paths *) - -let dirpath sp = let (p,_) = repr_path sp in p -let basename sp = let (_,id) = repr_path sp in id - -let path_of_constructor env ((sp,tyi),ind) = - let mib = Environ.lookup_mind sp env in - let mip = mib.mind_packets.(tyi) in - let (pa,_) = repr_path sp in - Names.make_path pa (mip.mind_consnames.(ind-1)) - -let path_of_inductive env (sp,tyi) = - if tyi = 0 then sp - else - let mib = Environ.lookup_mind sp env in - let mip = mib.mind_packets.(tyi) in - let (pa,_) = repr_path sp in - Names.make_path pa (mip.mind_typename) - -(* parsing *) -let parse_sp s = - let len = String.length s in - let rec decoupe_dirs n = - try - let pos = String.index_from s n '.' in - let dir = String.sub s n (pos-n) in - let dirs,n' = decoupe_dirs (succ pos) in - (id_of_string dir)::dirs,n' - with - | Not_found -> [],n - in - if len = 0 then invalid_arg "parse_section_path"; - let dirs,n = decoupe_dirs 0 in - let id = String.sub s n (len-n) in - make_dirpath (List.rev dirs), (id_of_string id) - -let dirpath_of_string s = - try - let sl,s = parse_sp s in - extend_dirpath sl s - with - | Invalid_argument _ -> invalid_arg "dirpath_of_string" - -let path_of_string s = - try - let sl,s = parse_sp s in - make_path sl s - with - | Invalid_argument _ -> invalid_arg "path_of_string" - -(* Section paths *) -let pr_sp sp = (str (string_of_path sp)) diff --git a/library/nameops.mli b/library/nameops.mli index 35346b0a6..591e9030d 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -34,9 +34,11 @@ val next_name_away_with_default : val out_name : name -> identifier -(* Section and module mechanism: dealinng with dir paths *) -val pr_dirpath : dir_path -> Pp.std_ppcmds -val empty_dirpath : dir_path + +val pr_lab : label -> Pp.std_ppcmds + +(* some preset paths *) + val default_module : dir_path (* This is the root of the standard library of Coq *) @@ -45,31 +47,3 @@ val coq_root : module_ident (* This is the default root prefix for developments which doesn't mention a root *) val default_root_prefix : dir_path - - -val dirpath_of_string : string -> dir_path -val path_of_string : string -> section_path - -val path_of_constructor : env -> constructor -> section_path -val path_of_inductive : env -> inductive -> section_path - - -val dirpath : section_path -> dir_path -val basename : section_path -> identifier - -(* Give the immediate prefix of a [dir_path] *) -val dirpath_prefix : dir_path -> dir_path - -(* Give the immediate prefix and basename of a [dir_path] *) -val split_dirpath : dir_path -> dir_path * identifier - -val extend_dirpath : dir_path -> module_ident -> dir_path -val add_dirpath_prefix : module_ident -> dir_path -> dir_path - -val extract_dirpath_prefix : int -> dir_path -> dir_path -val is_dirpath_prefix_of : dir_path -> dir_path -> bool - -val restrict_path : int -> section_path -> section_path - -(* Section path *) -val pr_sp : section_path -> Pp.std_ppcmds diff --git a/library/nametab.ml b/library/nametab.ml index b28506f91..c80675aec 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -11,23 +11,10 @@ open Util open Pp open Names +open Libnames open Nameops open Declarations -(*s qualified names *) -type qualid = section_path - -let make_qualid = make_path -let repr_qualid = repr_path - -let string_of_qualid = string_of_path -let pr_qualid = pr_sp - -let qualid_of_sp sp = sp -let make_short_qualid id = make_qualid empty_dirpath id -let qualid_of_dirpath dir = - let (l,a) = split_dirpath dir in - make_qualid l a exception GlobalizationError of qualid exception GlobalizationConstantError of qualid @@ -40,118 +27,150 @@ let error_global_constant_not_found_loc loc q = let error_global_not_found q = raise (GlobalizationError q) -(* Constructions and syntactic definitions live in the same space *) -type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor - -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of section_path - -let sp_of_global env = function - | VarRef id -> make_path empty_dirpath id - | ConstRef sp -> sp - | IndRef (sp,tyi) -> - (* Does not work with extracted inductive types when the first - inductive is logic : if tyi=0 then basename sp else *) - let mib = Environ.lookup_mind sp env in - assert (tyi < mib.mind_ntypes && tyi >= 0); - let mip = mib.mind_packets.(tyi) in - let (p,_) = repr_path sp in - make_path p mip.mind_typename - | ConstructRef ((sp,tyi),i) -> - let mib = Environ.lookup_mind sp env in - assert (tyi < mib.mind_ntypes && i >= 0); - let mip = mib.mind_packets.(tyi) in - assert (i <= Array.length mip.mind_consnames && i > 0); - let (p,_) = repr_path sp in - make_path p mip.mind_consnames.(i-1) - +type 'a path_status = Nothing | Relative of 'a | Absolute of 'a (* Dictionaries of short names *) -type 'a nametree = ('a option * 'a nametree ModIdmap.t) +type 'a nametree = ('a path_status * 'a nametree ModIdmap.t) type ccitab = extended_global_reference nametree Idmap.t +type kntab = kernel_name nametree Idmap.t type objtab = section_path nametree Idmap.t -type dirtab = dir_path nametree ModIdmap.t +type dirtab = global_dir_reference nametree ModIdmap.t let the_ccitab = ref (Idmap.empty : ccitab) -let the_libtab = ref (ModIdmap.empty : dirtab) -let the_sectab = ref (ModIdmap.empty : dirtab) +let the_dirtab = ref (ModIdmap.empty : dirtab) let the_objtab = ref (Idmap.empty : objtab) +let the_modtypetab = ref (Idmap.empty : kntab) + +(* This table translates extended_global_references back to section paths *) +module Globtab = Map.Make(struct type t=extended_global_reference + let compare = compare end) + +type globtab = section_path Globtab.t + +let the_globtab = ref (Globtab.empty : globtab) + + +let sp_of_global ctx_opt ref = + match (ctx_opt,ref) with + | Some ctx, VarRef id -> + let _ = Sign.lookup_named id ctx in + make_path empty_dirpath id + | _ -> Globtab.find (TrueGlobal ref) !the_globtab + + +let full_name = sp_of_global None + +let id_of_global ctx_opt ref = + let (_,id) = repr_path (sp_of_global ctx_opt ref) in + id + +let sp_of_syntactic_definition kn = + Globtab.find (SyntacticDef kn) !the_globtab + +(******************************************************************) +(* the_dirpath is the table matching dir_paths to toplevel + modules/files or sections + + If we have a closed module M having a submodule N, than N does not + have the entry here. + +*) + +type visibility = Until of int | Exactly of int -let dirpath_of_reference ref = - let sp = match ref with - | ConstRef sp -> sp - | VarRef id -> make_path empty_dirpath id - | ConstructRef ((sp,_),_) -> sp - | IndRef (sp,_) -> sp in - let (p,_) = repr_path sp in - p - -let dirpath_of_extended_ref = function - | TrueGlobal ref -> dirpath_of_reference ref - | SyntacticDef sp -> - let (p,_) = repr_path sp in p - -(* How [visibility] works: a value of [0] means all suffixes of [dir] are - allowed to access the object, a value of [1] means all suffixes, except the - base name, are available, [2] means all suffixes except the base name and - the name qualified by the module name *) - -(* Concretely, library roots and directory are - always open but modules/files are open only during their interactive - construction or on demand if a precompiled one: for a name - "Root.Rep.Lib.name", then "Lib.name", "Rep.Lib.name" and - "Root.Rep.Lib.name", but not "name" are pushed; which means, visibility is - always 1 *) - -(* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *) -(* We proceed in the reverse way, looking first to [id] *) -let push_tree extract_dirpath tab visibility dir o = - let extract = option_app (fun c -> repr_dirpath (extract_dirpath c)) in +(* is the short name visible? tests for 1 *) +let is_short_visible v sp = match v with + Until 1 | Exactly 1 -> true + | _ -> false + +(* In general, directories and sections are always open and modules + (and files) are open on request only *) + +(* We add a binding of ["modid1.....modidn.id"] to [o] in the table *) +(* Using the fact that the reprezentation of a [dir_path] is already + reversed, we proceed in the reverse way, looking first for [id] *) + +(* [push_many] is used to register [Until vis] visibility and + [push_one] to [Exactly vis] and [push_tree] chooses the right one*) + +let push_many vis tab dir o = let rec push level (current,dirmap) = function | modid :: path as dir -> let mc = try ModIdmap.find modid dirmap - with Not_found -> (None, ModIdmap.empty) + with Not_found -> (Nothing, ModIdmap.empty) in let this = - if level >= visibility then - if extract current = Some dir then + if level >= vis then + match current with + | Absolute _ -> + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + warning "Trying to zaslonic an absolute name!"; current + | Nothing + | Relative _ -> Relative o + else current + in + (this, ModIdmap.add modid (push (level+1) mc path) dirmap) + | [] -> + match current with + | Absolute _ -> (* This is an absolute name, we must keep it otherwise it may - become unaccessible forever *) - current - else - Some o - else current in - (this, ModIdmap.add modid (push (level+1) mc path) dirmap) - | [] -> (Some o,dirmap) in - push 0 tab (repr_dirpath dir) - -let push_idtree extract_dirpath tab n dir id o = + become unaccessible forever *) + (* But ours is also absolute! This is an error! *) + error "Trying to zaslonic an absolute name!" + | Nothing + | Relative _ -> Absolute o, dirmap + in + push 0 tab (repr_dirpath dir) + +let push_one vis tab dir o = + let rec push level (current,dirmap) = function + | modid :: path as dir -> + let mc = + try ModIdmap.find modid dirmap + with Not_found -> (Nothing, ModIdmap.empty) + in + if level = vis then + let this = + match current with + | Absolute _ -> + (* This is an absolute name, we must keep it otherwise it may + become unaccessible forever *) + error "Trying to zaslonic an absolute name!" + | Nothing + | Relative _ -> Relative o + in + (this, dirmap) + else + (current, ModIdmap.add modid (push (level+1) mc path) dirmap) + | [] -> anomaly "We should never come to this point" + in + push 0 tab (repr_dirpath dir) + + +let push_tree = function + | Until i -> push_many (i-1) + | Exactly i -> push_one (i-1) + + + +let push_idtree tab visibility sp o = + let dir,id = repr_path sp in let modtab = try Idmap.find id !tab - with Not_found -> (None, ModIdmap.empty) in - tab := Idmap.add id (push_tree extract_dirpath modtab n dir o) !tab + with Not_found -> (Nothing, ModIdmap.empty) in + tab := + Idmap.add id (push_tree visibility modtab dir o) !tab -let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab -let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab -let push_long_names_objpath = - push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab -let push_short_name_objpath = - push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab -let push_modidtree tab dir id o = +let push_modidtree tab visibility dirpath o = + let dir,id = split_dirpath dirpath in let modtab = try ModIdmap.find id !tab - with Not_found -> (None, ModIdmap.empty) in - tab := ModIdmap.add id (push_tree (fun x -> x) modtab 0 dir o) !tab + with Not_found -> (Nothing, ModIdmap.empty) in + tab := ModIdmap.add id (push_tree visibility modtab dir o) !tab -let push_long_names_secpath = push_modidtree the_sectab -let push_long_names_libpath = push_modidtree the_libtab (* These are entry points for new declarations at toplevel *) @@ -159,95 +178,122 @@ let push_long_names_libpath = push_modidtree the_libtab possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom, Parameter but also Remark and Fact) *) -let push_cci ~visibility:n sp ref = - let dir, s = repr_path sp in - (* We push partially qualified name (with at least one prefix) *) - push_long_names_ccipath n dir s (TrueGlobal ref) +let push_xref visibility sp xref = + push_idtree the_ccitab visibility sp xref; + match visibility with + | Until _ -> + the_globtab := Globtab.add xref sp !the_globtab + | _ -> () -let push = push_cci +let push_cci visibility sp ref = + push_xref visibility sp (TrueGlobal ref) (* This is for Syntactic Definitions *) +let push_syntactic_definition visibility sp kn = + push_xref visibility sp (SyntacticDef kn) -let push_syntactic_definition sp = - let dir, s = repr_path sp in - push_long_names_ccipath 0 dir s (SyntacticDef sp) +let push = push_cci + +let push_modtype = push_idtree the_modtypetab -let push_short_name_syntactic_definition sp = - let _, s = repr_qualid (qualid_of_sp sp) in - push_short_name_ccipath Pervasives.max_int empty_dirpath s (SyntacticDef sp) (* This is for dischargeable non-cci objects (removed at the end of the section -- i.e. Hints, Grammar ...) *) (* --> Unused *) -let push_short_name_object sp = - let _, s = repr_qualid (qualid_of_sp sp) in - push_short_name_objpath 0 empty_dirpath s sp +let push_object visibility sp = + push_idtree the_objtab visibility sp sp (* This is for tactic definition names *) -let push_tactic_path sp = - let dir, s = repr_qualid (qualid_of_sp sp) in - push_long_names_objpath 0 dir s sp +let push_tactic = push_object (* This is to remember absolute Section/Module names and to avoid redundancy *) -let push_section fulldir = - let dir, s = split_dirpath fulldir in - (* We push all partially qualified name *) - push_long_names_secpath dir s fulldir; - push_long_names_secpath empty_dirpath s fulldir - -(* These are entry points to locate names *) -let locate_in_tree tab dir = - let dir = repr_dirpath dir in +let push_dir = push_modidtree the_dirtab + + +(* As before we start with generic functions *) + +let find_in_tree tab dir = let rec search (current,modidtab) = function | modid :: path -> search (ModIdmap.find modid modidtab) path - | [] -> match current with Some o -> o | _ -> raise Not_found + | [] -> current in search tab dir -let locate_cci (qid:qualid) = +let find_in_idtree tab qid = + let (dir,id) = repr_qualid qid in + find_in_tree (Idmap.find id !tab) (repr_dirpath dir) + +let find_in_modidtree tab qid = let (dir,id) = repr_qualid qid in - locate_in_tree (Idmap.find id !the_ccitab) dir + find_in_tree (ModIdmap.find id !tab) (repr_dirpath dir) + +let get = function + Absolute o | Relative o -> o + | Nothing -> raise Not_found + +let absolute = function + Absolute _ -> true + | Relative _ + | Nothing -> false + + +(* These are entry points to locate different things *) +let find_cci = find_in_idtree the_ccitab + +let find_dir = find_in_modidtree the_dirtab + +let find_modtype = find_in_idtree the_modtypetab (* This should be used when syntactic definitions are allowed *) -let extended_locate = locate_cci +let extended_locate qid = get (find_cci qid) (* This should be used when no syntactic definitions is expected *) -let locate qid = match locate_cci qid with +let locate qid = match extended_locate qid with | TrueGlobal ref -> ref | SyntacticDef _ -> raise Not_found -let locate_obj qid = - let (dir,id) = repr_qualid qid in - locate_in_tree (Idmap.find id !the_objtab) dir +let locate_syntactic_definition qid = match extended_locate qid with + | TrueGlobal _ -> raise Not_found + | SyntacticDef kn -> kn -let locate_tactic qid = - let (dir,id) = repr_qualid qid in - locate_in_tree (Idmap.find id !the_objtab) dir +let locate_modtype qid = get (find_modtype qid) -(* Actually, this table has only two levels, since only basename and *) -(* fullname are registered *) -let push_loaded_library fulldir = - let dir, s = split_dirpath fulldir in - push_long_names_libpath dir s fulldir; - push_long_names_libpath empty_dirpath s fulldir +let locate_obj qid = get (find_in_idtree the_objtab qid) -let locate_loaded_library qid = - let (dir,id) = repr_qualid qid in - locate_in_tree (ModIdmap.find id !the_libtab) dir +let locate_tactic qid = get (find_in_idtree the_objtab qid) + +let locate_dir qid = get (find_dir qid) + +let locate_module qid = + match locate_dir qid with + | DirModule (_,(mp,_)) -> mp + | _ -> raise Not_found + +let locate_loaded_library qid = + match locate_dir qid with + | DirModule (dir,_) -> dir + | _ -> raise Not_found let locate_section qid = - let (dir,id) = repr_qualid qid in - locate_in_tree (ModIdmap.find id !the_sectab) dir + match locate_dir qid with + | DirOpenSection (dir, _) + | DirClosedSection dir -> dir + | _ -> raise Not_found (* Derived functions *) let locate_constant qid = - (* TODO: restrict to defined constants *) - match locate_cci qid with - | TrueGlobal (ConstRef sp) -> sp + match extended_locate qid with + | TrueGlobal (ConstRef kn) -> kn + | _ -> raise Not_found + +let locate_mind qid = + match extended_locate qid with + | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found +(* let sp_of_id id = match locate_cci (make_short_qualid id) with | TrueGlobal ref -> ref | SyntacticDef _ -> @@ -258,14 +304,11 @@ let constant_sp_of_id id = match locate_cci (make_short_qualid id) with | TrueGlobal (ConstRef sp) -> sp | _ -> raise Not_found +*) let absolute_reference sp = - let a = locate_cci sp in - let (p,_) = repr_path sp in - if not (dirpath_of_extended_ref a = p) then - anomaly ("Not an absolute path: "^(string_of_path sp)); - match a with - | TrueGlobal ref -> ref + match find_cci (qualid_of_sp sp) with + | Absolute (TrueGlobal ref) -> ref | _ -> raise Not_found let locate_in_absolute_module dir id = @@ -282,13 +325,23 @@ let global (loc,qid) = error_global_not_found_loc loc qid let exists_cci sp = - try let _ = locate_cci sp in true + try + absolute (find_cci (qualid_of_sp sp)) with Not_found -> false - -let exists_section dir = - try let _ = locate_section (qualid_of_dirpath dir) in true + +let exists_dir dir = + try + absolute (find_dir (qualid_of_dirpath dir)) with Not_found -> false +let exists_section = exists_dir + +let exists_module = exists_dir + +let exists_modtype sp = + try + absolute (find_modtype (qualid_of_sp sp)) + with Not_found -> false (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x is a qualid that denotes the same object. *) @@ -323,25 +376,25 @@ let global_inductive (loc,qid as locqid) = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * dirtab * objtab * identifier list +type frozen = ccitab * dirtab * objtab * globtab let init () = the_ccitab := Idmap.empty; - the_libtab := ModIdmap.empty; - the_sectab := ModIdmap.empty; - the_objtab := Idmap.empty + the_dirtab := ModIdmap.empty; + the_objtab := Idmap.empty; + the_globtab := Globtab.empty let freeze () = !the_ccitab, - !the_libtab, - !the_sectab, - !the_objtab + !the_dirtab, + !the_objtab, + !the_globtab -let unfreeze (mc,ml,ms,mo) = +let unfreeze (mc,md,mo,gt) = the_ccitab := mc; - the_libtab := ml; - the_sectab := ms; - the_objtab := mo + the_dirtab := md; + the_objtab := mo; + the_globtab := gt let _ = Summary.declare_summary "names" @@ -350,7 +403,3 @@ let _ = Summary.init_function = init; Summary.survive_section = false } -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge diff --git a/library/nametab.mli b/library/nametab.mli index d71e3e379..b64fe0d9d 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -12,44 +12,49 @@ open Util open Pp open Names +open Libnames (*i*) -(*s This module contains the table for globalization, which associates global - names (section paths) to qualified names. *) +(*s This module contains the tables for globalization, which + associates internal object references to qualified names (qualid). *) -type global_reference = - | VarRef of variable - | ConstRef of constant - | IndRef of inductive - | ConstructRef of constructor +(* Most functions in this module fall into one of the following categories: + \begin{itemize} + \item [push : visibility -> full_user_name -> object_reference -> unit] + + Registers the [object_reference] to be referred to by the + [full_user_name] (and its suffixes according to [visibility]) -(* Finds the real name of a global (e.g. fetch the constructor names - from the inductive name and constructor number) *) -val sp_of_global : Environ.env -> global_reference -> section_path - -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of section_path + \item [exists : full_user_name -> bool] + + Is the [full_user_name] already atributed as an absolute user name + of some object? -(*s A [qualid] is a partially qualified ident; it includes fully - qualified names (= absolute names) and all intermediate partial - qualifications of absolute names, including single identifiers *) -type qualid + \item [locate : qualid -> object_reference] -val make_qualid : dir_path -> identifier -> qualid -val repr_qualid : qualid -> dir_path * identifier -val make_short_qualid : identifier -> qualid + Finds the object referred to by [qualid] or raises Not_found + + \item [name_of] : object_reference -> user_name -val string_of_qualid : qualid -> string -val pr_qualid : qualid -> std_ppcmds + The [user_name] can be for example the shortest non ambiguous [qualid] or + the [full_user_name] or [identifier]. Such a function can also have a + local context argument. +*) + + -val qualid_of_sp : section_path -> qualid +(* Finds the real name of a global (e.g. fetch the constructor names + from the inductive name and constructor number) *) +val sp_of_global : Sign.named_context option -> global_reference -> section_path +val sp_of_syntactic_definition : kernel_name -> section_path (* Turns an absolute name into a qualified name denoting the same name *) -val shortest_qualid_of_global : Environ.env -> global_reference -> qualid +val full_name : global_reference -> section_path +val shortest_qualid_of_global : Sign.named_context option -> global_reference -> qualid +val id_of_global : Sign.named_context option -> global_reference -> identifier (* Printing of global references using names as short as possible *) -val pr_global_env : Environ.env -> global_reference -> std_ppcmds +val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds exception GlobalizationError of qualid exception GlobalizationConstantError of qualid @@ -59,29 +64,29 @@ val error_global_not_found_loc : loc -> qualid -> 'a val error_global_not_found : qualid -> 'a val error_global_constant_not_found_loc : loc -> qualid -> 'a -(*s Register visibility of absolute paths by qualified names *) -val push : visibility:int -> section_path -> global_reference -> unit -val push_syntactic_definition : section_path -> unit +(*s Register visibility of things *) -(*s Register visibility of absolute paths by short names *) -val push_short_name_syntactic_definition : section_path -> unit -val push_short_name_object : section_path -> unit +(* The visibility can be registered either for all suffixes not + shorter then a given int - when the object is loaded inside a module, + or for a precise suffix, when the module containing (the module + containing ...) the object is open (imported) *) -(*s Register visibility of absolute paths by short names *) -val push_tactic_path : section_path -> unit -val locate_tactic : qualid -> section_path +type visibility = Until of int | Exactly of int -(*s Register visibility by all qualifications *) -val push_section : dir_path -> unit +(* is the short name visible? tests for 1 *) +val is_short_visible : visibility -> section_path -> bool -(* This should eventually disappear *) -val sp_of_id : identifier -> global_reference +val push : visibility -> section_path -> global_reference -> unit +val push_syntactic_definition : + visibility -> section_path -> kernel_name -> unit +val push_modtype : visibility -> section_path -> kernel_name -> unit +val push_dir : visibility -> dir_path -> global_dir_reference -> unit +val push_object : visibility -> section_path -> unit +val push_tactic : visibility -> section_path -> unit (*s The following functions perform globalization of qualified names *) (* This returns the section path of a constant or fails with [Not_found] *) -val constant_sp_of_id : identifier -> section_path - val locate : qualid -> global_reference (* This function is used to transform a qualified identifier into a @@ -97,11 +102,23 @@ val extended_locate : qualid -> extended_global_reference val locate_obj : qualid -> section_path val locate_constant : qualid -> constant +val locate_mind : qualid -> mutual_inductive val locate_section : qualid -> dir_path +val locate_modtype : qualid -> kernel_name +val locate_syntactic_definition : qualid -> kernel_name + +val locate_tactic : qualid -> section_path +val locate_dir : qualid -> global_dir_reference +val locate_module : qualid -> module_path (* [exists sp] tells if [sp] is already bound to a cci term *) val exists_cci : section_path -> bool -val exists_section : dir_path -> bool +val exists_modtype : section_path -> bool + +(* Those three functions are the same *) +val exists_dir : dir_path -> bool +val exists_section : dir_path -> bool (* deprecated *) +val exists_module : dir_path -> bool (* deprecated *) (*s Roots of the space of absolute names *) @@ -114,10 +131,10 @@ val absolute_reference : section_path -> global_reference one of its section/subsection *) val locate_in_absolute_module : dir_path -> identifier -> global_reference -val push_loaded_library : dir_path -> unit val locate_loaded_library : qualid -> dir_path -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge +type frozen + +val freeze : unit -> frozen +val unfreeze : frozen -> unit + diff --git a/library/summary.ml b/library/summary.ml index 210a1a81b..59560af22 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,7 +10,6 @@ open Pp open Util -open Names type 'a summary_declaration = { freeze_function : unit -> 'a; @@ -21,8 +20,8 @@ type 'a summary_declaration = { let summaries = (Hashtbl.create 17 : (string, Dyn.t summary_declaration) Hashtbl.t) -let declare_summary sumname sdecl = - let (infun,outfun) = Dyn.create (sumname^"-SUMMARY") in +let internal_declare_summary sumname sdecl = + let (infun,outfun) = Dyn.create sumname in let dyn_freeze () = infun (sdecl.freeze_function()) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -37,6 +36,14 @@ let declare_summary sumname sdecl = (str "Cannot declare a summary twice: " ++ str sumname); Hashtbl.add summaries sumname ddecl +let declare_summary sumname decl = + internal_declare_summary (sumname^"-SUMMARY") decl + +let envsummary = "Global environment SUMMARY" + +let declare_global_environment sdecl = + internal_declare_summary envsummary sdecl + type frozen = Dyn.t Stringmap.t let freeze_summaries () = @@ -62,5 +69,14 @@ let unfreeze_lost_summaries fs = with Not_found -> decl.init_function()) summaries +let unfreeze_other_summaries fs = + Hashtbl.iter + (fun id decl -> + try + if id <> envsummary then + decl.unfreeze_function (Stringmap.find id fs) + with Not_found -> decl.init_function()) + summaries + let init_summaries () = Hashtbl.iter (fun _ decl -> decl.init_function()) summaries diff --git a/library/summary.mli b/library/summary.mli index d381543b9..781b31144 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Libnames (*i*) (* This module registers the declaration of global tables, which will be kept @@ -22,12 +23,14 @@ type 'a summary_declaration = { survive_section : bool } val declare_summary : string -> 'a summary_declaration -> unit +val declare_global_environment : 'a summary_declaration -> unit type frozen val freeze_summaries : unit -> frozen val unfreeze_summaries : frozen -> unit val unfreeze_lost_summaries : frozen -> unit +val unfreeze_other_summaries : frozen -> unit val init_summaries : unit -> unit -- cgit v1.2.3