diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index 646ba8975ae5ac8eb5285c10c85f1b670ec7a63e..c1961ebbb4cb1abb613794dd18b45ed27808dece 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -143,7 +143,7 @@ module Bottom = struct
(* Monadic operations *)
- include Monad.Extend_Kleisli_with_product (struct
+ include Monad.Make_based_on_bind_with_product (struct
type 'a t = 'a or_bottom
let return x = `Value x
let bind f = function `Bottom -> `Bottom | `Value x -> f x
@@ -242,7 +242,7 @@ module Top = struct
(** Monadic operators *)
- include Monad.Extend_Kleisli_with_product (struct
+ include Monad.Make_based_on_bind_with_product(struct
type 'a t = 'a or_top
let return x = `Value x
let bind f = function `Top -> `Top | `Value x -> f x
diff --git a/src/libraries/monads/list.ml b/src/libraries/monads/list.ml
index 252a97bdaec00ddb1dc78cb1a5a3ec81eb019d4e..414e994c6299aa7d5ab906eff9c3f8dc6f54c373 100644
--- a/src/libraries/monads/list.ml
+++ b/src/libraries/monads/list.ml
@@ -30,4 +30,4 @@ module Minimal = struct
let product ls rs = combine ls rs
end
-include Monad.Extend_Categoric_with_product (Minimal)
+include Monad.Make_based_on_map_with_product (Minimal)
diff --git a/src/libraries/monads/monad.ml b/src/libraries/monads/monad.ml
index 61099357703f0429a7066e09247dbaf5ca82f980..65bf2131e9ca1b48db331c6efd448039bbdf1f5f 100644
--- a/src/libraries/monads/monad.ml
+++ b/src/libraries/monads/monad.ml
@@ -22,38 +22,77 @@
-(* Kleisli triple minimal signature *)
-module type Kleisli = sig
- type 'a t
- val return : 'a -> 'a t
- val bind : ('a -> 'b t) -> 'a t -> 'b t
-end
-
-(* Categoric minimal signature *)
-module type Categoric = sig
+(* Complete signature *)
+module type S = sig
type 'a t
val return : 'a -> 'a t
- val map : ('a -> 'b) -> 'a t -> 'b t
val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ end
end
-(* Complete signature *)
-module type S = sig
+(* Complete signature with a product *)
+module type S_with_product = sig
type 'a t
val return : 'a -> 'a t
val flatten : 'a t t -> 'a t
val map : ('a -> 'b ) -> 'a t -> 'b t
val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
module Operators : sig
val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
end
end
-(** Extend a Kleisli triple monad *)
-module Extend_Kleisli (M : Kleisli) = struct
+
+
+(* Minimal signature based on bind *)
+module type Based_on_bind = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+end
+
+(* Minimal signature based on bind with product *)
+module type Based_on_bind_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+end
+
+(* Minimal definition based on map *)
+module type Based_on_map = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val map : ('a -> 'b) -> 'a t -> 'b t
+ val flatten : 'a t t -> 'a t
+end
+
+(* Minimal signature based on map with product *)
+module type Based_on_map_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val map : ('a -> 'b) -> 'a t -> 'b t
+ val flatten : 'a t t -> 'a t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+end
+
+
+
+(* Extend a based on bind minimal monad *)
+module Make_based_on_bind (M : Based_on_bind) = struct
type 'a t = 'a M.t
let return x = M.return x
let bind f m = M.bind f m
@@ -67,8 +106,8 @@ module Extend_Kleisli (M : Kleisli) = struct
end
end
-(** Extend a categoric monad *)
-module Extend_Categoric (M : Categoric) = struct
+(* Extend a based on map minimal monad *)
+module Make_based_on_map (M : Based_on_map) = struct
type 'a t = 'a M.t
let return x = M.return x
let map f m = M.map f m
@@ -82,46 +121,8 @@ module Extend_Categoric (M : Categoric) = struct
end
end
-
-
-(* Product on monads *)
-module type Product = sig
- type 'a t
- val product : 'a t -> 'b t -> ('a * 'b) t
-end
-
-(* Kleisli triple with a product *)
-module type Kleisli_with_product = sig
- include Kleisli
- include Product with type 'a t := 'a t
-end
-
-(* Categoric monad with a product *)
-module type Categoric_with_product = sig
- include Categoric
- include Product with type 'a t := 'a t
-end
-
-(* Complete signature with a product *)
-module type S_with_product = sig
- type 'a t
- val return : 'a -> 'a t
- val flatten : 'a t t -> 'a t
- val map : ('a -> 'b ) -> 'a t -> 'b t
- val bind : ('a -> 'b t) -> 'a t -> 'b t
- val product : 'a t -> 'b t -> ('a * 'b) t
- module Operators : sig
- val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
- val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
- val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
- val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
- end
-end
-
-(** Extend a Kleisli triple monad with a product *)
-module Extend_Kleisli_with_product (M : Kleisli_with_product) = struct
+(* Extend a based on bind monad with a product *)
+module Make_based_on_bind_with_product (M : Based_on_bind_with_product) = struct
type 'a t = 'a M.t
let return x = M.return x
let bind f m = M.bind f m
@@ -138,8 +139,8 @@ module Extend_Kleisli_with_product (M : Kleisli_with_product) = struct
end
end
-(** Extend a categoric monad with a product *)
-module Extend_Categoric_with_product (M : Categoric_with_product) = struct
+(** Extend a based on map monad with a product *)
+module Make_based_on_map_with_product (M : Based_on_map_with_product) = struct
type 'a t = 'a M.t
let return x = M.return x
let map f m = M.map f m
diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
index 7fd24d094808ac8ee7b156b312f3e287728c4faa..a9cb659688cfa777a0c89dc32006018d98988e15 100644
--- a/src/libraries/monads/monad.mli
+++ b/src/libraries/monads/monad.mli
@@ -20,18 +20,113 @@
(* *)
(**************************************************************************)
-(** This module provides a generic monad interface based on Keisli and
- Categoric definitions of monads. *)
+(** This module provides generic signatures for monads along with tools
+ to build them based on minimal definitions. Those tools are provided
+ for advanced users that would like to define their own monads. Any
+ user that only wants to use the monads provided by the kernel can
+ completly ignore them. *)
+
+
+
+(** {2 Monad signature with let-bindings}
+
+ This signature provides all the usual monadic operators along with
+ let-bindings definitions used to simplify codes relying on monads.
+ The provides operators are as follows:
+ - [return] embeds a value [x] in the monad.
+ - [bind] encodes the idea of "sequence" in the monadic world, i.e the
+ call [bind f m] comes down to performing the computation [m] before
+ applying the next computation step, represented by the function [f],
+ to the resulting value.
+ - [map] applies a function through the monad. One can examplify it by
+ making a parallel with the list [map] operator.
+ - [flatten] is used to handle nested applications of the monad.
+
+ The provided let-bindings operators can be used to write simpler and
+ cleaner code. For example, one can write [let+ v = compute x in v + 1]
+ instead of [map (fun v -> v + 1) (compute x)]. The more monadic steps,
+ the more simpler the code will get when written using those operators.
+ In this module, [>>-] and [let*] always correspond to the [bind]
+ operator while [>>-:] and [let+] always correspond to the [map].
+ All those operators are provided in an [Operators] module to avoid
+ spacename conflicts. Indeed, one can use the expression
+ [let open Monad.Operators in] to use all the let-bindings without
+ risking conflicts by including the other definitions, which have
+ rather common names. This idiom also helps indicate which monad is
+ currently used in a code. *)
+module type S = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ end
+end
-(** {2 Kleisli triple signature for a monadic type constructor ['a t]}
- This is the usual minimal definition of a monadic type constructor.
- The [return] function embeds a value {m x} in the monad. The [bind]
- function, also called the "combinator", corresponds to the idea of
- "sequence" in the monadic world, i.e the call [bind f m] comes down
- to performing the computation [m] before applying the next computation
- step, represented by the function [f], to the resulting value.
+(** {2 Monad signature with product}
+
+ In a computational point of view, a monad is an abstraction of a sequence
+ of operations. But sometimes, one may need to specify that two operations
+ can be perform in *any* order, for instance when dealing with concurrency
+ or generic errors handling using the [option] type. To do so, one needs
+ a *product* on monadic values, i.e a way to combine two monads into a new
+ one. Thus a second signature is provided, including a product operator
+ and two the let-bindings [and*] and [and+]. *)
+module type S_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val flatten : 'a t t -> 'a t
+ val map : ('a -> 'b ) -> 'a t -> 'b t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+ module Operators : sig
+ val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+ val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
+ val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+ val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
+ end
+end
+
+
+
+(** {2 Building monads from minimal signatures}
+
+ From now on, all provided definitions are designed for advanced users
+ that would like to build their own monads. Each monad can be build
+ by directly implementing all required operators in the previous
+ signatures. However, this is a tedious and error prone work, in
+ particular for the let-binging operators which are just syntactic
+ sugars for other operators.
+
+ To simplify this, two minimal definitions and the corresponding
+ functors are provided to alleviate this as much as possible. Both
+ definitions lead to strictly equivalent monads, as all operators of
+ one definition can be build from the other. Therefore, one can use
+ the simplest one to implement for their monad.
+
+ In depth explanations on those minimal definitions and the properties
+ they should respect are given. A huge effort has been made to make
+ those explanations as simple as possible even if deep down, monads
+ take roots in the category theory, a notoriously difficult topic. *)
+
+
+(** {3 Minimal signature based on bind}
+
+ This is the usual minimal definition of a monadic type constructor, also
+ called a Kleisli triple. The [return] function embeds a value {m x} in
+ the monad. The [bind] function, also called the "combinator", corresponds
+ to the idea of "sequence" in the monadic world, i.e the call [bind f m]
+ comes down to performing the computation [m] before applying the next
+ computation step, represented by the function [f], to the resulting value.
To fully qualify as a monad, these three parts must respect the three
following laws :
@@ -49,15 +144,25 @@
As there is no way in the OCaml type system to enforce those properties,
users have to trust the implemented monad when using it, and developpers
have to manually check that they are respected. *)
-module type Kleisli = sig
+module type Based_on_bind = sig
type 'a t
val return : 'a -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t
end
+(** {3 Minimal signature based on bind with product}
+
+ This signature simply extends the previous one with a product operator. *)
+module type Based_on_bind_with_product = sig
+ type 'a t
+ val return : 'a -> 'a t
+ val bind : ('a -> 'b t) -> 'a t -> 'b t
+ val product : 'a t -> 'b t -> ('a * 'b) t
+end
-(** {2 Categoric signature for a monadic type constructor ['a t]}
+
+(** {3 Minimal definition based on map}
In a computer science context, this is a rarer definition of a monadic
type constructor. It is however equivalent to the Kleisli triple one,
@@ -125,7 +230,7 @@ end
As there is no way in the OCaml type system to enforce those properties,
users have to trust the implemented monad when using it, and developpers
have to manually check that they are respected. *)
-module type Categoric = sig
+module type Based_on_map = sig
type 'a t
val return : 'a -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
@@ -133,35 +238,22 @@ module type Categoric = sig
end
+(** {3 Minimal signature based on map with product}
-(** {2 Extended signature with let-bindings}
-
- The minimal definitions of a monad are not that useful when one tries to
- develop clean monadic code. To help alleviate this, one should instead
- uses monads respecting this extended signature, that combines both the
- Kleisli triple and categoric definitions and provides two let-binding
- operators. The operator [let*] corresponds to the [bind] function
- while the operator [let+] corresponds to the [map]. *)
-module type S = sig
+ This signature simply extends the previous one with a product operator. *)
+module type Based_on_map_with_product = sig
type 'a t
val return : 'a -> 'a t
+ val map : ('a -> 'b) -> 'a t -> 'b t
val flatten : 'a t t -> 'a t
- val map : ('a -> 'b ) -> 'a t -> 'b t
- val bind : ('a -> 'b t) -> 'a t -> 'b t
- module Operators : sig
- val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
- val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
- end
+ val product : 'a t -> 'b t -> ('a * 'b) t
end
-
-(** {2 Extend minimal signature}
+(** {3 Functors extending minimal signatures}
Those functors provide a way to extend a minimal signature into a full
- monad that satisfies the signature defined above. This is possible
+ monad that satisfies the signatures defined above. This is possible
because one can defines operations from one monadic definition
using the operations required by the others. Indeed :
@@ -174,97 +266,18 @@ end
All required laws expressed in both minimal signatures are respected
using those definitions. *)
-(** Extend a Kleisli triple monad *)
-module Extend_Kleisli (M : Kleisli) : S with type 'a t = 'a M.t
-
-(** Extend a categoric monad *)
-module Extend_Categoric (M : Categoric) : S with type 'a t = 'a M.t
-
-
-
-(** {2 Product on monads}
-
- In a computational point of view, a monad is an abstraction of a sequence
- of operations. But sometimes, one may need to specify that two operations
- can be perform in *any* order, for instance when dealing with concurrency
- or generic errors handling using the [option] type. To do so, one needs
- to specify a *product* on monadic values, i.e a way to combine two monads
- into a new one. The concept of a product has also deep roots in category
- theory, but there is no need to dive into this for the purpose of this
- module. *)
-module type Product = sig
- type 'a t
- val product : 'a t -> 'b t -> ('a * 'b) t
-end
-
-
-
-(** {3 Product on Kleisli triple monads}
-
- When combined with a Kleisli triple monad, the product should respect
- the following property if one wants it to truly encode that computations
- can be performed in *any* order :
-
- 1. ∀l:('a t), ∀r:('b t), ∀f:(('a * 'b) -> 'c t),
- [bind f (product l r) ≣ bind (fun (b, a) -> f (a, b)) (product r l)]
-
- However, in some cases, this property is not feasible. In those cases, it
- should be explicitly stated. *)
-module type Kleisli_with_product = sig
- include Kleisli
- include Product with type 'a t := 'a t
-end
-
-
-
-(** {3 Product on Categoric monads}
-
- When combined with a Categoric monad, the product should respect the
- following property if one wants it to truly encode that computations
- can be performed in *any* order :
-
- 1. ∀l:('a t), ∀r:('b t), ∀f:(('a * 'b) -> 'c),
- [map f (product l r) ≣ map (fun (b, a) -> f (a, b)) (product r l)]
-
- However, in some cases, this property is not feasible. In those cases, it
- should be explicitly stated.*)
-module type Categoric_with_product = sig
- include Categoric
- include Product with type 'a t := 'a t
-end
-
-
-
-(** {3 Extended monads with product}
-
- Extended monads that provides a product also provides two and-binding
- operators implementing it, the [and*] and [and+] operators.
+(** Extend a minimal monad based on bind *)
+module Make_based_on_bind (M : Based_on_bind) :
+ S with type 'a t = 'a M.t
- Take note that a generic implementation of the product can be given
- as [bind (fun a -> map (fun b -> (a, b)) r) l]. However, this
- definition may not be symmetric, which is why one is required to
- provide a custom product. *)
-module type S_with_product = sig
- type 'a t
- val return : 'a -> 'a t
- val flatten : 'a t t -> 'a t
- val map : ('a -> 'b ) -> 'a t -> 'b t
- val bind : ('a -> 'b t) -> 'a t -> 'b t
- val product : 'a t -> 'b t -> ('a * 'b) t
- module Operators : sig
- val ( >>- ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
- val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
- val ( >>-: ) : 'a t -> ('a -> 'b) -> 'b t
- val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
- val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
- end
-end
+(** Extend a minimal monad based on map *)
+module Make_based_on_map (M : Based_on_map) :
+ S with type 'a t = 'a M.t
-(** Extend a Kleisli triple monad with product *)
-module Extend_Kleisli_with_product (M : Kleisli_with_product) :
+(** Extend a minimal monad based on bind with product *)
+module Make_based_on_bind_with_product (M : Based_on_bind_with_product) :
S_with_product with type 'a t = 'a M.t
-(** Extend a categoric monad *)
-module Extend_Categoric_with_product (M : Categoric_with_product) :
+(** Extend a minimal monad based on map with product *)
+module Make_based_on_map_with_product (M : Based_on_map_with_product) :
S_with_product with type 'a t = 'a M.t
diff --git a/src/libraries/monads/option.ml b/src/libraries/monads/option.ml
index beb92fc126b85fca0c40e97dbcce914714e933d7..e29639209fb61724824fea3024308aea02de9ee1 100644
--- a/src/libraries/monads/option.ml
+++ b/src/libraries/monads/option.ml
@@ -29,5 +29,5 @@ module Minimal = struct
let product l r = match l, r with Some l, Some r -> Some (l, r) | _ -> None
end
-include Monad.Extend_Kleisli_with_product (Minimal)
+include Monad.Make_based_on_bind_with_product (Minimal)
let bind m f = bind f m
diff --git a/src/libraries/monads/state_monad.ml b/src/libraries/monads/state_monad.ml
index 30dc807702abdbda9c16aace18982953b082406c..199b34d8bb2ad827bd2b1c38da6fd7c7737c3a43 100644
--- a/src/libraries/monads/state_monad.ml
+++ b/src/libraries/monads/state_monad.ml
@@ -43,7 +43,7 @@ module Make (Env : Datatype.S_with_collections) = struct
end
- include Monad.Extend_Kleisli (Minimal)
+ include Monad.Make_based_on_bind (Minimal)
let get_environment : env t = None, fun env -> env, env
let set_environment (env : env) : unit t = None, fun _ -> (), env
let resolve (m : 'a t) (env : env) : 'a * env = Minimal.compute m env
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index e8cb4065e2695d6d67bac40ef3a7571232a9e486..30fccb773db74e278fe05193e17569d7a709caaa 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -1729,7 +1729,8 @@ module Make
let kfs, alarm' = compatible_funcs ?args:args_types kfs in
let reduce = backward_function_pointer valuation state v in
let process acc kf = let+ acc and+ v = reduce kf in (kf, v) :: acc in
- let valuations = List.fold_left process (`Value []) kfs in
+ let bottom_if_empty = function `Value [] -> `Bottom | res -> res in
+ let res = List.fold_left process (`Value []) kfs |> bottom_if_empty in
let status =
if kfs = [] then Alarmset.False
else if alarm || alarm' then Alarmset.Unknown
@@ -1739,7 +1740,7 @@ module Make
let cil_args = Option.map (List.map Eva_ast.to_cil_exp) args in
let alarm = Alarms.Function_pointer (cil_v, cil_args) in
let alarms = Alarmset.singleton ~status alarm in
- valuations, alarms
+ res, alarms
end
| _ -> assert false
end