Module Qcert.Dataframe.Lang.DataframeSize

Require Import List.
Require Import Lia.
Require Import DataSystem.
Require Import Dataframe.

Section DataframeSize.
  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 dataframe_size (d:dataframe)
    := match d with
       | DSVar _ => 1
       | DSSelect scl d0 => S (
                                (fold_left (fun acc sc => column_size (snd sc) + acc) scl 0)
                                  + dataframe_size d0)
       | DSFilter c0 d0 => S (column_size c0 + dataframe_size d0)
       | DSCartesian d1 d2 => S (dataframe_size d1 + dataframe_size d2)
       | DSExplode _ d0 => S (dataframe_size d0)
       end.


  Lemma column_size_nzero (c:column) : column_size c <> 0.

    Lemma dataframe_size_nzero (d:dataframe) : dataframe_size d <> 0.

End DataframeSize.