source: src/ERTL/ERTL.ma @ 1241

Last change on this file since 1241 was 1241, checked in by mulligan, 9 years ago

changes for claudio

File size: 1.1 KB
Line 
1include "joint/Joint.ma".
2include "common/Graphs.ma".
3
4definition registers ≝ list register.
5
6inductive move_registers: Type[0] ≝
7  | pseudo: register → move_registers
8  | hardware: Register → move_registers.
9                 
10inductive ertl_statement_extension: Type[0] ≝
11  | ertl_st_ext_new_frame: label → ertl_statement_extension
12  | ertl_st_ext_del_frame: label → ertl_statement_extension
13  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
14
15definition ertl_params_: params_ ≝
16  mk_params_ register register register register
17    (move_registers × move_registers) register
18      ertl_statement_extension unit (list register) nat.
19
20definition ertl_params: params ≝
21  mk_params ertl_params_ label.
22
23definition ertl_statement ≝ joint_statement ertl_params.
24
25(*
26definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
27 λglobals.
28  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
29*)
30
31definition ertl_internal_function ≝
32  joint_internal_function ertl_params.
33
34definition ertl_program ≝ joint_program ertl_params.
Note: See TracBrowser for help on using the repository browser.