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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
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.
|
