source: src/RTL/RTL.ma @ 783

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

rtl to ertl pass complete (modulo some straightforward axioms that need filling in) and refactoring to get rid of all the option types.

File size: 2.5 KB
Line 
1include "basics/list.ma".
2include "common/Registers.ma".
3include "common/AST.ma".
4include "common/Graphs.ma".
5include "common/CostLabel.ma".
6include "ASM/I8051.ma".
7
8definition registers ≝ list register.
9
10inductive rtl_statement: Type[0] ≝
11  | rtl_st_skip: label → rtl_statement
12  | rtl_st_cost: costlabel → label → rtl_statement
13  | rtl_st_addr: register → register → ident → label → rtl_statement
14  | rtl_st_stack_addr: register → register → label → rtl_statement
15  | rtl_st_int: register → Byte → label → rtl_statement
16  | rtl_st_move: register → register → label → rtl_statement
17  | rtl_st_opaccs: OpAccs → register → register → register → label → rtl_statement
18  | rtl_st_op1: Op1 → register → register → label → rtl_statement
19  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
20  | rtl_st_clear_carry: label → rtl_statement
21  | rtl_st_load: register → register → register → label → rtl_statement
22  | rtl_st_store: register → register → register → label → rtl_statement
23  | rtl_st_call_id: ident → registers → registers → label → rtl_statement
24  | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
25  | rtl_st_tailcall_id: ident → registers → rtl_statement
26  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
27  | rtl_st_cond_acc: register → label → label → rtl_statement
28  | rtl_st_return: registers → rtl_statement.
29 
30definition rtl_statement_graph ≝ graph rtl_statement.
31
32record rtl_internal_function: Type[0] ≝
33{
34  rtl_if_luniverse: universe LabelTag;
35  rtl_if_runiverse: universe RegisterTag;
36  rtl_if_sig: signature;
37  rtl_if_result: registers;
38  rtl_if_params: registers;
39  rtl_if_locals: registers;
40  rtl_if_stacksize: nat;
41  rtl_if_graph: rtl_statement_graph;
42  rtl_if_entry: label;
43  rtl_if_exit: label
44}.
45
46definition rtl_if_stacksize: rtl_internal_function → nat.
47  # R
48  cases R
49  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8 # H9 # H10
50  @ H7
51qed.
52
53inductive rtl_function_definition: Type[0] ≝
54  | rtl_f_internal: rtl_internal_function → rtl_function_definition
55  | rtl_f_external: external_function → rtl_function_definition.
56 
57record rtl_program: Type[0] ≝
58{
59  rtl_pr_vars: list (ident × nat);
60  rtl_pr_functs: list (ident × rtl_function_definition);
61  rtl_pr_main: option ident
62}.
63
64definition rtl_pr_vars: rtl_program → list (ident × nat).
65  # P
66  cases P
67  # H1 # H2 # H3
68  @ H1
69qed.
Note: See TracBrowser for help on using the repository browser.