Require Import Util LengthEq AllInRel Map Env DecSolve.
Require Import IL Annotation AutoIndTac Exp SetOperations.
Require Export Liveness.Liveness Filter LabelsDefined OUnion.

Set Implicit Arguments.

Local Hint Resolve incl_empty minus_incl incl_right incl_left.

Inductive argsLive (Caller Callee:set var) : args → params → Prop :=
| AL_nil : argsLive Caller Callee nil nil
| AL_cons y z Y Z
  : argsLive Caller Callee Y Z
    → (z ∈ Callee → live_op_sound y Caller)
    → argsLive Caller Callee (y::Y) (z::Z).

Lemma argsLive_length lv bv Y Z
  : argsLive lv bv Y Z
    → length Y = length Z.
Proof.
  intros. general induction H; simpl; eauto.
Qed.

Hint Resolve argsLive_length : len.

Lemma argsLive_liveSound lv blv Y Z
  : argsLive lv blv Y Z
    → ∀ (n : nat) (y : op),
      get (filter_by (fun y : var ⇒ B[y ∈ blv]) Z Y) n y →
      live_op_sound y lv.
Proof.
  intros. general induction H; simpl in × |- ×.
  - isabsurd.
  - decide (z ∈ blv); eauto.
    inv H1; eauto.
Qed.

Lemma argsLive_live_exp_sound lv blv Y Z y z n
  : argsLive lv blv Y Z
    → get Y n y
    → get Z n z
    → z ∈ blv
    → live_op_sound y lv.
Proof.
  intros. general induction n; invt argsLive; isabsurd; eauto.
Qed.

Lemma live_exp_sound_argsLive lv blv Y Z
  : length Y = length Z
    → (∀ n y z, get Y n y → get Z n z → z ∈ blv → live_op_sound y lv)
    → argsLive lv blv Y Z.
Proof.
  intros. length_equify.
  general induction H; eauto 20 using argsLive, get.
Qed.

Lemma argsLive_agree_on' (V E E':onv val) lv blv Y Z v v'
  : argsLive lv blv Y Z
     → agree_on eq lv E E'
     → omap (op_eval E) Y = Some v
     → omap (op_eval E') Y = Some v'
     → agree_on eq blv (V [Z <-- List.map Some v]) (V [Z <-- List.map Some v']).
Proof.
  intros. general induction H; simpl in × |- *; eauto.
  - monad_inv H2. monad_inv H3.
    decide (z ∈ blv).
    +erewrite <- op_eval_live in EQ0; eauto.
     × assert (x1 = x) by congruence.
        subst. simpl.
        eauto using agree_on_update_same, agree_on_incl.
    + eapply agree_on_update_dead_both; eauto.
Qed.

Lemma argsLive_agree_on (V V' E E':onv val) lv blv Y Z v v'
  : agree_on eq (blv \ of_list Z) V V'
    → argsLive lv blv Y Z
    → agree_on eq lv E E'
    → omap (op_eval E) Y = Some v
    → omap (op_eval E') Y = Some v'
    → agree_on eq blv (V [Z <-- List.map Some v]) (V' [Z <-- List.map Some v']).
Proof.
  intros. etransitivity; eauto using argsLive_agree_on'.
  eapply update_with_list_agree; eauto with len.
Qed.

Lemma filter_by_incl_argsLive lv blv Y Z
  : ❬Y❭ = ❬Z❭
    → list_union (Op.freeVars ⊝ filter_by (fun x ⇒ if [x \In blv] then true else false) Z Y) ⊆ lv
    → argsLive lv blv Y Z.
Proof.
  intros LEN INCL. length_equify.
  general induction LEN; simpl in *; eauto using argsLive.
  - econstructor.
    + cases in INCL; try congruence; eauto.
      × eapply IHLEN. rewrite <- INCL.
        simpl List.map. rewrite list_union_cons. eauto with cset.
    + intros. cases in INCL.
      simpl List.map in INCL.
      rewrite list_union_cons in INCL.
      eapply live_op_sound_incl;[eapply Op.live_freeVars|].
      rewrite <- INCL. eauto with cset.
Qed.

Inductive true_live_sound (i:overapproximation)
  : list params → list (set var) → stmt → ann (set var) → Prop :=
| TLOpr ZL Lv x b lv e al
  : true_live_sound i ZL Lv b al
     → (x ∈ getAnn al ∨ isCall e → live_exp_sound e lv)
     → (getAnn al\ singleton x) ⊆ lv
     → true_live_sound i ZL Lv (stmtLet x e b) (ann1 lv al)
| TLIf ZL Lv e b1 b2 lv al1 al2
  : true_live_sound i ZL Lv b1 al1
     → true_live_sound i ZL Lv b2 al2
     → live_op_sound e lv
     → getAnn al1 ⊆ lv
     → getAnn al2 ⊆ lv
     → true_live_sound i ZL Lv (stmtIf e b1 b2) (ann2 lv al1 al2)
| TLGoto ZL Lv l Y lv blv Z
  : get ZL (counted l) Z
    → get Lv (counted l) blv
    → (if isImperative i then (blv \ of_list Z ⊆ lv) else True)
    → argsLive lv blv Y Z
    → length Y = length Z
    → true_live_sound i ZL Lv (stmtApp l Y) (ann0 lv)
| TLReturn ZL Lv e lv
  : live_op_sound e lv
    → true_live_sound i ZL Lv (stmtReturn e) (ann0 lv)
| TLLet ZL Lv F t lv als alt
  : true_live_sound i (fst ⊝ F ++ ZL) (getAnn ⊝ als ++ Lv) t alt
    → length F = length als
    → (∀ n Zs a, get F n Zs →
                 get als n a →
                 true_live_sound i (fst ⊝ F ++ ZL) (getAnn ⊝ als ++ Lv) (snd Zs) a)
    → (∀ n Zs a, get F n Zs →
                 get als n a →
                 if isFunctional i then (getAnn a \ of_list (fst Zs)) ⊆ lv
                 else True)
    → getAnn alt ⊆ lv
    → true_live_sound i ZL Lv (stmtFun F t)(annF lv als alt).

Lemma true_live_sound_overapproximation_I ZL Lv s slv
  : true_live_sound FunctionalAndImperative ZL Lv s slv
    → true_live_sound Imperative ZL Lv s slv.
Proof.
  intros. general induction H; simpl in × |- *; econstructor; simpl; eauto.
Qed.

Lemma true_live_sound_overapproximation_F ZL Lv s slv
  : true_live_sound FunctionalAndImperative ZL Lv s slv
    → true_live_sound Functional ZL Lv s slv.
Proof.
  intros. general induction H; simpl in × |- *; econstructor; simpl; eauto.
Qed.

Lemma argsLive_monotone lv blv blv' Y Z
  : argsLive lv blv Y Z
    → blv' ⊆ blv
    → argsLive lv blv' Y Z.
Proof.
  intros Args LE.
  general induction Args; eauto using argsLive.
Qed.

Lemma true_live_sound_monotone i ZL LV LV' s lv
: true_live_sound i ZL LV s lv
  → PIR2 Subset LV' LV
  → true_live_sound i ZL LV' s lv.
Proof.
  intros LS LE.
  general induction LS; simpl; eauto 20 using true_live_sound, PIR2_app.
  - PIR2_inv.
    econstructor; eauto.
    cases; eauto with cset.
    eauto using argsLive_monotone.
Qed.