Indices for tuples, relations and tables

Tup α β is the tuple of components α ++ [β], Rel α β a set of such tuples and Tab α β a bag of them. Splitting the last component off keeps the list non-empty and lets signatures name it, so that relational join is typed by its signature alone:

relJoin : Term (Rel α μ) → Term (Rel (μ :: α') β') → Env (Term (Rel (α ++ α') β'))

Neither a relation nor a table is a sort of its own, so relToSet/relOfSet and tableToBag/tableOfBag cross over for free.

class Cvc.ToTypList (α : List Type) : Type

The Typs a list of Lean types denotes.

• typs : List Typ

  The Typs, in order.

@[instance_reducible]

instance Cvc.ToTypList.instNil : ToTypList []

Equations

• Cvc.ToTypList.instNil = { typs := [] }

@[instance_reducible]

instance Cvc.ToTypList.instConsOfToTyp {α : Type} {αs : List Type} [A : ToTyp α] [As : ToTypList αs] : ToTypList (α :: αs)

Equations

• Cvc.ToTypList.instConsOfToTyp = { typs := Cvc.ToTyp.typ α :: Cvc.ToTypList.typs αs }

def Cvc.ToTypList.typsOf (α : List Type) (β : Type) [As : ToTypList α] [B : ToTyp β] : List Typ

The Typs of α ++ [β], which is what every index here describes.

Equations

• Cvc.ToTypList.typsOf α β = Cvc.ToTypList.typs α ++ [Cvc.ToTyp.typ β]

structure Cvc.Tup (α : List Type) (β : Type) : Type

A tuple of the components α ++ [β].

Carries no data: it only indexes terms, which Cvc.Typed.Term.mkTup builds.

structure Cvc.Rel (α : List Type) (β : Type) : Type

A relation over the components α ++ [β]: a set of Tup α β.

structure Cvc.Tab (α : List Type) (β : Type) : Type

A table over the columns α ++ [β]: a bag of Tup α β, so a row may repeat.

Instances for nesting

These indices carry no data, so their comparisons are trivial. They exist only so that a container of them can be written: relGroup answers a Set (Rel α β).

@[instance_reducible]

instance Cvc.instDecidableEqTup {α : List Type} {β : Type} : DecidableEq (Tup α β)

Equations

• Cvc.instDecidableEqTup x✝¹ x✝ = isTrue ⋯

@[instance_reducible]

instance Cvc.instDecidableEqRel {α : List Type} {β : Type} : DecidableEq (Rel α β)

Equations

• Cvc.instDecidableEqRel x✝¹ x✝ = isTrue ⋯

@[instance_reducible]

instance Cvc.instDecidableEqTab {α : List Type} {β : Type} : DecidableEq (Tab α β)

Equations

• Cvc.instDecidableEqTab x✝¹ x✝ = isTrue ⋯

@[instance_reducible]

instance Cvc.instOrdTup {α : List Type} {β : Type} : Ord (Tup α β)

Equations

• Cvc.instOrdTup = { compare := fun (x x_1 : Cvc.Tup α β) => Ordering.eq }

@[instance_reducible]

instance Cvc.instOrdRel {α : List Type} {β : Type} : Ord (Rel α β)

Equations

• Cvc.instOrdRel = { compare := fun (x x_1 : Cvc.Rel α β) => Ordering.eq }

@[instance_reducible]

instance Cvc.instOrdTab {α : List Type} {β : Type} : Ord (Tab α β)

Equations

• Cvc.instOrdTab = { compare := fun (x x_1 : Cvc.Tab α β) => Ordering.eq }

@[instance_reducible]

instance Cvc.instHashableTup {α : List Type} {β : Type} : Hashable (Tup α β)

Equations

• Cvc.instHashableTup = { hash := fun (x : Cvc.Tup α β) => 0 }

@[instance_reducible]

instance Cvc.instHashableRel {α : List Type} {β : Type} : Hashable (Rel α β)

Equations

• Cvc.instHashableRel = { hash := fun (x : Cvc.Rel α β) => 0 }

@[instance_reducible]

instance Cvc.instHashableTab {α : List Type} {β : Type} : Hashable (Tab α β)

Equations

• Cvc.instHashableTab = { hash := fun (x : Cvc.Tab α β) => 0 }

@[instance_reducible]

instance Cvc.instToTypTupOfToTypList {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : ToTyp (Tup α β)

Equations

• Cvc.instToTypTupOfToTypList = { typ := Cvc.Typ.prod (Cvc.ToTypList.typsOf α β) }

@[instance_reducible]

instance Cvc.instToTypRelOfToTypList {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : ToTyp (Rel α β)

Equations

• Cvc.instToTypRelOfToTypList = { typ := Cvc.Typ.set (Cvc.Typ?.prod (Cvc.ToTypList.typsOf α β)) }

@[instance_reducible]

instance Cvc.instToTypTabOfToTypList {α : List Type} {β : Type} [ToTypList α] [ToTyp β] : ToTyp (Tab α β)

Equations

• Cvc.instToTypTabOfToTypList = { typ := Cvc.Typ.bag (Cvc.Typ?.prod (Cvc.ToTypList.typsOf α β)) }

Positions

A Col is a component's position that knows the component's type, and a Cols a selection of positions that knows the index it lands at, which is what types projection (Cvc.Typed.Term.tupProject and friends). Positions count from zero over α ++ [β], and are written with col% and cols% under open Cvc.

class Cvc.ColHead (α : List Type) (β : Type) (γ : outParam Type) : Type

The component a position-zero column has: the head of α, or β when α is empty.

@[instance_reducible]

instance Cvc.instColHeadNil {β : Type} : ColHead [] β β

Equations

• Cvc.instColHeadNil = { }

@[instance_reducible]

instance Cvc.instColHeadCons {γ : Type} {αs : List Type} {β : Type} : ColHead (γ :: αs) β γ

Equations

• Cvc.instColHeadCons = { }

structure Cvc.Col (α : List Type) (β γ : Type) : Type

The position of a component of type gamma in a tuple whose components are α ++ [β].

Carries nothing but the position. Built with col%, or with zero/next directly.

• idx : Nat

def Cvc.Col.zero {α : List Type} {β γ : Type} [ColHead α β γ] : Col α β γ

The first component.

Equations

• Cvc.Col.zero = { idx := 0 }

def Cvc.Col.next {αs : List Type} {β γ α : Type} (c : Col αs β γ) : Col (α :: αs) β γ

The position after the given one, in a tuple with one more component in front.

Equations

• c.next = { idx := Cvc.Col.idx✝ c + 1 }

def Cvc.Col.toNat {α : List Type} {β γ : Type} (c : Col α β γ) : Nat

The position as a number, counting from zero over α ++ [β].

Equations

• c.toNat = Cvc.Col.idx✝ c

structure Cvc.Cols (α : List Type) (β : Type) (α' : List Type) (β' : Type) : Type

Positions to project onto, in order, along with the index they land at.

last and cons are the only builders, so the positions collected and the components the result index describes stay in step, and the selection cannot come out empty. A position may appear twice and they need not increase, so this reorders and duplicates as readily as it selects.

• idxs : Array Nat

def Cvc.Cols.last {α : List Type} {β β' : Type} (c : Col α β β') : Cols α β [] β'

The final position of the selection.

Equations

• Cvc.Cols.last c = { idxs := #[Cvc.Col.idx✝ c] }

def Cvc.Cols.cons {α : List Type} {β γ : Type} {α' : List Type} {β' : Type} (c : Col α β γ) (rest : Cols α β α' β') : Cols α β (γ :: α') β'

Adds a position in front of the ones collected so far.

Equations

• Cvc.Cols.cons c rest = { idxs := #[Cvc.Col.idx✝ c] ++ Cvc.Cols.idxs✝ rest }

def Cvc.Cols.toArray {α : List Type} {β : Type} {α' : List Type} {β' : Type} (cols : Cols α β α' β') : Array Nat

The positions as numbers, in order.

Equations

• cols.toArray = Cvc.Cols.idxs✝ cols

def Cvc.«termCol%_» : Lean.ParserDescr

A component's position, written as a numeral: col%2 is the third component.

Out of range is a type error, there being no ColHead instance left to end the chain. Declared at maximum precedence, so it needs no parentheses as a function argument.

Equations

• Cvc.«termCol%_» = Lean.ParserDescr.node `Cvc.«termCol%_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "col%") (Lean.ParserDescr.const `num))

def Cvc.«termCols%[_,,]» : Lean.ParserDescr

A selection of positions: cols% [2, 0] projects onto the third component then the first.

An element may be any Col term, so a named column works — cols% [dept, 0] — and a numeral is shorthand for col% of it.

Equations

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