[Eva] Removes unused module [Bool] from Abstract_interp.

src/kernel_services/abstract_interp/abstract_interp.ml

@@ -306,101 +306,6 @@ module Rel = struct
   let sub_abs = sub
 end
 
-
-module Bool = struct
-  type t = Top | True | False | Bottom
-  let hash (b : t) = Hashtbl.hash b
-  let equal (b1 : t) (b2 : t) = b1 = b2
-  let compare (b1 : t) (b2 : t) = Stdlib.compare b1 b2
-  let pretty fmt = function
-    | Top -> Format.fprintf fmt "Top"
-    | True -> Format.fprintf fmt "True"
-    | False -> Format.fprintf fmt "False"
-    | Bottom -> Format.fprintf fmt "Bottom"
-  let is_included t1 t2 = match t1, t2 with
-    | Bottom, _
-    | _, Top
-    | True, True
-    | False, False -> true
-    | _ -> false
-  let bottom = Bottom
-  let top = Top
-  let join b1 b2 = match b1, b2 with
-    | Top, _
-    | _, Top
-    | True, False -> Top
-    | True, _
-    | _, True -> True
-    | False, _
-    | _, False -> False
-    | Bottom, Bottom -> Bottom
-  let narrow b1 b2 = match b1, b2 with
-    | Bottom, _
-    | _, Bottom
-    | True, False -> Bottom
-    | True, _
-    | _, True -> True
-    | False, _
-    | _, False -> False
-    | Top, Top -> Top
-  let link = join
-  let meet = narrow
-  type widen_hint = unit
-  let widen () = join
-  let cardinal_zero_or_one b = not (equal b top)
-  let intersects b1 b2 = match b1, b2 with
-    | Bottom, _ | _, Bottom -> false
-    | _, Top | Top, _ -> true
-    | False, False | True, True -> true
-    | False, True | True, False -> false
-  let diff b1 b2 = match b1, b2 with
-    | b1, Bottom -> b1
-    | _, Top -> Bottom
-    | Bottom, _ -> Bottom
-    | Top, True -> False
-    | Top, False -> True
-    | True, True -> Bottom
-    | True, False -> True
-    | False, True -> False
-    | False, False -> Bottom
-  let diff_if_one b1 b2 = match b1, b2 with
-    | b1, Top -> b1
-    | _, _ -> diff b1 b2
-  let fold_enum f b init =
-    let elements = match b with
-      | Top -> [True; False]
-      | True -> [True]
-      | False -> [False]
-      | Bottom -> []
-    in
-    List.fold_right (fun b acc -> f b acc) elements init
-  let cardinal = function
-    | Top -> 2
-    | True | False -> 1
-    | Bottom -> 0
-  let cardinal_less_than b i =
-    let c = cardinal b in
-    if c > i then raise Not_less_than
-    else c
-
-  type blt = t
-  include (Datatype.Make_with_collections
-             (struct
-               type t = blt
-               let name = "Bool_lattice"
-               let structural_descr = Structural_descr.t_abstract
-               let reprs = [Top; True; False; Bottom]
-               let equal = equal
-               let compare = compare
-               let hash = hash
-               let rehash = Datatype.identity
-               let copy = Datatype.identity
-               let pretty = pretty
-               let mem_project = Datatype.never_any_project
-             end) :
-             Datatype.S with type t := t)
-end
-
 (*
 Local Variables:
 compile-command: "make -C ../../.."

src/kernel_services/abstract_interp/abstract_interp.mli

@@ -92,11 +92,6 @@ module Rel : sig
   val check: rem:t -> modu:Int.t -> bool
 end
 
-module Bool : sig
-  type t = Top | True | False | Bottom
-  include Full_AI_Lattice_with_cardinality with type t := t
-end
-
 module Make_Lattice_Set
     (V : Datatype.S)
     (Set: Lattice_type.Hptset with type elt = V.t)