source: src/RTLabs/syntax.ma @ 762

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

Make naming of RTLabs files more uniform

File size: 3.3 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
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
[750]35definition addr ≝ λm.Vector register (addr_mode_args m).
[639]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
[750]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 → signature → label → statement
48| St_call_ptr : register → list register → option register → signature → label → statement
49| St_tailcall_id : ident → list register → signature → statement
50| St_tailcall_ptr : register → list register → signature → statement
[639]51(* Um, what? *)
52| St_condcst : constant → label → label → statement
[750]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 : register → statement
[639]57.
58
59record internal_function : Type[0] ≝
[738]60{ f_labgen    : universe LabelTag
61; f_reggen    : universe RegisterTag
[639]62; f_sig       : signature
[750]63; f_result    : option register
64; f_params    : list register
65; f_locals    : list register
66; f_ptrs      : list register
[639]67; f_stacksize : nat
68; f_graph     : graph statement
69; f_entry     : label
70; f_exit      : label
71}.
72(* XXX: matita interpretations bug workaround *)
73definition f_stacksize : internal_function → nat ≝
[750]74λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
[639]75
76(* Global variables only need to be given their size at this stage of
77   compilation. *)
78
79definition RTLabs_program ≝ program (fundef internal_function) nat.
80
81(* TO CONSIDER:
82
83   - removing most successor labels from the statements (bit icky, what about
84     return and jump tables?)
85   - seems like load and store ought to have types that control the size of the
[750]86     register list based on the addressing mode; similarly, memory_chunk and
87     register are probably related.
[639]88   - label and register generation really tell us something about the sets of
[750]89     labels and register that may appear, perhaps it should be renamed, or the
[639]90     graph made dependent on them to make it obvious, etc.
[720]91 *)
Note: See TracBrowser for help on using the repository browser.