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
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(* 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
35definition addr ≝ λm.Vector register (addr_mode_args m).
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
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
51(* Um, what? *)
52| St_condcst : constant → label → label → statement
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
57.
58
59record internal_function : Type[0] ≝
60{ f_labgen    : universe LabelTag
61; f_reggen    : universe RegisterTag
62; f_sig       : signature
63; f_result    : option register
64; f_params    : list register
65; f_locals    : list register
66; f_ptrs      : list register
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 ≝
74λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
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
86     register list based on the addressing mode; similarly, memory_chunk and
87     register are probably related.
88   - label and register generation really tell us something about the sets of
89     labels and register that may appear, perhaps it should be renamed, or the
90     graph made dependent on them to make it obvious, etc.
91 *)
Note: See TracBrowser for help on using the repository browser.