aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xcatalog.ml49
1 files changed, 17 insertions, 32 deletions
diff --git a/catalog.ml b/catalog.ml
index e7bdb17..3d84af3 100755
--- a/catalog.ml
+++ b/catalog.ml
@@ -1,4 +1,3 @@
-module D = DataType
module T = Tools
module type DATA_SIG = sig
@@ -38,43 +37,30 @@ module Make(Data:DATA_SIG) = struct
(** Compare two signature *)
let eq: type a b. a sig_typ -> b sig_typ -> (a, b) T.cmp = begin fun a b ->
- match a, b with
- | T1(a), T1(b) ->
- begin match Data.compare_typ a b with
+ let cmp: type c d. c Data.typ -> d Data.typ -> ((c, d) T.cmp -> (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.Lt -> T.Lt
| T.Gt -> T.Gt
- | T.Eq -> T.Eq
- end
+ end in
+
+ match a, b with
+
+ | T1(a), T1(b) -> cmp a b (fun T.Eq -> T.Eq)
| T2(a, b), T2(c, d) ->
- begin match (Data.compare_typ a c) with
- | T.Lt -> T.Lt
- | T.Gt -> T.Gt
- | T.Eq ->
- begin match (Data.compare_typ b d) with
- | T.Lt -> T.Lt
- | T.Gt -> T.Gt
- | T.Eq -> T.Eq
- end
- end
+ cmp a c (fun T.Eq ->
+ cmp b d (fun T.Eq -> T.Eq)
+ )
| T3(a, b, c), T3(d, e, f) ->
- begin match (Data.compare_typ a d) with
- | T.Lt -> T.Lt
- | T.Gt -> T.Gt
- | T.Eq ->
- begin match (Data.compare_typ b e) with
- | T.Lt -> T.Lt
- | T.Gt -> T.Gt
- | T.Eq ->
- begin match (Data.compare_typ c f) with
- | T.Lt -> T.Lt
- | T.Gt -> T.Gt
- | T.Eq -> T.Eq
- end
- end
- end
+ cmp a d (fun T.Eq ->
+ cmp b e (fun T.Eq ->
+ cmp c f (fun T.Eq -> T.Eq)
+ )
+ )
+
| x, y -> if (T.Ex x) > (T.Ex y) then T.Gt else T.Lt
end
@@ -113,7 +99,6 @@ module Make(Data:DATA_SIG) = struct
Catalog.add name' map t
end
-
(** Look in the catalog for a function with the given name and signature *)
let find_function:
type a. t -> string -> a t_function sig_typ -> a t_function =