Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Annotation SetOperations MoreList.

Set Implicit Arguments.

Inductive renamedApart : stmt → ann (set var × set var) → Prop :=
  | renamedApartExp x e s D D´ D´´ an
    : x ∉ D
      → Exp.freeVars e ⊆ D
      → renamedApart s an
      → pe (getAnn an) ({x; D}, D´)
      → D´´ [=] {x; D´}
      → renamedApart (stmtLet x e s) (ann1 (D, D´´) an)
  | renamedApartIf D D´ Ds Dt e s t ans ant
    : Exp.freeVars e ⊆ D
      → Ds ∩ Dt [=] ∅
      → Ds ∪ Dt [=] D´
      → renamedApart s ans
      → renamedApart t ant
      → pe (getAnn ans) (D, Ds)
      → pe (getAnn ant) (D, Dt)
      → renamedApart (stmtIf e s t) (ann2 (D, D´) ans ant)
  | renamedApartRet D D´ e
    : Exp.freeVars e ⊆ D
      → D´ [=] ∅
      → renamedApart (stmtReturn e) (ann0 (D, D´))
  | renamedApartGoto D D´ f Y
    : list_union (List.map Exp.freeVars Y) ⊆ D
      → D´ [=] ∅
      → renamedApart (stmtApp f Y) (ann0 (D, D´))
  | renamedApartExtern x f Y s D D´ D´´ an
    : x ∉ D
      → list_union (List.map Exp.freeVars Y) ⊆ D
      → renamedApart s an
      → pe (getAnn an) ({x; D}, D´)
      → D´´ [=] {x; D´}
      → renamedApart (stmtExtern x f Y s) (ann1 (D, D´´) an)
  | renamedApartLet D D´ s t Ds Dt Z ans ant
    : of_list Z ∩ D [=] ∅
      → (Ds ++ of_list Z) ∩ Dt [=] ∅
      → Ds ∪ Dt ∪ of_list Z [=] D´
      → renamedApart s ans
      → pe (getAnn ans) (of_list Z ∪ D, Ds)
      → renamedApart t ant
      → pe (getAnn ant) (D, Dt)
      → unique Z
      → renamedApart (stmtFun Z s t) (ann2 (D,D´) ans ant).

Lemma renamedApart_ext s an an´
  : ann_R (@pe _ _) an an´
  → renamedApart s an
  → renamedApart s an´.

Instance renamedApart_morphism
: Proper (eq ==> (ann_R (@pe _ _)) ==> iff) renamedApart.

Lemma renamedApart_freeVars s an
  : renamedApart s an → freeVars s ⊆ fst (getAnn an).

Lemma renamedApart_occurVars s an
  : renamedApart s an → definedVars s [=] snd (getAnn an).

Definition pminus (D´´:set var) (s:set var × set var) :=
  match s with
    | pair s s´ ⇒ (s \ D´´, s´)
  end.

Instance pminus_morphism
: Proper (Equal ==> (@pe _ _) ==> (@pe _ _) ) pminus.

Instance mapAnn_pminus_morphism G´
  : Proper (ann_R (@pe _ _) ==> ann_R (@pe _ _)) (mapAnn (pminus G´)).

Lemma not_in_minus X `{OrderedType X} (s t: set X) x
: x ∉ s
  → x ∉ s \ t.

Hint Resolve not_in_minus : cset.

Lemma not_incl_minus X `{OrderedType X} (s t u: set X)
: s ⊆ t
  → disj s u
  → s ⊆ t \ u.

Hint Resolve not_incl_minus : cset.
Hint Resolve disj_1_incl disj_2_incl : cset.

Hint Extern 20 (pe ?a ?a) ⇒ reflexivity.

Lemma renamedApart_minus D an an´ s
  : disj (occurVars s) D
    → renamedApart s an
    → ann_R (@pe _ _) an´ (mapAnn (pminus D) an)
    → renamedApart s an´.

Lemma renamedApart_disj s G
: renamedApart s G
  → disj (fst (getAnn G)) (snd (getAnn G)).