Lvc.RenamedApart_Liveness

Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Annotation SetOperations MoreList.
Require Import Liveness Restrict RenamedApart LabelsDefined.

Set Implicit Arguments.

Lemma renamedApart_live_functional s ang DL
: renamedApart s ang
  → paramsMatch s (List.map (snd ∘ @length _) DL)
  → live_sound Functional DL s (mapAnn fst ang).

Lemma renamedApart_live s ang DL i
: renamedApart s ang
  → paramsMatch s (List.map (snd ∘ @length _) DL)
  → bounded (List.map (fun x ⇒ Some (fst x \ of_list (snd x))) DL) (fst (getAnn ang))
  → live_sound i DL s (mapAnn fst ang).


Definition disjoint (DL:list (option (set var))) (G:set var) :=
  ∀ n s, get DL n (Some s) → disj s G.

Instance disjoint_morphism_subset
  : Proper (eq ==> Subset ==> flip impl) disjoint.

Instance disjoint_morphism
  : Proper (eq ==> Equal ==> iff) disjoint.

Definition disj1 (x:set var) (y: set var × set var) := disj x (snd y).

Lemma disjoint_let D D´ D´´ x (DL:list (set var × list var)) an
: D´´[=]{x; D´}
  → disjoint (live_globals DL) (D´´)
  → pe (getAnn an) ({x; D}, D´)
  → disjoint (live_globals DL) (snd (getAnn an)).

Lemma disjoint_if1 D D´ Ds Dt (DL:list (set var × list var)) an
: Ds ++ Dt[=]D´
  → disjoint (live_globals DL) D´
  → pe (getAnn an) (D, Ds)
  → disjoint (live_globals DL) (snd (getAnn an)).

Lemma disjoint_if2 D D´ Ds Dt (DL:list (set var × list var)) an
: Ds ++ Dt[=]D´
  → disjoint (live_globals DL) D´
  → pe (getAnn an) (D, Dt)
  → disjoint (live_globals DL) (snd (getAnn an)).

Definition Subset1 (x : set var) (y : set var × set var) :=
  match y with
    | (y, _) ⇒ x[<=] y
  end.

Instance Subset1_morph
: Proper (Equal ==> @pe _ _ ==> iff) Subset1.

Lemma disjoint_fun1 D D´ Ds Dt (DL:list (set var × list var)) ans als Z s
: (Ds ++ Dt) ++ of_list Z[=]D´
    → disjoint (live_globals DL) D´
    → pe (getAnn ans) ((of_list Z ++ D)%set, Ds)
    → ann_R Subset1 als ans
    → renamedApart s ans
    → disjoint (live_globals ((getAnn als, Z) :: DL)) (snd (getAnn ans)).

Lemma disjoint_fun2 D D´ Ds Dt (DL:list (set var × list var)) ant als Z s ans
: (Ds ++ Dt) ++ of_list Z[=]D´
    → disjoint (live_globals DL) D´
    → pe (getAnn ant) (D, Dt)
    → ann_R Subset1 als ans
    → renamedApart s ant
    → pe (getAnn ans) ((of_list Z ++ D)%set, Ds)
    → (Ds ++ of_list Z) ∩ Dt[=]{}
    → disjoint (live_globals ((getAnn als, Z) :: DL)) (snd (getAnn ant)).

Lemma renamedApart_globals_live s AL alv f ang
: live_sound Imperative AL s alv
  → renamedApart s ang
  → isCalled s f
  → ann_R Subset1 alv ang
  → disjoint (live_globals AL) (snd (getAnn ang))
  → ∃ lvZ, get AL (counted f) lvZ ∧ (fst lvZ \ of_list (snd lvZ)) ⊆ getAnn alv.

Lemma renamedApart_live_imperative_is_functional s ang DL alv
: renamedApart s ang
  → noUnreachableCode s
  → live_sound Imperative DL s alv
  → ann_R Subset1 alv ang
  → disjoint (live_globals DL) (snd (getAnn ang))
  → live_sound FunctionalAndImperative DL s alv.

Fixpoint mapAnn2 X X´ Y (f:X → X´ → Y) (a:ann X) (b:ann X´) : ann Y :=
  match a, b with
    | ann1 a an, ann1 b bn ⇒ ann1 (f a b) (mapAnn2 f an bn)
    | ann2 a an1 an2, ann2 b bn1 bn2 ⇒ ann2 (f a b) (mapAnn2 f an1 bn1) (mapAnn2 f an2 bn2)
    | ann0 a, ann0 b ⇒ ann0 (f a b)
    | a, b ⇒ ann0 (f (getAnn a) (getAnn b))
  end.

Lemma getAnn_mapAnn2 A A´ A´´ (a:ann A) (b:ann A´) (f:A→A´→A´´) s
: annotation s a
  → annotation s b
  → getAnn (mapAnn2 f a b) = f (getAnn a) (getAnn b).

Lemma renamedApart_annotation s ang
: renamedApart s ang
  → annotation s ang.

Lemma live_exp_sound_meet e D lv
: Exp.freeVars e[<=]D
   → live_exp_sound e lv
   → live_exp_sound e (lv ∩ D).

Definition meet1 (x:set var) (y:set var × set var) :=
  match y with
    | (y, _) ⇒ x ∩ y
  end.

Lemma meet1_incl a b
: meet1 a b ⊆ a.

Lemma meet1_Subset s alv ang
: annotation s alv
  → annotation s ang
  → ann_R Subset (mapAnn2 meet1 alv ang) alv.

Instance meet1_morphism
: Proper (Subset ==> @pe _ _ ==> Subset) meet1.

Instance meet1_morphism´
: Proper (Equal ==> @pe _ _ ==> Equal) meet1.

Lemma live_sound_renamedApart_minus s ang DL alv i
: renamedApart s ang
  → live_sound i DL s alv
  → bounded (live_globals DL) (fst (getAnn ang))
  → live_sound i DL s (mapAnn2 meet1 alv ang).