source: src/RTLabs/syntax.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.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
[1071]37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
[639]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.