Module Qcert.Imp.Lang.ImpVars

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 Imp.

Section ImpVars.
  Import ListNotations.


  Context {Constant: Set}.
  Context {Op: Set}.
  Context {Runtime: Set}.


  Fixpoint imp_expr_free_vars (e:@imp_expr Constant Op Runtime) : list var
    := match e with
       | ImpExprError _ => nil
       | ImpExprVar v => v :: nil
       | ImpExprConst _ => nil
       | ImpExprOp _ l => List.fold_left (fun acc e => imp_expr_free_vars e ++ acc) l []
       | ImpExprRuntimeCall _ l => List.fold_left (fun acc e => imp_expr_free_vars e ++ acc) l []
       end.


  Fixpoint imp_stmt_free_vars (stmt:imp_stmt) : list var
    := match stmt with
       | ImpStmtBlock decls stmts =>
         List.fold_right
           (fun decl acc =>
              match decl with
              | (v, None) => remove string_eqdec v acc
              | (v, Some e) => imp_expr_free_vars e ++ (remove string_eqdec v acc)
              end)
           (List.fold_right (fun s acc => imp_stmt_free_vars s ++ acc) [] stmts)
           decls
       | ImpStmtAssign x e =>
         x :: imp_expr_free_vars e
       | ImpStmtFor v e s =>
         imp_expr_free_vars e ++ remove string_eqdec v (imp_stmt_free_vars s)
       | ImpStmtForRange v e1 e2 s =>
         imp_expr_free_vars e1 ++ imp_expr_free_vars e2 ++ remove string_eqdec v (imp_stmt_free_vars s)
       | ImpStmtIf e s1 s2 =>
         imp_expr_free_vars e ++ imp_stmt_free_vars s1 ++ imp_stmt_free_vars s2
       end.

  Fixpoint imp_stmt_bound_vars (stmt:@imp_stmt Constant Op Runtime) : list var
    := match stmt with
       | ImpStmtBlock decls stmts =>
         List.fold_left
           (fun acc decl =>
              match decl with
              | (v, None) => v :: acc
              | (v, Some e) => v :: acc
              end)
           decls
           (List.fold_left (fun acc s => imp_stmt_bound_vars s ++ acc) stmts [])
       | ImpStmtAssign x e => nil
       | ImpStmtFor v e s => v :: imp_stmt_bound_vars s
       | ImpStmtForRange v e1 e2 s => v :: imp_stmt_bound_vars s
       | ImpStmtIf e s1 s2 => imp_stmt_bound_vars s1 ++ imp_stmt_bound_vars s2
       end.

    Global Instance remove_perm_proper {A} dec v :
      Proper ((@Permutation A) ==> (@Permutation A)) (remove dec v).


End ImpVars.