Module cNRAEnvSize

Section cNRAEnvSize.
  Require Import Omega.
  Require Import BasicRuntime.
  Require Import cNRAEnv.

  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_core_size (a:nraenv_core) : nat
    := match a with
         | ANID => 1
         | ANConst d => 1
         | ANBinop op a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANUnop op a₁ => S (nraenv_core_size a₁)
         | ANMap a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANMapConcat a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANProduct a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANSelect a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANDefault a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANEither a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANEitherConcat a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANApp a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANGetConstant _ => 1
         | ANEnv => 1
         | ANAppEnv a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
         | ANMapEnv a₁ => S (nraenv_core_size a₁)
       end.

  Lemma nraenv_core_size_nzero (a:nraenv_core) : nraenv_core_size a <> 0.
  
  Fixpoint nraenv_core_depth (a:nraenv_core) : nat :=
    match a with
    | ANID => 0
    | ANConst d => 0
    | ANBinop op a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANUnop op a₁ => nraenv_core_depth a₁
    | ANMap a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | ANMapConcat a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | ANProduct a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANSelect a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | ANDefault a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANEither a₁ a₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANEitherConcat a₁ a₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANApp a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANGetConstant _ => 0
    | ANEnv => 0
    | ANAppEnv a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | ANMapEnv a₁ => (S (nraenv_core_depth a₁))
    end.

End cNRAEnvSize.