Module DNNRCBaseSize

Section size.

  Require Import List.
  Require Import Omega.
  Require Import BasicRuntime DNNRCBase.

  Context {fruntime:foreign_runtime}.
  Context {A plug_type:Set}.

  Context (plug_size:plug_type->nat).
  
  Fixpoint dnnrc_size (d:@dnnrc _ A plug_type)
    := match d with
       | DNNRCVar _ _ => 1
       | DNNRCConst _ _ => 1
       | DNNRCBinop _ _ d1 d2 => S (dnnrc_size d1 + dnnrc_size d2)
       | DNNRCUnop _ _ d0 => S (dnnrc_size d0)
       | DNNRCLet _ _ d1 d2 => S (dnnrc_size d1 + dnnrc_size d2)
       | DNNRCFor _ _ d1 d2 => S (dnnrc_size d1 + dnnrc_size d2)
       | DNNRCIf _ d1 d2 d3 => S (dnnrc_size d1 + dnnrc_size d2 + dnnrc_size d3)
       | DNNRCEither _ d1 _ d2 _ d3 => S (dnnrc_size d1 + dnnrc_size d2 + dnnrc_size d3)
       | DNNRCGroupBy _ _ _ d0 => S (dnnrc_size d0)
       | DNNRCCollect _ d0 => S (dnnrc_size d0)
       | DNNRCDispatch _ d0 => S (dnnrc_size d0)
       | DNNRCAlg _ pt sdl => S ( 0)
       end.

  Lemma dnnrc_size_nzero (d:@dnnrc _ A plug_type) : dnnrc_size d <> 0.

End size.