source: src/RTL/RTL.ma @ 773

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

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

File size: 2.3 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 → 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_condacc: 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}.
Note: See TracBrowser for help on using the repository browser.