diff --git a/src/kernel_services/abstract_interp/bottom.ml b/src/kernel_services/abstract_interp/bottom.ml index b420661b852603263dd60a303203bd1f345ceab3..58bc2ea996c531c97f4bc378a1ae64046c67014f 100644 --- a/src/kernel_services/abstract_interp/bottom.ml +++ b/src/kernel_services/abstract_interp/bottom.ml @@ -25,16 +25,23 @@ module Type = struct type 'a or_bottom = [ `Value of 'a | `Bottom ] - (* This monad propagates the `Bottom value if needed. *) let (>>-) t f = match t with | `Bottom -> `Bottom | `Value t -> f t - (* Use this monad if the following function returns a simple value. *) let (>>-:) t f = match t with | `Bottom -> `Bottom | `Value t -> `Value (f t) + let zip x y = + match x, y with + | `Bottom, _ | _, `Bottom -> `Bottom + | `Value x, `Value y -> `Value (x,y) + + let (let+) = (>>-:) + let (and+) = zip + let (let*) = (>>-) + let (and*) = zip end include Type diff --git a/src/kernel_services/abstract_interp/bottom.mli b/src/kernel_services/abstract_interp/bottom.mli index fad87be41a342bee62ce8fe041c9ba0e4aa7c0ca..58242fa68b73479d5f13b2c7cc4048f14faaa98d 100644 --- a/src/kernel_services/abstract_interp/bottom.mli +++ b/src/kernel_services/abstract_interp/bottom.mli @@ -33,6 +33,13 @@ module Type : sig (** Use this monad if the following function returns a simple value. *) val (>>-:) : 'a or_bottom -> ('a -> 'b) -> 'b or_bottom + (* Binding operators, applicative syntax *) + val (let+) : 'a or_bottom -> ('a -> 'b) -> 'b or_bottom + val (and+) : 'a or_bottom -> 'b or_bottom -> ('a * 'b) or_bottom + + (* Binding operators, monad syntax *) + val (let*) : 'a or_bottom -> ('a -> 'b or_bottom) -> 'b or_bottom + val (and*) : 'a or_bottom -> 'b or_bottom -> ('a * 'b) or_bottom end include module type of Type