moved stuff around

1 files changed, 0 insertions, 175 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 92d9202a..257149b5 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -93,57 +93,9 @@ Definition eq_id := positive.
 Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
   Regmap.set i (PSet.add j (Regmap.get i m)) m.
 
-Lemma add_i_j_adds : forall i j m,
-    PSet.contains (Regmap.get i (add_i_j i j m)) j = true.
-Proof.
-  intros.
-  unfold add_i_j.
-  rewrite Regmap.gss.
-  auto with pset.
-Qed.
-Hint Resolve add_i_j_adds: cse3.
-
-Lemma add_i_j_monotone : forall i j i' j' m,
-    PSet.contains (Regmap.get i' m) j' = true ->
-    PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true.
-Proof.
-  intros.
-  unfold add_i_j.
-  destruct (peq i i').
-  - subst i'.
-    rewrite Regmap.gss.
-    destruct (peq j j').
-    + subst j'.
-      apply PSet.gadds.
-    + eauto with pset.
-  - rewrite Regmap.gso.
-    assumption.
-    congruence.
-Qed.
-
-Hint Resolve add_i_j_monotone: cse3.
-
 Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) :=
   List.fold_left (fun already i => add_i_j i j already) ilist m.
 
-Lemma add_ilist_j_monotone : forall ilist j i' j' m,
-    PSet.contains (Regmap.get i' m) j' = true ->
-    PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true.
-Proof.
-  induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3.
-Qed.
-Hint Resolve add_ilist_j_monotone: cse3.
-
-Lemma add_ilist_j_adds : forall ilist j m,
-    forall i, In i ilist ->
-              PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true.
-Proof.
-  induction ilist; simpl; intros until i; intro IN.
-  contradiction.
-  destruct IN as [HEAD | TAIL]; subst; auto with cse3.
-Qed.
-Hint Resolve add_ilist_j_adds: cse3.
-
 Definition get_kills (eqs : PTree.t equation) :
   Regmap.t PSet.t :=
   PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
@@ -151,131 +103,4 @@ Definition get_kills (eqs : PTree.t equation) :
                         (add_ilist_j (eq_args eq) eqno already)) eqs
   (PMap.init PSet.empty). 
 
-Definition xlget_kills (eqs : list (eq_id * equation)) (m :  Regmap.t PSet.t) :
-  Regmap.t PSet.t :=
-  List.fold_left (fun already (item : eq_id * equation) =>
-    add_i_j (eq_lhs (snd item)) (fst item)
-            (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. 
-
-Lemma xlget_kills_monotone :
-  forall eqs m i j,
-    PSet.contains (Regmap.get i m) j = true ->
-    PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true.
-Proof.
-  induction eqs; simpl; trivial.
-  intros.
-  auto with cse3.
-Qed.
-
-Hint Resolve xlget_kills_monotone : cse3.
-
-Lemma xlget_kills_has_lhs :
-  forall eqs m lhs sop args j,
-    In (j, {| eq_lhs := lhs;
-              eq_op  := sop;
-              eq_args:= args |}) eqs ->
-    PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true.
-Proof.
-  induction eqs; simpl.
-  contradiction.
-  intros until j.
-  intro HEAD_TAIL.
-  destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl.
-  - auto with cse3.
-  - eapply IHeqs. eassumption.
-Qed.
-Hint Resolve xlget_kills_has_lhs : cse3.
-
-Lemma xlget_kills_has_arg :
-  forall eqs m lhs sop arg args j,
-    In (j, {| eq_lhs := lhs;
-              eq_op  := sop;
-              eq_args:= args |}) eqs ->
-    In arg args ->
-    PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true.
-Proof.
-  induction eqs; simpl.
-  contradiction.
-  intros until j.
-  intros HEAD_TAIL ARG.
-  destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl.
-  - auto with cse3.
-  - eapply IHeqs; eassumption.
-Qed.
-
-Hint Resolve xlget_kills_has_arg : cse3.
-
-
-Lemma get_kills_has_lhs :
-  forall eqs lhs sop args j,
-    PTree.get j eqs = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
-    PSet.contains (Regmap.get lhs (get_kills eqs)) j = true.
-Proof.
-  unfold get_kills.
-  intros.
-  rewrite PTree.fold_spec.
-  change (fold_left
-       (fun (a : Regmap.t PSet.t) (p : positive * equation) =>
-        add_i_j (eq_lhs (snd p)) (fst p)
-          (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
-  eapply xlget_kills_has_lhs.
-  apply PTree.elements_correct.
-  eassumption.
-Qed.
-
-Lemma get_kills_has_arg :
-  forall eqs lhs sop arg args j,
-    PTree.get j eqs = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
-    In arg args ->
-    PSet.contains (Regmap.get arg (get_kills eqs)) j = true.
-Proof.
-  unfold get_kills.
-  intros.
-  rewrite PTree.fold_spec.
-  change (fold_left
-       (fun (a : Regmap.t PSet.t) (p : positive * equation) =>
-        add_i_j (eq_lhs (snd p)) (fst p)
-          (add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
-  eapply xlget_kills_has_arg.
-  - apply PTree.elements_correct.
-    eassumption.
-  - assumption.
-Qed.
-
-(*
-Lemma xget_kills_monotone :
-  forall eqs m i j,
-    PSet.contains (Regmap.get i m) j = true ->
-    PSet.contains (Regmap.get i (xget_kills eqs m)) j = true.
-Proof.
-  unfold xget_kills.
-  intros eqs m.
-  rewrite PTree.fold_spec.
-  generalize (PTree.elements eqs).
-  intro.
-  generalize m.
-  clear m.
-  induction l; simpl; trivial.
-  intros.
-  apply IHl.
-  apply add_i_j_monotone.
-  apply add_ilist_j_monotone.
-  assumption.
-Qed.
-*)
-Lemma xget_kills_has_lhs :
-  forall eqs m lhs sop args j,
-    PTree.get j eqs = Some {| eq_lhs := lhs;
-                              eq_op  := sop;
-                              eq_args:= args |} ->
-    PSet.contains (Regmap.get lhs (xget_kills eqs m)) j = true.
-
-Definition eq_involves (eq : equation) (i : reg) :=
-  i = (eq_lhs eq) \/ In i (eq_args eq).
-
-
 Definition totoro := RELATION.lub.