Module Qcert.NNRSimp.Lang.NNRSimpVars

Require Import String.
Require Import List.
Require Import Permutation.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Arith.
Require Import Max.
Require Import Bool.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Decidable.

Require Import Utils.
Require Import DataRuntime.
Require Import NNRSimp.

Section NNRSimpVars.

  Context {fruntime:foreign_runtime}.
  Context (h:brand_relation_t).
  
  Fixpoint nnrs_imp_expr_free_vars (e:nnrs_imp_expr) : list var
    := match e with
       | NNRSimpGetConstant _ => nil
       | NNRSimpVar v => v :: nil
       | NNRSimpConst _ => nil
       | NNRSimpBinop _ e₁ e₂ => nnrs_imp_expr_free_vars e₁ ++ nnrs_imp_expr_free_vars e₂
       | NNRSimpUnop _ e₁ => nnrs_imp_expr_free_vars e₁
       | NNRSimpGroupBy _ _ e₁ => nnrs_imp_expr_free_vars e₁
       end.

  Fixpoint nnrs_imp_stmt_free_vars (s:nnrs_imp_stmt) : list var
    := match s with
       | NNRSimpSkip => nil
       | NNRSimpSeq s₁ s₂ =>
         nnrs_imp_stmt_free_vars s₁ ++ nnrs_imp_stmt_free_vars s₂
       | NNRSimpAssign v e =>
         v::(nnrs_imp_expr_free_vars e)
       | NNRSimpLet v eo s₀ =>
         match eo with
         | Some e => nnrs_imp_expr_free_vars e
         | None => nil
         end ++ remove string_eqdec v (nnrs_imp_stmt_free_vars s₀)
       | NNRSimpFor v e s₀ =>
         nnrs_imp_expr_free_vars e ++ remove string_eqdec v (nnrs_imp_stmt_free_vars s₀)
       | NNRSimpIf e s₁ s₂ =>
         nnrs_imp_expr_free_vars e ++ nnrs_imp_stmt_free_vars s₁ ++ nnrs_imp_stmt_free_vars s₂
       | NNRSimpEither e x₁ s₁ x₂ s₂ =>
         nnrs_imp_expr_free_vars e ++ remove string_eqdec x₁ (nnrs_imp_stmt_free_vars s₁) ++ remove string_eqdec x₂ (nnrs_imp_stmt_free_vars s₂)
       end.

  Fixpoint nnrs_imp_stmt_bound_vars (s:nnrs_imp_stmt) : list var
    := match s with
       | NNRSimpSkip => nil
       | NNRSimpSeq s₁ s₂ =>
         nnrs_imp_stmt_bound_vars s₁ ++ nnrs_imp_stmt_bound_vars s₂
       | NNRSimpAssign v e =>
         nil
       | NNRSimpLet v eo s₀ =>
         v::(nnrs_imp_stmt_bound_vars s₀)
       | NNRSimpFor v e s₀ =>
         v::(nnrs_imp_stmt_bound_vars s₀)
       | NNRSimpIf e s₁ s₂ =>
         nnrs_imp_stmt_bound_vars s₁ ++ nnrs_imp_stmt_bound_vars s₂
       | NNRSimpEither e x₁ s₁ x₂ s₂ =>
         x₁::(nnrs_imp_stmt_bound_vars s₁) ++ x₂::(nnrs_imp_stmt_bound_vars s₂)
       end.

  Fixpoint nnrs_imp_stmt_mayberead_vars (s:nnrs_imp_stmt) : list var
    := match s with
       | NNRSimpSkip => nil
       | NNRSimpSeq s₁ s₂ =>
         nnrs_imp_stmt_mayberead_vars s₁ ++ nnrs_imp_stmt_mayberead_vars s₂
       | NNRSimpAssign v e =>
         nnrs_imp_expr_free_vars e
       | NNRSimpLet v eo s₀ =>
         match eo with
         | Some e => nnrs_imp_expr_free_vars e
         | None => nil
         end ++ remove string_eqdec v (nnrs_imp_stmt_mayberead_vars s₀)
       | NNRSimpFor v e s₀ =>
         nnrs_imp_expr_free_vars e ++ remove string_eqdec v (nnrs_imp_stmt_mayberead_vars s₀)
       | NNRSimpIf e s₁ s₂ =>
         nnrs_imp_expr_free_vars e ++ nnrs_imp_stmt_mayberead_vars s₁ ++ nnrs_imp_stmt_mayberead_vars s₂
       | NNRSimpEither e x₁ s₁ x₂ s₂ =>
         nnrs_imp_expr_free_vars e ++ remove string_eqdec x₁ (nnrs_imp_stmt_mayberead_vars s₁) ++ remove string_eqdec x₂ (nnrs_imp_stmt_mayberead_vars s₂)
       end.

    Fixpoint nnrs_imp_stmt_maybewritten_vars (s:nnrs_imp_stmt) : list var
    := match s with
       | NNRSimpSkip => nil
       | NNRSimpSeq s₁ s₂ =>
         nnrs_imp_stmt_maybewritten_vars s₁ ++ nnrs_imp_stmt_maybewritten_vars s₂
       | NNRSimpAssign v e =>
         v::nil
       | NNRSimpLet v eo s₀ =>
         remove string_eqdec v (nnrs_imp_stmt_maybewritten_vars s₀)
       | NNRSimpFor v e s₀ =>
         remove string_eqdec v (nnrs_imp_stmt_maybewritten_vars s₀)
       | NNRSimpIf e s₁ s₂ =>
         nnrs_imp_stmt_maybewritten_vars s₁ ++ nnrs_imp_stmt_maybewritten_vars s₂
       | NNRSimpEither e x₁ s₁ x₂ s₂ =>
         remove string_eqdec x₁ (nnrs_imp_stmt_maybewritten_vars s₁) ++ remove string_eqdec x₂ (nnrs_imp_stmt_maybewritten_vars s₂)
       end.

    Global Instance remove_perm_proper {A} dec v :
      Proper ((@Permutation A) ==> (@Permutation A)) (remove dec v).
        
    Lemma nnrs_imp_stmt_free_vars_readwrite_perm (s:nnrs_imp_stmt)
      : Permutation
          (nnrs_imp_stmt_free_vars s)
          (nnrs_imp_stmt_mayberead_vars s ++ nnrs_imp_stmt_maybewritten_vars s).

    Lemma nnrs_imp_stmt_free_vars_readwrite_equiv (s:nnrs_imp_stmt)
      : equivlist
          (nnrs_imp_stmt_free_vars s)
          (nnrs_imp_stmt_mayberead_vars s ++ nnrs_imp_stmt_maybewritten_vars s).

End NNRSimpVars.