source: src/ERTL/ERTL.ma @ 1168

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

Joint statements parameterized over a record.

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