Qcert.NRAEnv.Lang.NRAEnvSize

Section NRAEnvSize.

  Context {fruntime:foreign_runtime}.

  Fixpoint nraenv_size (a:nraenv) : nat
    := match a with
         | 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₂)
         | NRAEnvMapConcat 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₂)
         | NRAEnvGetConstant _ ⇒ 1
         | 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₃)
         | 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
    | 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₂)
    | NRAEnvMapConcat 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₂)
    | NRAEnvGetConstant _ ⇒ 0
    | 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₃))
    | NRAEnvProject _ a₁ ⇒ (nraenv_depth a₁)
    | NRAEnvGroupBy _ _ a₁ ⇒ (nraenv_depth a₁)
    | NRAEnvUnnest _ _ a₁ ⇒ (nraenv_depth a₁)
    end.

End NRAEnvSize.