Module ValuesC
This module defines the type of values that is used in the dynamic semantics of all our intermediate languages.
Require
Import
CoqlibC
.
Require
Import
AST
.
Require
Import
Integers
.
Require
Import
Floats
.
Require
Import
sflib
.
newly added *
Require
Export
Values
.
Require
Import
Conventions1
.
Set
Implicit
Arguments
.
Global
Program
Instance
inject_incr_PreOrder
:
PreOrder
inject_incr
.
Next Obligation.
ii
.
eapply
inject_incr_trans
;
eauto
. Qed.
Section
TYPIFY
.
Lemma
Val_has_type_dec
:
forall
v
ty
,
{
Val.has_type
v
ty
} + {~
Val.has_type
v
ty
}.
Proof.
destruct
v
,
ty
;
ss
;
eauto
. Qed.
Definition
typify
(
v
:
val
) (
ty
:
typ
):
val
:=
if
Val_has_type_dec
v
ty
then
v
else
Vundef
.
Lemma
typify_has_type
:
forall
v
ty
,
<<
TYP
:
Val.has_type
(
typify
v
ty
)
ty
>>.
Proof.
i
.
unfold
typify
.
des_ifs
. Qed.
Definition
typify_list
(
vs
:
list
val
) (
tys
:
list
typ
):
list
val
:=
zip
typify
vs
tys
.
Lemma
typify_list_length
:
forall
vs
tys
,
length
(
typify_list
vs
tys
) =
Nat.min
(
length
vs
) (
length
tys
).
Proof.
i
.
ginduction
vs
;
ii
;
ss
.
destruct
tys
;
ss
.
rewrite
IHvs
;
ss
.
Qed.
End
TYPIFY
.
Hint
Unfold
typify
typify_list
.
Lemma
lessdef_typify
x
y
ty
(
LD
:
Val.lessdef
x
y
):
<<
LD
:
Val.lessdef
(
typify
x
ty
) (
typify
y
ty
)>>.
Proof.
unfold
typify
.
des_ifs
.
inv
LD
;
ss
. Qed.
Lemma
inject_typify
j
x
y
ty
(
INJ
:
Val.inject
j
x
y
):
<<
INJ
:
Val.inject
j
(
typify
x
ty
) (
typify
y
ty
)>>.
Proof.
unfold
typify
.
des_ifs
.
inv
INJ
;
ss
. Qed.
Lemma
lessdef_list_typify_list
xs
ys
tys
(
LEN
:
length
tys
=
length
xs
)
(
LD
:
Val.lessdef_list
xs
ys
):
<<
LD
:
Val.lessdef_list
(
typify_list
xs
tys
) (
typify_list
ys
tys
)>>.
Proof.
ginduction
LD
;
ii
;
ss
.
unfold
typify_list
.
ss
.
des_ifs
.
ss
.
econs
;
eauto
.
-
eapply
lessdef_typify
;
eauto
.
-
eapply
IHLD
;
eauto
.
Qed.
Lemma
lessdef_list_length
xs
ys
(
LD
:
Val.lessdef_list
xs
ys
):
<<
LEN
:
xs
.(
length
) =
ys
.(
length
)>>.
Proof.
ginduction
LD
;
ii
;
ss
.
des
.
red
.
xomega
. Qed.
Lemma
inject_list_typify_list
inj
xs
ys
tys
(
LEN
:
length
tys
=
length
xs
)
(
LD
:
Val.inject_list
inj
xs
ys
):
<<
LD
:
Val.inject_list
inj
(
typify_list
xs
tys
) (
typify_list
ys
tys
)>>.
Proof.
ginduction
LD
;
ii
;
ss
.
unfold
typify_list
.
ss
.
des_ifs
.
ss
.
econs
;
eauto
.
-
eapply
inject_typify
;
eauto
.
-
eapply
IHLD
;
eauto
.
Qed.
Lemma
inject_list_length
j
xs
ys
(
INJ
:
Val.inject_list
j
xs
ys
):
<<
LEN
:
xs
.(
length
) =
ys
.(
length
)>>.
Proof.
ginduction
INJ
;
ii
;
ss
.
des
.
red
.
xomega
. Qed.
Lemma
typify_has_type_list
vs
tys
(
LEN
:
length
vs
=
length
tys
):
<<
TYS
:
Val.has_type_list
(
typify_list
vs
tys
)
tys
>>.
Proof.
ginduction
vs
;
ii
;
ss
.
{
des_ifs
. }
destruct
tys
;
ss
.
clarify
.
esplits
;
eauto
.
-
eapply
typify_has_type
.
-
eapply
IHvs
;
eauto
.
Qed.
Lemma
has_type_typify
v
ty
(
TY
:
Val.has_type
v
ty
):
<<
TY
: (
typify
v
ty
) =
v
>>.
Proof.
rr
.
unfold
typify
.
des_ifs
. Qed.
Lemma
has_type_list_typify
vs
tys
(
TYS
:
Val.has_type_list
vs
tys
):
<<
TYS
: (
typify_list
vs
tys
) =
vs
>>.
Proof.
ginduction
vs
;
ii
;
ss
.
destruct
tys
;
ss
.
des
.
unfold
typify_list
.
ss
.
r
.
f_equal
.
-
eapply
has_type_typify
;
et
.
-
eapply
IHvs
;
et
.
Qed.
Inductive
typecheck
(
vs
:
list
val
) (
sg
:
signature
) (
tvs
:
list
val
):
Prop
:=
|
typecheck_intro
(
LEN
:
length
vs
=
length
sg
.(
sig_args
))
(
TYP
:
typify_list
vs
sg
.(
sig_args
) =
tvs
).
Lemma
Val_hiword_spec
vhi
vlo
(
DEFINED
: (
Val.longofwords
vhi
vlo
) <>
Vundef
):
<<
EQ
: (
Val.hiword
(
Val.longofwords
vhi
vlo
)) =
vhi
>>.
Proof.
u
.
unfold
Val.longofwords
,
Val.hiword
.
des_ifs
;
ss
;
eauto
.
rewrite
Int64.hi_ofwords
.
ss
.
Qed.
Lemma
Val_loword_spec
vhi
vlo
(
DEFINED
: (
Val.longofwords
vhi
vlo
) <>
Vundef
):
<<
EQ
: (
Val.loword
(
Val.longofwords
vhi
vlo
)) =
vlo
>>.
Proof.
u
.
unfold
Val.longofwords
,
Val.loword
.
des_ifs
;
ss
;
eauto
.
rewrite
Int64.lo_ofwords
.
ss
.
Qed.