diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml
index c02dcd7ae8095bbcae9769b626d00f451ff70e3e..5fcb70859e1daaf17600794fab0dc7eb92d2f16c 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.ml
+++ b/src/kernel_services/abstract_interp/lattice_bounds.ml
@@ -20,14 +20,19 @@
(* *)
(**************************************************************************)
+
+
+(** Types definitions *)
+
type 'a or_bottom = [ `Value of 'a | `Bottom ]
type 'a or_top = [ `Value of 'a | `Top ]
type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
+
+
(** Common functions *)
-module Common =
-struct
+module Common = struct
(* Pretty-printing *)
@@ -82,19 +87,22 @@ struct
| `Value vx, `Value vy -> is_included vx vy
(* Iterator *)
+
let iter f = function
| `Bottom | `Top -> ()
| `Value v -> f v
(* Conversion *)
+
let to_option = function
| `Bottom | `Top -> None
| `Value x -> Some x
end
+
+
module Bottom = struct
- type 'a t = 'a or_bottom
include Common
@@ -110,41 +118,38 @@ module Bottom = struct
(* Lattice operators *)
- let join join x y = match x, y with
- | `Value vx, `Value vy -> `Value (join vx vy)
+ let join join x y =
+ match x, y with
+ | `Value vx, `Value vy -> `Value (join vx vy)
| `Bottom, (`Value _ as v)
| (`Value _ as v), `Bottom
| (`Bottom as v), `Bottom -> v
- let join_list j l = List.fold_left (join j) `Bottom l
-
- let narrow narrow x y = match x, y with
- | `Value vx, `Value vy -> narrow vx vy
+ let narrow narrow x y =
+ match x, y with
+ | `Value vx, `Value vy -> narrow vx vy
| `Bottom, `Value _
| `Value _, `Bottom
| `Bottom, `Bottom -> `Bottom
- (* Iterators *)
-
- let bind f = function
- | `Bottom -> `Bottom
- | `Value v -> f v
-
- let fold ~bottom f = function
- | `Bottom -> bottom
- | `Value v -> f v
-
- let map f = function
- | `Bottom -> `Bottom
- | `Value v -> `Value (f v)
+ let join_list f = List.fold_left (join f) `Bottom
(* Combination *)
let zip x y =
match x, y with
- | `Bottom, #t | #t, `Bottom -> `Bottom
+ | `Bottom, _ | _, `Bottom -> `Bottom
| `Value x, `Value y -> `Value (x,y)
+ (* Monadic operations *)
+
+ 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
+ let product l r = zip l r
+ end)
+
(** Conversion *)
let of_option = function
@@ -155,41 +160,19 @@ module Bottom = struct
| `Bottom -> []
| `Value v -> [v]
- let bot_of_list = function
- | [] -> `Bottom
- | l -> `Value l
-
- let list_of_bot = function
- | `Bottom -> []
- | `Value l -> l
-
- let add_to_list elt list = match elt with
+ let add_to_list elt list =
+ match elt with
| `Bottom -> list
| `Value elt -> elt :: list
let list_values l =
List.fold_left (fun l elt -> add_to_list elt l) [] l
- (** Operators *)
-
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
- end
-
(** Datatype construction *)
+
let counter = ref 0
- module Make_Datatype
- (Domain: Datatype.S)
- =
- Datatype.Make (
- struct
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
include Datatype.Serializable_undefined
type t = Domain.t or_bottom
let () = incr counter
@@ -207,21 +190,18 @@ module Bottom = struct
(* Bound lattice *)
- module Bound_Lattice
- (Lattice: Lattice_type.Join_Semi_Lattice)
- = struct
+ module Bound_Lattice (Lattice: Lattice_type.Join_Semi_Lattice) = struct
include Make_Datatype (Lattice)
-
let bottom = `Bottom
let join = join Lattice.join
let is_included = is_included Lattice.is_included
end
+
end
-module Top =
-struct
- type 'a t = 'a or_top
+
+module Top = struct
include Common
@@ -235,6 +215,12 @@ struct
| `Value v -> v
| `Top -> top
+ (** Conversion. *)
+
+ let of_option = function
+ | None -> `Top
+ | Some x -> `Value x
+
(** Lattice *)
let join join_value x y =
@@ -247,52 +233,88 @@ struct
| `Top, v | v, `Top -> v
| `Value vx, `Value vy -> `Value (narrow_value vx vy)
- (* Iterators *)
+ (** Combination *)
- let bind f = function
- | `Top -> `Top
- | `Value v -> f v
+ let zip x y =
+ match x, y with
+ | `Top, _ | _, `Top -> `Top
+ | `Value x, `Value y -> `Value (x,y)
- let fold ~top f = function
- | `Top -> top
- | `Value v -> f v
+ (** Monadic operators *)
- let map f = function
- | `Top -> `Top
- | `Value v -> `Value (f v)
+ 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
+ let product l r = zip l r
+ end)
+
+ (** Datatype construction *)
+
+ let counter = ref 0
+
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ type t = Domain.t or_top
+ let () = incr counter
+ let name = Domain.name ^ "+top(" ^ string_of_int !counter ^ ")"
+ let reprs = `Top :: (List.map (fun v -> `Value v) Domain.reprs)
+ let structural_descr = Structural_descr.t_unknown
+ let hash = Common.hash Domain.hash
+ let equal = (Common.equal Domain.equal :> t -> t -> bool)
+ let compare = Common.compare Domain.compare
+ let rehash = Datatype.identity
+ let copy = map Domain.copy
+ let pretty = Common.pretty Domain.pretty
+ let mem_project = Datatype.never_any_project
+ end)
+
+end
+
+
+
+module TopBottom = struct
+
+ type 'a t = 'a or_top_bottom
+ include Common
(** Combination *)
let zip x y =
match x, y with
+ | `Bottom, #t | #t, `Bottom -> `Bottom
| `Top, #t | #t, `Top -> `Top
| `Value x, `Value y -> `Value (x,y)
- (** Conversion. *)
+ (** Monadic operators. We have to redefines every operators to ensure
+ subtyping properties. *)
- let of_option = function
- | None -> `Top
- | Some x -> `Value x
+ let return x = `Value x
+ let product l r = zip l r
- (** Operators *)
+ let bind f = function
+ | `Bottom -> `Bottom
+ | `Top -> `Top
+ | `Value x -> f x
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
+ let map f = function
+ | `Bottom -> `Bottom
+ | `Top -> `Top
+ | `Value x -> `Value (f x)
+
+ let flatten = function
+ | `Bottom | `Value `Bottom -> `Bottom
+ | `Top | `Value `Top -> `Top
+ | `Value `Value x -> `Value x
+
+ module Operators = struct
+ let ( >>- ) (m : [< 'a t]) (f : 'a -> ([> 'b t] as 'c)) : 'c = bind f m
+ let ( let* ) (m : [< 'a t]) (f : 'a -> ([> 'b t] as 'c)) : 'c = bind f m
+ let ( and* ) (l : [< 'a t]) (r : [< 'b t]) : [> ('a * 'b) t] = product l r
+ let ( >>-: ) (m : [< 'a t]) (f : 'a -> 'b) : [> 'b t] = map f m
+ let ( let+ ) (m : [< 'a t]) (f : 'a -> 'b) : [> 'b t] = map f m
+ let ( and+ ) (l : [< 'a t]) (r : [< 'b t]) : [> ('a * 'b) t] = product l r
end
-end
-
-
-module TopBottom =
-struct
- type 'a t = 'a or_top_bottom
-
- include Common
(* Lattice operators *)
@@ -306,40 +328,24 @@ struct
| `Bottom, _ | _, `Bottom -> `Bottom
| `Value vx, `Value vy -> (narrow_value vx vy :> 'a t)
- (* Iterators *)
-
- let bind f = function
- | `Top -> `Top
- | `Bottom -> `Bottom
- | `Value v -> f v
-
- let fold ~top ~bottom f = function
- | `Top -> top
- | `Bottom -> bottom
- | `Value v -> f v
-
- let map f = function
- | `Top -> `Top
- | `Bottom -> `Bottom
- | `Value v -> `Value (f v)
-
- (** Combination *)
+ (** Datatype construction *)
- let zip x y =
- match x, y with
- | `Bottom, #t | #t, `Bottom -> `Bottom
- | `Top, #t | #t, `Top -> `Top
- | `Value x, `Value y -> `Value (x,y)
+ let counter = ref 0
- (** Operators *)
+ module Make_Datatype (Domain: Datatype.S) = Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ type t = Domain.t or_top_bottom
+ let () = incr counter
+ let name = Domain.name ^ "+top_bottom(" ^ string_of_int !counter ^ ")"
+ let reprs = `Bottom :: `Top :: (List.map (fun v -> `Value v) Domain.reprs)
+ let structural_descr = Structural_descr.t_unknown
+ let hash = Common.hash Domain.hash
+ let equal = (Common.equal Domain.equal :> t -> t -> bool)
+ let compare = Common.compare Domain.compare
+ let rehash = Datatype.identity
+ let copy = map Domain.copy
+ let pretty = Common.pretty Domain.pretty
+ let mem_project = Datatype.never_any_project
+ end)
- module Operators =
- struct
- let (>>-) x f = bind f x
- let (>>-:) x f = map f x
- let (let+) x f = map f x
- let (and+) = zip
- let (let*) x f = bind f x
- let (and*) = zip
- end
end
diff --git a/src/kernel_services/abstract_interp/lattice_bounds.mli b/src/kernel_services/abstract_interp/lattice_bounds.mli
index bfee4d2752dfc13bdeecce6e7c849fd13f9e5867..1e01e1139886b1c49599408106e491191891699b 100644
--- a/src/kernel_services/abstract_interp/lattice_bounds.mli
+++ b/src/kernel_services/abstract_interp/lattice_bounds.mli
@@ -29,163 +29,123 @@ type 'a or_top_bottom = [ `Value of 'a | `Bottom | `Top ]
module Bottom : sig
- type 'a t = 'a or_bottom
- (** Operators *)
- module Operators : sig
- (** This monad propagates `Bottom and or `Top if needed. *)
- val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
-
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
-
- (* Binding operators, applicative syntax *)
- val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
- val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
-
- (* Binding operators, monad syntax *)
- val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
- val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
- end
+ include Monad.S_with_product with type 'a t = 'a or_bottom
(** Datatype constructor *)
- module Make_Datatype
- (Domain: Datatype.S)
- : Datatype.S with type t = Domain.t or_bottom
+ module Make_Datatype (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_bottom
(** Bounds a semi-lattice *)
- module Bound_Lattice
- (Lattice: Lattice_type.Join_Semi_Lattice)
- : Lattice_type.Bounded_Join_Semi_Lattice with type t = Lattice.t or_bottom
+ module Bound_Lattice (Lattice: Lattice_type.Join_Semi_Lattice) :
+ Lattice_type.Bounded_Join_Semi_Lattice with type t = Lattice.t or_bottom
(** Access *)
- val is_bottom: 'a t -> bool
- val non_bottom: 'a t -> 'a
- val value: bottom: 'a -> 'a t -> 'a
+ val is_bottom : 'a t -> bool
+ val non_bottom : 'a t -> 'a
+ val value : bottom:'a -> 'a t -> 'a
(** Datatype *)
- val hash: ('a -> int) -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
- val pretty_bottom :Format.formatter -> unit (* for %t specifier *)
- val pretty :
- (Format.formatter -> 'a -> unit) ->
- Format.formatter -> 'a t -> unit
+ val pretty_bottom : Format.formatter -> unit (* for %t specifier *)
+ val pretty : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
(* Lattice operators *)
- val is_included: ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
- val join: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
- val join_list: ('a -> 'a -> 'a) -> 'a t list -> 'a t
- val narrow: ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val join_list : ('a -> 'a -> 'a) -> 'a t list -> 'a t
(* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: bottom:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
-
- (* Combination *)
- val zip: 'a t -> 'b t -> ('a * 'b) t (* `Bottom if any is `Bottom *)
+ val iter : ('a -> unit) -> 'a t -> unit
(** In a lattice where the elements are lists of non-bottom values,
the empty list is the bottom case. *)
(** Conversion *)
- val to_option: 'a t -> 'a option
- val of_option: 'a option -> 'a t
- val to_list: 'a t -> 'a list
- val bot_of_list: 'a list -> 'a list t
- val list_of_bot: 'a list t -> 'a list
- val list_values: 'a t list -> 'a list
+ val to_option : 'a t -> 'a option
+ val of_option : 'a option -> 'a t
+ val to_list : 'a t -> 'a list
+ val list_values : 'a t list -> 'a list
(** [elt >:: list] adds [elt] to the [list] if it is not bottom. *)
- val add_to_list: 'a t -> 'a list -> 'a list
+ val add_to_list : 'a t -> 'a list -> 'a list
+
end
module Top : sig
- type 'a t = 'a or_top
- (** Operators *)
- module Operators : sig
- (** This monad propagates `Bottom and or `Top if needed. *)
- val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ include Monad.S_with_product with type 'a t = 'a or_top
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
-
- (* Binding operators, applicative syntax *)
- val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
- val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
-
- (* Binding operators, monad syntax *)
- val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
- val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
- end
+ (** Datatype constructor *)
+ module Make_Datatype (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_top
(** Access *)
- val is_top: 'a t -> bool
- val non_top: 'a t -> 'a
- val value: top: 'a -> 'a t -> 'a
+ val is_top : 'a t -> bool
+ val non_top : 'a t -> 'a
+ val value : top:'a -> 'a t -> 'a
(** Datatype *)
- val hash: ('a -> int) -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
- val pretty_top :Format.formatter -> unit (* for %t specifier *)
+ val pretty_top : Format.formatter -> unit (* for %t specifier *)
val pretty :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit
(** Lattice operators *)
- val join: ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
- val narrow: ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
(* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: top:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
-
- (** Combination *)
- val zip: 'a t -> 'b t -> ('a * 'b) t (* `Top if any is `Top *)
+ val iter : ('a -> unit) -> 'a t -> unit
(** Conversion *)
val to_option : 'a t -> 'a option
val of_option : 'a option -> 'a t
+
end
module TopBottom: sig
- type 'a t = 'a or_top_bottom
- (** Operators *)
- (* In presence of simultaneous `Bottom and `Top in and+ / and*, everything
- narrows down to `Bottom *)
- module Operators : sig
- (** This monad propagates `Bottom and or `Top if needed. *)
- val (>>-) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
+ include Monad.S_with_product with type 'a t = 'a or_top_bottom
- (** Use this monad if the following function returns a simple value. *)
- val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
+ (** Datatype constructor *)
+ module Make_Datatype (Domain: Datatype.S) :
+ Datatype.S with type t = Domain.t or_top_bottom
+
+ (** Operators. In presence of simultaneous `Bottom and `Top in and+ / and*,
+ everything narrows down to `Bottom. Every operators is redefined to
+ ensure subtyping properties. *)
+ module Operators : sig
(* Binding operators, applicative syntax *)
+ val (>>-:) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
val (let+) : [< 'a t] -> ('a -> 'b) -> [> 'b t]
val (and+) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
(* Binding operators, monad syntax *)
+ val (>>- ) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
val (let*) : [< 'a t] -> ('a -> ([> 'b t] as 'c)) -> 'c
val (and*) : [< 'a t] -> [< 'b t] -> [> ('a * 'b) t]
+
end
(** Datatype *)
- val hash: ('a -> int) -> 'a t -> int
- val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
- val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
+ val hash : ('a -> int) -> 'a t -> int
+ val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+ val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Pretty-printing *)
val pretty :
@@ -193,12 +153,8 @@ module TopBottom: sig
Format.formatter -> 'a t -> unit
(* Lattice operators *)
- val join: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
- val narrow: ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
+ val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+ val join : ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
+ val narrow : ('a -> 'a -> [< 'a t]) -> 'a t -> 'a t -> 'a t
- (* Iterators *)
- val iter: ('a -> unit) -> 'a t -> unit
- val bind: ('a -> 'b t) -> 'a t -> 'b t
- val fold: top:'b -> bottom:'b -> ('a -> 'b) -> 'a t -> 'b
- val map: ('a -> 'b) -> 'a t -> 'b t
end
diff --git a/src/libraries/monads/composition.ml b/src/libraries/monads/composition.ml
new file mode 100644
index 0000000000000000000000000000000000000000..522d0b676f77b647cf2576c32b5355de198d2c3b
--- /dev/null
+++ b/src/libraries/monads/composition.ml
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module type Axiom = sig
+ type 'a interior and 'a exterior
+ val swap : 'a exterior interior -> 'a interior exterior
+end
+
+(* Using [Based_on_map] here, as the natural way to write the [bind] is through
+ [map] and [flatten]. *)
+module Make
+ (Int : Monad.S)
+ (Ext : Monad.S)
+ (X : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t)
+ = Monad.Make_based_on_map (struct
+ type 'a t = 'a Int.t Ext.t
+ let return x = Ext.return (Int.return x)
+ let map f m = Ext.map (Int.map f) m
+ let flatten m = Ext.map X.swap m |> Ext.flatten |> Ext.map Int.flatten
+ end)
+
+(* As for the previous functor and for the exact same reason, we use
+ [Based_on_map_with_product]. *)
+module Make_with_product
+ (Int : Monad.S_with_product) (Ext : Monad.S_with_product)
+ (X : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t)
+ = Monad.Make_based_on_map_with_product (struct
+ type 'a t = 'a Int.t Ext.t
+ let return x = Ext.return (Int.return x)
+ let map f m = Ext.map (Int.map f) m
+ let flatten m = Ext.map X.swap m |> Ext.flatten |> Ext.map Int.flatten
+ let product l r = Ext.product l r |> Ext.map (fun (l, r) -> Int.product l r)
+ end)
diff --git a/src/libraries/monads/composition.mli b/src/libraries/monads/composition.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e2f9aba8e6e9f7ad328fb303ec75796bccf19a1e
--- /dev/null
+++ b/src/libraries/monads/composition.mli
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** This module exposes two functors that, given a monad T called the
+ "interior monad" and a monad S called the "exterior monad", build
+ a monad of type ['a T.t S.t]. To be able to do so, one has to provide
+ a [swap] function that, simply put, swap the exterior monad out of
+ the interior one. In other word, this function allows fixing
+ "badly ordered" monads compositions, in the sens that they are
+ applied in the opposite order as the desired one.
+
+ For example, one may want to combine the State monad and the Option
+ monad to represent a stateful computation that may fail. To do so,
+ one can either rewrite all the needed monadic operations, which may
+ prove difficult, or use the provided functors of this module. Using
+ the Option monad as the interior and the State monad as the exterior,
+ one can trivially provide the following swap function:
+ {[
+ let swap (m : 'a State.t Option.t) : 'a Option.t State.t =
+ match m with
+ | None -> State.return None
+ | Some s -> State.map Option.return s
+ ]}
+ Note here that trying to reverse the order of the Option and State
+ monads makes the [swap] function way harder to write. Moreover, the
+ resulting function does not actually satisfy the required axioms.
+
+ Indeed, all [swap] functions will not result in a valid composed monad.
+ To produce such a monad, the given [swap] function must verify the
+ following equations:
+ 1. ∀t: 'a T.t, [swap (T.map S.return t) ≣ S.return t]
+ 2. ∀s: 'a S.t, [swap (T.return s) ≣ S.map T.return s]
+ 3. ∀x: 'a S.t S.t T.t, [swap (T.map S.flatten x) ≣ S.flatten (S.map swap (swap x))]
+ 4. ∀x: 'a S.t T.t T.t, [swap (T.flatten x) ≣ S.map T.flatten (swap (T.map swap x))]
+ More details on this at the end of this file.
+ @since Frama-C+dev *)
+
+module type Axiom = sig
+ type 'a interior and 'a exterior
+ val swap : 'a exterior interior -> 'a interior exterior
+end
+
+module Make
+ (Interior : Monad.S)
+ (Exterior : Monad.S)
+ (_ : Axiom with type 'a interior = 'a Interior.t
+ and type 'a exterior = 'a Exterior.t)
+ : Monad.S with type 'a t = 'a Interior.t Exterior.t
+
+module Make_with_product
+ (Interior : Monad.S_with_product)
+ (Exterior : Monad.S_with_product)
+ (_ : Axiom with type 'a interior = 'a Interior.t
+ and type 'a exterior = 'a Exterior.t)
+ : Monad.S_with_product with type 'a t = 'a Interior.t Exterior.t
+
+
+(** {3 Notes}
+
+ Monads composition is a notoriously difficult topic, and no general
+ approach exists. The one provided in this module is, in theory,
+ quite restrictive as the [swap] function, also called a distributive
+ law, has to satisfy the four presented axioms to guarantee that a
+ valid monad can be built. Roughly speaking, those axioms enforce the
+ idea that the distributive law must preserve all structures in the
+ two monads.
+
+ Distributive laws, their application to monads composition and weakenings
+ of their axioms are a broad topic with profound implications in category
+ theory. Even if none of this formal knowledge is required to use this
+ module, one can check the following references to satisfy their curiosity.
+
+ @see Jon Beck paper "Distributive laws" for more details on this topic.
+ @see Alexandre Goy thesis "On the compositionality of monads via weak
+ distributive laws" for details on how to relax some of those axioms. *)
diff --git a/src/libraries/monads/list.ml b/src/libraries/monads/list.ml
new file mode 100644
index 0000000000000000000000000000000000000000..414e994c6299aa7d5ab906eff9c3f8dc6f54c373
--- /dev/null
+++ b/src/libraries/monads/list.ml
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Stdlib.List
+
+module Minimal = struct
+ type 'a t = 'a list
+ let return x = [ x ]
+ let map f xs = map f xs
+ let flatten xs = flatten xs
+ let product ls rs = combine ls rs
+end
+
+include Monad.Make_based_on_map_with_product (Minimal)
diff --git a/src/libraries/monads/list.mli b/src/libraries/monads/list.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9403f94d5dd26c435e73bf7346b04e83ea6aa678
--- /dev/null
+++ b/src/libraries/monads/list.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Extend the [list] type to a full fleshed monad. This monad can be used
+ to represent non-deterministic computations.
+ @since Frama-C+dev *)
+
+include module type of Stdlib.List
+include Monad.S_with_product with type 'a t = 'a list
diff --git a/src/libraries/monads/monad.ml b/src/libraries/monads/monad.ml
new file mode 100644
index 0000000000000000000000000000000000000000..65bf2131e9ca1b48db331c6efd448039bbdf1f5f
--- /dev/null
+++ b/src/libraries/monads/monad.ml
@@ -0,0 +1,158 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+
+
+(* Complete signature *)
+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
+
+(* 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
+
+
+
+(* 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
+ let flatten m = bind (fun x -> x) m
+ let map f m = bind (fun x -> return (f x)) m
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( >>-: ) m f = map f m
+ let ( let+ ) m f = map f m
+ end
+end
+
+(* 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
+ let flatten m = M.flatten m
+ let bind f m = flatten (map f m)
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( >>-: ) m f = map f m
+ let ( let+ ) m f = map f m
+ end
+end
+
+(* 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
+ let flatten m = bind (fun x -> x) m
+ let map f m = bind (fun x -> return (f x)) m
+ let product l r = M.product l r
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( let+ ) m f = map f m
+ let ( >>-: ) m f = map f m
+ let ( and* ) l r = product l r
+ let ( and+ ) l r = product l r
+ end
+end
+
+(** 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
+ let flatten m = M.flatten m
+ let bind f m = flatten (map f m)
+ let product l r = M.product l r
+ module Operators = struct
+ let ( >>- ) m f = bind f m
+ let ( let* ) m f = bind f m
+ let ( let+ ) m f = map f m
+ let ( >>-: ) m f = map f m
+ let ( and* ) l r = product l r
+ let ( and+ ) l r = product l r
+ end
+end
diff --git a/src/libraries/monads/monad.mli b/src/libraries/monads/monad.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9d1ed937b9f5a809dff646b842fd81573a816268
--- /dev/null
+++ b/src/libraries/monads/monad.mli
@@ -0,0 +1,299 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** 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.
+ @since Frama-C+dev *)
+
+
+
+(** {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 provided 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 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
+ namespace conflicts. Indeed, one can use the expression
+ [let open MyMonad.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.
+ @since Frama-C+dev *)
+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 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 performed 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 the two let-bindings [and*] and [and+].
+ @since Frama-C+dev *)
+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}
+
+ Below are functors for creating monads (with or without product). Both
+ gives a strictly equivalent implementation but differ from the primitives
+ given as argument. For an example of monad implementation based on this
+ module, see {!Option}. *)
+
+
+(** {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 :
+
+ 1. [return] is a left-identity for [bind] :
+ ∀f:('a -> 'b t), ∀x:'a, [bind f (return x) ≣ return (f x)]
+
+ 2. [return] is a right-identity for [bind] :
+ ∀m:'a t, [bind return m ≣ m]
+
+ 3. [bind] is associative :
+ ∀m:'a t, ∀f:('a -> 'b t), ∀g:('b -> 'c t),
+ [bind (fun x -> bind g (f x)) m ≣ bind g (bind f m)]
+
+ 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 developers
+ have to manually check that they are respected.
+ @since Frama-C+dev *)
+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.
+ @since Frama-C+dev *)
+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
+
+
+(** {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,
+ and may be simpler to use for certain monads, such as the [list] one.
+
+ This approach requires three monadic operations. The first one, as in
+ the Kleisli triple approach, is a [return] function, allowing to plundge
+ values into the monad. The second one is a [map], that can be understand
+ as a parallel of the [map] on list, i.e a way to apply a function through
+ the monad. Finally, the third one is a [flatten] function, which allows
+ to handle nested applications of the monad.
+
+ As in the Kleisli triple approach, all those functions must satisfy some
+ laws to fully qualify as a monad :
+
+ 1. ∀x:'a, ∀f:('a -> 'b), [return (f x) ≣ map f (return x)]
+
+ 2. ∀m:('a t t t), [flatten (map flatten m) ≣ flatten (flatten m)]
+
+ 3. ∀m:('a t), [flatten (map return m) ≣ flatten (return m) ≣ m]
+
+ 4. ∀m:('a t t), ∀f: ('a -> 'b), [flatten (map (map f) m) ≣ map f (flatten m)]
+
+ 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 developers
+ have to manually check that they are respected.
+
+ More explanations on this approach on monads and its deep roots in the
+ category theory can be found at the end of this file.
+ @since Frama-C+dev *)
+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
+
+
+(** {3 Minimal signature based on map with product}
+
+ This signature simply extends the previous one with a product operator.
+ @since Frama-C+dev *)
+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
+
+
+(** {3 Functors extending minimal signatures}
+
+ Those functors provide a way to extend a minimal signature into a full
+ monad that satisfies the signatures defined above. This is possible
+ because one can define operations from one monadic definition
+ using the operations required by the others. Indeed :
+
+ 1. ∀m:('a t), ∀f:('a -> 'b), [map f m ≣ bind (fun x -> return (f x)) m]
+
+ 2. ∀m:('a t t), [flatten m ≣ bind identity m]
+
+ 3. ∀m:('a t), ∀f:('a -> 'b t), [bind f m ≣ flatten (map f m)]
+
+ All required laws expressed in both minimal signatures are respected
+ using those definitions. *)
+
+(** Extend a minimal monad based on bind.
+ @since Frama-C+dev *)
+module Make_based_on_bind (M : Based_on_bind) :
+ S with type 'a t = 'a M.t
+
+(** Extend a minimal monad based on map.
+ @since Frama-C+dev *)
+module Make_based_on_map (M : Based_on_map) :
+ S with type 'a t = 'a M.t
+
+(** Extend a minimal monad based on bind with product.
+ @since Frama-C+dev *)
+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 minimal monad based on map with product.
+ @since Frama-C+dev *)
+module Make_based_on_map_with_product (M : Based_on_map_with_product) :
+ S_with_product with type 'a t = 'a M.t
+
+
+
+(** {3 Detailled explanations and category theory}
+
+ To be pedantic, the map based approach defines a monad as a categoric
+ functor equipped with two natural transformations. This does sound
+ frightening but this breaks down to rather simple concepts.
+
+ Let's start at the beginning. A category is just a collection of objets
+ and arrows (or morphisms) between those objets that satisfies two
+ properties: there exists a morphism from all objects to themselves, i.e
+ an identity, and if there is a morphism between objects [a] and [b] and
+ a morphism between objects [b] and [c], then there must be a morphism
+ between [a] and [c], i.e morphisms are associative.
+
+ There is a strong parallel between categories and type systems. Indeed,
+ if one uses the collection of all types as objects, then for all types
+ ['a] and ['b], the function [f : 'a -> 'b] can be seen as a morphism
+ between the objets ['a] and ['b]. As functions are naturally associative
+ and, for any type ['a], one can trivially defines the identity function
+ ['a -> 'a], one can conclude that types along with all functions of
+ arity one forms a category.
+
+ Next, there is the idea of functors. In the category theory, a functor
+ is a mapping between categories. That means that, given two categories
+ [A] and [B], a functor maps all objects of [A] to an object of [B] and
+ maps any morphism of [A] into a morphism of [B]. But, not all mappings
+ are functors. Indeed, to be a valid functor, one has to preserve the
+ identity morphisms and the composition of morphims.
+
+ The idea of functors can also be seen in a type systems. At least, the
+ more restricted but enough here of an endofunctor, a functor from a
+ category to itself. Indeed, for any type [v] and for any parametric
+ type ['a t], the type [v t] can be seen as a mapping from values of
+ type [v] to values of type [v t]. Thus the type ['a t] encodes the first
+ part of what a functor is, a mapping from objects of the Type category
+ to objects of the Type category. For the second part, we need a way to
+ transform morphisms of the Type category, i.e functions of type ['a -> 'b],
+ in a way that preserves categoric properties. Expressed as a type, this
+ transformation can be seen as a higher-order function [map] with the
+ type [map : ('a -> 'b) -> ('a t -> 'b t)].
+
+ Finally, this definition of a monad requires two natural transformations.
+ Simply put, a natural transformation is a mapping between functors that
+ preserves the structures of all the underlying categories (mathematicians
+ and naming conventions...). That may be quite complicated to grasp, but in
+ this case, the two required transformations are quite simple and intuitive.
+
+ The first one is the [return] function that embeds values into the monad,
+ which can be seen as a natural transformation from the identity functor
+ to the monad functor. The second one is the [flatten] function, which
+ is a transformation from two applications of the monad functor to the
+ monad functor. With this two transformations, any number of application
+ of the monad functor can be taken down to a unique application of the
+ monad. *)
diff --git a/src/libraries/utils/option.ml b/src/libraries/monads/option.ml
similarity index 86%
rename from src/libraries/utils/option.ml
rename to src/libraries/monads/option.ml
index f6487051fd02f6ff6dd2e652bce92f302ec6238f..653bd86f92be7a7ddbdbc0d23112fa9851decfda 100644
--- a/src/libraries/utils/option.ml
+++ b/src/libraries/monads/option.ml
@@ -22,11 +22,12 @@
include Stdlib.Option
-let zip l r = match l, r with Some l, Some r -> Some (l, r) | _ -> None
-
-module Operators = struct
- let ( let* ) m f = bind m f
- let ( let+ ) m f = map f m
- let ( and* ) l r = zip l r
- let ( and+ ) l r = zip l r
+module Minimal = struct
+ type 'a t = 'a option
+ let return v = Some v
+ let bind f m = bind m f
+ let product l r = match l, r with Some l, Some r -> Some (l, r) | _ -> None
end
+
+include Monad.Make_based_on_bind_with_product (Minimal)
+let bind m f = bind f m
diff --git a/src/libraries/utils/option.mli b/src/libraries/monads/option.mli
similarity index 78%
rename from src/libraries/utils/option.mli
rename to src/libraries/monads/option.mli
index 5e13d5e8245e779fa2f60a9873e14f6d3f9fe71d..eabf184d63c32fc9a6e7d1e7e4d9526df33c8bda 100644
--- a/src/libraries/utils/option.mli
+++ b/src/libraries/monads/option.mli
@@ -20,16 +20,11 @@
(* *)
(**************************************************************************)
-(* Adding let binding operators to the Option module. See
- https://v2.ocaml.org/manual/bindingops.html for more information. *)
+(** Extend the [option] type to a full fleshed monad.
+ @since Frama-C+dev *)
include module type of Stdlib.Option
+include Monad.S_with_product with type 'a t = 'a option
-val zip : 'a option -> 'b option -> ('a * 'b) option
-
-module Operators : sig
- val ( let* ) : 'a option -> ('a -> 'b option) -> 'b option
- val ( let+ ) : 'a option -> ('a -> 'b) -> 'b option
- val ( and* ) : 'a option -> 'b option -> ('a * 'b) option
- val ( and+ ) : 'a option -> 'b option -> ('a * 'b) option
-end
+(** The bind is reversed for retrocompatibility reasons. *)
+val bind : 'a t -> ('a -> 'b t) -> 'b t
diff --git a/src/libraries/utils/result.ml b/src/libraries/monads/result.ml
similarity index 96%
rename from src/libraries/utils/result.ml
rename to src/libraries/monads/result.ml
index 993f64f752e309c6dbf9a82cbb0c6b5bd03ce4b7..ae4257392a5433de02df382f4240450069f28915 100644
--- a/src/libraries/utils/result.ml
+++ b/src/libraries/monads/result.ml
@@ -29,7 +29,9 @@ let zip l r =
| _, Error e -> Error e
module Operators = struct
+ let ( >>- ) r f = bind r f
let ( let* ) r f = bind r f
+ let ( >>-: ) r f = map f r
let ( let+ ) r f = map f r
let ( and* ) l r = zip l r
let ( and+ ) l r = zip l r
diff --git a/src/libraries/utils/result.mli b/src/libraries/monads/result.mli
similarity index 84%
rename from src/libraries/utils/result.mli
rename to src/libraries/monads/result.mli
index 51edb89cf62ae989d4651a247023d03a50fd8619..6afddc1e457471b73bcb72d873865fb8eb756355 100644
--- a/src/libraries/utils/result.mli
+++ b/src/libraries/monads/result.mli
@@ -20,9 +20,10 @@
(* *)
(**************************************************************************)
-(* Adding let binding operators to the Result module. See
- https://v2.ocaml.org/manual/bindingops.html for more information. *)
-
+(** Adding let binding operators to the Result module.
+ @see <https://v2.ocaml.org/manual/bindingops.html>
+ This module does not use the generic monad interface (cf. {!Monad}) because
+ of the error type, which would require another layer of functors. *)
include module type of Stdlib.Result
(** [zip r1 r2] regroups values in a pair [Ok (v1, v2)] if both arguments are
@@ -31,7 +32,9 @@ include module type of Stdlib.Result
val zip : ('a, 'e) result -> ('b, 'e) result -> ('a * 'b, 'e) result
module Operators : sig
+ val ( >>- ) : ('a, 'e) result -> ('a -> ('b, 'e) result) -> ('b, 'e) result
val ( let* ) : ('a, 'e) result -> ('a -> ('b, 'e) result) -> ('b, 'e) result
+ val ( >>-: ) : ('a, 'e) result -> ('a -> 'b) -> ('b, 'e) result
val ( let+ ) : ('a, 'e) result -> ('a -> 'b) -> ('b, 'e) result
val ( and* ) : ('a, 'e) result -> ('b, 'e) result -> ('a * 'b, 'e) result
val ( and+ ) : ('a, 'e) result -> ('b, 'e) result -> ('a * 'b, 'e) result
diff --git a/src/libraries/monads/state_monad.ml b/src/libraries/monads/state_monad.ml
new file mode 100644
index 0000000000000000000000000000000000000000..199b34d8bb2ad827bd2b1c38da6fd7c7737c3a43
--- /dev/null
+++ b/src/libraries/monads/state_monad.ml
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Make (Env : Datatype.S_with_collections) = struct
+
+ module Cache = Env.Hashtbl
+ type 'a cache = 'a Cache.t
+ type env = Env.t
+
+ module Minimal = struct
+
+ type 'a t = ('a * env) cache option * (env -> 'a * env)
+ let return (x : 'a) : 'a t = (None, fun env -> x, env)
+
+ let compute ((cache, make) : 'a t) (env : env) : 'a * env =
+ match cache with
+ | None -> make env
+ | Some cache when Cache.mem cache env -> Cache.find cache env
+ | Some cache -> let r = make env in Cache.add cache env r ; r
+
+ let bind (f : 'a -> 'b t) (m : 'a t) : 'b t =
+ let make env = let a, env = compute m env in compute (f a) env in
+ (Some (Cache.create 13), make)
+
+ end
+
+ 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
+
+end
diff --git a/src/libraries/monads/state_monad.mli b/src/libraries/monads/state_monad.mli
new file mode 100644
index 0000000000000000000000000000000000000000..60d728ff45e4bb94175a17580dc02b2b91646180
--- /dev/null
+++ b/src/libraries/monads/state_monad.mli
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** The State monad represents computations relying on a global mutable
+ state but implemented in a functionnal way.
+ @since Frama-C+dev *)
+
+module Make (Env : Datatype.S_with_collections) : sig
+ include Monad.S
+ type env = Env.t
+ val get_environment : env t
+ val set_environment : env -> unit t
+ val resolve : 'a t -> env -> 'a * env
+end
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 3cbd20fe5f0e556d02c8d09bca4ad6f10a458067..83aec8185f76a68874230e92c8cbdd19f9b9b49e 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -417,7 +417,7 @@ module Proxy(A : Analysis.Engine) : EvaProxy = struct
| Status truth -> Alarmset.Status.pretty fmt truth
let get_pointed_bases = function
- | Value v -> get_bases (Bottom.fold ~bottom:Cvalue.V.bottom get_cvalue v.v)
+ | Value v -> get_bases Bottom.(map get_cvalue v.v |> value ~bottom:Cvalue.V.bottom)
| Offsetmap offsm -> get_pointed_bases offsm
| Status _ -> Base.Hptset.empty
@@ -445,7 +445,7 @@ module Proxy(A : Analysis.Engine) : EvaProxy = struct
let pretty_eval = Bottom.pretty (pp_result typ) in
let value = Pretty_utils.to_string pretty_eval result in
let pointed_markers = get_pointed_markers eval_point in
- let pointed_vars = Bottom.fold ~bottom:[] pointed_markers result in
+ let pointed_vars = Bottom.(map pointed_markers result |> value ~bottom:[]) in
{ value; alarms; pointed_vars }
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
diff --git a/src/plugins/eva/contexts/context_product.ml b/src/plugins/eva/contexts/context_product.ml
index a6db310f46c7d3d9312ab3af56533fb508530bda..2ff2aeb9a1d71b01e53a43e893e0880e7fdc7e68 100644
--- a/src/plugins/eva/contexts/context_product.ml
+++ b/src/plugins/eva/contexts/context_product.ml
@@ -24,5 +24,5 @@ module Make (L : Abstract_context.S) (R : Abstract_context.S) = struct
type t = L.t * R.t
let top = (L.top, R.top)
let narrow (l, r) (l', r') =
- Lattice_bounds.Bottom.zip (L.narrow l l') (R.narrow r r')
+ Lattice_bounds.Bottom.product (L.narrow l l') (R.narrow r r')
end
diff --git a/src/plugins/eva/domains/multidim/segmentation.ml b/src/plugins/eva/domains/multidim/segmentation.ml
index bff6e16b6292ec970b956cacb1041704e333d1b3..26225f7a0730443604b05a0faf257b31c8b9f231 100644
--- a/src/plugins/eva/domains/multidim/segmentation.ml
+++ b/src/plugins/eva/domains/multidim/segmentation.ml
@@ -304,14 +304,14 @@ struct
let lower_bound ~oracle b1 b2 =
if b1 == b2 || eq b1 b2 then `Value b1 else
- let+ i1,i2 = Top.zip
+ let+ i1,i2 = Top.product
(lower_integer ~oracle:(oracle Left) b1)
(lower_integer ~oracle:(oracle Right) b2) in
Const (Integer.min i1 i2)
let upper_bound ~oracle b1 b2 =
if b1 == b2 || eq b1 b2 then `Value b1 else
- let+ i1,i2 = Top.zip
+ let+ i1,i2 = Top.product
(upper_integer ~oracle:(oracle Left) b1)
(upper_integer ~oracle:(oracle Right) b2) in
Const (Integer.max i1 i2)
@@ -510,7 +510,7 @@ struct
let hull ~oracle (m : t) : (bound * bound) or_top =
let l = m.start and u = last_bound m.segments in
- Top.zip (B.lower_const ~oracle l) (B.upper_const ~oracle u)
+ Top.product (B.lower_const ~oracle l) (B.upper_const ~oracle u)
let is_empty_segment ~oracle l u =
let open (val (B.operators oracle)) in
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index df124cd60bfa28d3db684dda973544f806d6e1b9..37469f52eb31c2b763583a1d8a7b796790b062c4 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1277,8 +1277,9 @@ module State = struct
let mk_variable_builder (eval : evaluator) (_: t) =
let (let*) x f = Option.bind (Top.to_option x) f in
(* Is the interval computed for a variable a singleton? *)
- let is_singleton =
- Top.fold ~top:false Cvalue.V.cardinal_zero_or_one
+ let is_singleton v =
+ Top.map Cvalue.V.cardinal_zero_or_one v
+ |> Top.value ~top:false
in
fun exp ->
match exp.node with
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index a852fd484d95515b460de07548be7f1f3350ab60..c661e6c5a7719e90919634cc3fff9cd9f94eef7c 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -1723,26 +1723,24 @@ module Make
match kfs with
| `Top -> top_function_pointer funcexp
| `Value kfs ->
+ let open Bottom.Operators in
let args_types = Option.map (List.map (fun e -> e.typ)) args in
- let kfs, alarm' =
- Eval_typ.compatible_functions funcexp.typ ?args:args_types kfs
- in
+ let compatible_funcs = Eval_typ.compatible_functions funcexp.typ in
+ let kfs, alarm' = compatible_funcs ?args:args_types kfs in
let reduce = backward_function_pointer valuation state v in
- let process acc kf =
- let res = reduce kf >>-: fun valuation -> kf, valuation in
- Bottom.add_to_list res acc
- in
- let list = List.fold_left process [] kfs in
- let status =
- if kfs = [] then Alarmset.False
- else if alarm || alarm' then Alarmset.Unknown
- else Alarmset.True
+ let reduce kf = let+ value = reduce kf in (kf, value) in
+ let process acc kf = Bottom.add_to_list (reduce kf) acc in
+ let res, status =
+ let res = `Value (List.fold_left process [] kfs) in
+ if kfs = [] then `Bottom, Alarmset.False
+ else if alarm || alarm' then res, Alarmset.Unknown
+ else res, Alarmset.True
in
let cil_v = Eva_ast.to_cil_exp v in
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
- Bottom.bot_of_list list, alarms
+ res, alarms
end
| _ -> assert false
end
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 2d673a4556c5ece200ac5fe3792012e419b58a2b..8d4445d59d31546df2895cf99edc074e8a6bd21a 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -735,7 +735,7 @@ module Make (Engine: Engine_sig.S) = struct
cacheable := NoCacheCallers;
states
in
- Bottom.list_of_bot states
+ Bottom.value ~bottom:[] states
in
(* Process each possible function apart, and append the result list. *)
let process acc (kf, valuation) =
@@ -743,7 +743,7 @@ module Make (Engine: Engine_sig.S) = struct
in
List.fold_left process [] functions
in
- Bottom.list_of_bot eval, !cacheable
+ Bottom.value ~bottom:[] eval, !cacheable
(* ------------------------------------------------------------------------ *)
(* Unspecified Sequence *)