source: src/ERTL/ERTL.ma @ 1246

Last change on this file since 1246 was 1242, checked in by sacerdot, 8 years ago

Some clean-up.

File size: 816 bytes
Line 
1include "joint/Joint.ma".
2
3inductive move_registers: Type[0] ≝
4  | pseudo: register → move_registers
5  | hardware: Register → move_registers.
6                 
7inductive ertl_statement_extension: Type[0] ≝
8  | ertl_st_ext_new_frame: label → ertl_statement_extension
9  | ertl_st_ext_del_frame: label → ertl_statement_extension
10  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
11
12definition ertl_params: params ≝
13 mk_params
14  (mk_params_ register register register register
15    (move_registers × move_registers) register
16      ertl_statement_extension unit (list register) nat) label.
17
18definition ertl_statement ≝ joint_statement ertl_params.
19
20definition ertl_internal_function ≝ joint_internal_function ertl_params.
21
22definition ertl_program ≝ joint_program ertl_params.
Note: See TracBrowser for help on using the repository browser.