diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 10 | ||||
| -rw-r--r-- | library/declaremods.ml | 38 | ||||
| -rw-r--r-- | library/globnames.mli | 1 | ||||
| -rw-r--r-- | library/heads.ml | 1 | ||||
| -rw-r--r-- | library/kindops.ml | 48 | ||||
| -rw-r--r-- | library/kindops.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 76 | ||||
| -rw-r--r-- | library/libnames.ml | 29 | ||||
| -rw-r--r-- | library/libnames.mli | 40 | ||||
| -rw-r--r-- | library/library.ml | 21 | ||||
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | library/loadpath.ml | 6 | ||||
| -rw-r--r-- | library/nameops.ml | 215 | ||||
| -rw-r--r-- | library/nameops.mli | 135 | ||||
| -rw-r--r-- | library/nametab.ml | 10 | ||||
| -rw-r--r-- | library/univops.ml | 40 | ||||
| -rw-r--r-- | library/univops.mli | 15 |
17 files changed, 150 insertions, 539 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml index 141fff0335..4a23909858 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,7 @@ open Libnames open Globnames open Nametab -let coq = Nameops.coq_string (* "Coq" *) +let coq = Libnames.coq_string (* "Coq" *) (************************************************************************) (* Generic functions to find Coq objects *) @@ -32,7 +32,7 @@ let find_reference locstr dir s = of not found errors here *) user_err ~hdr:locstr Pp.(str "cannot find " ++ Libnames.pr_path sp ++ - str "; maybe library " ++ Libnames.pr_dirpath dp ++ + str "; maybe library " ++ DirPath.print dp ++ str " has to be required first.") let coq_reference locstr dir s = find_reference locstr (coq::dir) s @@ -52,14 +52,14 @@ let gen_reference_in_modules locstr dirs s = | [] -> anomaly ~label:locstr (str "cannot find " ++ str s ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") + prlist_with_sep pr_comma DirPath.print dirs ++ str ".") | l -> anomaly ~label:locstr (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs ++ str ".") + prlist_with_sep pr_comma DirPath.print dirs ++ str ".") (* For tactics/commands requiring vernacular libraries *) @@ -79,7 +79,7 @@ let check_required_library d = *) (* or failing ...*) user_err ~hdr:"Coqlib.check_required_library" - (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") + (str "Library " ++ DirPath.print dir ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/library/declaremods.ml b/library/declaremods.ml index cda40f49f1..41e00a41c6 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -167,29 +167,29 @@ let consistency_checks exists dir dirinfo = try Nametab.locate_dir (qualid_of_dirpath dir) with Not_found -> user_err ~hdr:"consistency_checks" - (pr_dirpath dir ++ str " should already exist!") + (DirPath.print dir ++ str " should already exist!") in assert (eq_global_dir_reference globref dirinfo) else if Nametab.exists_dir dir then user_err ~hdr:"consistency_checks" - (pr_dirpath dir ++ str " already exists") + (DirPath.print dir ++ str " already exists") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i (** Iterate some function [iter_objects] on all components of a module *) -let do_module exists iter_objects i dir mp sobjs kobjs = - let prefix = (dir,(mp,DirPath.empty)) in +let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = + let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in let dirinfo = DirModule prefix in - consistency_checks exists dir dirinfo; - Nametab.push_dir (compute_visibility exists i) dir dirinfo; - ModSubstObjs.set mp sobjs; + consistency_checks exists obj_dir dirinfo; + Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; + ModSubstObjs.set obj_mp sobjs; (* If we're not a functor, let's iter on the internal components *) if sobjs_no_functor sobjs then begin let objs = expand_sobjs sobjs in - ModObjs.set mp (prefix,objs,kobjs); + ModObjs.set obj_mp (prefix,objs,kobjs); iter_objects (i+1) prefix objs; iter_objects (i+1) prefix kobjs end @@ -222,20 +222,20 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!") let load_keep i ((sp,kn),kobjs) = (* Invariant : seg isn't empty *) - let dir = dir_of_sp sp and mp = mp_of_kn kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = { obj_dir ; obj_mp; obj_sec = DirPath.empty } in let prefix',sobjs,kobjs0 = - try ModObjs.get mp + try ModObjs.get obj_mp with Not_found -> assert false (* a substobjs should already be loaded *) in assert (eq_op prefix' prefix); assert (List.is_empty kobjs0); - ModObjs.set mp (prefix,sobjs,kobjs); + ModObjs.set obj_mp (prefix,sobjs,kobjs); Lib.load_objects i prefix kobjs let open_keep i ((sp,kn),kobjs) = - let dir = dir_of_sp sp and mp = mp_of_kn kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in + let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in Lib.open_objects i prefix kobjs let in_modkeep : Lib.lib_objects -> obj = @@ -284,9 +284,9 @@ let (in_modtype : substitutive_objects -> obj), (** {6 Declaration of substitutive objects for Include} *) let do_include do_load do_open i ((sp,kn),aobjs) = - let dir = Libnames.dirpath sp in - let mp = KerName.modpath kn in - let prefix = (dir,(mp,DirPath.empty)) in + let obj_dir = Libnames.dirpath sp in + let obj_mp = KerName.modpath kn in + let prefix = { obj_dir; obj_mp; obj_sec = DirPath.empty } in let o = expand_aobjs aobjs in if do_load then Lib.load_objects i prefix o; if do_open then Lib.open_objects i prefix o @@ -577,7 +577,7 @@ let start_module interp_modast export id args res fs = in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in - Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); + Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModule prefix); mp let end_module () = @@ -684,7 +684,7 @@ let start_modtype interp_modast id args mtys fs = let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in - Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); + Nametab.push_dir (Nametab.Until 1) (prefix.obj_dir) (DirOpenModtype prefix); mp let end_modtype () = diff --git a/library/globnames.mli b/library/globnames.mli index 5c484b391a..2e0cd62db7 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -47,6 +47,7 @@ val global_of_constr : constr -> global_reference (** Obsolete synonyms for constr_of_global and global_of_constr *) val reference_of_constr : constr -> global_reference +[@@ocaml.deprecated "Alias of Globnames.global_of_constr"] module RefOrdered : sig type t = global_reference diff --git a/library/heads.ml b/library/heads.ml index 8b8e407f76..ee3bfe1bdd 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -8,7 +8,6 @@ open Util open Names -open Term open Constr open Vars open Mod_subst diff --git a/library/kindops.ml b/library/kindops.ml index 882f620862..83985ce974 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -23,45 +23,13 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind def = - let (locality, poly, kind) = def in - let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in - match kind with - | Definition -> - begin match locality with - | Discharge -> "Let" - | Local -> "Local Definition" - | Global -> "Definition" - end - | Example -> - begin match locality with - | Discharge -> error () - | Local -> "Local Example" - | Global -> "Example" - end - | Coercion -> - begin match locality with - | Discharge -> error () - | Local -> "Local Coercion" - | Global -> "Coercion" - end - | SubClass -> - begin match locality with - | Discharge -> error () - | Local -> "Local SubClass" - | Global -> "SubClass" - end - | CanonicalStructure -> - begin match locality with - | Discharge -> error () - | Local -> error () - | Global -> "Canonical Structure" - end - | Instance -> - begin match locality with - | Discharge -> error () - | Local -> "Instance" - | Global -> "Global Instance" - end +let string_of_definition_object_kind = function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli index 77979c9159..06f873e857 100644 --- a/library/kindops.mli +++ b/library/kindops.mli @@ -12,4 +12,4 @@ open Decl_kinds val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_kind : definition_kind -> string +val string_of_definition_object_kind : definition_object_kind -> string diff --git a/library/lib.ml b/library/lib.ml index df9563e453..499e2ae21f 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -9,9 +9,9 @@ open Pp open CErrors open Util +open Names open Libnames open Globnames -open Nameops open Libobject open Context.Named.Declaration @@ -93,12 +93,16 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = default_library,(Names.ModPath.initial,Names.DirPath.empty) +let initial_prefix = { + obj_dir = default_library; + obj_mp = ModPath.initial; + obj_sec = DirPath.empty; +} type lib_state = { - comp_name : Names.DirPath.t option; + comp_name : DirPath.t option; lib_stk : library_segment; - path_prefix : Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t); + path_prefix : object_prefix; } let initial_lib_state = { @@ -115,10 +119,9 @@ let library_dp () = (* [path_prefix] is a pair of absolute dirpath and a pair of current module path and relative section path *) -let cwd () = fst !lib_state.path_prefix -let current_prefix () = snd !lib_state.path_prefix -let current_mp () = fst (snd !lib_state.path_prefix) -let current_sections () = snd (snd !lib_state.path_prefix) +let cwd () = !lib_state.path_prefix.obj_dir +let current_mp () = !lib_state.path_prefix.obj_mp +let current_sections () = !lib_state.path_prefix.obj_sec let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) @@ -136,7 +139,7 @@ let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id let make_kn id = - let mp,dir = current_prefix () in + let mp, dir = current_mp (), current_sections () in Names.KerName.make mp dir (Names.Label.of_id id) let make_oname id = Libnames.make_oname !lib_state.path_prefix id @@ -152,8 +155,11 @@ let recalc_path_prefix () = lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk } let pop_path_prefix () = - let dir,(mp,sec) = !lib_state.path_prefix in - lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)} + let op = !lib_state.path_prefix in + lib_state := { !lib_state + with path_prefix = { op with obj_dir = pop_dirpath op.obj_dir; + obj_sec = pop_dirpath op.obj_sec; + } } let find_entry_p p = let rec find = function @@ -226,7 +232,7 @@ let add_anonymous_entry node = add_entry (make_oname (anonymous_id ())) node let add_leaf id obj = - if Names.ModPath.equal (current_mp ()) Names.ModPath.initial then + if ModPath.equal (current_mp ()) ModPath.initial then user_err Pp.(str "No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -278,14 +284,14 @@ let current_mod_id () = let start_mod is_type export id mp fs = - let dir = add_dirpath_suffix (cwd ()) id in - let prefix = dir,(mp,Names.DirPath.empty) in + let dir = add_dirpath_suffix (!lib_state.path_prefix.obj_dir) id in + let prefix = { obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_module dir in if exists then - user_err ~hdr:"open_module" (pr_id id ++ str " already exists"); + user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix @@ -296,7 +302,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in user_err - (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") + (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -328,17 +334,17 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (current_sections ())) then + if not (Names.DirPath.is_empty (!lib_state.path_prefix.obj_sec)) then user_err Pp.(str "some sections are already opened"); - let prefix = s, (mp, Names.DirPath.empty) in - let () = add_anonymous_entry (CompilingLibrary prefix) in + let prefix = Libnames.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } let open_blocks_message es = let open_block_name = function - | oname, OpenedSection _ -> str "section " ++ pr_id (basename (fst oname)) - | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ pr_id (basename (fst oname)) + | oname, OpenedSection _ -> str "section " ++ Id.print (basename (fst oname)) + | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ Id.print (basename (fst oname)) | _ -> assert false in str "The " ++ pr_enum open_block_name es ++ spc () ++ str "need" ++ str (if List.length es == 1 then "s" else "") ++ str " to be closed." @@ -360,8 +366,8 @@ let end_compilation_checks dir = | None -> anomaly (Pp.str "There should be a module name...") | Some m -> if not (Names.DirPath.equal m dir) then anomaly - (str "The current open module has name" ++ spc () ++ pr_dirpath m ++ - spc () ++ str "and not" ++ spc () ++ pr_dirpath m ++ str "."); + (str "The current open module has name" ++ spc () ++ DirPath.print m ++ + spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str "."); in oname @@ -395,7 +401,7 @@ let find_opening_node id = let id' = basename (fst oname) in if not (Names.Id.equal id id') then user_err ~hdr:"Lib.find_opening_node" - (str "Last block to end has name " ++ pr_id id' ++ str "."); + (str "Last block to end has name " ++ Id.print id' ++ str "."); entry with Not_found -> user_err Pp.(str "There is nothing to end.") @@ -522,15 +528,15 @@ let is_in_section ref = (*************) (* Sections. *) let open_section id = - let olddir,(mp,oldsec) = !lib_state.path_prefix in - let dir = add_dirpath_suffix olddir id in - let prefix = dir, (mp, add_dirpath_suffix oldsec id) in - if Nametab.exists_section dir then - user_err ~hdr:"open_section" (pr_id id ++ str " already exists."); + let opp = !lib_state.path_prefix in + let obj_dir = add_dirpath_suffix opp.obj_dir id in + let prefix = { obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + if Nametab.exists_section obj_dir then + user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); + Nametab.push_dir (Nametab.Until 1) obj_dir (DirOpenSection prefix); lib_state := { !lib_state with path_prefix = prefix }; add_section () @@ -556,7 +562,7 @@ let close_section () = in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - let full_olddir = fst !lib_state.path_prefix in + let full_olddir = !lib_state.path_prefix.obj_dir in pop_path_prefix (); add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in @@ -596,10 +602,10 @@ let init () = (* Misc *) let mp_of_global = function - |VarRef id -> current_mp () - |ConstRef cst -> Names.Constant.modpath cst - |IndRef ind -> Names.ind_modpath ind - |ConstructRef constr -> Names.constr_modpath constr + | VarRef id -> !lib_state.path_prefix.obj_mp + | ConstRef cst -> Names.Constant.modpath cst + | IndRef ind -> Names.ind_modpath ind + | ConstructRef constr -> Names.constr_modpath constr let rec dp_of_mp = function |Names.MPfile dp -> dp diff --git a/library/libnames.ml b/library/libnames.ml index efb1348ab2..a471d83966 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,7 +13,7 @@ open Names (**********************************************) -let pr_dirpath sl = str (DirPath.to_string sl) +let pr_dirpath sl = DirPath.print sl (*s Operations on dirpaths *) @@ -156,10 +156,15 @@ let qualid_of_dirpath dir = type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (ModPath.t * DirPath.t) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} -let make_oname (dirpath,(mp,dir)) id = - make_path dirpath id, KerName.make mp dir (Label.of_id id) +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp; obj_sec } id = + make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id) (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = @@ -170,10 +175,10 @@ type global_dir_reference = | DirClosedSection of DirPath.t (* this won't last long I hope! *) -let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - DirPath.equal d1 d2 && - DirPath.equal p1 p2 && - ModPath.equal mp1 mp2 +let eq_op op1 op2 = + DirPath.equal op1.obj_dir op2.obj_dir && + DirPath.equal op1.obj_sec op2.obj_sec && + ModPath.equal op1.obj_mp op2.obj_mp let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 @@ -232,6 +237,14 @@ let join_reference ns r = Qualid (loc, make_qualid (dirpath_of_string (Names.Id.to_string id1)) id2) +(* Default paths *) +let default_library = Names.DirPath.initial (* = ["Top"] *) + +(*s Roots of the space of absolute names *) +let coq_string = "Coq" +let coq_root = Id.of_string coq_string +let default_root_prefix = DirPath.empty + (* Deprecated synonyms *) let make_short_qualid = qualid_of_ident diff --git a/library/libnames.mli b/library/libnames.mli index ab25853346..71f5422404 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -11,12 +11,13 @@ open Loc open Names (** {6 Dirpaths } *) -(** FIXME: ought to be in Names.dir_path *) +val dirpath_of_string : string -> DirPath.t val pr_dirpath : DirPath.t -> Pp.t +[@@ocaml.deprecated "Alias for DirPath.print"] -val dirpath_of_string : string -> DirPath.t val string_of_dirpath : DirPath.t -> string +[@@ocaml.deprecated "Alias for DirPath.to_string"] (** Pop the suffix of a [DirPath.t]. Raises a [Failure] for an empty path *) val pop_dirpath : DirPath.t -> DirPath.t @@ -93,7 +94,25 @@ val qualid_of_ident : Id.t -> qualid type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (ModPath.t * DirPath.t) +(** Object prefix morally contains the "prefix" naming of an object to + be stored by [library], where [obj_dir] is the "absolute" path, + [obj_mp] is the current "module" prefix and [obj_sec] is the + "section" prefix. + + Thus, for an object living inside [Module A. Section B.] the + prefix would be: + + [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ] + + Note that both [obj_dir] and [obj_sec] are "paths" that is to say, + as opposed to [obj_mp] which is a single module name. + + *) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} val eq_op : object_prefix -> object_prefix -> bool @@ -127,7 +146,20 @@ val pr_reference : reference -> Pp.t val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference -(** Deprecated synonyms *) +(** some preset paths *) +val default_library : DirPath.t + +(** This is the root of the standard library of Coq *) +val coq_root : module_ident (** "Coq" *) +val coq_string : string (** "Coq" *) + +(** This is the default root prefix for developments which doesn't + mention a root *) +val default_root_prefix : DirPath.t +(** Deprecated synonyms *) val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *) +[@@ocaml.deprecated "Alias for qualid_of_ident"] + val qualid_of_sp : full_path -> qualid (** = qualid_of_path *) +[@@ocaml.deprecated "Alias for qualid_of_sp"] diff --git a/library/library.ml b/library/library.ml index 840fe563a1..88470d121b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -12,9 +12,8 @@ open Util open Names open Libnames -open Nameops -open Libobject open Lib +open Libobject (************************************************************************) (*s Low-level interning/externing of libraries to files *) @@ -132,7 +131,7 @@ let try_find_library dir = try find_library dir with Not_found -> user_err ~hdr:"Library.find_library" - (str "Unknown library " ++ pr_dirpath dir) + (str "Unknown library " ++ DirPath.print dir) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -331,7 +330,7 @@ let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) + str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) let error_lib_not_found qid = user_err ~hdr:"load_absolute_library_from" @@ -465,8 +464,8 @@ let rec intern_library (needed, contents) (dir, f) from = if not (DirPath.equal dir m.library_name) then user_err ~hdr:"load_physical_library" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ - pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ - spc() ++ pr_dirpath dir); + DirPath.print m.library_name ++ spc () ++ str "and not library" ++ + spc() ++ DirPath.print dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); m.library_digests, intern_library_deps (needed, contents) dir m f @@ -477,9 +476,9 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err (str "Compiled library " ++ pr_dirpath caller ++ + user_err (str "Compiled library " ++ DirPath.print caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ - over library " ++ pr_dirpath dir); + over library " ++ DirPath.print dir); libs let rec_intern_library libs (dir, f) = @@ -617,7 +616,7 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then user_err - (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ DirPath.print p ++ str "." ++ Id.print id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") let start_library fo = @@ -625,7 +624,7 @@ let start_library fo = try let lp = Loadpath.find_load_path (Filename.dirname fo) in Loadpath.logical lp - with Not_found -> Nameops.default_root_prefix + with Not_found -> Libnames.default_root_prefix in let file = Filename.chop_extension (Filename.basename fo) in let id = Id.of_string file in @@ -665,7 +664,7 @@ let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = user_err - (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ + (strbrk "Unable to use logical name " ++ DirPath.print dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") diff --git a/library/library.mllib b/library/library.mllib index d94fc22919..e43bfb5a1f 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,5 +1,3 @@ -Univops -Nameops Libnames Globnames Libobject diff --git a/library/loadpath.ml b/library/loadpath.ml index 757e972b1a..eb6dae84aa 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -54,8 +54,8 @@ let warn_overriding_logical_loadpath = CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" (fun (phys_path, old_path, coq_path) -> str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath old_path ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path) + DirPath.print old_path ++ strbrk "; it is remapped to " ++ + DirPath.print coq_path) let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in @@ -75,7 +75,7 @@ let add_load_path phys_path coq_path ~implicit = else let () = (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Nameops.default_root_prefix) then + if not (DirPath.equal old_path Libnames.default_root_prefix) then warn_overriding_logical_loadpath (phys_path, old_path, coq_path) in true in diff --git a/library/nameops.ml b/library/nameops.ml deleted file mode 100644 index d598a63b8d..0000000000 --- a/library/nameops.ml +++ /dev/null @@ -1,215 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names - -(* Identifiers *) - -let pr_id id = Id.print id - -(* Utilities *) - -let code_of_0 = Char.code '0' -let code_of_9 = Char.code '9' - -let cut_ident skip_quote s = - let s = Id.to_string s in - let slen = String.length s in - (* [n'] is the position of the first non nullary digit *) - let rec numpart n n' = - if Int.equal n 0 then - (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *) - slen - else - let c = Char.code (String.get s (n-1)) in - if Int.equal c code_of_0 && not (Int.equal n slen) then - numpart (n-1) n' - else if code_of_0 <= c && c <= code_of_9 then - numpart (n-1) (n-1) - else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then - numpart (n-1) (n-1) - else - n' - in - numpart slen slen - -let repr_ident s = - let numstart = cut_ident false s in - let s = Id.to_string s in - let slen = String.length s in - if Int.equal numstart slen then - (s, None) - else - (String.sub s 0 numstart, - Some (int_of_string (String.sub s numstart (slen - numstart)))) - -let make_ident sa = function - | Some n -> - let c = Char.code (String.get sa (String.length sa -1)) in - let s = - if c < code_of_0 || c > code_of_9 then sa ^ (string_of_int n) - else sa ^ "_" ^ (string_of_int n) in - Id.of_string s - | None -> Id.of_string sa - -let root_of_id id = - let suffixstart = cut_ident true id in - Id.of_string (String.sub (Id.to_string id) 0 suffixstart) - -(* Return the same identifier as the original one but whose {i subscript} is incremented. - If the original identifier does not have a suffix, [0] is appended to it. - - Example mappings: - - [bar] ↦ [bar0] - [bar0] ↦ [bar1] - [bar00] ↦ [bar01] - [bar1] ↦ [bar2] - [bar01] ↦ [bar01] - [bar9] ↦ [bar10] - [bar09] ↦ [bar10] - [bar99] ↦ [bar100] -*) -let increment_subscript id = - let id = Id.to_string id in - let len = String.length id in - let rec add carrypos = - let c = id.[carrypos] in - if is_digit c then - if Int.equal (Char.code c) (Char.code '9') then begin - assert (carrypos>0); - add (carrypos-1) - end - else begin - let newid = Bytes.of_string id in - Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; - Bytes.set newid carrypos (Char.chr (Char.code c + 1)); - newid - end - else begin - let newid = Bytes.of_string (id^"0") in - if carrypos < len-1 then begin - Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; - Bytes.set newid (carrypos+1) '1' - end; - newid - end - in Id.of_bytes (add (len-1)) - -let has_subscript id = - let id = Id.to_string id in - is_digit (id.[String.length id - 1]) - -let forget_subscript id = - let numstart = cut_ident false id in - let newid = Bytes.make (numstart+1) '0' in - String.blit (Id.to_string id) 0 newid 0 numstart; - (Id.of_bytes newid) - -let add_suffix id s = Id.of_string (Id.to_string id ^ s) -let add_prefix s id = Id.of_string (s ^ Id.to_string id) - -let atompart_of_id id = fst (repr_ident id) - -(* Names *) - -module type ExtName = -sig - - include module type of struct include Names.Name end - - exception IsAnonymous - - val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a - val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a - val iter : (Id.t -> unit) -> t -> unit - val map : (Id.t -> Id.t) -> t -> t - val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t - val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a - val get_id : t -> Id.t - val pick : t -> t -> t - val cons : t -> Id.t list -> Id.t list - val to_option : Name.t -> Id.t option - -end - -module Name : ExtName = -struct - - include Names.Name - - exception IsAnonymous - - let fold_left f a = function - | Name id -> f a id - | Anonymous -> a - - let fold_right f na a = - match na with - | Name id -> f id a - | Anonymous -> a - - let iter f na = fold_right (fun x () -> f x) na () - - let map f = function - | Name id -> Name (f id) - | Anonymous -> Anonymous - - let fold_left_map f a = function - | Name id -> let (a, id) = f a id in (a, Name id) - | Anonymous -> a, Anonymous - - let fold_right_map f na a = match na with - | Name id -> let (id, a) = f id a in (Name id, a) - | Anonymous -> Anonymous, a - - let get_id = function - | Name id -> id - | Anonymous -> raise IsAnonymous - - let pick na1 na2 = - match na1 with - | Name _ -> na1 - | Anonymous -> na2 - - let cons na l = - match na with - | Anonymous -> l - | Name id -> id::l - - let to_option = function - | Anonymous -> None - | Name id -> Some id - -end - -open Name - -(* Compatibility *) -let out_name = get_id -let name_fold = fold_right -let name_iter = iter -let name_app = map -let name_fold_map = fold_left_map -let name_cons = cons -let name_max = pick -let pr_name = print - -let pr_lab l = Label.print l - -let default_library = Names.DirPath.initial (* = ["Top"] *) - -(*s Roots of the space of absolute names *) -let coq_string = "Coq" -let coq_root = Id.of_string coq_string -let default_root_prefix = DirPath.empty - -(* Metavariables *) -let pr_meta = Pp.int -let string_of_meta = string_of_int diff --git a/library/nameops.mli b/library/nameops.mli deleted file mode 100644 index 26f300b615..0000000000 --- a/library/nameops.mli +++ /dev/null @@ -1,135 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names - -(** Identifiers and names *) - -val make_ident : string -> int option -> Id.t -val repr_ident : Id.t -> string * int option - -val atompart_of_id : Id.t -> string (** remove trailing digits *) -val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *) - -val add_suffix : Id.t -> string -> Id.t -val add_prefix : string -> Id.t -> Id.t - -(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *) - -val has_subscript : Id.t -> bool - -val increment_subscript : Id.t -> Id.t -(** Return the same identifier as the original one but whose {i subscript} is incremented. - If the original identifier does not have a suffix, [0] is appended to it. - - Example mappings: - - [bar] ↦ [bar0] - - [bar0] ↦ [bar1] - - [bar00] ↦ [bar01] - - [bar1] ↦ [bar2] - - [bar01] ↦ [bar01] - - [bar9] ↦ [bar10] - - [bar09] ↦ [bar10] - - [bar99] ↦ [bar100] -*) - -val forget_subscript : Id.t -> Id.t - -module Name : sig - - include module type of struct include Names.Name end - - exception IsAnonymous - - val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a - (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) - - val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a - (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) - - val iter : (Id.t -> unit) -> Name.t -> unit - (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) - - val map : (Id.t -> Id.t) -> Name.t -> t - (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) - - val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t - (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. - It is [a,Anonymous] otherwise. *) - - val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a - (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')]. - It is [Anonymous,a] otherwise. *) - - val get_id : Name.t -> Id.t - (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) - - val pick : Name.t -> Name.t -> Name.t - (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. - Pick one of [na] or [na'] otherwise. *) - - val cons : Name.t -> Id.t list -> Id.t list - (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) - - val to_option : Name.t -> Id.t option - (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) - -end - -val out_name : Name.t -> Id.t -(** @deprecated Same as [Name.get_id] *) - -val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a -(** @deprecated Same as [Name.fold_right] *) - -val name_iter : (Id.t -> unit) -> Name.t -> unit -(** @deprecated Same as [Name.iter] *) - -val name_app : (Id.t -> Id.t) -> Name.t -> Name.t -(** @deprecated Same as [Name.map] *) - -val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t -(** @deprecated Same as [Name.fold_left_map] *) - -val name_max : Name.t -> Name.t -> Name.t -(** @deprecated Same as [Name.pick] *) - -val name_cons : Name.t -> Id.t list -> Id.t list -(** @deprecated Same as [Name.cons] *) - -val pr_name : Name.t -> Pp.t -(** @deprecated Same as [Name.print] *) - -val pr_id : Id.t -> Pp.t -(** @deprecated Same as [Names.Id.print] *) - -val pr_lab : Label.t -> Pp.t - -(** some preset paths *) - -val default_library : DirPath.t - -(** This is the root of the standard library of Coq *) -val coq_root : module_ident (** "Coq" *) -val coq_string : string (** "Coq" *) - -(** This is the default root prefix for developments which doesn't - mention a root *) -val default_root_prefix : DirPath.t - -(** Metavariables *) -val pr_meta : Constr.metavariable -> Pp.t -val string_of_meta : Constr.metavariable -> string diff --git a/library/nametab.ml b/library/nametab.ml index 0ec4a37cdb..222c4cedcb 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -359,8 +359,8 @@ let push_modtype vis sp kn = let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with - DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab - | _ -> () + | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab + | _ -> () (* Locate functions *******************************************************) @@ -386,17 +386,17 @@ let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = match locate_dir qid with - | DirModule (_,(mp,_)) -> mp + | DirModule { obj_mp ; _} -> obj_mp | _ -> raise Not_found let full_name_module qid = match locate_dir qid with - | DirModule (dir,_) -> dir + | DirModule { obj_dir ; _} -> obj_dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection (dir, _) + | DirOpenSection { obj_dir; _ } -> obj_dir | DirClosedSection dir -> dir | _ -> raise Not_found diff --git a/library/univops.ml b/library/univops.ml deleted file mode 100644 index 9dc138eb8d..0000000000 --- a/library/univops.ml +++ /dev/null @@ -1,40 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Constr -open Univ - -let universes_of_constr c = - let rec aux s c = - match kind c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = Term.univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> Constr.fold aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty diff --git a/library/univops.mli b/library/univops.mli deleted file mode 100644 index 9af568bcb3..0000000000 --- a/library/univops.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Constr -open Univ - -(** Shrink a universe context to a restricted set of variables *) - -val universes_of_constr : constr -> LSet.t -val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t |