source: src/ERTL/ERTL.ma @ 1142

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

merged ertl_st_opaccs_a and ertl_st_opaccs_b into each other

File size: 2.8 KB
RevLine 
[733]1include "ASM/I8051.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "utilities/IdentifierTools.ma".
4include "common/Graphs.ma".
[756]5include "common/CostLabel.ma".
6include "common/Registers.ma".
[733]7
[756]8definition registers ≝ list register.
[733]9
[756]10inductive ertl_statement: Type[0] ≝
[759]11  | ertl_st_skip: label → ertl_statement
12  | ertl_st_comment: String → label → ertl_statement
13  | ertl_st_cost: costlabel → label → ertl_statement
[1082]14  | ertl_st_get_hdw: register → Register → label → ertl_statement
15  | ertl_st_set_hdw: Register → register → label → ertl_statement
16  | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
[759]17  | ertl_st_new_frame: label → ertl_statement
18  | ertl_st_del_frame: label → ertl_statement
[777]19  | ertl_st_frame_size: register → label → ertl_statement
20  | ertl_st_pop: register → label → ertl_statement
21  | ertl_st_push: register → label → ertl_statement
[1131]22  | ertl_st_addr: register → register → ident → label → ertl_statement
23(* XXX: changed from O'Caml
[782]24  | ertl_st_addr_h: register → ident → label → ertl_statement
25  | ertl_st_addr_l: register → ident → label → ertl_statement
[1131]26*)
[777]27  | ertl_st_int: register → Byte → label → ertl_statement
28  | ertl_st_move: register → register → label → ertl_statement
[1138]29  | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
30(* XXX: changed from O'Caml
[1071]31  | ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement
32  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
[1138]33*)
[777]34  | ertl_st_op1: Op1 → register → register → label → ertl_statement
35  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
[759]36  | ertl_st_clear_carry: label → ertl_statement
[1071]37  | ertl_st_set_carry: label → ertl_statement
[777]38  | ertl_st_load: register → register → register → label → ertl_statement
39  | ertl_st_store: register → register → register → label → ertl_statement
[1136]40  | ertl_st_call_id: ident → nat → label → ertl_statement
[1071]41  | ertl_st_cond: register → label → label → ertl_statement
[1107]42  | ertl_st_return: ertl_statement.
[733]43
[756]44definition ertl_statement_graph ≝ graph ertl_statement.
45
46record ertl_internal_function: Type[0] ≝
[733]47{
[756]48  ertl_if_luniverse: universe LabelTag;
49  ertl_if_runiverse: universe RegisterTag;
50  ertl_if_params: nat;
51  ertl_if_locals: registers;
[782]52  ertl_if_stacksize: nat;
[756]53  ertl_if_graph: ertl_statement_graph;
[1077]54  ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?;
55  ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?
[733]56}.
57
[1071]58definition ertl_function ≝ fundef ertl_internal_function.
[733]59 
[756]60record ertl_program: Type[0] ≝
[733]61{
[756]62  ertl_pr_vars: list (ident × nat);
63  ertl_pr_funcs: list (ident × ertl_function);
[783]64  ertl_pr_main: option ident
[733]65}.
Note: See TracBrowser for help on using the repository browser.