Require Import List Map Env AllInRel Exp AppExpFree RenamedApart.
Require Import IL Annotation AutoIndTac.
Require Import Liveness.Liveness LabelsDefined.
Require Import SpillSound DoSpill DoSpillRm SpillUtil ReconstrLive AnnP InVD SetUtil.
Require Import ToBeOutsourced.
Require Export SlotLiftParams.

Set Implicit Arguments.

Definition reconstr_live_do_spill
           (slot : var → var)
           (Λ : list (⦃var⦄ × ⦃var⦄))
           (ZL : list params)
           (G : ⦃var⦄)
           (s : stmt)
           (sl : spilling)
  : ann ⦃var⦄
  :=
    reconstr_live (slot_merge slot Λ)
                  ((slot_lift_params slot) ⊜ Λ ZL)
                  G
                  (do_spill slot s sl ZL Λ)
                  (do_spill_rm slot sl)
.

Lemma get_ofl_VD
      (ZL : 〔params〕)
      (F : 〔params × stmt〕)
      (VD : ⦃var⦄)
      (Z_VD : ∀ (Z : params) (n : nat), get ZL n Z → of_list Z ⊆ VD)
      (D D' Dt : ⦃var⦄)
      (ans : 〔ann (⦃var⦄ × ⦃var⦄)〕)
      (H6 : ❬F❭ = ❬ans❭)
      (H8 : Indexwise.indexwise_R (funConstr D Dt) F ans)
      (H13 : list_union (defVars ⊜ F ans) ∪ Dt [=] D')
      (ra_VD : D ∪ D' ⊆ VD)
  : ∀ (Z : params) (n : nat), get (fst ⊝ F ++ ZL) n Z → of_list Z ⊆ VD.
Proof.
  intros.
  decide (n < length F).
  -- apply get_in_range in l as [Zs get_Zs].
     assert (get_a := get_Zs).
     eapply get_length_eq in get_a as [a get_a];
       [ | apply H6].
     exploit H8 as fnCnstr; eauto.
     destruct fnCnstr as [fnCnstr _].

     assert (of_list (fst Zs) ⊆ fst (getAnn a)) as ofl. {
       clear - fnCnstr.
       apply eq_incl in fnCnstr as [fnCnstr _].
       rewrite <- fnCnstr.
       cset_tac.
     }
     assert (get_Zs' := get_Zs).
     eapply map_get_1 with (f:=fst) in get_Zs; eauto.
     eapply get_app with (L':=ZL) in get_Zs; eauto.
     eapply get_get_eq with (x':=Z) in get_Zs; eauto.
     subst Z.
     rewrite ofl, fnCnstr.
     rewrite <- ra_VD, <- H13.
     assert (of_list (fst Zs) ⊆ of_list (fst Zs) ∪ fst (getAnn a))
       as ofl' by (clear - ofl; cset_tac).
     assert (of_list (fst Zs) ⊆ list_union (defVars ⊜ F ans)) as ofl_def. {
       eapply incl_list_union.
       apply zip_get; eauto.
       unfold defVars.
       clear; cset_tac.
     }
     rewrite ofl_def.
     clear; cset_tac.
  -- apply not_lt in n0.
     rewrite <- map_length with (f:=fst) in n0.
     eapply get_app_right_ge with (L':=ZL) in n0; eauto.
Qed.

Lemma nth_rfmf
      (l : lab)
      (Λ : 〔⦃var⦄ × ⦃var⦄〕)
      (slot : var → var)
      (R_f M_f : ⦃var⦄)
      (H15 : get Λ (counted l) (R_f, M_f))
  : nth (counted l) (slot_merge slot Λ) ∅ [=] R_f ∪ map slot M_f .
Proof.
  eapply get_nth with (d:=(∅,∅)) in H15 as H15'.
  simpl in H15'.
  assert ((fun RM
           ⇒ fst RM ∪ map slot (snd RM)) (nth l Λ (∅,∅))
          = (fun RM
             ⇒ fst RM ∪ map slot (snd RM)) (R_f,M_f))
    as H_sms. {
    f_equal; simpl; [ | f_equal];
      rewrite H15'; simpl; eauto.
  }
  unfold slot_merge.
  rewrite <- map_nth in H_sms.
  simpl in H_sms.
  assert (l < length ((fun RM : ⦃var⦄ × ⦃var⦄
                       ⇒ fst RM ∪ map slot (snd RM)) ⊝ Λ))
    as l_len. {
    apply get_length in H15.
    clear - H15; eauto with len.
  }
  assert (nth l ((fun RM : ⦃var⦄ × ⦃var⦄
                  ⇒ fst RM ∪ map slot (snd RM)) ⊝ Λ) ∅
          = R_f ∪ map slot M_f)
    as H_sms'. {
    rewrite nth_indep with (d':=∅ ∪ map slot ∅).
    × exact H_sms.
    × eauto with len.
  }
  simpl.
  rewrite H_sms'.
  reflexivity.
Qed.


Lemma al_sub_RfMf
      (als : list (ann ⦃var⦄))
      (rms : list (⦃var⦄ × ⦃var⦄))
      (al : ann ⦃var⦄)
      (R M : ⦃var⦄)
      (n : nat)
  : get rms n (R,M)
    → get als n al
    → PIR2 Equal (merge ⊝ rms) (getAnn ⊝ als)
    → getAnn al ⊆ R ∪ M.
Proof.
  intros get_rm get_al H16.
  general induction get_rm;
    try invc get_al; invc H16;
      unfold merge in *; simpl in *; eauto.
  rewrite pf; eauto.
Qed.

Lemma al_eq_RfMf

      (als : list (ann ⦃var⦄))
      (rms : list (⦃var⦄ × ⦃var⦄))
      (al : ann ⦃var⦄)
      (R M : ⦃var⦄)
      (n : nat)
  : get rms n (R,M)
    → get als n al
    → merge ⊝ rms = getAnn ⊝ als
    → getAnn al [=] R ∪ M .
Proof.
  intros get_rm get_al H16.
  general induction get_rm;
    try invc get_al; invc H16;
      simpl in *; eauto.
Qed.

Lemma ofl_slp_sub_rm
      (al : ann ⦃var⦄)
      (R M : ⦃var⦄)
      (Z : params)
      (slot : var → var)
  : getAnn al ⊆ R ∪ M
    → of_list Z ⊆ getAnn al
    → of_list (slot_lift_params slot (R,M) Z) ⊆ R ∪ map slot M .
Proof.
  intros ofl_in_rm H2'.
  rewrite <- H2' in ofl_in_rm.
  induction Z;
    simpl in *; eauto.
  - clear; cset_tac.
  - assert (of_list Z ⊆ getAnn al) as ofl_al
        by (rewrite <- H2'; clear; cset_tac).
    assert (of_list Z ⊆ R ∪ M) as ofl_rm
        by (rewrite <- ofl_in_rm; clear; cset_tac).
    assert (a ∈ M → slot a ∈ map slot M)
      as slot_a_in. {
      intro a_in.
      apply in_singleton.
      rewrite <- map_singleton; eauto.
      apply lookup_set_incl; eauto.
      apply incl_singleton; eauto.
    }
    specialize (IHZ ofl_rm ofl_al).
    decide (a ∈ R ∩ M); simpl.
    + apply inter_iff in i as [a_fst a_snd].
      rewrite IHZ.
      apply slot_a_in in a_snd.
      clear - a_fst a_snd; cset_tac.
    + decide (a ∈ R); simpl.
      × rewrite IHZ.
        clear - i; cset_tac.
      × rewrite add_union_singleton in ofl_in_rm.
        eapply union_incl_split2 in ofl_in_rm as [ofl_in_rm _].
        eapply in_singleton in ofl_in_rm.
        assert (a ∈ M) as a_in
            by (clear - ofl_in_rm n0; cset_tac).
        apply slot_a_in in a_in.
        rewrite IHZ.
        clear - a_in; cset_tac.
Qed.

Lemma nth_mark_elements
      (l : lab)
      (ZL : list params)
      (Λ : list (⦃var⦄ × ⦃var⦄))
      (rm : ⦃var⦄ × ⦃var⦄)
      (Z : params)
  :
    get ZL l Z
    → get Λ l rm
    → nth l (mark_elements ⊜ ZL ((fun RM : ⦃var⦄ × ⦃var⦄ ⇒ fst RM ∩ snd RM) ⊝ Λ)) nil
      = mark_elements Z ((fun RM : ⦃var⦄ × ⦃var⦄ ⇒ fst RM ∩ snd RM) rm)
.
Proof.
  intros get_Z get_rm.
  apply get_nth.
  eapply zip_get; eauto.
  eapply map_get_eq; eauto.
Qed.

Lemma sla_extargs_slp_length
      (slot : var → var)
      RM RMapp
      (ZL : list params)
      (Z : params)
      (l : lab)
      (Λ : list (⦃var⦄ × ⦃var⦄))
      (Y : args)
  :
    length Y = length Z →
    ❬slot_lift_args slot RM RMapp Y Z❭ = ❬slot_lift_params slot RM Z❭ .
Proof.
  intros Len.
  general induction Len; simpl; eauto.
  repeat cases; simpl; eauto.
Qed.