Lvc.Spilling.RLiveSound

Require Import List Map Env AllInRel Exp MoreList.
Require Import IL Annotation.
Require Import Liveness.Liveness.
Require Import ExpVarsBounded SpillSound SpillUtil.

Inductive rlive_sound
  : list params → list (set var) → stmt → spilling → ann (set var) → Prop :=
| RLiveLet ZL Lv x e s Sp L sl lv (al:ann (set var))
  : Sp ⊆ lv
     → rlive_sound ZL Lv s sl al
     → live_exp_sound e (lv ∪ L)
     → (getAnn al \ singleton x) ⊆ lv ∪ L
     → x ∈ getAnn al
     → rlive_sound ZL Lv (stmtLet x e s) (ann1 (Sp,L,nil) sl) (ann1 lv al)
| RLiveIf Lv ZL e s1 s2 Sp L sl1 sl2 lv al1 al2
  : Sp ⊆ lv
     → rlive_sound ZL Lv s1 sl1 al1
     → rlive_sound ZL Lv s2 sl2 al2
     → live_op_sound e (lv ∪ L)
     → getAnn al1 ⊆ lv ∪ L
     → getAnn al2 ⊆ lv ∪ L
     → rlive_sound ZL Lv (stmtIf e s1 s2) (ann2 (Sp,L,nil) sl1 sl2) (ann2 lv al1 al2)
| RLiveApp ZL Lv l Y Sp L R' M' lv blv Z
  : Sp ⊆ lv
    → get ZL (counted l) Z
    → get Lv (counted l) blv
    → (blv \ of_list Z) ⊆ lv ∪ L
    → (∀ n y, get Y n y → live_op_sound y (lv ∪ M' ∪ L))
    → R' ⊆ lv ∪ L
    → rlive_sound ZL Lv (stmtApp l Y) (ann0 (Sp,L,(R',M')::nil)) (ann0 lv)
| RLiveReturn ZL Lv e Sp L lv
  : Sp ⊆ lv
    → live_op_sound e (lv ∪ L)
    → rlive_sound ZL Lv (stmtReturn e) (ann0 (Sp,L,nil)) (ann0 lv)
| RLiveFun ZL Lv F t lv Sp L rms sl_F sl_t als alb
  : Sp ⊆ lv
    → rlive_sound (fst ⊝ F ++ ZL) (getAnn ⊝ als ++ Lv) t sl_t alb
    → length F = length als
    → (∀ n Zs a sl_s, get F n Zs →
                 get als n a →
                 get sl_F n sl_s →
                 rlive_sound (fst ⊝ F ++ ZL) (getAnn ⊝ als ++ Lv) (snd Zs) sl_s a)
    → (∀ n Zs a rm, get F n Zs →
                    get als n a →
                    get rms n rm →
                    (fst rm) ⊆ getAnn a)
    → getAnn alb ⊆ lv ∪ L
    → rlive_sound ZL Lv (stmtFun F t) (annF (Sp,L,rms) sl_F sl_t) (annF lv als alb)
.

Lemma rlive_sound_monotone
  : ∀ (ZL : 〔params〕) (LV LV' : 〔⦃var⦄〕) (s : stmt) (sl : spilling) (rlv : ann ⦃var⦄),
    rlive_sound ZL LV s sl rlv → PIR2 Subset LV' LV → rlive_sound ZL LV' s sl rlv.
Proof.
  intros ? ? ? ? ? ? rlvSnd pir2.
  general induction rlvSnd.
  - econstructor; eauto.
  - econstructor; eauto.
  - eapply PIR2_nth_2 in pir2 as [lv' [get_lv' lv'_sub]]; eauto.
    econstructor; eauto. rewrite lv'_sub. eauto.
  - econstructor; eauto.
  - econstructor; eauto.
    + eapply IHrlvSnd. apply PIR2_app; [apply PIR2_refl|]; eauto.
    + intros; inv_get. eapply H2; eauto. apply PIR2_app; [apply PIR2_refl|]; eauto.
Qed.