Module HoareDomain.HoarePO
Parameters
Signature
type t = bucket Batteries.Map.Int.tmodule Map = Batteries.Map.Intval elements : 'a list Map.t -> 'a listval merge :
[< `Join | `Meet Join ] ->
('a -> 'a -> 'a) ->
'a list Map.t ->
'a list Map.t ->
'a list Map.tval merge_meet :
('a -> 'b -> 'c) ->
'b list Map.t ->
'a list Map.t ->
'c list Map.tval merge_widen :
(E.t -> E.t -> E.t) ->
E.t list Map.t ->
E.t list Map.t ->
E.t list Map.tval merge_join :
(E.t -> E.t -> E.t) ->
E.t list Map.t ->
E.t list Map.t ->
E.t list Map.tval join : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval widen : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval meet : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval narrow : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval of_list : E.t list -> E.t list Map.tval singleton : E.t -> E.t list Map.tval exists : ('a -> bool) -> 'a list Map.t -> boolval for_all : ('a -> bool) -> 'a list Map.t -> boolval mem : E.t -> E.t list Map.t -> boolval choose : 'a list Map.t -> 'aval apply_list : ('a list -> E.t list) -> 'a list Map.t -> E.t list Map.tval map : ('a -> E.t) -> 'a list Map.t -> E.t list Map.tval filter : (E.t -> bool) -> E.t list Map.t -> E.t list Map.tval remove : E.t -> E.t list Map.t -> E.t list Map.tval add : E.t -> E.t list Map.t -> E.t list Map.tval fold : ('a -> 'b -> 'b) -> 'a list Map.t -> 'b -> 'bval cardinal : 'a list Map.t -> intval diff : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval empty : unit -> 'a Map.tval is_empty : 'a Map.t -> boolval union : E.t list Map.t -> E.t list Map.t -> E.t list Map.tval iter : ('a -> unit) -> 'a list Map.t -> unitval bot : unit -> 'a Map.tval is_bot : 'a Map.t -> boolval leq : E.t list Map.t -> E.t list Map.t -> boolval name : unit -> stringval equal : E.t list Map.t -> E.t list Map.t -> boolval hash : E.t list Map.t -> intval compare : E.t list Map.t -> E.t list Map.t -> intval show : E.t list Map.t -> stringval to_yojson : E.t list Map.t -> [> `List of Yojson.Safe.t list ]val pretty : unit -> E.t list Map.t -> Pretty.docval pretty_diff : unit -> (t * t) -> Pretty.docval printXml : 'a BatInnerIO.output -> E.t list Map.t -> unit