diff options
Diffstat (limited to 'backend/Typed_interfgraphs.v')
| -rwxr-xr-x | backend/Typed_interfgraphs.v | 740 |
1 files changed, 0 insertions, 740 deletions
diff --git a/backend/Typed_interfgraphs.v b/backend/Typed_interfgraphs.v deleted file mode 100755 index 0f25228..0000000 --- a/backend/Typed_interfgraphs.v +++ /dev/null @@ -1,740 +0,0 @@ -Require Import InterfGraph. -Require Import AST. -Require Import FSets. -Require Import Locations. -Require Import Registers. - -Module Import SRRFacts := Facts SetRegReg. -Module MRegset := FSetAVL.Make OrderedMreg. - -Close Scope nat_scope. - -Definition regregpartition : Type := SetRegReg.t*SetRegReg.t*Regset.t*Regset.t. - -Definition rr1 := fun (p : regregpartition) => fst (fst (fst p)). -Definition rr2 := fun (p : regregpartition) => snd (fst (fst p)). -Definition rr3 := fun (p : regregpartition) => snd (fst p). -Definition rr4 := fun (p : regregpartition) => snd p. - -Definition regreg_edge_type_partition s env := -SetRegReg.fold (fun e s => match env (fst e), env (snd e) with - | Tint, Tint => (SetRegReg.add e (rr1 s), rr2 s, - Regset.add (fst e) (Regset.add (snd e) (rr3 s)), rr4 s) - | Tfloat, Tfloat => (rr1 s, SetRegReg.add e (rr2 s), rr3 s, - Regset.add (fst e) (Regset.add (snd e) (rr4 s))) - | Tint, Tfloat => (rr1 s, rr2 s, Regset.add (fst e) (rr3 s), Regset.add (snd e) (rr4 s)) - | Tfloat, Tint => (rr1 s, rr2 s, Regset.add (snd e) (rr3 s), Regset.add (fst e) (rr4 s)) - end) - s - (SetRegReg.empty, SetRegReg.empty, Regset.empty, Regset.empty). - -Lemma in_partition_in_fst : forall e s env, -SetRegReg.In e (rr1 (regreg_edge_type_partition s env)) -> -SetRegReg.In e s. - -Proof. -intros e s env H. -unfold regreg_edge_type_partition in H. -set (f := fun (e : SetRegReg.elt) (s : regregpartition) => - match env (fst e) with - | Tint => - match env (snd e) with - | Tint => - (SetRegReg.add e (rr1 s), rr2 s, - Regset.add (fst e) (Regset.add (snd e) (rr3 s)), - rr4 s) - | Tfloat => - (rr1 s, rr2 s, Regset.add (fst e) (rr3 s), - Regset.add (snd e) (rr4 s)) - end - | Tfloat => - match env (snd e) with - | Tint => - (rr1 s, rr2 s, Regset.add (snd e) (rr3 s), - Regset.add (fst e) (rr4 s)) - | Tfloat => - (rr1 s, SetRegReg.add e (rr2 s), rr3 s, - Regset.add (fst e) (Regset.add (snd e) (rr4 s))) - end - end). -unfold regregpartition in *. fold f in H. - -assert (forall e set1 set2 set3 set4, SetRegReg.In e (rr1 (SetRegReg.fold f s (set1, set2, set3, set4))) -> - SetRegReg.In e s \/ SetRegReg.In e set1 \/ SetRegReg.In e set2). -clear H. -intros e' s1 s2 s3 s4 H. -rewrite SetRegReg.fold_1 in H. -generalize H. generalize s1 s2 s3 s4. clear s1 s2 s3 s4 H. -generalize (SetRegReg.elements_2). intro HH. -generalize (HH s). clear HH. intro HH. -induction (SetRegReg.elements s). -simpl. right. left. assumption. -intros s1 s2 s3 s4 H. -simpl in H. -assert ((forall x : SetRegReg.elt, - SetoidList.InA (fun x0 y : OrderedRegReg.t => fst x0 = fst y /\ snd x0 = snd y) x l -> - SetRegReg.In x s)). -intros. apply HH. right. assumption. -generalize (IHl H0). clear IHl H0. intro IHl. -assert (f a (s1, s2, s3, s4) = (SetRegReg.add a s1, s2, Regset.add (fst a) (Regset.add (snd a) s3), s4) \/ - f a (s1, s2, s3, s4) = (s1, SetRegReg.add a s2, s3, Regset.add (fst a) (Regset.add (snd a) s4)) \/ - f a (s1, s2, s3, s4) = (s1, s2, Regset.add (fst a) s3, Regset.add (snd a) s4) \/ - f a (s1, s2, s3, s4) = (s1, s2, Regset.add (snd a) s3, Regset.add (fst a) s4)). -unfold f. -destruct (env (snd a)); destruct (env (fst a)); unfold rr1, rr2, rr3, rr4; simpl. -left. reflexivity. -right. right. right. reflexivity. -right. right. left. reflexivity. -right. left. reflexivity. -destruct H0. -rewrite H0 in H. - -generalize (IHl (SetRegReg.add a s1) s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. - -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. left. assumption. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 (SetRegReg.add a s2) _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -rewrite H0 in H. -generalize (IHl s1 s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -generalize (H0 _ _ _ _ _ H). clear H0. intro H0. -destruct H0. -assumption. -destruct H0; elim (SetRegReg.empty_1 H0). -Qed. - -Lemma in_partition_in_snd : forall e s env, -SetRegReg.In e (rr2 (regreg_edge_type_partition s env)) -> -SetRegReg.In e s. - -Proof. -intros e s env H. -unfold regreg_edge_type_partition in H. -set (f := fun (e : SetRegReg.elt) (s : regregpartition) => - match env (fst e) with - | Tint => - match env (snd e) with - | Tint => - (SetRegReg.add e (rr1 s), rr2 s, - Regset.add (fst e) (Regset.add (snd e) (rr3 s)), - rr4 s) - | Tfloat => - (rr1 s, rr2 s, Regset.add (fst e) (rr3 s), - Regset.add (snd e) (rr4 s)) - end - | Tfloat => - match env (snd e) with - | Tint => - (rr1 s, rr2 s, Regset.add (snd e) (rr3 s), - Regset.add (fst e) (rr4 s)) - | Tfloat => - (rr1 s, SetRegReg.add e (rr2 s), rr3 s, - Regset.add (fst e) (Regset.add (snd e) (rr4 s))) - end - end). -unfold regregpartition in *. fold f in H. - -assert (forall e set1 set2 set3 set4, SetRegReg.In e (rr2 (SetRegReg.fold f s (set1, set2, set3, set4))) -> - SetRegReg.In e s \/ SetRegReg.In e set1 \/ SetRegReg.In e set2). -clear H. -intros e' s1 s2 s3 s4 H. -rewrite SetRegReg.fold_1 in H. -generalize H. generalize s1 s2 s3 s4. clear s1 s2 s3 s4 H. -generalize (SetRegReg.elements_2). intro HH. -generalize (HH s). clear HH. intro HH. -induction (SetRegReg.elements s). -simpl. right. right. assumption. -intros s1 s2 s3 s4 H. -simpl in H. -assert ((forall x : SetRegReg.elt, - SetoidList.InA (fun x0 y : OrderedRegReg.t => fst x0 = fst y /\ snd x0 = snd y) x l -> - SetRegReg.In x s)). -intros. apply HH. right. assumption. -generalize (IHl H0). clear IHl H0. intro IHl. -assert (f a (s1, s2, s3, s4) = (SetRegReg.add a s1, s2, Regset.add (fst a) (Regset.add (snd a) s3), s4) \/ - f a (s1, s2, s3, s4) = (s1, SetRegReg.add a s2, s3, Regset.add (fst a) (Regset.add (snd a) s4)) \/ - f a (s1, s2, s3, s4) = (s1, s2, Regset.add (fst a) s3, Regset.add (snd a) s4) \/ - f a (s1, s2, s3, s4) = (s1, s2, Regset.add (snd a) s3, Regset.add (fst a) s4)). -unfold f. -destruct (env (snd a)); destruct (env (fst a)); unfold rr1, rr2, rr3, rr4; simpl. -left. reflexivity. -right. right. right. reflexivity. -right. right. left. reflexivity. -right. left. reflexivity. -destruct H0. -rewrite H0 in H. - -generalize (IHl (SetRegReg.add a s1) s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. - -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. left. assumption. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 (SetRegReg.add a s2) _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -rewrite H0 in H. -generalize (IHl s1 s2 _ _ H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -generalize (H0 _ _ _ _ _ H). clear H0. intro H0. -destruct H0. -assumption. -destruct H0; elim (SetRegReg.empty_1 H0). -Qed. - -Lemma in_partition_type_fst : forall e s env, -SetRegReg.In e (rr1 (regreg_edge_type_partition s env)) -> -env (fst e) = Tint /\ env (snd e) = Tint. - -Proof. -intros e s env H. -unfold regreg_edge_type_partition in H. -set (f := fun (e : SetRegReg.elt) (s : regregpartition) => - match env (fst e) with - | Tint => - match env (snd e) with - | Tint => - (SetRegReg.add e (rr1 s), rr2 s, - Regset.add (fst e) (Regset.add (snd e) (rr3 s)), - rr4 s) - | Tfloat => - (rr1 s, rr2 s, Regset.add (fst e) (rr3 s), - Regset.add (snd e) (rr4 s)) - end - | Tfloat => - match env (snd e) with - | Tint => - (rr1 s, rr2 s, Regset.add (snd e) (rr3 s), - Regset.add (fst e) (rr4 s)) - | Tfloat => - (rr1 s, SetRegReg.add e (rr2 s), rr3 s, - Regset.add (fst e) (Regset.add (snd e) (rr4 s))) - end - end). -unfold regregpartition in *. fold f in H. - -cut (forall e set1 set2 set3 set4, SetRegReg.In e (rr1 (SetRegReg.fold f s (set1, set2, set3, set4))) -> - (env (fst e) = Tint /\ env (snd e) = Tint) \/ SetRegReg.In e set1). - -intros. -generalize (H0 _ _ _ _ _ H). clear H H0. intro H. -destruct H. assumption. elim (SetRegReg.empty_1 H). - -(* cut property *) -intros. -generalize H0. clear H H0. intro H. -rewrite SetRegReg.fold_1 in H. -generalize H. clear H. generalize set1 set2 set3 set4. -induction (SetRegReg.elements s); intros s1 s2 s3 s4 H. -simpl in H. right. assumption. -simpl in H. - -assert ((f a (s1, s2, s3, s4) = (SetRegReg.add a s1, s2, Regset.add (fst a) (Regset.add (snd a) s3), s4) /\ - env (fst a) = Tint /\ - env (snd a) = Tint)\/ - (f a (s1, s2, s3, s4) = (s1, SetRegReg.add a s2, s3, Regset.add (fst a) (Regset.add (snd a) s4)) /\ - env (fst a) = Tfloat /\ - env (snd a) = Tfloat) \/ - f a (s1, s2, s3, s4) = (s1,s2, Regset.add (fst a) s3, Regset.add (snd a) s4) \/ - f a (s1, s2, s3, s4) = (s1,s2, Regset.add (snd a) s3, Regset.add (fst a) s4) -). -unfold f. -destruct (env (snd a)); destruct (env (fst a)); unfold rr1, rr2, rr3, rr4; simpl. -left. auto. -right. right. right. reflexivity. -right. right. left. reflexivity. -right. left. auto. - -destruct H0. -destruct H0. destruct H1. rewrite H0 in H. -generalize (IHl (SetRegReg.add a s1) s2 _ _ H). intro H3. -destruct H3. -left. assumption. -destruct (proj1 (add_iff _ _ _) H3). -left. intuition. rewrite <-H5. auto. rewrite <-H6. auto. -right. assumption. - -destruct H0. destruct H0. destruct H1. rewrite H0 in H. -apply (IHl s1 (SetRegReg.add a s2) _ _ H). - -destruct H0. rewrite H0 in H. apply (IHl s1 s2 _ _ H). -rewrite H0 in H. apply (IHl s1 s2 _ _ H). -Qed. - -Lemma in_partition_type_snd : forall e s env, -SetRegReg.In e (rr2 (regreg_edge_type_partition s env)) -> -env (fst e) = Tfloat /\ env (snd e) = Tfloat. - -Proof. -intros e s env H. -unfold regreg_edge_type_partition in H. -set (f := fun (e : SetRegReg.elt) (s : regregpartition) => - match env (fst e) with - | Tint => - match env (snd e) with - | Tint => - (SetRegReg.add e (rr1 s), rr2 s, - Regset.add (fst e) (Regset.add (snd e) (rr3 s)), - rr4 s) - | Tfloat => - (rr1 s, rr2 s, Regset.add (fst e) (rr3 s), - Regset.add (snd e) (rr4 s)) - end - | Tfloat => - match env (snd e) with - | Tint => - (rr1 s, rr2 s, Regset.add (snd e) (rr3 s), - Regset.add (fst e) (rr4 s)) - | Tfloat => - (rr1 s, SetRegReg.add e (rr2 s), rr3 s, - Regset.add (fst e) (Regset.add (snd e) (rr4 s))) - end - end). -unfold regregpartition in *. fold f in H. - -cut (forall e set1 set2 set3 set4, SetRegReg.In e (rr2 (SetRegReg.fold f s (set1, set2, set3, set4))) -> - (env (fst e) = Tfloat /\ env (snd e) = Tfloat) \/ SetRegReg.In e set2). - -intros. -generalize (H0 _ _ _ _ _ H). clear H H0. intro H. -destruct H. assumption. elim (SetRegReg.empty_1 H). - -(* cut property *) -intros. -generalize H0. clear H H0. intro H. -rewrite SetRegReg.fold_1 in H. -generalize H. clear H. generalize set1 set2 set3 set4. -induction (SetRegReg.elements s); intros s1 s2 s3 s4 H. -simpl in H. right. assumption. -simpl in H. - -assert ((f a (s1, s2, s3, s4) = (SetRegReg.add a s1, s2, Regset.add (fst a) (Regset.add (snd a) s3), s4) /\ - env (fst a) = Tint /\ - env (snd a) = Tint)\/ - (f a (s1, s2, s3, s4) = (s1, SetRegReg.add a s2, s3, Regset.add (fst a) (Regset.add (snd a) s4)) /\ - env (fst a) = Tfloat /\ - env (snd a) = Tfloat) \/ - f a (s1, s2, s3, s4) = (s1,s2, Regset.add (fst a) s3, Regset.add (snd a) s4) \/ - f a (s1, s2, s3, s4) = (s1,s2, Regset.add (snd a) s3, Regset.add (fst a) s4) -). -unfold f. -destruct (env (snd a)); destruct (env (fst a)); unfold rr1, rr2, rr3, rr4; simpl. -left. auto. -right. right. right. reflexivity. -right. right. left. reflexivity. -right. left. auto. - -destruct H0. -destruct H0. rewrite H0 in H. -apply (IHl (SetRegReg.add a s1) s2 _ _ H). -destruct H0. destruct H0. rewrite H0 in H. -generalize (IHl s1 (SetRegReg.add a s2) _ _ H). intro. -destruct H2. -left. assumption. -destruct (proj1 (add_iff _ _ _) H2). -left. intuition. rewrite <-H1. auto. rewrite <-H6. auto. -right. assumption. - -destruct H0. rewrite H0 in H. apply (IHl _ _ _ _ H). - -rewrite H0 in H. apply (IHl s1 s2 _ _ H). -Qed. - -Definition regmregpartition : Type := SetRegMreg.t*SetRegMreg.t*Regset.t*Regset.t*MRegset.t*MRegset.t. - -Definition rm1 := fun (p : regmregpartition) => fst (fst (fst (fst (fst p)))). -Definition rm2 := fun (p : regmregpartition) => snd (fst (fst (fst (fst p)))). -Definition rm3 := fun (p : regmregpartition) => snd (fst (fst (fst p))). -Definition rm4 := fun (p : regmregpartition) => snd (fst (fst p)). -Definition rm5 := fun (p : regmregpartition) => snd (fst p). -Definition rm6 := fun (p : regmregpartition) => snd p. - -Module Import SRMFacts := Facts SetRegMreg. - -Definition regmreg_edge_type_partition s env := -SetRegMreg.fold (fun e s => match env (fst e), mreg_type (snd e) with - | Tint, Tint => (SetRegMreg.add e (rm1 s), rm2 s, - Regset.add (fst e) (rm3 s), rm4 s, - MRegset.add (snd e) (rm5 s), rm6 s) - | Tfloat, Tfloat => (rm1 s, SetRegMreg.add e (rm2 s), - rm3 s, Regset.add (fst e) (rm4 s), - rm5 s, MRegset.add (snd e) (rm6 s)) - | Tint, Tfloat => (rm1 s, rm2 s, - Regset.add (fst e) (rm3 s), rm4 s, - rm5 s, MRegset.add (snd e) (rm6 s)) - |Tfloat, Tint => (rm1 s, rm2 s, - rm3 s, Regset.add (fst e) (rm4 s), - MRegset.add (snd e) (rm5 s), rm6 s) - end) -s -(SetRegMreg.empty, SetRegMreg.empty, Regset.empty, Regset.empty, MRegset.empty, MRegset.empty). - -Lemma in_mreg_partition_in_fst : forall e s env, -SetRegMreg.In e (rm1 (regmreg_edge_type_partition s env)) -> -SetRegMreg.In e s. - -Proof. -Admitted. -(* -intros e s env H. -unfold regmreg_edge_type_partition in H. -set (f := (fun (e : SetRegMreg.elt) (s : SetRegMreg.t * SetRegMreg.t) => - match env (fst e) with - | Tint => - match mreg_type (snd e) with - | Tint => (SetRegMreg.add e (fst s), snd s) - | Tfloat => s - end - | Tfloat => - match mreg_type (snd e) with - | Tint => s - | Tfloat => (fst s, SetRegMreg.add e (snd s)) - end - end)) in H. - -assert (forall e set1 set2, SetRegMreg.In e (fst (SetRegMreg.fold f s (set1, set2))) -> - SetRegMreg.In e s \/ SetRegMreg.In e set1 \/ SetRegMreg.In e set2). -clear H. -intros e' s1 s2 H. -rewrite SetRegMreg.fold_1 in H. -generalize H. generalize s1 s2. clear s1 s2 H. -generalize (SetRegMreg.elements_2). intro HH. -generalize (HH s). clear HH. intro HH. -induction (SetRegMreg.elements s). -simpl. right. left. assumption. -intros s1 s2 H. -simpl in H. -assert ((forall x : SetRegMreg.elt, - SetoidList.InA (fun x0 y : OrderedRegMreg.t => fst x0 = fst y /\ snd x0 = snd y) x l -> - SetRegMreg.In x s)). -intros. apply HH. right. assumption. -generalize (IHl H0). clear IHl H0. intro IHl. -assert (f a (s1, s2) = (SetRegMreg.add a s1, s2) \/ - f a (s1, s2) = (s1, SetRegMreg.add a s2) \/ - f a (s1, s2) = (s1,s2)). -unfold f. -destruct (mreg_type (snd a)); destruct (env (fst a)); simpl. -left. reflexivity. -right. right. reflexivity. -right. right. reflexivity. -right. left. reflexivity. -destruct H0. -rewrite H0 in H. - -generalize (IHl (SetRegMreg.add a s1) s2 H). -intro H1. destruct H1. -left. assumption. -destruct H1. - -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. left. assumption. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 (SetRegMreg.add a s2) H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. right. assumption. -rewrite H0 in H. -generalize (IHl s1 s2 H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -generalize (H0 _ _ _ H). clear H0. intro H0. -destruct H0. -assumption. -destruct H0; elim (SetRegMreg.empty_1 H0). -Qed. -*) - -Lemma in_mreg_partition_in_snd : forall e s env, -SetRegMreg.In e (rm2 (regmreg_edge_type_partition s env)) -> -SetRegMreg.In e s. - -Proof. -Admitted. -(* -intros e s env H. -unfold regmreg_edge_type_partition in H. -set (f := (fun (e : SetRegMreg.elt) (s : SetRegMreg.t * SetRegMreg.t) => - match env (fst e) with - | Tint => - match mreg_type (snd e) with - | Tint => (SetRegMreg.add e (fst s), snd s) - | Tfloat => s - end - | Tfloat => - match mreg_type (snd e) with - | Tint => s - | Tfloat => (fst s, SetRegMreg.add e (snd s)) - end - end)) in H. - -assert (forall e set1 set2, SetRegMreg.In e (snd (SetRegMreg.fold f s (set1, set2))) -> - SetRegMreg.In e s \/ SetRegMreg.In e set1 \/ SetRegMreg.In e set2). -clear H. -intros e' s1 s2 H. -rewrite SetRegMreg.fold_1 in H. -generalize H. generalize s1 s2. clear s1 s2 H. -generalize (SetRegMreg.elements_2). intro HH. -generalize (HH s). clear HH. intro HH. -induction (SetRegMreg.elements s). -simpl. right. right. assumption. -intros s1 s2 H. -simpl in H. -assert ((forall x : SetRegMreg.elt, - SetoidList.InA (fun x0 y : OrderedRegMreg.t => fst x0 = fst y /\ snd x0 = snd y) x l -> - SetRegMreg.In x s)). -intros. apply HH. right. assumption. -generalize (IHl H0). clear IHl H0. intro IHl. -assert (f a (s1, s2) = (SetRegMreg.add a s1, s2) \/ - f a (s1, s2) = (s1, SetRegMreg.add a s2) \/ - f a (s1, s2) = (s1,s2)). -unfold f. -destruct (mreg_type (snd a)); destruct (env (fst a)); simpl. -left. reflexivity. -right. right. reflexivity. -right. right. reflexivity. -right. left. reflexivity. -destruct H0. -rewrite H0 in H. - -generalize (IHl (SetRegMreg.add a s1) s2 H). -intro H1. destruct H1. -left. assumption. -destruct H1. - -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. left. assumption. -right. right. assumption. -destruct H0. -rewrite H0 in H. -generalize (IHl s1 (SetRegMreg.add a s2) H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -destruct (proj1 (add_iff _ _ _) H1). -left. apply HH. left. intuition. -right. right. assumption. -rewrite H0 in H. -generalize (IHl s1 s2 H). -intro H1. destruct H1. -left. assumption. -destruct H1. -right. left. assumption. -right. right. assumption. -generalize (H0 _ _ _ H). clear H0. intro H0. -destruct H0. -assumption. -destruct H0; elim (SetRegMreg.empty_1 H0). -Qed. -*) - -Lemma in_mreg_partition_type_fst : forall e s env, -SetRegMreg.In e (rm1 (regmreg_edge_type_partition s env)) -> -env (fst e) = Tint /\ mreg_type (snd e) = Tint. - -Proof. -Admitted. -(* -intros e s env H. -unfold regmreg_edge_type_partition in H. -set (f := (fun (e : SetRegMreg.elt) (s : SetRegMreg.t * SetRegMreg.t) => - match env (fst e) with - | Tint => - match mreg_type (snd e) with - | Tint => (SetRegMreg.add e (fst s), snd s) - | Tfloat => s - end - | Tfloat => - match mreg_type (snd e) with - | Tint => s - | Tfloat => (fst s, SetRegMreg.add e (snd s)) - end - end)) in H. - -cut (forall e set1 set2, SetRegMreg.In e (fst (SetRegMreg.fold f s (set1, set2))) -> - (env (fst e) = Tint /\ mreg_type (snd e) = Tint) \/ SetRegMreg.In e set1). - -intros. -generalize (H0 _ _ _ H). clear H H0. intro H. -destruct H. assumption. elim (SetRegMreg.empty_1 H). - -(* cut property *) -intros. -generalize H0. clear H H0. intro H. -rewrite SetRegMreg.fold_1 in H. -generalize H. clear H. generalize set1 set2. -induction (SetRegMreg.elements s); intros s1 s2 H. -simpl in H. right. assumption. -simpl in H. - -assert ((f a (s1, s2) = (SetRegMreg.add a s1, s2) /\ - env (fst a) = Tint /\ - mreg_type (snd a) = Tint)\/ - (f a (s1, s2) = (s1, SetRegMreg.add a s2) /\ - env (fst a) = Tfloat /\ - mreg_type (snd a) = Tfloat) \/ - f a (s1, s2) = (s1,s2)). -unfold f. -destruct (mreg_type (snd a)); destruct (env (fst a)); simpl. -left. auto. -right. right. reflexivity. -right. right. reflexivity. -right. left. auto. - -destruct H0. -destruct H0. destruct H1. rewrite H0 in H. -generalize (IHl (SetRegMreg.add a s1) s2 H). intro H3. -destruct H3. -left. assumption. -destruct (proj1 (add_iff _ _ _) H3). -left. intuition. rewrite <-H5. auto. rewrite <-H6. auto. -right. assumption. - -destruct H0. destruct H0. destruct H1. rewrite H0 in H. -apply (IHl s1 (SetRegMreg.add a s2) H). - -rewrite H0 in H. -apply (IHl s1 s2 H). -Qed. -*) - -Lemma in_mreg_partition_type_snd : forall e s env, -SetRegMreg.In e (rm2 (regmreg_edge_type_partition s env)) -> -env (fst e) = Tfloat /\ mreg_type (snd e) = Tfloat. - -Proof. -Admitted. -(* -intros e s env H. -unfold regmreg_edge_type_partition in H. -set (f := (fun (e : SetRegMreg.elt) (s : SetRegMreg.t * SetRegMreg.t) => - match env (fst e) with - | Tint => - match mreg_type (snd e) with - | Tint => (SetRegMreg.add e (fst s), snd s) - | Tfloat => s - end - | Tfloat => - match mreg_type (snd e) with - | Tint => s - | Tfloat => (fst s, SetRegMreg.add e (snd s)) - end - end)) in H. - -cut (forall e set1 set2, SetRegMreg.In e (snd (SetRegMreg.fold f s (set1, set2))) -> - (env (fst e) = Tfloat /\ mreg_type (snd e) = Tfloat) \/ SetRegMreg.In e set2). - -intros. -generalize (H0 _ _ _ H). clear H H0. intro H. -destruct H. assumption. elim (SetRegMreg.empty_1 H). - -(* cut property *) -intros. -generalize H0. clear H H0. intro H. -rewrite SetRegMreg.fold_1 in H. -generalize H. clear H. generalize set1 set2. -induction (SetRegMreg.elements s); intros s1 s2 H. -simpl in H. right. assumption. -simpl in H. - -assert ((f a (s1, s2) = (SetRegMreg.add a s1, s2) /\ - env (fst a) = Tint /\ - mreg_type (snd a) = Tint)\/ - (f a (s1, s2) = (s1, SetRegMreg.add a s2) /\ - env (fst a) = Tfloat /\ - mreg_type (snd a) = Tfloat) \/ - f a (s1, s2) = (s1,s2)). -unfold f. -destruct (mreg_type (snd a)); destruct (env (fst a)); simpl. -left. auto. -right. right. reflexivity. -right. right. reflexivity. -right. left. auto. - -destruct H0. -destruct H0. destruct H1. rewrite H0 in H. -apply (IHl (SetRegMreg.add a s1) s2 H). - -destruct H0. destruct H0. destruct H1. rewrite H0 in H. -generalize (IHl s1 (SetRegMreg.add a s2) H). intro. -destruct H3. -left. auto. -destruct (proj1 (add_iff _ _ _) H3). -destruct H4. left. rewrite H4 in *. rewrite H5 in *. intuition. -right. auto. -rewrite H0 in H. apply (IHl s1 s2 H). -Qed. - -Definition Typed_interfgraphs g env := -let (int_regreg_interf, float_regreg_interf) := - regreg_edge_type_partition (interf_reg_reg g) env in -let (int_regmreg_interf, float_regmreg_interf) := - regmreg_edge_type_partition (interf_reg_mreg g) env in -let (int_regreg_pref, float_regreg_pref) := - regreg_edge_type_partition (pref_reg_reg g) env in -let (int_regmreg_pref, float_regmreg_pref) := - regmreg_edge_type_partition (pref_reg_mreg g) env in -(mkgraph int_regreg_interf int_regmreg_interf int_regreg_pref int_regmreg_pref, - mkgraph float_regreg_interf float_regmreg_interf float_regreg_pref float_regmreg_pref). -*) - - |