From c1a32f17a2cbe3a3fe5a16d87180bd8dbf706f46 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 24 Mar 2022 22:58:08 +0100
Subject: [PATCH] [Eva] add bindings operators for Bottom
---
src/kernel_services/abstract_interp/bottom.ml | 11 +++++++++--
src/kernel_services/abstract_interp/bottom.mli | 7 +++++++
2 files changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/abstract_interp/bottom.ml b/src/kernel_services/abstract_interp/bottom.ml
index b420661b852..58bc2ea996c 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 fad87be41a3..58242fa68b7 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
--
GitLab