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 --- dev/doc/changes.txt | 22 ++++ dev/top_printers.ml | 2 +- interp/constrintern.ml | 20 +-- interp/coqlib.ml | 6 +- interp/coqlib.mli | 2 +- interp/dumpglob.ml | 6 +- interp/implicit_quantifiers.ml | 6 +- interp/notation.ml | 8 +- interp/notation.mli | 2 +- interp/syntax_def.ml | 13 +- interp/syntax_def.mli | 3 +- interp/topconstr.ml | 2 +- kernel/cooking.ml | 6 +- lib/util.mli | 1 + 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 +++++++++---------- parsing/g_prim.ml4 | 2 +- parsing/prettyp.ml | 24 +--- parsing/printmod.ml | 2 +- plugins/dp/dp.ml | 2 +- plugins/extraction/common.ml | 4 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/table.ml | 12 +- plugins/extraction/table.mli | 2 +- plugins/field/field.ml4 | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/indfun.ml | 2 +- plugins/funind/indfun_common.ml | 6 +- plugins/funind/recdef.ml | 4 +- plugins/interface/centaur.ml4 | 12 +- plugins/interface/coqparser.ml | 2 +- plugins/interface/name_to_ast.ml | 16 +-- plugins/interface/name_to_ast.mli | 2 +- plugins/omega/coq_omega.ml | 6 +- plugins/ring/ring.ml | 4 +- plugins/romega/const_omega.ml | 8 +- plugins/setoid_ring/newring.ml4 | 40 ++---- plugins/subtac/equations.ml4 | 8 +- plugins/xml/cic2acic.ml | 10 +- plugins/xml/xmlcommand.ml | 4 +- pretyping/classops.ml | 2 +- pretyping/detyping.ml | 2 +- pretyping/indrec.ml | 32 +---- pretyping/recordops.ml | 8 +- pretyping/tacred.ml | 2 +- pretyping/termops.ml | 22 ++-- pretyping/typeclasses.ml | 4 +- proofs/redexpr.ml | 2 +- tactics/auto.ml | 6 +- tactics/autorewrite.ml | 2 +- tactics/dhyp.ml | 2 +- tactics/extratactics.ml4 | 2 +- tactics/rewrite.ml4 | 2 +- tactics/tacinterp.ml | 4 +- tactics/tactics.ml | 2 +- tactics/tauto.ml4 | 2 +- tools/coq_makefile.ml4 | 4 +- toplevel/autoinstance.ml | 2 +- toplevel/command.ml | 8 +- toplevel/libtypes.ml | 4 +- toplevel/metasyntax.ml | 10 +- toplevel/mltop.ml4 | 2 +- toplevel/search.ml | 17 ++- toplevel/vernacentries.ml | 54 ++++----- toplevel/whelp.ml4 | 6 +- 83 files changed, 506 insertions(+), 585 deletions(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 92ea62b5e..ebbcb46ce 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,28 @@ = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= +** Cleaning in libnames/nametab interfaces + +Functions: + +dirpath_prefix -> pop_dirpath +extract_dirpath_prefix pop_dirpath_n +extend_dirpath -> add_dirpath_suffix +qualid_of_sp -> qualid_of_path +pr_sp -> pr_path +make_short_qualid -> qualid_of_ident +sp_of_syntactic_definition -> path_of_syntactic_definition +sp_of_global -> path_of_global +id_of_global -> basename_of_global +absolute_reference -> global_of_path +locate_syntactic_definition -> locate_syndef +path_of_syntactic_definition -> path_of_syndef +push_syntactic_definition -> push_syndef + +Types: + +section_path -> full_path + ** Cleaning in parsing extensions (commit 12108) Many moves and renamings, one new file (Extrawit, that contains wit_tactic). diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e3addd6f0..b35d5d489 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -46,7 +46,7 @@ let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (string_of_mp mp)) let ppcon con = pp(pr_con con) let ppkn kn = pp(pr_kn kn) -let ppsp sp = pp(pr_sp sp) +let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Classops.pr_cl_index cl) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1d89306ed..e4e625205 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -336,11 +336,11 @@ let check_no_explicitation l = (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env args = - try match Nametab.extended_locate qid with + try match Nametab.locate_extended qid with | TrueGlobal ref -> Dumpglob.add_glob loc ref; RRef (loc, ref), args - | SyntacticDef sp -> + | SynDef sp -> Dumpglob.add_glob_kn loc sp; let (ids,c) = Syntax_def.search_syntactic_definition loc sp in let nids = List.length ids in @@ -365,7 +365,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function | Ident (loc, id) -> try intern_var env lvar loc id, args with Not_found -> - let qid = make_short_qualid id in + let qid = qualid_of_ident id in try let r,args2 = intern_non_secvar_qualid loc qid intern env args in find_appl_head_data lvar r, args2 @@ -536,10 +536,10 @@ type pattern_qualid_kind = let find_constructor ref f aliases pats scopes = let (loc,qid) = qualid_of_reference ref in let gref = - try extended_locate qid + try locate_extended qid with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in match gref with - | SyntacticDef sp -> + | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition loc sp in (match a with | ARef (ConstructRef cstr) -> @@ -1357,21 +1357,21 @@ let interp_context_evars ?(fail_anonymous=false) evdref env params = (* Locating reference, possibly via an abbreviation *) let locate_reference qid = - match Nametab.extended_locate qid with + match Nametab.locate_extended qid with | TrueGlobal ref -> ref - | SyntacticDef kn -> + | SynDef kn -> match Syntax_def.search_syntactic_definition dummy_loc kn with | [],ARef ref -> ref | _ -> raise Not_found let is_global id = try - let _ = locate_reference (make_short_qualid id) in true + let _ = locate_reference (qualid_of_ident id) in true with Not_found -> false let global_reference id = - constr_of_global (locate_reference (make_short_qualid id)) + constr_of_global (locate_reference (qualid_of_ident id)) let construct_reference ctx id = try @@ -1380,5 +1380,5 @@ let construct_reference ctx id = global_reference id let global_reference_in_absolute_module dir id = - constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id)) + constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index e110ad00a..d38ef592f 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -26,7 +26,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (id_of_string s) in - try global_of_extended_global (Nametab.extended_absolute_reference sp) + try global_of_extended_global (Nametab.extended_global_of_path sp) with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp)) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s @@ -36,7 +36,7 @@ let gen_reference = coq_reference let gen_constant = coq_constant let has_suffix_in_dirs dirs ref = - let dir = dirpath (sp_of_global ref) in + let dir = dirpath (path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let global_of_extended q = @@ -45,7 +45,7 @@ let global_of_extended q = let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let id = id_of_string s in - let all = Nametab.extended_locate_all (make_short_qualid id) in + let all = Nametab.locate_extended_all (qualid_of_ident id) in let all = list_uniquize (list_map_filter global_of_extended all) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5b550a86b..8b0384960 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -59,7 +59,7 @@ val logic_module : dir_path val logic_type_module : dir_path (* Natural numbers *) -val nat_path : section_path +val nat_path : full_path val glob_nat : global_reference val path_of_O : constructor val path_of_S : constructor diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 71f38063a..79b58da84 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -118,7 +118,7 @@ let type_of_global_ref gr = let remove_sections dir = if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then (* Not yet (fully) discharged *) - Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) else (* Theorem/Lemma outside its outer section of definition *) dir @@ -139,7 +139,7 @@ let add_glob_gen loc sp lib_dp ty = let add_glob loc ref = if dump () && loc <> Util.dummy_loc then - let sp = Nametab.sp_of_global ref in + let sp = Nametab.path_of_global ref in let lib_dp = Lib.library_part ref in let ty = type_of_global_ref ref in add_glob_gen loc sp lib_dp ty @@ -150,7 +150,7 @@ let mp_of_kn kn = let add_glob_kn loc kn = if dump () && loc <> Util.dummy_loc then - let sp = Nametab.sp_of_syntactic_definition kn in + let sp = Nametab.path_of_syndef kn in let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen loc sp lib_dp "syndef" diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4495c22c6..a550111a3 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -30,13 +30,13 @@ let ids_of_list l = List.fold_right Idset.add l Idset.empty let locate_reference qid = - match Nametab.extended_locate qid with + match Nametab.locate_extended qid with | TrueGlobal ref -> true - | SyntacticDef kn -> true + | SynDef kn -> true let is_global id = try - locate_reference (make_short_qualid id) + locate_reference (qualid_of_ident id) with Not_found -> false diff --git a/interp/notation.ml b/interp/notation.ml index e6c627e86..2857f9ad8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -113,7 +113,7 @@ let subst_scope (_,subst,sc) = sc open Libobject -let classify_scope (_,(local,_,_ as o)) = +let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o let export_scope (local,_,_ as x) = if local then None else Some x @@ -201,7 +201,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) (**********************************************************************) (* Interpreting numbers (not in summary because functional objects) *) -type required_module = section_path * string list +type required_module = full_path * string list type 'a prim_token_interpreter = loc -> 'a -> rawconstr @@ -248,7 +248,7 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = (patl, (fun r -> Option.map mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = - try let _ = Nametab.absolute_reference sp in () + try let _ = Nametab.global_of_path sp in () with Not_found -> user_err_loc (loc,"prim_token_interpreter", str ("Cannot interpret in "^sc^" without requiring first module " @@ -485,7 +485,7 @@ let (inArgumentsScope,outArgumentsScope) = cache_function = cache_arguments_scope; load_function = load_arguments_scope; subst_function = subst_arguments_scope; - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); discharge_function = discharge_arguments_scope; rebuild_function = rebuild_arguments_scope; export_function = (fun x -> Some x) } diff --git a/interp/notation.mli b/interp/notation.mli index 06349014d..21d3ae1a0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -66,7 +66,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name an appropriate error message *) type notation_location = dir_path * string -type required_module = section_path * string list +type required_module = full_path * string list type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_interpreter = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index bb8d68323..ef5ecf62a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -16,6 +16,7 @@ open Topconstr open Libobject open Lib open Nameops +open Nametab (* Syntactic definitions. *) @@ -37,13 +38,13 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) = errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); add_syntax_constant kn pat; - Nametab.push_syntactic_definition (Nametab.Until i) sp kn; + Nametab.push_syndef (Nametab.Until i) sp kn; if not onlyparse then (* Declare it to be used as long name *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = - Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn; + Nametab.push_syndef (Nametab.Exactly i) sp kn; if not onlyparse then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared inbetween *) @@ -55,7 +56,7 @@ let cache_syntax_constant d = let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) = (local,subst_interpretation subst pat,onlyparse) -let classify_syntax_constant (_,(local,_,_ as o)) = +let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o let export_syntax_constant (local,_,_ as o) = @@ -85,19 +86,19 @@ let search_syntactic_definition loc kn = let global_of_extended_global = function | TrueGlobal ref -> ref - | SyntacticDef kn -> + | SynDef kn -> match search_syntactic_definition dummy_loc kn with | [],ARef ref -> ref | _ -> raise Not_found let locate_global_with_alias (loc,qid) = - let ref = Nametab.extended_locate qid in + let ref = Nametab.locate_extended qid in try global_of_extended_global ref with Not_found -> user_err_loc (loc,"",pr_qualid qid ++ str " is bound to a notation that does not denote a reference") -let inductive_of_reference_with_alias r = +let global_inductive_with_alias r = match locate_global_with_alias (qualid_of_reference r) with | IndRef ind -> ind | ref -> diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 39583d856..fb0c3c9f2 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,6 +13,7 @@ open Util open Names open Topconstr open Rawterm +open Nametab open Libnames (*i*) @@ -39,4 +40,4 @@ val global_of_extended_global : extended_global_reference -> global_reference val global_with_alias : reference -> global_reference (* The same for inductive types *) -val inductive_of_reference_with_alias : reference -> inductive +val global_inductive_with_alias : reference -> inductive diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 32595cdc6..eb46a5d6e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -770,7 +770,7 @@ let ids_of_cases_tomatch tms = tms [] let is_constructor id = - try ignore (Nametab.extended_locate (make_short_qualid id)); true + try ignore (Nametab.locate_extended (qualid_of_ident id)); true with Not_found -> true let rec cases_pattern_fold_names f a = function diff --git a/kernel/cooking.ml b/kernel/cooking.ml index a5cda5d13..edd3e498d 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,17 +21,17 @@ open Reduction type work_list = identifier array Cmap.t * identifier array KNmap.t -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 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 type my_global_reference = | ConstRef of constant diff --git a/lib/util.mli b/lib/util.mli index 04d3a52fc..84762bade 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -171,6 +171,7 @@ val list_lastn : int -> 'a list -> 'a list val list_skipn : int -> 'a list -> 'a list val list_addn : int -> 'a -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *) val list_drop_prefix : 'a list -> 'a list -> 'a list val list_drop_last : 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) 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 diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 524e7b468..0e91fddbd 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -71,7 +71,7 @@ GEXTEND Gram ; basequalid: [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> make_short_qualid id + | id = ident -> qualid_of_ident id ] ] ; name: diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index cf88256bc..538828fca 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -191,7 +191,7 @@ let locate_any_name ref = let (loc,qid) = qualid_of_reference ref in try Term (N.locate qid) with Not_found -> - try Syntactic (N.locate_syntactic_definition qid) + try Syntactic (N.locate_syndef qid) with Not_found -> try Dir (N.locate_dir qid) with Not_found -> @@ -205,9 +205,9 @@ let pr_located_qualid = function | IndRef _ -> "Inductive" | ConstructRef _ -> "Constructor" | VarRef _ -> "Variable" in - str ref_str ++ spc () ++ pr_sp (Nametab.sp_of_global ref) + str ref_str ++ spc () ++ pr_global ref | Syntactic kn -> - str "Notation" ++ spc () ++ pr_sp (Nametab.sp_of_syntactic_definition kn) + str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> let s,dir = match dir with | DirOpenModule (dir,_) -> "Open Module", dir @@ -218,7 +218,7 @@ let pr_located_qualid = function in str s ++ spc () ++ pr_dirpath dir | ModuleType (qid,_) -> - str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid) + str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid) | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." @@ -228,9 +228,9 @@ let print_located_qualid ref = let expand = function | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref - | SyntacticDef kn -> + | SynDef kn -> Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in - match List.map expand (N.extended_locate_all qid) with + match List.map expand (N.locate_extended_all qid) with | [] -> let (dir,id) = repr_qualid qid in if dir = empty_dirpath then @@ -635,18 +635,6 @@ let print_name ref = if (repr_dirpath dir) <> [] then raise Not_found; let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) - with Not_found -> - try - let sp = Nametab.locate_obj qid in - let (oname,lobj) = - let (oname,entry) = - List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) - in - match entry with - | Lib.Leaf obj -> (oname,obj) - | _ -> raise Not_found - in - print_leaf_entry true (oname,lobj) with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 596ce6b24..2ec914d6c 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -137,7 +137,7 @@ and print_modexpr locals mexpr = match mexpr with let rec printable_body dir = - let dir = dirpath_prefix dir in + let dir = pop_dirpath dir in dir = empty_dirpath || try match Nametab.locate_dir (qualid_of_dirpath dir) with diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 79ffaf3f9..3a408909d 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -115,7 +115,7 @@ let rename_global r = s end in - loop (Nametab.id_of_global r) + loop (Nametab.basename_of_global r) let foralls = List.fold_right diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 11c3b3b5b..e1edeec37 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -303,9 +303,9 @@ let ref_renaming_fun (k,r) = if l = [""] (* this happens only at toplevel of the monolithic case *) then let globs = Idset.elements (get_global_ids ()) in - let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in + let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in string_of_id id - else modular_rename k (safe_id_of_global r) + else modular_rename k (safe_basename_of_global r) in add_global_ids (id_of_string s); s::l diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 39e277081..ba4786d37 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -506,7 +506,7 @@ let simple_extraction r = match locate_ref [r] with let extraction_library is_rec m = init true; let dir_m = - let q = make_short_qualid m in + let q = qualid_of_ident m in try Nametab.full_name_module q with Not_found -> error_unknown_module q in Visit.add_mp (MPfile dir_m); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 83a780198..13a730ac2 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -182,7 +182,7 @@ let modular () = !modular_ref WARNING: for inductive objects, an extract_inductive must have been done before. *) -let safe_id_of_global = function +let safe_basename_of_global = function | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> @@ -191,7 +191,7 @@ let safe_id_of_global = function let safe_pr_global r = try Printer.pr_global r - with _ -> pr_id (safe_id_of_global r) + with _ -> pr_id (safe_basename_of_global r) (* idem, but with qualification, and only for constants. *) @@ -207,7 +207,7 @@ let pr_long_mp mp = let lid = repr_dirpath (Nametab.dir_of_mp mp) in str (String.concat "." (List.map string_of_id (List.rev lid))) -let pr_long_global ref = pr_sp (Nametab.sp_of_global ref) +let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) @@ -452,7 +452,7 @@ let (inline_extraction,_) = cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } @@ -535,7 +535,7 @@ let (blacklist_extraction,_) = cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Libobject.Keep o); + classify_function = (fun o -> Libobject.Keep o); subst_function = (fun (_,_,x) -> x) } @@ -595,7 +595,7 @@ let (in_customs,_) = cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 6e3f2ec56..42ed6eef0 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -13,7 +13,7 @@ open Libnames open Miniml open Declarations -val safe_id_of_global : global_reference -> identifier +val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index c9b993690..916294774 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -75,7 +75,7 @@ let (in_addfield,out_addfield)= Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); Libobject.cache_function = cache_addfield; Libobject.subst_function = subst_addfield; - Libobject.classify_function = (fun (_,a) -> Libobject.Substitute a); + Libobject.classify_function = (fun a -> Libobject.Substitute a); Libobject.export_function = export_addfield } (* Adds a theory to the table *) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index fc31ee6fc..75d69099a 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -45,7 +45,7 @@ let wrap n b continue seq gls= add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in continue seq2 gls -let id_of_global=function +let basename_of_global=function VarRef id->id | _->assert false diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 1c2c93a49..b804c93ae 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -21,7 +21,7 @@ type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val id_of_global: global_reference -> identifier +val basename_of_global: global_reference -> identifier val clear_global: global_reference -> tactic diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index adfb9ce2f..9087f5179 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let finfos = find_Function_infos (destConst f) in update_Function {finfos with - equation_lemma = Some (match Nametab.locate (make_short_qualid equation_lemma_id) with + equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" ) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 348a17b11..46da3a01d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -471,7 +471,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b in let ltof = let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in - Libnames.Qualid (dummy_loc,Libnames.qualid_of_sp + Libnames.Qualid (dummy_loc,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) in let fun_from_mes = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b29bdf3f1..868a876be 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -350,7 +350,7 @@ let subst_Function (_,subst,finfos) = is_general = finfos.is_general } -let classify_Function (_,infos) = Libobject.Substitute infos +let classify_Function infos = Libobject.Substitute infos let export_Function infos = Some infos @@ -440,7 +440,7 @@ let _ = let find_or_none id = try Some - (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" ) with Not_found -> None @@ -467,7 +467,7 @@ let add_Function is_general f = and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec") and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = - match Nametab.locate (make_short_qualid (mk_rel_id f_id)) + match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive" in let finfos = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 25e664336..876f3de4b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1386,7 +1386,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = - let term_ref = Nametab.locate (make_short_qualid term_id) in + let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in (* message "start second proof"; *) let stop = ref false in @@ -1404,7 +1404,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num end; if not !stop then - let eq_ref = Nametab.locate (make_short_qualid equation_id ) in + let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in let f_ref = destConst (constr_of_global f_ref) and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4 index f8c088779..c8fc7bdf3 100644 --- a/plugins/interface/centaur.ml4 +++ b/plugins/interface/centaur.ml4 @@ -146,7 +146,7 @@ let ctf_acknowledge_command request_id command_count opt_exn = g_count, !current_goal_index else (0, 0) - and statnum = Lib.current_command_label () + and statnum = Lib.current_state_label () and dpth = let d = Pfedit.current_proof_depth() in if d >= 0 then d else 0 and pending = CT_id_list (List.map xlate_ident (Pfedit.get_all_proof_names())) in (ctf_header "acknowledge" request_id ++ @@ -409,12 +409,12 @@ let inspect n = (match oname, object_tag lobj with (sp,_), "VARIABLE" -> let (_, _, v) = Global.lookup_named (basename sp) in - add_search2 (Nametab.locate (qualid_of_sp sp)) v + add_search2 (Nametab.locate (qualid_of_path sp)) v | (sp,kn), "CONSTANT" -> let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in - add_search2 (Nametab.locate (qualid_of_sp sp)) typ + add_search2 (Nametab.locate (qualid_of_path sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> - add_search2 (Nametab.locate (qualid_of_sp sp)) + add_search2 (Nametab.locate (qualid_of_path sp)) (Pretyping.Default.understand Evd.empty (Global.env()) (RRef(dummy_loc, IndRef(kn,0)))) | _ -> failwith ("unexpected value 1 for "^ @@ -764,12 +764,12 @@ let full_name_of_ref r = | ConstRef _ -> str "CST" | IndRef _ -> str "IND" | ConstructRef _ -> str "CSR") - ++ str " " ++ (pr_sp (Nametab.sp_of_global r)) + ++ str " " ++ (pr_path (Nametab.path_of_global r)) (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *) let string_of_ref = (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*) - Depends.o Libnames.string_of_path Nametab.sp_of_global + Depends.o Libnames.string_of_path Nametab.path_of_global let print_depends compute_depends ptree = output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl()) diff --git a/plugins/interface/coqparser.ml b/plugins/interface/coqparser.ml index a63e18d27..df5e66b50 100644 --- a/plugins/interface/coqparser.ml +++ b/plugins/interface/coqparser.ml @@ -335,7 +335,7 @@ let print_version_action () = let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); try - (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in + (let qid = Libnames.qualid_of_ident (Names.id_of_string module_name) in require_library [dummy_loc,qid] None; msg (str "opening... "); Declaremods.import_module false (Nametab.locate_module qid); diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index 668a581e1..f5e8be31e 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -106,7 +106,7 @@ let convert_one_inductive sp tyi = let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in let env = Global.env () in let envpar = push_rel_context params env in - let sp = sp_of_global (IndRef (sp, tyi)) in + let sp = path_of_global (IndRef (sp, tyi)) in (((false,(dummy_loc,basename sp)), convert_env(List.rev params), Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw , @@ -192,18 +192,6 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = let name_to_ast ref = let (loc,qid) = qualid_of_reference ref in let l = - try - let sp = Nametab.locate_obj qid in - let (sp,lobj) = - let (sp,entry) = - List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) - in - match entry with - | Lib.Leaf obj -> (sp,obj) - | _ -> raise Not_found - in - leaf_entry_to_ast_list (sp,lobj) - with Not_found -> try match Nametab.locate qid with | ConstRef sp -> constant_to_ast_list sp @@ -220,7 +208,7 @@ let name_to_ast ref = | Some c1 -> make_definition_ast name c1 typ []) with Not_found -> try - let _sp = Nametab.locate_syntactic_definition qid in + let _sp = Nametab.locate_syndef qid in errorlabstrm "print" (str "printing of syntax definitions not implemented") with Not_found -> diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli index f9e83b5e1..a532604f5 100644 --- a/plugins/interface/name_to_ast.mli +++ b/plugins/interface/name_to_ast.mli @@ -2,4 +2,4 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;; val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;; val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;; val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;; -val leaf_entry_to_ast_list : (Libnames.section_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; +val leaf_entry_to_ast_list : (Libnames.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 8c8640ea5..075188f54 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -398,11 +398,11 @@ let destructurate_prop t = | _, [_;_] when c = Lazy.force coq_ge -> Kapp (Ge,args) | _, [_;_] when c = Lazy.force coq_gt -> Kapp (Gt,args) | Const sp, args -> - Kapp (Other (string_of_id (id_of_global (ConstRef sp))),args) + Kapp (Other (string_of_id (basename_of_global (ConstRef sp))),args) | Construct csp , args -> - Kapp (Other (string_of_id (id_of_global (ConstructRef csp))), args) + Kapp (Other (string_of_id (basename_of_global (ConstructRef csp))), args) | Ind isp, args -> - Kapp (Other (string_of_id (id_of_global (IndRef isp))),args) + Kapp (Other (string_of_id (basename_of_global (IndRef isp))),args) | Var id,[] -> Kvar id | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | Prod (Name _,_,_),[] -> error "Omega: Not a quantifier-free goal" diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 6dcc1e872..a07ec4757 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -274,7 +274,7 @@ let (theory_to_obj, obj_to_theory) = open_function = (fun i o -> if i=1 then cache_th o); cache_function = cache_th; subst_function = subst_th; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); export_function = export_th } (* from the set A, guess the associated theory *) @@ -733,7 +733,7 @@ let build_setspolynom gl th lc = module SectionPathSet = Set.Make(struct - type t = section_path + type t = full_path let compare = Pervasives.compare end) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index bdec6bf45..1caa5db1c 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -20,15 +20,15 @@ let destructurate t = match Term.kind_of_term c, args with | Term.Const sp, args -> Kapp (Names.string_of_id - (Nametab.id_of_global (Libnames.ConstRef sp)), + (Nametab.basename_of_global (Libnames.ConstRef sp)), args) | Term.Construct csp , args -> Kapp (Names.string_of_id - (Nametab.id_of_global (Libnames.ConstructRef csp)), + (Nametab.basename_of_global (Libnames.ConstructRef csp)), args) | Term.Ind isp, args -> Kapp (Names.string_of_id - (Nametab.id_of_global (Libnames.IndRef isp)), + (Nametab.basename_of_global (Libnames.IndRef isp)), args) | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) @@ -46,7 +46,7 @@ let dest_const_apply t = | Term.Construct csp -> Libnames.ConstructRef csp | Term.Ind isp -> Libnames.IndRef isp | _ -> raise Destruct - in Nametab.id_of_global ref, args + in Nametab.basename_of_global ref, args let logic_dir = ["Coq";"Logic";"Decidable"] diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 32f36ef85..24cb84ed5 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -352,18 +352,11 @@ let from_name = ref Spmap.empty let ring_for_carrier r = Cmap.find r !from_carrier let ring_for_relation rel = Cmap.find rel !from_relation -let ring_lookup_by_name ref = - Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name -let find_ring_structure env sigma l oname = - match oname, l with - Some rf, _ -> - (try ring_lookup_by_name rf - with Not_found -> - errorlabstrm "ring" - (str "found no ring named "++pr_reference rf)) - | None, t::cl' -> +let find_ring_structure env sigma l = + match l with + | t::cl' -> let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in @@ -377,7 +370,7 @@ let find_ring_structure env sigma l oname = errorlabstrm "ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> assert false + | [] -> assert false (* let (req,_,_) = dest_rel cl in (try ring_for_relation req @@ -457,7 +450,7 @@ let (theory_to_obj, obj_to_theory) = open_function = (fun i o -> if i=1 then cache_th o); cache_function = cache_th; subst_function = subst_th; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); export_function = export_th } @@ -835,7 +828,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in let rl = make_args_list rl t in - let e = find_ring_structure env sigma rl None in + let e = find_ring_structure env sigma rl in let rl = carg (make_term_list e.ring_carrier rl) in let lH = carg (make_hyp_list env lH) in let ring = ltac_ring_structure e in @@ -941,20 +934,11 @@ let field_from_name = ref Spmap.empty let field_for_carrier r = Cmap.find r !field_from_carrier let field_for_relation rel = Cmap.find rel !field_from_relation -let field_lookup_by_name ref = - Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) - !field_from_name - -let find_field_structure env sigma l oname = +let find_field_structure env sigma l = check_required_library (cdir@["Field_tac"]); - match oname, l with - Some rf, _ -> - (try field_lookup_by_name rf - with Not_found -> - errorlabstrm "field" - (str "found no field named "++pr_reference rf)) - | None, t::cl' -> + match l with + | t::cl' -> let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in @@ -968,7 +952,7 @@ let find_field_structure env sigma l oname = errorlabstrm "field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> assert false + | [] -> assert false (* let (req,_,_) = dest_rel cl in (try field_for_relation req with Not_found -> @@ -1046,7 +1030,7 @@ let (ftheory_to_obj, obj_to_ftheory) = open_function = (fun i o -> if i=1 then cache_th o); cache_function = cache_th; subst_function = subst_th; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); export_function = export_th } let field_equality r inv req = @@ -1175,7 +1159,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in let rl = make_args_list rl t in - let e = find_field_structure env sigma rl None in + let e = find_field_structure env sigma rl in let rl = carg (make_term_list e.field_carrier rl) in let lH = carg (make_hyp_list env lH) in let field = ltac_field_structure e in diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4 index 5b76c9587..5ae15e00a 100644 --- a/plugins/subtac/equations.ml4 +++ b/plugins/subtac/equations.ml4 @@ -10,7 +10,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *) +(* $Id$ *) open Cases open Util @@ -824,13 +824,13 @@ open Decl_kinds type equation = constr_expr * (constr_expr, identifier located) rhs let locate_reference qid = - match Nametab.extended_locate qid with + match Nametab.locate_extended qid with | TrueGlobal ref -> true - | SyntacticDef kn -> true + | SynDef kn -> true let is_global id = try - locate_reference (make_short_qualid id) + locate_reference (qualid_of_ident id) with Not_found -> false diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 13e5e6d5f..1ac022159 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -15,7 +15,7 @@ (* Utility Functions *) exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; -let get_module_path_of_section_path path = +let get_module_path_of_full_path path = let dirpath = fst (Libnames.repr_path path) in let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in match @@ -177,7 +177,7 @@ let uri_of_kernel_name tag = let uri_of_declaration id tag = let module LN = Libnames in - let dir = LN.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) in + let dir = LN.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in let tokens = token_list_of_path dir id tag in "cic:/" ^ String.concat "/" tokens @@ -468,14 +468,14 @@ print_endline "PASSATO" ; flush stdout ; match g with Libnames.ConstructRef ((induri,_),_) | Libnames.IndRef (induri,_) -> - Nametab.sp_of_global (Libnames.IndRef (induri,0)) + Nametab.path_of_global (Libnames.IndRef (induri,0)) | Libnames.VarRef id -> (* Invariant: variables are never cooked in Coq *) raise Not_found - | _ -> Nametab.sp_of_global g + | _ -> Nametab.path_of_global g in Dischargedhypsmap.get_discharged_hyps sp, - get_module_path_of_section_path sp + get_module_path_of_full_path sp with Not_found -> (* no explicit substitution *) [], Libnames.dirpath_of_string "dummy" diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 1ae186614..4a27c3247 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -102,7 +102,7 @@ let filter_params pvars hyps = in let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in aux (Names.repr_dirpath modulepath) (List.rev pvars) ;; @@ -118,7 +118,7 @@ let search_variables () = let module N = Names in let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in - let modulepath = Cic2acic.get_module_path_of_section_path cwdsp in + let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in let rec aux = function [] -> [] diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 911ded641..901341e7b 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -384,7 +384,7 @@ let (inCoercion,_) = load_function = load_coercion; cache_function = cache_coercion; subst_function = subst_coercion; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_coercion; export_function = (function x -> Some x) } diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d43bc0780..2c3de28a5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -32,7 +32,7 @@ let dl = dummy_loc (* Tools for printing of Cases *) let encode_inductive r = - let indsp = inductive_of_reference r in + let indsp = global_inductive r in let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index f8dab16cd..6a4c066ce 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -579,14 +579,14 @@ let lookup_eliminator ind_sp s = let id = add_suffix ind_id (elimination_suffix s) in (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) - let ref = ConstRef (make_con mp dp (label_of_id id)) in - try - let _ = sp_of_global ref in - constr_of_global ref + try + let cst = make_con mp dp (label_of_id id) in + let _ = Global.lookup_constant cst in + mkConst cst with Not_found -> (* Then try to get a user-defined eliminator in some other places *) (* using short name (e.g. for "eq_rec") *) - try constr_of_global (Nametab.locate (make_short_qualid id)) + try constr_of_global (Nametab.locate (qualid_of_ident id)) with Not_found -> errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ @@ -594,25 +594,3 @@ let lookup_eliminator ind_sp s = pr_global_env Idset.empty (IndRef ind_sp) ++ strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") - - -(* let env = Global.env() in - let path = sp_of_global None (IndRef ind_sp) in - let dir, base = repr_path path in - let id = add_suffix base (elimination_suffix s) in - (* Try first to get an eliminator defined in the same section as the *) - (* inductive type *) - try construct_absolute_reference (Names.make_path dir id) - with Not_found -> - (* Then try to get a user-defined eliminator in some other places *) - (* using short name (e.g. for "eq_rec") *) - try constr_of_global (Nametab.locate (make_short_qualid id)) - with Not_found -> - errorlabstrm "default_elim" - (str "Cannot find the elimination combinator " ++ - pr_id id ++ spc () ++ - str "The elimination of the inductive definition " ++ - pr_id base ++ spc () ++ str "on sort " ++ - spc () ++ pr_sort_family s ++ - str " is probably not allowed") -*) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 8bf95ecbf..c82589b9a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -77,7 +77,7 @@ let (inStruc,outStruc) = cache_function = cache_structure; load_function = load_structure; subst_function = subst_structure; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_structure; export_function = (function x -> Some x) } @@ -141,7 +141,7 @@ let (in_method,out_method) = cache_function = load_method; subst_function = (fun (_,s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); export_function = (fun x -> Some x); - classify_function = (fun (_,x) -> Substitute x) + classify_function = (fun x -> Substitute x) } let methods_matching c = MethodsDnet.search_pattern !meth_dnet c @@ -271,7 +271,7 @@ let (inCanonStruc,outCanonStruct) = open_function = open_canonical_structure; cache_function = cache_canonical_structure; subst_function = subst_canonical_structure; - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = discharge_canonical_structure; export_function = (function x -> Some x) } @@ -281,7 +281,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref = errorlabstrm "object_declare" - (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.") + (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b7013a703..024f190f2 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -807,7 +807,7 @@ let unfold env sigma name = else error (string_of_evaluable_ref env name^" is opaque.") -(* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)] +(* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. * Performs a betaiota reduction after unfolding. *) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index b7a4fc925..4034d8667 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -34,7 +34,7 @@ let pr_name = function | Name id -> pr_id id | Anonymous -> str "_" -let pr_sp sp = str(string_of_kn sp) +let pr_path sp = str(string_of_kn sp) let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with @@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with (str"Evar#" ++ int e ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") | Const c -> str"Cst(" ++ pr_con c ++ str")" - | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" + | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> - str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" + str"Constr(" ++ pr_path sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" | Case (ci,p,c,bl) -> v 0 (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ pr_constr c ++ str"of") ++ cut() ++ @@ -711,7 +711,7 @@ let add_vname vars = function Name id -> Idset.add id vars | _ -> vars -let id_of_global = Nametab.id_of_global +let basename_of_global = Nametab.basename_of_global let sort_hdchar = function | Prop(_) -> "P" @@ -731,9 +731,9 @@ let hdchar env c = if i=0 then lowercase_first_char (id_of_label (label kn)) else - lowercase_first_char (id_of_global (IndRef x)) + lowercase_first_char (basename_of_global (IndRef x)) | Construct ((sp,i) as x) -> - lowercase_first_char (id_of_global (ConstructRef x)) + lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id | Sort s -> sort_hdchar s | Rel n -> @@ -839,14 +839,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (make_short_qualid id) in + let ref = locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (make_short_qualid id) with + match locate (qualid_of_ident id) with | ConstructRef _ as ref -> not (is_imported_ref ref) | _ -> false with Not_found -> @@ -907,12 +907,12 @@ let occur_rel p env id = let occur_id nenv id0 c = let rec occur n c = match kind_of_term c with | Var id when id=id0 -> raise Occur - | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur + | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur | Ind ind_sp - when id_of_global (IndRef ind_sp) = id0 -> + when basename_of_global (IndRef ind_sp) = id0 -> raise Occur | Construct cstr_sp - when id_of_global (ConstructRef cstr_sp) = id0 -> + when basename_of_global (ConstructRef cstr_sp) = id0 -> raise Occur | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur | _ -> iter_constr_with_binders succ occur n c diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2f2796f1c..52e2eb24e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -168,7 +168,7 @@ let (class_input,class_output) = cache_function = cache_class; load_function = (fun _ -> load_class); open_function = (fun _ -> load_class); - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_class a)); rebuild_function = rebuild_class; subst_function = subst_class; @@ -212,7 +212,7 @@ let (instance_input,instance_output) = cache_function = cache_instance; load_function = (fun _ -> load_instance); open_function = (fun _ -> load_instance); - classify_function = (fun (_,x) -> Substitute x); + classify_function = (fun x -> Substitute x); discharge_function = (fun a -> Some (discharge_instance a)); rebuild_function = rebuild_instance; subst_function = subst_instance; diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c7d6ffe14..2e10a9f4a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -77,7 +77,7 @@ let export_strategy (local,obj) = EvalVarRef _ -> None | EvalConstRef _ as q -> Some q) obj -let classify_strategy (_,(local,_ as obj)) = +let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj let disch_ref ref = diff --git a/tactics/auto.ml b/tactics/auto.ml index 741753521..b998daa74 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -446,7 +446,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = if hintlist' == hintlist then obj else (local,name,AddTactic hintlist') -let classify_autohint (_,((local,name,hintlist) as obj)) = +let classify_autohint ((local,name,hintlist) as obj) = if local or hintlist = (AddTactic []) then Dispose else Substitute obj let export_autohint ((local,name,hintlist) as obj) = @@ -548,7 +548,7 @@ let interp_hints h = HintsTransparencyEntry (List.map fr lhints, b) | HintsConstructors lqid -> let constr_hints_of_ind qid = - let isp = inductive_of_reference qid in + let isp = global_inductive qid in let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in list_tabulate (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in @@ -1121,7 +1121,7 @@ let superauto n to_add argl = let interp_to_add gl r = let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in - let id = id_of_global r in + let id = basename_of_global r in (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r) let gen_superauto nopt l a b gl = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 04c4ed161..63481abde 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -224,7 +224,7 @@ let subst_hintrewrite (_,subst,(rbase,list as node)) = if list' == list then node else (rbase,list') -let classify_hintrewrite (_,x) = Libobject.Substitute x +let classify_hintrewrite x = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 3d34a2d68..be4343b4f 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -206,7 +206,7 @@ let cache_dd (_,(_,na,dd)) = (str"The code which adds destructor hints broke;" ++ spc () ++ str"this is not supposed to happen") -let classify_dd (_,(local,_,_ as o)) = +let classify_dd (local,_,_ as o) = if local then Dispose else Substitute o let export_dd (local,_,_ as x) = if local then None else Some x diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f1c255154..c6c9bdd10 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -408,7 +408,7 @@ let (inTransitivity,_) = cache_function = cache_transitivity_lemma; open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); subst_function = subst_transitivity_lemma; - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); export_function = (fun x -> Some x) } (* Synchronisation with reset *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 43ae99203..385e86587 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -67,7 +67,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in - Nametab.absolute_reference sp + Nametab.global_of_path sp let try_find_reference dir s = constr_of_global (try_find_global_reference dir s) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 32c69ddcd..e79174c66 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -374,7 +374,7 @@ let loc_of_by_notation f = function let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let intern_inductive_or_by_notation = function - | AN r -> Nametab.inductive_of_reference r + | AN r -> Nametab.global_inductive r | ByNotation (loc,ntn,sc) -> destIndRef (Notation.interp_notation_as_global_reference loc (function IndRef ind -> true | _ -> false) ntn sc) @@ -2847,7 +2847,7 @@ let (inMD,outMD) = load_function = load_md; open_function = open_md; subst_function = subst_md; - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); export_function = (fun x -> Some x)} let print_ltac id = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca64a8d3d..663c426f9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2054,7 +2054,7 @@ let make_up_names n ind_opt cname = if is_hyp then match ind_opt with | None -> id_of_string ind_prefix - | Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id) + | Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id) else add_prefix ind_prefix cname in let hyprecname = make_base n base_ind in let avoid = diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index bbc1285e2..ad2fd9009 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -277,7 +277,7 @@ let tauto_classical nnpp g = let tauto g = try - let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in + let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in (* try intuitionistic version first to avoid an axiom if possible *) tclORELSE tauto_intuitionistic (tauto_classical nnpp) g with Not_found -> diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 919aacbbe..8a39c383a 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -331,12 +331,12 @@ let rec special = function | _ :: r -> special r let custom sps = - let pr_sp (file,dependencies,com) = + let pr_path (file,dependencies,com) = print file; print ": "; print dependencies; print "\n"; print "\t"; print com; print "\n\n" in if sps <> [] then section "Custom targets."; - List.iter pr_sp sps + List.iter pr_path sps let subdirs sds = let pr_subdir s = diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 29bef7b5a..4946ee933 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -161,7 +161,7 @@ let new_inst_no = fun () -> incr cnt; string_of_int !cnt let make_instance_ident gr = - Nameops.add_suffix (Nametab.id_of_global gr) ("_autoinstance_"^new_inst_no()) + Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no()) let new_instance_message ident typ def = Flags.if_verbose diff --git a/toplevel/command.ml b/toplevel/command.ml index 48a5119d1..82fd9bc1a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -612,7 +612,7 @@ let eq_local_binders bl1 bl2 = List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2 let extract_coercions indl = - let mkqid (_,((_,id),_)) = make_short_qualid id in + let mkqid (_,((_,id),_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) @@ -930,7 +930,7 @@ requested let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> - let ind = mkInd (Nametab.inductive_of_reference y) in + let ind = mkInd (Nametab.global_inductive y) in let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind) in let z' = family_of_sort (interp_sort z) in @@ -969,7 +969,7 @@ let build_induction_scheme lnamedepindsort = let lrecspec = List.map (fun (_,dep,indid,sort) -> - let ind = Nametab.inductive_of_reference indid in + let ind = Nametab.global_inductive indid in let (mib,mip) = Global.lookup_inductive ind in (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort @@ -998,7 +998,7 @@ tried to declare different schemes at once *) else ( if ischeme <> [] then build_induction_scheme ischeme; List.iter ( fun indname -> - let ind = Nametab.inductive_of_reference indname + let ind = Nametab.global_inductive indname in declare_eq_scheme (fst ind); try make_eq_decidability ind diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index 6fd49b15b..4e10d1d52 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -74,7 +74,7 @@ let (input,output) = load_function = (fun _ -> load); subst_function = (fun (_,s,t) -> subst s t); export_function = (fun x -> Some x); - classify_function = (fun (_,x) -> Substitute x) + classify_function = (fun x -> Substitute x) } let update () = Lib.add_anonymous_leaf (input !defined_types) @@ -102,7 +102,7 @@ let add a b = Profile.profile1 add_key add a b let _ = Declare.add_cache_hook ( fun sp -> - let gr = Nametab.absolute_reference sp in + let gr = Nametab.global_of_path sp in let ty = Global.type_of_global gr in add ty gr ) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d08558426..e6c469974 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -35,7 +35,7 @@ let (inToken, outToken) = open_function = (fun i o -> if i=1 then cache_token o); cache_function = cache_token; subst_function = Libobject.ident_subst_function; - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); export_function = (fun x -> Some x)} let add_token_obj s = Lib.add_anonymous_leaf (inToken s) @@ -74,7 +74,7 @@ let (inTacticGrammar, outTacticGrammar) = open_function = (fun i o -> if i=1 then cache_tactic_notation o); cache_function = cache_tactic_notation; subst_function = subst_tactic_notation; - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); export_function = (fun x -> Some x)} let cons_production_parameter l = function @@ -681,7 +681,7 @@ let subst_syntax_extension (_,subst,(local,sy)) = (local, List.map (fun (prec,ntn,gr,pp) -> (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy) -let classify_syntax_definition (_,(local,_ as o)) = +let classify_syntax_definition (local,_ as o) = if local then Dispose else Substitute o let export_syntax_definition (local,_ as o) = @@ -873,7 +873,7 @@ let cache_notation o = let subst_notation (_,subst,(lc,scope,pat,b,ndf)) = (lc,scope,subst_interpretation subst pat,b,ndf) -let classify_notation (_,(local,_,_,_,_ as o)) = +let classify_notation (local,_,_,_,_ as o) = if local then Dispose else Substitute o let export_notation (local,_,_,_,_ as o) = @@ -1058,7 +1058,7 @@ let (inScopeCommand,outScopeCommand) = open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun (_,obj) -> Substitute obj); + classify_function = (fun obj -> Substitute obj); export_function = (fun x -> Some x) } let add_delimiters scope key = diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 334b4d82a..837d50207 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -309,7 +309,7 @@ let (inMLModule,outMLModule) = cache_function = cache_ml_module_object; export_function = export_ml_module_object; subst_function = (fun (_,_,o) -> o); - classify_function = (fun (_,o) -> Substitute o) } + classify_function = (fun o -> Substitute o) } let declare_ml_modules l = Lib.add_anonymous_leaf (inMLModule {mnames=l}) diff --git a/toplevel/search.ml b/toplevel/search.ml index 481d91787..66dc28e2d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -47,7 +47,7 @@ let rec head_const c = match kind_of_term c with let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let env = Global.env () in - let crible_rec (sp,_) lobj = match object_tag lobj with + let crible_rec (sp,kn) lobj = match object_tag lobj with | "VARIABLE" -> (try let (id,_,typ) = Global.lookup_named (basename sp) in @@ -57,14 +57,13 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let cst = locate_constant (qualid_of_sp sp) in + let cst = constant_of_kn kn in let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> - let kn = locate_mind (qualid_of_sp sp) in let mib = Global.lookup_mind kn in (match refopt with | Some (IndRef ((kn',tyi) as ind)) when kn=kn' -> @@ -86,7 +85,7 @@ let crible ref = gen_crible (Some ref) (* Fine Search. By Yves Bertot. *) -exception No_section_path +exception No_full_path let rec head c = let c = strip_outer_cast c in @@ -95,9 +94,9 @@ let rec head c = | LetIn (_,_,_,c) -> head c | _ -> c -let constr_to_section_path c = match kind_of_term c with +let constr_to_full_path c = match kind_of_term c with | Const sp -> sp - | _ -> raise No_section_path + | _ -> raise No_full_path let xor a b = (a or b) & (not (a & b)) @@ -109,14 +108,14 @@ let plain_display ref a c = let filter_by_module (module_list:dir_path list) (accept:bool) (ref:global_reference) _ _ = try - let sp = sp_of_global ref in + let sp = path_of_global ref in let sl = dirpath sp in let rec filter_aux = function | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl) | [] -> true in xor accept (filter_aux module_list) - with No_section_path -> + with No_full_path -> false let ref_eq = Libnames.encode_kn Coqlib.logic_module (id_of_string "eq"), 0 @@ -209,7 +208,7 @@ let gen_filtered_search filter_function display_function = (** SearchAbout *) -let name_of_reference ref = string_of_id (id_of_global ref) +let name_of_reference ref = string_of_id (basename_of_global ref) type glob_search_about_item = | GlobSearchSubPattern of constr_pattern diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fa56e60f6..1de9d739a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -506,12 +506,11 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export -let vernac_end_module export (loc,id) = - let mp = Declaremods.end_module id in - Dumpglob.dump_modref loc mp "mod"; - if_verbose message ("Module "^ string_of_id id ^" is defined") ; - Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export - +let vernac_end_module export (loc,id as lid) = + let mp = Declaremods.end_module () in + Dumpglob.dump_modref loc mp "mod"; + if_verbose message ("Module "^ string_of_id id ^" is defined") ; + Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if Lib.sections_are_opened () then @@ -549,46 +548,43 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = if_verbose message ("Module Type "^ string_of_id id ^" is defined") - let vernac_end_modtype (loc,id) = - let mp = Declaremods.end_modtype id in - Dumpglob.dump_modref loc mp "modtype"; - if_verbose message - ("Module Type "^ string_of_id id ^" is defined") - + let mp = Declaremods.end_modtype () in + Dumpglob.dump_modref loc mp "modtype"; + if_verbose message ("Module Type "^ string_of_id id ^" is defined") + let vernac_include = function | CIMTE mty_ast -> Declaremods.declare_include Modintern.interp_modtype mty_ast false | CIME mexpr_ast -> Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true - - (**********************) (* Gallina extensions *) - (* Sections *) +(* Sections *) let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); Dumpglob.dump_definition lid true "sec"; Lib.open_section id -let vernac_end_section (loc, id) = - - Dumpglob.dump_reference loc - (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; - Lib.close_section id +let vernac_end_section (loc,_) = + Dumpglob.dump_reference loc + (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; + Lib.close_section () + +(* Dispatcher of the "End" command *) -let vernac_end_segment lid = +let vernac_end_segment (_,id as lid) = check_no_pending_proofs (); - let o = try Lib.what_is_opened () with - Not_found -> error "There is nothing to end." in - match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export lid - | _,Lib.OpenedModtype _ -> vernac_end_modtype lid - | _,Lib.OpenedSection _ -> vernac_end_section lid - | _ -> anomaly "No more opened things" + match Lib.find_opening_node id with + | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid + | Lib.OpenedModtype _ -> vernac_end_modtype lid + | Lib.OpenedSection _ -> vernac_end_section lid + | _ -> anomaly "No more opened things" + +(* Libraries *) let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in @@ -597,6 +593,8 @@ let vernac_require import _ qidl = List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import +(* Coercions and canonical structures *) + let vernac_canonical r = Recordops.declare_canonical_structure (global_with_alias r) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 63d93a767..b844f03ca 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -131,9 +131,9 @@ let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) let section_parameters = function | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) -> - get_discharged_hyp_names (sp_of_global (IndRef(induri,0))) + get_discharged_hyp_names (path_of_global (IndRef(induri,0))) | RRef (_,(ConstRef cst as ref)) -> - get_discharged_hyp_names (sp_of_global ref) + get_discharged_hyp_names (path_of_global ref) | _ -> [] let merge vl al = @@ -217,7 +217,7 @@ END VERNAC COMMAND EXTEND Whelp | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (inductive_of_reference_with_alias r) ] +| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (global_inductive_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END -- cgit v1.2.3