module Relation:sig..end
Functions to manipulate Relation expressions
val is_relation : Expr.expr -> boolIndicates whether the term is of a relation sort.
val is_store : Expr.expr -> boolIndicates 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 -> boolIndicates whether the term is an empty relation
val is_is_empty : Expr.expr -> boolIndicates whether the term is a test for the emptiness of a relation
val is_join : Expr.expr -> boolIndicates whether the term is a relational join
val is_union : Expr.expr -> boolIndicates whether the term is the union or convex hull of two relations. The function takes two arguments.
val is_widen : Expr.expr -> boolIndicates whether the term is the widening of two relations The function takes two arguments.
val is_project : Expr.expr -> boolIndicates whether the term is a projection of columns (provided as numbers in the parameters). The function takes one argument.
val is_filter : Expr.expr -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates whether the term is the complement of a relation
val is_select : Expr.expr -> boolIndicates 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 -> boolIndicates 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 -> intThe arity of the relation sort.
val get_column_sorts : Sort.sort -> Sort.sort listThe sorts of the columns of the relation sort.