From d39d55610e792bd4f6f1c2d452f4f1142b27c489 Mon Sep 17 00:00:00 2001 From: Sébastien Dailly Date: Fri, 14 Jul 2017 11:35:19 +0200 Subject: Added pure equality type in catalog --- catalog.ml | 18 ++++++++++-------- 1 file 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) ) ) -- cgit v1.2.3