Module NRASize

Section NRASize.
  Require Import Omega.
  Require Import BasicRuntime NRA.

  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₂)
    | AGetConstant s => 1
    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₂)
    | AGetConstant s => 0
    end.

End NRASize.