source: src/ERTL/ERTL.ma @ 1183

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

removed parameterised label types in the three lowest level languages

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