source: src/ERTL/ERTL.ma @ 1221

Last change on this file since 1221 was 1221, checked in by sacerdot, 9 years ago

Cleanup.

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
17   register register register register
18     (move_registers × move_registers) register
19       ertl_statement_extension unit (list register) nat.
20
21definition ertl_statement ≝ joint_statement ertl_params.
22
23definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
24 λglobals.
25  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
26
27(*
28definition ertl_internal_function ≝
29 λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
30*)
31
32definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
Note: See TracBrowser for help on using the repository browser.