From f6d8fc17dc9474e4d043cf709d672d9259599354 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 Aug 2013 14:30:01 +0000 Subject: Nicer code concerning dirpaths and modpath around Lib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'library/libnames.ml') diff --git a/library/libnames.ml b/library/libnames.ml index bc2406f27..d1bef531a 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -17,33 +17,34 @@ 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 = - DirPath.make (List.skipn n (DirPath.repr dir)) +let split_dirpath d = match DirPath.repr d with + | id :: l -> DirPath.make l, id + | _ -> failwith "split_dirpath" let pop_dirpath p = match DirPath.repr p with - | [] -> anomaly (str "dirpath_prefix: empty dirpath") | _::l -> DirPath.make l + | [] -> failwith "pop_dirpath" + +(* Pop the last n module idents *) +let pop_dirpath_n n dir = DirPath.make (List.skipn n (DirPath.repr dir)) let is_dirpath_prefix_of d1 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 (DirPath.repr d)) in - DirPath.make (List.rev d1), DirPath.make (List.rev d2) + DirPath.make (List.rev d1), DirPath.make (List.rev d2) let drop_dirpath_prefix d1 d2 = - let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in - DirPath.make (List.rev d) + let d = + List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) + in + DirPath.make (List.rev d) 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 = DirPath.make (DirPath.repr d @ [id]) -let split_dirpath d = - let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l) - let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) (* parsing *) -- cgit v1.2.3