diff options
Diffstat (limited to 'backend/MyRegisters.v')
-rwxr-xr-x | backend/MyRegisters.v | 143 |
1 files changed, 143 insertions, 0 deletions
diff --git a/backend/MyRegisters.v b/backend/MyRegisters.v new file mode 100755 index 00000000..c2c7460d --- /dev/null +++ b/backend/MyRegisters.v @@ -0,0 +1,143 @@ +Require Import OrderedType. +Require Import Registers. +Require Import NArith. +Require Import Locations. +Require Import InterfGraph. + +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. + +(* Definition of registers as Pseudo-registers or machine registers *) + +Module Import Regs <: OrderedType. + +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. + +Definition is_mreg x := +match x with +| P _ => false +| M _ => true +end. + +Lemma mreg_ext : forall x y, +Regs.eq x y -> is_mreg x = is_mreg y. + +Proof. +intros. +destruct x; destruct y; simpl in *. +reflexivity. +inversion H. +inversion H. +reflexivity. +Qed. |