Module Qcert.cNNRC.Lang.cNNRCVars

Require Import String.
Require Import List.
Require Import Arith.
Require Import Max.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import cNNRC.

Section cNNRCVars.
  Close Scope nnrc_scope.
  

  Context {fruntime:foreign_runtime}.

  Fixpoint nnrc_global_vars (e:nnrc) : list var :=
    match e with
    | NNRCGetConstant x => x :: nil
    | NNRCVar x => nil
    | NNRCConst d => nil
    | NNRCBinop bop e1 e2 => nnrc_global_vars e1 ++ nnrc_global_vars e2
    | NNRCUnop uop e1 => nnrc_global_vars e1
    | NNRCLet x e1 e2 => (nnrc_global_vars e1 ++ remove string_eqdec x (nnrc_global_vars e2))
    | NNRCFor x e1 e2 => (nnrc_global_vars e1 ++ remove string_eqdec x (nnrc_global_vars e2))
    | NNRCIf e1 e2 e3 => nnrc_global_vars e1 ++ nnrc_global_vars e2 ++ nnrc_global_vars e3
    | NNRCEither ed xl el xr er => nnrc_global_vars ed ++ (remove string_eqdec xl (nnrc_global_vars el)) ++ (remove string_eqdec xr (nnrc_global_vars er))
    | NNRCGroupBy g sl e => nnrc_global_vars e
    end.
  
  Fixpoint nnrc_bound_vars (e:nnrc) : list var :=
    match e with
    | NNRCGetConstant x => nil
    | NNRCVar x => nil
    | NNRCConst d => nil
    | NNRCBinop bop e1 e2 => nnrc_bound_vars e1 ++ nnrc_bound_vars e2
    | NNRCUnop uop e1 => nnrc_bound_vars e1
    | NNRCLet x e1 e2 => x :: (nnrc_bound_vars e1 ++ nnrc_bound_vars e2)
    | NNRCFor x e1 e2 => x :: (nnrc_bound_vars e1 ++ nnrc_bound_vars e2)
    | NNRCIf e1 e2 e3 => nnrc_bound_vars e1 ++ nnrc_bound_vars e2 ++ nnrc_bound_vars e3
    | NNRCEither ed xl el xr er => xl :: xr :: nnrc_bound_vars ed ++ nnrc_bound_vars el++ nnrc_bound_vars er
    | NNRCGroupBy g s e => nnrc_bound_vars e
    end.

  Fixpoint nnrc_free_vars (e:nnrc) : list var :=
    match e with
    | NNRCGetConstant x => nil
    | NNRCVar x => x :: nil
    | NNRCConst d => nil
    | NNRCBinop bop e1 e2 => nnrc_free_vars e1 ++ nnrc_free_vars e2
    | NNRCUnop uop e1 => nnrc_free_vars e1
    | NNRCLet x e1 e2 => (nnrc_free_vars e1 ++ remove string_eqdec x (nnrc_free_vars e2))
    | NNRCFor x e1 e2 => (nnrc_free_vars e1 ++ remove string_eqdec x (nnrc_free_vars e2))
    | NNRCIf e1 e2 e3 => nnrc_free_vars e1 ++ nnrc_free_vars e2 ++ nnrc_free_vars e3
    | NNRCEither ed xl el xr er => nnrc_free_vars ed ++ (remove string_eqdec xl (nnrc_free_vars el)) ++ (remove string_eqdec xr (nnrc_free_vars er))
    | NNRCGroupBy g sl e => nnrc_free_vars e
    end.

  Definition nnrc_vars e := nnrc_free_vars e ++ nnrc_bound_vars e.

  Fixpoint nnrc_subst (e:nnrc) (x:var) (e':nnrc) : nnrc
    := match e with
       | NNRCGetConstant y => NNRCGetConstant y
       | NNRCVar y => if y == x then e' else NNRCVar y
       | NNRCConst d => NNRCConst d
       | NNRCBinop bop e1 e2 => NNRCBinop bop
                                          (nnrc_subst e1 x e')
                                          (nnrc_subst e2 x e')
       | NNRCUnop uop e1 => NNRCUnop uop (nnrc_subst e1 x e')
       | NNRCLet y e1 e2 =>
         NNRCLet y
                 (nnrc_subst e1 x e')
                 (if y == x then e2 else nnrc_subst e2 x e')
       | NNRCFor y e1 e2 =>
         NNRCFor y
                 (nnrc_subst e1 x e')
                 (if y == x then e2 else nnrc_subst e2 x e')
       | NNRCIf e1 e2 e3 => NNRCIf
                               (nnrc_subst e1 x e')
                               (nnrc_subst e2 x e')
                               (nnrc_subst e3 x e')
       | NNRCEither ed xl el xr er =>
         NNRCEither (nnrc_subst ed x e')
                    xl
                    (if xl == x then el else nnrc_subst el x e')
                    xr
                    (if xr == x then er else nnrc_subst er x e')
       | NNRCGroupBy g sl e1 => NNRCGroupBy g sl (nnrc_subst e1 x e')
       end.

  Lemma nnrc_subst_not_free e x :
    ~ In x (nnrc_free_vars e) ->
    forall e', nnrc_subst e x e' = e.

  Lemma nnrc_subst_remove_one_free e x e' :
    nnrc_free_vars e' = nil ->
    nnrc_free_vars (nnrc_subst e x e') = remove string_eqdec x (nnrc_free_vars e).

  Lemma nnrc_subst_not_in_free e x e':
    nnrc_free_vars e' = nil ->
    forall y,
      In y (nnrc_free_vars (nnrc_subst e x e')) -> x <> y.

  Lemma nnrc_subst_remove_free e x e':
    nnrc_free_vars e' = nil ->
    forall y,
      In y (nnrc_free_vars (nnrc_subst e x e')) -> In y (nnrc_free_vars e).

  Definition really_fresh_in (sep:string) (oldvar:var) (avoid:list var) (e:nnrc)
    := fresh_var_from
         sep
         oldvar
         (avoid ++ nnrc_free_vars e ++ nnrc_bound_vars e).

  Lemma really_fresh_in_fresh (sep:string) (oldvar:var) (avoid:list var) (e:nnrc) :
    ~ In (really_fresh_in sep oldvar avoid e)
      (avoid ++ nnrc_free_vars e ++ nnrc_bound_vars e).
  
  Lemma really_fresh_from_avoid sep old avoid (e:nnrc) :
    ~ In (really_fresh_in sep old avoid e) avoid.

  Lemma really_fresh_from_free sep old avoid (e:nnrc) :
    ~ In (really_fresh_in sep old avoid e) (nnrc_free_vars e).

  Lemma really_fresh_from_bound sep old avoid (e:nnrc) :
    ~ In (really_fresh_in sep old avoid e) (nnrc_bound_vars e).

  Lemma nnrc_bound_vars_subst_preserved e x e' :
    nnrc_bound_vars e' = nil ->
    nnrc_bound_vars (nnrc_subst e x e') = nnrc_bound_vars e.

  Lemma nnrc_free_vars_subst e v n: ~ In n (nnrc_bound_vars e) ->
                                    nnrc_free_vars ((nnrc_subst e v (NNRCVar n))) =
                                    replace_all (nnrc_free_vars e) v n.

  Lemma nnrc_subst_eq e v : nnrc_subst e v (NNRCVar v) = e.

  Lemma incl_letvars1 v e1 e2 env :
    incl (nnrc_vars (NNRCLet v e1 e2)) env ->
    incl (nnrc_vars e1) env.
  
  Lemma incl_letvars2 v e1 e2 env :
    incl (nnrc_vars (NNRCLet v e1 e2)) env ->
    incl (nnrc_vars e2) (env).
  
  Section core.
    Lemma nnrc_subst_preserve_core n1 n2 v1 :
      nnrcIsCore n1 -> nnrcIsCore n2 -> nnrcIsCore (nnrc_subst n1 v1 n2).

  End core.
  
  Section FreeVars.
    Definition nnrc_free_variables (q:nnrc) : list var := nnrc_free_vars q.
  End FreeVars.

End cNNRCVars.