Require Import CSet Le.

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

Set Implicit Arguments.

Renamed-apart (formally)

Every subterm is annotated with two sets D and D' such that D contains all free variables of the subterm and D' is extactly the set of variables that occur in a binding position.

Definition defVars (Zs:params × stmt) (a:ann (set var × set var)) := of_list (fst Zs) snd (getAnn a).

Hint Unfold defVars.

Definition funConstr D Dt (Zs:params × stmt) a :=
  fst (getAnn a) [=] of_list (fst Zs) D
   unique (fst Zs)
   disj (of_list (fst Zs)) D
   disj (of_list (fst Zs) snd (getAnn a)) Dt.

Inductive renamedApart : stmt ann (set var × set var) Prop :=
  | renamedApartExp x e s D Ds D' an
    : x D
       Exp.freeVars e D
       renamedApart s an
       D' [=] {x; Ds}
       pe (getAnn an) ({x; D}, Ds)
       renamedApart (stmtLet x e s) (ann1 (D, D') an)
  | renamedApartIf D D' Ds Dt e s t ans ant
    : Op.freeVars e D
       disj 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
    : Op.freeVars e D
       D' [=]
       renamedApart (stmtReturn e) (ann0 (D, D'))
  | renamedApartGoto D D' f Y
    : list_union ( Op.freeVars Y) D
       D' [=]
       renamedApart (stmtApp f Y) (ann0 (D, D'))
  | renamedApartLet D D' F t Dt ans ant
    : length F = length ans
       ( n Zs a, get F n Zs get ans n a renamedApart (snd Zs) a)
       indexwise_R (funConstr D Dt) F ans
       pairwise_ne disj (zip defVars F ans)
       renamedApart t ant
       pe (getAnn ant) (D, Dt)
       list_union (zip defVars F ans) Dt [=] D'
       renamedApart (stmtFun F t) (annF (D,D') ans ant).


Lemma renamedApart_ext s an an'
  : ann_R (@pe _ _) an an'
   renamedApart s an
   renamedApart s an'.
  general induction H0; simpl; invt (ann_R (@pe var _));
  invt (@pe var _); eauto using renamedApart.
  - econstructor; try srewrite c; try srewrite d; eauto.
    rewrite <- (ann_R_get H9). eauto.
  - econstructor; try srewrite c; try srewrite d; eauto.
    + rewrite <- (ann_R_get H10); eauto.
    + rewrite <- (ann_R_get H11); eauto.

  - econstructor; try srewrite c; try srewrite d; eauto.
  - econstructor; try srewrite c; try srewrite d; eauto.
  - assert (PIR2 Equal (zip defVars F bns) (zip defVars F ans)).
    { eapply zip_ext_PIR2; eauto; try congruence.
      intros. get_functional.
      exploit H14; eauto. unfold defVars.
      rewrite H13. reflexivity.
    econstructor; try srewrite c; try srewrite d; eauto with len.
    + intros. edestruct (get_length_eq _ H13 (eq_sym H12)).
      eapply H1; eauto.
    + hnf; intros. edestruct (get_length_eq _ H13 (eq_sym H12)).
      exploit H2; eauto. destruct H18. dcr.
      exploit H14; eauto. hnf. rewrite <- H10.
      instantiate (1:=Dt).
      rewrite <- H19; eauto.
    + eapply pairwise_disj_PIR2; eauto. symmetry; eauto.
    + rewrite <- H15; eauto.
    + rewrite H8. eauto.

Instance renamedApart_morphism
: Proper (eq ==> (ann_R (@pe _ _)) ==> iff) renamedApart.
  intros x s t A; subst. intros. split; intros.
  eapply renamedApart_ext; eauto.
  eapply renamedApart_ext; try symmetry; eauto.

Relation to freeVars and occurVars

Lemma renamedApart_freeVars s an
  : renamedApart s an freeVars s fst (getAnn an).
  intros. general induction H; simpl; eauto; pe_rewrite.
  - rewrite IHrenamedApart, H0.
    clear_all; cset_tac; intuition.
  - rewrite H, IHrenamedApart1, IHrenamedApart2. cset_tac.
  - rewrite IHrenamedApart.
    rewrite (@list_union_incl _ _ _ _ D); eauto with cset.
    intros ? ? GET. inv_map GET.
    edestruct (get_length_eq _ H7 H); eauto.
    rewrite H1; eauto.
    edestruct H2; eauto; dcr; eauto with cset.

Lemma renamedApart_occurVars s an
  : renamedApart s an definedVars s [=] snd (getAnn an).
  general induction H; simpl; eauto;
  pe_rewrite; srewrite D'; eauto with cset.
  - rewrite IHrenamedApart.
    eapply eq_union_lr; eauto.
    eapply list_union_eq; eauto with len.
    intros. inv_map H7. inv_zip H8. get_functional; subst.
    rewrite H1; eauto. unfold defVars. eauto with cset.

Definition pminus (D'':set var) (s:set var × set var) :=
  match s with
    | pair s s'(s \ D'', s')

Instance pminus_morphism
: Proper (Equal ==> (@pe _ _) ==> (@pe _ _) ) pminus.
  unfold Proper, respectful; intros.
  inv H0; simpl; econstructor. rewrite H1, <- H. reflexivity.

Instance mapAnn_pminus_morphism G'
  : Proper (ann_R (@pe _ _) ==> ann_R (@pe _ _)) (mapAnn (pminus G')).
  unfold Proper, respectful; intros.
  general induction H; simpl; constructor; eauto with len pe.
  - intros. inv_map H4. inv_map H5. eauto.

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'.
  intros DISJ RN PE. revert an' PE.
  induction RN; indros; try rewrite PE; simpl in × |- ×.
  - econstructor; eauto 20 with cset pe ann.
  - econstructor; eauto with cset pe ann.
  - econstructor; eauto with cset.
  - econstructor; eauto with cset.
  - econstructor; eauto with cset len.
    + intros ? ? ? GET1 GET2. inv_map GET2. eapply H1; eauto.
      eapply disj_1_incl; eauto.
      rewrite <- get_list_union_map; eauto. cset_tac.
    + hnf; intros ? ? ? GET1 GET2.
      inv_map GET2. edestruct H2; eauto; dcr. instantiate (1:=Dt).
      hnf. rewrite getAnn_mapAnn.
      destruct (getAnn x); simpl in ×.
      assert (disj (of_list (fst a)) D).
      eapply disj_1_incl; eauto.
      rewrite <- get_list_union_map; eauto. cset_tac; intuition.
      split. rewrite H7.
      revert H8; unfold disj; clear_all; cset_tac; intuition; eauto.
      eauto with cset.
    + eapply pairwise_disj_PIR2; eauto.
      eapply zip_ext_PIR2; eauto. rewrite map_length; eauto.
      intros ? ? ? ? ? GET1 GET2 GET3 GET4. get_functional; subst.
      inv_map GET4.
      unfold defVars. rewrite getAnn_mapAnn. destruct (getAnn y); reflexivity.
    + eauto with cset pe ann.
    + rewrite list_union_eq; eauto with len.
      intros ? ? ? GET1 GET2. inv_zip GET1. inv_zip GET2. inv_map H7.
      get_functional; subst. unfold defVars.
      rewrite getAnn_mapAnn. destruct (getAnn x2); simpl. reflexivity.

The two annotating sets are disjoint.

Lemma renamedApart_disj s G
: renamedApart s G
   disj (fst (getAnn G)) (snd (getAnn G)).
  intros. general induction H; simpl; pe_rewrite; try srewrite D'.
  - eauto with cset.
  - eauto with cset.
  - eauto with cset.
  - eauto with cset.
  - eapply disj_app; split; eauto.
    + symmetry. rewrite <- list_union_disjunct.
      intros ? ? GET. inv_zip GET.
      exploit H1; eauto.
      unfold defVars.
      edestruct H2; eauto; dcr. rewrite H10 in H9.
      eapply disj_app; split.
      symmetry; eauto.
      eauto with cset.