Added pure equality type in catalog

1 files changed, 10 insertions, 8 deletions

diff --git a/catalog.ml b/catalog.ml
index 3d84af3..450966f 100755
--- a/catalog.ml
+++ b/catalog.ml
@@ -34,30 +34,32 @@ module Make(Data:DATA_SIG) = struct
 

     type 'a t = 'a sig_typ

 

+    (* Type for pure equality *)

+    type (_, _) eq = Eq : ('a, 'a) eq

 

     (** Compare two signature *)

     let eq: type a b. a sig_typ -> b sig_typ -> (a, b) T.cmp = begin fun a b ->

 

-      let cmp: type c d. c Data.typ -> d Data.typ -> ((c, d) T.cmp -> (a, b) T.cmp) -> (a, b) T.cmp =

+      let cmp: type c d. c Data.typ -> d Data.typ -> ((c, d) eq -> (a, b) T.cmp) -> (a, b) T.cmp =

         begin fun a b f -> match Data.compare_typ a b with

-        | T.Eq -> f T.Eq

+        | T.Eq -> f Eq

         | T.Lt -> T.Lt

         | T.Gt -> T.Gt

         end in

 

       match a, b with

 

-      | T1(a), T1(b) -> cmp a b (fun T.Eq -> T.Eq)

+      | T1(a), T1(b) -> cmp a b (fun Eq -> T.Eq)

 

       | T2(a, b), T2(c, d) ->

-        cmp a c (fun T.Eq ->

-          cmp b d (fun T.Eq -> T.Eq)

+        cmp a c (fun Eq ->

+          cmp b d (fun Eq -> T.Eq)

         )

 

       | T3(a, b, c), T3(d, e, f) ->

-        cmp a d (fun T.Eq ->

-          cmp b e (fun T.Eq ->

-            cmp c f (fun T.Eq -> T.Eq)

+        cmp a d (fun Eq ->

+          cmp b e (fun Eq ->

+            cmp c f (fun Eq -> T.Eq)

           )

         )