Lvc.IL.Annotation

Require Import Util LengthEq Get Drop Map CSet MoreList DecSolve AllInRel.
Require Import Var Val Exp Env IL.
Require Import PartialOrder Terminating .

Set Implicit Arguments.

Inductive ann (A:Type) : Type :=
| ann0 (a:A) : ann A
| ann1 (a:A) (sa:ann A) : ann A
| ann2 (a:A) (sa:ann A) (ta:ann A) : ann A
| annF (a:A) (sa:list (ann A)) (ta:ann A).

Instance Ann_size A : Size (ann A). gen_Size. Defined.

Definition getAnn {A} (a:ann A) : A :=
  match a with
    | ann0 aa
    | ann1 a _a
    | ann2 a _ _a
    | annF a _ _a
  end.

Definition setTopAnn A (s:ann A) (a:A) : ann A :=
  match s with
   | ann0 _ann0 a
   | ann1 _ s'ann1 a s'
   | ann2 _ s1 s2ann2 a s1 s2
   | annF _ s1 s2annF a s1 s2
   end.

Fixpoint setAnn A (a:A) (s:stmt) : ann A :=
  match s with
    | stmtLet x e s0ann1 a (setAnn a s0)
    | stmtIf e s1 s2ann2 a (setAnn a s1) (setAnn a s2)
    | stmtApp l Yann0 a
    | stmtReturn eann0 a
    | stmtFun s0 s1annF a (List.map (snd (setAnn a)) s0) (setAnn a s1)
  end.

Lemma getAnn_setTopAnn A (an:ann A) a
 : getAnn (setTopAnn an a) = a.
Proof.
  destruct an; eauto.
Qed.

Lemma setTopAnn_eta A (an:ann A) a
  : getAnn an = a
     setTopAnn an a = an.
Proof.
  intros; destruct an; simpl in *; subst; eauto.
Qed.

Fixpoint mapAnn X Y (f:XY) (a:ann X) : ann Y :=
  match a with
    | ann0 aann0 (f a)
    | ann1 a anann1 (f a) (mapAnn f an)
    | ann2 a an1 an2ann2 (f a) (mapAnn f an1) (mapAnn f an2)
    | annF a an1 an2annF (f a) (List.map (mapAnn f) an1) (mapAnn f an2)
  end.

Lemma getAnn_mapAnn A A' (f:AA') (a:ann A)
  : getAnn (mapAnn f a) = f (getAnn a).
Proof.
  general induction a; simpl; eauto.
Qed.

Inductive annotation {A:Type} : stmt ann A Prop :=
| antExp x e s a sa
  : annotation s sa
     annotation (stmtLet x e s) (ann1 a sa)
| antIf x s t a sa ta
  : annotation s sa
     annotation t ta
     annotation (stmtIf x s t) (ann2 a sa ta)
| antGoto l Y a
  : annotation (stmtApp l Y) (ann0 a)
| antReturn x a
  : annotation (stmtReturn x) (ann0 a)
| antLet s t a sa ta
  : length s = length sa
     ( n s' sa', get sa n sa' get s n s' annotation (snd s') sa')
     annotation t ta
     annotation (stmtFun s t) (annF a sa ta).

Definition indexwise_R_dec' {A} {B} {R:ABProp} LA LB (Rdec:( n a b, get LA n a get LB n b Computable (R a b)))
: Computable ( n a b, get LA n a get LB n b R a b).
Proof.
unfold Computable. revert LA LB Rdec. fix 2. intros LA LB Rdec.
destruct LA, LB; try now left; isabsurd.
intros. destruct (Rdec 0 a b).
- eauto using get.
- eauto using get.
- destruct (indexwise_R_dec' LA LB).
  + intros. eauto using get.
  + left. hnf; intros. destruct n; inv H; inv H0; eauto.
  + right; intro HH. eapply n; hnf; intros; eapply HH; eauto using get.
- right; intro. eapply n; hnf; intros. eapply H; eauto using get.
Defined.

Instance annotation_dec_inst {A} {s} {a} : Computable (@annotation A s a).
Proof.
  revert a. sind s; destruct s; destruct a;
  try (now left; econstructor; eauto);
  try (now right; inversion 1; eauto).
  edestruct (IH); eauto;
    try (now left; econstructor; eauto);
    try (now right; inversion 1; eauto); eauto.
  edestruct (IH s1); edestruct (IH s2);
    try (now left; econstructor; eauto);
    try (now right; inversion 1; eauto); eauto.
  edestruct (IH); eauto;
    try (now left; econstructor; eauto);
    try (now right; inversion 1; eauto); eauto.
  decide (length F = length sa); try dec_solve.
  edestruct (IH s); try dec_solve; eauto.
  destruct (@indexwise_R_dec' _ _ (fun a b ⇒ @annotation A (snd a) b) F sa);
    try dec_solve.
  intros. eapply IH; eauto.
  Grab Existential Variables. eauto. eauto.
Defined.

Lemma setAnn_annotation A (a:A) s
  : annotation s (setAnn a s).
Proof.
  sind s; destruct s; simpl; eauto using @annotation.
  - econstructor; eauto with len.
    intros; inv_get; unfold comp; simpl; eauto.
Qed.

Inductive ann_R {A B} (R:ABProp) : ann A ann B Prop :=
| annLt0 a b
  : R a b
     ann_R R (ann0 a) (ann0 b)
| annLt1 a b an bn
  : R a b
     ann_R R an bn
     ann_R R (ann1 a an) (ann1 b bn)
| annLt2 a ans ant b bns bnt
  : R a b
     ann_R R ans bns
     ann_R R ant bnt
     ann_R R (ann2 a ans ant) (ann2 b bns bnt)
| annLtF a ans b bns ant bnt
  : R a b
     length ans = length bns
     ( n a b, get ans n a get bns n b ann_R R a b)
     ann_R R ant bnt
     ann_R R (annF a ans ant) (annF b bns bnt).

Lemma ann_R_get A B (R: A B Prop) a b
: ann_R R a b
   R (getAnn a) (getAnn b).
Proof.
  intros. inv H; eauto.
Qed.

Instance ann_R_refl {A} {R} `{Reflexive A R} : Reflexive (ann_R R).
Proof.
  hnf in H.
  hnf; intros. sinduction x; eauto using ann_R; try econstructor; eauto.
  - intros. get_functional; subst. eapply H; eauto.
Qed.

Instance ann_R_sym {A} {R} `{Symmetric A R} : Symmetric (ann_R R).
Proof.
  hnf in H.
  hnf; intros. general induction H0; eauto using ann_R; econstructor; eauto.
Qed.

Instance ann_R_trans A R `{Transitive A R} : Transitive (ann_R R).
Proof.
  hnf; intros ? ? ? B C.
  general induction B; inv C; econstructor; eauto.
  - congruence.
  - intros. edestruct get_length_eq; try eapply H0; eauto.
Qed.

Instance ann_R_Equivalence A R `{Equivalence A R} : Equivalence (ann_R R).
Proof.
  econstructor.
  - hnf; intros; reflexivity.
  - hnf; intros; symmetry; eauto.
  - hnf; intros; etransitivity; eauto.
Qed.

Instance ann_R_anti A R Eq `{EqA:Equivalence _ Eq} `{@Antisymmetric A Eq EqA R}
  : @Antisymmetric _ (ann_R Eq) _ (ann_R R).
Proof.
  intros ? ? B C. general induction B; inv C; eauto 20 using @ann_R.
Qed.

Instance ann_R_ann1_pe_morphism X `{OrderedType X}
: Proper (@pe X _ ==> ann_R (@pe X _) ==> ann_R (@pe X _)) (@ann1 _).
Proof.
  unfold Proper, respectful; intros.
  econstructor; eauto.
Qed.

Instance ordered_type_lt_dec A `{OrderedType A} (a b: A)
: Computable (_lt a b).
pose proof (_compare_spec a b).
destruct (_cmp a b).
right; inv H0. hnf; intros. eapply (lt_not_eq H2 H1).
left. inv H0; eauto.
right; inv H0. intro. eapply (lt_not_gt H1 H2).
Defined.

Instance ann_R_dec A B (R:ABProp)
         `{ a b, Computable (R a b)} (a:ann A) (b:ann B) :
  Computable (ann_R R a b).
Proof.
  revert b.
  sinduction a; destruct b; try dec_solve.
  + decide (R a a0); dec_solve.
  + decide (R a a0); try dec_solve.
    edestruct (X x); hnf in *;
    try eassumption; try dec_solve.
  + decide (R a a0); try dec_solve.
    edestruct (X x1); try dec_solve; eauto.
    edestruct (X x2); try dec_solve; eauto.
  + decide (R a a0); try dec_solve.
    decide (length sa = length sa0); try dec_solve.
    edestruct (X x); try dec_solve; eauto.
    destruct (@indexwise_R_dec' _ _ (ann_R R) sa sa0); try dec_solve.
    intros. eapply X; eauto.
Defined.

Instance PartialOrder_ann Dom `{PartialOrder Dom}
: PartialOrder (ann Dom) := {
  poLe := ann_R poLe;
  poLe_dec := @ann_R_dec _ _ poLe poLe_dec;
  poEq := ann_R poEq;
  poEq_dec := @ann_R_dec _ _ poEq poEq_dec
}.
Proof.
  - intros. general induction H0; eauto using @ann_R, poLe_refl.
Defined.

Instance getAnn_ann_R_morphism A (R:AAProp)
: Proper (ann_R R ==> R) (getAnn).
Proof.
  unfold Proper, respectful; intros.
  inv H; simpl; eauto.
Qed.

Hint Extern 20 (ann_R _ ?a ?a') ⇒ progress (first [ has_evar a | has_evar a' | reflexivity ]).

Create HintDb ann discriminated.

Hint Extern 1 ⇒
match goal with
| [ |- context [ getAnn (mapAnn _ _) ] ] ⇒ setoid_rewrite getAnn_mapAnn
end : ann.

Hint Extern 10 ⇒
match goal with
| [ H : ann_R poLe ?a ?b, H': ann_R poLe ?b ?c |- ann_R poLe ?a ?c ] ⇒
  etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H': ann_R poLe ?b ?c, H'' : poLe ?c ?d |- poLe ?a ?d ] ⇒
  etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : ann_R poLe ?a ?b, H': ann_R poLe ?b ?c, H'' : ann_R poLe ?c ?d |- ann_R poLe ?a ?d ] ⇒
  etransitivity; [ eapply H | etransitivity; [ eapply H' | eapply H''] ]
| [ H : poLe ?a ?b, H': ann_R poLe ?b ?c |- poLe ?a ?c ] ⇒
  etransitivity; [ eapply H | eapply H' ]
| [ H : poLe ?a ?b, H' : ann_R poLe ?b ?c, H'' : ¬ poEq ?b ?c |- poLt ?a ?c ] ⇒
  rewrite H; eapply poLt_intro; [ eapply H' | eapply H'']
end.

Lemma ann_R_annotation s A B (R : A B Prop) (a:ann A) (b:ann B)
  : annotation s a
     ann_R R a b
     annotation s b.
Proof.
  intros Ann AnnR.
  general induction Ann; inv AnnR; eauto using @annotation.
  - econstructor; eauto with len.
    intros. edestruct (get_length_eq _ H2 (eq_sym H6)); eauto.
Qed.

Lemma setTopAnn_annotation s A (an:ann A) a
  : annotation s an
     annotation s (setTopAnn an a).
Proof.
  intros. inv H; simpl; eauto using @annotation.
Qed.

Lemma ann_R_setTopAnn A B (R: A B Prop) (a:A) (b:B) an bn
  : R a b
     ann_R R an bn
     ann_R R (setTopAnn an a) (setTopAnn bn b).
Proof.
  intros. inv H0; simpl; econstructor; eauto.
Qed.

Lemma poLe_setTopAnn A `{PartialOrder A} (a b:A) an bn
  : poLe a b
     poLe an bn
     poLe (setTopAnn an a) (setTopAnn bn b).
Proof.
  intros. eapply ann_R_setTopAnn; eauto.
Qed.

Instance getAnn_poLe Dom `{PartialOrder Dom}
  : Proper (poLe ==> poLe) getAnn.
Proof.
  unfold Proper, respectful; intros.
  inv H0; simpl; eauto.
Qed.

Instance getAnn_poEq Dom `{PartialOrder Dom}
  : Proper (poEq ==> poEq) getAnn.
Proof.
  unfold Proper, respectful; intros.
  inv H0; simpl; eauto.
Qed.

Lemma getAnn_mapAnn_map (A B:Type) (f:AB) L
  : getAnn mapAnn f L = f getAnn L.
Proof.
  rewrite map_map. setoid_rewrite getAnn_mapAnn.
  rewrite <- map_map. reflexivity.
Qed.

Lemma terminating_ann Dom `{PO:PartialOrder Dom}
  : Terminating Dom poLt
     Terminating (ann Dom) poLt.
Proof.
  intros Trm a.
  econstructor. intros ? [A _].
  induction A.
  - specialize (Trm b).
    general induction Trm.
    econstructor. intros ? [A B].
    inv A.
    eapply H0; eauto. split; eauto.
    intro. eapply B. econstructor. eauto.
  - pose proof (Trm b) as FST. clear A H.
    rename IHA into SND.
    assert (poLe bn bn) by reflexivity.
    revert H. generalize bn at 2 3.
    induction FST as [? ? FST].
    assert (poLe x x) by reflexivity.
    revert H0. generalize x at 2 3.
    induction SND as [? ? SND].
    intros.
    econstructor; intros ? [A B].
    inv A.
    decide (poEq bn bn0).
    + decide (poEq x1 b).
      exfalso; eapply B; econstructor; eauto.
      eapply FST; eauto.
    + eapply (SND bn0); eauto.
  - clear H A1 A2 ans ant a.
    assert (poLe bns bns) by reflexivity.
    revert H. generalize bns at 2 3.
    assert (poLe bnt bnt) by reflexivity.
    revert H. generalize bnt at 2 3.
    assert (poLe b b) by reflexivity.
    revert H. generalize b at 2 3.
    specialize (Trm b).
    induction Trm.
    induction IHA1.
    induction IHA2.
    intros.
    econstructor; intros ? [A B].
    inv A.
    decide (poEq b b0).
    + decide (poEq bns bns0).
      × decide (poEq bnt bnt0).
        exfalso; apply B; econstructor; eauto.
        eapply (H4 bnt0); eauto.
      × eapply (H2 bns0); eauto.
    + eapply (H0 b0); eauto.
  - clear H A.
    pose proof (Trm b) as FST.
    rename IHA into SND.
    assert (TRD:terminates poLt bns). {
      eapply terminates_list_get.
      intros. symmetry in H0; edestruct get_length_eq; eauto.
    }
    clear H0 H1 H2.
    assert (poLe bns bns) by reflexivity.
    revert H. generalize bns at 2 3.
    assert (poLe bnt bnt) by reflexivity.
    revert H. generalize bnt at 2 3.
    assert (poLe b b) by reflexivity.
    revert H. generalize b at 2 3.
    induction FST.
    induction SND.
    induction TRD.
    intros.
    econstructor; intros ? [A B].
    inv A.
    decide (poEq b b0).
    + decide (poEq bns bns0).
      × decide (poEq bnt bnt0).
        exfalso; apply B; eauto. econstructor; eauto.
        intros. eapply PIR2_nth in p0; eauto.
        dcr. get_functional. eauto.
        eapply (H2 bnt0); eauto.
      × eapply PIR2_get in H14; eauto.
        eapply (H4 bns0); eauto.
    + eapply PIR2_get in H14; eauto.
      eapply (H0 b0); eauto.
Qed.

Lemma list_get_eq A (L L':list A)
  : length L = length L'
     ( n a b, get L n a get L' n b a = b)
     L = L'.
Proof.
  intros. length_equify. general induction H; f_equal; eauto using get.
Qed.

Lemma ann_R_eq A (a b:ann A)
  : ann_R eq a b a = b.
Proof.
  split; intros; subst; eauto.
  induction H; subst; eauto.
  f_equal. eapply list_get_eq; eauto.
Qed.

Lemma setTopAnn_inv A R (an an':ann A) a
  : ann_R R (setTopAnn an a) an'
     R a (getAnn an').
Proof.
  intros; destruct an; inv H; simpl; eauto.
Qed.

Lemma getAnn_setAnn A s (a:A)
 : getAnn (setAnn a s) = a.
Proof.
  destruct s; eauto.
Qed.

Lemma ann_R_setTopAnn_left (A B : Type) (R : A B Prop) (a : A)
      (an : ann A) (bn : ann B)
  : R a (getAnn bn) ann_R R an bn ann_R R (setTopAnn an a) bn.
Proof.
  intros. inv H0; simpl; eauto using @ann_R.
Qed.