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.

End size.