Lvc.Coherence.DelocationAlgoIsCalled

Require Import Util LengthEq IL RenamedApart LabelsDefined OptionR.
Require Import Keep Drop Take Restrict SetOperations OUnion.
Require Import Annotation Liveness.Liveness Coherence Delocation.
Require Import AddParam AddAdd MoreListSet DelocationAlgo.

Set Implicit Arguments.

Lemma computeParameters_isCalled_Some_F' b Lv ZL AP als D Z F s alb l
      k k' x0 x1 Zs
      (IH : k Zs,
          get F k Zs
           (ZL : params) (Lv AP : var) (lv : ann var)
            (n : nat) (D : var) (Z : params) (p : ؟ var),
            live_sound Imperative ZL Lv (snd Zs) lv
            AP = Lv
            Lv = ZL
            isCalled b (snd Zs) (LabI n)
            get Lv n D
            get ZL n Z
            get (snd (computeParameters (Lv \\ ZL) ZL AP (snd Zs) lv)) n p
             Za : var, p = Za D \ of_list Z \ Za getAnn lv)
      (LEN1 : AP = Lv) (LEN2 : Lv = ZL) (LEN3 : F = als)
      (GetDL : get (getAnn als ++ Lv) l D) (GetZL : get (fst F ++ ZL) l Z)
      (LS:live_sound Imperative (fst F ++ ZL) (getAnn als ++ Lv) s alb)
      (LSF : (n : nat) (Zs : params × stmt) (a : ann var),
          get F n Zs
          get als n a
          live_sound Imperative (fst F ++ ZL) (getAnn als ++ Lv) (snd Zs) a)
      (INCL: (n : nat) (Zs : params × stmt) (a : ann var),
          get F n Zs get als n a of_list (fst Zs) getAnn a True)
      (GetLV : get (olu F als Lv ZL AP s alb) l x0)
      (GetF : get F k Zs) (GetAls : get als k x1)
      (IC : isCalled b (snd Zs) (LabI k'))
      (CC: callChain (isCalled b) F (LabI k') (LabI l))
  : Za : var,
     addAdd
       (list_union (oget take F (olu F als Lv ZL AP s alb))
         list_union (fst of_list F)) (D \ of_list Z) x0 =
      Za
     D \ of_list Z \ Za
      getAnn x1 \ of_list (fst Zs) \
       (list_union (oget take F (olu F als Lv ZL AP s alb))
                    list_union (fst of_list F)).
Proof.
  general induction CC.
  - destruct (@get_in_range _ (snd
                                 (computeParameters ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                                    (fst F ++ ZL) (tab {} F ++ AP) (snd Zs) x1)) l0)
      as [pF GETpF].
    rewrite computeParameters_length; [ |eauto | eauto with len | eauto with len].
    eapply get_range in GetDL. eauto.
    edestruct (IH k Zs); try eapply GETpF;
      eauto using get_app_right, map_get_1 with len;
      dcr; subst.
    edestruct get_olist_union_A' as [? [? ?]]; try eapply GetLV;
      eauto using map_get_1, zip_get.
    eapply computeParametersF_length; eauto with len.
    rewrite computeParameters_length; eauto with len.
    subst; simpl. eexists; split; eauto.
    rewrite <- H0, <- H1.
    repeat rewrite minus_union.
    assert (of_list (fst Zs) list_union (fst of_list F)). {
      eapply incl_list_union. eapply map_get_1; eauto. reflexivity.
    }
    revert H; clear_all; cset_tac.
  - inv_get.
    exploit IHCC; try eapply H0; eauto.
    dcr. eexists; split; eauto.
    rewrite H5.
    destruct (@get_in_range _ (snd
                                 (computeParameters ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                                    (fst F ++ ZL) (tab {} F ++ AP) (snd Zs0) x1)) k'0)
      as [pF' GETpF'].
    rewrite computeParameters_length; [ |eauto | eauto with len | eauto with len].
    rewrite app_length, map_length. eapply get_range in H1. omega.
    exploit (IH k0 Zs0); try eapply GETpF'; eauto using get_app, map_get_1 with len.
    dcr; subst. rewrite <- H7.
    assert (x3 list_union (oget take F
                                  (olist_union (snd computeParametersF F als Lv ZL AP)
                                               (snd
                                                  (computeParameters
                                                     ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                                     (fst F ++ ZL) (tab {} F ++ AP) s alb))))).
    {
      exploit (@get_olist_union_A _ _ (snd computeParametersF F als Lv ZL AP));
        [| eapply GETpF' | | ]. instantiate (1:=k0).
      eapply map_get_1. eapply zip_get_eq; [| | reflexivity]. eauto. eauto.
      instantiate (1:=(snd
                         (computeParameters ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                            (fst F ++ ZL) (tab {} F ++ AP) s alb))).
      rewrite computeParameters_length; eauto.
      eapply computeParametersF_length; eauto with len.
      eauto with len. eauto with len.
      dcr.
      eapply incl_list_union. eapply map_get_1.
      eapply get_take; try eapply H6; eauto using get_range. eauto.
    }
    rewrite H2.
    assert (of_list (fst Zs0) list_union (fst of_list F)). {
      eapply incl_list_union. eapply map_get_1.
      instantiate (1:=Zs0). eauto. eauto.
    }
    revert H3; clear_all; cset_tac.
Qed.

Lemma computeParameters_isCalled_Some b ZL Lv AP s lv n D Z p
  : live_sound Imperative ZL Lv s lv
     length AP = length Lv
     length Lv = length ZL
     isCalled b s (LabI n)
     get Lv n D
     get ZL n Z
     get (snd (computeParameters (Lv \\ ZL) ZL AP s lv)) n p
     Za, p = Some Za D \ of_list Z \ Za (getAnn lv).
Proof.
  revert ZL Lv AP lv n D Z p.
  sind s; destruct s;
    intros ZL Lv AP lv n D Z p LS LEN1 LEN2 IC GetDL GetZL GetLV;
    simpl in × |- *; inv LS; invt isCalled;
      repeat let_case_eq; repeat let_pair_case_eq; subst; simpl in ×.
  - edestruct (IH s) as [Za [A B]]; try eapply GetLV; eauto with len;
      subst; simpl.
    eexists; split; eauto.
    inv_get.
    exploit (@computeParameters_AP_LV Lv ZL (addParam x (Lv \\ ZL) AP));
      try eapply H2; eauto with len.
    PIR2_inv. unfold addParam in H3. inv_get.
    rewrite <- H7.
    revert H10 B. clear_all; cases; intros; cset_tac.
  - inv_get.
    edestruct (IH s1) as [? [? SUB]]; eauto; subst.
    setoid_rewrite <- H8. setoid_rewrite <- SUB.
    destruct x0;
      eexists; simpl; split; eauto; clear_all; cset_tac.
  - inv_get.
    edestruct (IH s2) as [? [? SUB]]; eauto; subst.
    setoid_rewrite <- H9. setoid_rewrite <- SUB.
    destruct x;
      eexists; simpl; split; eauto; clear_all; cset_tac.
  - simpl in ×. unfold keep in GetLV.
    inv_get.
    cases; eauto.
    eexists; split; eauto.
    rewrite <- H3. eauto with cset.
  - lnorm. inv_get.
    invc H4.
    + exploit (computeParameters_length (tab {} F ++ AP) H1) as Len;
        [ eauto with len | eauto with len | ].
      assert (LE:F + n < snd
                           (computeParameters ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                              (fst F ++ ZL) (tab {} F ++ AP) s alb)).
      rewrite Len, app_length, map_length. exploit (get_range GetDL). omega.
      destruct (get_in_range _ LE) as [pF GETpF].
      edestruct (IH s) with (AP:=tab {} F ++ AP); eauto.
      eauto with len. eauto with len.
      eapply get_app_right; eauto using map_get_1.
      orewrite (n+0 = n); eauto.
      eapply get_app_right; eauto using map_get_1.
      rewrite map_length; eauto. dcr; subst.
      edestruct (@get_olist_union_b _ _ (snd computeParametersF F als Lv ZL AP))
        as [? [? ?]]; try eapply GETpF.
      eapply computeParametersF_length; eauto.
      get_functional.
      eexists; split; try reflexivity.
      rewrite <- H0, <- H8, <- H4.
      clear_all; cset_tac.
    + inv_get.
      destruct (@get_in_range _ (snd
                                   (computeParameters ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                                      (fst F ++ ZL) (tab {} F ++ AP) s alb)) k)
        as [ps GETps]; eauto.
      rewrite computeParameters_length; eauto with len.
      exploit (IH s); try eapply GETps; eauto using get_app, map_get_1 with len.
      dcr; subst.
      setoid_rewrite <- H8. setoid_rewrite <- H13.
      assert (x2 list_union (oget take F
                                    (olist_union (snd computeParametersF F als Lv ZL AP)
                                                 (snd
                                                    (computeParameters
                                                       ((getAnn als ++ Lv) \\ (fst F ++ ZL))
                                                       (fst F ++ ZL) (tab {} F ++ AP) s alb))))
                  list_union (fst of_list F)). {
        exploit (@get_olist_union_b _ _ (snd computeParametersF F als Lv ZL AP));
          try eapply GETps.
        eapply computeParametersF_length; eauto with len.
        rewrite computeParameters_length; eauto with len.
        dcr. eapply incl_union_left.
        eapply incl_list_union. eapply map_get_1.
        eapply get_take; eauto using get_range.
        eauto.
      }
      clear H8 H13 LS GETps. setoid_rewrite H10. clear H7 H10.
      eapply computeParameters_isCalled_Some_F'; eauto.
      intros. eapply (IH (snd Zs0)); eauto.
      eapply get_app_right; eauto. orewrite (n + 0 = n); eauto.
      eapply get_app_right; eauto. eauto with len.
      intros; edestruct H6; eauto.
Qed.

Lemma computeParameters_isCalled_get_Some b Lv ZL AP s lv n p A D Z
  : live_sound Imperative ZL Lv s lv
     length AP = length Lv
     length Lv = length ZL
     isCalled b s (LabI n)
     n < snd (computeParameters (Lv \\ ZL) ZL AP s lv)
     get Lv n D
     get ZL n Z
     get (olist_union A (snd (computeParameters (Lv \\ ZL) ZL AP s lv))) n p
     ( (n0 : nat) (a : ؟var),
          get A n0 a a = snd (computeParameters (Lv \\ ZL) ZL AP s lv))
     Za, p = Some Za D \ of_list Z \ Za (getAnn lv).
Proof.
  intros LS LEN1 LEN2 IC LE GETDL GETZL GET LEN3.
  destruct (get_in_range _ LE); eauto.
  edestruct computeParameters_isCalled_Some; eauto; dcr; subst.
  edestruct get_olist_union_b; eauto; dcr.
  get_functional.
  eexists; split; try reflexivity. rewrite <- H1, <- H2; eauto.
Qed.

Lemma computeParameters_isCalledFrom_get_Some b Lv ZL AP F alv s lv p Da Zs l
      (LSF : (n : nat) (Zs : params × stmt) (a : ann var),
          get F n Zs
          get alv n a
          live_sound Imperative (fst F ++ ZL) (getAnn alv ++ Lv) (snd Zs) a)
       (INCL: (n : nat) (Zs : params × stmt) (a : ann var),
          get F n Zs get alv n a of_list (fst Zs) getAnn a True)
  : live_sound Imperative (fst F ++ ZL) (getAnn alv ++ Lv) s lv
     length AP = length Lv
     length Lv = length ZL
     length F = length alv
     isCalledFrom (isCalled b) F s (LabI l)
     get alv l Da
     get F l Zs
     get (olist_union (snd computeParametersF F alv Lv ZL AP)
                       (snd (computeParameters ((getAnn alv ++ Lv) \\ (fst F ++ ZL))
                                               (fst F ++ ZL) (tab {} F ++ AP)
                                               s lv))) l p
     Za, p = Some Za getAnn Da \ of_list (fst Zs) \ Za \
                                 list_union (oget take F (olu F alv Lv ZL AP s lv))
                                 \ list_union (fst of_list F) (getAnn lv).
Proof.
  intros LS LEN1 LEN2 LEN3 [[n] [IC CC]] GETDL GETZL GET.
  exploit callChain_range' as LE; eauto using get_range. simpl in ×.
  assert (NLE:n < snd (computeParameters ((getAnn alv ++ Lv)
                                     \\ (fst F ++ ZL))
                                  (fst F ++ ZL)
                                  (tab {} F ++ AP) s lv)).
  rewrite computeParameters_length; eauto with len.
  destruct (get_in_range _ NLE); eauto.
  assert (LE':n < getAnn alv ++ Lv).
  rewrite app_length, map_length. omega.
  destruct (get_in_range _ LE'); eauto.
  assert (LE'':n < fst F ++ ZL).
  rewrite app_length, map_length. omega.
  destruct (get_in_range _ LE''); eauto.
  edestruct computeParameters_isCalled_Some; try eapply g; eauto; dcr; subst.
  eauto with len. eauto with len.
  edestruct get_olist_union_b; eauto; dcr.
  intros.
  eapply computeParametersF_length; eauto.
  eapply computeParameters_length; eauto with len.
  setoid_rewrite <- H1.
  inv CC.
  - inv_get. eexists; split; eauto.
    rewrite H2. clear_all; cset_tac.
  - inv_get.
    exploit computeParameters_isCalled_Some_F'; try eapply H4; try eapply H5;
      eauto using get_app, map_get_1.
    intros. eapply computeParameters_isCalled_Some; eauto.
    dcr. destruct p; simpl in *; invc H8.
    eexists; split; [ reflexivity | ].
    rewrite H2.
    assert (Incl:x (list_union (oget take F (olu F alv Lv ZL AP s lv))
                              list_union (fst of_list F))). {
      eapply incl_union_left.
      eapply incl_list_union.
      eapply map_get_1. eapply get_take; eauto using get_range. reflexivity.
    }
    rewrite Incl. rewrite <- H9.
    rewrite union_comm.
    rewrite <- minus_union.
    clear_all; cset_tac.
Qed.