source: src/Cminor/syntax.ma @ 1878

Last change on this file since 1878 was 1878, checked in by campbell, 6 years ago

Enforce typing of constants in front-end, plus binops for RTLabs.

File size: 5.8 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "basics/lists/list.ma".
5
6inductive expr : typ → Type[0] ≝
7| Id : ∀t. ident → expr t
8| Cst : ∀t. constant t → expr t
9| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
10| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
11| Mem : ∀t,r. expr (ASTptr r) → expr t
12| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
13| Ecost : ∀t. costlabel → expr t → expr t.
14
15(* Assert a predicate on every variable or parameter identifier. *)
16let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
17match e with
18[ Id t i ⇒ P i t
19| Cst _ _ ⇒ True
20| Op1 _ _ _ e ⇒ expr_vars ? e P
21| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
22| Mem _ _ e ⇒ expr_vars ? e P
23| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
24| Ecost _ _ e ⇒ expr_vars ? e P
25].
26
27lemma expr_vars_mp : ∀t,e,P,Q.
28  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
29#t0 #e elim e normalize /3/
30[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
31  % /3/
32| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
33] qed.
34
35axiom Label : String.
36
37inductive stmt : Type[0] ≝
38| St_skip : stmt
39| St_assign : ∀t. ident → expr t → stmt
40| St_store : ∀t,r. expr (ASTptr r) → expr t → stmt
41(* ident for returned value, expression to identify fn, args. *)
42| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
43(* We don't use these at the moment, and they're getting in the way.
44| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
45*)
46| St_seq : stmt → stmt → stmt
47| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
48| St_loop : stmt → stmt
49| St_block : stmt → stmt
50| St_exit : nat → stmt
51(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
52| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
53| St_return : option (𝚺t. expr t) → stmt
54| St_label : identifier Label → stmt → stmt
55| St_goto : identifier Label → stmt
56| St_cost : costlabel → stmt → stmt.
57
58let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
59match s with
60[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
61| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
62| St_loop s' ⇒ P s ∧ stmt_P P s'
63| St_block s' ⇒ P s ∧ stmt_P P s'
64| St_label _ s' ⇒ P s ∧ stmt_P P s'
65| St_cost _ s' ⇒ P s ∧ stmt_P P s'
66| _ ⇒ P s
67].
68
69lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
70#P * normalize /2/
71[ #s1 #s2 * * /2/
72| #sz #sg #e #s1 #s2 * * /2/
73| 3,4: #s * /2/
74| 5,6: #i #s normalize * /2/
75] qed.
76
77(* Assert a predicate on every variable or parameter identifier. *)
78definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
79λP,s.
80match s with
81[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
82| St_store _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
83| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
84(*
85| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
86*)
87| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
88| St_switch _ _ e _ _ ⇒ expr_vars ? e P
89| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
90| _ ⇒ True
91].
92
93definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
94λP,s.
95match s with
96[ St_label l _ ⇒ P l
97| St_goto l ⇒ P l
98| _ ⇒ True
99].
100
101lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
102#P #Q #H #s elim s /2/
103[ #s1 #s2 #H1 #H2 normalize * * /4/
104| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
105| #s #H * /5/
106| #s #H * /5/
107| #l #s #H * /5/
108| #l #s #H * /5/
109] qed.
110
111lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
112#P #Q #H #s elim s normalize
113[ //
114| #t #id #e * /4/
115| #t #r #e1 #e2 * /4/
116| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
117(*
118| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
119*)
120| #s1 #s2 #H1 #H2 * /3/
121| #sz #sg #e #s1 #s2 #H1 #H2 /5/
122| 7,8: #s #H1 #H2 /2/
123| //
124| /5/
125| * normalize [ // | *; normalize /3/ ]
126| /2/
127| //
128| /2/
129] qed.
130
131lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
132#P #Q #H #s elim s normalize /2/ qed.
133
134(* Get labels from a Cminor statement. *)
135let rec labels_of (s:stmt) : list (identifier Label) ≝
136match s with
137[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
138| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
139| St_loop s ⇒ labels_of s
140| St_block s ⇒ labels_of s
141| St_label l s ⇒ l::(labels_of s)
142| St_cost _ s ⇒ labels_of s
143| _ ⇒ [ ]
144].
145
146record internal_function : Type[0] ≝
147{ f_return    : option typ
148; f_params    : list (ident × typ)
149; f_vars      : list (ident × typ)
150; f_distinct  : distinct_env … (f_params @ f_vars)
151; f_stacksize : nat
152; f_body      : stmt
153     (* Ensure that variables appear in the params and vars list with the
154        correct typ; and that all goto labels used are declared. *)
155; f_inv       : stmt_P (λs.stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) (f_params @ f_vars)) s ∧
156                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
157}.
158
159(* We define two closely related versions of Cminor, the first with the original
160   initialisation data for global variables, and the second where the code is
161   responsible for initialisation and we only give the size of each variable. *)
162
163definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
164
165definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.