Tables, typed

A table is a bag of tuples, indexed by Tab α β: a relation with duplicates kept. Its rows are the Tup α β tuples of Cvc.Typed.Theory.Relation, built with mkTup.

The bag operators are restated at a table's index (tableUnionMax, tableCount, …); tableToBag crosses to Bag, for bagMap and bagFold. cvc5 marks every table-specific kind experimental.

Crossing to and from bags

Both directions are the identity on terms: a table is a bag of tuples, and only the index differs.

def Cvc.Typed.Term.tableToBag [Ω] {α : List Type} {β : Type} [Ord (Tup α β)] (table : Term (Tab α β)) : Term (Bag (Tup α β))

Reads a table as the bag of tuples it is.

Equations

• table.tableToBag = table

def Cvc.Typed.Term.tableOfBag [Ω] {α : List Type} {β : Type} [Ord (Tup α β)] (bag : Term (Bag (Tup α β))) : Term (Tab α β)

Reads a bag of tuples as the table it is.

Equations

• bag.tableOfBag = bag

Table operators

def Cvc.Typed.Term.tableProduct [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (lft : Term (Tab α β)) (rgt : Term (Tab α' β')) : Env (Term (Tab (α ++ β :: α') β'))

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

Equations

• lft.tableProduct rgt = lft.erase.tableProduct rgt.erase

def Cvc.Typed.Term.tableJoin [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (columns : Array (Nat × Nat)) (lft : Term (Tab α β)) (rgt : Term (Tab α' β')) : Env (Term (Tab (α ++ β :: α') β'))

Equi-join: the product, keeping the pairings whose given column pairs agree.

The result's sort is the product's, since the pairs only filter.

Equations

• Cvc.Typed.Term.tableJoin columns lft rgt = Cvc.Untyped.Term.tableJoin columns lft.erase rgt.erase

def Cvc.Typed.Term.tableGroup [Ω] {α : List Type} {β : Type} [Ord (Tab α β)] (columns : Array Nat) (table : Term (Tab α β)) : Env (Term (Bag (Tab α β)))

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

Answers a bag of tables. The columns choose what is compared and so do not reach the result's sort.

Equations

• Cvc.Typed.Term.tableGroup columns table = Cvc.Untyped.Term.tableGroup columns table.erase

def Cvc.Typed.Term.tableAggregate [Ω] {γ : Type} {α : List Type} {β : Type} [Ord γ] (columns : Array Nat) (f : Term (Tup α β → γ → γ)) (init : Term γ) (table : Term (Tab α β)) : Env (Term (Bag γ))

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

The groups are tableGroup's, but the answer is a bag of accumulators rather than a bag of tables: f runs over each group's rows starting from init, and the result collects one value of gamma per group.

f is a function-sorted term, which Term.lambda builds. Its two arguments are a row of the table and the accumulator, in that order, and its result is the new accumulator — so gamma is fixed by init and by f's codomain together. This is SQL's GROUP BY with an aggregate function.

The columns only say what is grouped, so they do not reach the result's sort. With none of them every row is in one group, which is an ordinary fold over the whole table.

Equations

• Cvc.Typed.Term.tableAggregate columns f init table = Cvc.Untyped.Term.tableAggregate columns f.erase init.erase table.erase

def Cvc.Typed.Term.tableProject [Ω] {α : List Type} {β : Type} {α' : List Type} {β' : Type} (cols : Cols α β α' β') (table : Term (Tab α β)) : Env (Term (Tab α' β'))

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

Columns are written cols% [2, 0]. Untyped.Term.tableProject takes them as an Array Nat, for columns known only at run time.

Equations

• Cvc.Typed.Term.tableProject cols table = Cvc.Untyped.Term.tableProject cols.toArray table.erase

The bag operators, at a table's index

def Cvc.Typed.Term.tableMember [Ω] {α : List Type} {β : Type} (row : Term (Tup α β)) (table : Term (Tab α β)) : Env (Term Bool)

Whether a row occurs at least once.

Equations

• row.tableMember table = row.erase.bagMember table.erase

def Cvc.Typed.Term.tableSubtable [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term Bool)

Whether every row of the first table occurs at least as often in the second.

Equations

• lft.tableSubtable rgt = lft.erase.bagSubbag rgt.erase

def Cvc.Typed.Term.tableMake [Ω] {α : List Type} {β : Type} (row : Term (Tup α β)) (count : Term Int) : Env (Term (Tab α β))

The table holding one row, with the given multiplicity.

Equations

• row.tableMake count = row.erase.bagMake count.erase

def Cvc.Typed.Term.tableCount [Ω] {α : List Type} {β : Type} (row : Term (Tup α β)) (table : Term (Tab α β)) : Env (Term Int)

How often a row occurs.

Equations

• row.tableCount table = row.erase.bagCount table.erase

def Cvc.Typed.Term.tableCard [Ω] {α : List Type} {β : Type} (table : Term (Tab α β)) : Env (Term Int)

How many rows the table holds, counting duplicates.

Equations

• table.tableCard = table.erase.bagCard

def Cvc.Typed.Term.tableSetof [Ω] {α : List Type} {β : Type} (table : Term (Tab α β)) : Env (Term (Tab α β))

The table with every multiplicity reduced to one.

Equations

• table.tableSetof = table.erase.bagSetof

def Cvc.Typed.Term.tableChoose [Ω] {α : List Type} {β : Type} (table : Term (Tab α β)) : Env (Term (Tup α β))

Some row of the table, unspecified which; undefined on the empty table.

Equations

• table.tableChoose = table.erase.bagChoose

def Cvc.Typed.Term.tableUnionMax [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term (Tab α β))

Union taking the greater multiplicity of each row.

Equations

• lft.tableUnionMax rgt = lft.erase.bagUnionMax rgt.erase

def Cvc.Typed.Term.tableUnionMaxN [Ω] {α : List Type} {β : Type} (tables : Terms (Tab α β)) (atLeastTwoElements : 2 ≤ Array.size tables := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Tab α β))

N-ary version of tableUnionMax, requires at least two elements.

Equations

• Cvc.Typed.Term.tableUnionMaxN tables atLeastTwoElements = Cvc.Untyped.Term.bagUnionMaxN tables atLeastTwoElements

def Cvc.Typed.Term.tableUnionDisjoint [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term (Tab α β))

Union adding the multiplicities of each row.

Equations

• lft.tableUnionDisjoint rgt = lft.erase.bagUnionDisjoint rgt.erase

def Cvc.Typed.Term.tableUnionDisjointN [Ω] {α : List Type} {β : Type} (tables : Terms (Tab α β)) (atLeastTwoElements : 2 ≤ Array.size tables := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Tab α β))

N-ary version of tableUnionDisjoint, requires at least two elements.

Equations

• Cvc.Typed.Term.tableUnionDisjointN tables atLeastTwoElements = Cvc.Untyped.Term.bagUnionDisjointN tables atLeastTwoElements

def Cvc.Typed.Term.tableInterMin [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term (Tab α β))

Intersection taking the lesser multiplicity of each row.

Equations

• lft.tableInterMin rgt = lft.erase.bagInterMin rgt.erase

def Cvc.Typed.Term.tableInterMinN [Ω] {α : List Type} {β : Type} (tables : Terms (Tab α β)) (atLeastTwoElements : 2 ≤ Array.size tables := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Tab α β))

N-ary version of tableInterMin, requires at least two elements.

Equations

• Cvc.Typed.Term.tableInterMinN tables atLeastTwoElements = Cvc.Untyped.Term.bagInterMinN tables atLeastTwoElements

def Cvc.Typed.Term.tableDifferenceSubtract [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term (Tab α β))

Difference subtracting multiplicities.

Equations

• lft.tableDifferenceSubtract rgt = lft.erase.bagDifferenceSubtract rgt.erase

def Cvc.Typed.Term.tableDifferenceRemove [Ω] {α : List Type} {β : Type} (lft rgt : Term (Tab α β)) : Env (Term (Tab α β))

Difference removing a row entirely wherever it occurs on the right.

Equations

• lft.tableDifferenceRemove rgt = lft.erase.bagDifferenceRemove rgt.erase

def Cvc.Typed.Term.tableFilter [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (table : Term (Tab α β)) : Env (Term (Tab α β))

The rows satisfying a predicate.

Equations

• p.tableFilter table = p.erase.bagFilter table.erase

def Cvc.Typed.Term.tableAll [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (table : Term (Tab α β)) : Env (Term Bool)

Whether every row satisfies a predicate.

Equations

• p.tableAll table = p.erase.bagAll table.erase

def Cvc.Typed.Term.tableSome [Ω] {α : List Type} {β : Type} (p : Term (Tup α β → Bool)) (table : Term (Tab α β)) : Env (Term Bool)

Whether some row satisfies a predicate.

Equations

• p.tableSome table = p.erase.bagSome table.erase

def Cvc.Typed.Term.tablePartition [Ω] {α : List Type} {β : Type} [Ord (Tab α β)] (p : Term (Tup α β → Tup α β → Bool)) (table : Term (Tab α β)) : Env (Term (Bag (Tab α β)))

Partitions the rows by an equivalence, answering a bag of tables.

Equations

• p.tablePartition table = p.erase.bagPartition table.erase

def Cvc.Typed.Term.tableEmpty' [Ω] (α : List Type) (β : Type) [ToTypList α] [ToTyp β] : Env (Term (Tab α β))

The empty table of the given shape.

Equations

• Cvc.Typed.Term.tableEmpty' α β = do let __do_lift ← Cvc.Srt.of (Cvc.Tup α β) Cvc.Untyped.Term.bagEmpty __do_lift

@[reducible, inline]

abbrev Cvc.Typed.Term.tableEmpty [Ω] {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : Env (Term (Tab α β))

The empty table of the given shape.

Equations

• Cvc.Typed.Term.tableEmpty = Cvc.Typed.Term.tableEmpty' α β