Qcert.NRA.Lang.NRASize

Section NRASize.

  Context {fruntime:foreign_runtime}.

  Fixpoint nra_size (a:nra) : nat :=
    match a with
    | AID ⇒ 1
    | AConst d ⇒ 1
    | ABinop op a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | AUnop op a₁ ⇒ S (nra_size a₁)
    | AMap a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | AMapConcat a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | AProduct a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | ASelect a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | ADefault a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | AEither a₁ a₂⇒ S (nra_size a₁ + nra_size a₂)
    | AEitherConcat a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    | AApp a₁ a₂ ⇒ S (nra_size a₁ + nra_size a₂)
    end.

  Lemma nra_size_nzero (a:nra) : nra_size a ≠ 0.

  Fixpoint nra_depth (a:nra) : nat :=
    
    match a with
    | AID ⇒ 0
    | AConst d ⇒ 0
    | ABinop op a₁ a₂ ⇒ max (nra_depth a₁) (nra_depth a₂)
    | AUnop op a₁ ⇒ nra_depth a₁
    | AMap a₁ a₂ ⇒ max (S (nra_depth a₁)) (nra_depth a₂)
    | AMapConcat a₁ a₂ ⇒ max (S (nra_depth a₁)) (nra_depth a₂)
    | AProduct a₁ a₂ ⇒ max (nra_depth a₁) (nra_depth a₂)
    | ASelect a₁ a₂ ⇒ max (S (nra_depth a₁)) (nra_depth a₂)
    | ADefault a₁ a₂ ⇒ max (nra_depth a₁) (nra_depth a₂)
    | AEither a₁ a₂⇒ max (nra_depth a₁) (nra_depth a₂)
    | AEitherConcat a₁ a₂ ⇒ max (nra_depth a₁) (nra_depth a₂)
    | AApp a₁ a₂ ⇒ max (nra_depth a₁) (nra_depth a₂)
    end.

End NRASize.