def
Filter.evalDecidableAnnotated
{T : Type}
[ValueType T]
{K : Type}
{n : ℕ}
(φ : Filter T n)
:
DecidablePred fun (ta : AnnotatedTuple T K n) => φ.eval ta.1
Equations
- φ.evalDecidableAnnotated t = match φ.evalDecidable t.1 with | isTrue h => isTrue h | isFalse h => isFalse ⋯
Instances For
def
groupByKey
{T : Type}
[ValueType T]
{K : Type}
[SemiringWithMonus K]
[DecidableEq K]
{n : ℕ}
(m : Multiset (Tuple T n × K))
:
Equations
Instances For
def
Query.evaluateAnnotated
{T : Type}
[ValueType T]
{K : Type}
[SemiringWithMonus K]
[DecidableEq K]
{n : ℕ}
(q : Query T n)
(hq : q.noAgg)
(d : AnnotatedDatabase T K)
:
AnnotatedRelation T K n
Equations
- One or more equations did not get rendered due to their size.
- (Query.Rel n s).evaluateAnnotated hq_2 d = match h : AnnotatedDatabase.find n s d with | none => ∅ | some rn => rn
- (Π ts q').evaluateAnnotated hq_2 d = Multiset.map (fun (t : AnnotatedTuple T K n_2) => (fun (k : Fin n) => (ts k).eval t.1, t.2)) (q'.evaluateAnnotated ⋯ d)
- (σ φ q_2).evaluateAnnotated hq_2 d = Multiset.filter (fun (ta : AnnotatedTuple T K n) => φ.eval ta.1) (q_2.evaluateAnnotated ⋯ d)
- (q₁ ⊎ q₂).evaluateAnnotated hq_2 d = q₁.evaluateAnnotated ⋯ d + q₂.evaluateAnnotated ⋯ d
- (ε q_2).evaluateAnnotated hq_2 d = ↑↑(groupByKey (q_2.evaluateAnnotated ⋯ d))
- (Query.Agg a a_1 a_2 a_3).evaluateAnnotated hq_2 d = ⋯.elim