Module Qcert.cNRAEnv.Lang.cNRAEnvSize

Require Import Lia.
Require Import DataRuntime.
Require Import cNRAEnv.

Section cNRAEnvSize.
  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_core_size (a:nraenv_core) : nat :=
    match a with
    | cNRAEnvID => 1
    | cNRAEnvConst d => 1
    | cNRAEnvBinop op a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvUnop op a₁ => S (nraenv_core_size a₁)
    | cNRAEnvMap a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvMapProduct a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvProduct a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvSelect a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvDefault a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvEither a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvEitherConcat a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvApp a₁ a₂ => S (nraenv_core_size a₁ + nraenv_core_size a₂)
    | cNRAEnvGetConstant _ => 1
    | cNRAEnvEnv => 1
    | cNRAEnvAppEnv a₁ a₂ => 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.
  
  Fixpoint nraenv_core_depth (a:nraenv_core) : nat :=
    match a with
    | cNRAEnvID => 0
    | cNRAEnvConst d => 0
    | cNRAEnvBinop op a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvUnop op a₁ => nraenv_core_depth a₁
    | cNRAEnvMap a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvMapProduct a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvProduct a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvSelect a₁ a₂ => max (S (nraenv_core_depth a₁)) (nraenv_core_depth a₂)
    | cNRAEnvDefault a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvEither a₁ a₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvEitherConcat a₁ a₂=> max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvApp a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvGetConstant _ => 0
    | cNRAEnvEnv => 0
    | cNRAEnvAppEnv a₁ a₂ => max (nraenv_core_depth a₁) (nraenv_core_depth a₂)
    | cNRAEnvMapEnv a₁ => (S (nraenv_core_depth a₁))
    end.

End cNRAEnvSize.