From ffa57bae1e18fd52d63e8512a352ac63db15a7a9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 6 Aug 2009 19:00:11 +0000 Subject: - Cleaning phase of the interfaces of libnames.ml and nametab.ml (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 4 +- library/declare.mli | 2 +- library/declaremods.ml | 32 +++++---- library/declaremods.mli | 4 +- library/dischargedhypsmap.ml | 2 +- library/dischargedhypsmap.mli | 6 +- library/goptions.ml | 2 +- library/heads.ml | 2 +- library/impargs.ml | 2 +- library/lib.ml | 162 +++++++++++++++++++----------------------- library/lib.mli | 16 ++--- library/libnames.ml | 59 +++++++-------- library/libnames.mli | 79 +++++++++++--------- library/libobject.ml | 18 ++--- library/libobject.mli | 4 +- library/library.ml | 8 +-- library/nametab.ml | 78 +++++++++----------- library/nametab.mli | 127 +++++++++++++++------------------ 18 files changed, 284 insertions(+), 323 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index a973e6a55..0cd1250c7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -141,7 +141,7 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let export_constant cst = Some (dummy_constant cst) -let classify_constant (_,cst) = Substitute (dummy_constant cst) +let classify_constant cst = Substitute (dummy_constant cst) let (inConstant,_) = declare_object { (default_object "CONSTANT") with @@ -267,7 +267,7 @@ let (inInductive,_) = cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; - classify_function = (fun (_,a) -> Substitute (dummy_inductive_entry a)); + classify_function = (fun a -> Substitute (dummy_inductive_entry a)); subst_function = ident_subst_function; discharge_function = discharge_inductive; export_function = export_inductive } diff --git a/library/declare.mli b/library/declare.mli index 32b651122..d5933ffb0 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -65,4 +65,4 @@ val set_xml_declare_constant : (bool * constant -> unit) -> unit val set_xml_declare_inductive : (bool * object_name -> unit) -> unit (* hook for the cache function of constants and inductives *) -val add_cache_hook : (section_path -> unit) -> unit +val add_cache_hook : (full_path -> unit) -> unit diff --git a/library/declaremods.ml b/library/declaremods.ml index f1a2c9e6c..0aa3d96bb 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -104,7 +104,7 @@ let _ = Summary.declare_summary "MODULE-INFO" Summary.survive_module = false; Summary.survive_section = false } -(* auxiliary functions to transform section_path and kernel_name given +(* auxiliary functions to transform full_path and kernel_name given by Lib into module_path and dir_path needed for modules *) let mp_of_kn kn = @@ -116,7 +116,7 @@ let mp_of_kn kn = let dir_of_sp sp = let dir,id = repr_path sp in - extend_dirpath dir id + add_dirpath_suffix dir id let msid_of_mp = function MPself msid -> msid @@ -287,7 +287,7 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = (None,substobjs,substituted) -let classify_module (_,(_,substobjs,_)) = +let classify_module (_,substobjs,_) = Substitute (None,substobjs,None) @@ -449,7 +449,7 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = end | None -> anomaly "Modops: Empty info" -and classify_module_alias (_,(entry,substobjs,_)) = +and classify_module_alias (entry,substobjs,_) = Substitute (entry,substobjs,None) let (in_module_alias,out_module_alias) = @@ -530,7 +530,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) = if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" - (pr_sp sp ++ str " already exists") ; + (pr_path sp ++ str " already exists") ; Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); @@ -542,7 +542,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" - (pr_sp sp ++ str " already exists") ; + (pr_path sp ++ str " already exists") ; Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); @@ -553,11 +553,11 @@ let open_modtype i ((sp,kn),(entry,_)) = check_empty "open_modtype" entry; if - try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) + try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) with Not_found -> true then errorlabstrm ("open_modtype") - (pr_sp sp ++ str " should already exist!"); + (pr_path sp ++ str " should already exist!"); Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) @@ -566,7 +566,7 @@ let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = (entry,(join subs subst,mbids,msid,objs)) -let classify_modtype (_,(_,substobjs)) = +let classify_modtype (_,substobjs) = Substitute (None,substobjs) @@ -726,9 +726,9 @@ let start_module interp_modtype export id args res_o = Lib.add_frozen_state (); mp -let end_module id = +let end_module () = - let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in + let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in let mbids, res_o, sub_o = !openmod_info in let substitute, keep, special = Lib.classify_segment lib_stack in @@ -753,6 +753,7 @@ let end_module id = (* must be called after get_modtype_substobjs, because of possible dependencies on functor arguments *) + let id = basename (fst oldoname) in let mp = Global.end_module id res_o in begin match sub_o with @@ -845,7 +846,7 @@ let cache_import (_,(_,mp)) = let mp = Nametab.locate_module (qualid_of_dirpath dir) in *) really_import_module mp -let classify_import (_,(export,_ as obj)) = +let classify_import (export,_ as obj) = if export then Substitute obj else Dispose let subst_import (_,subst,(export,mp as obj)) = @@ -880,9 +881,10 @@ let start_modtype interp_modtype id args = Lib.add_frozen_state (); mp -let end_modtype id = +let end_modtype () = - let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in + let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in + let id = basename (fst oldoname) in let ln = Global.end_modtype id in let substitute, _, special = Lib.classify_segment lib_stack in @@ -1041,7 +1043,7 @@ let subst_include (oname,subst,((me,is_mod),substobj,_)) = let substituted = subst_substobjs dir mp1 substobjs in ((subst_inc_expr subst' me,is_mod),substobjs,substituted) -let classify_include (_,((me,is_mod),substobjs,_)) = +let classify_include ((me,is_mod),substobjs,_) = Substitute ((me,is_mod),substobjs,None) let (in_include,out_include) = diff --git a/library/declaremods.mli b/library/declaremods.mli index 322078e9b..058bfa6ad 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -46,7 +46,7 @@ val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> module_path -val end_module : identifier -> module_path +val end_module : unit -> module_path @@ -58,7 +58,7 @@ val declare_modtype : (env -> 'modtype -> module_struct_entry) -> val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> module_path -val end_modtype : identifier -> module_path +val end_modtype : unit -> module_path (*s Objects of a module. They come in two lists: the substitutive ones diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 4a28c2fa5..7812b1f9e 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -20,7 +20,7 @@ open Libobject open Lib open Nametab -type discharged_hyps = section_path list +type discharged_hyps = full_path list let discharged_hyps_map = ref Spmap.empty diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 56e5492d8..f9d0f9b4f 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -15,10 +15,10 @@ open Environ open Nametab (*i*) -type discharged_hyps = section_path list +type discharged_hyps = full_path list (*s Discharged hypothesis. Here we store the discharged hypothesis of each *) (* constant or inductive type declaration. *) -val set_discharged_hyps : section_path -> discharged_hyps -> unit -val get_discharged_hyps : section_path -> discharged_hyps +val set_discharged_hyps : full_path -> discharged_hyps -> unit +val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/goptions.ml b/library/goptions.ml index 95259c9b5..6e58fd218 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -105,7 +105,7 @@ module MakeTable = Libobject.open_function = load_options; Libobject.cache_function = cache_options; Libobject.subst_function = subst_options; - Libobject.classify_function = (fun (_,x) -> Substitute x); + Libobject.classify_function = (fun x -> Substitute x); Libobject.export_function = export_options} in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), diff --git a/library/heads.ml b/library/heads.ml index ea3acbbe8..ba3a45594 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -164,7 +164,7 @@ let (inHead, _) = cache_function = cache_head; load_function = load_head; subst_function = subst_head; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_head; rebuild_function = rebuild_head; export_function = export_head } diff --git a/library/impargs.ml b/library/impargs.ml index 96c5c2a5c..68809d6aa 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -529,7 +529,7 @@ let (inImplicits, _) = cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_implicits; rebuild_function = rebuild_implicits; export_function = export_implicits } diff --git a/library/lib.ml b/library/lib.ml index 9dbf7ddc0..c033a3805 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -58,9 +58,9 @@ let load_and_subst_objects i prefix subst seg = let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc - | ((sp,kn as oname),Leaf o) :: stk -> + | ((sp,kn),Leaf o) :: stk -> let id = Names.id_of_label (Names.label kn) in - (match classify_object (oname,o) with + (match classify_object o with | Dispose -> clean acc stk | Keep o' -> clean (substl, (id,o')::keepl, anticipl) stk @@ -117,7 +117,7 @@ let cwd () = fst !path_prefix let current_dirpath sec = Libnames.drop_dirpath_prefix (library_dp ()) (if sec then cwd () - else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ())) + else Libnames.pop_dirpath_n (sections_depth ()) (cwd ())) let make_path id = Libnames.make_path (cwd ()) id @@ -211,10 +211,6 @@ let add_anonymous_entry node = 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 = if fst (current_prefix ()) = Names.initial_path then error ("No session module started (use -top dir)"); @@ -250,58 +246,55 @@ let add_frozen_state () = (* Modules. *) -let is_something_opened = function - (_,OpenedSection _) -> true - | (_,OpenedModule _) -> true - | (_,OpenedModtype _) -> true +let is_opened id = function + oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when + basename (fst oname) = id -> true + | _ -> false + +let is_opening_node = function + _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true | _ -> false let current_mod_id () = - try match find_entry_p is_something_opened with - | oname,OpenedModule (_,_,nametab) -> + try match find_entry_p is_opening_node with + | oname,OpenedModule (_,_,fs) -> basename (fst oname) - | oname,OpenedModtype (_,nametab) -> + | oname,OpenedModtype (_,fs) -> basename (fst oname) | _ -> error "you are not in a module" with Not_found -> error "no opened modules" -let start_module export id mp nametab = - let dir = extend_dirpath (fst !path_prefix) id in +let start_module export id mp fs = + let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.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 (export,prefix,nametab)); + add_entry oname (OpenedModule (export,prefix,fs)); path_prefix := prefix; prefix (* add_frozen_state () must be called in declaremods *) + +let error_still_opened string oname = + let id = basename (fst oname) in + errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.") -let end_module id = - let oname,nametab = - try match find_entry_p is_something_opened with - | oname,OpenedModule (_,_,nametab) -> - let id' = basename (fst oname) in - if id<>id' then - errorlabstrm "end_module" (str "last opened module is " ++ pr_id id'); - oname,nametab - | oname,OpenedModtype _ -> - let id' = basename (fst oname) in - errorlabstrm "end_module" - (str "module type " ++ pr_id id' ++ str " is still opened") - | oname,OpenedSection _ -> - let id' = basename (fst oname) in - errorlabstrm "end_module" - (str "section " ++ pr_id id' ++ str " is still opened") +let end_module () = + let oname,fs = + try match find_entry_p is_opening_node with + | oname,OpenedModule (_,_,fs) -> oname,fs + | oname,OpenedModtype _ -> error_still_opened "Module Type" oname + | oname,OpenedSection _ -> error_still_opened "Section" oname | _ -> assert false with Not_found -> - error "no opened modules" + error "No opened modules." in let (after,modopening,before) = split_lib oname in lib_stk := before; - add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening))); + add_entry oname (ClosedModule (List.rev_append after (List.rev modopening))); let prefix = !path_prefix in (* LEM: This module business seems more complicated than sections; shouldn't a backtrack into a closed module also do something @@ -311,48 +304,37 @@ let end_module id = recalc_path_prefix (); (* add_frozen_state must be called after processing the module, because we cannot recache interactive modules *) - (oname, prefix, nametab,after) + (oname, prefix, fs, after) -let start_modtype id mp nametab = - let dir = extend_dirpath (fst !path_prefix) id in +let start_modtype id mp fs = + let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.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)); + add_entry name (OpenedModtype (prefix,fs)); path_prefix := prefix; prefix -let end_modtype id = - let sp,nametab = - try match find_entry_p is_something_opened with - | oname,OpenedModtype (_,nametab) -> - let id' = basename (fst oname) in - if id<>id' then - errorlabstrm "end_modtype" (str "last opened module type is " ++ pr_id id'); - oname,nametab - | oname,OpenedModule _ -> - let id' = basename (fst oname) in - errorlabstrm "end_modtype" - (str "module " ++ pr_id id' ++ str " is still opened") - | oname,OpenedSection _ -> - let id' = basename (fst oname) in - errorlabstrm "end_modtype" - (str "section " ++ pr_id id' ++ str " is still opened") +let end_modtype () = + let oname,fs = + try match find_entry_p is_opening_node with + | oname,OpenedModtype (_,fs) -> oname,fs + | oname,OpenedModule _ -> error_still_opened "Module" oname + | oname,OpenedSection _ -> error_still_opened "Section" oname | _ -> assert false with Not_found -> error "no opened module types" in - let (after,modtypeopening,before) = split_lib sp in + let (after,modtypeopening,before) = split_lib oname in lib_stk := before; - add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening))); + add_entry oname (ClosedModtype (List.rev_append after (List.rev modtypeopening))); 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) - + (oname,dir,fs,after) let contents_after = function @@ -381,16 +363,16 @@ let start_compilation s mp = 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" + try match snd (find_entry_p is_opening_node) 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 (_,CompilingLibrary _) -> true | x -> is_something_opened x + function (_,CompilingLibrary _) -> true | x -> is_opening_node x in let oname = try match find_entry_p module_p with @@ -434,8 +416,12 @@ let is_module () = Not_found -> false -(* Returns the most recent OpenedThing node *) -let what_is_opened () = find_entry_p is_something_opened +(* Returns the opening node of a given name *) +let find_opening_node id = + try snd (find_entry_p (is_opened id)) + with Not_found -> + try ignore (find_entry_p is_opening_node); error "There is nothing to end." + with Not_found -> error "Nothing to end of this name." (* Discharge tables *) @@ -549,18 +535,18 @@ let set_xml_close_section f = xml_close_section := f let open_section id = let olddir,(mp,oldsec) = !path_prefix in - let dir = extend_dirpath olddir id in - let prefix = dir, (mp, extend_dirpath oldsec id) in + let dir = add_dirpath_suffix olddir id in + let prefix = dir, (mp, add_dirpath_suffix 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 name (OpenedSection (prefix, sum)); - (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); - path_prefix := prefix; - if !Flags.xml_export then !xml_open_section id; - add_section () + if Nametab.exists_section dir then + errorlabstrm "open_section" (pr_id id ++ str " already exists."); + let fs = freeze_summaries() in + add_entry name (OpenedSection (prefix, fs)); + (*Pushed for the lifetime of the section: removed by unfrozing the summary*) + Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); + path_prefix := prefix; + if !Flags.xml_export then !xml_open_section id; + add_section () (* Restore lib_stk and summaries as before the section opening, and @@ -575,14 +561,10 @@ let discharge_item ((sp,_ as oname),e) = | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" -let close_section id = +let close_section () = let oname,fs = - try match find_entry_p is_something_opened with - | oname,OpenedSection (_,fs) -> - let id' = basename (fst oname) in - if id <> id' then - errorlabstrm "close_section" (str "Last opened section is " ++ pr_id id' ++ str "."); - (oname,fs) + try match find_entry_p is_opening_node with + | oname,OpenedSection (_,fs) -> oname,fs | _ -> assert false with Not_found -> error "No opened section." @@ -591,8 +573,8 @@ let close_section id = lib_stk := before; let full_olddir = fst !path_prefix in pop_path_prefix (); - add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening))); - if !Flags.xml_export then !xml_close_section id; + add_entry oname (ClosedSection (List.rev_append secdecls (List.rev secopening))); + if !Flags.xml_export then !xml_close_section (basename (fst oname)); let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; @@ -826,7 +808,7 @@ let library_part ref = | _ -> dp_of_mp (mp_of_global ref) let remove_section_part ref = - let sp = Nametab.sp_of_global ref in + let sp = Nametab.path_of_global ref in let dir,_ = repr_path sp in match ref with | VarRef id -> @@ -834,7 +816,7 @@ let remove_section_part ref = | _ -> if is_dirpath_prefix_of dir (cwd ()) then (* Not yet (fully) discharged *) - extract_dirpath_prefix (sections_depth ()) (cwd ()) + pop_dirpath_n (sections_depth ()) (cwd ()) else (* Theorem/Lemma outside its outer section of definition *) dir @@ -844,11 +826,11 @@ let remove_section_part ref = let pop_kn kn = let (mp,dir,l) = Names.repr_kn kn in - Names.make_kn mp (dirpath_prefix dir) l + Names.make_kn mp (pop_dirpath dir) l let pop_con con = let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (dirpath_prefix dir) l + Names.make_con mp (pop_dirpath dir) l let con_defined_in_sec kn = let _,dir,_ = Names.repr_con kn in diff --git a/library/lib.mli b/library/lib.mli index 3330a20a7..1207511f0 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -52,7 +52,6 @@ val segment_of_objects : current list of operations (most recent ones coming first). *) val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name -val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit val add_anonymous_leaf : Libobject.obj -> unit (* this operation adds all objects with the same name and calls [load_object] @@ -81,8 +80,8 @@ val contents_after : Libnames.object_name option -> library_segment (* User-side names *) val cwd : unit -> Names.dir_path val current_dirpath : bool -> Names.dir_path -val make_path : Names.identifier -> Libnames.section_path -val path_of_include : unit -> Libnames.section_path +val make_path : Names.identifier -> Libnames.full_path +val path_of_include : unit -> Libnames.full_path (* Kernel-side names *) val current_prefix : unit -> Names.module_path * Names.dir_path @@ -98,20 +97,19 @@ val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident -(* Returns the most recent OpenedThing node *) -val what_is_opened : unit -> Libnames.object_name * node - +(* Returns the opening node of a given name *) +val find_opening_node : Names.identifier -> node (*s Modules and module types *) val start_module : bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_module : Names.module_ident +val end_module : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment val start_modtype : Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_modtype : Names.module_ident +val end_modtype : unit -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment (* [Lib.add_frozen_state] must be called after each of the above functions *) @@ -134,7 +132,7 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path (*s Sections *) val open_section : Names.identifier -> unit -val close_section : Names.identifier -> unit +val close_section : unit -> unit (*s Backtracking (undo). *) diff --git a/library/libnames.ml b/library/libnames.ml index 44da7b6de..650b5c33f 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -66,6 +66,14 @@ module RefOrdered = module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) +(* Extended global references *) + +type syndef_name = kernel_name + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + (**********************************************) let pr_dirpath sl = (str (string_of_dirpath sl)) @@ -73,10 +81,10 @@ 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 pop_dirpath_n n dir = make_dirpath (list_skipn n (repr_dirpath dir)) -let dirpath_prefix p = match repr_dirpath p with +let pop_dirpath p = match repr_dirpath p with | [] -> anomaly "dirpath_prefix: empty dirpath" | _::l -> make_dirpath l @@ -99,24 +107,8 @@ 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 add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p) -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 @@ -137,12 +129,15 @@ let parse_dir s = let dirpath_of_string s = make_dirpath (if s = "" then [] else parse_dir s) +let string_of_dirpath = Names.string_of_dirpath + + module Dirset = Set.Make(struct type t = dir_path let compare = compare end) module Dirmap = Map.Make(struct type t = dir_path let compare = compare end) (*s Section paths are absolute names *) -type section_path = { +type full_path = { dirpath : dir_path ; basename : identifier } @@ -163,7 +158,7 @@ let sp_ord sp1 sp2 = module SpOrdered = struct - type t = section_path + type t = full_path let compare = sp_ord end @@ -181,17 +176,13 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" -let pr_sp sp = str (string_of_path sp) +let pr_path sp = str (string_of_path sp) let restrict_path n sp = let dir, s = repr_path sp in let dir' = list_firstn n (repr_dirpath dir) in make_path (make_dirpath dir') s -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of kernel_name - let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id) @@ -223,23 +214,23 @@ let decode_con kn = | _ -> anomaly "Section part should be empty!" (*s qualified names *) -type qualid = section_path +type qualid = full_path let make_qualid = make_path let repr_qualid = repr_path let string_of_qualid = string_of_path -let pr_qualid = pr_sp +let pr_qualid = pr_path 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_path sp = sp +let qualid_of_ident 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_name = full_path * kernel_name type object_prefix = dir_path * (module_path * dir_path) @@ -269,7 +260,7 @@ type reference = let qualid_of_reference = function | Qualid (loc,qid) -> loc, qid - | Ident (loc,id) -> loc, make_short_qualid id + | Ident (loc,id) -> loc, qualid_of_ident id let string_of_reference = function | Qualid (loc,qid) -> string_of_qualid qid @@ -287,11 +278,11 @@ let loc_of_reference = function let pop_con con = let (mp,dir,l) = repr_con con in - Names.make_con mp (dirpath_prefix dir) l + Names.make_con mp (pop_dirpath dir) l let pop_kn kn = let (mp,dir,l) = repr_kn kn in - Names.make_kn mp (dirpath_prefix dir) l + Names.make_kn mp (pop_dirpath dir) l let pop_global_reference = function | ConstRef con -> ConstRef (pop_con con) diff --git a/library/libnames.mli b/library/libnames.mli index 399387dd7..e6591734b 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -42,53 +42,61 @@ val reference_of_constr : constr -> global_reference module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +(*s Extended global references *) + +type syndef_name = kernel_name + +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name + (*s Dirpaths *) val pr_dirpath : dir_path -> Pp.std_ppcmds val dirpath_of_string : string -> dir_path +val string_of_dirpath : dir_path -> string -(* Give the immediate prefix of a [dir_path] *) -val dirpath_prefix : dir_path -> dir_path +(* Pop the suffix of a [dir_path] *) +val pop_dirpath : dir_path -> dir_path + +(* Pop the suffix n times *) +val pop_dirpath_n : int -> 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_suffix : dir_path -> module_ident -> dir_path val add_dirpath_prefix : module_ident -> dir_path -> dir_path val chop_dirpath : int -> dir_path -> dir_path * dir_path +val append_dirpath : dir_path -> dir_path -> dir_path + val drop_dirpath_prefix : dir_path -> dir_path -> dir_path -val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool -val append_dirpath : dir_path -> dir_path -> dir_path module Dirset : Set.S with type elt = dir_path module Dirmap : Map.S with type key = dir_path -(*s Section paths are {\em absolute} names *) -type section_path +(*s Full paths are {\em absolute} paths of declarations *) +type full_path -(* Constructors of [section_path] *) -val make_path : dir_path -> identifier -> section_path +(* Constructors of [full_path] *) +val make_path : dir_path -> identifier -> full_path -(* Destructors of [section_path] *) -val repr_path : section_path -> dir_path * identifier -val dirpath : section_path -> dir_path -val basename : section_path -> identifier +(* Destructors of [full_path] *) +val repr_path : full_path -> dir_path * identifier +val dirpath : full_path -> dir_path +val basename : full_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 +val path_of_string : string -> full_path +val string_of_path : full_path -> string +val pr_path : full_path -> std_ppcmds -module Sppred : Predicate.S with type elt = section_path -module Spmap : Map.S with type key = section_path +module Sppred : Predicate.S with type elt = full_path +module Spmap : Map.S with type key = full_path -val restrict_path : int -> section_path -> section_path - -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of kernel_name +val restrict_path : int -> full_path -> full_path (*s Temporary function to brutally form kernel names from section paths *) @@ -100,29 +108,30 @@ val decode_con : constant -> 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 *) + qualifications of absolute names, including single identifiers. + The [qualid] are used to access the name table. *) + 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 string_of_qualid : qualid -> string 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 +(* Turns an absolute name, a dirpath, or an identifier into a + qualified name denoting the same name *) +val qualid_of_path : full_path -> qualid val qualid_of_dirpath : dir_path -> qualid - -val make_short_qualid : identifier -> qualid +val qualid_of_ident : 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 + can be substituted and a "syntactic" [full_path] which can be printed *) -type object_name = section_path * kernel_name +type object_name = full_path * kernel_name type object_prefix = dir_path * (module_path * dir_path) @@ -137,6 +146,10 @@ type global_dir_reference = | DirClosedSection of dir_path (* this won't last long I hope! *) +(*s A [reference] is the user-level notion of name. It denotes either a + global name (referred either by a qualified name or by a single + name) or a variable *) + type reference = | Qualid of qualid located | Ident of identifier located @@ -146,7 +159,7 @@ val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc -(* popping one level of section in global names *) +(*s Popping one level of section in global names *) val pop_con : constant -> constant val pop_kn : kernel_name -> kernel_name diff --git a/library/libobject.ml b/library/libobject.ml index 90636dbee..504c1ffdd 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -33,7 +33,7 @@ type 'a object_declaration = { 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; + classify_function : 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a; @@ -48,7 +48,7 @@ let default_object s = { open_function = (fun _ _ -> ()); subst_function = (fun _ -> yell ("The object "^s^" does not know how to substitute!")); - classify_function = (fun (_,obj) -> Keep obj); + classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -74,7 +74,7 @@ type dynamic_object_declaration = { 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_classify_function : obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } @@ -100,9 +100,9 @@ let declare_object odecl = 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) = + and classifier lobj = if Dyn.tag lobj = na then - match odecl.classify_function (spopt,outfun lobj) with + match odecl.classify_function (outfun lobj) with | Dispose -> Dispose | Substitute obj -> Substitute (infun obj) | Keep obj -> Keep (infun obj) @@ -167,14 +167,14 @@ let open_object i ((_,lobj) as node) = let subst_object ((_,_,lobj) as node) = apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj -let classify_object ((_,lobj) as node) = - apply_dyn_fun Dispose (fun d -> d.dyn_classify_function node) lobj +let classify_object lobj = + apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj -let rebuild_object (lobj as node) = - apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj +let rebuild_object lobj = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) 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 d104635cd..f32d3baa7 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -76,7 +76,7 @@ type 'a object_declaration = { 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; + classify_function : 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a; @@ -111,7 +111,7 @@ 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 classify_object : obj -> obj substitutivity val export_object : obj -> obj option val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj diff --git a/library/library.ml b/library/library.ml index abca3c7e7..24c2c3803 100644 --- a/library/library.ml +++ b/library/library.ml @@ -308,7 +308,7 @@ let subst_import (_,_,o) = o let export_import o = Some o -let classify_import (_,(_,export as obj)) = +let classify_import (_,export as obj) = if export then Substitute obj else Dispose @@ -367,7 +367,7 @@ let locate_qualified_library warn qid = if loadpath = [] then raise LibUnmappedDir; let name = string_of_id base ^ ".vo" in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = extend_dirpath (List.assoc lpath loadpath) base in + let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -540,7 +540,7 @@ let (in_require, out_require) = open_function = (fun _ _ -> assert false); export_function = export_require; discharge_function = discharge_require; - classify_function = (fun (_,o) -> Anticipate o) } + classify_function = (fun o -> Anticipate o) } (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) @@ -615,7 +615,7 @@ let start_library f = let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in check_coq_overwriting ldir0 id; - let ldir = extend_dirpath ldir0 id in + let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; ldir,longf diff --git a/library/nametab.ml b/library/nametab.ml index 5bb21b3e5..7f148f0d3 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -27,7 +27,9 @@ let error_global_constant_not_found_loc loc q = let error_global_not_found q = raise (GlobalizationError q) +(* Kinds of global names *) +type ltac_constant = kernel_name (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -42,7 +44,7 @@ type visibility = Until of int | Exactly of int (* Data structure for nametabs *******************************************) -(* This module type will be instantiated by [section_path] of [dir_path] *) +(* This module type will be instantiated by [full_path] of [dir_path] *) (* The [repr] function is assumed to return the reversed list of idents. *) module type UserName = sig type t @@ -251,7 +253,7 @@ end (* Global name tables *************************************************) module SpTab = Make (struct - type t = section_path + type t = full_path let to_string = string_of_path let repr sp = let dir,id = repr_path sp in @@ -268,9 +270,6 @@ let the_tactictab = ref (SpTab.empty : kntab) type mptab = module_path SpTab.t let the_modtypetab = ref (SpTab.empty : mptab) -type objtab = unit SpTab.t -let the_objtab = ref (SpTab.empty : objtab) - module DirTab = Make(struct type t = dir_path @@ -294,17 +293,17 @@ module Globrevtab = Map.Make(struct let compare = compare end) -type globrevtab = section_path Globrevtab.t +type globrevtab = full_path Globrevtab.t let the_globrevtab = ref (Globrevtab.empty : globrevtab) type mprevtab = dir_path MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) -type mptrevtab = section_path MPmap.t +type mptrevtab = full_path MPmap.t let the_modtyperevtab = ref (MPmap.empty : mptrevtab) -type knrevtab = section_path KNmap.t +type knrevtab = full_path KNmap.t let the_tacticrevtab = ref (KNmap.empty : knrevtab) @@ -328,8 +327,8 @@ 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_syndef visibility sp kn = + push_xref visibility sp (SynDef kn) let push = push_cci @@ -344,12 +343,6 @@ let push_tactic vis sp kn = the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab -(* This is for dischargeable non-cci objects (removed at the end of the - section -- i.e. Hints, Grammar ...) *) (* --> Unused *) - -let push_object visibility sp = - the_objtab := SpTab.push visibility sp () !the_objtab - (* This is to remember absolute Section/Module names and to avoid redundancy *) let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; @@ -362,24 +355,21 @@ let push_dir vis dir dir_ref = (* This should be used when syntactic definitions are allowed *) -let extended_locate qid = SpTab.locate qid !the_ccitab +let locate_extended qid = SpTab.locate qid !the_ccitab (* This should be used when no syntactic definitions is expected *) -let locate qid = match extended_locate qid with +let locate qid = match locate_extended qid with | TrueGlobal ref -> ref - | SyntacticDef _ -> raise Not_found + | SynDef _ -> raise Not_found let full_name_cci qid = SpTab.user_name qid !the_ccitab -let locate_syntactic_definition qid = match extended_locate qid with +let locate_syndef qid = match locate_extended qid with | TrueGlobal _ -> raise Not_found - | SyntacticDef kn -> kn + | SynDef kn -> kn let locate_modtype qid = SpTab.locate qid !the_modtypetab let full_name_modtype qid = SpTab.user_name qid !the_modtypetab -let locate_obj qid = SpTab.user_name qid !the_objtab - -type ltac_constant = kernel_name let locate_tactic qid = SpTab.locate qid !the_tactictab let full_name_tactic qid = SpTab.user_name qid !the_tactictab @@ -405,35 +395,35 @@ let locate_all qid = List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l) (SpTab.find_prefixes qid !the_ccitab) [] -let extended_locate_all qid = SpTab.find_prefixes qid !the_ccitab +let locate_extended_all qid = SpTab.find_prefixes qid !the_ccitab (* Derived functions *) let locate_constant qid = - match extended_locate qid with + match locate_extended qid with | TrueGlobal (ConstRef kn) -> kn | _ -> raise Not_found let locate_mind qid = - match extended_locate qid with + match locate_extended qid with | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found -let absolute_reference sp = +let global_of_path sp = match SpTab.find sp !the_ccitab with | TrueGlobal ref -> ref | _ -> raise Not_found -let extended_absolute_reference sp = SpTab.find sp !the_ccitab +let extended_global_of_path sp = SpTab.find sp !the_ccitab let locate_in_absolute_module dir id = - absolute_reference (make_path dir id) + global_of_path (make_path dir id) let global r = let (loc,qid) = qualid_of_reference r in - try match extended_locate qid with + try match locate_extended qid with | TrueGlobal ref -> ref - | SyntacticDef _ -> + | SynDef _ -> user_err_loc (loc,"global", str "Unexpected reference to a notation: " ++ pr_qualid qid) @@ -456,18 +446,19 @@ let exists_tactic sp = SpTab.exists sp !the_tactictab (* Reverse locate functions ***********************************************) -let sp_of_global ref = +let path_of_global ref = match ref with | VarRef id -> make_path empty_dirpath id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab +let dirpath_of_global ref = + fst (repr_path (path_of_global ref)) -let id_of_global ref = - let (_,id) = repr_path (sp_of_global ref) in - id +let basename_of_global ref = + snd (repr_path (path_of_global ref)) -let sp_of_syntactic_definition kn = - Globrevtab.find (SyntacticDef kn) !the_globrevtab +let path_of_syndef kn = + Globrevtab.find (SynDef kn) !the_globrevtab let dir_of_mp mp = MPmap.find mp !the_modrevtab @@ -483,7 +474,7 @@ let shortest_qualid_of_global ctx ref = SpTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_syndef ctx kn = - let sp = sp_of_syntactic_definition kn in + let sp = path_of_syndef kn in SpTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_module mp = @@ -505,7 +496,7 @@ let pr_global_env env ref = let s = string_of_qualid (shortest_qualid_of_global env ref) in (str s) -let inductive_of_reference r = +let global_inductive r = match global r with | IndRef ind -> ind | ref -> @@ -518,13 +509,12 @@ let inductive_of_reference r = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * objtab * kntab * kntab +type frozen = ccitab * dirtab * kntab * kntab * globrevtab * mprevtab * knrevtab * knrevtab let init () = the_ccitab := SpTab.empty; the_dirtab := DirTab.empty; - the_objtab := SpTab.empty; the_modtypetab := SpTab.empty; the_tactictab := SpTab.empty; the_globrevtab := Globrevtab.empty; @@ -537,7 +527,6 @@ let init () = let freeze () = !the_ccitab, !the_dirtab, - !the_objtab, !the_modtypetab, !the_tactictab, !the_globrevtab, @@ -545,10 +534,9 @@ let freeze () = !the_modtyperevtab, !the_tacticrevtab -let unfreeze (ccit,dirt,objt,mtyt,tact,globr,modr,mtyr,tacr) = +let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) = the_ccitab := ccit; the_dirtab := dirt; - the_objtab := objt; the_modtypetab := mtyt; the_tactictab := tact; the_globrevtab := globr; diff --git a/library/nametab.mli b/library/nametab.mli index 225a8b080..c529120dd 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -16,7 +16,7 @@ open Libnames (*i*) (*s This module contains the tables for globalization, which - associates internal object references to qualified names (qualid). *) + associates internal object references to qualified names (qualid). *) (* Most functions in this module fall into one of the following categories: \begin{itemize} @@ -24,7 +24,7 @@ open Libnames Registers the [object_reference] to be referred to by the [full_user_name] (and its suffixes according to [visibility]). - [full_user_name] can either be a [section_path] or a [dir_path]. + [full_user_name] can either be a [full_path] or a [dir_path]. \item [exists : full_user_name -> bool] @@ -34,8 +34,12 @@ open Libnames \item [locate : qualid -> object_reference] Finds the object referred to by [qualid] or raises [Not_found] + + \item [full_name : qualid -> full_user_name] + + Finds the full user name referred to by [qualid] or raises [Not_found] - \item [name_of : object_reference -> user_name] + \item [shortest_qualid_of : object_reference -> user_name] 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 @@ -52,9 +56,6 @@ 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 things *) (* The visibility can be registered either @@ -70,88 +71,79 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a type visibility = Until of int | Exactly of int -val push : visibility -> section_path -> global_reference -> unit -val push_syntactic_definition : - visibility -> section_path -> kernel_name -> unit -val push_modtype : visibility -> section_path -> module_path -> unit +val push : visibility -> full_path -> global_reference -> unit +val push_modtype : visibility -> full_path -> module_path -> unit val push_dir : visibility -> dir_path -> global_dir_reference -> unit -val push_object : visibility -> section_path -> unit -val push_tactic : visibility -> section_path -> kernel_name -> unit - - -(*s The following functions perform globalization of qualified names *) - -(* This returns the section path of a constant or fails with [Not_found] *) -val locate : qualid -> global_reference - -(* This function is used to transform a qualified identifier into a - global reference, with a nice error message in case of failure *) -val global : reference -> global_reference - -(* The same for inductive types *) -val inductive_of_reference : reference -> inductive +val push_syndef : visibility -> full_path -> syndef_name -> unit -(* This locates also syntactic definitions; raise [Not_found] if not found *) -val extended_locate : qualid -> extended_global_reference +type ltac_constant = kernel_name +val push_tactic : visibility -> full_path -> ltac_constant -> unit -(* This locates all names with a given suffix, if qualid is valid as - such, it comes first in the list *) -val extended_locate_all : qualid -> extended_global_reference list -(* This locates all global references with a given suffixe *) -val locate_all : qualid -> global_reference list +(*s The following functions perform globalization of qualified names *) -val locate_obj : qualid -> section_path +(* These functions globalize a (partially) qualified name or fail with + [Not_found] *) +val locate : qualid -> global_reference +val locate_extended : qualid -> extended_global_reference val locate_constant : qualid -> constant -val locate_mind : qualid -> mutual_inductive -val locate_section : qualid -> dir_path +val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> module_path -val locate_syntactic_definition : qualid -> kernel_name - -type ltac_constant = kernel_name -val locate_tactic : qualid -> ltac_constant val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path +val locate_section : qualid -> dir_path +val locate_tactic : qualid -> ltac_constant -(* A variant looking up a [section_path] *) -val absolute_reference : section_path -> global_reference -val extended_absolute_reference : section_path -> extended_global_reference +(* These functions globalize user-level references into global + references, like [locate] and co, but raise a nice error message + in case of failure *) +val global : reference -> global_reference +val global_inductive : reference -> inductive -(*s These functions tell if the given absolute name is already taken *) +(* These functions locate all global references with a given suffix; + if [qualid] is valid as such, it comes first in the list *) -val exists_cci : section_path -> bool -val exists_modtype : section_path -> bool +val locate_all : qualid -> global_reference list +val locate_extended_all : qualid -> extended_global_reference list -(* 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 *) +(* Mapping a full path to a global reference *) +val global_of_path : full_path -> global_reference +val extended_global_of_path : full_path -> extended_global_reference -(*s These functions turn qualids into full user names: [section_path]s - or [dir_path]s *) +(*s These functions tell if the given absolute name is already taken *) -val full_name_modtype : qualid -> section_path -val full_name_cci : qualid -> section_path +val exists_cci : full_path -> bool +val exists_modtype : full_path -> bool +val exists_dir : dir_path -> bool +val exists_section : dir_path -> bool (* deprecated synonym of [exists_dir] *) +val exists_module : dir_path -> bool (* deprecated synonym of [exists_dir] *) -(* As above but checks that the path found is indeed a module *) -val full_name_module : qualid -> dir_path +(*s These functions locate qualids into full user names *) +val full_name_cci : qualid -> full_path +val full_name_modtype : qualid -> full_path +val full_name_module : qualid -> dir_path (*s Reverse lookup -- finding user names corresponding to the given internal name *) -val sp_of_syntactic_definition : kernel_name -> section_path -val shortest_qualid_of_global : Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid -val shortest_qualid_of_tactic : ltac_constant -> qualid +(* Returns the dirpath associated to a module path *) val dir_of_mp : module_path -> dir_path -val sp_of_global : global_reference -> section_path -val id_of_global : global_reference -> identifier +(* Returns full path bound to a global reference or syntactic definition *) + +val path_of_syndef : syndef_name -> full_path +val path_of_global : global_reference -> full_path + +(* Returns in particular the dirpath or the basename of the full path + associated to global reference *) + +val dirpath_of_global : global_reference -> dir_path +val basename_of_global : global_reference -> identifier (* Printing of global references using names as short as possible *) val pr_global_env : Idset.t -> global_reference -> std_ppcmds @@ -161,13 +153,8 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes the same object. *) -val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_global : Idset.t -> global_reference -> qualid +val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid val shortest_qualid_of_modtype : module_path -> qualid - - -(* -type frozen - -val freeze : unit -> frozen -val unfreeze : frozen -> unit -*) +val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_tactic : ltac_constant -> qualid -- cgit v1.2.3