source: src/RTLabs/syntax.ma @ 1066

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

Switch to delayed identifier error scheme.

File size: 2.2 KB
RevLine 
[639]1
2include "basics/logic.ma".
3
[747]4include "common/AST.ma".
[720]5include "common/CostLabel.ma".
[702]6include "common/FrontEndOps.ma".
7include "common/Registers.ma".
[639]8
[702]9include "ASM/Vector.ma".
10include "common/Graphs.ma".
[639]11
12inductive statement : Type[0] ≝
13| St_skip : label → statement
14| St_cost : costlabel → label → statement
[1056]15| St_const : register → constant → label → statement
[750]16| St_op1 : unary_operation → register → register → label → statement
17| St_op2 : binary_operation → register → register → register → label → statement
[887]18| St_load : memory_chunk → register → register → label → statement
19| St_store : memory_chunk → register → register → label → statement
[816]20| St_call_id : ident → list register → option register → label → statement
21| St_call_ptr : register → list register → option register → label → statement
22| St_tailcall_id : ident → list register → statement
23| St_tailcall_ptr : register → list register → statement
[888]24| St_cond : register → label → label → statement
[750]25| St_jumptable : register → list label → statement
[765]26| St_return : statement
[639]27.
28
29record internal_function : Type[0] ≝
[738]30{ f_labgen    : universe LabelTag
31; f_reggen    : universe RegisterTag
[887]32; f_result    : option (register × typ)
33; f_params    : list (register × typ)
34; f_locals    : list (register × typ)
[639]35; f_stacksize : nat
36; f_graph     : graph statement
37; f_entry     : label
38; f_exit      : label
39}.
40
[764]41(* Note that the global variables will be initialised by the code in main
42   by this stage.  All initialisation data should only reserve space. *)
[639]43
[764]44definition RTLabs_program ≝ program (fundef internal_function) unit.
[639]45
46(* TO CONSIDER:
47
48   - removing most successor labels from the statements (bit icky, what about
49     return and jump tables?)
50   - seems like load and store ought to have types that control the size of the
[750]51     register list based on the addressing mode; similarly, memory_chunk and
52     register are probably related.
[639]53   - label and register generation really tell us something about the sets of
[750]54     labels and register that may appear, perhaps it should be renamed, or the
[639]55     graph made dependent on them to make it obvious, etc.
[720]56 *)
Note: See TracBrowser for help on using the repository browser.