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 aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvUnop op a₁ => S (nraenv_size a₁)
       | NRAEnvMap aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvMapProduct aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvProduct aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvSelect aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvDefault aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEither aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEitherConcat aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvApp aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvEnv => 1
       | NRAEnvAppEnv aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvMapEnv a₁ => S (nraenv_size a₁)
       | NRAEnvFlatMap aa₂ => S (nraenv_size a₁ + nraenv_size a₂)
       | NRAEnvJoin aaa₃ => S (nraenv_size a₁ + nraenv_size a₂ + nraenv_size a₃)
       | NRAEnvNaturalJoin aa₂ => 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.
Proof.
    induction a; simpl; lia.
  Qed.
  
  Fixpoint nraenv_depth (a:nraenv) : nat :=
    match a with
    | NRAEnvGetConstant _ => 0
    | NRAEnvID => 0
    | NRAEnvConst d => 0
    | NRAEnvBinop op aa₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvUnop op a₁ => nraenv_depth a
    | NRAEnvMap aa₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvMapProduct aa₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvProduct aa₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvSelect aa₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvDefault aa₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEither aa₂=> max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEitherConcat aa₂=> max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvApp aa₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvEnv => 0
    | NRAEnvAppEnv aa₂ => max (nraenv_depth a₁) (nraenv_depth a₂)
    | NRAEnvMapEnv a₁ => (S (nraenv_depth a₁))
    | NRAEnvFlatMap aa₂ => max (S (nraenv_depth a₁)) (nraenv_depth a₂)
    | NRAEnvJoin aaa₃ => max (S (nraenv_depth a₁)) (max (nraenv_depth a₂) (nraenv_depth a₃))
    | NRAEnvNaturalJoin aa₂ => 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.