module Abstract_interp:sig
..end
exception Error_Top
exception Error_Bottom
exception Not_less_than
Lattice.cardinal_less_than
.exception Can_not_subdiv
Fval.subdiv_float_interval
.type
truth =
| |
True |
|||
| |
False |
|||
| |
Unknown |
(* |
Truth values with a possibility for 'Unknown'
| *) |
val inv_truth : truth -> truth
module Comp:sig
..end
==, !=, <, >, <=, >=
.
module Int:sig
..end
module Rel:sig
..end
module Bool:sig
..end
module Make_Lattice_Base:
module Make_Lattice_Set:functor (
V
:
Datatype.S
) ->
functor (
Set
:
Lattice_type.Hptset
with type elt = V.t
) ->
Lattice_type.Lattice_Set
with module O = Set
module Make_Hashconsed_Lattice_Set:
module type Collapse =sig
..end
module Make_Lattice_Product:functor (
L1
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
C.collapse
then L1.bottom,_
= _,L2.bottom
= bottom
module Make_Lattice_UProduct:functor (
L1
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
functor (
L2
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
Lattice_UProduct
with type t1 = L1.t and type t2 = L2.t
module Make_Lattice_Sum:functor (
L1
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
functor (
L2
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
Lattice_Sum
with type t1 = L1.t and type t2 = L2.t