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/astfe_tree1.ma".
23 include "compiler/sigma.ma".
25 (* ************************ *)
26 (* PASSO 2 : da AST a ASTFE *)
27 (* ************************ *)
30 AST_ID: ∀str:aux_str_type.
31 (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
33 lemma ast_to_astfe_id :
34 ∀e,b,t.∀ast:ast_id e b t.
35 ∀d.∀m:aux_map_type d.∀fe,fe'.
36 ∀dimInv:env_to_flatEnv_inv d e m fe'.
37 ∀dimLe:le_flatEnv fe fe' = true.
38 ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
41 unfold env_to_flatEnv_inv;
44 lapply (ASTFE_ID fe' (STR_ID a1 (get_id_map d m a1)) ?);
45 [ apply (proj2 ?? (proj1 ?? (dimInv a1 H)))
46 | rewrite > (proj2 ?? (dimInv a1 H));
51 lemma ast_to_astfe_retype_id :
52 ∀fe,b,t.∀ast:astfe_id fe b t.
53 ∀d.∀e.∀m:aux_map_type d.∀fe'.
54 ∀dimInv:env_to_flatEnv_inv d e m fe'.
55 ∀dimLe:le_flatEnv fe fe' = true.
56 ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
59 unfold env_to_flatEnv_inv;
62 lapply (ASTFE_ID fe' a1 ?);
63 [ apply (leflatenv_to_check fe fe' a1 dimLe H)
64 | rewrite > (leflatenv_to_get fe fe' a1 dimLe H);
70 AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
71 AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
72 AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
74 AST_EXPR_NEG: ∀t:ast_base_type.
75 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
76 AST_EXPR_NOT: ∀t:ast_base_type.
77 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
78 AST_EXPR_COM: ∀t:ast_base_type.
79 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
81 AST_EXPR_ADD: ∀t:ast_base_type.
82 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
83 AST_EXPR_SUB: ∀t:ast_base_type.
84 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
85 AST_EXPR_MUL: ∀t:ast_base_type.
86 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
87 AST_EXPR_DIV: ∀t:ast_base_type.
88 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
89 AST_EXPR_SHR: ∀t:ast_base_type.
90 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
91 AST_EXPR_SHL: ∀t:ast_base_type.
92 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
94 AST_EXPR_GT : ∀t:ast_base_type.
95 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
96 AST_EXPR_GTE: ∀t:ast_base_type.
97 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
98 AST_EXPR_LT : ∀t:ast_base_type.
99 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
100 AST_EXPR_LTE: ∀t:ast_base_type.
101 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
102 AST_EXPR_EQ : ∀t:ast_base_type.
103 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
104 AST_EXPR_NEQ: ∀t:ast_base_type.
105 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
107 AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
108 AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
109 AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
110 AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
111 AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
112 AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
114 AST_EXPR_ID: ∀b:bool.∀t:ast_type.
115 ast_var e b t → ast_expr e t
117 let rec ast_to_astfe_expr e t (ast:ast_expr e t)
118 d (m:aux_map_type d) fe fe'
119 (dimInv:env_to_flatEnv_inv d e m fe')
120 (dimLe:le_flatEnv fe fe' = true)
121 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
123 return λW.λa:ast_expr e W.astfe_expr fe' W
125 [ AST_EXPR_BYTE8 val ⇒
126 ASTFE_EXPR_BYTE8 fe' val
127 | AST_EXPR_WORD16 val ⇒
128 ASTFE_EXPR_WORD16 fe' val
129 | AST_EXPR_WORD32 val ⇒
130 ASTFE_EXPR_WORD32 fe' val
132 | AST_EXPR_NEG bType sExpr ⇒
133 ASTFE_EXPR_NEG fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
134 | AST_EXPR_NOT bType sExpr ⇒
135 ASTFE_EXPR_NOT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
136 | AST_EXPR_COM bType sExpr ⇒
137 ASTFE_EXPR_COM fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
139 | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
140 ASTFE_EXPR_ADD fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
141 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
142 | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
143 ASTFE_EXPR_SUB fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
144 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
145 | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
146 ASTFE_EXPR_MUL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
147 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
148 | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
149 ASTFE_EXPR_DIV fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
150 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
151 | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
152 ASTFE_EXPR_SHR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
153 (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
154 | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
155 ASTFE_EXPR_SHL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
156 (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
158 | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
159 ASTFE_EXPR_GT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
160 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
161 | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
162 ASTFE_EXPR_GTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
163 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
164 | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
165 ASTFE_EXPR_LT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
166 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
167 | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
168 ASTFE_EXPR_LTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
169 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
170 | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
171 ASTFE_EXPR_EQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
172 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
173 | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
174 ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
175 (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
177 | AST_EXPR_B8toW16 sExpr ⇒
178 ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
179 | AST_EXPR_B8toW32 sExpr ⇒
180 ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
181 | AST_EXPR_W16toB8 sExpr ⇒
182 ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
183 | AST_EXPR_W16toW32 sExpr ⇒
184 ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
185 | AST_EXPR_W32toB8 sExpr ⇒
186 ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
187 | AST_EXPR_W32toW16 sExpr ⇒
188 ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
190 | AST_EXPR_ID b sType var ⇒
191 ASTFE_EXPR_ID fe' b sType (ast_to_astfe_var e b sType var d m fe fe' dimInv dimLe emfe)
195 AST_VAR_ID: ∀b:bool.∀t:ast_type.
196 ast_id e b t → ast_var e b t
197 AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
198 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
199 AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
200 ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
202 and ast_to_astfe_var e b t (ast:ast_var e b t)
203 d (m:aux_map_type d) fe fe'
204 (dimInv:env_to_flatEnv_inv d e m fe')
205 (dimLe:le_flatEnv fe fe' = true)
206 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
208 return λW,X.λa:ast_var e W X.astfe_var fe' W X
210 [ AST_VAR_ID sB sType sId ⇒
211 ASTFE_VAR_ID fe' sB sType (ast_to_astfe_id e sB sType sId d m fe fe' dimInv dimLe emfe)
213 | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
214 ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe fe' dimInv dimLe emfe)
215 (ast_to_astfe_base_expr e sExpr d m fe fe' dimInv dimLe emfe)
217 | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
218 ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe fe' dimInv dimLe emfe)
221 AST_BASE_EXPR: ∀t:ast_base_type.
222 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
224 and ast_to_astfe_base_expr e (ast:ast_base_expr e)
225 d (m:aux_map_type d) fe fe'
226 (dimInv:env_to_flatEnv_inv d e m fe')
227 (dimLe:le_flatEnv fe fe' = true)
228 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝
230 return λa:ast_base_expr e.astfe_base_expr fe'
232 [ AST_BASE_EXPR bType sExpr ⇒
233 ASTFE_BASE_EXPR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
236 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
237 d e (m:aux_map_type d) fe'
238 (dimInv:env_to_flatEnv_inv d e m fe')
239 (dimLe:le_flatEnv fe fe' = true)
240 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
242 return λW.λa:astfe_expr fe W.astfe_expr fe' W
244 [ ASTFE_EXPR_BYTE8 val ⇒
245 ASTFE_EXPR_BYTE8 fe' val
246 | ASTFE_EXPR_WORD16 val ⇒
247 ASTFE_EXPR_WORD16 fe' val
248 | ASTFE_EXPR_WORD32 val ⇒
249 ASTFE_EXPR_WORD32 fe' val
251 | ASTFE_EXPR_NEG bType sExpr ⇒
252 ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
253 | ASTFE_EXPR_NOT bType sExpr ⇒
254 ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
255 | ASTFE_EXPR_COM bType sExpr ⇒
256 ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
258 | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
259 ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
260 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
261 | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
262 ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
263 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
264 | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
265 ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
266 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
267 | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
268 ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
269 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
270 | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
271 ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
272 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
273 | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
274 ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
275 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
277 | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
278 ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
279 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
280 | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
281 ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
282 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
283 | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
284 ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
285 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
286 | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
287 ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
288 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
289 | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
290 ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
291 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
292 | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
293 ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
294 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
296 | ASTFE_EXPR_B8toW16 sExpr ⇒
297 ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe emfe)
298 | ASTFE_EXPR_B8toW32 sExpr ⇒
299 ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe emfe)
300 | ASTFE_EXPR_W16toB8 sExpr ⇒
301 ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe emfe)
302 | ASTFE_EXPR_W16toW32 sExpr ⇒
303 ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe emfe)
304 | ASTFE_EXPR_W32toB8 sExpr ⇒
305 ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe emfe)
306 | ASTFE_EXPR_W32toW16 sExpr ⇒
307 ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe emfe)
309 | ASTFE_EXPR_ID b sType var ⇒
310 ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe emfe)
313 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
314 d e (m:aux_map_type d) fe'
315 (dimInv:env_to_flatEnv_inv d e m fe')
316 (dimLe:le_flatEnv fe fe' = true)
317 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
319 return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
321 [ ASTFE_VAR_ID sB sType sId ⇒
322 ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe)
324 | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
325 ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe emfe)
326 (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
328 | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
329 ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe emfe)
331 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
332 d e (m:aux_map_type d) fe'
333 (dimInv:env_to_flatEnv_inv d e m fe')
334 (dimLe:le_flatEnv fe fe' = true)
335 (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝
337 return λa:astfe_base_expr fe.astfe_base_expr fe'
339 [ ASTFE_BASE_EXPR bType sExpr ⇒
340 ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
344 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
345 ast_var e b t → ast_init e t
346 AST_INIT_VAL: ∀t:ast_type.
347 aux_ast_init_type t → ast_init e t
349 definition ast_to_astfe_init ≝
350 λe,t.λast:ast_init e t.
351 λd.λm:aux_map_type d.λfe,fe'.
352 λdimInv:env_to_flatEnv_inv d e m fe'.
353 λdimLe:le_flatEnv fe fe' = true.
354 λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
356 return λW.λa:ast_init e W.astfe_init fe' W
358 [ AST_INIT_VAR sB sType sVar ⇒
359 ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_var e sB sType sVar d m fe fe' dimInv dimLe emfe)
361 | AST_INIT_VAL sType sArgs ⇒
362 ASTFE_INIT_VAL fe' sType sArgs
366 definition ast_to_astfe_retype_init ≝
367 λfe,t.λast:astfe_init fe t.
368 λd.λe.λm:aux_map_type d.λfe'.
369 λdimInv:env_to_flatEnv_inv d e m fe'.
370 λdimLe:le_flatEnv fe fe' = true.
371 λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
373 return λW.λa:astfe_init fe W.astfe_init fe' W
375 [ ASTFE_INIT_VAR sB sType sVar ⇒
376 ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe emfe)
378 | ASTFE_INIT_VAL sType sArgs ⇒
379 ASTFE_INIT_VAL fe' sType sArgs
384 AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
385 ast_var e false t → ast_expr e t → ast_stm e
386 AST_STM_WHILE: ∀e:aux_env_type.
387 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
388 AST_STM_IF: ∀e:aux_env_type.
389 ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
391 (*lemma ast_to_astfe_stm_aux :
392 ∀d,e.∀m:aux_map_type d.∀fe,fe',dimInv,dimLe.
393 ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
395 (ΣD.(ΣE.(ΣM.(ΣFE.(ΣFE'.(ΣDIMINV.(ΣDIMLE.Prod (env_map_flatEnv D E M FE FE' DIMINV DIMLE) (astfe_stm FE')))))))).
398 inductive ast_to_astfe_stm_res (d:nat) : Type ≝
399 AST_TO_ASTFE_STM_RES:
400 ∀e.∀m:aux_map_type d.∀fe,fe'.
401 ∀dimInv:env_to_flatEnv_inv d e m fe'.
402 ∀dimLe:le_flatEnv fe fe' = true.
403 ∀trsf:Prod3T aux_str_type bool ast_type.
404 env_map_flatEnv d e m fe fe' dimInv dimLe → astfe_stm fe' → ast_to_astfe_stm_res d.
406 let rec ast_to_astfe_stm e (ast:ast_stm e) on ast ≝
408 return λX.λast:ast_stm X.
409 Πd.Πm:aux_map_type d.Πfe.Πfe'.ΠdimInv:env_to_flatEnv_inv d X m fe'.
410 ΠdimLe:le_flatEnv fe fe' = true.env_map_flatEnv d X m fe fe' dimInv dimLe →
411 ast_to_astfe_stm_res d
413 [ AST_STM_ASG sE sType sVar sExpr ⇒
414 λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.
415 λdimLe:le_flatEnv fe fe' = true.λemfe:env_map_flatEnv d sE m fe fe' dimInv dimLe.
416 AST_TO_ASTFE_STM_RES d sE m fe fe' dimInv dimLe emfe []
417 (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe fe' dimInv dimLe emfe)
418 (ast_to_astfe_expr sE sType sExpr d m fe fe' dimInv dimLe emfe))
420 | _ ⇒ False_rect ? daemon
426 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
427 : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
429 return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
431 [ AST_STM_ASG e' subType var expr ⇒
432 λmap:aux_trasfMap_type e' fe.
433 opt_map ?? (ast_to_astfe_var e' false subType var fe map)
434 (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
435 (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
437 | AST_STM_WHILE e' expr decl ⇒
438 λmap:aux_trasfMap_type e' fe.
439 opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
440 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
441 (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
442 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
443 [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
444 [ pair map' resDecl ⇒
445 match le_flatEnv fe fe'
446 return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
448 [ true ⇒ λp:(le_flatEnv fe fe' = true).
449 opt_map ?? (retype_base_expr fe resExpr fe' p)
450 (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
451 (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
452 | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
453 ] (refl_eq ? (le_flatEnv fe fe'))
456 | AST_STM_IF e' nelExprDecl optDecl ⇒
457 λmap:aux_trasfMap_type e' fe.
458 let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
459 (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
462 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
463 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
464 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
465 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
466 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
468 match le_flatEnv fenv fenv'
469 return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
471 [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
472 opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
473 (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
474 «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
475 | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
476 ] (refl_eq ? (le_flatEnv fenv fenv'))
480 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
481 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
482 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
483 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
484 [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
486 opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
487 (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
488 [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
490 match le_flatEnv fenv fenv''
491 return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
493 [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
494 match le_flatEnv fenv' fenv''
495 return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
497 [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
498 opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
499 (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
501 Some ? (≪fenv'',pair ?? m''
503 (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
504 | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
505 ] (refl_eq ? (le_flatEnv fenv' fenv''))
506 | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
507 ] (refl_eq ? (le_flatEnv fenv fenv''))
510 opt_map ?? (aux fe map nelExprDecl)
511 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
512 [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
513 [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
514 [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
516 opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
517 (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
518 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
519 [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
520 [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
521 match le_flatEnv fe' fe''
522 return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
524 [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
525 opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
526 (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
527 (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
528 (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
529 | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
530 ] (refl_eq ? (le_flatEnv fe' fe''))
534 AST_NO_DECL: ∀e:aux_env_type.
535 list (ast_stm e) → ast_decl e
536 AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
537 (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
539 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
540 : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝
542 return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
544 [ AST_NO_DECL e' lStm ⇒
545 λmap:aux_trasfMap_type e' fe.
546 let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
547 : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
549 [ nil ⇒ let trsf ≝ []
550 in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
551 (list (astfe_stm fenv))
552 (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
555 opt_map ?? (ast_to_astfe_stm e' h fenv m)
556 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
557 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
559 opt_map ?? (aux tl fenv' m')
560 (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
561 [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
562 [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
564 match le_flatEnv fenv' fenv''
565 return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
567 [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
568 opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
569 (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
570 (list (astfe_stm fenv''))
573 | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
574 ] (refl_eq ? (le_flatEnv fenv' fenv''))
578 | AST_DECL e' b name t dim optInit subDecl ⇒
579 λmap:aux_trasfMap_type e' fe.
580 opt_map ?? (match optInit with
583 opt_map ?? (ast_to_astfe_init e' t init fe map)
584 (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
585 (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
586 (next_nameId e' fe map name)
587 (ast_to_astfe_dec_aux e' name b t fe map dim))
589 (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
590 (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
591 (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
593 (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
594 (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
595 (add_maxcur_map e' fe map map name b t))
596 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
597 [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
598 [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
599 [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
600 match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
601 return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe'))))
603 [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
604 opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
605 (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
606 in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
607 (list (astfe_stm fe'))
610 | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
611 ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
616 AST_ROOT: ast_decl empty_env → ast_root.
618 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
619 λast:ast_root.match ast with
620 [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
621 (* impossibile: dummy *)
622 [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
623 | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
624 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
625 [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
626 [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
630 include "compiler/preast_tree.ma".
631 include "compiler/preast_to_ast.ma".
634 const byte8[3] b={0,1,2};
652 PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
653 PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) (
654 PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
658 (PREAST_EXPR_BYTE8 〈xF,x0〉)
659 (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
662 (PREAST_EXPR_BYTE8 〈xF,x1〉)
664 (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
665 PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
670 (PREAST_EXPR_BYTE8 〈xF,x2〉)
671 (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
673 » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
693 ASTFE_STM_ASG: ∀t:ast_type.
694 astfe_var e false t → astfe_expr e t → astfe_stm e
695 ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
696 astfe_id e b t → astfe_init e t → astfe_stm e
697 ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
698 ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
700 let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_stm fe' ≝
702 [ ASTFE_STM_ASG sType sVar sExpr ⇒
703 ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe emfe)
704 (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe emfe)
706 | ASTFE_STM_INIT sB sType sId sInit ⇒
707 ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe)
708 (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe emfe)
710 | ASTFE_STM_WHILE sExpr sBody ⇒
711 ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
712 (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe)
714 | ASTFE_STM_IF sNelExprBody sOptBody ⇒
715 ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe emfe)
716 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
718 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
721 (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe)))
724 ASTFE_BODY: list (astfe_stm e) → astfe_body e
726 and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_body fe' ≝
729 ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe ]@t) [] sLStm)
732 definition ast_to_astfe_retype_stm_list ≝
733 λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
734 fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe]@t) [] ast.
736 definition ast_to_astfe_retype_exprBody_neList ≝
737 λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
738 cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe emfe)
739 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
741 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»