source: src/ERTL/ERTL.ma @ 1463

Last change on this file since 1463 was 1388, checked in by sacerdot, 8 years ago

fetch_result implemented for ERTL. This required a different istantiation of
resultT that is not in line with the OCaml's code. Look at CHANGES for details.
RTLToERTL has been ported in an hopefully correct manner.

File size: 1.1 KB
RevLine 
[1168]1include "joint/Joint.ma".
[733]2
[1163]3inductive move_registers: Type[0] ≝
4  | pseudo: register → move_registers
5  | hardware: Register → move_registers.
[1161]6                 
[1171]7inductive ertl_statement_extension: Type[0] ≝
[1254]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.
[1161]11
[1280]12definition ertl_params__: params__ ≝
13 mk_params__ register register register register (move_registers × move_registers)
14  register nat unit ertl_statement_extension.
15definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
[1388]16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ (list register) nat.
[1280]17definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
18definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
[1241]19
[1248]20definition ertl_statement ≝ joint_statement ertl_params_.
[1178]21
[1248]22definition ertl_internal_function ≝
[1280]23  λglobals.joint_internal_function … (ertl_params globals).
[1248]24
[1388]25definition ertl_program ≝ joint_program ertl_params.
Note: See TracBrowser for help on using the repository browser.