aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/util.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-13 17:48:28 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-03-13 17:48:28 +0100
commit0dfd0fb7d7c04eedfb3b161b9b5cfab103c17916 (patch)
tree9517b8e5e12cc25e20dc436e5086bfd216739a7b /lib/util.ml
parent04b7394eaae170685a09ccd85ef47991466e6681 (diff)
Adding a few functions on type union.
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml33
1 files changed, 30 insertions, 3 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 0f79c10df..cae996e33 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -132,9 +132,36 @@ type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
-let map_union f g = function
- | Inl a -> Inl (f a)
- | Inr b -> Inr (g b)
+module Union =
+struct
+ let map f g = function
+ | Inl a -> Inl (f a)
+ | Inr b -> Inr (g b)
+
+ (** Lifting equality onto union types. *)
+ let equal f g x y = match x, y with
+ | Inl x, Inl y -> f x y
+ | Inr x, Inr y -> g x y
+ | _, _ -> false
+
+ let fold_left f g a = function
+ | Inl y -> f a y
+ | Inr y -> g a y
+ | _ -> a
+end
+
+let map_union = Union.map
+
+(** Lifting equality onto union types. *)
+let equal_union f g x y = match x, y with
+ | Inl x, Inl y -> f x y
+ | Inr x, Inr y -> g x y
+ | _, _ -> false
+
+let fold_left_union f g a = function
+ | Inl y -> f a y
+ | Inr y -> g a y
+ | _ -> a
type iexn = Exninfo.iexn