1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
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.
|
