source: src/ERTL/ERTL.ma @ 1172

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

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

File size: 2.0 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
15definition ertl_params: params ≝
16 mk_params register register register register (move_registers × move_registers) register.
17                 
18inductive ertl_statement_extension: Type[0] ≝
19  | ertl_st_ext_new_frame: label → ertl_statement_extension
20  | ertl_st_ext_del_frame: label → ertl_statement_extension
21  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
22
23definition ertl_statement ≝ joint_statement label ertl_statement_extension ertl_params.
24
25definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
26
27record ertl_internal_function (globals: list ident): Type[0] ≝
28{
29  ertl_if_luniverse: universe LabelTag;
30  ertl_if_runiverse: universe RegisterTag;
31  ertl_if_params: nat;
32  ertl_if_locals: registers;
33  ertl_if_stacksize: nat;
34  ertl_if_graph: ertl_statement_graph globals;
35  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
36  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
37}.
38
39definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
40 
41record ertl_program (globals: list ident): Type[0] ≝
42{
43  ertl_pr_vars: list (ident × nat);
44  ertl_pr_funcs: list (ident × (ertl_function globals));
45  ertl_pr_main: option ident
46}.
47
48
49(* XXX: changed from O'Caml
50  | ertl_st_addr_h: register → ident → label → ertl_statement
51  | ertl_st_addr_l: register → ident → label → ertl_statement
52*)
53
54(* XXX: changed from O'Caml
55  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
56  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
57*)
Note: See TracBrowser for help on using the repository browser.