diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f | |
| parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) | |
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
93 files changed, 451 insertions, 453 deletions
diff --git a/checker/check.ml b/checker/check.ml index 4c4ba980d..c3f0e976f 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -11,19 +11,19 @@ open Errors open Util open Names -let pr_dirpath dp = str (Dir_path.to_string dp) -let default_root_prefix = Dir_path.empty +let pr_dirpath dp = str (DirPath.to_string dp) +let default_root_prefix = DirPath.empty let split_dirpath d = - let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l) -let extend_dirpath p id = Dir_path.make (id :: Dir_path.repr p) + let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l) +let extend_dirpath p id = DirPath.make (id :: DirPath.repr p) type section_path = { dirpath : string list ; basename : string } let dir_of_path p = - Dir_path.make (List.map Id.of_string p.dirpath) + DirPath.make (List.map Id.of_string p.dirpath) let path_of_dirpath dir = - match Dir_path.repr dir with + match DirPath.repr dir with [] -> failwith "path_of_dirpath" | l::dir -> {dirpath=List.map Id.to_string dir;basename=Id.to_string l} @@ -36,7 +36,7 @@ let pr_path sp = type library_objects -type compilation_unit_name = Dir_path.t +type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; @@ -61,10 +61,10 @@ type library_t = { module LibraryOrdered = struct - type t = Dir_path.t + type t = DirPath.t let compare d1 d2 = Pervasives.compare - (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) + (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) end module LibrarySet = Set.Make(LibraryOrdered) @@ -81,7 +81,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (Dir_path.to_string dir)) + error ("Unknown library " ^ (DirPath.to_string dir)) let library_full_filename dir = (find_library dir).library_filename @@ -113,7 +113,7 @@ let check_one_lib admit (dir,m) = (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) -type logical_path = Dir_path.t +type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) diff --git a/checker/checker.ml b/checker/checker.ml index 5cfd71fbf..9834b1331 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -36,7 +36,7 @@ let parse_dir s = let dirpath_of_string s = match parse_dir s with [] -> Check.default_root_prefix - | dir -> Dir_path.make (List.map Id.of_string dir) + | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = match parse_dir s with [] -> invalid_arg "path_of_string" @@ -77,11 +77,11 @@ let convert_string d = let add_rec_path ~unix_path ~coq_root = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in - let prefix = Dir_path.repr coq_root in + let prefix = DirPath.repr coq_root in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.Dir_path.make path) + Some (lp, Names.DirPath.make path) with Exit -> None in let dirs = List.map_filter convert_dirs dirs in @@ -113,9 +113,9 @@ let init_load_path () = let plugins = coqlib/"plugins" in (* NOTE: These directories are searched from last to first *) (* first standard library *) - add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.Dir_path.make[coq_root]); + add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); (* then plugins *) - add_rec_path ~unix_path:plugins ~coq_root:(Names.Dir_path.make [coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]); (* then user-contrib *) if Sys.file_exists user_contrib then add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; diff --git a/checker/environ.mli b/checker/environ.mli index 0ec14cc92..095d93ae5 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -27,8 +27,8 @@ val engagement : env -> Declarations.engagement option val set_engagement : Declarations.engagement -> env -> env (* Digests *) -val add_digest : env -> Dir_path.t -> Digest.t -> env -val lookup_digest : env -> Dir_path.t -> Digest.t +val add_digest : env -> DirPath.t -> Digest.t -> env +val lookup_digest : env -> DirPath.t -> Digest.t (* de Bruijn variables *) val rel_context : env -> rel_context diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8b56b5365..9a669e403 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -19,12 +19,12 @@ open Declarations open Environ let rec debug_string_of_mp = function - | MPfile sl -> Dir_path.to_string sl + | MPfile sl -> DirPath.to_string sl | MPbound uid -> "bound("^MBId.to_string uid^")" | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l let rec string_of_mp = function - | MPfile sl -> Dir_path.to_string sl + | MPfile sl -> DirPath.to_string sl | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index abc2da8b6..169fa5ca8 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -258,10 +258,10 @@ and check_module env mp mb = and check_structure_field env mp lab res = function | SFBconst cb -> - let c = make_con mp Dir_path.empty lab in + let c = make_con mp DirPath.empty lab in check_constant_declaration env c cb | SFBmind mib -> - let kn = make_mind mp Dir_path.empty lab in + let kn = make_mind mp DirPath.empty lab in let kn = mind_of_delta res kn in Indtypes.check_inductive env kn mib | SFBmodule msb -> diff --git a/checker/modops.ml b/checker/modops.ml index 6b7a9c7a1..38cd09956 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -67,7 +67,7 @@ let module_body_of_type mp mtb = let rec add_signature mp sign resolver env = let add_one env (l,elem) = - let kn = make_kn mp Dir_path.empty l in + let kn = make_kn mp DirPath.empty l in let con = constant_of_kn kn in let mind = mind_of_delta resolver (mind_of_kn kn) in match elem with @@ -97,7 +97,7 @@ let strengthen_const mp_from l cb resolver = match cb.const_body with | Def _ -> cb | _ -> - let con = make_con mp_from Dir_path.empty l in + let con = make_con mp_from DirPath.empty l in (* let con = constant_of_delta resolver con in*) { cb with const_body = Def (Declarations.from_val (Const con)) } diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index f0bcb3a12..5a190de7f 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -43,9 +43,9 @@ let check_engagement env c = let report_clash f caller dir = let msg = - str "compiled library " ++ str(Dir_path.to_string caller) ++ + str "compiled library " ++ str(DirPath.to_string caller) ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(Dir_path.to_string dir) ++ fnl() in + str(DirPath.to_string dir) ++ fnl() in f msg @@ -55,15 +55,15 @@ let check_imports f caller env needed = let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp with Not_found -> - error ("Reference to unknown module " ^ (Dir_path.to_string dp)) + error ("Reference to unknown module " ^ (DirPath.to_string dp)) in List.iter check needed type compiled_library = - Dir_path.t * + DirPath.t * module_body * - (Dir_path.t * Digest.t) list * + (DirPath.t * Digest.t) list * engagement option (* Store the body of modules' opaque constants inside a table. diff --git a/checker/subtyping.ml b/checker/subtyping.ml index b23043a37..02006a7ac 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -35,7 +35,7 @@ type namedmodule = constructors *) let add_mib_nameobjects mp l mib map = - let ind = make_mind mp Dir_path.empty l in + let ind = make_mind mp DirPath.empty l in let add_mip_nameobjects j oib map = let ip = (ind,j) in let map = @@ -83,7 +83,7 @@ let check_conv_error error f env a1 a2 = (* for now we do not allow reorderings *) let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= - let kn = make_mind mp1 Dir_path.empty l in + let kn = make_mind mp1 DirPath.empty l in let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let mib1 = diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 9386c82de..0dc09f9ba 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -322,7 +322,7 @@ let print_pure_constr csr = and sp_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev_map Id.to_string (Dir_path.repr dir) with + match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -331,7 +331,7 @@ let print_pure_constr csr = and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev_map Id.to_string (Dir_path.repr dir) with + match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -449,10 +449,10 @@ let encode_path loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (Dir_path.repr (dirpath_of_string (string_of_mp mp))@ - Dir_path.repr dir) in + (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + DirPath.repr dir) in Qualid (loc, make_qualid - (Dir_path.make (List.rev (Id.of_string prefix::dir@suffix))) id) + (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref loc = function | ConstRef cst -> diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 540e78b0b..6aefd3b72 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -33,8 +33,8 @@ let mlexpr_of_name = function <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >> let mlexpr_of_dirpath dir = - let l = Names.Dir_path.repr dir in - <:expr< Names.Dir_path.make $mlexpr_of_list mlexpr_of_ident l$ >> + let l = Names.DirPath.repr dir in + <:expr< Names.DirPath.make $mlexpr_of_list mlexpr_of_ident l$ >> let mlexpr_of_qualid qid = let (dir, id) = Libnames.repr_qualid qid in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 83cc1dcad..99c2a338e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -171,7 +171,7 @@ val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env - val is_global : Id.t -> bool val construct_reference : named_context -> Id.t -> constr val global_reference : Id.t -> constr -val global_reference_in_absolute_module : Dir_path.t -> Id.t -> constr +val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr (** Interprets a term as the left-hand side of a notation; the boolean list is a set and this set is [true] for a variable occurring in diff --git a/interp/coqlib.ml b/interp/coqlib.ml index b0a9831b7..0c9ac5830 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -21,7 +21,7 @@ open Smartlocate type message = string -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in @@ -64,10 +64,10 @@ let gen_constant_in_modules locstr dirs s = let check_required_library d = let d' = List.map Id.of_string d in - let dir = Dir_path.make (List.rev d') in + let dir = DirPath.make (List.rev d') in let mp = (fst(Lib.current_prefix())) in let current_dir = match mp with - | MPfile dp -> Dir_path.equal dir dp + | MPfile dp -> DirPath.equal dir dp | _ -> false in if not (Library.library_is_loaded dir) then @@ -75,10 +75,10 @@ let check_required_library d = (* Loading silently ... let m, prefix = List.sep_last d' in read_library - (Loc.ghost,make_qualid (Dir_path.make (List.rev prefix)) m) + (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(Dir_path.to_string dir)^" has to be required first.") + error ("Library "^(DirPath.to_string dir)^" has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 02174c876..37be549d6 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -54,8 +54,8 @@ val check_required_library : string list -> unit (** {6 Global references } *) (** Modules *) -val logic_module : Dir_path.t -val logic_type_module : Dir_path.t +val logic_module : DirPath.t +val logic_type_module : DirPath.t val datatypes_module_name : string list val logic_module_name : string list diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 23c1b2abc..c708d93da 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -133,8 +133,8 @@ let add_glob_gen loc sp lib_dp ty = let mod_dp,id = Libnames.repr_path sp in let mod_dp = remove_sections mod_dp in let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in - let filepath = Names.Dir_path.to_string lib_dp in - let modpath = Names.Dir_path.to_string mod_dp_trunc in + let filepath = Names.DirPath.to_string lib_dp in + let modpath = Names.DirPath.to_string mod_dp_trunc in let ident = Names.Id.to_string id in dump_ref loc filepath modpath ident ty @@ -160,12 +160,12 @@ let dump_binding loc id = () let dump_definition (loc, id) sec s = let bl,el = interval loc in dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el - (Names.Dir_path.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)) + (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)) let dump_reference loc modpath ident ty = let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" - bl el (Names.Dir_path.to_string (Lib.library_dp ())) modpath ident ty) + bl el (Names.DirPath.to_string (Lib.library_dp ())) modpath ident ty) let dump_constraint ((loc, n), _, _) sec ty = match n with @@ -176,8 +176,8 @@ let dump_modref loc mp ty = if dump () then let (dp, l) = Lib.split_modpath mp in let l = if List.is_empty l then l else List.drop_last l in - let fp = Names.Dir_path.to_string dp in - let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in + let fp = Names.DirPath.to_string dp in + let mp = Names.DirPath.to_string (Names.DirPath.make l) in let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el fp mp "<>" ty) @@ -186,13 +186,13 @@ let dump_moddef loc mp ty = if dump () then let bl,el = interval loc in let (dp, l) = Lib.split_modpath mp in - let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in + let mp = Names.DirPath.to_string (Names.DirPath.make l) in dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp) let dump_libref loc dp ty = let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n" - bl el (Names.Dir_path.to_string dp) ty) + bl el (Names.DirPath.to_string dp) ty) let cook_notation df sc = (* We encode notations so that they are space-free and still human-readable *) @@ -234,12 +234,12 @@ let cook_notation df sc = let dump_notation (loc,(df,_)) sc sec = (* We dump the location of the opening '"' *) dump_string (Printf.sprintf "not %d %s %s\n" (fst (Loc.unloc loc)) - (Names.Dir_path.to_string (Lib.current_dirpath sec)) (cook_notation df sc)) + (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc)) let dump_notation_location posl df (((path,secpath),_),sc) = if dump () then - let path = Names.Dir_path.to_string path in - let secpath = Names.Dir_path.to_string secpath in + let path = Names.DirPath.to_string path in + let secpath = Names.DirPath.to_string secpath in let df = cook_notation df sc in List.iter (fun (bl,el) -> dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df)) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 7674322c3..edea94f0c 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -29,7 +29,7 @@ val dump_definition : Loc.t * Names.Id.t -> bool -> string -> unit val dump_moddef : Loc.t -> Names.module_path -> string -> unit val dump_modref : Loc.t -> Names.module_path -> string -> unit val dump_reference : Loc.t -> string -> string -> string -> unit -val dump_libref : Loc.t -> Names.Dir_path.t -> string -> unit +val dump_libref : Loc.t -> Names.DirPath.t -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit val dump_binding : Loc.t -> Names.Id.Set.elt -> unit diff --git a/interp/notation.ml b/interp/notation.ml index c55b7b999..e72151777 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -44,14 +44,14 @@ open Ppextend type level = precedence * tolerability list type delimiters = string -type notation_location = (Dir_path.t * Dir_path.t) * string +type notation_location = (DirPath.t * DirPath.t) * string type scope = { notations: (string, interpretation * notation_location) Gmap.t; delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level * Dir_path.t *) +(* Uninterpreted notation map: notation -> level * DirPath.t *) let notation_level_map = ref Gmap.empty (* Scopes table: scope_name -> symbol_interpretation *) @@ -397,7 +397,7 @@ let find_prim_token g loc p sc = (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in check_required_module loc sc spdir; - g (interp ()), ((dirpath (fst spdir),Dir_path.empty),"") + g (interp ()), ((dirpath (fst spdir),DirPath.empty),"") let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in diff --git a/interp/notation.mli b/interp/notation.mli index 4a28ce255..e4a912494 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -65,7 +65,7 @@ val find_delimiters_scope : Loc.t -> delimiters -> scope_name negative numbers are not supported, the interpreter must fail with an appropriate error message *) -type notation_location = (Dir_path.t * Dir_path.t) * string +type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list type cases_pattern_status = bool (** true = use prim token in patterns *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index bb3eeb2e0..96ba0bcc5 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -42,7 +42,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in - Dir_path.is_empty dir && Id.equal id (basename sp) + DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 1d7e9374f..719cf0d33 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -167,7 +167,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of Loc.t * string * - (Id.t * 'lev generic_argument) list * (Dir_path.t * glob_tactic_expr) + (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr) (** Possible arguments of a tactic definition *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 528fd69f3..4655e3588 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -38,11 +38,11 @@ type printable = | PrintSectionContext of reference | PrintInspect of int | PrintGrammar of string - | PrintLoadPath of Dir_path.t option + | PrintLoadPath of DirPath.t option | PrintModules | PrintModule of reference | PrintModuleType of reference - | PrintNamespace of Dir_path.t + | PrintNamespace of DirPath.t | PrintMLLoadPath | PrintMLModules | PrintName of reference or_by_notation @@ -289,7 +289,7 @@ type vernac_expr = (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * string - | VernacAddLoadPath of rec_flag * string * Dir_path.t option + | VernacAddLoadPath of rec_flag * string * DirPath.t option | VernacRemoveLoadPath of string | VernacAddMLPath of rec_flag * string | VernacDeclareMLModule of locality_flag * string list diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4fde7474b..fb3303687 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -25,9 +25,9 @@ open Environ type work_list = Id.t array Cmap.t * Id.t array Mindmap.t -let pop_dirpath p = match Dir_path.repr p with +let pop_dirpath p = match DirPath.repr p with | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath") - | _::l -> Dir_path.make l + | _::l -> DirPath.make l let pop_mind kn = let (mp,dir,l) = Names.repr_mind kn in diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 357a48080..d80c69bee 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -373,7 +373,7 @@ if Int.equal nmr 0 then 0 else in find 0 (n-1) (lpar,List.rev hyps) let lambda_implicit_lift n a = - let level = UniverseLevel.make (Dir_path.make [Id.of_string "implicit"]) 0 in + let level = UniverseLevel.make (DirPath.make [Id.of_string "implicit"]) 0 in let implicit_sort = mkType (Universe.make level) in let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in iterate lambda_implicit n (lift n a) diff --git a/kernel/modops.ml b/kernel/modops.ml index e247a5712..48ce47bd4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -259,7 +259,7 @@ let add_retroknowledge mp = let rec add_signature mp sign resolver env = let add_one env (l,elem) = - let kn = make_kn mp Dir_path.empty l in + let kn = make_kn mp DirPath.empty l in match elem with | SFBconst cb -> Environ.add_constant (constant_of_delta_kn resolver kn) cb env @@ -284,7 +284,7 @@ let strengthen_const mp_from l cb resolver = match cb.const_body with | Def _ -> cb | _ -> - let kn = make_kn mp_from Dir_path.empty l in + let kn = make_kn mp_from DirPath.empty l in let con = constant_of_delta_kn resolver kn in { cb with const_body = Def (Declarations.from_val (mkConst con)); @@ -429,8 +429,8 @@ and strengthen_and_subst_struct (* If we are performing an inclusion we need to add the fact that the constant mp_to.l is \Delta-equivalent to resolver(mp_from.l) *) - let kn_from = make_kn mp_from Dir_path.empty l in - let kn_to = make_kn mp_to Dir_path.empty l in + let kn_from = make_kn mp_from DirPath.empty l in + let kn_to = make_kn mp_to DirPath.empty l in let old_name = kn_of_delta resolver kn_from in (add_kn_delta_resolver kn_to old_name resolve_out), item'::rest' @@ -446,8 +446,8 @@ and strengthen_and_subst_struct strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in if incl then - let kn_from = make_kn mp_from Dir_path.empty l in - let kn_to = make_kn mp_to Dir_path.empty l in + let kn_from = make_kn mp_from DirPath.empty l in + let kn_to = make_kn mp_to DirPath.empty l in let old_name = kn_of_delta resolver kn_from in (add_kn_delta_resolver kn_to old_name resolve_out), item'::rest' diff --git a/kernel/names.ml b/kernel/names.ml index e207c998e..f74240a23 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -126,7 +126,7 @@ module ModIdmap = Id.Map let default_module_name = "If you see this, it's a bug" -module Dir_path = +module DirPath = struct type t = module_ident list @@ -181,7 +181,7 @@ end module MBId = struct - type t = int * Id.t * Dir_path.t + type t = int * Id.t * DirPath.t let gen = let seed = ref 0 in fun () -> @@ -194,7 +194,7 @@ struct let repr mbid = mbid let to_string (i, s, p) = - Dir_path.to_string p ^ "." ^ s + DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">" @@ -209,7 +209,7 @@ struct let ans = Id.compare idl idr in if not (Int.equal ans 0) then ans else - Dir_path.compare dpl dpr + DirPath.compare dpl dpr let equal x y = Int.equal (compare x y) 0 @@ -219,7 +219,7 @@ struct struct type _t = t type t = _t - type u = (Id.t -> Id.t) * (Dir_path.t -> Dir_path.t) + type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.t) let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir) let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || @@ -229,7 +229,7 @@ struct module HashMBId = Hashcons.Make(Self_Hashcons) - let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, Dir_path.hcons) + let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, DirPath.hcons) end @@ -248,7 +248,7 @@ end module ModPath = struct type t = - | MPfile of Dir_path.t + | MPfile of DirPath.t | MPbound of MBId.t | MPdot of t * Label.t @@ -260,7 +260,7 @@ module ModPath = struct | _ -> false let rec to_string = function - | MPfile sl -> Dir_path.to_string sl + | MPfile sl -> DirPath.to_string sl | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l @@ -268,7 +268,7 @@ module ModPath = struct let rec compare mp1 mp2 = if mp1 == mp2 then 0 else match mp1, mp2 with - | MPfile p1, MPfile p2 -> Dir_path.compare p1 p2 + | MPfile p1, MPfile p2 -> DirPath.compare p1 p2 | MPbound id1, MPbound id2 -> MBId.compare id1 id2 | MPdot (mp1, l1), MPdot (mp2, l2) -> let c = String.compare l1 l2 in @@ -281,11 +281,11 @@ module ModPath = struct let equal mp1 mp2 = Int.equal (compare mp1 mp2) 0 - let initial = MPfile Dir_path.initial + let initial = MPfile DirPath.initial module Self_Hashcons = struct type t = module_path - type u = (Dir_path.t -> Dir_path.t) * (MBId.t -> MBId.t) * + type u = (DirPath.t -> DirPath.t) * (MBId.t -> MBId.t) * (string -> string) let rec hashcons (hdir,huniqid,hstr as hfuns) = function | MPfile dir -> MPfile (hdir dir) @@ -305,7 +305,7 @@ module ModPath = struct let hcons = Hashcons.simple_hcons HashMP.generate - (Dir_path.hcons,MBId.hcons,String.hcons) + (DirPath.hcons,MBId.hcons,String.hcons) end @@ -316,7 +316,7 @@ module MPmap = Map.Make(ModPath) module KerName = struct - type t = ModPath.t * Dir_path.t * Label.t + type t = ModPath.t * DirPath.t * Label.t type kernel_name = t @@ -328,8 +328,8 @@ module KerName = struct let to_string (mp,dir,l) = let dp = - if Dir_path.is_empty dir then "." - else "#" ^ Dir_path.to_string dir ^ "#" + if DirPath.is_empty dir then "." + else "#" ^ DirPath.to_string dir ^ "#" in ModPath.to_string mp ^ dp ^ Label.to_string l @@ -342,7 +342,7 @@ module KerName = struct let c = String.compare l1 l2 in if not (Int.equal c 0) then c else - let c = Dir_path.compare dir1 dir2 in + let c = DirPath.compare dir1 dir2 in if not (Int.equal c 0) then c else ModPath.compare mp1 mp2 @@ -350,7 +350,7 @@ module KerName = struct module Self_Hashcons = struct type t = kernel_name - type u = (ModPath.t -> ModPath.t) * (Dir_path.t -> Dir_path.t) + type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t) * (string -> string) let hashcons (hmod,hdir,hstr) (mp,dir,l) = (hmod mp,hdir dir,hstr l) @@ -363,7 +363,7 @@ module KerName = struct let hcons = Hashcons.simple_hcons HashKN.generate - (ModPath.hcons,Dir_path.hcons,String.hcons) + (ModPath.hcons,DirPath.hcons,String.hcons) end @@ -479,7 +479,7 @@ let debug_pr_con cst = str (debug_string_of_con cst) let con_with_label cst lbl = let (mp1,dp1,l1) = KerName.repr (user_con cst) and (mp2,dp2,l2) = KerName.repr (canonical_con cst) in - assert (String.equal l1 l2 && Dir_path.equal dp1 dp2); + assert (String.equal l1 l2 && DirPath.equal dp1 dp2); if String.equal lbl l1 then cst else make_con_equiv mp1 mp2 dp1 lbl @@ -669,17 +669,17 @@ module Idpred = Id.Pred let name_eq = Name.equal -(** Compatibility layer for [Dir_path] *) +(** Compatibility layer for [DirPath] *) -type dir_path = Dir_path.t -let dir_path_ord = Dir_path.compare -let dir_path_eq = Dir_path.equal -let make_dirpath = Dir_path.make -let repr_dirpath = Dir_path.repr -let empty_dirpath = Dir_path.empty -let is_empty_dirpath = Dir_path.is_empty -let string_of_dirpath = Dir_path.to_string -let initial_dir = Dir_path.initial +type dir_path = DirPath.t +let dir_path_ord = DirPath.compare +let dir_path_eq = DirPath.equal +let make_dirpath = DirPath.make +let repr_dirpath = DirPath.repr +let empty_dirpath = DirPath.empty +let is_empty_dirpath = DirPath.is_empty +let string_of_dirpath = DirPath.to_string +let initial_dir = DirPath.initial (** Compatibility layer for [MBId] *) @@ -705,7 +705,7 @@ let eq_label = Label.equal (** Compatibility layer for [ModPath] *) type module_path = ModPath.t = - | MPfile of Dir_path.t + | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t let check_bound_mp = ModPath.is_bound diff --git a/kernel/names.mli b/kernel/names.mli index 9a15a3a69..e194b3856 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -76,7 +76,7 @@ type module_ident = Id.t (** {6 Directory paths = section names paths } *) -module Dir_path : +module DirPath : sig type t (** Type of directory paths. Essentially a list of module identifiers. The @@ -155,11 +155,11 @@ sig val compare : t -> t -> int (** Comparison over unique bound names. *) - val make : Dir_path.t -> Id.t -> t + val make : DirPath.t -> Id.t -> t (** The first argument is a file name, to prevent conflict between different files. *) - val repr : t -> int * Id.t * Dir_path.t + val repr : t -> int * Id.t * DirPath.t (** Reverse of [make]. *) val to_id : t -> Id.t @@ -180,7 +180,7 @@ module ModIdmap : Map.S with type key = module_ident module ModPath : sig type t = - | MPfile of Dir_path.t + | MPfile of DirPath.t | MPbound of MBId.t | MPdot of t * Label.t @@ -206,8 +206,8 @@ sig type t (** Constructor and destructor *) - val make : ModPath.t -> Dir_path.t -> Label.t -> t - val repr : t -> ModPath.t * Dir_path.t * Label.t + val make : ModPath.t -> DirPath.t -> Label.t -> t + val repr : t -> ModPath.t * DirPath.t * Label.t (** Projections *) val modpath : t -> ModPath.t @@ -255,12 +255,12 @@ module Constrmap_env : Map.S with type key = constructor val constant_of_kn : KerName.t -> constant val constant_of_kn_equiv : KerName.t -> KerName.t -> constant -val make_con : ModPath.t -> Dir_path.t -> Label.t -> constant -val make_con_equiv : ModPath.t -> ModPath.t -> Dir_path.t +val make_con : ModPath.t -> DirPath.t -> Label.t -> constant +val make_con_equiv : ModPath.t -> ModPath.t -> DirPath.t -> Label.t -> constant val user_con : constant -> KerName.t val canonical_con : constant -> KerName.t -val repr_con : constant -> ModPath.t * Dir_path.t * Label.t +val repr_con : constant -> ModPath.t * DirPath.t * Label.t val eq_constant : constant -> constant -> bool val con_ord : constant -> constant -> int val con_user_ord : constant -> constant -> int @@ -277,12 +277,12 @@ val debug_string_of_con : constant -> string val mind_of_kn : KerName.t -> mutual_inductive val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive -val make_mind : ModPath.t -> Dir_path.t -> Label.t -> mutual_inductive -val make_mind_equiv : ModPath.t -> ModPath.t -> Dir_path.t +val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive +val make_mind_equiv : ModPath.t -> ModPath.t -> DirPath.t -> Label.t -> mutual_inductive val user_mind : mutual_inductive -> KerName.t val canonical_mind : mutual_inductive -> KerName.t -val repr_mind : mutual_inductive -> ModPath.t * Dir_path.t * Label.t +val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t val eq_mind : mutual_inductive -> mutual_inductive -> bool val mind_ord : mutual_inductive -> mutual_inductive -> int val mind_user_ord : mutual_inductive -> mutual_inductive -> int @@ -393,32 +393,32 @@ end (** {5 Directory paths} *) -type dir_path = Dir_path.t -(** @deprecated Alias for [Dir_path.t]. *) +type dir_path = DirPath.t +(** @deprecated Alias for [DirPath.t]. *) val dir_path_ord : dir_path -> dir_path -> int -(** @deprecated Same as [Dir_path.compare]. *) +(** @deprecated Same as [DirPath.compare]. *) val dir_path_eq : dir_path -> dir_path -> bool -(** @deprecated Same as [Dir_path.equal]. *) +(** @deprecated Same as [DirPath.equal]. *) val make_dirpath : module_ident list -> dir_path -(** @deprecated Same as [Dir_path.make]. *) +(** @deprecated Same as [DirPath.make]. *) val repr_dirpath : dir_path -> module_ident list -(** @deprecated Same as [Dir_path.repr]. *) +(** @deprecated Same as [DirPath.repr]. *) val empty_dirpath : dir_path -(** @deprecated Same as [Dir_path.empty]. *) +(** @deprecated Same as [DirPath.empty]. *) val is_empty_dirpath : dir_path -> bool -(** @deprecated Same as [Dir_path.is_empty]. *) +(** @deprecated Same as [DirPath.is_empty]. *) val string_of_dirpath : dir_path -> string -(** @deprecated Same as [Dir_path.to_string]. *) +(** @deprecated Same as [DirPath.to_string]. *) -val initial_dir : Dir_path.t -(** @deprecated Same as [Dir_path.initial]. *) +val initial_dir : DirPath.t +(** @deprecated Same as [DirPath.initial]. *) (** {5 Labels} *) @@ -454,10 +454,10 @@ val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool (** @deprecated Same as [MBId.equal]. *) -val make_mbid : Dir_path.t -> Id.t -> mod_bound_id +val make_mbid : DirPath.t -> Id.t -> mod_bound_id (** @deprecated Same as [MBId.make]. *) -val repr_mbid : mod_bound_id -> int * Id.t * Dir_path.t +val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t (** @deprecated Same as [MBId.repr]. *) val id_of_mbid : mod_bound_id -> Id.t @@ -477,7 +477,7 @@ val name_eq : name -> name -> bool (** {5 Module paths} *) type module_path = ModPath.t = - | MPfile of Dir_path.t + | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t (** @deprecated Alias type *) @@ -502,10 +502,10 @@ val initial_path : module_path type kernel_name = KerName.t (** @deprecated Alias type *) -val make_kn : ModPath.t -> Dir_path.t -> Label.t -> kernel_name +val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name (** @deprecated Same as [KerName.make]. *) -val repr_kn : kernel_name -> module_path * Dir_path.t * Label.t +val repr_kn : kernel_name -> module_path * DirPath.t * Label.t (** @deprecated Same as [KerName.repr]. *) val modpath : kernel_name -> module_path diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 2e21a86ff..a591fb433 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -76,7 +76,7 @@ type modvariant = | NONE | SIG of (* funsig params *) (MBId.t * module_type_body) list | STRUCT of (* functor params *) (MBId.t * module_type_body) list - | LIBRARY of Dir_path.t + | LIBRARY of DirPath.t type module_info = {modpath : module_path; @@ -90,7 +90,7 @@ let set_engagement_opt oeng env = Some eng -> set_engagement eng env | _ -> env -type library_info = Dir_path.t * Digest.t +type library_info = DirPath.t * Digest.t type safe_environment = { old : safe_environment; @@ -271,7 +271,7 @@ let add_constant dir l decl senv = | ConstantEntry ce -> translate_constant senv.env kn ce | GlobalRecipe r -> let cb = translate_recipe senv.env kn r in - if Dir_path.is_empty dir then hcons_const_body cb else cb + if DirPath.is_empty dir then hcons_const_body cb else cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with @@ -482,10 +482,10 @@ let end_module l restype senv = let add senv ((l,elem) as field) = let new_name = match elem with | SFBconst _ -> - let kn = make_kn mp_sup Dir_path.empty l in + let kn = make_kn mp_sup DirPath.empty l in C (constant_of_delta_kn resolver kn) | SFBmind _ -> - let kn = make_kn mp_sup Dir_path.empty l in + let kn = make_kn mp_sup DirPath.empty l in I (mind_of_delta_kn resolver kn) | SFBmodule _ -> M | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l)) @@ -630,7 +630,7 @@ let set_engagement c senv = (* Libraries = Compiled modules *) type compiled_library = - Dir_path.t * module_body * library_info list * engagement option + DirPath.t * module_body * library_info list * engagement option * Nativecode.symbol array type native_library = Nativecode.global list @@ -646,10 +646,10 @@ let start_library dir senv = if not (is_empty senv) then anomaly ~label:"Safe_typing.start_library" (Pp.str "environment should be empty"); let dir_path,l = - match (Dir_path.repr dir) with + match (DirPath.repr dir) with [] -> anomaly (Pp.str "Empty dirpath in Safe_typing.start_library") | hd::tl -> - Dir_path.make tl, Label.of_id hd + DirPath.make tl, Label.of_id hd in let mp = MPfile dir in let modinfo = {modpath = mp; @@ -685,7 +685,7 @@ let export senv dir = begin match modinfo.variant with | LIBRARY dp -> - if not (Dir_path.equal dir dp) then + if not (DirPath.equal dir dp) then anomaly (Pp.str "We are not exporting the right library!") | _ -> anomaly (Pp.str "We are not exporting the library") @@ -720,9 +720,9 @@ let check_imports senv needed = let actual_stamp = List.assoc id imports in if not (String.equal stamp actual_stamp) then error - ("Inconsistent assumptions over module "^(Dir_path.to_string id)^".") + ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") with Not_found -> - error ("Reference to unknown module "^(Dir_path.to_string id)^".") + error ("Reference to unknown module "^(DirPath.to_string id)^".") in List.iter check needed diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 7cddde954..1bb43a53e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,12 +43,12 @@ type global_declaration = | GlobalRecipe of Cooking.recipe val add_constant : - Dir_path.t -> Label.t -> global_declaration -> safe_environment -> + DirPath.t -> Label.t -> global_declaration -> safe_environment -> constant * safe_environment (** Adding an inductive type *) val add_mind : - Dir_path.t -> Label.t -> mutual_inductive_entry -> safe_environment -> + DirPath.t -> Label.t -> mutual_inductive_entry -> safe_environment -> mutual_inductive * safe_environment (** Adding a module *) @@ -103,10 +103,10 @@ type compiled_library type native_library = Nativecode.global list -val start_library : Dir_path.t -> safe_environment +val start_library : DirPath.t -> safe_environment -> module_path * safe_environment -val export : safe_environment -> Dir_path.t +val export : safe_environment -> DirPath.t -> module_path * compiled_library * native_library val import : compiled_library -> Digest.t -> safe_environment diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 11ae7c863..9e9d5b580 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -39,7 +39,7 @@ type namedmodule = constructors *) let add_mib_nameobjects mp l mib map = - let ind = make_mind mp Dir_path.empty l in + let ind = make_mind mp DirPath.empty l in let add_mip_nameobjects j oib map = let ip = (ind,j) in let map = @@ -88,8 +88,8 @@ let check_conv_error error why cst f env a1 a2 = (* for now we do not allow reorderings *) let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= - let kn1 = make_mind mp1 Dir_path.empty l in - let kn2 = make_mind mp2 Dir_path.empty l in + let kn1 = make_mind mp1 DirPath.empty l in + let kn2 = make_mind mp2 DirPath.empty l in let error why = error_signature_mismatch l spec2 why in let check_conv why cst f = check_conv_error error why cst f in let mib1 = diff --git a/kernel/univ.ml b/kernel/univ.ml index 9a27ff2a3..26254be23 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -33,10 +33,10 @@ module UniverseLevel = struct type t = | Set - | Level of int * Names.Dir_path.t + | Level of int * Names.DirPath.t (* A specialized comparison function: we compare the [int] part first. - This way, most of the time, the [Dir_path.t] part is not considered. + This way, most of the time, the [DirPath.t] part is not considered. Normally, placing the [int] first in the pair above in enough in Ocaml, but to be sure, we write below our own comparison function. @@ -53,19 +53,19 @@ module UniverseLevel = struct | Level (i1, dp1), Level (i2, dp2) -> if i1 < i2 then -1 else if i1 > i2 then 1 - else Names.Dir_path.compare dp1 dp2) + else Names.DirPath.compare dp1 dp2) let equal u v = match u,v with | Set, Set -> true | Level (i1, dp1), Level (i2, dp2) -> - Int.equal i1 i2 && Int.equal (Names.Dir_path.compare dp1 dp2) 0 + Int.equal i1 i2 && Int.equal (Names.DirPath.compare dp1 dp2) 0 | _ -> false let make m n = Level (n, m) let to_string = function | Set -> "Set" - | Level (n,d) -> Names.Dir_path.to_string d^"."^string_of_int n + | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n end module UniverseLMap = Map.Make (UniverseLevel) @@ -776,7 +776,7 @@ let bellman_ford bottom g = graph already contains [Type.n] nodes (calling a module Type is probably a bad idea anyway). *) let sort_universes orig = - let mp = Names.Dir_path.make [Names.Id.of_string "Type"] in + let mp = Names.DirPath.make [Names.Id.of_string "Type"] in let rec make_level accu g i = let type0 = UniverseLevel.Level (i, mp) in let distances = bellman_ford type0 g in @@ -838,7 +838,7 @@ let sort_universes orig = let fresh_level = let n = ref 0 in - fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.empty) + fun () -> incr n; UniverseLevel.Level (!n, Names.DirPath.empty) let fresh_local_univ () = Atom (fresh_level ()) @@ -972,7 +972,7 @@ module Hunivlevel = Hashcons.Make( struct type t = universe_level - type u = Names.Dir_path.t -> Names.Dir_path.t + type u = Names.DirPath.t -> Names.DirPath.t let hashcons hdir = function | UniverseLevel.Set -> UniverseLevel.Set | UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d) @@ -1005,7 +1005,7 @@ module Huniv = let hash = Hashtbl.hash end) -let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.Dir_path.hcons +let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel module Hconstraint = diff --git a/kernel/univ.mli b/kernel/univ.mli index b466057a2..c74797c8b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -20,7 +20,7 @@ sig val equal : t -> t -> bool (** Equality function *) - val make : Names.Dir_path.t -> int -> t + val make : Names.DirPath.t -> int -> t (** Create a new universe level from a unique identifier and an associated module path. *) diff --git a/library/declare.ml b/library/declare.ml index 3627df7fe..ee4656f75 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -53,7 +53,7 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types * bool (* Implicit status *) -type variable_declaration = Dir_path.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with diff --git a/library/declare.mli b/library/declare.mli index 54a0160bf..bcb72be58 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -32,7 +32,7 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (** opacity *) | SectionLocalAssum of types * bool (** Implicit status *) -type variable_declaration = Dir_path.t * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name diff --git a/library/declaremods.ml b/library/declaremods.ml index c96a9fbc0..591567fea 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -123,7 +123,7 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = - ref ((MPfile(Dir_path.initial),[],None,[]) + ref ((MPfile(DirPath.initial),[],None,[]) : module_path * MBId.t list * (module_struct_entry * int option) option * module_type_body list) @@ -146,16 +146,16 @@ let _ = Summary.declare_summary "MODULE-INFO" Summary.init_function = (fun () -> modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; - openmod_info := ((MPfile(Dir_path.initial), + openmod_info := ((MPfile(DirPath.initial), [],None,[])); library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given - by Lib into module_path and Dir_path.t needed for modules *) + by Lib into module_path and DirPath.t needed for modules *) let mp_of_kn kn = let mp,sec,l = repr_kn kn in - if Dir_path.is_empty sec then + if DirPath.is_empty sec then MPdot (mp,l) else anomaly (str "Non-empty section in module name!" ++ spc () ++ pr_kn kn) @@ -246,8 +246,8 @@ let compute_visibility exists what i dir dirinfo = Nametab.Until i (* let do_load_and_subst_module i dir mp substobjs keep = - let prefix = (dir,(mp,Dir_path.empty)) in - let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in + let prefix = (dir,(mp,DirPath.empty)) in + let dirinfo = DirModule (dir,(mp,DirPath.empty)) in let vis = compute_visibility false "load_and_subst" i dir dirinfo in let objects = compute_subst_objects mp substobjs resolver in Nametab.push_dir vis dir dirinfo; @@ -263,8 +263,8 @@ let do_load_and_subst_module i dir mp substobjs keep = *) let do_module exists what iter_objects i dir mp substobjs keep= - let prefix = (dir,(mp,Dir_path.empty)) in - let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in + let prefix = (dir,(mp,DirPath.empty)) in + let dirinfo = DirModule (dir,(mp,DirPath.empty)) in let vis = compute_visibility exists what i dir dirinfo in Nametab.push_dir vis dir dirinfo; modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; @@ -314,7 +314,7 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!") let load_keep i ((sp,kn),seg) = let mp = mp_of_kn kn in - let prefix = dir_of_sp sp, (mp,Dir_path.empty) in + let prefix = dir_of_sp sp, (mp,DirPath.empty) in begin try let prefix',objects = MPmap.find mp !modtab_objects in @@ -328,7 +328,7 @@ let load_keep i ((sp,kn),seg) = let open_keep i ((sp,kn),seg) = let dirpath,mp = dir_of_sp sp, mp_of_kn kn in - open_objects i (dirpath,(mp,Dir_path.empty)) seg + open_objects i (dirpath,(mp,DirPath.empty)) seg let in_modkeep : lib_objects -> obj = declare_object {(default_object "MODULE KEEP OBJECTS") with @@ -506,7 +506,7 @@ let rec get_modtype_substobjs env mp_from inline = function (* add objects associated to them *) let process_module_bindings argids args = let process_arg id (mbid,(mty,ann)) = - let dir = Dir_path.make [id] in + let dir = DirPath.make [id] in let mp = MPbound mbid in let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in @@ -539,7 +539,7 @@ let intern_args interp_modtype (idl,(arg,ann)) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> MBId.make lib_dir id) idl in let mty = interp_modtype (Global.env()) arg in - let dirs = List.map (fun (_,id) -> Dir_path.make [id]) idl in + let dirs = List.map (fun (_,id) -> DirPath.make [id]) idl in let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env()) (MPbound (List.hd mbids)) inl mty in List.map2 @@ -643,7 +643,7 @@ let module_objects mp = (************************************************************************) (* libraries *) -type library_name = Dir_path.t +type library_name = DirPath.t (* The first two will form substitutive_objects, the last one is keep *) type library_objects = @@ -890,18 +890,18 @@ let lift_oname (sp,kn) = let cache_include (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,Dir_path.empty)) in + let prefix = (dir,(mp1,DirPath.empty)) in load_objects 1 prefix objs; open_objects 1 prefix objs let load_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,Dir_path.empty)) in + let prefix = (dir,(mp1,DirPath.empty)) in load_objects i prefix objs let open_include i (oname,(me,(mbis,mp1,objs))) = let dir,mp1 = lift_oname oname in - let prefix = (dir,(mp1,Dir_path.empty)) in + let prefix = (dir,(mp1,DirPath.empty)) in open_objects i prefix objs let subst_include (subst,(me,substobj)) = diff --git a/library/declaremods.mli b/library/declaremods.mli index f3c06b158..06446e2eb 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -104,7 +104,7 @@ val module_objects : module_path -> library_segment (** {6 Libraries i.e. modules on disk } *) -type library_name = Dir_path.t +type library_name = DirPath.t type library_objects diff --git a/library/decls.ml b/library/decls.ml index 35b75dab1..0ceea8b43 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -18,7 +18,7 @@ open Libnames (** Datas associated to section variables and local definitions *) type variable_data = - Dir_path.t * bool (* opacity *) * Univ.constraints * logical_kind + DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind let vartab = ref (Id.Map.empty : variable_data Id.Map.t) @@ -65,7 +65,7 @@ let initialize_named_context_for_proof () = let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> - try if Dir_path.equal dir (variable_path id) then id::sec_ids else sec_ids + try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) ~init:[] diff --git a/library/decls.mli b/library/decls.mli index 2e080c7ba..87d963cd4 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -18,10 +18,10 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - Dir_path.t * bool (** opacity *) * Univ.constraints * logical_kind + DirPath.t * bool (** opacity *) * Univ.constraints * logical_kind val add_variable_data : variable -> variable_data -> unit -val variable_path : variable -> Dir_path.t +val variable_path : variable -> DirPath.t val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool @@ -40,4 +40,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val (** Miscellaneous functions *) -val last_section_hyps : Dir_path.t -> Id.t list +val last_section_hyps : DirPath.t -> Id.t list diff --git a/library/global.mli b/library/global.mli index 141cfe50b..f8edf3165 100644 --- a/library/global.mli +++ b/library/global.mli @@ -43,9 +43,9 @@ val push_named_def : (Id.t * constr * types option) -> Univ.constraints functions verify that given names match those generated by kernel *) val add_constant : - Dir_path.t -> Id.t -> global_declaration -> constant + DirPath.t -> Id.t -> global_declaration -> constant val add_mind : - Dir_path.t -> Id.t -> mutual_inductive_entry -> mutual_inductive + DirPath.t -> Id.t -> mutual_inductive_entry -> mutual_inductive val add_module : Id.t -> module_entry -> inline -> module_path * delta_resolver @@ -59,7 +59,7 @@ val add_constraints : constraints -> unit val set_engagement : engagement -> unit (** {6 Interactive modules and module types } - Both [start_*] functions take the [Dir_path.t] argument to create a + Both [start_*] functions take the [DirPath.t] argument to create a [mod_self_id]. This should be the name of the compilation unit. *) (** [start_*] functions return the [module_path] valid for components @@ -90,8 +90,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive val exists_objlabel : Label.t -> bool (** Compiled modules *) -val start_library : Dir_path.t -> module_path -val export : Dir_path.t -> module_path * compiled_library * native_library +val start_library : DirPath.t -> module_path +val export : DirPath.t -> module_path * compiled_library * native_library val import : compiled_library -> Digest.t -> module_path * Nativecode.symbol array diff --git a/library/globnames.ml b/library/globnames.ml index 02570d339..50c91cc05 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -138,26 +138,26 @@ let constr_of_global_or_constr = function (** {6 Temporary function to brutally form kernel names from section paths } *) -let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id) +let encode_mind dir id = make_mind (MPfile dir) DirPath.empty (Label.of_id id) -let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id) +let encode_con dir id = make_con (MPfile dir) DirPath.empty (Label.of_id id) let check_empty_section dp = - if not (Dir_path.is_empty dp) then + if not (DirPath.is_empty dp) then anomaly (Pp.str "Section part should be empty!") let decode_mind kn = let rec dir_of_mp = function - | MPfile dir -> Dir_path.repr dir + | MPfile dir -> DirPath.repr dir | MPbound mbid -> let _,_,dp = MBId.repr mbid in let id = MBId.to_id mbid in - id::(Dir_path.repr dp) + id::(DirPath.repr dp) | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp) in let mp,sec_dir,l = repr_mind kn in check_empty_section sec_dir; - (Dir_path.make (dir_of_mp mp)),Label.to_id l + (DirPath.make (dir_of_mp mp)),Label.to_id l let decode_con kn = let mp,sec_dir,l = repr_con kn in diff --git a/library/globnames.mli b/library/globnames.mli index 1e53186f4..74da2cca8 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -83,10 +83,10 @@ val constr_of_global_or_constr : global_reference_or_constr -> constr (** {6 Temporary function to brutally form kernel names from section paths } *) -val encode_mind : Dir_path.t -> Id.t -> mutual_inductive -val decode_mind : mutual_inductive -> Dir_path.t * Id.t -val encode_con : Dir_path.t -> Id.t -> constant -val decode_con : constant -> Dir_path.t * Id.t +val encode_mind : DirPath.t -> Id.t -> mutual_inductive +val decode_mind : mutual_inductive -> DirPath.t * Id.t +val encode_con : DirPath.t -> Id.t -> constant +val decode_con : constant -> DirPath.t * Id.t (** {6 Popping one level of section in global names } *) diff --git a/library/lib.ml b/library/lib.ml index 6b3110c20..baed92bd5 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -92,7 +92,7 @@ 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.initial_path,Names.Dir_path.empty) +let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty) let lib_stk = ref ([] : library_segment) @@ -106,10 +106,10 @@ let library_dp () = let path_prefix = ref initial_prefix let sections_depth () = - List.length (Names.Dir_path.repr (snd (snd !path_prefix))) + List.length (Names.DirPath.repr (snd (snd !path_prefix))) let sections_are_opened () = - match Names.Dir_path.repr (snd (snd !path_prefix)) with + match Names.DirPath.repr (snd (snd !path_prefix)) with [] -> false | _ -> true @@ -127,10 +127,10 @@ let make_path id = Libnames.make_path (cwd ()) id let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id let path_of_include () = - let dir = Names.Dir_path.repr (cwd ()) in + let dir = Names.DirPath.repr (cwd ()) in let new_dir = List.tl dir in let id = List.hd dir in - Libnames.make_path (Names.Dir_path.make new_dir) id + Libnames.make_path (Names.DirPath.make new_dir) id let current_prefix () = snd !path_prefix @@ -275,7 +275,7 @@ let current_mod_id () = let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in - let prefix = dir,(mp,Names.Dir_path.empty) in + let prefix = dir,(mp,Names.DirPath.empty) in let sp = make_path id in let oname = sp, make_kn id in let exists = @@ -328,9 +328,9 @@ let contents_after = function let start_compilation s mp = if !comp_name != None then error "compilation unit is already started"; - if not (Names.Dir_path.equal (snd (snd (!path_prefix))) Names.Dir_path.empty) then + if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then error "some sections are already opened"; - let prefix = s, (mp, Names.Dir_path.empty) in + let prefix = s, (mp, Names.DirPath.empty) in let _ = add_anonymous_entry (CompilingLibrary prefix) in comp_name := Some s; path_prefix := prefix @@ -356,7 +356,7 @@ let end_compilation dir = match !comp_name with | None -> anomaly (Pp.str "There should be a module name...") | Some m -> - if not (Names.Dir_path.equal m dir) then anomaly + 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); in @@ -621,7 +621,7 @@ let label_before_name (loc,id) = (* State and initialization. *) -type frozen = Names.Dir_path.t option * library_segment +type frozen = Names.DirPath.t option * library_segment let freeze () = (!comp_name, !lib_stk) @@ -654,11 +654,11 @@ let rec dp_of_mp modp = let rec split_mp mp = match mp with - | Names.MPfile dp -> dp, Names.Dir_path.empty + | Names.MPfile dp -> dp, Names.DirPath.empty | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in - mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.Dir_path.make [id] + mprec, Names.DirPath.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.DirPath.repr dprec)) + | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in library_dp(), Names.DirPath.make [id] let split_modpath mp = let rec aux = function @@ -695,13 +695,13 @@ let remove_section_part ref = let con_defined_in_sec kn = let _,dir,_ = Names.repr_con kn in - not (Names.Dir_path.is_empty dir) && - Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ())) + not (Names.DirPath.is_empty dir) && + Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ())) let defined_in_sec kn = let _,dir,_ = Names.repr_mind kn in - not (Names.Dir_path.is_empty dir) && - Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ())) + not (Names.DirPath.is_empty dir) && + Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ())) let discharge_global = function | ConstRef kn when con_defined_in_sec kn -> diff --git a/library/lib.mli b/library/lib.mli index 13a79caf1..1ea76f1ad 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -72,15 +72,15 @@ val contents_after : Libnames.object_name option -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.Dir_path.t -val cwd_except_section : unit -> Names.Dir_path.t -val current_dirpath : bool -> Names.Dir_path.t (* false = except sections *) +val cwd : unit -> Names.DirPath.t +val cwd_except_section : unit -> Names.DirPath.t +val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path val path_of_include : unit -> Libnames.full_path (** Kernel-side names *) -val current_prefix : unit -> Names.module_path * Names.Dir_path.t +val current_prefix : unit -> Names.module_path * Names.DirPath.t val make_kn : Names.Id.t -> Names.kernel_name val make_con : Names.Id.t -> Names.constant @@ -124,19 +124,19 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.Dir_path.t -> Names.module_path -> unit -val end_compilation : Names.Dir_path.t -> Libnames.object_prefix * library_segment +val start_compilation : Names.DirPath.t -> Names.module_path -> unit +val end_compilation : Names.DirPath.t -> Libnames.object_prefix * library_segment -(** The function [library_dp] returns the [Dir_path.t] of the current +(** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.Dir_path.t +val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.module_path -> Names.Dir_path.t -val split_mp : Names.module_path -> Names.Dir_path.t * Names.Dir_path.t -val split_modpath : Names.module_path -> Names.Dir_path.t * Names.Id.t list -val library_part : Globnames.global_reference -> Names.Dir_path.t -val remove_section_part : Globnames.global_reference -> Names.Dir_path.t +val dp_of_mp : Names.module_path -> Names.DirPath.t +val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t +val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list +val library_part : Globnames.global_reference -> Names.DirPath.t +val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) diff --git a/library/libnames.ml b/library/libnames.ml index 9f129793e..43ece3417 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,38 +13,38 @@ open Names (**********************************************) -let pr_dirpath sl = (str (Dir_path.to_string sl)) +let pr_dirpath sl = (str (DirPath.to_string sl)) (*s Operations on dirpaths *) (* Pop the last n module idents *) let pop_dirpath_n n dir = - Dir_path.make (List.skipn n (Dir_path.repr dir)) + DirPath.make (List.skipn n (DirPath.repr dir)) -let pop_dirpath p = match Dir_path.repr p with +let pop_dirpath p = match DirPath.repr p with | [] -> anomaly (str "dirpath_prefix: empty dirpath") - | _::l -> Dir_path.make l + | _::l -> DirPath.make l let is_dirpath_prefix_of d1 d2 = - List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) + List.prefix_of (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) let chop_dirpath n d = - let d1,d2 = List.chop n (List.rev (Dir_path.repr d)) in - Dir_path.make (List.rev d1), Dir_path.make (List.rev d2) + let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in + DirPath.make (List.rev d1), DirPath.make (List.rev d2) let drop_dirpath_prefix d1 d2 = - let d = Util.List.drop_prefix (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) in - Dir_path.make (List.rev d) + let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in + DirPath.make (List.rev d) -let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1) +let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1) (* To know how qualified a name should be to be understood in the current env*) -let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id]) +let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id]) let split_dirpath d = - let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l) + let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l) -let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p) +let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) (* parsing *) let parse_dir s = @@ -68,22 +68,22 @@ let dirpath_of_string s = | "" -> [] | _ -> parse_dir s in - Dir_path.make path + DirPath.make path -let string_of_dirpath = Names.Dir_path.to_string +let string_of_dirpath = Names.DirPath.to_string -module Dirset = Set.Make(struct type t = Dir_path.t let compare = Dir_path.compare end) -module Dirmap = Map.Make(struct type t = Dir_path.t let compare = Dir_path.compare end) +module Dirset = Set.Make(struct type t = DirPath.t let compare = DirPath.compare end) +module Dirmap = Map.Make(struct type t = DirPath.t let compare = DirPath.compare end) (*s Section paths are absolute names *) type full_path = { - dirpath : Dir_path.t ; + dirpath : DirPath.t ; basename : Id.t } let eq_full_path p1 p2 = Id.equal p1.basename p2.basename && - Dir_path.equal p1.dirpath p2.dirpath + DirPath.equal p1.dirpath p2.dirpath let make_path pa id = { dirpath = pa; basename = id } @@ -92,9 +92,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id) (* parsing and printing of section paths *) let string_of_path sp = let (sl,id) = repr_path sp in - match Dir_path.repr sl with + match DirPath.repr sl with | [] -> Id.to_string id - | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id) + | _ -> (DirPath.to_string sl) ^ "." ^ (Id.to_string id) let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 @@ -124,8 +124,8 @@ 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 (Dir_path.repr dir) in - make_path (Dir_path.make dir') s + let dir' = List.firstn n (DirPath.repr dir) in + make_path (DirPath.make dir') s (*s qualified names *) type qualid = full_path @@ -141,30 +141,30 @@ let pr_qualid = pr_path let qualid_of_string = path_of_string let qualid_of_path sp = sp -let qualid_of_ident id = make_qualid Dir_path.empty id +let qualid_of_ident id = make_qualid DirPath.empty id let qualid_of_dirpath dir = let (l,a) = split_dirpath dir in make_qualid l a type object_name = full_path * kernel_name -type object_prefix = Dir_path.t * (module_path * Dir_path.t) +type object_prefix = DirPath.t * (module_path * DirPath.t) let make_oname (dirpath,(mp,dir)) id = make_path dirpath id, make_kn mp dir (Label.of_id id) -(* to this type are mapped Dir_path.t's in the nametab *) +(* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of Dir_path.t + | DirClosedSection of DirPath.t (* this won't last long I hope! *) let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - Dir_path.equal d1 d2 && - Dir_path.equal p1 p2 && + DirPath.equal d1 d2 && + DirPath.equal p1 p2 && mp_eq mp1 mp2 let eq_global_dir_reference r1 r2 = match r1, r2 with @@ -172,7 +172,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 | DirModule op1, DirModule op2 -> eq_op op1 op2 -| DirClosedSection dp1, DirClosedSection dp2 -> Dir_path.equal dp1 dp2 +| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2 | _ -> false type reference = diff --git a/library/libnames.mli b/library/libnames.mli index 090709549..c44fea543 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -13,31 +13,31 @@ open Names (** {6 Dirpaths } *) (** FIXME: ought to be in Names.dir_path *) -val pr_dirpath : Dir_path.t -> Pp.std_ppcmds +val pr_dirpath : DirPath.t -> Pp.std_ppcmds -val dirpath_of_string : string -> Dir_path.t -val string_of_dirpath : Dir_path.t -> string +val dirpath_of_string : string -> DirPath.t +val string_of_dirpath : DirPath.t -> string -(** Pop the suffix of a [Dir_path.t] *) -val pop_dirpath : Dir_path.t -> Dir_path.t +(** Pop the suffix of a [DirPath.t] *) +val pop_dirpath : DirPath.t -> DirPath.t (** Pop the suffix n times *) -val pop_dirpath_n : int -> Dir_path.t -> Dir_path.t +val pop_dirpath_n : int -> DirPath.t -> DirPath.t -(** Give the immediate prefix and basename of a [Dir_path.t] *) -val split_dirpath : Dir_path.t -> Dir_path.t * Id.t +(** Give the immediate prefix and basename of a [DirPath.t] *) +val split_dirpath : DirPath.t -> DirPath.t * Id.t -val add_dirpath_suffix : Dir_path.t -> module_ident -> Dir_path.t -val add_dirpath_prefix : module_ident -> Dir_path.t -> Dir_path.t +val add_dirpath_suffix : DirPath.t -> module_ident -> DirPath.t +val add_dirpath_prefix : module_ident -> DirPath.t -> DirPath.t -val chop_dirpath : int -> Dir_path.t -> Dir_path.t * Dir_path.t -val append_dirpath : Dir_path.t -> Dir_path.t -> Dir_path.t +val chop_dirpath : int -> DirPath.t -> DirPath.t * DirPath.t +val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t -val drop_dirpath_prefix : Dir_path.t -> Dir_path.t -> Dir_path.t -val is_dirpath_prefix_of : Dir_path.t -> Dir_path.t -> bool +val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t +val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool -module Dirset : Set.S with type elt = Dir_path.t -module Dirmap : Map.S with type key = Dir_path.t +module Dirset : Set.S with type elt = DirPath.t +module Dirmap : Map.S with type key = DirPath.t (** {6 Full paths are {e absolute} paths of declarations } *) type full_path @@ -45,11 +45,11 @@ type full_path val eq_full_path : full_path -> full_path -> bool (** Constructors of [full_path] *) -val make_path : Dir_path.t -> Id.t -> full_path +val make_path : DirPath.t -> Id.t -> full_path (** Destructors of [full_path] *) -val repr_path : full_path -> Dir_path.t * Id.t -val dirpath : full_path -> Dir_path.t +val repr_path : full_path -> DirPath.t * Id.t +val dirpath : full_path -> DirPath.t val basename : full_path -> Id.t (** Parsing and printing of section path as ["coq_root.module.id"] *) @@ -69,8 +69,8 @@ val restrict_path : int -> full_path -> full_path type qualid -val make_qualid : Dir_path.t -> Id.t -> qualid -val repr_qualid : qualid -> Dir_path.t * Id.t +val make_qualid : DirPath.t -> Id.t -> qualid +val repr_qualid : qualid -> DirPath.t * Id.t val qualid_eq : qualid -> qualid -> bool @@ -82,7 +82,7 @@ val qualid_of_string : string -> qualid qualified name denoting the same name *) val qualid_of_path : full_path -> qualid -val qualid_of_dirpath : Dir_path.t -> qualid +val qualid_of_dirpath : DirPath.t -> qualid val qualid_of_ident : Id.t -> qualid (** Both names are passed to objects: a "semantic" [kernel_name], which @@ -91,19 +91,19 @@ val qualid_of_ident : Id.t -> qualid type object_name = full_path * kernel_name -type object_prefix = Dir_path.t * (module_path * Dir_path.t) +type object_prefix = DirPath.t * (module_path * DirPath.t) val eq_op : object_prefix -> object_prefix -> bool val make_oname : object_prefix -> Id.t -> object_name -(** to this type are mapped [Dir_path.t]'s in the nametab *) +(** to this type are mapped [DirPath.t]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix | DirModule of object_prefix - | DirClosedSection of Dir_path.t + | DirClosedSection of DirPath.t (** this won't last long I hope! *) val eq_global_dir_reference : diff --git a/library/library.ml b/library/library.ml index 0fdd6d75e..92104348e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -20,7 +20,7 @@ open Lib (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) -type logical_path = Dir_path.t +type logical_path = DirPath.t let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list) @@ -49,15 +49,15 @@ let add_load_path isroot (phys_path,coq_path) = let filter (p, _, _) = String.equal p phys_path in match List.filter filter !load_paths with | [_,dir,_] -> - if not (Dir_path.equal coq_path dir) + if not (DirPath.equal coq_path dir) (* If this is not the default -I . to coqtop *) && not (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) - && Dir_path.equal coq_path (Nameops.default_root_prefix)) + && DirPath.equal coq_path (Nameops.default_root_prefix)) then begin (* Assume the user is concerned by library naming *) - if not (Dir_path.equal dir Nameops.default_root_prefix) then + if not (DirPath.equal dir Nameops.default_root_prefix) then Flags.if_warn msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ @@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) = let extend_path_with_dirpath p dir = List.fold_left Filename.concat p - (List.rev_map Id.to_string (Dir_path.repr dir)) + (List.rev_map Id.to_string (DirPath.repr dir)) let root_paths_matching_dir_path dir = let rec aux = function @@ -90,7 +90,7 @@ let root_paths_matching_dir_path dir = let intersections d1 d2 = let rec aux d1 = - if Dir_path.is_empty d1 then [d2] else + if DirPath.is_empty d1 then [d2] else let rest = aux (snd (chop_dirpath 1 d1)) in if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest else rest in @@ -114,7 +114,7 @@ let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (*s Modules on disk contain the following informations (after the magic number, and before the digest). *) -type compilation_unit_name = Dir_path.t +type compilation_unit_name = DirPath.t type library_disk = { md_name : compilation_unit_name; @@ -134,7 +134,7 @@ type library_t = { library_imports : compilation_unit_name list; library_digest : Digest.t } -module LibraryOrdered = Dir_path +module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) @@ -182,7 +182,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (Dir_path.to_string dir)) + error ("Unknown library " ^ (DirPath.to_string dir)) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -205,7 +205,7 @@ let library_is_loaded dir = with Not_found -> false let library_is_opened dir = - List.exists (fun m -> Dir_path.equal m.library_name dir) !libraries_imports_list + List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list @@ -226,7 +226,7 @@ let register_loaded_library m = in let rec aux = function | [] -> link m; [m] - | m'::_ as l when Dir_path.equal m'.library_name m.library_name -> l + | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; libraries_table := LibraryMap.add m.library_name m !libraries_table @@ -240,7 +240,7 @@ let register_loaded_library m = let rec remember_last_of_each l m = match l with | [] -> [m] - | m'::l' when Dir_path.equal m'.library_name m.library_name -> remember_last_of_each l' m + | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m | m'::l' -> m' :: remember_last_of_each l' m let register_open_library export m = @@ -254,7 +254,7 @@ let register_open_library export m = (* [open_library export explicit m] opens library [m] if not already opened _or_ if explicitly asked to be (re)opened *) -let eq_lib_name m1 m2 = Dir_path.equal m1.library_name m2.library_name +let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name let open_library export explicit_libs m = if @@ -303,7 +303,7 @@ let subst_import (_,o) = o let classify_import (_,export as obj) = if export then Substitute obj else Dispose -let in_import : Dir_path.t * bool -> obj = +let in_import : DirPath.t * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; @@ -434,7 +434,7 @@ let rec intern_library needed (dir, f) = with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in - if not (Dir_path.equal dir m.library_name) then + if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" (str ("The file " ^ f ^ " contains library") ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ @@ -447,9 +447,9 @@ and intern_library_deps needed dir m = and intern_mandatory_library caller needed (dir,d) = let m,needed = intern_library needed (try_locate_absolute_library dir) in if not (String.equal d m.library_digest) then - errorlabstrm "" (strbrk ("Compiled library "^(Dir_path.to_string caller)^ + errorlabstrm "" (strbrk ("Compiled library "^(DirPath.to_string caller)^ ".vo makes inconsistent assumptions over library " - ^(Dir_path.to_string dir))); + ^(DirPath.to_string dir))); needed let rec_intern_library needed mref = @@ -533,7 +533,7 @@ let discharge_require (_,o) = Some o (* open_function is never called from here because an Anticipate object *) -type require_obj = library_t list * Dir_path.t list * bool option +type require_obj = library_t list * DirPath.t list * bool option let in_require : require_obj -> obj = declare_object {(default_object "REQUIRE") with @@ -604,11 +604,11 @@ let import_module export (loc,qid) = (*s Initializing the compilation of a library. *) let check_coq_overwriting p id = - let l = Dir_path.repr p in + let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (strbrk ("Cannot build module "^Dir_path.to_string p^"."^Id.to_string id^ + (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^ ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) let start_library f = diff --git a/library/library.mli b/library/library.mli index 6cf4107cb..11253087a 100644 --- a/library/library.mli +++ b/library/library.mli @@ -24,7 +24,7 @@ open Libobject (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library : qualid located list -> bool option -> unit -val require_library_from_dirpath : (Dir_path.t * string) list -> bool option -> unit +val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit @@ -34,40 +34,40 @@ val require_library_from_file : val import_module : bool -> qualid located -> unit (** {6 Start the compilation of a library } *) -val start_library : string -> Dir_path.t * string +val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : Dir_path.t -> string -> unit +val save_library_to : DirPath.t -> string -> unit (** {6 Interrogate the status of libraries } *) (** - Tell if a library is loaded or opened *) -val library_is_loaded : Dir_path.t -> bool -val library_is_opened : Dir_path.t -> bool +val library_is_loaded : DirPath.t -> bool +val library_is_opened : DirPath.t -> bool (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> Dir_path.t list -val opened_libraries : unit -> Dir_path.t list +val loaded_libraries : unit -> DirPath.t list +val opened_libraries : unit -> DirPath.t list (** - Return the full filename of a loaded library. *) -val library_full_filename : Dir_path.t -> string +val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) -val set_xml_require : (Dir_path.t -> unit) -> unit +val set_xml_require : (DirPath.t -> unit) -> unit (** {6 ... } *) (** Global load paths: a load path is a physical path in the file - system; to each load path is associated a Coq [Dir_path.t] (the "logical" + system; to each load path is associated a Coq [DirPath.t] (the "logical" path of the physical path) *) val get_load_paths : unit -> CUnix.physical_path list -val get_full_load_paths : unit -> (CUnix.physical_path * Dir_path.t) list -val add_load_path : bool -> CUnix.physical_path * Dir_path.t -> unit +val get_full_load_paths : unit -> (CUnix.physical_path * DirPath.t) list +val add_load_path : bool -> CUnix.physical_path * DirPath.t -> unit val remove_load_path : CUnix.physical_path -> unit -val find_logical_path : CUnix.physical_path -> Dir_path.t +val find_logical_path : CUnix.physical_path -> DirPath.t val is_in_load_paths : CUnix.physical_path -> bool (** {6 Locate a library in the load paths } *) @@ -76,8 +76,8 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * Dir_path.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> Dir_path.t * string + bool -> qualid -> library_location * DirPath.t * CUnix.physical_path +val try_locate_qualified_library : qualid located -> DirPath.t * string (** {6 Statistics: display the memory use of a library. } *) -val mem : Dir_path.t -> Pp.std_ppcmds +val mem : DirPath.t -> Pp.std_ppcmds diff --git a/library/nameops.ml b/library/nameops.ml index 0891d306b..3b8de17d2 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -138,11 +138,11 @@ let name_fold_map f e = function let pr_lab l = str (Label.to_string l) -let default_library = Names.Dir_path.initial (* = ["Top"] *) +let default_library = Names.DirPath.initial (* = ["Top"] *) (*s Roots of the space of absolute names *) let coq_root = Id.of_string "Coq" -let default_root_prefix = Dir_path.empty +let default_root_prefix = DirPath.empty (* Metavariables *) let pr_meta = Pp.int diff --git a/library/nameops.mli b/library/nameops.mli index 1d3275d30..53cc86786 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -40,14 +40,14 @@ val pr_lab : Label.t -> Pp.std_ppcmds (** some preset paths *) -val default_library : Dir_path.t +val default_library : DirPath.t (** This is the root of the standard library of Coq *) val coq_root : module_ident (** This is the default root prefix for developments which doesn't mention a root *) -val default_root_prefix : Dir_path.t +val default_root_prefix : DirPath.t (** Metavariables *) val pr_meta : Term.metavariable -> Pp.std_ppcmds diff --git a/library/nametab.ml b/library/nametab.ml index 92b13d669..01324a3a4 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -42,7 +42,7 @@ type visibility = Until of int | Exactly of int (* Data structure for nametabs *******************************************) -(* This module type will be instantiated by [full_path] of [Dir_path.t] *) +(* This module type will be instantiated by [full_path] of [DirPath.t] *) (* The [repr] function is assumed to return the reversed list of idents. *) module type UserName = sig type t @@ -194,7 +194,7 @@ let rec search tree = function let find_node qid tab = let (dir,id) = repr_qualid qid in - search (Id.Map.find id tab) (Dir_path.repr dir) + search (Id.Map.find id tab) (DirPath.repr dir) let locate qid tab = let o = match find_node qid tab with @@ -238,7 +238,7 @@ let shortest_qualid ctx uname tab = in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in - make_qualid (Dir_path.make found_dir) id + make_qualid (DirPath.make found_dir) id let push_node node l = match node with @@ -256,7 +256,7 @@ let rec search_prefixes tree = function let find_prefixes qid tab = try let (dir,id) = repr_qualid qid in - search_prefixes (Id.Map.find id tab) (Dir_path.repr dir) + search_prefixes (Id.Map.find id tab) (DirPath.repr dir) with Not_found -> [] end @@ -272,7 +272,7 @@ struct let to_string = string_of_path let repr sp = let dir,id = repr_path sp in - id, (Dir_path.repr dir) + id, (DirPath.repr dir) end module ExtRefEqual = @@ -298,12 +298,10 @@ let the_tactictab = ref (KnTab.empty : kntab) type mptab = MPTab.t let the_modtypetab = ref (MPTab.empty : mptab) -module DirPath = +module DirPath' = struct - type t = Dir_path.t - let equal = Dir_path.equal - let to_string = Dir_path.to_string - let repr dir = match Dir_path.repr dir with + include DirPath + let repr dir = match DirPath.repr dir with | [] -> anomaly (Pp.str "Empty dirpath") | id :: l -> (id, l) end @@ -314,7 +312,7 @@ struct let equal = eq_global_dir_reference end -module DirTab = Make(DirPath)(GlobDir) +module DirTab = Make(DirPath')(GlobDir) (* If we have a (closed) module M having a submodule N, than N does not have the entry in [the_dirtab]. *) @@ -331,7 +329,7 @@ type globrevtab = full_path Globrevtab.t let the_globrevtab = ref (Globrevtab.empty : globrevtab) -type mprevtab = Dir_path.t MPmap.t +type mprevtab = DirPath.t MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t @@ -479,7 +477,7 @@ let exists_modtype sp = MPTab.exists sp !the_modtypetab let path_of_global ref = match ref with - | VarRef id -> make_path Dir_path.empty id + | VarRef id -> make_path DirPath.empty id | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab let dirpath_of_global ref = @@ -501,7 +499,7 @@ let path_of_tactic kn = let shortest_qualid_of_global ctx ref = match ref with - | VarRef id -> make_qualid Dir_path.empty id + | VarRef id -> make_qualid DirPath.empty id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in ExtRefTab.shortest_qualid ctx sp !the_ccitab diff --git a/library/nametab.mli b/library/nametab.mli index 188e2dcee..d561735fd 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -17,7 +17,7 @@ open Globnames qualified names (qualid). There are three classes of names: - 1a) internal kernel names: [kernel_name], [constant], [inductive], - [module_path], [Dir_path.t] + [module_path], [DirPath.t] - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... @@ -33,7 +33,7 @@ open Globnames 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 [full_path] or a [Dir_path.t]. + [full_user_name] can either be a [full_path] or a [DirPath.t]. } {- [exists : full_user_name -> bool] @@ -79,7 +79,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit val push_modtype : visibility -> full_path -> module_path -> unit -val push_dir : visibility -> Dir_path.t -> global_dir_reference -> unit +val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit type ltac_constant = kernel_name @@ -98,7 +98,7 @@ val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path -val locate_section : qualid -> Dir_path.t +val locate_section : qualid -> DirPath.t val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global @@ -123,15 +123,15 @@ val extended_global_of_path : full_path -> extended_global_reference val exists_cci : full_path -> bool val exists_modtype : full_path -> bool -val exists_dir : Dir_path.t -> bool -val exists_section : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) -val exists_module : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_dir : DirPath.t -> bool +val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) (** {6 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.t +val full_name_module : qualid -> DirPath.t (** {6 Reverse lookup } Finding user names corresponding to the given @@ -142,13 +142,13 @@ val full_name_module : qualid -> Dir_path.t val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> Dir_path.t +val dirpath_of_module : module_path -> DirPath.t val path_of_tactic : ltac_constant -> 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.t +val dirpath_of_global : global_reference -> DirPath.t val basename_of_global : global_reference -> Id.t (** Printing of global references using names as short as possible *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index eb27c2f4e..e80d9301f 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -248,7 +248,7 @@ type tactic_grammar = { tacgram_key : string; tacgram_level : int; tacgram_prods : grammar_prod_item list; - tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr; + tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } type all_grammar_command = diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 1cc890158..91a636306 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -43,7 +43,7 @@ type tactic_grammar = { tacgram_key : string; tacgram_level : int; tacgram_prods : grammar_prod_item list; - tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr; + tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr; } (** Adding notations *) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 5f75a1d9e..f30ebfb7c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] let _ = List.iter Lexer.add_keyword prim_kw -let local_make_qualid l id = make_qualid (Dir_path.make l) id +let local_make_qualid l id = make_qualid (DirPath.make l) id let my_int_of_string loc s = try @@ -101,7 +101,7 @@ GEXTEND Gram ; dirpath: [ [ id = ident; l = LIST0 field -> - Dir_path.make (List.rev (id::l)) ] ] + DirPath.make (List.rev (id::l)) ] ] ; string: [ [ s = STRING -> s ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8ccc3ebef..bbb71a170 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -174,7 +174,7 @@ module Prim : val reference : reference Gram.entry val by_notation : (Loc.t * string * string option) Gram.entry val smart_global : reference or_by_notation Gram.entry - val dirpath : Dir_path.t Gram.entry + val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry val ne_lstring : string located Gram.entry val var : Id.t located Gram.entry diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 286c11e5a..073f77403 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -584,7 +584,7 @@ let pp_module mp = the constants are directly turned into chars *) let mk_ind path s = - make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (Label.make s) + make_mind (MPfile (dirpath_of_string path)) DirPath.empty (Label.make s) let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 85b9bde71..e94644821 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl = let rec extract_sfb_spec env mp = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = make_con mp Dir_path.empty l in + let kn = make_con mp DirPath.empty l in let s = extract_constant_spec env kn cb in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = make_mind mp Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs @@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vc = Array.map (make_con mp Dir_path.empty) vl in + let vc = Array.map (make_con mp DirPath.empty) vl in let ms = extract_sfb env mp all msb in let b = Array.exists Visit.needed_con vc in if all || b then @@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function else ms with Impossible -> let ms = extract_sfb env mp all msb in - let c = make_con mp Dir_path.empty l in + let c = make_con mp DirPath.empty l in let b = Visit.needed_con c in if all || b then let d = extract_constant env c cb in @@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let mind = make_mind mp Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index dba77b923..7d95d2e17 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1304,9 +1304,9 @@ let inline_test r t = not (is_fix t2) && ml_size t < 12 && is_not_strict t) let con_of_string s = - let null = Dir_path.empty in - match Dir_path.repr (dirpath_of_string s) with - | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id) + let null = DirPath.empty in + match DirPath.repr (dirpath_of_string s) with + | id :: d -> make_con (MPfile (DirPath.make d)) null (Label.of_id id) | [] -> assert false let manual_inline_set = diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index eb166675e..01234aa18 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp = let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l')) in + let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index fbd3fd4ea..dfa5ff6f9 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -650,7 +650,7 @@ and pp_module_type params = function let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in + let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 320e0d1fc..aabbdc7a4 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -56,7 +56,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (Id.to_string (List.hd (Dir_path.repr f))) + | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -175,7 +175,7 @@ let add_recursors env kn = make_con_equiv (modpath (user_mind kn)) (modpath (canonical_mind kn)) - Dir_path.empty (Label.of_id id) + DirPath.empty (Label.of_id id) in let mib = Environ.lookup_mind kn env in Array.iter @@ -272,7 +272,7 @@ let safe_pr_long_global r = | _ -> assert false let pr_long_mp mp = - let lid = Dir_path.repr (Nametab.dirpath_of_module mp) in + let lid = DirPath.repr (Nametab.dirpath_of_module mp) in str (String.concat "." (List.rev_map Id.to_string lid)) let pr_long_global ref = pr_path (Nametab.path_of_global ref) @@ -424,7 +424,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (current_toplevel ()) with | MPfile dp' when dp<>dp' -> - err (str ("Please load library "^(Dir_path.to_string dp^" first."))) + err (str ("Please load library "^(DirPath.to_string dp^" first."))) | _ -> () end | _ -> () @@ -727,7 +727,7 @@ let string_of_modfile mp = let file_of_modfile mp = let s0 = match mp with - | MPfile f -> Id.to_string (List.hd (Dir_path.repr f)) + | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in let s = String.copy (string_of_modfile mp) in diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 1a97689b5..53acccf84 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -46,7 +46,7 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * Dir_path.t * Label.t +val repr_of_r : global_reference -> module_path * DirPath.t * Label.t val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> Label.t val current_toplevel : unit -> module_path diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4c3c48915..fbb00285c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -81,8 +81,8 @@ type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = match Names.repr_con kn with | MPfile dir, sec_dir, id when - sec_dir = Dir_path.empty && - Dir_path.to_string dir = "Coq.Reals.Rdefinitions" + sec_dir = DirPath.empty && + DirPath.to_string dir = "Coq.Reals.Rdefinitions" -> Label.to_string id | _ -> "constant_not_of_R" diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 69e22da43..99bf66d1f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -460,7 +460,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match wf_rel_expr_opt with | None -> let ltof = - let make_dir l = Dir_path.make (List.rev_map Id.of_string l) in + let make_dir l = DirPath.make (List.rev_map Id.of_string l) in Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e89e2f894..92d2fe680 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -132,7 +132,7 @@ let coq_constant s = Coqlib.init_modules s;; let find_reference sl s = - let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in + let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) let eq = lazy(coq_constant "eq") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index addce6b1c..d5e1ee53a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -50,7 +50,7 @@ let coq_base_constant s = (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; let find_reference sl s = - let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in + let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 11281f114..d23a07ba6 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -19,7 +19,7 @@ let meaningful_submodule = [ "Z"; "N"; "Pos" ] let string_of_global r = let dp = Nametab.dirpath_of_global r in - let prefix = match Names.Dir_path.repr dp with + let prefix = match Names.DirPath.repr dp with | [] -> "" | m::_ -> let s = Names.Id.to_string m in diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 6cfac9605..35189f786 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -245,13 +245,13 @@ let my_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) let new_ring_path = - Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = - lazy(make_kn (MPfile new_ring_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) let znew_ring_path = - Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; @@ -827,10 +827,10 @@ END (***********************************************************************) let new_field_path = - Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index fc64da58e..b6fdf315c 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -16,7 +16,7 @@ open Coqlib exception Non_closed_ascii -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index ef4636699..8d3629d35 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -15,10 +15,10 @@ open Glob_term (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***) -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) -let make_mind mp id = Names.make_mind mp Dir_path.empty (Label.make id) +let make_mind mp id = Names.make_mind mp DirPath.empty (Label.make id) let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = let mp = MPdot (MPfile (make_dir dir), Label.make modname) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 055b99adc..bddca9e65 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -19,7 +19,7 @@ exception Non_closed_number open Glob_term open Bigint -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] let make_path dir id = Libnames.make_path dir (Id.of_string id) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index ca02f61b7..e5e4e9331 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -23,7 +23,7 @@ open Glob_term let binnums = ["Coq";"Numbers";"BinNums"] -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let positive_path = make_path binnums "positive" diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 90712c473..5f4add47a 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -38,7 +38,7 @@ let get_module_path_of_full_path path = let remove_module_dirpath_from_dirpath ~basedir dir = let module Ln = Libnames in if Ln.is_dirpath_prefix_of basedir dir then - let ids = Names.Dir_path.repr dir in + let ids = Names.DirPath.repr dir in let rec remove_firsts n l = match n,l with (0,l) -> l @@ -48,11 +48,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let ids' = List.rev (remove_firsts - (List.length (Names.Dir_path.repr basedir)) + (List.length (Names.DirPath.repr basedir)) (List.rev ids)) in ids' - else Names.Dir_path.repr dir + else Names.DirPath.repr dir ;; @@ -63,7 +63,7 @@ let get_uri_of_var v pvars = function [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> - let dirpath = N.Dir_path.make modules in + let dirpath = N.DirPath.make modules in if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then modules else @@ -73,7 +73,7 @@ let get_uri_of_var v pvars = if List.mem v pvars then [] else - search_in_open_sections (N.Dir_path.repr (Lib.cwd ())) + search_in_open_sections (N.DirPath.repr (Lib.cwd ())) in "cic:" ^ List.fold_left @@ -108,21 +108,21 @@ let ext_of_tag = exception FunctorsXMLExportationNotImplementedYet;; let subtract l1 l2 = - let l1' = List.rev (Names.Dir_path.repr l1) in - let l2' = List.rev (Names.Dir_path.repr l2) in + let l1' = List.rev (Names.DirPath.repr l1) in + let l2' = List.rev (Names.DirPath.repr l2) in let rec aux = function he::tl when tl = l2' -> [he] | he::tl -> he::(aux tl) | [] -> assert (l2' = []) ; [] in - Names.Dir_path.make (List.rev (aux l1')) + Names.DirPath.make (List.rev (aux l1')) ;; let token_list_of_path dir id tag = let module N = Names in let token_list_of_dirpath dirpath = - List.rev_map N.Id.to_string (N.Dir_path.repr dirpath) in + List.rev_map N.Id.to_string (N.DirPath.repr dirpath) in token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index fcd01569a..c95cf94b6 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -20,7 +20,7 @@ let cprop = N.make_con (N.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.Dir_path.empty) + (N.DirPath.empty) (N.Label.make "CProp") ;; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 91e15e8a6..033c84691 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -46,7 +46,7 @@ let filter_params pvars hyps = let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - aux (Names.Dir_path.repr modulepath) (List.rev pvars) + aux (Names.DirPath.repr modulepath) (List.rev pvars) ;; (* The computation is very inefficient, but we can't do anything *) @@ -62,7 +62,7 @@ let search_variables () = [] -> [] | he::tl as modules -> let one_section_variables = - let dirpath = N.Dir_path.make (modules @ N.Dir_path.repr modulepath) in + let dirpath = N.DirPath.make (modules @ N.DirPath.repr modulepath) in let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in [he,t] in @@ -113,7 +113,7 @@ let theory_filename xml_library_root = match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> - let toks = List.map N.Id.to_string (N.Dir_path.repr (Lib.library_dp ())) in + let toks = List.map N.Id.to_string (N.DirPath.repr (Lib.library_dp ())) in (* theory from A/B/C/F.v goes into A/B/C/F.theory *) let alltoks = List.rev toks in Some (join_dirs xml_library_root' alltoks ^ ".theory") @@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ; let uri_of_dirpath dir = "/" ^ String.concat "/" - (List.rev_map Names.Id.to_string (Names.Dir_path.repr dir)) + (List.rev_map Names.Id.to_string (Names.DirPath.repr dir)) ;; let _ = @@ -550,5 +550,5 @@ let _ = Library.set_xml_require (fun d -> theory_output_string (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>" - (uri_of_dirpath d) (Names.Dir_path.to_string d))) + (uri_of_dirpath d) (Names.DirPath.to_string d))) ;; diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 8009524de..bf1adb3cf 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -30,7 +30,7 @@ let is_imported_modpath mp = match mp with | MPfile dp -> let rec find_prefix = function - |MPfile dp1 -> not (Dir_path.equal dp1 dp) + |MPfile dp1 -> not (DirPath.equal dp1 dp) |MPdot(mp,_) -> find_prefix mp |MPbound(_) -> false in find_prefix current_mp diff --git a/pretyping/program.ml b/pretyping/program.ml index 1201ff8e0..a701fdef4 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -12,7 +12,7 @@ open Util open Names open Term -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7359b2e2a..624645a8f 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -259,7 +259,7 @@ let magicaly_constant_of_fixbody env bd = function | Name.Name id -> try let cst = Nametab.locate_constant - (Libnames.make_qualid Dir_path.empty id) in + (Libnames.make_qualid DirPath.empty id) in match constant_opt_value env cst with | None -> bd | Some t -> if eq_constr t bd then mkConst cst else bd diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d10289820..825a6adb7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -141,7 +141,7 @@ let print_env env = in (sign_env ++ db_env) -(*let current_module = ref Dir_path.empty +(*let current_module = ref DirPath.empty let set_module m = current_module := m*) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0264f67fa..732903af9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -331,7 +331,7 @@ let print_located_qualid ref = match List.map expand (N.locate_extended_all qid) with | [] -> let (dir,id) = repr_qualid qid in - if Dir_path.is_empty dir then + if DirPath.is_empty dir then str "No object of basename " ++ pr_id id else str "No object of suffix " ++ pr_qualid qid @@ -634,7 +634,7 @@ let print_any_name = function | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in - if not (Dir_path.is_empty dir) then raise Not_found; + if not (DirPath.is_empty dir) then raise Not_found; let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) with Not_found -> diff --git a/printing/printmod.ml b/printing/printmod.ml index c9341eead..0b8393d52 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -37,7 +37,7 @@ let _ = let get_new_id locals id = let rec get_id l id = - let dir = Dir_path.make [id] in + let dir = DirPath.make [id] in if not (Nametab.exists_module dir) then id else @@ -71,9 +71,9 @@ let print_kn locals kn = let nametab_register_dir mp = let id = Id.of_string "FAKETOP" in - let fp = Libnames.make_path Dir_path.empty id in - let dir = Dir_path.make [id] in - Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,Dir_path.empty))); + let fp = Libnames.make_path DirPath.empty id in + let dir = DirPath.make [id] in + Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))); fp (** Nota: the [global_reference] we register in the nametab below @@ -90,9 +90,9 @@ let nametab_register_body mp fp (l,body) = | SFBmodule _ -> () (* TODO *) | SFBmodtype _ -> () (* TODO *) | SFBconst _ -> - push (Label.to_id l) (ConstRef (make_con mp Dir_path.empty l)) + push (Label.to_id l) (ConstRef (make_con mp DirPath.empty l)) | SFBmind mib -> - let mind = make_mind mp Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in Array.iteri (fun i mip -> push mip.mind_typename (IndRef (mind,i)); @@ -126,7 +126,7 @@ let print_body is_impl env mp (l,body) = | SFBmind mib -> try let env = Option.get env in - Printer.pr_mutual_inductive_body env (make_mind mp Dir_path.empty l) mib + Printer.pr_mutual_inductive_body env (make_mind mp DirPath.empty l) mib with _ -> (if mib.mind_finite then str "Inductive " else str "CoInductive") ++ name) @@ -208,7 +208,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with let rec printable_body dir = let dir = pop_dirpath dir in - Dir_path.is_empty dir || + DirPath.is_empty dir || try match Nametab.locate_dir (qualid_of_dirpath dir) with DirOpenModtype _ -> false diff --git a/printing/printmod.mli b/printing/printmod.mli index afd4d37f3..1e6d1f4ce 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -9,7 +9,7 @@ open Names (** false iff the module is an element of an open module type *) -val printable_body : Dir_path.t -> bool +val printable_body : DirPath.t -> bool val print_module : bool -> module_path -> Pp.std_ppcmds diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index fbe11432e..f7f52de70 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -38,7 +38,7 @@ open Decl_kinds (** Typeclass-based generalized rewriting. *) let classes_dirpath = - Dir_path.make (List.map Id.of_string ["Classes";"Coq"]) + DirPath.make (List.map Id.of_string ["Classes";"Coq"]) let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () @@ -52,7 +52,7 @@ let proper_proxy_class = let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 8712b291e..b9a9d4d83 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -298,7 +298,7 @@ let tauto_intuitionistic flags g = let coq_nnpp_path = let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in - Libnames.make_path (Dir_path.make dir) (Id.of_string "NNPP") + Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP") let tauto_classical flags nnpp g = try tclTHEN (apply nnpp) (tauto_intuitionistic flags) g diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 51e567f0a..046bf7812 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -59,8 +59,8 @@ let load_rcfile() = (* Puts dir in the path of ML and in the LoadPath *) let coq_add_path unix_path s = - Mltop.add_path ~unix_path ~coq_root:(Names.Dir_path.make [Nameops.coq_root;Names.Id.of_string s]) -let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.Dir_path.make [Nameops.coq_root]) + Mltop.add_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) +let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root]) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -107,7 +107,7 @@ let init_load_path () = if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; (* then standard library *) List.iter - (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.Dir_path.make [Names.Id.of_string alias; Nameops.coq_root])) + (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.DirPath.make [Names.Id.of_string alias; Nameops.coq_root])) theories_dirs_map; (* then plugins *) List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs; diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 0039620f0..88b7a9e9d 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,8 +15,8 @@ val set_rcfile : string -> unit val no_load_rc : unit -> unit val load_rcfile : unit -> unit -val push_include : string * Names.Dir_path.t -> unit -val push_rec_include : string * Names.Dir_path.t -> unit +val push_include : string * Names.DirPath.t -> unit +val push_rec_include : string * Names.DirPath.t -> unit val init_load_path : unit -> unit val init_library_roots : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8ba105657..fadf301b8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -52,10 +52,10 @@ let engage () = let set_batch_mode () = batch_mode := true -let toplevel_default_name = Dir_path.make [Id.of_string "Top"] +let toplevel_default_name = DirPath.make [Id.of_string "Top"] let toplevel_name = ref (Some toplevel_default_name) let set_toplevel_name dir = - if Dir_path.is_empty dir then error "Need a non empty toplevel module name"; + if DirPath.is_empty dir then error "Need a non empty toplevel module name"; toplevel_name := Some dir let unset_toplevel_name () = toplevel_name := None diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 98ba3e792..fcec3a128 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -231,11 +231,11 @@ let inloadpath dir = Library.is_in_load_paths (CUnix.physical_path_of_string dir) let status () = - (** We remove the initial part of the current [Dir_path.t] + (** We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) let path = - let l = Names.Dir_path.repr (Lib.cwd ()) in + let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l in let proof = diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 59fb3bbc1..c4d9dcaf4 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -171,11 +171,11 @@ let convert_string d = let add_rec_path ~unix_path ~coq_root = if exists_dir unix_path then let dirs = all_subdirs ~unix_path in - let prefix = Names.Dir_path.repr coq_root in + let prefix = Names.DirPath.repr coq_root in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.Dir_path.make path) + Some (lp, Names.DirPath.make path) with Exit -> None in let dirs = List.map_filter convert_dirs dirs in diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 761a52d4a..3696a654f 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -43,8 +43,8 @@ val add_ml_dir : string -> unit val add_rec_ml_dir : string -> unit (** Adds a path to the Coq and ML paths *) -val add_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit -val add_rec_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit +val add_path : unix_path:string -> coq_root:Names.DirPath.t -> unit +val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> unit (** List of modules linked to the toplevel *) val add_known_module : string -> unit diff --git a/toplevel/search.ml b/toplevel/search.ml index 30e7dca8b..80ffa36fb 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -118,7 +118,7 @@ let plain_display accu ref a c = let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) -let filter_by_module (module_list:Dir_path.t list) (accept:bool) +let filter_by_module (module_list:DirPath.t list) (accept:bool) (ref:global_reference) _ _ = let sp = path_of_global ref in let sl = dirpath sp in @@ -180,7 +180,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref) let full_name_of_reference ref = let (dir,id) = repr_path (path_of_global ref) in - Dir_path.to_string dir ^ "." ^ Id.to_string id + DirPath.to_string dir ^ "." ^ Id.to_string id (* * functions to use the new Libtypes facility @@ -317,10 +317,10 @@ let interface_search flags = in let ans = ref [] in let print_function ref env constr = - let fullpath = Dir_path.repr (Nametab.dirpath_of_global ref) in + let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in let (shortpath, basename) = Libnames.repr_qualid qualid in - let shortpath = Dir_path.repr shortpath in + let shortpath = DirPath.repr shortpath in (* [shortpath] is a suffix of [fullpath] and we're looking for the missing prefix *) let rec prefix full short accu = match full, short with diff --git a/toplevel/search.mli b/toplevel/search.mli index 919fafc6c..dce553c9f 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -23,11 +23,11 @@ type glob_search_about_item = type filter_function = global_reference -> env -> constr -> bool type display_function = global_reference -> env -> constr -> unit -val search_by_head : constr -> Dir_path.t list * bool -> std_ppcmds -val search_rewrite : constr -> Dir_path.t list * bool -> std_ppcmds -val search_pattern : constr -> Dir_path.t list * bool -> std_ppcmds +val search_by_head : constr -> DirPath.t list * bool -> std_ppcmds +val search_rewrite : constr -> DirPath.t list * bool -> std_ppcmds +val search_pattern : constr -> DirPath.t list * bool -> std_ppcmds val search_about : - (bool * glob_search_about_item) list -> Dir_path.t list * bool -> std_ppcmds + (bool * glob_search_about_item) list -> DirPath.t list * bool -> std_ppcmds val interface_search : (Interface.search_constraint * bool) list -> string Interface.coq_object list @@ -35,7 +35,7 @@ val interface_search : (Interface.search_constraint * bool) list -> (** The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. *) -val filter_by_module_from_list : Dir_path.t list * bool -> filter_function +val filter_by_module_from_list : DirPath.t list * bool -> filter_function val filter_blacklist : filter_function diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7ec19b26a..2cac3d98c 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -437,7 +437,7 @@ let load_vernac verb file = let compile verbosely f = let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in Dumpglob.start_dump_glob long_f_dot_v; - Dumpglob.dump_string ("F" ^ Names.Dir_path.to_string ldir ^ "\n"); + Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in let pfs = Pfedit.get_all_proof_names () in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6b1055441..55a8f5f80 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -201,7 +201,7 @@ let show_match id = (* "Print" commands *) let print_path_entry (s,l) = - (str (Dir_path.to_string l) ++ str " " ++ tbrk (0,0) ++ str s) + (str (DirPath.to_string l) ++ str " " ++ tbrk (0,0) ++ str s) let print_loadpath dir = let l = Library.get_full_load_paths () in @@ -250,7 +250,7 @@ let print_modtype r = msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = - let ns = List.rev (Names.Dir_path.repr ns) in + let ns = List.rev (Names.DirPath.repr ns) in (* [match_dirpath], [match_modulpath] are helpers for [matches] which checks whether a constant is in the namespace [ns]. *) let rec match_dirpath ns = function @@ -266,7 +266,7 @@ let print_namespace ns = in let rec match_modulepath ns = function | MPbound _ -> None (* Not a proper namespace. *) - | MPfile dir -> match_dirpath ns (Names.Dir_path.repr dir) + | MPfile dir -> match_dirpath ns (Names.DirPath.repr dir) | MPdot (mp,lbl) -> let id = Names.Label.to_id lbl in begin match match_modulepath ns mp with @@ -286,7 +286,7 @@ let print_namespace ns = let qualified_minus n mp = let rec list_of_modulepath = function | MPbound _ -> assert false (* MPbound never matches *) - | MPfile dir -> Names.Dir_path.repr dir + | MPfile dir -> Names.DirPath.repr dir | MPdot (mp,lbl) -> (Names.Label.to_id lbl)::(list_of_modulepath mp) in snd (Util.List.chop n (List.rev (list_of_modulepath mp))) @@ -400,7 +400,7 @@ let print_located_module r = let dir = Nametab.full_name_module qid in msg_notice (str "Module " ++ pr_dirpath dir) with Not_found -> - if Dir_path.is_empty (fst (repr_qualid qid)) then + if DirPath.is_empty (fst (repr_qualid qid)) then msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid) else msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid) @@ -737,7 +737,7 @@ let vernac_begin_section (_, id as lid) = let vernac_end_section (loc,_) = Dumpglob.dump_reference loc - (Dir_path.to_string (Lib.current_dirpath true)) "<>" "sec"; + (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () (* Dispatcher of the "End" command *) @@ -1499,7 +1499,7 @@ let vernac_reset_name id = if not globalized then begin try begin match Lib.find_opening_node (snd id) with | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id) - (Dir_path.to_string (Lib.current_dirpath true)) "<>" "sec"; + (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; (* Might be nice to implement module cases, too.... *) | _ -> () end with UserError _ -> () diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 7e27d8693..8929fb32c 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -83,7 +83,7 @@ let error_whelp_unknown_reference ref = let uri_of_repr_kn ref (mp,dir,l) = match mp with | MPfile sl -> - uri_of_dirpath (Label.to_id l :: Dir_path.repr dir @ Dir_path.repr sl) + uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl) | _ -> error_whelp_unknown_reference ref |