sig
type set = Wp.Vset.vset list
and 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 : Wp.Vset.set -> Wp.Lang.F.Vars.t
val occurs : Wp.Lang.F.var -> Wp.Vset.set -> bool
val empty : Wp.Vset.set
val singleton : Wp.Lang.F.term -> Wp.Vset.set
val range : Wp.Lang.F.term option -> Wp.Lang.F.term option -> Wp.Vset.set
val union : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
val inter : Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term
val member : Wp.Lang.F.term -> Wp.Vset.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
val equal : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
val subset : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
val disjoint : Wp.Vset.set -> Wp.Vset.set -> Wp.Lang.F.pred
val concretize : Wp.Vset.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
val pp_bound : Format.formatter -> Wp.Lang.F.term option -> unit
val pp_vset : Format.formatter -> Wp.Vset.vset -> unit
val map : (Wp.Lang.F.term -> Wp.Lang.F.term) -> Wp.Vset.set -> Wp.Vset.set
val map_opp : Wp.Vset.set -> Wp.Vset.set
val lift :
(Wp.Lang.F.term -> Wp.Lang.F.term -> Wp.Lang.F.term) ->
Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
val lift_add : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
val lift_sub : Wp.Vset.set -> Wp.Vset.set -> Wp.Vset.set
val descr :
Wp.Vset.vset -> Wp.Lang.F.var list * Wp.Lang.F.term * Wp.Lang.F.pred
end