Module Qcert.cNRAEnv.Lang.cNRAEnvSize


Section cNRAEnvSize.
  Require Import Omega.
  Require Import CommonRuntime.
  Require Import cNRAEnv.

  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_core_size (a:nraenv_core) : nat :=
    match a with
    | cNRAEnvID => 1
    | cNRAEnvConst d => 1
    | cNRAEnvBinop op aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvUnop op a₁ => S (nraenv_core_size a₁)
    | cNRAEnvMap aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvMapProduct aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvProduct aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvSelect aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvDefault aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvEither aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvEitherConcat aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvApp aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvGetConstant _ => 1
    | cNRAEnvEnv => 1
    | cNRAEnvAppEnv aa₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvMapEnv a₁ => S (nraenv_core_size a₁)
    end.

  Lemma nraenv_core_size_nzero (a:nraenv_core) : nraenv_core_size a <> 0.
Proof.
    induction a; simpl; omega.
  Qed.
  
  Fixpoint nraenv_core_depth (a:nraenv_core) : nat :=
    match a with
    | cNRAEnvID => 0
    | cNRAEnvConst d => 0
    | cNRAEnvBinop op aa₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvUnop op a₁ => nraenv_core_depth a
    | cNRAEnvMap aa₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvMapProduct aa₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvProduct aa₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvSelect aa₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvDefault aa₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvEither aa₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvEitherConcat aa₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvApp aa₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvGetConstant _ => 0
    | cNRAEnvEnv => 0
    | cNRAEnvAppEnv aa₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvMapEnv a₁ => (S (nraenv_core_depth a₁))
    end.

End cNRAEnvSize.