From f42dd8d8530e6227621ccd662741f1da23700304 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 15:57:08 +0000 Subject: Modulification of dir_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 61 ++++++++++++++++++++++++++--------------------------- 1 file changed, 30 insertions(+), 31 deletions(-) (limited to 'library/libnames.ml') diff --git a/library/libnames.ml b/library/libnames.ml index ee24b2575..8e026d8c2 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,38 +13,38 @@ open Names (**********************************************) -let pr_dirpath sl = (str (string_of_dirpath sl)) +let pr_dirpath sl = (str (Dir_path.to_string sl)) (*s Operations on dirpaths *) (* Pop the last n module idents *) let pop_dirpath_n n dir = - make_dirpath (List.skipn n (repr_dirpath dir)) + Dir_path.make (List.skipn n (Dir_path.repr dir)) -let pop_dirpath p = match repr_dirpath p with +let pop_dirpath p = match Dir_path.repr p with | [] -> anomaly "dirpath_prefix: empty dirpath" - | _::l -> make_dirpath l + | _::l -> Dir_path.make l let is_dirpath_prefix_of d1 d2 = - List.prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) let chop_dirpath n d = - let d1,d2 = List.chop n (List.rev (repr_dirpath d)) in - make_dirpath (List.rev d1), make_dirpath (List.rev d2) + 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 drop_dirpath_prefix d1 d2 = - let d = Util.List.drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in - make_dirpath (List.rev d) + 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 append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1) +let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1) (* To know how qualified a name should be to be understood in the current env*) -let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) +let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id]) let split_dirpath d = - let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) + let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l) -let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p) +let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p) (* parsing *) let parse_dir s = @@ -68,23 +68,22 @@ let dirpath_of_string s = | "" -> [] | _ -> parse_dir s in - make_dirpath path + Dir_path.make path -let string_of_dirpath = Names.string_of_dirpath +let string_of_dirpath = Names.Dir_path.to_string - -module Dirset = Set.Make(struct type t = dir_path let compare = dir_path_ord end) -module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end) +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) (*s Section paths are absolute names *) type full_path = { - dirpath : dir_path ; + dirpath : Dir_path.t ; basename : Id.t } let eq_full_path p1 p2 = Id.equal p1.basename p2.basename && - Int.equal (dir_path_ord p1.dirpath p2.dirpath) 0 + Int.equal (Dir_path.compare p1.dirpath p2.dirpath) 0 let make_path pa id = { dirpath = pa; basename = id } @@ -93,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 repr_dirpath sl with + match Dir_path.repr sl with | [] -> Id.to_string id - | _ -> (string_of_dirpath sl) ^ "." ^ (Id.to_string id) + | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id) let sp_ord sp1 sp2 = let (p1,id1) = repr_path sp1 @@ -125,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 (repr_dirpath dir) in - make_path (make_dirpath dir') s + let dir' = List.firstn n (Dir_path.repr dir) in + make_path (Dir_path.make dir') s (*s qualified names *) type qualid = full_path @@ -142,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 empty_dirpath id +let qualid_of_ident id = make_qualid Dir_path.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 * (module_path * dir_path) +type object_prefix = Dir_path.t * (module_path * Dir_path.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's in the nametab *) +(* to this type are mapped Dir_path.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 + | DirClosedSection of Dir_path.t (* this won't last long I hope! *) let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - Int.equal (dir_path_ord d1 d2) 0 && - Int.equal (dir_path_ord p1 p2) 0 && + Int.equal (Dir_path.compare d1 d2) 0 && + Int.equal (Dir_path.compare p1 p2) 0 && mp_eq mp1 mp2 let eq_global_dir_reference r1 r2 = match r1, r2 with @@ -173,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 -> Int.equal (dir_path_ord dp1 dp2) 0 +| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (Dir_path.compare dp1 dp2) 0 | _ -> false type reference = -- cgit v1.2.3