diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml index 771b861ac05f3044f24b08d8f7d1ee7228478da8..1e48cad2696860e219610e9ed5df536a8fdd9c78 100644 --- a/src/kernel_services/abstract_interp/lattice_bounds.ml +++ b/src/kernel_services/abstract_interp/lattice_bounds.ml @@ -126,6 +126,10 @@ module Bottom = struct (* Iterators *) + let bind f = function + | `Bottom -> `Bottom + | `Value v -> f v + let fold ~bottom f = function | `Bottom -> bottom | `Value v -> f v @@ -170,17 +174,11 @@ module Bottom = struct module Operators = struct - let (>>-) t f = match t with - | `Bottom -> `Bottom - | `Value t -> f t - - let (>>-:) t f = match t with - | `Bottom -> `Bottom - | `Value t -> `Value (f t) - - let (let+) = (>>-:) + let (>>-) x f = bind f x + let (>>-:) x f = map f x + let (let+) x f = map f x let (and+) = zip - let (let*) = (>>-) + let (let*) x f = bind f x let (and*) = zip end @@ -249,6 +247,20 @@ struct | `Top, v | v, `Top -> v | `Value vx, `Value vy -> `Value (narrow_value vx vy) + (* Iterators *) + + let bind f = function + | `Top -> `Top + | `Value v -> f v + + let fold ~top f = function + | `Top -> top + | `Value v -> f v + + let map f = function + | `Top -> `Top + | `Value v -> `Value (f v) + (** Combination *) let zip x y = @@ -264,18 +276,13 @@ struct (** Operators *) - module Operators = struct - let (>>-) t f = match t with - | `Top -> `Top - | `Value t -> f t - - let (>>-:) t f = match t with - | `Top -> `Top - | `Value t -> `Value (f t) - - let (let+) = (>>-:) + 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*) = (>>-) + let (let*) x f = bind f x let (and*) = zip end end @@ -299,6 +306,23 @@ 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 *) let zip x y = @@ -309,20 +333,13 @@ struct (** Operators *) - module Operators = struct - let (>>-) t f = match t with - | `Top -> `Top - | `Bottom -> `Bottom - | `Value t -> f t - - let (>>-:) t f = match t with - | `Top -> `Top - | `Bottom -> `Bottom - | `Value t -> `Value (f t) - - let (let+) = (>>-:) + 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*) = (>>-) + 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 827f7856fffd3758e7f20cbe376c7aa1b1d918c5..ead45a00fb69b5e5aa017b8608dfa5039d605eb1 100644 --- a/src/kernel_services/abstract_interp/lattice_bounds.mli +++ b/src/kernel_services/abstract_interp/lattice_bounds.mli @@ -82,7 +82,8 @@ module Bottom : sig (* Iterators *) val iter: ('a -> unit) -> 'a t -> unit - val fold: bottom: 'b -> ('a -> 'b) -> 'a t -> 'b + 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 *) @@ -144,6 +145,12 @@ module Top : sig 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 *) @@ -188,4 +195,10 @@ module TopBottom: sig (* 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 + + (* 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