Module CAMPSize

Section CAMPSize.
  Require Import Omega.
  Require Import BasicRuntime CAMP.

  Context {fruntime:foreign_runtime}.

  Fixpoint camp_size (p:camp) : nat
    := match p with
         | pconst d' => 1
         | punop op p₁ => S (camp_size p₁)
         | pbinop op p₁ p₂ => S (camp_size p₁ + camp_size p₂)
         | pmap p₁ => S (camp_size p₁)
         | passert p₁ => S (camp_size p₁)
         | porElse p₁ p₂ => S (camp_size p₁ + camp_size p₂)
         | pit => 1
         | pletIt p₁ p₂ => S (camp_size p₁ + camp_size p₂)
         | pgetConstant _ => 1
         | penv => 1
         | pletEnv p₁ p₂ => S (camp_size p₁ + camp_size p₂)
         | pleft => 1
         | pright => 1
       end.

  Lemma camp_size_nzero (a:camp) : camp_size a <> 0.

End CAMPSize.