Qcert.DNNRC.Lang.DatasetSize

Section size.


  Context {fruntime:foreign_runtime}.
  Context {ftype: foreign_type}.

  Fixpoint column_size (c:column)
    := match c with
       | CCol _ ⇒ 1
       | CDot _ c0 ⇒ S (column_size c0)
       | CLit _ ⇒ 1
       | CPlus c1 c2 ⇒ S (column_size c1 + column_size c2)
       | CEq c1 c2 ⇒ S (column_size c1 + column_size c2)
       | CLessThan c1 c2 ⇒ S (column_size c1 + column_size c2)
       | CNeg c0 ⇒ S (column_size c0)
       
       | CToString c0 ⇒ S (column_size c0)
       | CSConcat c1 c2 ⇒ S (column_size c1 + column_size c2)
       | CUDFCast _ c0 ⇒ S (column_size c0)
       | CUDFUnbrand _ c0 ⇒ S (column_size c0)
       end.

  Fixpoint dataset_size (d:dataset)
    := match d with
       | DSVar _ ⇒ 1
       | DSSelect scl d0 ⇒ S (
                                (fold_left (fun acc sc ⇒ column_size (snd sc) + acc) scl 0)
                                  + dataset_size d0)
       | DSFilter c0 d0 ⇒ S (column_size c0 + dataset_size d0)
       | DSCartesian d1 d2 ⇒ S (dataset_size d1 + dataset_size d2)
       | DSExplode _ d0 ⇒ S (dataset_size d0)
       end.

  Lemma column_size_nzero (c:column) : column_size c ≠ 0.

    Lemma dataset_size_nzero (d:dataset) : dataset_size d ≠ 0.

End size.