source: src/ERTL/ERTL.ma @ 756

Last change on this file since 756 was 756, checked in by mulligan, 10 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.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
8inductive abstract_register: Type[0] ≝
9  mk_abstract_register: Word → abstract_register.
10
11definition abstract_registers ≝ list abstract_register.
12
13definition registers ≝ list register.
14
15inductive ertl_statement: Type[0] ≝
16  | ertl_st_skip: ident → ertl_statement
17  | ertl_st_comment: String → ident → ertl_statement
18  | ertl_st_cost: costlabel → ident → ertl_statement
19  | ertl_st_get_hdw: register → abstract_register → ident → ertl_statement
20  | ertl_st_set_hdw: abstract_register → register → ident → ertl_statement
21  | ertl_st_hdw_to_hdw: register → register → ident → ertl_statement
22  | ertl_st_new_frame: ident → ertl_statement
23  | ertl_st_del_frame: ident → ertl_statement
24  | ertl_st_frame_size: abstract_register → ident → ertl_statement
25  | ertl_st_pop: abstract_register → ident → ertl_statement
26  | ertl_st_push: abstract_register → ident → ertl_statement
27  | ertl_st_addr_h: abstract_register → ident → ident → ertl_statement
28  | ertl_st_addr_l: abstract_register → ident → ident → ertl_statement
29  | ertl_st_int: abstract_register → Byte → ident → ertl_statement
30  | ertl_st_move: abstract_register → abstract_register → ident → ertl_statement
31  | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident → ertl_statement
32  | ertl_st_op1: Op1 → abstract_register → abstract_register → ident → ertl_statement
33  | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident → ertl_statement
34  | ertl_st_clear_carry: ident → ertl_statement
35  | ertl_st_load: abstract_register → abstract_register → abstract_register → ident → ertl_statement
36  | ertl_st_store: abstract_register → abstract_register → abstract_register → ident → ertl_statement
37  | ertl_st_call_id: ident → Byte → ident → ertl_statement
38  | ertl_st_cond_acc: abstract_register → ident → ident → ertl_statement
39  | ertl_st_return: abstract_registers → ertl_statement.
40
41definition ertl_statement_graph ≝ graph ertl_statement.
42
43record ertl_internal_function: Type[0] ≝
44{
45  ertl_if_luniverse: universe LabelTag;
46  ertl_if_runiverse: universe RegisterTag;
47  ertl_if_params: nat;
48  ertl_if_locals: registers;
49  ertl_if_graph: ertl_statement_graph;
50  ertl_if_entry: ident;
51  ertl_if_exit: ident
52}.
53
54inductive ertl_function: Type[0] ≝
55  | ertl_fu_internal: ertl_internal_function → ertl_function
56  | ertl_fu_external: external_function → ertl_function.
57 
58record ertl_program: Type[0] ≝
59{
60  ertl_pr_vars: list (ident × nat);
61  ertl_pr_funcs: list (ident × ertl_function);
62  ertl_pr_main: option ident
63}.
64
65definition ertl_pr_vars: ertl_program → list (ident × nat).
66  # E
67  cases E
68  # H1 # H2 # H3
69  @ H1
70qed.
Note: See TracBrowser for help on using the repository browser.