source: src/ERTL/ERTL.ma @ 782

Last change on this file since 782 was 782, checked in by mulligan, 10 years ago

More work on rtl-ertl pass from today, plus resolved conflict.

File size: 2.9 KB
Line 
1include "ASM/I8051.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "utilities/IdentifierTools.ma".
4include "common/Graphs.ma".
5include "common/CostLabel.ma".
6include "common/Registers.ma".
7
8definition hardware_register ≝ Register.
9definition registers ≝ list register.
10
11inductive ertl_statement: Type[0] ≝
12  | ertl_st_skip: label → ertl_statement
13  | ertl_st_comment: String → label → ertl_statement
14  | ertl_st_cost: costlabel → label → ertl_statement
15  | ertl_st_get_hdw: register → hardware_register → label → ertl_statement
16  | ertl_st_set_hdw: hardware_register → register → label → ertl_statement
17  | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement
18  | ertl_st_new_frame: label → ertl_statement
19  | ertl_st_del_frame: label → ertl_statement
20  | ertl_st_frame_size: register → label → ertl_statement
21  | ertl_st_pop: register → label → ertl_statement
22  | ertl_st_push: register → label → ertl_statement
23  | ertl_st_addr_h: register → ident → label → ertl_statement
24  | ertl_st_addr_l: register → ident → label → ertl_statement
25  | ertl_st_int: register → Byte → label → ertl_statement
26  | ertl_st_move: register → register → label → ertl_statement
27  | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement
28  | ertl_st_op1: Op1 → register → register → label → ertl_statement
29  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
30  | ertl_st_clear_carry: label → ertl_statement
31  | ertl_st_load: register → register → register → label → ertl_statement
32  | ertl_st_store: register → register → register → label → ertl_statement
33  | ertl_st_call_id: ident → Byte → label → ertl_statement
34  | ertl_st_cond_acc: register → label → label → ertl_statement
35  | ertl_st_return: registers → ertl_statement.
36
37definition ertl_statement_graph ≝ graph ertl_statement.
38
39record ertl_internal_function: Type[0] ≝
40{
41  ertl_if_luniverse: universe LabelTag;
42  ertl_if_runiverse: universe RegisterTag;
43  ertl_if_params: nat;
44  ertl_if_locals: registers;
45  ertl_if_stacksize: nat;
46  ertl_if_graph: ertl_statement_graph;
47  ertl_if_entry: label;
48  ertl_if_exit: label
49}.
50
51definition ertl_if_params: ertl_internal_function → nat.
52  # E
53  cases E
54  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
55  @ H3
56qed.
57
58definition ertl_if_stacksize: ertl_internal_function → nat.
59  # E
60  cases E
61  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
62  @ H5
63qed.
64
65inductive ertl_function: Type[0] ≝
66  | ertl_f_internal: ertl_internal_function → ertl_function
67  | ertl_f_external: external_function → ertl_function.
68 
69record ertl_program: Type[0] ≝
70{
71  ertl_pr_vars: list (ident × nat);
72  ertl_pr_funcs: list (ident × ertl_function);
73  ertl_pr_main: option label
74}.
75
76definition ertl_pr_vars: ertl_program → list (ident × nat).
77  # E
78  cases E
79  # H1 # H2 # H3
80  @ H1
81qed.
Note: See TracBrowser for help on using the repository browser.