Module BTLtoRTL
Require
Import
Maps
.
Require
Import
AST
.
Require
Import
RTL
.
Require
Export
BTLmatchRTL
.
Require
Import
Errors
.
Module
Type
BTLtoRTL_TranslationOracle
.
External oracle that can be configured according to the translation mode
Parameter
btl2rtl
:
BTL.function
->
RTL.code
*
node
* (
PTree.t
node
).
End
BTLtoRTL_TranslationOracle
.
Module
BTLtoRTL_Translation
(
B
:
BTLtoRTL_TranslationOracle
).
Export
B
.
Local
Open
Scope
error_monad_scope
.
Definition
transf_function
(
f
:
BTL.function
) :
res
RTL.function
:=
let
(
tcte
,
dupmap
) :=
btl2rtl
f
in
let
(
tc
,
te
) :=
tcte
in
let
f'
:=
RTL.mkfunction
(
fn_sig
f
) (
fn_params
f
) (
fn_stacksize
f
)
tc
te
in
do
u
<-
verify_function
dupmap
f
f'
false
;
OK
f'
.
Definition
transf_fundef
(
f
:
fundef
) :
res
RTL.fundef
:=
transf_partial_fundef
transf_function
f
.
Definition
transf_program
(
p
:
program
) :
res
RTL.program
:=
transform_partial_program
transf_fundef
p
.
End
BTLtoRTL_Translation
.