|
Last change
on this file since 1363 was
1280,
checked in by sacerdot, 9 years ago
|
|
Some progress in the porting of RTLAbstoRTL to the joint syntax:
1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are
probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.
|
|
File size:
1.0 KB
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | |
|---|
| 3 | inductive move_registers: Type[0] ≝ |
|---|
| 4 | | pseudo: register → move_registers |
|---|
| 5 | | hardware: Register → move_registers. |
|---|
| 6 | |
|---|
| 7 | inductive ertl_statement_extension: Type[0] ≝ |
|---|
| 8 | | ertl_st_ext_new_frame: ertl_statement_extension |
|---|
| 9 | | ertl_st_ext_del_frame: ertl_statement_extension |
|---|
| 10 | | ertl_st_ext_frame_size: register → ertl_statement_extension. |
|---|
| 11 | |
|---|
| 12 | definition ertl_params__: params__ ≝ |
|---|
| 13 | mk_params__ register register register register (move_registers × move_registers) |
|---|
| 14 | register nat unit ertl_statement_extension. |
|---|
| 15 | definition ertl_params_: params_ ≝ graph_params_ ertl_params__. |
|---|
| 16 | definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat. |
|---|
| 17 | definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0. |
|---|
| 18 | definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0. |
|---|
| 19 | |
|---|
| 20 | definition ertl_statement ≝ joint_statement ertl_params_. |
|---|
| 21 | |
|---|
| 22 | definition ertl_internal_function ≝ |
|---|
| 23 | λglobals.joint_internal_function … (ertl_params globals). |
|---|
| 24 | |
|---|
| 25 | definition ertl_program ≝ joint_program ertl_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
