source: src/ERTL/ERTL.ma @ 1071

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

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File size: 2.6 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_a: OpAccs → register → register → register → label → ertl_statement
28  | ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement
29  | ertl_st_op1: Op1 → register → register → label → ertl_statement
30  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
31  | ertl_st_clear_carry: label → ertl_statement
32  | ertl_st_set_carry: label → ertl_statement
33  | ertl_st_load: register → register → register → label → ertl_statement
34  | ertl_st_store: register → register → register → label → ertl_statement
35  | ertl_st_call_id: ident → Byte → label → ertl_statement
36  | ertl_st_cond: register → label → label → ertl_statement
37  | ertl_st_return: ertl_statement. (* XXX: change from o'caml *)
38
39definition ertl_statement_graph ≝ graph ertl_statement.
40
41record ertl_internal_function: Type[0] ≝
42{
43  ertl_if_luniverse: universe LabelTag;
44  ertl_if_runiverse: universe RegisterTag;
45  ertl_if_params: nat;
46  ertl_if_locals: registers;
47  ertl_if_stacksize: nat;
48  ertl_if_graph: ertl_statement_graph;
49  ertl_if_entry: label;
50  ertl_if_exit: label
51}.
52
53definition ertl_function ≝ fundef ertl_internal_function.
54 
55record ertl_program: Type[0] ≝
56{
57  ertl_pr_vars: list (ident × nat);
58  ertl_pr_funcs: list (ident × ertl_function);
59  ertl_pr_main: option ident
60}.
Note: See TracBrowser for help on using the repository browser.