diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
commit | 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac (patch) | |
tree | 1f8ce41f366bf19b777a1934ae0b1eb09be0a9f3 /backend/Regs.v | |
parent | 33a4bcf3695d0ee2793b3bdd12f6ee787d152f36 (diff) | |
download | compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.tar.gz compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.zip |
Backtracking on commit 1220v1.6
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Regs.v')
-rwxr-xr-x | backend/Regs.v | 122 |
1 files changed, 0 insertions, 122 deletions
diff --git a/backend/Regs.v b/backend/Regs.v deleted file mode 100755 index 33e3fea9..00000000 --- a/backend/Regs.v +++ /dev/null @@ -1,122 +0,0 @@ -Require Import Registers. - - -Definition op_plus (x y : option N) : option N := -match (x,y) with -|(None,None) => None -|(Some a,Some b) => Some (Nplus a b) -|(Some a,None) => Some a -|(None,Some b) => Some b -end. - -Module Regs <: OrderedType. - -(* Definition of registers as Pseudo-registers or machine registers *) - -Inductive registers : Type := -|P : reg -> registers -|M : mreg -> registers. - -Definition t := registers. - -Definition reg_to_Reg := fun r => P r. -Definition mreg_to_Reg := fun r => M r. - -Inductive req : t -> t -> Prop := -|Peq : forall x y, eq x y -> req (P x) (P y) -|Meq : forall x y, eq x y -> req (M x) (M y). - -Definition eq := req. - -Inductive rlt : t -> t -> Prop := -|Plt : forall x y, OrderedReg.lt x y -> rlt (P x) (P y) -|Mlt : forall x y, OrderedMreg.lt x y -> rlt (M x) (M y) -|PMlt : forall x y, rlt (M x) (P y). - -Definition lt := rlt. - -Lemma eq_refl : forall x, eq x x. - -Proof. -induction x;constructor;reflexivity. -Qed. - -Lemma eq_sym : forall x y, eq x y -> eq y x. - -Proof. -induction 1;rewrite H;apply eq_refl. -Qed. - -Lemma eq_trans : forall x y z, eq x y -> eq y z -> eq x z. - -Proof. -intros x y z H H0. -inversion H;inversion H0;subst. -rewrite H5;apply eq_refl. -inversion H5. -inversion H5. -rewrite H5;apply eq_refl. -Qed. - -Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z. - -Proof. -intros x y z H H0. -inversion H;inversion H0;subst. -inversion H5;subst. -constructor. apply (OrderedReg.lt_trans H1 H4). -inversion H5. -inversion H4. -inversion H5. -inversion H5;subst. -constructor. apply (OrderedMreg.lt_trans _ _ _ H1 H4). -constructor. -constructor. -inversion H4. -constructor. -Qed. - -Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. - -Proof. -induction 1;intro H0;inversion H0. -elim (OrderedReg.lt_not_eq H H3). -elim (OrderedMreg.lt_not_eq _ _ H H3). -Qed. - -Lemma compare : forall x y, Compare lt eq x y. - -Proof. -intros x y. -destruct x;destruct y. -destruct (OrderedReg.compare r r0). -apply LT. constructor. assumption. -apply EQ. constructor. assumption. -apply GT. constructor. assumption. -apply GT. constructor. -apply LT. constructor. -destruct (OrderedMreg.compare m m0). -apply LT. constructor. assumption. -apply EQ. constructor. assumption. -apply GT. constructor. assumption. -Qed. - -Lemma eq_dec : forall x y, {eq x y}+{~eq x y}. - -Proof. -intros x y. -destruct (compare x y). -right. apply lt_not_eq. assumption. -left. assumption. -right. (cut (~ eq y x)). -intros H H0. elim H. apply eq_sym. assumption. -apply lt_not_eq. assumption. -Qed. - -Definition get_type x env := -match x with -| P y => env y -| M y => mreg_type y -end. - -End Regs.
\ No newline at end of file |