source: Deliverables/D3.1/C-semantics/RTLabs/RTLabs-syntax.ma @ 639

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

Preliminary work on RTLabs semantics
Will move to somewhere more appropriate soon.

File size: 3.3 KB
Line 
1
2include "basics/logic.ma".
3
4include "AST.ma".
5include "CostLabel.ma".
6include "FrontEndOps.ma".
7include "Registers.ma".
8
9include "cerco/Vector.ma".
10include "Graphs.ma".
11
12(* XXX: ASTish stuff *)
13
14definition immediate : Type[0] ≝ int.
15definition registers ≝ Sig nat (Vector register).
16
17(* Addressing modes *)
18
19inductive addressing : Type[0] ≝
20| Aindexed  : immediate → addressing         (* r1 + offset *)
21| Aindexed2 : addressing                     (* r1 + r2 *)
22| Aglobal   : ident → immediate → addressing (* global + offset *)
23| Abased    : ident → immediate → addressing (* global + offset + r1 *)
24| Ainstack  : immediate → addressing         (* stack + offset *)
25.
26
27definition addr_mode_args : addressing → nat ≝
28λa. match a with
29[ Aindexed _  ⇒ 1
30| Aindexed2   ⇒ 2
31| Aglobal _ _ ⇒ 0
32| Abased _ _  ⇒ 1
33| Ainstack _  ⇒ 0
34].
35
36definition addr ≝ λm.Vector registers (addr_mode_args m).
37
38(* Statements, including the label of successor(s). *)
39
40inductive statement : Type[0] ≝
41| St_skip : label → statement
42| St_cost : costlabel → label → statement
43| St_const : registers → constant → label → statement
44| St_op1 : unary_operation → registers → registers → label → statement
45| St_op2 : binary_operation → registers → registers → registers → label → statement
46| St_load : memory_chunk → ∀m:addressing. addr m → registers → label → statement
47| St_store : memory_chunk → ∀m:addressing. addr m → registers → label → statement
48| St_call_id : ident → list registers → registers → signature → label → statement
49| St_call_ptr : registers → list registers → registers → signature → label → statement
50| St_tailcall_id : ident → list registers → signature → statement
51| St_tailcall_ptr : registers → list registers → signature → statement
52(* Um, what? *)
53| St_condcst : constant → label → label → statement
54| St_cond1 : unary_operation → registers → label → label → statement
55| St_cond2 : binary_operation → registers → registers → label → label → statement
56| St_jumptable : registers → list label → statement
57| St_return : registers → statement
58.
59
60record internal_function : Type[0] ≝
61{ f_labgen    : label_generation
62; f_reggen    : register_generation
63; f_sig       : signature
64; f_result    : registers
65; f_params    : list registers
66; f_locals    : list registers
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     registers list based on the addressing mode; similarly, memory_chunk and
87     registers are probably related.
88   - label and register generation really tell us something about the sets of
89     labels and registers 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.