Represents a relation between a domain and a co-domain. An element of t can be see as a set of bindings, i.e., a subset of dom * codom, or as a function from dom to subsets of codom. Relations are imutable, purely functional data-structures.
This data-type maintains both the relation and its inverse, so that we can efficiently compute both the image of a domain element and the inverse image of a codomain element, at the cost of slower insersion and removal (to keep the maps consistent).
map f r returns a relation where every binding (x,y) is replaced with (x',y')=f x y. The bindings are considered in increasing order for the lexicographic order sorting through dom first, and then codom.
domain_map f r returns a relation where every binding (x,y) is replaced with (f x,y). The bindings are considered in increasing order for the lexicographic order sorting through dom first, and then codom.
codomain_map f r returns a relation where every binding (x,y) is replaced with (x,f y). The bindings are considered in increasing order for the dual lexicographic order sorting through codom first, and then dom.
for_all f r returns true if f x y is true for every binding (x,y) in r. The bindings are considered in increasing order for the lexicographic order sorting through dom first, and then codom.
exists f r returns true if f x y is true for at leat one binding (x,y) in r. The bindings are considered in increasing order for the lexicographic order sorting through dom first, and then codom.
iter2 f1 f2 f r1 r2 applies f1 to the bindings only in r1, f2 to the bindings only in r2, and f to the bindings in both r1 and r2. The bindings are considered in increasing lexicographic order.
fold2 f1 f2 f r1 r2 applies f1 to the bindings only in r1, f2 to the bindings only in r2, and f to the bindings in both r1 and r2. The bindings are considered in increasing lexicographic order.
for_all2 f1 f2 f r1 r2 is true if f1 is true on all the bindings only in r1, f2 is true on all the bindings only in r2, and f is true on all the bindings both in r1 and r2. The bindings are considered in increasing lexicographic order.
exists2 f1 f2 f r1 r2 is true if f1 is true on one binding only in r1 or f2 is true on one binding only in r2, or f is true on one binding both in r1 and r2. The bindings are considered in increasing lexicographic order.
iter2_diff f1 f2 r1 r2 applies f1 to the bindings only in r1 and f2 to the bindings only in r2. The bindings both in r1 and r2 are ignored. The bindings are considered in increasing lexicographic order. It is equivalent to calling iter2 with f = fun x y -> (), but more efficient.
val fold2_diff :
(dom->codom->'a->'a)->(dom->codom->'a->'a)->t->t->'a->'a
fold2_diff f1 f2 r1 r2 applies f1 to the bindings only in r1 and f2 to the bindings only in r2. The bindings both in r1 and r2 are ignored. The bindings are considered in increasing lexicographic order. It is equivalent to calling fold2 with f = fun x y acc -> acc, but more efficient.
val for_all2_diff :
(dom->codom-> bool)->(dom->codom-> bool)->t->t->
bool
for_all2_diff f1 f2 f r1 r2 is true if f1 is true on all the bindings only in r1 and f2 is true on all the bindings only in r2. The bindings both in r1 and r2 are ignored. The bindings are considered in increasing lexicographic order. It is equivalent to calling for_all2 with f = fun x y -> true, but more efficient.
val exists2_diff :
(dom->codom-> bool)->(dom->codom-> bool)->t->t->
bool
exists2_diff f1 f2 f r1 r2 is true if f1 is true on one binding only in r1 or f2 is true on one binding only in r2. The bindings both in r1 and r2 are ignored. The bindings are considered in increasing lexicographic order. It is equivalent to calling exists2 with f = fun x y -> false, but more efficient.
Multi-map domain operations
These functions consider the relation as a map from domain elements to codomain sets.
map_domain f r returns a new relation where the image set ys of x in r is replaced with f x ys. The domain elements are considered in increasing order.
map2_domain f r1 r2 is similar to map_domain but applies f to pairs of image sets ys1 and ys2 corresponding to the same domain element x in r1 and r2 respectively. r1 and r2 must have the same domain set. The bindings are passed to f in increasing order of domain elements.
map2_domain f1 f2 f r1 r2 is similar to map2_domain but accepts relations with different domain sets. To get a new binding, f1 is used for domain elements appearing only in r1, f2 for domain elements appearing only in r2 and f for common domain elements. The bindings are passed in increasing order of domain elements.
map2zo_domain f1 f2 f r1 r2 is similar to map2o_domain but f is not called on physically equal image sets. The bindings are passed in increasing order of domain elements.
map_domain f r returns a new relation where the image set ys of x in r is replaced with f x ys. The domain elements are considered in increasing order.
val for_all_domain : (dom->codom_set-> bool)->t-> bool
for_all_domain f r returns true if f x ys is true for every domain element x and its image set ys in r. The domain elements are considered in increasing order.
val exists_domain : (dom->codom_set-> bool)->t-> bool
exists_domain f r returns true if f x ys is true for at least one domain element x and its image set ys in r. The domain elements are considered in increasing order.
elemets_domain r returns the list of domain elements used in r. The elements are returned in increasing order.
Multi-map codomain operations
These functions consider the relation as a map from codomain elements to domain sets.
val iter_codomain : (codom->dom_set-> unit)->t-> unit
iter_codomain f r applies f y xs for every codomain element y and its inverse image set xs in r. The codomain elements are considered in increasing order.
val fold_codomain : (codom->dom_set->'a->'a)->t->'a->'a
fold_codomain f r acc applies f y xs acc for every codomain element y and its inverse image set xs in r. The codomain elements are considered in increasing order.
map_codomain f r returns a new relation where the inverse image set xs of y in r is replaced with f y xs. The codomain elements are considered in increasing order.
val for_all_codomain : (codom->dom_set-> bool)->t-> bool
for_all_codomain f r returns true if f y xs is true for every codomain element y and its inverse image set xs in r. The codomain elements are considered in increasing order.
val exists_codomain : (codom->dom_set-> bool)->t-> bool
exists_codomain f r returns true if f y xs is true for at least one codomain element y and its inverse image set xs in r. The codomain elements are considered in increasing order.