From 248728628f5da946f96c22ba0a0e7e9b33019382 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 20:27:51 +0000 Subject: 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 --- library/libnames.ml | 60 ++++++++++++++++++++++++++--------------------------- 1 file changed, 30 insertions(+), 30 deletions(-) (limited to 'library/libnames.ml') 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 = -- cgit v1.2.3