diff options
Diffstat (limited to 'backend/WS.v')
| -rwxr-xr-x | backend/WS.v | 231 |
1 files changed, 0 insertions, 231 deletions
diff --git a/backend/WS.v b/backend/WS.v deleted file mode 100755 index 2f43327..0000000 --- a/backend/WS.v +++ /dev/null @@ -1,231 +0,0 @@ -Require Import FSets. -Require Import InterfGraphMapImp. -Require Import Conservative_criteria. -Require Import Edges. -Require Import MyRegisters. -Require Import Affinity_relation. - -Import Edge RegFacts Props OTFacts. - -(* Intersections of vertices sets of the worklists are empty *) -Lemma WS_empty_inter_1 : forall g palette WL, -WS_properties g palette WL -> -VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_freezeWL WL)). - -Proof. -intros g palette WL H. -unfold VertexSet.Empty. -intros a H0. -generalize (VertexSet.inter_1 H0);intro H1. -generalize (VertexSet.inter_2 H0);intro H2. -unfold WS_properties in H. -destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. -generalize (proj1 (H a) H1);intro H6. -destruct H6 as [H6 _]. -generalize (proj1 (H3 a) H2);intro H7. -destruct H7 as [H7 _]. -rewrite H6 in H7; inversion H7. -Qed. - -Lemma WS_empty_inter_2 : forall g palette WL, -WS_properties g palette WL -> -VertexSet.Empty (VertexSet.inter (get_spillWL WL) (get_simplifyWL WL)). - -Proof. -intros g palette WL H. -unfold VertexSet.Empty. -intros a H0. -generalize (VertexSet.inter_1 H0);intro H1. -generalize (VertexSet.inter_2 H0);intro H2. -unfold WS_properties in H. -destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. -generalize (proj1 (H a) H1);intro H6. -destruct H6 as [H6 _]. -generalize (proj1 (H4 a) H2);intro H7. -destruct H7 as [H7 _]. -rewrite H6 in H7; inversion H7. -Qed. - -Lemma WS_empty_inter_3 : forall g palette WL, -WS_properties g palette WL -> -VertexSet.Empty (VertexSet.inter (get_freezeWL WL) (get_simplifyWL WL)). - -Proof. -intros g palette WL H. -unfold VertexSet.Empty. -intros a H0. -generalize (VertexSet.inter_1 H0);intro H1. -generalize (VertexSet.inter_2 H0);intro H2. -unfold WS_properties in H. -destruct H as [H H3];destruct H3 as [H3 H4];destruct H4 as [H4 H5]. -generalize (proj1 (H3 a) H1);intro H6. -destruct H6 as [_ H6]. -destruct H6 as [H6 _]. -generalize (proj1 (H4 a) H2);intro H7. -destruct H7 as [_ H7]. -destruct H7 as [H7 _]. -rewrite H6 in H7; inversion H7. -Qed. - -(* A tactic for simplifying proofs of belonging of a vertex to a worklist *) -Ltac WS_apply H := generalize H;intro HWS_; -match goal with -| |- (VertexSet.In ?A _) => destruct HWS_ as [HWS_ HWS__]; - try (apply (proj2 (HWS_ A))); - destruct HWS__ as [HWS__ HWS___]; - try (apply (proj2 (HWS__ A))); - destruct HWS___ as [HWS___ HWS____]; - try (apply (proj2 (HWS___ A))); - clear HWS_ HWS__ HWS___ HWS____ -| |- (EdgeSet.In ?A _) => do 3 destruct HWS_ as [_ HWS_]; - apply (proj2 (HWS_ A)); - clear HWS_ -end. - -(* Lemmas for generalizing properties of a vertex belonging to a given worklist *) -Lemma In_spill_props : forall x g WL s a b c palette, -VertexSet.In x s -> -WL = (s,a,b,c) -> -WS_properties g palette WL -> -has_low_degree g palette x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g). - -Proof. -intros x g WL s a b c palette H H0 H1. -unfold WS_properties in H1;rewrite H0 in H1. -destruct H1 as [H1 _]. -unfold get_spillWL in H1;simpl in H1. -apply (proj1 (H1 x) H). -Qed. - -Lemma In_freeze_props : forall x g WL s a b c palette, -VertexSet.In x s -> -WL = (a,s,b,c) -> -WS_properties g palette WL -> -has_low_degree g palette x = true /\ move_related g x = true /\ In_graph x g /\ ~VertexSet.In x (precolored g). - -Proof. -intros x g WL s a b c palette H H0 H1. -unfold WS_properties in H1;rewrite H0 in H1. -destruct H1 as [_ H1]. -destruct H1 as [H1 _]. -unfold get_freezeWL in H1;simpl in H1. -generalize (proj1 (H1 x) H);intro. -intuition. -apply move_related_in_graph;intuition. -Qed. - -Lemma In_simplify_props : forall x g WL s a b c palette, -VertexSet.In x s -> -WL = (a,b,s,c) -> -WS_properties g palette WL -> -has_low_degree g palette x = true /\ move_related g x = false /\ In_graph x g /\ ~VertexSet.In x (precolored g). - -Proof. -intros x g WL s a b c palette H H0 H1. -unfold WS_properties in H1;rewrite H0 in H1. -do 2 destruct H1 as [_ H1]. -destruct H1 as [H1 _]. -unfold get_spillWL in H1;simpl in H1. -apply (proj1 (H1 x) H). -Qed. - -Lemma In_move_props : forall e g WL s a b c palette, -EdgeSet.In e s -> -WL = (a,b,c,s) -> -WS_properties g palette WL -> -aff_edge e /\ In_graph_edge e g. - -Proof. -intros e g WL s a b c palette H H0 H1. -unfold WS_properties in H1;rewrite H0 in H1. -do 3 destruct H1 as [_ H1]. -unfold get_movesWL in H1;simpl in H1. -apply (proj1 (H1 e) H). -Qed. - -Lemma WS_props_equal : -forall g palette ws ws', -VertexSet.Equal (get_simplifyWL ws) (get_simplifyWL ws') -> -VertexSet.Equal (get_freezeWL ws) (get_freezeWL ws') -> -VertexSet.Equal (get_spillWL ws) (get_spillWL ws') -> -EdgeSet.Equal (get_movesWL ws) (get_movesWL ws') -> -WS_properties g palette ws -> -WS_properties g palette ws'. - -Proof. -unfold WS_properties;unfold get_spillWL;unfold get_freezeWL; -unfold get_simplifyWL;unfold get_movesWL;simpl;unfold VertexSet.Equal; -unfold EdgeSet.Equal;intros g palette ws ws' H H0 H1 H2 H3. -destruct ws as [ws d]; destruct ws as [ws c]; destruct ws as [a b]. -destruct ws' as [ws' p]; destruct ws' as [ws' o]; destruct ws' as [m n]. simpl in *. -generalize (VertexSet.eq_sym H);generalize (VertexSet.eq_sym H0); -generalize (VertexSet.eq_sym H1);generalize (EdgeSet.eq_sym H2); -clear H;clear H0;clear H1;clear H2;intros H2 H1 H0 H. - -destruct H3 as [Hsp H3];destruct H3 as [Hf H3]; -destruct H3 as [Hsi Hm]. -do 2 split. -intro H4;apply (proj1 (Hsp x) (proj1 (H1 x) H4)). -intro H4;apply (proj2 (H1 x) (proj2 (Hsp x) H4)). -split;intro H4. -apply (proj1 (Hf x) (proj1 (H0 x) H4)). -apply (proj2 (H0 x) (proj2 (Hf x) H4)). -split. -split;intro H4. -apply (proj1 (Hsi x) (proj1 (H x) H4)). -apply (proj2 (H x) (proj2 (Hsi x) H4)). -split;intro H4. -apply (proj1 (Hm e) (proj1 (H2 e) H4)). -apply (proj2 (H2 e) (proj2 (Hm e) H4)). -Qed. - -(* Definition of the nonprecolored vertices of a graph *) -Definition not_precolored g := VertexSet.diff (V g) (precolored g). - -(* The union of vertices worklists forms the nonprecolored vertices set of g *) -Lemma not_precolored_union_ws : forall g palette ws, -WS_properties g palette ws -> -VertexSet.Equal -(VertexSet.union (VertexSet.union (get_spillWL ws) (get_freezeWL ws)) (get_simplifyWL ws)) -(not_precolored g). - -Proof. -intros g palette ws HWS. -split. intro H. -unfold not_precolored. apply VertexSet.diff_3. -destruct (VertexSet.union_1 H). -destruct (VertexSet.union_1 H0). -apply (proj1(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). -apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). -apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))). -destruct (VertexSet.union_1 H). -destruct (VertexSet.union_1 H0). -apply (proj2(proj2 (In_spill_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). -apply (proj2(proj2 (In_freeze_props _ _ _ _ _ _ _ _ H1 (refl_equal _) HWS))). -apply (proj2(proj2 (In_simplify_props _ _ _ _ _ _ _ _ H0 (refl_equal _) HWS))). -intro H. -unfold not_precolored in H. -generalize (VertexSet.diff_1 H). intro H0. -generalize (VertexSet.diff_2 H). clear H. intro H. -case_eq (has_low_degree g palette a); intro Hlow. -case_eq (move_related g a); intro Haff. -apply VertexSet.union_2. apply VertexSet.union_3. -WS_apply HWS. intuition. -apply VertexSet.union_3. -WS_apply HWS. intuition. -apply VertexSet.union_2. apply VertexSet.union_2. -WS_apply HWS. intuition. -Qed. - -(* The moves worklists is equal to the set of affinity edges *) -Lemma moves_AE : forall g palette ws, -WS_properties g palette ws -> -EdgeSet.Equal (AE g) (get_movesWL ws). - -Proof. -split; intros. -destruct ws. destruct p. destruct p. -simpl. WS_apply H. apply (proj1 (In_graph_aff_edge_in_AE _ _) H0). -generalize (In_move_props _ _ _ _ _ _ _ _ H0 (refl_equal _) H). intro H1. -apply (proj2 (In_graph_aff_edge_in_AE _ _) H1). -Qed. |