source: src/RTLabs/syntax.ma @ 878

Last change on this file since 878 was 878, checked in by campbell, 9 years ago

Removal of manually inserted record projections.

File size: 3.1 KB
Line 
1
2include "basics/logic.ma".
3
4include "common/AST.ma".
5include "common/CostLabel.ma".
6include "common/FrontEndOps.ma".
7include "common/Registers.ma".
8
9include "ASM/Vector.ma".
10include "common/Graphs.ma".
11
12(* XXX: ASTish stuff *)
13
14definition immediate : Type[0] ≝ int.
15
16(* Addressing modes *)
17
18inductive addressing : Type[0] ≝
19| Aindexed  : immediate → addressing         (* r1 + offset *)
20| Aindexed2 : addressing                     (* r1 + r2 *)
21| Aglobal   : ident → immediate → addressing (* global + offset *)
22| Abased    : ident → immediate → addressing (* global + offset + r1 *)
23| Ainstack  : immediate → addressing         (* stack + offset *)
24.
25
26definition addr_mode_args : addressing → nat ≝
27λa. match a with
28[ Aindexed _  ⇒ 1
29| Aindexed2   ⇒ 2
30| Aglobal _ _ ⇒ 0
31| Abased _ _  ⇒ 1
32| Ainstack _  ⇒ 0
33].
34
35definition addr ≝ λm.Vector register (addr_mode_args m).
36
37(* Statements, including the label of successor(s). *)
38
39inductive statement : Type[0] ≝
40| St_skip : label → statement
41| St_cost : costlabel → label → statement
42| St_const : register → constant → label → statement
43| St_op1 : unary_operation → register → register → label → statement
44| St_op2 : binary_operation → register → register → register → label → statement
45| St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
46| St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
47| St_call_id : ident → list register → option register → label → statement
48| St_call_ptr : register → list register → option register → label → statement
49| St_tailcall_id : ident → list register → statement
50| St_tailcall_ptr : register → list register → statement
51(* Um, what? *)
52| St_condcst : constant → label → label → statement
53| St_cond1 : unary_operation → register → label → label → statement
54| St_cond2 : binary_operation → register → register → label → label → statement
55| St_jumptable : register → list label → statement
56| St_return : statement
57.
58
59record internal_function : Type[0] ≝
60{ f_labgen    : universe LabelTag
61; f_reggen    : universe RegisterTag
62; f_sig       : signature
63; f_result    : option register
64; f_params    : list register
65; f_locals    : list register
66; f_ptrs      : list register
67; f_stacksize : nat
68; f_graph     : graph statement
69; f_entry     : label
70; f_exit      : label
71}.
72
73(* Note that the global variables will be initialised by the code in main
74   by this stage.  All initialisation data should only reserve space. *)
75
76definition RTLabs_program ≝ program (fundef internal_function) unit.
77
78(* TO CONSIDER:
79
80   - removing most successor labels from the statements (bit icky, what about
81     return and jump tables?)
82   - seems like load and store ought to have types that control the size of the
83     register list based on the addressing mode; similarly, memory_chunk and
84     register are probably related.
85   - label and register generation really tell us something about the sets of
86     labels and register that may appear, perhaps it should be renamed, or the
87     graph made dependent on them to make it obvious, etc.
88 *)
Note: See TracBrowser for help on using the repository browser.