source: src/RTLabs/syntax.ma @ 887

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

Start bringing RTLabs into line with the prototype compiler:

  • a coarse-grained type is associated with every register
  • the special addressing modes have been removed
File size: 2.4 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(* Statements, including the label of successor(s). *)
13
14inductive statement : Type[0] ≝
15| St_skip : label → statement
16| St_cost : costlabel → label → statement
17| St_const : register → constant → label → statement
18| St_op1 : unary_operation → register → register → label → statement
19| St_op2 : binary_operation → register → register → register → label → statement
20| St_load : memory_chunk → register → register → label → statement
21| St_store : memory_chunk → register → register → label → statement
22| St_call_id : ident → list register → option register → label → statement
23| St_call_ptr : register → list register → option register → label → statement
24| St_tailcall_id : ident → list register → statement
25| St_tailcall_ptr : register → list register → statement
26(* Um, what? *)
27| St_condcst : constant → label → label → statement
28| St_cond1 : unary_operation → register → label → label → statement
29| St_cond2 : binary_operation → register → register → label → label → statement
30| St_jumptable : register → list label → statement
31| St_return : statement
32.
33
34record internal_function : Type[0] ≝
35{ f_labgen    : universe LabelTag
36; f_reggen    : universe RegisterTag
37; f_result    : option (register × typ)
38; f_params    : list (register × typ)
39; f_locals    : list (register × typ)
40; f_stacksize : nat
41; f_graph     : graph statement
42; f_entry     : label
43; f_exit      : label
44}.
45
46(* Note that the global variables will be initialised by the code in main
47   by this stage.  All initialisation data should only reserve space. *)
48
49definition RTLabs_program ≝ program (fundef internal_function) unit.
50
51(* TO CONSIDER:
52
53   - removing most successor labels from the statements (bit icky, what about
54     return and jump tables?)
55   - seems like load and store ought to have types that control the size of the
56     register list based on the addressing mode; similarly, memory_chunk and
57     register are probably related.
58   - label and register generation really tell us something about the sets of
59     labels and register that may appear, perhaps it should be renamed, or the
60     graph made dependent on them to make it obvious, etc.
61 *)
Note: See TracBrowser for help on using the repository browser.