Module Qcert.NRAEnv.Lang.NRAEnvIgnore

Require Import Bool.
Require Import List.
Require Import String.
Require Import Utils.
Require Import DataRuntime.
Require Import cNRAEnvIgnore.
Require Import NRAEnv.

Section NRAEnvIgnore.

  Local Open Scope nraenv_scope.
  

  Context {fruntime:foreign_runtime}.

  Fixpoint is_nra (e:nraenv) : Prop :=
    match e with
    | NRAEnvGetConstant _ => False
    | NRAEnvID => True
    | NRAEnvConst rd => True
    | NRAEnvBinop bop e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvUnop uop e1 => is_nra e1
    | NRAEnvMap e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvMapProduct e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvProduct e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvSelect e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvDefault e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvEither e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvEitherConcat e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvApp e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvEnv => False
    | NRAEnvAppEnv e1 e2 => False
    | NRAEnvMapEnv e1 => False
    | NRAEnvFlatMap e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvJoin e1 e2 e3 => (is_nra e1) /\ (is_nra e2) /\ (is_nra e3)
    | NRAEnvNaturalJoin e1 e2 => (is_nra e1) /\ (is_nra e2)
    | NRAEnvProject _ e1 => (is_nra e1)
    | NRAEnvGroupBy _ _ e1 => (is_nra e1)
    | NRAEnvUnnest _ _ e1 => (is_nra e1)
    end.

  Fixpoint is_nra_fun (e:nraenv) : bool :=
    match e with
    | NRAEnvGetConstant _ => false
    | NRAEnvID => true
    | NRAEnvConst rd => true
    | NRAEnvBinop bop e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvUnop uop e1 => is_nra_fun e1
    | NRAEnvMap e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvMapProduct e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvProduct e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvSelect e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvDefault e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvEither e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvEitherConcat e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvApp e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvEnv => false
    | NRAEnvAppEnv e1 e2 => false
    | NRAEnvMapEnv e1 => false
    | NRAEnvFlatMap e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvJoin e1 e2 e3 => andb (is_nra_fun e1) (andb (is_nra_fun e2) (is_nra_fun e3))
    | NRAEnvNaturalJoin e1 e2 => andb (is_nra_fun e1) (is_nra_fun e2)
    | NRAEnvProject _ e1 => (is_nra_fun e1)
    | NRAEnvGroupBy _ _ e1 => (is_nra_fun e1)
    | NRAEnvUnnest _ _ e1 => (is_nra_fun e1)
    end.

  Lemma is_nra_eq (e:nraenv):
    is_nra e <-> (is_nra_fun e = true).

  Fixpoint nraenv_ignores_env (e:nraenv) : Prop :=
    match e with
    | NRAEnvGetConstant _ => True
    | NRAEnvID => True
    | NRAEnvConst rd => True
    | NRAEnvBinop bop e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvUnop uop e1 => nraenv_ignores_env e1
    | NRAEnvMap e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvMapProduct e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvProduct e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvSelect e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvDefault e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvEither e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvEitherConcat e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvApp e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvEnv => False
    | NRAEnvAppEnv e1 e2 => (nraenv_ignores_env e2)
    | NRAEnvMapEnv e1 => False
    | NRAEnvFlatMap e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvJoin e1 e2 e3 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2) /\ (nraenv_ignores_env e3)
    | NRAEnvNaturalJoin e1 e2 => (nraenv_ignores_env e1) /\ (nraenv_ignores_env e2)
    | NRAEnvProject _ e1 => (nraenv_ignores_env e1)
    | NRAEnvGroupBy _ _ e1 => (nraenv_ignores_env e1)
    | NRAEnvUnnest _ _ e1 => (nraenv_ignores_env e1)
    end.

  Fixpoint nraenv_ignores_env_fun (e:nraenv) : bool :=
    match e with
    | NRAEnvGetConstant _ => true
    | NRAEnvID => true
    | NRAEnvConst rd => true
    | NRAEnvBinop bop e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvUnop uop e1 => nraenv_ignores_env_fun e1
    | NRAEnvMap e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvMapProduct e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvProduct e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvSelect e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvDefault e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvEither e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvEitherConcat e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvApp e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvEnv => false
    | NRAEnvAppEnv e1 e2 => (nraenv_ignores_env_fun e2)
    | NRAEnvMapEnv e1 => false
    | NRAEnvFlatMap e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvJoin e1 e2 e3 => andb (nraenv_ignores_env_fun e1) (andb (nraenv_ignores_env_fun e2) (nraenv_ignores_env_fun e3))
    | NRAEnvNaturalJoin e1 e2 => andb (nraenv_ignores_env_fun e1) (nraenv_ignores_env_fun e2)
    | NRAEnvProject _ e1 => (nraenv_ignores_env_fun e1)
    | NRAEnvGroupBy _ _ e1 => (nraenv_ignores_env_fun e1)
    | NRAEnvUnnest _ _ e1 => (nraenv_ignores_env_fun e1)
    end.

  Lemma nraenv_ignores_env_eq (e:nraenv):
    nraenv_ignores_env e <-> (nraenv_ignores_env_fun e = true).


  Fixpoint fixed_env (e:nraenv) : Prop :=
    match e with
      | NRAEnvID => True
      | NRAEnvConst rd => True
      | NRAEnvBinop bop e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvUnop uop e1 => fixed_env e1
      | NRAEnvMap e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvMapProduct e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvProduct e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvSelect e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvDefault e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvEither e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvEitherConcat e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvApp e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvGetConstant _ => True
      | NRAEnvEnv => True
      | NRAEnvAppEnv e1 e2 => False
      | NRAEnvMapEnv e1 => False
      | NRAEnvFlatMap e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvJoin e1 e2 e3 => (fixed_env e1) /\ (fixed_env e2) /\ (fixed_env e3)
      | NRAEnvNaturalJoin e1 e2 => (fixed_env e1) /\ (fixed_env e2)
      | NRAEnvProject _ e1 => (fixed_env e1)
      | NRAEnvGroupBy _ _ e1 => (fixed_env e1)
      | NRAEnvUnnest _ _ e1 => (fixed_env e1)
    end.

  Fixpoint fixed_env_fun (e:nraenv) : bool :=
    match e with
      | NRAEnvID => true
      | NRAEnvConst rd => true
      | NRAEnvBinop bop e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvUnop uop e1 => fixed_env_fun e1
      | NRAEnvMap e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvMapProduct e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvProduct e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvSelect e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvDefault e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvEither e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvEitherConcat e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvApp e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvGetConstant _ => true
      | NRAEnvEnv => true
      | NRAEnvAppEnv e1 e2 => false
      | NRAEnvMapEnv e1 => false
      | NRAEnvFlatMap e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvJoin e1 e2 e3 => andb (fixed_env_fun e1) (andb (fixed_env_fun e2) (fixed_env_fun e3))
      | NRAEnvNaturalJoin e1 e2 => andb (fixed_env_fun e1) (fixed_env_fun e2)
      | NRAEnvProject _ e1 => (fixed_env_fun e1)
      | NRAEnvGroupBy _ _ e1 => (fixed_env_fun e1)
      | NRAEnvUnnest _ _ e1 => (fixed_env_fun e1)
    end.

  Lemma fixed_env_eq (e:nraenv):
    fixed_env e <-> (fixed_env_fun e = true).

  
  Fixpoint nraenv_ignores_id (e:nraenv) : Prop :=
    match e with
      | NRAEnvID => False
      | NRAEnvConst rd => True
      | NRAEnvBinop bop e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvUnop uop e1 => nraenv_ignores_id e1
      | NRAEnvMap e1 e2 => nraenv_ignores_id e2
      | NRAEnvMapProduct e1 e2 => nraenv_ignores_id e2
      | NRAEnvProduct e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvSelect e1 e2 => (nraenv_ignores_id e2)
      | NRAEnvDefault e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvEither e1 e2 => False
      | NRAEnvEitherConcat e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvApp e1 e2 => (nraenv_ignores_id e2)
      | NRAEnvGetConstant _ => True
      | NRAEnvEnv => True
      | NRAEnvAppEnv e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvMapEnv e1 => (nraenv_ignores_id e1)
      | NRAEnvFlatMap e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvJoin e1 e2 e3 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2) /\ (nraenv_ignores_id e3)
      | NRAEnvNaturalJoin e1 e2 => (nraenv_ignores_id e1) /\ (nraenv_ignores_id e2)
      | NRAEnvProject _ e1 => (nraenv_ignores_id e1)
      | NRAEnvGroupBy _ _ e1 => (nraenv_ignores_id e1)
      | NRAEnvUnnest _ _ e1 => (nraenv_ignores_id e1)
    end.

  Fixpoint nraenv_ignores_id_fun (e:nraenv) : bool :=
    match e with
      | NRAEnvID => false
      | NRAEnvConst rd => true
      | NRAEnvBinop bop e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvUnop uop e1 => nraenv_ignores_id_fun e1
      | NRAEnvMap e1 e2 => nraenv_ignores_id_fun e2
      | NRAEnvMapProduct e1 e2 => nraenv_ignores_id_fun e2
      | NRAEnvProduct e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvSelect e1 e2 => (nraenv_ignores_id_fun e2)
      | NRAEnvDefault e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvEither e1 e2 => false
      | NRAEnvEitherConcat e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvApp e1 e2 => (nraenv_ignores_id_fun e2)
      | NRAEnvGetConstant _ => true
      | NRAEnvEnv => true
      | NRAEnvAppEnv e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvMapEnv e1 => (nraenv_ignores_id_fun e1)
      | NRAEnvFlatMap e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvJoin e1 e2 e3 => andb (nraenv_ignores_id_fun e1) (andb (nraenv_ignores_id_fun e2) (nraenv_ignores_id_fun e3))
      | NRAEnvNaturalJoin e1 e2 => andb (nraenv_ignores_id_fun e1) (nraenv_ignores_id_fun e2)
      | NRAEnvProject _ e1 => (nraenv_ignores_id_fun e1)
      | NRAEnvGroupBy _ _ e1 => (nraenv_ignores_id_fun e1)
      | NRAEnvUnnest _ _ e1 => (nraenv_ignores_id_fun e1)
    end.

  Lemma nraenv_ignores_id_eq (e:nraenv):
    nraenv_ignores_id e <-> (nraenv_ignores_id_fun e = true).

  Lemma nraenv_ignores_env_nraenv_core_eq (e:nraenv) :
    nraenv_ignores_env e ->
    nraenv_core_ignores_env (nraenv_to_nraenv_core e).
  
  Lemma nraenv_ignores_env_swap (e:nraenv) :
    nraenv_ignores_env e -> forall (h:list (string*string)) c,
                               forall (env1 env2:data), forall x:data,
                       h ⊢ e @ₓ x ⊣ c;env1 = h ⊢ e @ₓ x ⊣ c;env2.
  
  Lemma nraenv_ignores_id_nraenv_core_eq (e:nraenv) :
    nraenv_ignores_id e ->
    nraenv_core_ignores_id (nraenv_to_nraenv_core e).
  
  Lemma nraenv_ignores_id_swap (e:nraenv) :
    nraenv_ignores_id e -> forall h:list (string*string), forall c,
      forall env:data, forall x1 x2:data,
          h ⊢ e @ₓ x1 ⊣ c;env = h ⊢ e @ₓ x2 ⊣ c;env.

End NRAEnvIgnore.