source: src/ERTL/ERTL.ma @ 1178

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

fixed ertl.ma to use new version of joint params

File size: 2.6 KB
RevLine 
[733]1include "ASM/I8051.ma".
[1168]2include "joint/Joint.ma".
[733]3include "utilities/BitVectorTrieSet.ma".
4include "utilities/IdentifierTools.ma".
5include "common/Graphs.ma".
[756]6include "common/CostLabel.ma".
7include "common/Registers.ma".
[733]8
[756]9definition registers ≝ list register.
[733]10
[1163]11inductive move_registers: Type[0] ≝
12  | pseudo: register → move_registers
13  | hardware: Register → move_registers.
[1161]14                 
[1171]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.
[1161]19
[1178]20definition ertl_params: params ≝
21 mk_params
22   label register register register register
23     (move_registers × move_registers) register
24       ertl_statement_extension unit (list register) nat.
[1171]25
[1178]26definition ertl_statement ≝ joint_statement ertl_params.
27
[1161]28definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
[756]29
[1161]30record ertl_internal_function (globals: list ident): Type[0] ≝
[733]31{
[756]32  ertl_if_luniverse: universe LabelTag;
33  ertl_if_runiverse: universe RegisterTag;
34  ertl_if_params: nat;
35  ertl_if_locals: registers;
[782]36  ertl_if_stacksize: nat;
[1161]37  ertl_if_graph: ertl_statement_graph globals;
[1077]38  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
39  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
[733]40}.
41
[1175]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
[1161]57definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
[733]58 
[1161]59record ertl_program (globals: list ident): Type[0] ≝
[733]60{
[756]61  ertl_pr_vars: list (ident × nat);
[1161]62  ertl_pr_funcs: list (ident × (ertl_function globals));
[783]63  ertl_pr_main: option ident
[733]64}.
[1161]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
[1168]75*)
Note: See TracBrowser for help on using the repository browser.