Module Qcert.CAMP.Lang.CAMPSize


Section CAMPSize.
  Require Import Omega.
  Require Import CommonRuntime.
  Require Import 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 pp₂ => S (camp_size p₁ + camp_size p₂)
         | pmap p₁ => S (camp_size p₁)
         | passert p₁ => S (camp_size p₁)
         | porElse pp₂ => S (camp_size p₁ + camp_size p₂)
         | pit => 1
         | pletIt pp₂ => S (camp_size p₁ + camp_size p₂)
         | pgetConstant _ => 1
         | penv => 1
         | pletEnv pp₂ => S (camp_size p₁ + camp_size p₂)
         | pleft => 1
         | pright => 1
       end.

  Lemma camp_size_nzero (a:camp) : camp_size a <> 0.
Proof.
    induction a; simpl; omega.
  Qed.

End CAMPSize.