CList.prefix_of and CList.drop_prefix with a parametric equality

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 15 insertions, 17 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index a6d157291c..e0ac9839fc 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 aec326c514..013e00173d 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