Lvc.Coherence.DelocationAlgo

Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Annotation Liveness Coherence Sim MoreList Restrict Delocation.

Set Implicit Arguments.

Definition addParam x (DL:list (set var)) (AP:list (set var)) :=
  zip (fun (DL:set var) AP ⇒ if [x ∈ DL]
                   then {{x}} ∪ AP else AP) DL AP.


Definition addParams Z DL (AP:list (set var)) :=
  zip (fun DL AP ⇒ (of_list Z ∩ DL) ∪ AP) DL AP.

Definition oget {X} `{OrderedType X} (s:option (set X)) :=
  match s with Some s ⇒ s | None ⇒ ∅ end.

Definition addAdds s DL (AP:list (option (set var))) :=
  zip (fun (DL:set var) AP ⇒ mdo t <- AP; Some ((s ∩ DL) ∪ t)) DL AP.

Lemma addParam_length x DL AP
 : length DL = length AP
   → length (addParam x DL AP) = length DL.

Lemma addAdds_length Z DL AP
 : length DL = length AP
   → length (addAdds Z DL AP) = length DL.

Definition killExcept f (AP:list (set var)) :=
  mapi (fun n x ⇒ if [n = counted f] then Some x else None) AP.

Definition ounion {X} `{OrderedType X} (s t: option (set X)) :=
  match s, t with
    | Some s, Some t ⇒ Some (s ∪ t)
    | Some s, None ⇒ Some s
    | None, Some t ⇒ Some t
    | _, _ ⇒ None
  end.

Definition oto_list {X} `{OrderedType X} (s:option (set X)) :=
  match s with Some s ⇒ to_list s | None ⇒ nil end.

Fixpoint computeParameters (DL: list (set var)) (ZL:list (list var)) (AP:list (set var))
         (s:stmt) (an:ann (set var)) {struct s}
: ann (list var) × list (option (set var)) :=
  match s, an with
    | stmtLet x e s, ann1 _ an ⇒
      let (ar, r) := computeParameters DL ZL (addParam x DL AP) s an in
      (ann1 nil ar, r)
    | stmtIf x s t, ann2 _ ans ant ⇒
      let (ars, rs) := computeParameters DL ZL AP s ans in
      let (art, rt) := computeParameters DL ZL AP t ant in
      (ann2 nil ars art, zip ounion rs rt)
    | stmtApp f Y, ann0 lv ⇒ (ann0 nil, killExcept f AP)
    | stmtReturn x, ann0 _ ⇒ (ann0 nil, (mapi (fun _ _ ⇒ None) AP))
    | stmtExtern x f e s, ann1 _ an ⇒
      let (ar, r) := computeParameters DL ZL (addParam x DL AP) s an in
      (ann1 nil ar, r)
    | stmtFun Z s t, ann2 lv ans ant ⇒
      let DL´ := getAnn ans \ of_list Z in
      let (ars, rs) := computeParameters (DL´ :: DL)
                                        (Z :: ZL)
                                        (∅ :: addParams Z DL AP)
                                        s
                                        ans in
      let (art, rt) := computeParameters (DL´:: DL)
                                        (Z :: ZL)
                                        (∅:: AP)
                                        t
                                        ant in
      let a := ounion (hd None rs) (hd None rt) in
      let rs´ := addAdds (oget a) DL (tl rs) in
      let ur := zip ounion rs´ (tl rt) in
      (ann2 (oto_list a) ars art, ur)
    | s, a ⇒ (ann0 nil, nil)
  end.

Local Notation "≽" := (fstNoneOrR (flip Subset)).
Local Notation "≼" := (fstNoneOrR (Subset)).
Local Notation "A ≿ B" := (PIR2 (fstNoneOrR (flip Subset)) A B) (at level 60).

Instance fstNoneOrR_flip_Subset_trans {X} `{OrderedType X} : Transitive ≽.
Qed.

Instance fstNoneOrR_flip_Subset_trans2 {X} `{OrderedType X} : Transitive (fstNoneOrR Subset).
Qed.

Lemma trs_monotone (DL DL´ : list (option (set var))) ZL s lv a
 : trs DL ZL s lv a
   → DL ≿ DL´
   → trs DL´ ZL s lv a.


Lemma PIR2_restrict A B s
: A ≿ B
   → restrict A s ≿ B.

Lemma to_list_nil {X} `{OrderedType X}
  : to_list ∅ = nil.

Lemma trs_monotone3 (DL : list (option (set var))) AP AP´ ZL s lv a
 : trs DL (zip (fun Z a ⇒ match a with Some a ⇒ Z++to_list a | None ⇒ Z end) ZL AP) s lv a
   → PIR2 (fstNoneOrR Subset) AP AP´
   → trs DL (zip (fun Z a ⇒ match a with Some a ⇒ Z++to_list a | None ⇒ Z end) ZL AP´) s lv a.
    Opaque to_list.

Definition elem_eq {X} `{OrderedType X} (x y: list X) := of_list x [=] of_list y.

Instance elem_eq_refl {X} `{OrderedType X} : Reflexive elem_eq.
Qed.

Lemma trs_AP_seteq (DL : list (option (set var))) AP AP´ s lv a
 : trs DL AP s lv a
   → PIR2 elem_eq AP AP´
   → trs DL AP´ s lv a.

Lemma trs_AP_incl (DL : list (option (set var))) AP AP´ s lv a
 : trs DL AP s lv a
   → PIR2 (fun x y ⇒ of_list y ⊆ of_list x) AP AP´
   → trs DL AP´ s lv a.

Lemma trs_AP_incl´ (DL : list (option (set var))) AP AP´ s lv a
 : trs DL AP s lv a
   → PIR2 (fun x y ⇒ of_list x ⊆ of_list y) AP AP´
   → trs DL AP´ s lv a.

Definition map_to_list {X} `{OrderedType X} (AP:list (option (set X)))
  := List.map (fun a ⇒ match a with Some a ⇒ to_list a | None ⇒ nil end) AP.

Lemma PIR2_Subset_of_list (AP AP´: list (option (set var)))
: PIR2 (fstNoneOrR Subset) AP AP´
  → PIR2 (fun x y ⇒ of_list y ⊆ of_list x) (map_to_list AP´) (map_to_list AP).

Lemma trs_monotone3´ (DL : list (option (set var))) AP AP´ s lv a
 : trs DL (List.map oto_list AP) s lv a
   → PIR2 (fstNoneOrR Subset) AP AP´
   → trs DL (List.map oto_list AP´) s lv a.

Lemma PIR2_addParam DL AP x
  : length AP = length DL
    → PIR2 Subset AP (addParam x DL AP).

Lemma PIR2_map_some {X} R (AP AP´:list X)
: length AP = length AP´
  → PIR2 R AP AP´
  → PIR2 (fstNoneOrR R) (List.map Some AP) (List.map Some AP´).

Lemma PIR2_map_some_option {X} R (AP AP´:list X)
: length AP = length AP´
  → PIR2 R AP AP´
  → PIR2 (option_eq R) (List.map Some AP) (List.map Some AP´).

Lemma addParams_length Z DL AP
 : length DL = length AP
   → length (addParams Z DL AP) = length DL.

Lemma PIR2_ounion {X} `{OrderedType X} (A B C:list (option (set X)))
: length A = length B
  → length B = length C
  → PIR2 ≽ A C
  → PIR2 ≽ B C
  → PIR2 ≽ (zip ounion A B) C.

Lemma PIR2_ounion´ {X} `{OrderedType X} (A B C:list (option (set X)))
: length A = length B
  → length B = length C
  → PIR2 ≼ C A
  → PIR2 ≼ C B
  → PIR2 ≼ C (zip ounion A B).

Lemma PIR2_ounion_AB {X} `{OrderedType X} (A A´ B B´:list (option (set X)))
: length A = length A´
  → length B = length B´
  → length A = length B
  → PIR2 ≼ A A´
  → PIR2 ≼ B B´
  → PIR2 ≼ (zip ounion A B) (zip ounion A´ B´).

Lemma PIR2_option_eq_Subset_zip {X} `{OrderedType X} (A B C:list (option (set X)))
: length A = length B
  → length B = length C
  → PIR2 (option_eq Subset) C A
  → PIR2 (option_eq Subset) C B
  → PIR2 (option_eq Subset) C (zip ounion A B).

Lemma length_tl X (l:list X)
  : length (tl l) = length l - 1.

Definition lminus (s:set var) L := s \ of_list L.

Lemma addParam_zip_lminus_length DL ZL AP x
: length AP = length DL
  → length DL = length ZL
  → length (addParam x (zip lminus DL ZL) AP) = length DL.

Lemma addParams_zip_lminus_length DL ZL AP Z
: length AP = length DL
  → length DL = length ZL
  → length (addParams Z (zip lminus DL ZL) AP) = length DL.

Lemma computeParameters_length DL ZL AP s lv an´ LV
:live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → computeParameters (zip lminus DL ZL) ZL AP s lv = (an´, LV)
  → length AP = length DL
  → length DL = length ZL
  → length LV = length DL.


Inductive ifSndR {X Y} (R:X → Y → Prop) : X → option Y → Prop :=
  | ifsndR_None x : ifSndR R x None
  | ifsndR_R x y : R x y → ifSndR R x (Some y).

Lemma PIR2_ifSndR_right {X} `{OrderedType X} A B C
: PIR2 (ifSndR Subset) B A
→ PIR2 Subset C B
→ PIR2 (ifSndR Subset) C A.

Lemma ifSndR_zip_ounion {X} `{OrderedType X} A B C
: PIR2 (ifSndR Subset) C A
  → PIR2 (ifSndR Subset) C B
  → PIR2 (ifSndR Subset) C (zip ounion A B).

Lemma ifSndR_addAdds s DL A B
 : length DL = length A
   → PIR2 (ifSndR Subset) A B
   → PIR2 (ifSndR Subset) A (addAdds s DL B).

Lemma addParams_Subset Z DL AP
: length DL = length AP
  → PIR2 Subset AP (addParams Z DL AP).

Lemma computeParameters_AP_LV DL ZL AP s lv an´ LV
:live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → computeParameters (zip lminus DL ZL) ZL AP s lv = (an´, LV)
  → length AP = length DL
  → length DL = length ZL
  → PIR2 (ifSndR Subset) AP LV.

Inductive ifFstR {X Y} (R:X → Y → Prop) : option X → Y → Prop :=
  | IfFstR_None y : ifFstR R None y
  | IfFstR_R x y : R x y → ifFstR R (Some x) y.

Lemma ifFstR_zip_ounion {X} `{OrderedType X} A B C
: PIR2 (ifFstR Subset) A C
  → PIR2 (ifFstR Subset) B C
  → PIR2 (ifFstR Subset) (zip ounion A B) C.

Lemma ifFstR_addAdds s A B
: PIR2 (ifFstR Subset) B A
  → PIR2 (ifFstR Subset) (addAdds s A B) A.

Lemma addParam_Subset x DL AP
: PIR2 Subset AP DL
  → PIR2 Subset (addParam x DL AP) DL.

Lemma addParams_Subset2 Z DL AP
: PIR2 Subset AP DL
  → PIR2 Subset (addParams Z DL AP) DL.

Lemma computeParameters_LV_DL DL ZL AP s lv an´ LV
:live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → computeParameters (zip lminus DL ZL) ZL AP s lv = (an´, LV)
  → length AP = length DL
  → length DL = length ZL
  → PIR2 Subset AP (zip lminus DL ZL)
  → PIR2 (ifFstR Subset) LV (zip lminus DL ZL).

Lemma ounion_comm {X} `{OrderedType X} (s t:option (set X))
  : option_eq Equal (ounion s t) (ounion t s).

Lemma zip_PIR2 X Y (eqA:Y → Y → Prop) (f:X → X → Y) l l´
  : (∀ x y, eqA (f x y) (f y x))
    → PIR2 eqA (zip f l l´) (zip f l´ l).

Lemma PIR2_zip_ounion {X} `{OrderedType X} (b:list (option (set X))) b´
  : length b = length b´
    → PIR2 (fstNoneOrR Subset) b (zip ounion b b´).

Lemma PIR2_zip_ounion´ {X} `{OrderedType X} (b:list (option (set X))) b´
  : length b = length b´
    → PIR2 (fstNoneOrR Subset) b (zip ounion b´ b).

Definition ominus (s : set var) (t : option (set var)) := mdo t´ <- t; ⎣s \ t´ ⎦.


Lemma zip_ominus_contra DL b b´
  : length DL = length b
    → length b = length b´
    → PIR2 (fstNoneOrR Subset) b b´
    → zip ominus DL b ≿ zip ominus DL b´.

Lemma addParam_x DL AP x n ap´ dl
  : get (addParam x DL AP) n ap´
    → get DL n dl
    → x ∉ ap´ → x ∉ dl.

Lemma PIR2_not_in LV x DL AP
: length DL = length AP
  → PIR2 (ifSndR Subset) (addParam x DL AP) LV
  → ∀ (n : nat) (lv0 dl : set var),
       get LV n ⎣lv0 ⎦ → get DL n dl → x ∉ lv0 → x ∉ dl.

Lemma zip_bounded DL LV lv x
: length DL = length LV
  → bounded (List.map Some DL) lv
  → (∀ n lv dl, get LV n (Some lv) → get DL n dl → x ∉ lv → x ∉ dl)
  → bounded (zip (fun (s : set var) (t : option (set var)) ⇒ mdo t´ <- t; ⎣s \ t´ ⎦) DL LV) (lv \ {{ x }} ).

Lemma restrict_zip_ominus DL LV lv x al
: length DL = length LV
→ (∀ n lv dl, get LV n (Some lv) → get DL n dl → x ∉ lv → x ∉ dl)
→ al \ {{x}} ⊆ lv
→ restrict (zip ominus DL LV) al
 ≿ restrict (zip ominus DL LV) (lv \ {{x}}).

Lemma restrict_zip_ominus´ DL LV lv x al
: length DL = length LV
→ (∀ n lv dl, get LV n (Some lv) → get DL n dl → x ∉ lv → x ∉ dl)
→ al \ {{x}} ⊆ lv
→ restrict (zip ominus DL LV) al
 ≿ restrict (zip ominus DL LV) (lv \ {{x}}).

Lemma get_mapi_impl X Y L (f:nat→X→Y) n x k
 : get L n x
   → get (mapi_impl f k L) n (f (n+k) x).

Lemma get_mapi X Y L (f:nat→X→Y) n x
 : get L n x
   → get (mapi f L) n (f n x).

Lemma killExcept_get l AP s
: get AP (counted l) s →
  get (killExcept l AP) (counted l) (Some s).

Lemma restrict_get L s t n
: get L n (Some s)
  → s ⊆ t
  → get (restrict L t) n (Some s).

Transparent addAdds.

Lemma PIR2_addAdds s DL b
: length DL = length b
  → PIR2 ≼ b (addAdds s DL b).

Lemma computeParameters_trs DL ZL AP s an´ LV lv
: length DL = length ZL
  → length ZL = length AP
  → live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → computeParameters (zip lminus DL ZL) ZL AP s lv = (an´, LV)
  → PIR2 Subset AP (zip lminus DL ZL)
  → trs (restrict (zip ominus (zip lminus DL ZL) LV) (getAnn lv))
        (List.map oto_list LV) s lv an´.

Print Assumptions computeParameters_trs.

Definition oemp X `{OrderedType X} (s : option (set X)) :=
  match s with
    | ⎣s0 ⎦ ⇒ s0
    | ⎣⎦ ⇒ ∅
  end.


Lemma additionalParameters_live_monotone (LV´:list (option (set var))) DL ZL s an´ LV lv
: length DL = length ZL
  → live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → additionalParameters_live LV s lv an´
  → PIR2 (ifFstR Subset) LV´ (zip lminus DL ZL)
  → additionalParameters_live (List.map (@oemp var _) LV´) s lv an´.

Lemma computeParameters_live DL ZL AP s an´ LV lv
: length DL = length ZL
  → length ZL = length AP
  → live_sound FunctionalAndImperative (zip pair DL ZL) s lv
  → computeParameters (zip lminus DL ZL) ZL AP s lv = (an´, LV)
  → PIR2 Subset AP (zip lminus DL ZL)
  → additionalParameters_live (List.map (@oemp _ _) LV) s lv an´.