module Vset: sig
.. end
Logical Sets
type
set = vset list
type
vset =
| |
Set of Wp.Lang.F.tau * Wp.Lang.F.term |
| |
Singleton of Wp.Lang.F.term |
| |
Range of Wp.Lang.F.term option * Wp.Lang.F.term option |
| |
Descr of Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred |
val tau_of_set : Wp.Lang.F.tau -> Wp.Lang.F.tau
val vars : set -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> set -> bool
val empty : set
val singleton : Wp.Lang.F.term -> set
val range : Wp.Lang.F.term option -> Wp.Lang.F.term option -> set
val union : set -> set -> set
val inter : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val member : Wp.Lang.F.term -> set -> Wp.Lang.F.pred
val in_size : Wp.Lang.F.term -> int -> Wp.Lang.F.pred
val in_range : Wp.Lang.F.term ->
Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
val sub_range : Wp.Lang.F.term ->
Wp.Lang.F.term ->
Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
val ordered : limit:bool ->
strict:bool ->
Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.pred
-
limit
: result when either parameter is
None
strict
: if true
, comparison is <
instead of <=
val equal : set -> set -> Wp.Lang.F.pred
val subset : set -> set -> Wp.Lang.F.pred
val disjoint : set -> set -> Wp.Lang.F.pred
val concretize : set -> Wp.Lang.F.term
val bound_shift : Wp.Lang.F.term option -> Wp.Lang.F.term -> Wp.Lang.F.term option
val bound_add : Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.term option
val bound_sub : Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Lang.F.term option
Pretty
val pp_bound : Format.formatter -> Wp.Lang.F.term option -> unit
val pp_vset : Format.formatter -> vset -> unit
val pretty : Format.formatter -> set -> unit
Maping
These operations computes different kinds of {f x y with x in A, y in B}
.
val map : (Wp.Lang.F.term -> Wp.Lang.F.term) -> set -> set
val map_opp : set -> set
Lifting
These operations computes different sort of {f x y with x in A, y in B}
.
val lift : (Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) ->
set -> set -> set
val lift_add : set -> set -> set
val lift_sub : set -> set -> set
val descr : vset -> Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred