diff options
| -rw-r--r-- | lib/cList.ml | 28 | ||||
| -rw-r--r-- | lib/cList.mli | 4 | ||||
| -rw-r--r-- | library/libnames.ml | 6 |
3 files changed, 19 insertions, 19 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index a6d157291..e0ac9839f 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -118,8 +118,8 @@ sig val skipn : int -> 'a list -> 'a list val skipn_at_least : int -> 'a list -> 'a list val addn : int -> 'a -> 'a list -> 'a list - val prefix_of : 'a list -> 'a list -> bool - val drop_prefix : 'a list -> 'a list -> 'a list + val prefix_of : 'a eq -> 'a list -> 'a list -> bool + val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list val drop_last : 'a list -> 'a list val map_append : ('a -> 'b list) -> 'a list -> 'b list val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list @@ -653,25 +653,23 @@ let rec skipn n l = match n,l with let skipn_at_least n l = try skipn n l with Failure _ -> [] -let prefix_of prefl l = +let prefix_of cmp prefl l = let rec prefrec = function - | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2) (* FIXME *) + | (h1::t1, h2::t2) -> cmp h1 h2 && prefrec (t1,t2) | ([], _) -> true - | (_, _) -> false + | _ -> false in - prefrec (prefl,l) + prefrec (prefl,l) + +(** if [l=p++t] then [drop_prefix p l] is [t] else [l] *) -let drop_prefix p l = -(* if l=p++t then return t else l *) +let drop_prefix cmp p l = let rec drop_prefix_rec = function - | ([], tl) -> Some tl - | (_, []) -> None - | (h1::tp, h2::tl) -> - if h1 = h2 then drop_prefix_rec (tp,tl) else None (* FIXME *) + | (h1::tp, h2::tl) when cmp h1 h2 -> drop_prefix_rec (tp,tl) + | ([], tl) -> tl + | _ -> l in - match drop_prefix_rec (p,l) with - | Some r -> r - | None -> l + drop_prefix_rec (p,l) let map_append f l = List.flatten (List.map f l) diff --git a/lib/cList.mli b/lib/cList.mli index aec326c51..013e00173 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -185,11 +185,11 @@ sig val addn : int -> 'a -> 'a list -> 'a list (** [addn n x l] adds [n] times [x] on the left of [l]. *) - val prefix_of : 'a list -> 'a list -> bool + val prefix_of : 'a eq -> 'a list -> 'a list -> bool (** [prefix_of l1 l2] returns [true] if [l1] is a prefix of [l2], [false] otherwise. *) - val drop_prefix : 'a list -> 'a list -> 'a list + val drop_prefix : 'a eq -> 'a list -> 'a list -> 'a list (** [drop_prefix p l] returns [t] if [l=p++t] else return [l]. *) val drop_last : 'a list -> 'a list diff --git a/library/libnames.ml b/library/libnames.ml index d1bef531a..909a4dc3e 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -29,7 +29,8 @@ let pop_dirpath p = match DirPath.repr p with 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)) + List.prefix_of Id.equal + (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 @@ -37,7 +38,8 @@ let chop_dirpath n d = let drop_dirpath_prefix d1 d2 = let d = - List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) + List.drop_prefix Id.equal + (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in DirPath.make (List.rev d) |