Module Qcert.DNNRC.Lang.DNNRCBaseSize
Require
Import
List
.
Require
Import
Lia
.
Require
Import
DataRuntime
.
Require
Import
DNNRCBase
.
Section
size
.
Context
{
fruntime
:
foreign_runtime
}.
Context
{
A
plug_type
:
Set
}.
Context
(
plug_size
:
plug_type
->
nat
).
Fixpoint
dnnrc_base_size
(
d
:@
dnnrc_base
_
A
plug_type
)
:=
match
d
with
|
DNNRCGetConstant
_
_
=> 1
|
DNNRCVar
_
_
=> 1
|
DNNRCConst
_
_
=> 1
|
DNNRCBinop
_
_
d1
d2
=>
S
(
dnnrc_base_size
d1
+
dnnrc_base_size
d2
)
|
DNNRCUnop
_
_
d0
=>
S
(
dnnrc_base_size
d0
)
|
DNNRCLet
_
_
d1
d2
=>
S
(
dnnrc_base_size
d1
+
dnnrc_base_size
d2
)
|
DNNRCFor
_
_
d1
d2
=>
S
(
dnnrc_base_size
d1
+
dnnrc_base_size
d2
)
|
DNNRCIf
_
d1
d2
d3
=>
S
(
dnnrc_base_size
d1
+
dnnrc_base_size
d2
+
dnnrc_base_size
d3
)
|
DNNRCEither
_
d1
_
d2
_
d3
=>
S
(
dnnrc_base_size
d1
+
dnnrc_base_size
d2
+
dnnrc_base_size
d3
)
|
DNNRCGroupBy
_
_
_
d0
=>
S
(
dnnrc_base_size
d0
)
|
DNNRCCollect
_
d0
=>
S
(
dnnrc_base_size
d0
)
|
DNNRCDispatch
_
d0
=>
S
(
dnnrc_base_size
d0
)
|
DNNRCAlg
_
pt
sdl
=>
S
( 0)
end
.
Lemma
dnnrc_base_size_nzero
(
d
:@
dnnrc_base
_
A
plug_type
) :
dnnrc_base_size
d
<> 0.
Proof.
induction
d
;
simpl
;
lia
.
Qed.
End
size
.