source: src/ERTL/ERTL.ma @ 1248

Last change on this file since 1248 was 1248, checked in by mulligan, 9 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.