source: src/RTLabs/syntax.ma @ 1045

Last change on this file since 1045 was 1045, checked in by mulligan, 10 years ago

resolved conflict in rtlabs

File size: 2.9 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
[1045]12definition immediate : Type[0] ≝ Byte.
[639]13
[1045]14(* Addressing modes *)
15
16inductive addressing : Type[0] ≝
17(* dpm: changed from int to Byte *)
18| Aindexed  : immediate → addressing         (* r1 + offset *)
19| Aindexed2 : addressing                     (* r1 + r2 *)
20| Aglobal   : ident → immediate → addressing (* global + offset *)
21| Abased    : ident → immediate → addressing (* global + offset + r1 *)
22| Ainstack  : immediate → addressing         (* stack + offset *)
23.
24
25definition addr_mode_args : addressing → nat ≝
26λa. match a with
27[ Aindexed _  ⇒ 1
28| Aindexed2   ⇒ 2
29| Aglobal _ _ ⇒ 0
30| Abased _ _  ⇒ 1
31| Ainstack _  ⇒ 0
32].
33
34definition addr ≝ λm.Vector register (addr_mode_args m).
35
[639]36inductive statement : Type[0] ≝
37| St_skip : label → statement
38| St_cost : costlabel → label → statement
[750]39| St_const : register → constant → label → statement
40| St_op1 : unary_operation → register → register → label → statement
41| St_op2 : binary_operation → register → register → register → label → statement
[887]42| St_load : memory_chunk → register → register → label → statement
43| St_store : memory_chunk → register → register → label → statement
[816]44| St_call_id : ident → list register → option register → label → statement
45| St_call_ptr : register → list register → option register → label → statement
46| St_tailcall_id : ident → list register → statement
47| St_tailcall_ptr : register → list register → statement
[888]48| St_cond : register → label → label → statement
[750]49| St_jumptable : register → list label → statement
[765]50| St_return : statement
[639]51.
52
53record internal_function : Type[0] ≝
[738]54{ f_labgen    : universe LabelTag
55; f_reggen    : universe RegisterTag
[887]56; f_result    : option (register × typ)
57; f_params    : list (register × typ)
58; f_locals    : list (register × typ)
[639]59; f_stacksize : nat
60; f_graph     : graph statement
61; f_entry     : label
62; f_exit      : label
63}.
64
[764]65(* Note that the global variables will be initialised by the code in main
66   by this stage.  All initialisation data should only reserve space. *)
[639]67
[764]68definition RTLabs_program ≝ program (fundef internal_function) unit.
[639]69
70(* TO CONSIDER:
71
72   - removing most successor labels from the statements (bit icky, what about
73     return and jump tables?)
74   - seems like load and store ought to have types that control the size of the
[750]75     register list based on the addressing mode; similarly, memory_chunk and
76     register are probably related.
[639]77   - label and register generation really tell us something about the sets of
[750]78     labels and register that may appear, perhaps it should be renamed, or the
[639]79     graph made dependent on them to make it obvious, etc.
[720]80 *)
Note: See TracBrowser for help on using the repository browser.