Documentation

Provenance.WinKept

A window kept as a window over an all-regular input #

A pass that re-types every node to regular columns meets a window over an input holding aggregate columns. The window reads the regular columns of each row and nothing of the aggregate ones (ColKind.readTuple), its partition, its order, its term, its clause and the tie-break of its peers all seeing the nulled row; so the window over the re-typed input, which reads every column, is a different query – two peers that agree on their regular columns are ordered by their aggregate values there, which an order-dependent aggregate reads. The window is kept by doubling the input instead: each row is prefixed by its nulled copy, the window is written over the first block, and the first block is projected away afterwards. Peers that agree on the nulled row are then listed in an order the window cannot tell apart, the values it reads being read off the first block, and AggQueryIn.evaluatePlain_winKept is the equality.

A term over a longer row, reading its first block #

source
def TermIn.widen {T : Type} (n' : ℕ) {c k : ℕ} :
TermIn T c k → TermIn T c (k + n')

A term widened to a row with n' more columns on the right.

Equations
Instances For
    Dependency graph
    source
    def BoolTerm.widen {T : Type} (n' : ℕ) {k : ℕ} :
    BoolTerm T k → BoolTerm T (k + n')

    A comparison widened.

    Equations
    Instances For
      Dependency graph
      source
      def Selection.widen {T : Type} (n' : ℕ) {k : ℕ} :
      Selection T k → Selection T (k + n')

      A selection widened.

      Equations
      Instances For
        Dependency graph

        The two blocks of a doubled row #

        source
        def AggQueryIn.blockL {T : Type} (n : ℕ) (x : Tuple T (n + n)) :
        Tuple T n

        The first block of a doubled row.

        Equations
        Instances For
          Dependency graph
          source
          def AggQueryIn.blockR {T : Type} (n : ℕ) (x : Tuple T (n + n)) :
          Tuple T n

          Its second block.

          Equations
          Instances For
            Dependency graph
            source
            def AggQueryIn.castCols (n : ℕ) {m : ℕ} (P : Tuple (Fin n) m) :
            Tuple (Fin (n + n)) m

            Columns of the first block.

            Equations
            Instances For
              Dependency graph

              The frame and the window value read off the first block #

              The window, kept #

              source
              theorem AggQueryIn.doubled_kinds {T : Type} [ValueType T] {c : ℕ} (n : ℕ) (κ : Fin n → ColKind) :
              (fun (j : Fin (n + n)) => (Fin.append (nullCols κ) (fun (i : Fin n) => ProjColIn.term (TermGIn.index i ⋯)) j).kind) = ColKind.allReg (n + n)
              Dependency graph
              source
              def AggQueryIn.doubled {T : Type} [ValueType T] {c n : ℕ} (κ : Fin n → ColKind) (q : AggQueryIn T c n (ColKind.allReg n)) :
              AggQueryIn T c (n + n) (ColKind.allReg (n + n))

              The doubled input: each row prefixed by its nulled copy, the aggregate columns read as 0 as the window reads them.

              Equations
              Instances For
                Dependency graph
                source
                def AggQueryIn.keptCols {T : Type} {c : ℕ} (n : ℕ) :
                Tuple (ProjColIn T c (Fin.snoc (ColKind.allReg (n + n)) ColKind.agg)) (n + 1)

                The columns kept after the window: the second block and the window's column.

                Equations
                Instances For
                  Dependency graph
                  source
                  theorem AggQueryIn.keptCols_kinds {T : Type} {c : ℕ} (n : ℕ) :
                  (fun (j : Fin (n + 1)) => (keptCols n j).kind) = Fin.snoc (ColKind.allReg n) ColKind.agg
                  Dependency graph
                  source
                  def AggQueryIn.winKept {T : Type} [ValueType T] {c n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : TermIn T c n) (f : SeqAggFunc T) (κ : Fin n → ColKind) (q : AggQueryIn T c n (ColKind.allReg n)) (dist : Bool) (keep : Option (Selection T n)) :
                  AggQueryIn T c (n + 1) (Fin.snoc (ColKind.allReg n) ColKind.agg)

                  A window over an input of any kinds, written over an all-regular input computing the same rows: the window over the doubled input, reading its first block – partition, order, term and clause moved there – and the first block then dropped.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Dependency graph
                    source
                    theorem AggQueryIn.evaluatePlain_winKept {T : Type} [ValueType T] {c lab : ℕ} {rd : Fin c → Bool} {n m p : ℕ} (P : Tuple (Fin n) m) (O : Tuple (Fin n) p) (o : OrderSpec p) (w : ValueFrame T p) {hsql : ValueFrame.IsSQL o w} (t : TermIn T c n) (f : SeqAggFunc T) {κ : Fin n → ColKind} (q₀ : AggQueryIn T c n κ) (hrr : WinReadsReg κ P O t) (q : AggQueryIn T c n (ColKind.allReg n)) (dist : Bool) (keep : Option (Selection T n)) (D : Database T) (γ : Fin c → T) (hq : q₀.evaluatePlain D γ = q.evaluatePlain D γ) :
                    (winKept P O o w t f κ q dist keep).evaluatePlain D γ = (Win P O o w t f q₀ hrr dist keep).evaluatePlain D γ

                    It computes the window, whatever the kinds of the input it stands for, as long as the rows agree.

                    Dependency graph

                    What the kept window is made of #