source: src/ERTL/ERTL.ma @ 1175

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

changes to ertl pass

File size: 2.6 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 set_luniverse ≝
40  λglobals  : list ident.
41  λint_fun  : ertl_internal_function globals.
42  λluniverse: universe LabelTag.
43  let runiverse ≝ ertl_if_runiverse globals int_fun in
44  let params    ≝ ertl_if_params globals int_fun in
45  let locals    ≝ ertl_if_locals globals int_fun in
46  let stacksize ≝ ertl_if_stacksize globals int_fun in
47  let graph     ≝ ertl_if_graph globals int_fun in
48  let entry     ≝ ertl_if_entry globals int_fun in
49  let exit      ≝ ertl_if_exit globals int_fun in
50    mk_ertl_internal_function globals
51      luniverse runiverse params locals
52      stacksize graph entry exit.
53
54definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
55 
56record ertl_program (globals: list ident): Type[0] ≝
57{
58  ertl_pr_vars: list (ident × nat);
59  ertl_pr_funcs: list (ident × (ertl_function globals));
60  ertl_pr_main: option ident
61}.
62
63
64(* XXX: changed from O'Caml
65  | ertl_st_addr_h: register → ident → label → ertl_statement
66  | ertl_st_addr_l: register → ident → label → ertl_statement
67*)
68
69(* XXX: changed from O'Caml
70  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
71  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
72*)
Note: See TracBrowser for help on using the repository browser.