Module Vset

module Vset: sig .. end

Logical Sets

type set = vset list 
type vset = 
| Set of Lang.F.tau * Lang.F.term
| Singleton of Lang.F.term
| Range of Lang.F.term option * Lang.F.term option
| Descr of Lang.F.var list * Lang.F.term * Lang.F.pred
val tau_of_set : Lang.F.tau -> Lang.F.tau
val vars : set -> Lang.F.Vars.t
val occurs : Lang.F.var -> set -> bool
val empty : set
val singleton : Lang.F.term -> set
val range : Lang.F.term option -> Lang.F.term option -> set
val union : set -> set -> set
val inter : Lang.F.term -> Lang.F.term -> Lang.F.term
val member : Lang.F.term -> set -> Lang.F.pred
val in_size : Lang.F.term -> int -> Lang.F.pred
val in_range : Lang.F.term -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val sub_range : Lang.F.term ->
Lang.F.term -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val ordered : limit:bool ->
strict:bool -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred

- limit: result when either parameter is None

val is_empty : set -> Lang.F.pred
val equal : set -> set -> Lang.F.pred
val subset : set -> set -> Lang.F.pred
val disjoint : set -> set -> Lang.F.pred
val concretize : set -> Lang.F.term
val bound_shift : Lang.F.term option -> Lang.F.term -> Lang.F.term option
val bound_add : Lang.F.term option -> Lang.F.term option -> Lang.F.term option
val bound_sub : Lang.F.term option -> Lang.F.term option -> Lang.F.term option

Pretty

val pp_bound : Stdlib.Format.formatter -> Lang.F.term option -> unit
val pp_vset : Stdlib.Format.formatter -> vset -> unit
val pretty : Stdlib.Format.formatter -> set -> unit

Mapping

These operations compute different kinds of {f x y with x in A, y in B}.

val map : (Lang.F.term -> 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 : (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
set -> set -> set
val lift_add : set -> set -> set
val lift_sub : set -> set -> set
val descr : vset -> Lang.F.var list * Lang.F.term * Lang.F.pred