Module AsmregsC
Require
Import
CoqlibC
Maps
.
Require
Import
ValuesC
.
Require
Import
LocationsC
Stacklayout
Conventions
.
Require
Import
MemoryC
Integers
AST
.
newly added *
Require
Import
Asm
.
Require
Import
Locations
.
Require
Mach
.
Set
Implicit
Arguments
.
Lemma
to_mreg_injective
pr0
pr1
(
SOME
:
is_some
(
pr0
.(
to_mreg
)))
(
EQ
:
pr0
.(
to_mreg
) =
pr1
.(
to_mreg
)):
<<
EQ
:
pr0
=
pr1
>>.
Proof.
destruct
pr0
;
ss
;
destruct
pr1
;
ss
;
des_ifs
. Qed.
Lemma
preg_of_injective
mr0
mr1
(
EQ
:
preg_of
mr0
=
preg_of
mr1
):
<<
EQ
:
mr0
=
mr1
>>.
Proof.
destruct
mr0
,
mr1
;
ss
. Qed.
Lemma
to_mreg_to_preg
:
forall
pr0
,
o_map
(
pr0
.(
to_mreg
)) (
to_preg
) =
Some
pr0
\/
pr0
.(
to_mreg
) =
None
.
Proof.
destruct
pr0
;
ss
;
des_ifs
;
eauto
. Qed.
Corollary
to_mreg_some_to_preg
pr0
mr0
(
SOME
:
pr0
.(
to_mreg
) =
Some
mr0
):
<<
EQ
:
mr0
.(
to_preg
) =
pr0
>>.
Proof.
eapply
to_mreg_injective
with
(
pr0
:=
mr0
.(
to_preg
)) (
pr1
:=
pr0
).
{
rewrite
to_preg_to_mreg
;
ss
. }
rewrite
to_preg_to_mreg
;
ss
.
Qed.
Definition
to_pregset
(
mrs
:
Mach.regset
):
regset
:=
fun
pr
=>
match
pr
.(
to_mreg
)
with
|
Some
mr
=>
mrs
mr
|
None
=>
Vundef
end
.
Definition
to_mregset
(
prs
:
regset
):
Mach.regset
:=
fun
mr
=>
prs
(
to_preg
mr
).
Lemma
to_mreg_preg_of
pr
mr
(
MR
:
Asm.to_mreg
pr
=
Some
mr
):
<<
PR
:
preg_of
mr
=
pr
>>.
Proof.
destruct
mr
,
pr
;
ss
;
des_ifs
. Qed.