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_tree.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 d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str)))
33 lemma ast_to_astfe_id :
34 ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t.
35 ∀m:aux_map_type d.∀fe.
36 ∀dimInv:env_to_flatEnv_inv d e m fe.
41 lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
42 [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)))
43 | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H));
48 lemma ast_to_astfe_retype_id :
49 ∀fe,b,t.∀ast:astfe_id fe b t.
50 ∀d.∀e:aux_env_type d.∀m:aux_map_type d.∀fe'.
51 ∀dimInv:env_to_flatEnv_inv d e m fe'.
52 ∀dimLe:le_flatEnv fe fe' = true.
57 lapply (ASTFE_ID fe' a1 ?);
58 [ apply (leflatenv_to_check fe fe' a1 H2 H)
59 | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
65 AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
66 | AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
67 | AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
69 | AST_EXPR_NEG: ∀t:ast_base_type.
70 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
71 | AST_EXPR_NOT: ∀t:ast_base_type.
72 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
73 | AST_EXPR_COM: ∀t:ast_base_type.
74 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
76 | AST_EXPR_ADD: ∀t:ast_base_type.
77 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
78 | AST_EXPR_SUB: ∀t:ast_base_type.
79 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
80 | AST_EXPR_MUL: ∀t:ast_base_type.
81 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
82 | AST_EXPR_DIV: ∀t:ast_base_type.
83 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
84 | AST_EXPR_SHR: ∀t:ast_base_type.
85 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
86 | AST_EXPR_SHL: ∀t:ast_base_type.
87 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
88 | AST_EXPR_AND: ∀t:ast_base_type.
89 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
90 | AST_EXPR_OR: ∀t:ast_base_type.
91 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
92 | AST_EXPR_XOR: ∀t:ast_base_type.
93 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
95 | AST_EXPR_GT : ∀t:ast_base_type.
96 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
97 | AST_EXPR_GTE: ∀t:ast_base_type.
98 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
99 | AST_EXPR_LT : ∀t:ast_base_type.
100 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
101 | AST_EXPR_LTE: ∀t:ast_base_type.
102 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
103 | AST_EXPR_EQ : ∀t:ast_base_type.
104 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
105 | AST_EXPR_NEQ: ∀t:ast_base_type.
106 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
108 | AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
109 | AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
110 | AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
111 | AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
112 | AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
113 | AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
115 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
116 ast_var d e b t → ast_expr d e t
118 let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
119 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
121 return λW.λa:ast_expr d e W.astfe_expr fe W
123 [ AST_EXPR_BYTE8 val ⇒
124 ASTFE_EXPR_BYTE8 fe val
125 | AST_EXPR_WORD16 val ⇒
126 ASTFE_EXPR_WORD16 fe val
127 | AST_EXPR_WORD32 val ⇒
128 ASTFE_EXPR_WORD32 fe val
130 | AST_EXPR_NEG bType sExpr ⇒
131 ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
132 | AST_EXPR_NOT bType sExpr ⇒
133 ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
134 | AST_EXPR_COM bType sExpr ⇒
135 ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
137 | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
138 ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
139 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
140 | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
141 ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
142 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
143 | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
144 ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
145 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
146 | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
147 ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
148 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
149 | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
150 ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
151 (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
152 | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
153 ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
154 (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
155 | AST_EXPR_AND bType sExpr1 sExpr2 ⇒
156 ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
157 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
158 | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
159 ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
160 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
161 | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
162 ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
163 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
165 | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
166 ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
167 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
168 | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
169 ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
170 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
171 | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
172 ASTFE_EXPR_LT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
173 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
174 | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
175 ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
176 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
177 | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
178 ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
179 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
180 | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
181 ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
182 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
184 | AST_EXPR_B8toW16 sExpr ⇒
185 ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
186 | AST_EXPR_B8toW32 sExpr ⇒
187 ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
188 | AST_EXPR_W16toB8 sExpr ⇒
189 ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
190 | AST_EXPR_W16toW32 sExpr ⇒
191 ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
192 | AST_EXPR_W32toB8 sExpr ⇒
193 ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
194 | AST_EXPR_W32toW16 sExpr ⇒
195 ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
197 | AST_EXPR_ID b sType var ⇒
198 ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
202 AST_VAR_ID: ∀b:bool.∀t:ast_type.
203 ast_id d e b t → ast_var d e b t
204 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
205 ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
206 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
207 ast_var d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n)
209 and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
210 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
212 return λW,X.λa:ast_var d e W X.astfe_var fe W X
214 [ AST_VAR_ID sB sType sId ⇒
215 ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
217 | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
218 ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
219 (ast_to_astfe_base_expr d e sExpr m fe dimInv)
221 | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
222 ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)
225 AST_BASE_EXPR: ∀t:ast_base_type.
226 ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e
229 and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
230 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
232 return λa:ast_base_expr d e.astfe_base_expr fe
234 [ AST_BASE_EXPR bType sExpr ⇒
235 ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
238 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
239 d (e:aux_env_type d) (m:aux_map_type d) fe'
240 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) 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)
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)
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)
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)
260 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
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)
263 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
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)
266 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
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)
269 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
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)
272 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
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)
275 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
276 | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒
277 ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
278 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
279 | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒
280 ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
281 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
282 | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
283 ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
284 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
286 | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
287 ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
288 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
289 | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
290 ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
291 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
292 | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
293 ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
294 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
295 | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
296 ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
297 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
298 | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
299 ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
300 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
301 | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
302 ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
303 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
305 | ASTFE_EXPR_B8toW16 sExpr ⇒
306 ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
307 | ASTFE_EXPR_B8toW32 sExpr ⇒
308 ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
309 | ASTFE_EXPR_W16toB8 sExpr ⇒
310 ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
311 | ASTFE_EXPR_W16toW32 sExpr ⇒
312 ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
313 | ASTFE_EXPR_W32toB8 sExpr ⇒
314 ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
315 | ASTFE_EXPR_W32toW16 sExpr ⇒
316 ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
318 | ASTFE_EXPR_ID b sType var ⇒
319 ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
322 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
323 d (e:aux_env_type d) (m:aux_map_type d) fe'
324 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
326 return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
328 [ ASTFE_VAR_ID sB sType sId ⇒
329 ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
331 | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
332 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)
333 (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
335 | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
336 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)
338 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
339 d (e:aux_env_type d) (m:aux_map_type d) fe'
340 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
342 return λa:astfe_base_expr fe.astfe_base_expr fe'
344 [ ASTFE_BASE_EXPR bType sExpr ⇒
345 ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
349 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
350 ast_var d e b t → ast_init d e t
351 | AST_INIT_VAL: ∀t:ast_type.
352 aux_ast_init_type t → ast_init d e t
354 definition ast_to_astfe_init ≝
355 λd.λe:aux_env_type d.λt.λast:ast_init d e t.
356 λm:aux_map_type d.λfe.
357 λdimInv:env_to_flatEnv_inv d e m fe.
359 return λW.λa:ast_init d e W.astfe_init fe W
361 [ AST_INIT_VAR sB sType sVar ⇒
362 ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
364 | AST_INIT_VAL sType sArgs ⇒
365 ASTFE_INIT_VAL fe sType sArgs
369 definition ast_to_astfe_retype_init ≝
370 λfe,t.λast:astfe_init fe t.
371 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
372 λdimInv:env_to_flatEnv_inv d e m fe'.
373 λdimLe:le_flatEnv fe fe' = true.
375 return λW.λa:astfe_init fe W.astfe_init fe' W
377 [ ASTFE_INIT_VAR sB sType sVar ⇒
378 ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
380 | ASTFE_INIT_VAL sType sArgs ⇒
381 ASTFE_INIT_VAL fe' sType sArgs
386 ASTFE_STM_ASG: ∀t:ast_type.
387 astfe_var e false t → astfe_expr e t → astfe_stm e
388 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
389 astfe_id e b t → astfe_init e t → astfe_stm e
390 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
391 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
393 let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe)
394 d (e:aux_env_type d) (m:aux_map_type d) fe'
395 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝
397 [ ASTFE_STM_ASG sType sVar sExpr ⇒
398 ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
399 (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
401 | ASTFE_STM_INIT sB sType sId sInit ⇒
402 ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
403 (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
405 | ASTFE_STM_WHILE sExpr sBody ⇒
406 ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
407 (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
409 | ASTFE_STM_IF sNelExprBody sOptBody ⇒
410 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)
411 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
413 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
416 (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
419 ASTFE_BODY: list (astfe_stm e) → astfe_body e
421 and ast_to_astfe_retype_body fe (ast:astfe_body fe)
422 d (e:aux_env_type d) (m:aux_map_type d) fe'
423 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_body fe' ≝
426 ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
429 definition ast_to_astfe_retype_stm_list ≝
430 λfe.λast:list (astfe_stm fe).
431 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
432 λdimInv:env_to_flatEnv_inv d e m fe'.
433 λdimLe:le_flatEnv fe fe' = true.
434 fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
436 definition ast_to_astfe_retype_exprBody_neList ≝
437 λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).
438 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
439 λdimInv:env_to_flatEnv_inv d e m fe'.
440 λdimLe:le_flatEnv fe fe' = true.
441 cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
442 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
444 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
447 (* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
448 inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
449 AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
450 env_to_flatEnv_inv d e m fe' →
451 le_flatEnv fe fe' = true →
453 ast_to_astfe_stm_record d e fe.
455 inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
456 AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
457 env_to_flatEnv_inv d e m fe' →
458 le_flatEnv fe fe' = true →
459 ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
460 ast_to_astfe_if_record d e fe.
462 inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
463 AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
464 env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
465 le_flatEnv fe fe' = true →
466 list (astfe_stm fe') →
467 ast_to_astfe_decl_record d e fe.
469 inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
470 AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
471 env_to_flatEnv_inv d e m fe' →
472 le_flatEnv fe fe' = true →
473 list (astfe_stm fe') →
474 ast_to_astfe_decl_aux_record d e fe.
477 AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
478 ast_var d e false t → ast_expr d e t → ast_stm d e
479 | AST_STM_WHILE: ∀d.∀e:aux_env_type d.
480 ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
481 | AST_STM_IF: ∀d.∀e:aux_env_type d.
482 ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
484 let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe.
485 env_to_flatEnv_inv d e m fe →
486 ast_to_astfe_stm_record d e fe ≝
488 return λD.λE.λast:ast_stm D E.
489 Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
491 [ AST_STM_ASG sD sE sType sVar sExpr ⇒
492 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
493 AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
494 (eq_to_leflatenv ?? (refl_eq ??))
495 (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv)
496 (ast_to_astfe_expr sD sE sType sExpr m fe dimInv))
497 | AST_STM_WHILE sD sE sExpr sDecl ⇒
498 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
499 match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
500 (env_map_flatEnv_enter_aux sD sE m fe dimInv) with
501 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
502 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
503 (λenv.ast_to_astfe_stm_record sD env fe)
504 (AST_TO_ASTFE_STM_RECORD sD
505 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
507 (leave_map sD resMap)
509 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
511 (ASTFE_STM_WHILE resFe
512 (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv)
514 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
515 (leave_map sD resMap)
517 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
519 (ASTFE_BODY resFe resLStm)))
520 sE (leave_add_enter_env sD sE resTrsf) ]
522 | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
523 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
524 let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
525 (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
526 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝
529 match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
530 (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
531 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
532 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
533 (λenv.ast_to_astfe_if_record sD env pFe)
534 (AST_TO_ASTFE_IF_RECORD sD
535 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
537 (leave_map sD resMap)
539 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
541 «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
543 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
544 (leave_map sD resMap)
546 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
548 (ASTFE_BODY resFe resLStm))»)
549 sE (leave_add_enter_env sD sE resTrsf) ]
552 match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
553 (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
554 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
555 match aux t (leave_map sD resMap) resFe
556 (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
557 (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
558 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
559 sE (leave_add_enter_env sD sE resTrsf)) with
560 [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
561 AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
562 (leflatenv_trans ??? resDimLe resDimLe')
563 («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
564 sD sE resMap' resFe' resDimInv'
565 (leflatenv_trans ??? resDimLe resDimLe'))
566 (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
567 sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
570 match aux sExprDecl m fe dimInv with
571 [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
574 AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
577 match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe
578 (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with
579 [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
580 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
581 (λenv.ast_to_astfe_stm_record sD env fe)
582 (AST_TO_ASTFE_STM_RECORD sD
583 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
585 (leave_map sD resMap')
587 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
588 (leflatenv_trans ??? resDimLe resDimLe')
590 (ast_to_astfe_retype_exprBody_neList resFe resExprBody
592 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
593 (leave_map sD resMap')
595 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
597 (Some ? (ASTFE_BODY resFe' resLStm))))
598 sE (leave_add_enter_env sD sE resTrsf) ]]]
602 AST_NO_DECL: ∀d.∀e:aux_env_type d.
603 list (ast_stm d e) → ast_decl d e
604 | AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
605 (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
606 | AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
607 (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e
609 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
610 env_to_flatEnv_inv d e m fe →
611 ast_to_astfe_decl_record d e fe ≝
613 return λD.λE.λast:ast_decl D E.
614 Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
616 [ AST_NO_DECL sD sE sLStm ⇒
617 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
618 let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
619 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
622 AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) []
625 match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
626 [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
627 match aux t resMap resFe resDimInv with
628 [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
629 AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
630 (leflatenv_trans ??? resDimLe resDimLe')
631 ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
634 match aux sLStm m fe dimInv with
635 [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
636 AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
637 (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
640 | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
641 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
642 match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
643 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
644 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
645 (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
646 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
647 AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
648 ([ tripleT ??? sName true sType ]@resTrsf)
649 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
650 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
651 ([ ASTFE_STM_INIT resFe true sType
652 (* l'id e' sull'ambiente arricchito *)
653 (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
655 (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
657 (newid_from_init sD sE sName true sType)
658 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
659 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
660 (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
661 sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
663 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
665 (* l'init e' sull'ambiente non arricchito *)
666 (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
667 sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
669 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
670 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
673 | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒
674 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
675 match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl
676 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
677 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
678 (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with
679 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
680 AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
681 ([ tripleT ??? sName false sType ]@resTrsf)
682 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
683 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)
687 [ ASTFE_STM_INIT resFe false sType
688 (* l'id e' sull'ambiente arricchito *)
689 (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
691 (ast_to_astfe_id sD (add_desc_env sD sE sName false sType)
693 (newid_from_init sD sE sName false sType)
694 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
695 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
696 (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv))
697 sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
699 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
701 (* l'init e' sull'ambiente non arricchito *)
702 (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
703 sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
705 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
706 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe))
712 AST_ROOT: ast_decl O empty_env → ast_root
714 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
715 λast:ast_root.match ast with
716 [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
717 [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].