diff --git a/src/kernel_services/abstract_interp/lattice_bounds.ml b/src/kernel_services/abstract_interp/lattice_bounds.ml index be5326b31fb2a7651e91aa4ef7bcbb139cc868ca..e432e4e8c164c6ca8ced6c2d86f26e7021e65e4a 100644 --- a/src/kernel_services/abstract_interp/lattice_bounds.ml +++ b/src/kernel_services/abstract_interp/lattice_bounds.ml @@ -39,6 +39,9 @@ end module Common = struct + + (* Pretty-printing *) + let pretty_top fmt = Format.pp_print_string fmt (Unicode.top_string ()) @@ -50,6 +53,8 @@ struct | `Top -> pretty_top fmt | `Value v -> pretty_value fmt v + (* Datatype *) + let hash hash_value = function | `Bottom -> 7 | `Top -> 13 @@ -70,6 +75,33 @@ struct | `Top, `Value _ -> -1 | `Value _, `Top -> 1 | `Value vx, `Value vy -> compare_value vx vy + + (* Tests *) + + let is_bottom = function + | `Bottom -> true + | `Value _ | `Top -> false + + let is_top = function + | `Top -> true + | `Value _ | `Bottom -> false + + let is_included is_included x y = + match x, y with + | `Bottom, _ | _, `Top -> true + | _, `Bottom | `Top, _ -> false + | `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 @@ -79,10 +111,6 @@ module Bottom = struct (** Access *) - let is_bottom = function - | `Bottom -> true - | `Value _ -> false - let non_bottom = function | `Value v -> v | `Bottom -> assert false @@ -93,11 +121,6 @@ module Bottom = struct (* Lattice operators *) - let is_included is_included x y = match x, y with - | `Bottom, _ -> true - | _, `Bottom -> false - | `Value vx, `Value vy -> is_included vx vy - let join join x y = match x, y with | `Value vx, `Value vy -> `Value (join vx vy) | `Bottom, (`Value _ as v) @@ -114,10 +137,6 @@ module Bottom = struct (* Iterators *) - let iter f = function - | `Bottom -> () - | `Value v -> f v - let fold ~bottom f = function | `Bottom -> bottom | `Value v -> f v @@ -135,10 +154,6 @@ module Bottom = struct (** Conversion *) - let to_option = function - | `Bottom -> None - | `Value v -> Some v - let of_option = function | None -> `Bottom | Some v -> `Value v @@ -227,10 +242,6 @@ struct (** Access *) - let is_top = function - | `Value _ -> false - | `Top -> true - let non_top = function | `Value v -> v | `Top -> assert false @@ -252,10 +263,6 @@ struct | None -> `Top | Some x -> `Value x - let to_option = function - | `Top -> None - | `Value x -> Some x - (** Operators *) module Operators = struct