source: src/ERTL/ERTL.ma @ 1220

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

ERTL ported to the new joint syntax.

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