The order of cells, and the symbolic window

A window sorts its partition by an ORDER BY clause and reads frames off that order. Over symbolic rows the clause reads, for each order column, 3 + k columns of its cell (Sym.keyIdx): the value column, the two columns placing a code against its value, and the rank. Read lexicographically with the column's own direction and null placement, they sort the cells as the values they stand for (Sym.leOn_key).

def Sym.keyIdx (k : ℕ) : Fin (3 + k) → Fin (7 + k)

The columns of a cell an order reads: its value, the two columns placing it against its value, and its rank.

Equations

• Sym.keyIdx k = Fin.append ![Sym.iV k, Sym.iSA k, Sym.iSB k] fun (j : Fin k) => Sym.iR j

Order columns on non-null values

The key of a cell

def Sym.keyOf {T : Type} {k : ℕ} (e : Tuple T (7 + k)) : Tuple T (3 + k)

The key of a cell: the columns an order reads.

Equations

• Sym.keyOf e q = e (Sym.keyIdx k q)

@[reducible, inline]

abbrev Sym.q0 (k : ℕ) : Fin (3 + k)

The key column of the value.

Equations

• Sym.q0 k = Fin.castAdd k 0

@[reducible, inline]

abbrev Sym.q1 (k : ℕ) : Fin (3 + k)

The key column placing a code first.

Equations

• Sym.q1 k = Fin.castAdd k 1

@[reducible, inline]

abbrev Sym.q2 (k : ℕ) : Fin (3 + k)

The key column placing a code second.

Equations

• Sym.q2 k = Fin.castAdd k 2

The ranks, read lexicographically

The key read lexicographically

@[reducible, inline]

abbrev Sym.leKey {T : Type} [ValueType T] {k : ℕ} (cl : OrderCol) (X Y : Tuple T (3 + k)) : Bool

The lexicographic reading of two keys with one column direction.

Equations

• Sym.leKey cl X Y = OrderSpec.leOn (fun (x : Fin (3 + k)) => cl) (List.finRange (3 + k)) X Y

The value facts the key rests on

The order of keys is the order of values

A clause over the keys of its columns' cells

def Sym.expandSpec {k p : ℕ} (o : OrderSpec p) : OrderSpec (p * (3 + k))

The clause read over the keys: each of its columns becomes the 3 + k columns of its cell's key, with the column's direction and null placement.

Equations

• Sym.expandSpec o z = o (finProdFinEquiv.symm z).1

def Sym.flatKey {T : Type} {k p : ℕ} (X : Fin p → Tuple T (7 + k)) : Tuple T (p * (3 + k))

The keys of the cells a clause reads, flattened.

Equations

• Sym.flatKey X z = Sym.keyOf (X (finProdFinEquiv.symm z).1) (finProdFinEquiv.symm z).2

def Sym.expandCond {T : Type} {k p : ℕ} : FrameCond T p → FrameCond T (p * (3 + k))

A frame condition read over the keys. An offset bound has no reading there (it moves a value, not a key) and is sent to the whole partition; it is outside the signature the pass works in (FrameCond.noOff).

Equations

• Sym.expandCond FrameCond.whole = FrameCond.whole
• Sym.expandCond (FrameCond.le o) = FrameCond.le (Sym.expandSpec o)
• Sym.expandCond (FrameCond.lt o) = FrameCond.lt (Sym.expandSpec o)
• Sym.expandCond (FrameCond.ge o) = FrameCond.ge (Sym.expandSpec o)
• Sym.expandCond (FrameCond.gt o) = FrameCond.gt (Sym.expandSpec o)
• Sym.expandCond (a.and b) = (Sym.expandCond a).and (Sym.expandCond b)
• Sym.expandCond (a.or b) = (Sym.expandCond a).or (Sym.expandCond b)
• Sym.expandCond (FrameCond.orAll cs) = FrameCond.orAll fun (j : Fin q) => Sym.expandCond (cs j)
• Sym.expandCond (FrameCond.geOff o k_1 pre a) = FrameCond.whole
• Sym.expandCond (FrameCond.leOff o k_1 pre a) = FrameCond.whole

The window over symbolic rows

def Sym.winOIdx {k n p : ℕ} (O : Tuple (Fin n) p) : Tuple (Fin ((k + n) * (7 + k))) (p * (3 + k))

The order columns of a symbolic window: the key columns of the cells the clause reads.

Equations

• Sym.winOIdx O z = Sym.ci (Fin.natAdd k (O (finProdFinEquiv.symm z).1)) (Sym.keyIdx k (finProdFinEquiv.symm z).2)

def Sym.expandFrame {T : Type} {k p : ℕ} (w : ValueFrame T p) : ValueFrame T (p * (3 + k))

The frame expanded over the keys.

Equations

• Sym.expandFrame w = if w.cond.noOff = true then { cond := Sym.expandCond w.cond, self := w.self } else ValueFrame.whole

theorem Sym.isSQL_expandFrame {T : Type} {k p : ℕ} {o : OrderSpec p} {w : ValueFrame T p} (h : ValueFrame.IsSQL o w) : ValueFrame.IsSQL (expandSpec o) (expandFrame w)

def Sym.wOutSA {T : Type} [ValueType T] {k c : ℕ} (n : ℕ) : Fin ((k + (n + 1)) * (7 + k) + 0) → SA T c ((k + n) * (7 + k) + 1)

The cells of a window's row: the input row's cells, then the window's value as a concrete cell.

Equations

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

noncomputable def Sym.winRows {T : Type} [ValueType T] {m p c' n' : ℕ} (P : Tuple (Fin n') m) (O : Tuple (Fin n') p) (o : OrderSpec p) (w : ValueFrame T p) (t : TermIn T c' n') (f : SeqAggFunc T) (keep : Option (Selection T n')) (R : Multiset (Tuple T n')) (γ : Fin c' → T) : Multiset (Tuple T (n' + 1))

The rows a window over an all-regular input emits.

Equations

• Sym.winRows P O o w t f keep R γ = Multiset.map (fun (u : Fin n' → T) => Fin.snoc u (ValueFrame.windowValueOpt P O o w t f keep R u γ)) R

theorem Sym.sliceIs_symWin {T : Type} [ValueType T] {k : ℕ} {C : Finset T} {c n m p : ℕ} (par : Fin k → T) (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) (hw : w.cond.noOff = true) (t : TermIn T (k + c) n) (ht : t.noFun = true) {f : SeqAggFunc T} (hf : f.ReadsCount) (keep : Option (Selection T n)) (hkeep : ∀ (φ : Selection T n), keep = some φ → φ.noFun = true ∧ ∀ a ∈ φ.consts, CG C a) (Q : Multiset (Tuple T ((k + n) * (7 + k)))) (R : Multiset (Tuple T n)) (hR : ∀ v ∈ R, ∀ (i : Fin n), GoodVal par (v i)) (hQ : SliceIs C par Q (Multiset.map (fun (v : Tuple T n) => (v, Fin.elim0)) R)) (γ : Fin c → T) (hcnt : ∀ v ∈ R, CG C (ValueFrame.windowValueOpt P O o w t f keep R v (Fin.append par γ))) : SliceIs C par (Multiset.map (fun (x : Tuple T ((k + n) * (7 + k) + 1)) (y : Fin ((k + (n + 1)) * (7 + k) + 0)) => (wOutSA n y).eval x γ) (winRows (gKeyIdx P) (winOIdx O) (expandSpec o) (expandFrame w) (termV t) f (Option.map (fun (φ : Selection T n) => (transSel 0 φ).toSel) keep) Q γ)) (Multiset.map (fun (v : Tuple T (n + 1)) => (v, Fin.elim0)) (winRows P O o w t f keep R (Fin.append par γ)))

The symbolic window's slice: the encodings of the window's rows, its values being values of the cut.

Home · Documentation · Publications · Contributors · Source · Cite