source: Deliverables/D3.3/id-lookup-branch/RTLabs/syntax.ma @ 1153

Last change on this file since 1153 was 1153, checked in by campbell, 8 years ago

Merge trunk into branch.

File size: 2.6 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
12inductive statement : Type[0] ≝
13| St_skip : label → statement
14| St_cost : costlabel → label → statement
15| St_const : register → constant → label → statement
16| St_op1 : unary_operation → register → register → label → statement (* destination source *)
17| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
18| St_load : memory_chunk → register → register → label → statement
19| St_store : memory_chunk → register → register → label → statement
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
24| St_cond : register → label → label → statement
25| St_jumptable : register → list label → statement
26| St_return : statement
27.
28
29definition labels_P : (label → Prop) → statement → Prop ≝
30λP,s. match s with
31[ St_skip l ⇒ P l
32| St_cost _ l ⇒ P l
33| St_const _ _ l ⇒ P l
34| St_op1 _ _ _ l ⇒ P l
35| St_op2 _ _ _ _ l ⇒ P l
36| St_load _ _ _ l ⇒ P l
37| St_store _ _ _ l ⇒ P l
38| St_call_id _ _ _ l ⇒ P l
39| St_call_ptr _ _ _ l ⇒ P l
40| St_tailcall_id _ _ ⇒ True
41| St_tailcall_ptr _ _ ⇒ True
42| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
43| St_jumptable _ ls ⇒ All ? P ls
44| St_return ⇒ True
45].
46
47lemma labels_P_mp : ∀P,Q. (∀l. P l → Q l) → ∀s.labels_P P s → labels_P Q s.
48#P #Q #H * /3/
49#r #l #l' * /3/
50qed.
51
52definition labels_present : graph statement → statement → Prop ≝
53λg,s. labels_P (present ?? g) s.
54
55definition graph_closed : graph statement → Prop ≝
56λg. ∀l,s. lookup ?? g l = Some ? s → labels_present g s.
57
58record internal_function : Type[0] ≝
59{ f_labgen    : universe LabelTag
60; f_reggen    : universe RegisterTag
61; f_result    : option (register × typ)
62; f_params    : list (register × typ)
63; f_locals    : list (register × typ)
64; f_stacksize : nat
65; f_graph     : graph statement
66; f_closed    : graph_closed f_graph
67; f_entry     : Σl:label. present ?? f_graph l
68; f_exit      : Σl:label. present ?? f_graph l
69}.
70
71(* Note that the global variables will be initialised by the code in main
72   by this stage, so the only initialisation data is the amount of space to
73   allocate. *)
74
75definition RTLabs_program ≝ program (fundef internal_function) nat.
76
Note: See TracBrowser for help on using the repository browser.