source: src/RTL/RTL.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.3 KB
Line 
1include "basics/list.ma".
2include "common/Registers.ma".
3include "common/AST.ma".
4include "common/Graphs.ma".
5include "common/CostLabel.ma".
6
7definition registers ≝ list register.
8
9inductive rtl_statement: Type[0] ≝
10  | rtl_st_skip: label → rtl_statement
11  | rtl_st_cost: costlabel → label → rtl_statement
12  | rtl_st_addr: register → register → ident → label → rtl_statement
13  | rtl_st_stack_addr: register → register → label → rtl_statement
14  | rtl_st_int: register → Byte → label → rtl_statement
15  | rtl_st_move: register → register → label → rtl_statement
16  | rtl_st_clear_carry: label → rtl_statement
17  | rtl_st_opaccs: OpAccs → register → 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_load: register → register → register → label → rtl_statement
21  | rtl_st_store: register → register → register → label → rtl_statement
22  | rtl_st_call_id: ident → registers → registers → label → rtl_statement
23  | rtl_st_call_ptr: register → register → registers → registers → label → rtl_statement
24  | rtl_st_tailcall_id: ident → registers → rtl_statement
25  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
26  | rtl_st_cond: register → label → label → rtl_statement
27  | rtl_st_set_carry: label → rtl_statement
28  | rtl_st_return: rtl_statement. (* XXX: change from o'caml *)
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;  -- dropped in front end *)
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    : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?;
43  rtl_if_exit     : Σl: label. lookup ? ? rtl_if_graph l ≠ None ?
44}.
45
46definition rtl_function_definition ≝ fundef rtl_internal_function.
47 
48record rtl_program: Type[0] ≝
49{
50  rtl_pr_vars: list (ident × nat);
51  rtl_pr_functs: list (ident × rtl_function_definition);
52  rtl_pr_main: option ident
53}.
Note: See TracBrowser for help on using the repository browser.