Module Qcert.NRAEnv.Lang.NRAEnvSize

Require Import Lia.
Require Import DataRuntime.
Require Import NRAEnv.

Section NRAEnvSize.
  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_size (a:nraenv) : nat
    := match a with
       | NRAEnvGetConstant _ => 1
       | NRAEnvID => 1
       | NRAEnvConst d => 1
       | NRAEnvBinop op a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvUnop op a₁ => S (nraenv_size a₁)
       | NRAEnvMap a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvMapProduct a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvProduct a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvSelect a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvDefault a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEither a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEitherConcat a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvApp a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEnv => 1
       | NRAEnvAppEnv a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvMapEnv a₁ => S (nraenv_size a₁)
       | NRAEnvFlatMap a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvJoin a₁ a₂ a₃ => S (nraenv_size a₁ + nraenv_size a₂ + nraenv_size a₃)
       | NRAEnvNaturalJoin a₁ a₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvProject _ a₁ => S (nraenv_size a₁)
       | NRAEnvGroupBy _ _ a₁ => S (nraenv_size a₁)
       | NRAEnvUnnest _ _ a₁ => S (nraenv_size a₁)
       end.

  Lemma nraenv_size_nzero (a:nraenv) : nraenv_size a <> 0.
  
  Fixpoint nraenv_depth (a:nraenv) : nat :=
    match a with
    | NRAEnvGetConstant _ => 0
    | NRAEnvID => 0
    | NRAEnvConst d => 0
    | NRAEnvBinop op a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvUnop op a₁ => nraenv_depth a₁
    | NRAEnvMap a₁ a₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvMapProduct a₁ a₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvProduct a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvSelect a₁ a₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvDefault a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEither a₁ a₂=> max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEitherConcat a₁ a₂=> max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvApp a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEnv => 0
    | NRAEnvAppEnv a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvMapEnv a₁ => (S (nraenv_depth a₁))
    | NRAEnvFlatMap a₁ a₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvJoin a₁ a₂ a₃ => max (S (nraenv_depth a₁)) (max (nraenv_depth a₂) (nraenv_depth a₃))
    | NRAEnvNaturalJoin a₁ a₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvProject _ a₁ => (nraenv_depth a₁)
    | NRAEnvGroupBy _ _ a₁ => (nraenv_depth a₁)
    | NRAEnvUnnest _ _ a₁ => (nraenv_depth a₁)
    end.

End NRAEnvSize.