diff options
author | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-08 07:53:02 +0000 |
---|---|---|
committer | blazy <blazy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-08 07:53:02 +0000 |
commit | a8c744000247af207b489d3cdd4e3d3cf60f72e1 (patch) | |
tree | 96c7ee4e244fccdb840233007604ba52d97c09e0 /backend/Remove_Vertex_Adjacency.v | |
parent | 283afabc594b385e4f17fa59647aa8cddee27f85 (diff) | |
download | compcert-a8c744000247af207b489d3cdd4e3d3cf60f72e1.tar.gz compcert-a8c744000247af207b489d3cdd4e3d3cf60f72e1.zip |
ajout branche allocation de registres
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Remove_Vertex_Adjacency.v')
-rwxr-xr-x | backend/Remove_Vertex_Adjacency.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/backend/Remove_Vertex_Adjacency.v b/backend/Remove_Vertex_Adjacency.v new file mode 100755 index 00000000..668063d1 --- /dev/null +++ b/backend/Remove_Vertex_Adjacency.v @@ -0,0 +1,73 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Interference_adjacency. +Require Import Edges. +Require Import MyRegisters. + +Import RegFacts Props. + +Module Register := Regs. + +(* For any vertex x different from r, the neighborhood of x in + (remove_vertex r g) is its one in g, minus r *) +Lemma remove_interf_adj : forall x r g, +~Register.eq x r -> +VertexSet.Equal (interference_adj x (remove_vertex r g)) + (VertexSet.remove r (interference_adj x g)). + +Proof. +intros. +split; intros. +apply VertexSet.remove_2. intro. +rewrite <-H1 in H0. rewrite in_interf in H0. +generalize (proj1 (In_graph_edge_in_ext _ _ H0)). change_rewrite. intro. +rewrite In_remove_vertex in H2. destruct H2. elim (H3 (Register.eq_refl _)). +rewrite in_interf in H0. rewrite In_remove_edge in H0. destruct H0. +rewrite in_interf. assumption. + +rewrite in_interf. rewrite In_remove_edge. +split. +rewrite <-in_interf. apply (VertexSet.remove_3 H0). +intro. destruct H1; change_rewrite. +elim (VertexSet.remove_1 H1 H0). +elim H. auto. +Qed. + +(* If x is different from r and does not belong to the interference neighborhood + of r in g, then the interference neighborhood of x in (remove_vertex r g) + is equal to the interference neighborhood of x in g *) +Lemma interf_adj_remove : forall x r g, +~VertexSet.In x (interference_adj r g) -> +~Register.eq x r -> +VertexSet.Equal (interference_adj x g) (interference_adj x (remove_vertex r g)). + +Proof. +intros x r g H H0. +rewrite remove_interf_adj. rewrite remove_equal. apply VertexSet.eq_refl. +intro. elim H. apply interf_adj_comm. assumption. +auto. +Qed. + +(* The interference neighborhood of x in (remove_vertex r g) + is a subset of the interference neighborhood of x in g *) +Lemma sub_remove_interf : forall x r g, +~Register.eq x r -> +VertexSet.Subset (interference_adj x (remove_vertex r g)) + (interference_adj x g). + +Proof. +intros x r g H. rewrite remove_interf_adj. +unfold VertexSet.Subset. intros y H0. +apply (VertexSet.remove_3 H0). +assumption. +Qed. + +(* If x is a neighbor of r in g, then x belongs to (remove_vertex r g) *) +Lemma in_interf_adj_in_remove : forall x r g, +VertexSet.In x (interference_adj r g) -> In_graph x (remove_vertex r g). + +Proof. +intros x r g H. rewrite In_remove_vertex. split. +rewrite in_interf in H. apply (proj1 (In_graph_edge_in_ext _ _ H)). +intro H0. rewrite H0 in H. elim (not_in_interf_self _ _ H). +Qed. |