Merge pull request #16 from codex-semantics-library/dlesbre/equal-compare

Add equal/compare functions

Author: mlemerre

src/functors.ml

@@ -53,7 +53,6 @@ module MakeCustomHeterogeneousMap
     | Leaf{key;value} -> KeyValue(key,value)
     | Branch{tree1;_} -> unsigned_max_binding tree1
 
-
   (* Merge trees whose prefix disagree. *)
   let join pa treea pb treeb =
     (* Printf.printf "join %d %d\n" pa pb; *)
@@ -64,9 +63,6 @@ module MakeCustomHeterogeneousMap
     else
       branch ~prefix:p ~branching_bit:m ~tree0:treeb ~tree1:treea
 
-
-
-
   let singleton = leaf
 
   let rec cardinal m =
@@ -400,6 +396,47 @@ module MakeCustomHeterogeneousMap
         (* Any other case: there are elements in ta that are unmatched in tb. *)
       else false
 
+  type 'map polycompare =
+      { f : 'a. 'a key -> ('a, 'map) value -> ('a, 'map) value -> int; } [@@unboxed]
+
+  let compare_aux : type a b m. m polycompare -> a key -> (a,m) value -> b key -> (b,m) value -> int -> int =
+  fun f ka va kb vb default ->
+    let cmp = Int.compare (Key.to_int ka) (Key.to_int kb) in
+    if cmp <> 0 then cmp else
+    match Key.polyeq ka kb with
+      | Eq -> let cmp = f.f ka va vb in
+              if cmp <> 0 then cmp else default
+      | Diff -> default (* Should not happen since same Key.to_int values should imply equality *)
+
+  let rec reflexive_compare f ta tb = match (NODE.view ta),(NODE.view tb) with
+    | _ when ta == tb -> 0
+    | Empty, _ -> 1
+    | _, Empty -> -1
+    | Branch _, Leaf {key;value} ->
+        let KeyValue(k,v) = unsigned_min_binding ta in
+        compare_aux f k v key value 1
+    | Leaf {key;value}, Branch _ ->
+        let KeyValue(k,v) = unsigned_min_binding tb in
+        compare_aux f key value k v (-1)
+    | Leaf {key;value}, Leaf{key=keyb;value=valueb} ->
+        compare_aux f key value keyb valueb 0
+    | Branch{prefix=pa;branching_bit=ma;tree0=ta0;tree1=ta1},
+      Branch{prefix=pb;branching_bit=mb;tree0=tb0;tree1=tb1} ->
+      if ma == mb && pa == pb
+      (* Same prefix: divide the search. *)
+      then
+        let cmp = reflexive_compare f ta0 tb0 in
+        if cmp <> 0 then cmp else
+          reflexive_compare f ta1 tb1
+      else if branches_before pb mb pa ma (* ta has to be included in  tb0 or tb1. *)
+      then if (mb :> int) land (pa :> int) == 0
+        then let cmp = reflexive_compare f ta tb0 in if cmp <> 0 then cmp else -1
+        else -1 (* ta included in tb1, so there are elements of tb that appear before any elements of ta *)
+      else if branches_before pa ma pb mb (* tb has to be included in ta0 or ta1. *)
+        then if (mb :> int) land (pa :> int) == 0
+          then let cmp = reflexive_compare f ta0 tb in if cmp <> 0 then cmp else 1
+          else 1 (* tb included in ta1, so there are elements of ta that appear before any elements of tb *)
+      else Int.compare (pa :> int) (pb :> int)
 
   let rec disjoint ta tb =
     if ta == tb then is_empty ta
@@ -1098,6 +1135,8 @@ module MakeCustomHeterogeneousSet
   let of_seq s = add_seq s empty
   let of_list l = of_seq (List.to_seq l)
   let to_list s = List.of_seq (to_seq s)
+
+  let compare s1 s2 = BaseMap.reflexive_compare {f=fun _ () () -> 0} s1 s2
 end
 
 module MakeHeterogeneousMap(Key:HETEROGENEOUS_KEY)(Value:HETEROGENEOUS_VALUE) =
@@ -1225,6 +1264,9 @@ module MakeCustomMap
   let of_seq s = add_seq s empty
   let of_list l = of_seq (List.to_seq l)
   let to_list s = List.of_seq (to_seq s)
+
+  let reflexive_equal f m1 m2 = reflexive_same_domain_for_all2 (fun _ -> f) m1 m2
+  let reflexive_compare f m1 m2 = reflexive_compare {f=fun _ (Snd v1) (Snd v2) -> f v1 v2} m1 m2
 end
 
 

src/signatures.ml

@@ -424,6 +424,21 @@ module type BASE_MAP = sig
         val is_submap : 'a MyMap.t -> 'a MyMap.t -> bool = <fun>
       ]} *)
 
+  type 'map polycompare =
+      { f : 'a. 'a key -> ('a, 'map) value -> ('a, 'map) value -> int; } [@@unboxed]
+  val reflexive_compare : 'a polycompare -> 'a t -> 'a t -> int
+  (** [reflexive_compare f m1 m2] is an order relation on maps.
+      [m1] and [m2] are equal (return [0]) if they have the same domain and for all bindings
+      [(k,v)] in [m1], [(k,v')] in [m2], we have [f v v' = 0].
+
+      [m1] is considered striclty smaller than [m2] (return a negative integer)
+      when the first difference (lowest key in the {{!unsigned_lt}unsigned order} of {!KEY.to_int})
+      is either a shared binding [(k,v)] in [m1], [(k,v')] in [m2] with [f v v' < 0],
+      or a binding that only occurs in [m2].
+
+      Assumes that [f v v = 0].
+      @since 0.11.0 *)
+
   val disjoint : 'a t -> 'a t -> bool
   (** [disjoint m1 m2] is [true] iff [m1] and [m2] have disjoint domains *)
 
@@ -717,6 +732,14 @@ module type HETEROGENEOUS_SET = sig
   val equal : t -> t -> bool
   (** [equal a b] is [true] if [a] and [b] contain the same elements. *)
 
+  val compare : t -> t -> int
+  (** [compare s1 s2] is an order on setss.
+      [s1] and [s2] are equal if they contain the same bindings (compare by {!KEY.to_int}).
+      [s1] is strictly smaller than [s2] if the first difference (in the order of {!KEY.to_int})
+      is an element that appears in [s2] but not in [s1].
+
+      @since 0.11.0 *)
+
   val subset : t -> t -> bool
   (** [subset a b] is [true] if all elements of [a] are also in [b]. *)
 
@@ -895,6 +918,14 @@ module type SET = sig
   val equal : t -> t -> bool
   (** [equal a b] is [true] if [a] and [b] contain the same elements. *)
 
+  val compare : t -> t -> int
+  (** [compare s1 s2] is an order on setss.
+      [s1] and [s2] are equal if they contain the same bindings (compare by {!KEY.to_int}).
+      [s1] is strictly smaller than [s2] if the first difference (in the order of {!KEY.to_int})
+      is an element that appears in [s2] but not in [s1].
+
+      @since 0.11.0 *)
+
   val subset : t -> t -> bool
   (** [subset a b] is [true] if all elements of [a] are also in [b]. *)
 
@@ -1160,6 +1191,25 @@ module type MAP_WITH_VALUE = sig
       Delta is the number of different keys between [map1] and
       [map2]. *)
 
+  val reflexive_equal: ('a value -> 'a value -> bool) -> 'a t -> 'a t -> bool
+  (** [reflexive_equal f m1 m2] is true if both maps are equal, using [f] to compare values.
+      [f] is assumed to be reflexive (i.e. [f v v = true]).
+
+      @since 0.11.0 *)
+
+  val reflexive_compare: ('a value -> 'a value -> int) -> 'a t -> 'a t -> int
+  (** [reflexive_compare f m1 m2] is an order on both maps.
+      [m1] and [m2] are equal (return [0]) if they have the same domain and for all bindings
+      [(k,v)] in [m1], [(k,v')] in [m2], we have [f v v' = 0].
+
+      [m1] is considered striclty smaller than [m2] (return a negative integer)
+      when the first difference (lowest key in the {{!unsigned_lt}unsigned order} of {!KEY.to_int})
+      is either a shared binding [(k,v)] in [m1], [(k,v')] in [m2] with [f v v' < 0],
+      or a binding that only occurs in [m2].
+
+      Assumes that [f v v = 0].
+      @since 0.11.0 *)
+
   val disjoint : 'a t -> 'a t -> bool
   (** [disjoint a b] is [true] if and only if [a] and [b] have disjoint domains. *)