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/EqualSetMap.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/EqualSetMap.v')
-rwxr-xr-x | backend/EqualSetMap.v | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/backend/EqualSetMap.v b/backend/EqualSetMap.v new file mode 100755 index 00000000..292b1c0e --- /dev/null +++ b/backend/EqualSetMap.v @@ -0,0 +1,82 @@ +Require Import List. +Require Import InterfGraphMapImp. + +Section fold_assoc_interf_map. + +Variable A : Type. + +Inductive eq_set_option : option VertexSet.t -> option VertexSet.t -> Prop := +|None_eq : eq_set_option None None +|Some_eq : forall s s', VertexSet.Equal s s' -> eq_set_option (Some s) (Some s'). + +Definition EqualSetMap m1 m2 := forall x, eq_set_option (VertexMap.find x m1) (VertexMap.find x m2). + +Lemma EqualSetMap_refl : forall m, EqualSetMap m m. + +Proof. +unfold EqualSetMap. intro m. intro x. +destruct (VertexMap.find x m). +constructor. intuition. +constructor. +Qed. + +Lemma EqualSetMap_trans : forall m1 m2 m3, +EqualSetMap m1 m2 -> +EqualSetMap m2 m3 -> +EqualSetMap m1 m3. + +Proof. +intros m1 m2 m3 H H0. +unfold EqualSetMap in *. +intro x. +generalize (H x). clear H. intro H. +generalize (H0 x). clear H0. intro H0. +destruct (VertexMap.find x m1). +inversion H. subst. +rewrite <-H2 in H0. +destruct (VertexMap.find x m3). +constructor. inversion H0. subst. +rewrite H3. assumption. +inversion H0. +destruct (VertexMap.find x m3). +inversion H0. inversion H. subst. rewrite <-H4 in H1. inversion H1. +constructor. +Qed. + +Lemma fold_left_compat_map : forall (f : VertexMap.t VertexSet.t -> A -> VertexMap.t VertexSet.t) l e e', +EqualSetMap e e' -> +(forall e1 e2 a, EqualSetMap e1 e2 -> EqualSetMap (f e1 a) (f e2 a)) -> +EqualSetMap (fold_left f l e) (fold_left f l e'). + +Proof. +intro f;induction l;simpl. +auto. +intros e e' H H0 H1. +apply (IHl (f e a) (f e' a)). +apply H0;assumption. +assumption. +Qed. + +Lemma fold_left_assoc_map : forall l (f : VertexMap.t VertexSet.t -> A -> VertexMap.t VertexSet.t) x h, +(forall (y z : A) s, EqualSetMap (f (f s y) z) (f (f s z) y)) -> +(forall e1 e2 a, EqualSetMap e1 e2 -> EqualSetMap (f e1 a) (f e2 a)) -> +EqualSetMap (fold_left f (h :: l) x) (f (fold_left f l x) h). + +Proof. +induction l;simpl;intros f x h H H0. +apply EqualSetMap_refl. +apply EqualSetMap_trans with (m2 := fold_left f (h :: l) (f x a)). +simpl. apply fold_left_compat_map. apply H. +assumption. +apply IHl. assumption. assumption. +Qed. +(* +Add Morphism EqualSetMap : equalsetmap_m. + +Proof. +unfold EqualSetMap, VertexMap.Equal. split; intros. +rewrite <-(H0 x1). rewrite <-(H x1). apply H1. +rewrite (H0 x1). rewrite (H x1). apply H1. +Qed. +*) +End fold_assoc_interf_map.
\ No newline at end of file |