Tables, sort-erased

A table is a bag of tuples — (Bag (Tuple T₁ … Tⱼ)) — and not a sort of its own: there is no TABLE_SORT. These are relational-database tables, so a row can repeat, unlike in the relations of Cvc.Untyped.Theory.Relation, which have every operator here and more.

cvc5 marks every kind here experimental, "may be changed or removed in future versions".

tableAggregate takes its folding function as a term, which Term.lambda builds.

def Cvc.Untyped.Term.tableProduct [Ω] (lft rgt : Term) : Env Term

Cartesian product: every pairing of rows, with the columns appended.

Equations

• lft.tableProduct rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.TABLE_PRODUCT #[lft, rgt]

def Cvc.Untyped.Term.tableProject [Ω] (columns : Array Nat) (table : Term) : Env Term

Projects every row onto the given columns, in the order given.

Columns count from zero, and need be neither increasing nor distinct, so this reorders and duplicates as readily as it selects.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.tableJoin [Ω] (columns : Array (Nat × Nat)) (lft rgt : Term) : Env Term

Equi-join: the product of the two tables, keeping the pairings whose given columns agree.

Each pair is a column of lft and one of rgt that must be equal. The result's sort is the product's, since the columns only filter.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.tableGroup [Ω] (columns : Array Nat) (table : Term) : Env Term

Partitions the table, putting rows that agree on the given columns in the same part.

Answers a bag of tables: (Bag (Tuple Int Bool)) grouped gives (Bag (Bag (Tuple Int Bool))). SQL's GROUP BY.

Equations

• Cvc.Untyped.Term.tableGroup columns table = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.TABLE_GROUP columns tm.mkTermOfOp __do_lift #[table]

def Cvc.Untyped.Term.tableAggregate [Ω] (columns : Array Nat) (f init table : Term) : Env Term

Folds each group of rows that agree on the given columns.

f is a term of function sort (Tuple T₁ … Tⱼ) → T → T — a Term.lambda over a row bound variable and an accumulator — and init is the accumulator's starting value. The answer is a (Bag T): one entry per group, of the accumulator's sort rather than the table's.

With no column every row is in one group, which is an ordinary fold over the whole table.

Equations

• One or more equations did not get rendered due to their size.