module Relation:`sig`

..`end`

Functions to manipulate Relation expressions

`val is_relation : ``Expr.expr -> bool`

Indicates whether the term is of a relation sort.

`val is_store : ``Expr.expr -> bool`

Indicates whether the term is an relation store

Insert a record into a relation.
The function takes `n+1`

arguments, where the first argument is the relation and the remaining `n`

elements
correspond to the `n`

columns of the relation.

`val is_empty : ``Expr.expr -> bool`

Indicates whether the term is an empty relation

`val is_is_empty : ``Expr.expr -> bool`

Indicates whether the term is a test for the emptiness of a relation

`val is_join : ``Expr.expr -> bool`

Indicates whether the term is a relational join

`val is_union : ``Expr.expr -> bool`

Indicates whether the term is the union or convex hull of two relations. The function takes two arguments.

`val is_widen : ``Expr.expr -> bool`

Indicates whether the term is the widening of two relations The function takes two arguments.

`val is_project : ``Expr.expr -> bool`

Indicates whether the term is a projection of columns (provided as numbers in the parameters). The function takes one argument.

`val is_filter : ``Expr.expr -> bool`

Indicates whether the term is a relation filter

Filter (restrict) a relation with respect to a predicate. The first argument is a relation. The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation. So the first column in the relation has index 0.

`val is_negation_filter : ``Expr.expr -> bool`

Indicates whether the term is an intersection of a relation with the negation of another.

Intersect the first relation with respect to negation of the second relation (the function takes two arguments). Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in ( x : expr ) in pos, such that there is no y in neg that agrees with ( x : expr ) on the columns c1, d1, .., cN, dN.

`val is_rename : ``Expr.expr -> bool`

Indicates whether the term is the renaming of a column in a relation

The function takes one argument. The parameters contain the renaming as a cycle.

`val is_complement : ``Expr.expr -> bool`

Indicates whether the term is the complement of a relation

`val is_select : ``Expr.expr -> bool`

Indicates whether the term is a relational select

Check if a record is an element of the relation.
The function takes `n+1`

arguments, where the first argument is a relation,
and the remaining `n`

arguments correspond to a record.

`val is_clone : ``Expr.expr -> bool`

Indicates whether the term is a relational clone (copy)

Create a fresh copy (clone) of a relation.
The function is logically the identity, but
in the context of a register machine allows
for terms of kind `Relation.is_union`

to perform destructive updates to the first argument.

`val get_arity : ``Sort.sort -> int`

The arity of the relation sort.

`val get_column_sorts : ``Sort.sort -> Sort.sort list`

The sorts of the columns of the relation sort.