Module RTLtypingC
Typing rules and a type inference algorithm for RTL.
Require
Import
CoqlibC
.
Require
Import
Errors
.
Require
Import
Unityping
.
Require
Import
Maps
.
Require
Import
AST
.
Require
Import
Op
.
Require
Import
Registers
.
Require
Import
Globalenvs
.
Require
Import
ValuesC
.
Require
Import
IntegersC
.
Require
Import
MemoryC
.
Require
Import
Events
.
Require
Import
RTLC
.
Require
Import
ConventionsC
.
Require
Import
sflib
.
newly added *
Require
Export
RTLtyping
.
Require
Import
Skeleton
ModSem
Preservation
.
Require
Import
SoundTop
.
Require
Import
RTLC
.
Section
LPRSV
.
Variable
prog
:
program
.
Hypothesis
wt_prog
:
forall
i
fd
,
In
(
i
,
Gfun
fd
)
prog
.(
prog_defs
) ->
wt_fundef
fd
.
Theorem
wt_state_local_preservation
:
forall
skenv_link
,
local_preservation
(
modsem2
skenv_link
prog
) (
fun
_
_
st
=>
wt_state
st
).
Proof.
econs
;
ii
;
ss
;
eauto
.
-
(* init *)
inv
INIT
.
econs
;
et
.
+
econs
;
et
.
+
inv
TYP
.
eapply
typify_has_type_list
;
et
.
-
(* step *)
eapply
subject_reduction
;
et
.
ii
.
unfold
Genv.find_funct
,
Genv.find_funct_ptr
in
*.
des_ifs
.
unfold
Skeleton.SkEnv.revive
in
*.
eapply
Genv_map_defs_def
in
Heq
.
des
.
u
in
MAP
.
des_ifs_safe
.
esplits
.
eapply
in_prog_defmap
;
eauto
.
-
esplits
;
eauto
.
{
rr
.
esplits
;
ss
;
eauto
.
des_ifs
.
esplits
;
ss
.
rr
.
rewrite
Forall_forall
.
ii
;
ss
. }
ii
.
inv
AFTER
.
inv
SUST
.
econs
;
et
.
apply
typify_has_type
.
-
esplits
;
eauto
.
rr
.
des_ifs
.
Unshelve
.
all
:
ss
.
Qed.
End
LPRSV
.