source: src/ERTL/ERTL.ma @ 1248

Last change on this file since 1248 was 1248, checked in by mulligan, 10 years ago

deleted files that do not compile in utilities, changed ertl.ma to use new joint syntax

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