Module DataframeSize
Section
DataframeSize
.
Require
Import
List
.
Require
Import
Omega
.
Require
Import
BasicSystem
.
Require
Import
Dataframe
.
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.
Proof.
induction
c
;
simpl
;
omega
.
Qed.
Lemma
dataframe_size_nzero
(
d
:
dataframe
) :
dataframe_size
d
<> 0.
Proof.
induction
d
;
simpl
;
omega
.
Qed.
End
DataframeSize
.