1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "compiler/preast_tree.ma".
23 include "compiler/ast_tree.ma".
24 include "compiler/sigma.ma".
26 (* ************************* *)
27 (* PASSO 1 : da PREAST a AST *)
28 (* ************************* *)
31 al parser spetta il compito di rigettare le condizioni statiche verificabili
32 - divisione per valore 0
33 al parser spetta il compito di collassare le espressioni statiche
34 - val1+val2 -> val3, ...
35 al parser spetta il compito di collassare gli statement con condizioni statiche
36 - if(true) { b1 } else { b2 } -> b1, ...
37 al parser spetta il compito di individuare divergenza e dead code
38 - while(true) { b1 } -> loop infinito, ...
41 (* operatore di cast *)
42 definition preast_to_ast_expr_check ≝
43 λd.λe:aux_env_type d.λsig:(Σt'.ast_expr d e t').λt:ast_type.
44 match sig with [ sigma_intro t' expr ⇒
45 match eq_ast_type t' t
46 return λx.eq_ast_type t' t = x → option (ast_expr d e t)
48 [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr d e t) expr t (eqasttype_to_eq ?? p))
49 | false ⇒ λp:(eq_ast_type t' t = false).None ?
50 ] (refl_eq ? (eq_ast_type t' t))
53 definition preast_to_ast_init_check ≝
54 λd.λe:aux_env_type d.λsig:Σt'.ast_init d e t'.λt:ast_type.
55 match sig with [ sigma_intro t' expr ⇒
56 match eq_ast_type t' t
57 return λx.eq_ast_type t' t = x → option (ast_init d e t)
59 [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init d e t) expr t (eqasttype_to_eq ?? p))
60 | false ⇒ λp:(eq_ast_type t' t = false).None ?
61 ] (refl_eq ? (eq_ast_type t' t))
64 definition preast_to_ast_var_checkb ≝
65 λd.λe:aux_env_type d.λt:ast_type.λsig:(Σb'.ast_var d e b' t).λb:bool.
66 match sig with [ sigma_intro b' var ⇒
68 return λx.eq_bool b' b = x → option (ast_var d e b t)
70 [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var d e b t) var b (eqbool_to_eq ?? p))
71 | false ⇒ λp:(eq_bool b' b = false).None ?
72 ] (refl_eq ? (eq_bool b' b))
75 definition preast_to_ast_var_checkt ≝
76 λd.λe:aux_env_type d.λb:bool.λsig:(Σt'.ast_var d e b t').λt:ast_type.
77 match sig with [ sigma_intro t' var ⇒
78 match eq_ast_type t' t
79 return λx.eq_ast_type t' t = x → option (ast_var d e b t)
81 [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var d e b t) var t (eqasttype_to_eq ?? p))
82 | false ⇒ λp:(eq_ast_type t' t = false).None ?
83 ] (refl_eq ? (eq_ast_type t' t))
86 definition preast_to_ast_var_check ≝
87 λd.λe:aux_env_type d.λsig:(Σb'.(Σt'.ast_var d e b' t')).λb:bool.λt:ast_type.
88 opt_map ?? (preast_to_ast_var_checkt d e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
89 (λres1.opt_map ?? (preast_to_ast_var_checkb d e t ≪(sigmaFst ?? sig),res1≫ b)
93 PREAST_EXPR_BYTE8 : byte8 → preast_expr
94 PREAST_EXPR_WORD16: word16 → preast_expr
95 PREAST_EXPR_WORD32: word32 → preast_expr
96 PREAST_EXPR_NEG: preast_expr → preast_expr
97 PREAST_EXPR_NOT: preast_expr → preast_expr
98 PREAST_EXPR_COM: preast_expr → preast_expr
99 PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
100 PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
101 PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
102 PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
103 PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
104 PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
105 PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
106 PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
107 PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
108 PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
109 PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
110 PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
111 PREAST_EXPR_B8toW16 : preast_expr → preast_expr
112 PREAST_EXPR_B8toW32 : preast_expr → preast_expr
113 PREAST_EXPR_W16toB8 : preast_expr → preast_expr
114 PREAST_EXPR_W16toW32: preast_expr → preast_expr
115 PREAST_EXPR_W32toB8 : preast_expr → preast_expr
116 PREAST_EXPR_W32toW16: preast_expr → preast_expr
117 PREAST_EXPR_ID: preast_var → preast_expr
119 let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on preast : option (Σt.ast_expr d e t) ≝
121 [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 d e val)≫
122 | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 d e val)≫
123 | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 d e val)≫
125 | PREAST_EXPR_NEG subExpr ⇒
126 opt_map ?? (preast_to_ast_expr subExpr d e)
127 (λsigmaRes:(Σt.ast_expr d e t).
128 match (sigmaFst ?? sigmaRes) with
129 [ AST_TYPE_BASE bType ⇒
130 opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
131 (λres.Some ? ≪?,(AST_EXPR_NEG d e ? res)≫)
133 | PREAST_EXPR_NOT subExpr ⇒
134 opt_map ?? (preast_to_ast_expr subExpr d e)
135 (λsigmaRes:(Σt.ast_expr d e t).
136 match (sigmaFst ?? sigmaRes) with
137 [ AST_TYPE_BASE bType ⇒
138 opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
139 (λres.Some ? ≪?,(AST_EXPR_NOT d e ? res)≫)
141 | PREAST_EXPR_COM subExpr ⇒
142 opt_map ?? (preast_to_ast_expr subExpr d e)
143 (λsigmaRes:(Σt.ast_expr d e t).
144 match (sigmaFst ?? sigmaRes) with
145 [ AST_TYPE_BASE bType ⇒
146 opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
147 (λres.Some ? ≪?,(AST_EXPR_COM d e ? res)≫)
150 | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
151 opt_map ?? (preast_to_ast_expr subExpr1 d e)
152 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
153 (λsigmaRes2:(Σt.ast_expr d e t).
154 match (sigmaFst ?? sigmaRes1) with
155 [ AST_TYPE_BASE bType ⇒
156 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
157 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
158 (λres2.Some ? ≪?,(AST_EXPR_ADD d e ? res1 res2)≫))
160 | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
161 opt_map ?? (preast_to_ast_expr subExpr1 d e)
162 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
163 (λsigmaRes2:(Σt.ast_expr d e t).
164 match (sigmaFst ?? sigmaRes1) with
165 [ AST_TYPE_BASE bType ⇒
166 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
167 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
168 (λres2.Some ? ≪?,(AST_EXPR_SUB d e ? res1 res2)≫))
170 | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
171 opt_map ?? (preast_to_ast_expr subExpr1 d e)
172 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
173 (λsigmaRes2:(Σt.ast_expr d e t).
174 match (sigmaFst ?? sigmaRes1) with
175 [ AST_TYPE_BASE bType ⇒
176 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
177 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
178 (λres2.Some ? ≪?,(AST_EXPR_MUL d e ? res1 res2)≫))
180 | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
181 opt_map ?? (preast_to_ast_expr subExpr1 d e)
182 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
183 (λsigmaRes2:(Σt.ast_expr d e t).
184 match (sigmaFst ?? sigmaRes1) with
185 [ AST_TYPE_BASE bType ⇒
186 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
187 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
188 (λres2.Some ? ≪?,(AST_EXPR_DIV d e ? res1 res2)≫))
191 | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
192 opt_map ?? (preast_to_ast_expr subExpr1 d e)
193 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
194 (λsigmaRes2:(Σt.ast_expr d e t).
195 match (sigmaFst ?? sigmaRes1) with
196 [ AST_TYPE_BASE bType ⇒
197 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
198 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
199 (λres2.Some ? ≪?,(AST_EXPR_SHR d e ? res1 res2)≫))
201 | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
202 opt_map ?? (preast_to_ast_expr subExpr1 d e)
203 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
204 (λsigmaRes2:(Σt.ast_expr d e t).
205 match (sigmaFst ?? sigmaRes1) with
206 [ AST_TYPE_BASE bType ⇒
207 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
208 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
209 (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫))
212 | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
213 opt_map ?? (preast_to_ast_expr subExpr1 d e)
214 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
215 (λsigmaRes2:(Σt.ast_expr d e t).
216 match (sigmaFst ?? sigmaRes1) with
217 [ AST_TYPE_BASE bType ⇒
218 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
219 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
220 (λres2.Some ? ≪?,(AST_EXPR_GT d e ? res1 res2)≫))
222 | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
223 opt_map ?? (preast_to_ast_expr subExpr1 d e)
224 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
225 (λsigmaRes2:(Σt.ast_expr d e t).
226 match (sigmaFst ?? sigmaRes1) with
227 [ AST_TYPE_BASE bType ⇒
228 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
229 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
230 (λres2.Some ? ≪?,(AST_EXPR_GTE d e ? res1 res2)≫))
232 | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
233 opt_map ?? (preast_to_ast_expr subExpr1 d e)
234 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
235 (λsigmaRes2:(Σt.ast_expr d e t).
236 match (sigmaFst ?? sigmaRes1) with
237 [ AST_TYPE_BASE bType ⇒
238 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
239 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
240 (λres2.Some ? ≪?,(AST_EXPR_LT d e ? res1 res2)≫))
242 | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
243 opt_map ?? (preast_to_ast_expr subExpr1 d e)
244 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
245 (λsigmaRes2:(Σt.ast_expr d e t).
246 match (sigmaFst ?? sigmaRes1) with
247 [ AST_TYPE_BASE bType ⇒
248 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
249 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
250 (λres2.Some ? ≪?,(AST_EXPR_LTE d e ? res1 res2)≫))
252 | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
253 opt_map ?? (preast_to_ast_expr subExpr1 d e)
254 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
255 (λsigmaRes2:(Σt.ast_expr d e t).
256 match (sigmaFst ?? sigmaRes1) with
257 [ AST_TYPE_BASE bType ⇒
258 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
259 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
260 (λres2.Some ? ≪?,(AST_EXPR_EQ d e ? res1 res2)≫))
262 | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
263 opt_map ?? (preast_to_ast_expr subExpr1 d e)
264 (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
265 (λsigmaRes2:(Σt.ast_expr d e t).
266 match (sigmaFst ?? sigmaRes1) with
267 [ AST_TYPE_BASE bType ⇒
268 opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
269 (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
270 (λres2.Some ? ≪?,(AST_EXPR_NEQ d e ? res1 res2)≫))
273 | PREAST_EXPR_B8toW16 subExpr ⇒
274 opt_map ?? (preast_to_ast_expr subExpr d e)
275 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
276 (λres.Some ? ≪?,(AST_EXPR_B8toW16 d e res)≫))
277 | PREAST_EXPR_B8toW32 subExpr ⇒
278 opt_map ?? (preast_to_ast_expr subExpr d e)
279 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
280 (λres.Some ? ≪?,(AST_EXPR_B8toW32 d e res)≫))
281 | PREAST_EXPR_W16toB8 subExpr ⇒
282 opt_map ?? (preast_to_ast_expr subExpr d e)
283 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
284 (λres.Some ? ≪?,(AST_EXPR_W16toB8 d e res)≫))
285 | PREAST_EXPR_W16toW32 subExpr ⇒
286 opt_map ?? (preast_to_ast_expr subExpr d e)
287 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
288 (λres.Some ? ≪?,(AST_EXPR_W16toW32 d e res)≫))
289 | PREAST_EXPR_W32toB8 subExpr ⇒
290 opt_map ?? (preast_to_ast_expr subExpr d e)
291 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
292 (λres.Some ? ≪?,(AST_EXPR_W32toB8 d e res)≫))
293 | PREAST_EXPR_W32toW16 subExpr ⇒
294 opt_map ?? (preast_to_ast_expr subExpr d e)
295 (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
296 (λres.Some ? ≪?,(AST_EXPR_W32toW16 d e res)≫))
298 | PREAST_EXPR_ID var ⇒
299 opt_map ?? (preast_to_ast_var var d e)
300 (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
301 match sigmaRes with [ sigma_intro b sigmaRes' ⇒
302 match sigmaRes' with [ sigma_intro t _ ⇒
303 opt_map ?? (preast_to_ast_var_check d e sigmaRes b t)
304 (λres.Some ? ≪?,(AST_EXPR_ID d e ?? res)≫)]])
307 PREAST_VAR_ID: aux_str_type → preast_var
308 PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
309 PREAST_VAR_STRUCT: preast_var → nat → preast_var
311 and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast : option (Σb.(Σt.ast_var d e b t)) ≝
313 [ PREAST_VAR_ID name ⇒
314 match checkb_desc_env d e name
315 return λx.checkb_desc_env d e name = x → option (Σb.(Σt.ast_var d e b t))
317 [ true ⇒ λp:(checkb_desc_env d e name = true).
318 let desc ≝ get_desc_env d e name in
319 let b ≝ get_const_desc desc in
320 let t ≝ get_type_desc desc in
321 Some ? ≪b,≪t,(AST_VAR_ID d e b t (AST_ID d e name (checkbdescenv_to_checkdescenv d e name p)))≫≫
322 | false ⇒ λp:(checkb_desc_env d e name = false).None ?
323 ] (refl_eq ? (checkb_desc_env d e name))
325 | PREAST_VAR_ARRAY subVar expr ⇒
326 opt_map ?? (preast_to_ast_var subVar d e)
327 (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
328 match sigmaResV with [ sigma_intro b sigmaResV' ⇒
329 match sigmaResV' with [ sigma_intro t _ ⇒
331 [ AST_TYPE_ARRAY subType dim ⇒
332 opt_map ?? (preast_to_ast_var_check d e sigmaResV b (AST_TYPE_ARRAY subType dim))
335 1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
336 stato fatto dal parser, e qui controllo la condizione OUT_OF_BOUND
337 2) se l'indice non e' un'espressione riducibile ad un valore il controllo
338 OUT_OF_BOUND sara' fatto a run time
340 match (match expr with
341 [ PREAST_EXPR_BYTE8 val ⇒ (λx.ltb (nat_of_byte8 val) dim)
342 | PREAST_EXPR_WORD16 val ⇒ (λx.ltb (nat_of_word16 val) dim)
343 | PREAST_EXPR_WORD32 val ⇒ (λx.ltb (nat_of_word32 val) dim)
344 | _ ⇒ (λx.true) ]) expr with
346 opt_map ?? (preast_to_ast_expr expr d e)
347 (λsigmaResE:(Σt.ast_expr d e t).
348 match sigmaFst ?? sigmaResE with
349 [ AST_TYPE_BASE bType ⇒
350 opt_map ?? (preast_to_ast_expr_check d e sigmaResE (AST_TYPE_BASE bType))
351 (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY d e b subType dim resVar (AST_BASE_EXPR d e bType resExpr))≫≫)
356 | PREAST_VAR_STRUCT subVar field ⇒
357 opt_map ?? (preast_to_ast_var subVar d e)
358 (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
359 match sigmaRes with [ sigma_intro b sigmaRes' ⇒
360 match sigmaRes' with [ sigma_intro t _ ⇒
362 [ AST_TYPE_STRUCT nelSubType ⇒
363 opt_map ?? (preast_to_ast_var_check d e sigmaRes b (AST_TYPE_STRUCT nelSubType))
365 match ltb field (len_neList ? nelSubType)
366 return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var d e b t))
368 [ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true).
369 Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT d e b nelSubType field resVar p)≫≫
370 | false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ?
371 ] (refl_eq ? (ltb field (len_neList ? nelSubType)))
377 PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
378 PREAST_INIT_VAL_WORD16: word16 → preast_init_val
379 PREAST_INIT_VAL_WORD32: word32 → preast_init_val
380 PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
381 PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val
383 definition preast_to_ast_init_val_aux_array :
384 Πt.Πn.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)) → (aux_ast_init_type (AST_TYPE_ARRAY t (S n))) ≝
385 λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
387 definition preast_to_ast_init_val_aux_struct :
388 Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝
389 λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
391 let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
393 [ PREAST_INIT_VAL_BYTE8 val ⇒
394 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
395 | PREAST_INIT_VAL_WORD16 val ⇒
396 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
397 | PREAST_INIT_VAL_WORD32 val ⇒
398 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
400 | PREAST_INIT_VAL_ARRAY nelSubVal ⇒
401 let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
404 opt_map ?? (preast_to_ast_init_val_aux h)
405 (λsigmaRes.match sigmaRes with [ sigma_intro t res ⇒
406 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
408 opt_map ?? (preast_to_ast_init_val_aux h)
409 (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
410 (λsigmaRes2:(Σt.aux_ast_init_type t).
411 match sigmaRes1 with [ sigma_intro t1 res1 ⇒
412 match sigmaRes2 with [ sigma_intro t2 res2 ⇒
414 [ AST_TYPE_ARRAY bType dim ⇒
415 match eq_ast_type t1 bType
416 return λx.(eq_ast_type t1 bType = x) → option (Σt.aux_ast_init_type t)
418 [ true ⇒ λp:(eq_ast_type t1 bType = true).
419 match eq_ast_type t2 (AST_TYPE_ARRAY bType dim)
420 return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt.aux_ast_init_type t)
422 [ true ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = true).
423 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
424 (preast_to_ast_init_val_aux_array bType dim
425 (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
426 (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
427 (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
428 | false ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = false).None ?
429 ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_ARRAY bType dim)))
430 | false ⇒ λp:(eq_ast_type t1 bType = false).None ?
431 ] (refl_eq ? (eq_ast_type t1 bType))
436 | PREAST_INIT_VAL_STRUCT nelSubVal ⇒
437 let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
440 opt_map ?? (preast_to_ast_init_val_aux h)
441 (λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
442 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ])
444 opt_map ?? (preast_to_ast_init_val_aux h)
445 (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
446 (λsigmaRes2:(Σt.aux_ast_init_type t).
447 match sigmaRes1 with [ sigma_intro t1 res1 ⇒
448 match sigmaRes2 with [ sigma_intro t2 res2 ⇒
450 [ AST_TYPE_STRUCT nelSubType ⇒
451 match eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)
452 return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t)
454 [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
455 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)),
456 (preast_to_ast_init_val_aux_struct ??
457 (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
459 (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
460 | false ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = false).None ?
461 ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)))
467 PREAST_INIT_VAR: preast_var → preast_init
468 PREAST_INIT_VAL: preast_init_val → preast_init
470 definition preast_to_ast_init : preast_init → Πd.Πe:aux_env_type d.option (Σt.ast_init d e t) ≝
471 λpreast:preast_init.λd.λe:aux_env_type d.match preast with
472 [ PREAST_INIT_VAR var ⇒
473 opt_map ?? (preast_to_ast_var var d e)
474 (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
475 Some ? ≪?,(AST_INIT_VAR d e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
477 | PREAST_INIT_VAL val ⇒
478 opt_map ?? (preast_to_ast_init_val_aux val)
479 (λsigmaRes:(Σt.aux_ast_init_type t).
480 Some ? ≪?,(AST_INIT_VAL d e ? (sigmaSnd ?? sigmaRes))≫)
484 PREAST_STM_ASG: preast_var → preast_expr → preast_stm
485 PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
486 PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
488 definition preast_to_ast_base_expr : preast_expr → Πd.Πe:aux_env_type d.option (ast_base_expr d e) ≝
489 λpreast:preast_expr.λd.λe:aux_env_type d.
490 opt_map ?? (preast_to_ast_expr preast d e)
491 (λsigmaRes:(Σt.ast_expr d e t).
492 match sigmaFst ?? sigmaRes with
493 [ AST_TYPE_BASE bType ⇒
494 opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
495 (λres.Some ? (AST_BASE_EXPR d e ? res))
498 let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on preast : option (ast_stm d e) ≝
500 [ PREAST_STM_ASG var expr ⇒
501 opt_map ?? (preast_to_ast_var var d e)
502 (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
503 match sigmaResV with [ sigma_intro _ sigmaResV' ⇒
504 match sigmaResV' with [ sigma_intro t _ ⇒
505 opt_map ?? (preast_to_ast_var_check d e sigmaResV false t)
506 (λresVar.opt_map ?? (preast_to_ast_expr expr d e)
507 (λsigmaResE:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaResE t)
508 (λresExpr.Some ? (AST_STM_ASG d e t resVar resExpr)
511 | PREAST_STM_WHILE expr decl ⇒
512 opt_map ?? (preast_to_ast_base_expr expr d e)
513 (λresExpr.opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
514 (λresDecl.Some ? (AST_STM_WHILE d e resExpr resDecl)))
516 | PREAST_STM_IF nelExprDecl optDecl ⇒
517 opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) d e)
518 (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (S d) (enter_env d e))
519 (λresDecl.opt_map ?? t
520 (λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
521 (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR d e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 d e 〈x0,x0〉)) (AST_NO_DECL (S d) (enter_env d e) (nil ?)))))
523 (λres.match optDecl with
524 [ None ⇒ Some ? (AST_STM_IF d e (cut_last_neList ? res) (None ?))
525 | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
526 (λresDecl.Some ? (AST_STM_IF d e (cut_last_neList ? res) (Some ? resDecl)))
530 PREAST_NO_DECL: list preast_stm → preast_decl
531 PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
533 and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝
535 [ PREAST_NO_DECL lPreastStm ⇒
536 opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h d e)
538 (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
539 (λres.Some ? (AST_NO_DECL d e res))
541 | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
542 match checkb_not_already_def_env d e decName
543 return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
545 [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
546 opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName constFlag decType))
547 (λdecl.match optInitExpr with
548 [ None ⇒ Some ? (AST_DECL d e constFlag decName decType
549 (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl)
551 opt_map ?? (preast_to_ast_init initExpr d e)
552 (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
553 (λresInit.Some ? (AST_DECL d e constFlag decName decType
554 (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))])
555 | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
556 ] (refl_eq ? (checkb_not_already_def_env d e decName))
560 PREAST_ROOT: preast_decl → preast_root
562 definition preast_to_ast ≝
563 λpreast:preast_root.match preast with
564 [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl O empty_env)
565 (λres.Some ? (AST_ROOT res)) ].