Lvc.RenameApart

Require Import CSet Le.

Require Import Plus Util Map.
Require Import Env EnvTy IL Alpha Fresh Annotation RenamedApart SetOperations.

Set Implicit Arguments.

Fixpoint renameApart´ (ϱ:env var) (G:set var) (s:stmt) : set var × stmt:=
match s with
   | stmtLet x e s0 ⇒
     let y := fresh G in
     let ϱ´ := ϱ[x <- y] in
     let (G´, s´) := renameApart´ ϱ´ {y; G} s0 in
       ({y; G´}, stmtLet y (rename_exp ϱ e) s´)
   | stmtIf e s1 s2 ⇒
     let (G´, s1´) := renameApart´ ϱ G s1 in
     let (G´´, s2´) := renameApart´ ϱ (G ∪ G´) s2 in
      (G´ ∪ G´´, stmtIf (rename_exp ϱ e) s1´ s2´)
   | stmtApp l Y ⇒ (∅, stmtApp l (List.map (rename_exp ϱ) Y))
   | stmtReturn e ⇒ (∅, stmtReturn (rename_exp ϱ e))
   | stmtExtern x f Y s ⇒
     let y := fresh G in
     let ϱ´ := ϱ[x <- y] in
     let (G´, s´) := renameApart´ ϱ´ {y; G} s in
       ({y; G´}, stmtExtern y f (List.map (rename_exp ϱ) Y) s´)
   | stmtFun Z s1 s2 ⇒
     let Y := fresh_list fresh G (length Z) in
     let ϱZ := ϱ [ Z <-- Y ] in
     let (G´, s1´) := renameApart´ ϱZ (G ∪ of_list Y) s1 in
     let (G´´, s2´) := renameApart´ ϱ (G ∪ (G´ ∪ of_list Y)) s2 in
     (G´ ∪ (G´´ ∪ of_list Y), stmtFun Y s1´ s2´)
   end.

Lemma renameApart´_disj ϱ G s
  : disj G (fst (renameApart´ ϱ G s)).

Fixpoint renamedApartAnn (s:stmt) (G:set var) : ann (set var × set var) :=
  match s with
    | stmtLet x e s ⇒
      let an := renamedApartAnn s {x; G} in
      ann1 (G, {x; snd (getAnn an) }) an
    | stmtIf e s t ⇒
      let ans := renamedApartAnn s G in
      let ant := renamedApartAnn t G in
      ann2 (G, snd (getAnn ans) ∪ snd (getAnn ant)) ans ant
    | stmtReturn e ⇒
      ann0 (G, ∅)
    | stmtApp f Y ⇒
      ann0 (G, ∅)
    | stmtExtern x f Y s ⇒
      let an := renamedApartAnn s {x; G} in
      ann1 (G, {x; snd (getAnn an)}) an
    | stmtFun Z s t ⇒
      let ans := renamedApartAnn s (G ∪ of_list Z) in
      let ant := renamedApartAnn t G in
      ann2 (G, snd (getAnn ans) ∪ (snd (getAnn ant) ∪ of_list Z)) ans ant
  end.

Instance renamedApart_ann_morph
: Proper (eq ==> Equal ==> ann_R (@pe _ _ )) renamedApartAnn.

Lemma fst_renamedApartAnn s G
 : fst (getAnn (renamedApartAnn s G)) = G.

Lemma snd_renameApartAnn s G ϱ G´
: snd (getAnn (renamedApartAnn (snd (renameApart´ ϱ G s)) G´)) = fst (renameApart´ ϱ G s).

Lemma snd_renamedApartAnn s G
 : snd (getAnn (renamedApartAnn s G)) [=] definedVars s.

Lemma renameApartAnn_decomp s G
: pe (getAnn (renamedApartAnn s G)) (G, snd (getAnn (renamedApartAnn s G))).

Hint Resolve prod_eq_intro : cset.

Lemma ann_R_pe_notOccur G G´ s
: disj (occurVars s) G´
   → G \ G´ [=] G
   → ann_R (@pe var _)
           (renamedApartAnn s G)
                     (mapAnn (pminus G´) (renamedApartAnn s (G ∪ G´))).

Lemma freeVars_rename_exp_list ϱ Y
  : list_union (List.map Exp.freeVars (List.map (rename_exp ϱ) Y))[=]
               lookup_set ϱ (list_union (List.map Exp.freeVars Y)).

Lemma freeVars_renamedApart´ ϱ G s
: lookup_set ϱ (freeVars s) ⊆ G
  → freeVars (snd (renameApart´ ϱ G s)) [=] lookup_set ϱ (freeVars s).

Lemma definedVars_renamedApart´ ϱ G s
: definedVars (snd (renameApart´ ϱ G s)) [=] fst (renameApart´ ϱ G s).

Lemma renameApart´_renamedApart (s:stmt) ϱ G
  : lookup_set ϱ (freeVars s) ⊆ G
  → renamedApart (snd (renameApart´ ϱ G s)) (renamedApartAnn (snd (renameApart´ ϱ G s)) G).

Lemma rename_apart_alpha´ G ϱ ϱ´ s
  : lookup_set ϱ (freeVars s) ⊆ G
  → inverse_on (freeVars s) ϱ ϱ´
  → alpha ϱ´ ϱ (snd (renameApart´ ϱ G s)) s.

Definition rename_apart s := snd (renameApart´ id (freeVars s) s).

Lemma rename_apart_renamedApart (s:stmt)
: renamedApart (rename_apart s)
               (renamedApartAnn (snd (renameApart´ id (freeVars s) s)) (freeVars s)).

Lemma rename_apart_alpha s
  : alpha id id (rename_apart s) s.