Qcert.CAMP.Lang.CAMPSize

Section CAMPSize.

  Context {fruntime:foreign_runtime}.

  Fixpoint pat_size (p:pat) : nat
    := match p with
         | pconst d' ⇒ 1
         | punop op p₁ ⇒ S (pat_size p₁)
         | pbinop op p₁ p₂ ⇒ S (pat_size p₁ + pat_size p₂)
         | pmap p₁ ⇒ S (pat_size p₁)

         | passert p₁ ⇒ S (pat_size p₁)
         | porElse p₁ p₂ ⇒ S (pat_size p₁ + pat_size p₂)
         | pit ⇒ 1
         | pletIt p₁ p₂ ⇒ S (pat_size p₁ + pat_size p₂)
         | pgetconstant _ ⇒ 1
         | penv ⇒ 1
         | pletEnv p₁ p₂ ⇒ S (pat_size p₁ + pat_size p₂)
         | pleft ⇒ 1
         | pright ⇒ 1
       end.

  Lemma pat_size_nzero (a:pat) : pat_size a ≠ 0.

End CAMPSize.