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.
39 unfold env_to_flatEnv_inv;
42 lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
43 [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
44 | rewrite > (proj2 ?? (H1 a1 H));
49 lemma ast_to_astfe_retype_id :
50 ∀fe,b,t.∀ast:astfe_id fe b t.
51 ∀d.∀e:aux_env_type d.∀m:aux_map_type d.∀fe'.
52 ∀dimInv:env_to_flatEnv_inv d e m fe'.
53 ∀dimLe:le_flatEnv fe fe' = true.
56 unfold env_to_flatEnv_inv;
59 lapply (ASTFE_ID fe' a1 ?);
60 [ apply (leflatenv_to_check fe fe' a1 H2 H)
61 | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
67 AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
68 | AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
69 | AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
71 | AST_EXPR_NEG: ∀t:ast_base_type.
72 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
73 | AST_EXPR_NOT: ∀t:ast_base_type.
74 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
75 | AST_EXPR_COM: ∀t:ast_base_type.
76 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
78 | AST_EXPR_ADD: ∀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_SUB: ∀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_MUL: ∀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_DIV: ∀t:ast_base_type.
85 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
86 | AST_EXPR_SHR: ∀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_SHL: ∀t:ast_base_type.
89 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)
91 | AST_EXPR_GT : ∀t:ast_base_type.
92 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)
93 | AST_EXPR_GTE: ∀t:ast_base_type.
94 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)
95 | AST_EXPR_LT : ∀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_LTE: ∀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_EQ : ∀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_NEQ: ∀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)
104 | 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)
105 | 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)
106 | 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)
107 | 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)
108 | 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)
109 | 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)
111 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
112 ast_var d e b t → ast_expr d e t
114 let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
115 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
117 return λW.λa:ast_expr d e W.astfe_expr fe W
119 [ AST_EXPR_BYTE8 val ⇒
120 ASTFE_EXPR_BYTE8 fe val
121 | AST_EXPR_WORD16 val ⇒
122 ASTFE_EXPR_WORD16 fe val
123 | AST_EXPR_WORD32 val ⇒
124 ASTFE_EXPR_WORD32 fe val
126 | AST_EXPR_NEG bType sExpr ⇒
127 ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
128 | AST_EXPR_NOT bType sExpr ⇒
129 ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
130 | AST_EXPR_COM bType sExpr ⇒
131 ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
133 | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
134 ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
135 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
136 | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
137 ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
138 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
139 | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
140 ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
141 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
142 | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
143 ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
144 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
145 | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
146 ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
147 (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
148 | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
149 ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
150 (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
152 | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
153 ASTFE_EXPR_GT 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 bType) sExpr2 m fe dimInv)
155 | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
156 ASTFE_EXPR_GTE 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_LT bType sExpr1 sExpr2 ⇒
159 ASTFE_EXPR_LT 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_LTE bType sExpr1 sExpr2 ⇒
162 ASTFE_EXPR_LTE 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)
164 | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
165 ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
166 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
167 | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
168 ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
169 (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
171 | AST_EXPR_B8toW16 sExpr ⇒
172 ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
173 | AST_EXPR_B8toW32 sExpr ⇒
174 ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
175 | AST_EXPR_W16toB8 sExpr ⇒
176 ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
177 | AST_EXPR_W16toW32 sExpr ⇒
178 ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
179 | AST_EXPR_W32toB8 sExpr ⇒
180 ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
181 | AST_EXPR_W32toW16 sExpr ⇒
182 ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
184 | AST_EXPR_ID b sType var ⇒
185 ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
189 AST_VAR_ID: ∀b:bool.∀t:ast_type.
190 ast_id d e b t → ast_var d e b t
191 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
192 ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
193 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
194 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)
196 and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
197 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
199 return λW,X.λa:ast_var d e W X.astfe_var fe W X
201 [ AST_VAR_ID sB sType sId ⇒
202 ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
204 | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
205 ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
206 (ast_to_astfe_base_expr d e sExpr m fe dimInv)
208 | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
209 ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)
212 AST_BASE_EXPR: ∀t:ast_base_type.
213 ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e
216 and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
217 (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
219 return λa:ast_base_expr d e.astfe_base_expr fe
221 [ AST_BASE_EXPR bType sExpr ⇒
222 ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
225 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
226 d (e:aux_env_type d) (m:aux_map_type d) fe'
227 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
229 return λW.λa:astfe_expr fe W.astfe_expr fe' W
231 [ ASTFE_EXPR_BYTE8 val ⇒
232 ASTFE_EXPR_BYTE8 fe' val
233 | ASTFE_EXPR_WORD16 val ⇒
234 ASTFE_EXPR_WORD16 fe' val
235 | ASTFE_EXPR_WORD32 val ⇒
236 ASTFE_EXPR_WORD32 fe' val
238 | ASTFE_EXPR_NEG bType sExpr ⇒
239 ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
240 | ASTFE_EXPR_NOT bType sExpr ⇒
241 ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
242 | ASTFE_EXPR_COM bType sExpr ⇒
243 ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
245 | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
246 ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
247 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
248 | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
249 ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
250 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
251 | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
252 ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
253 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
254 | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
255 ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
256 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
257 | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
258 ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
259 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
260 | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
261 ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
262 (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
264 | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
265 ASTFE_EXPR_GT 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_GTE bType sExpr1 sExpr2 ⇒
268 ASTFE_EXPR_GTE 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_LT bType sExpr1 sExpr2 ⇒
271 ASTFE_EXPR_LT 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 bType) sExpr2 d e m fe' dimInv dimLe)
273 | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
274 ASTFE_EXPR_LTE 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 bType) sExpr2 d e m fe' dimInv dimLe)
276 | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
277 ASTFE_EXPR_EQ 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_NEQ bType sExpr1 sExpr2 ⇒
280 ASTFE_EXPR_NEQ 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)
283 | ASTFE_EXPR_B8toW16 sExpr ⇒
284 ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
285 | ASTFE_EXPR_B8toW32 sExpr ⇒
286 ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
287 | ASTFE_EXPR_W16toB8 sExpr ⇒
288 ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
289 | ASTFE_EXPR_W16toW32 sExpr ⇒
290 ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
291 | ASTFE_EXPR_W32toB8 sExpr ⇒
292 ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
293 | ASTFE_EXPR_W32toW16 sExpr ⇒
294 ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
296 | ASTFE_EXPR_ID b sType var ⇒
297 ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
300 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
301 d (e:aux_env_type d) (m:aux_map_type d) fe'
302 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
304 return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
306 [ ASTFE_VAR_ID sB sType sId ⇒
307 ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
309 | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
310 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)
311 (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
313 | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
314 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)
316 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
317 d (e:aux_env_type d) (m:aux_map_type d) fe'
318 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
320 return λa:astfe_base_expr fe.astfe_base_expr fe'
322 [ ASTFE_BASE_EXPR bType sExpr ⇒
323 ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
327 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
328 ast_var d e b t → ast_init d e t
329 | AST_INIT_VAL: ∀t:ast_type.
330 aux_ast_init_type t → ast_init d e t
332 definition ast_to_astfe_init ≝
333 λd.λe:aux_env_type d.λt.λast:ast_init d e t.
334 λm:aux_map_type d.λfe.
335 λdimInv:env_to_flatEnv_inv d e m fe.
337 return λW.λa:ast_init d e W.astfe_init fe W
339 [ AST_INIT_VAR sB sType sVar ⇒
340 ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
342 | AST_INIT_VAL sType sArgs ⇒
343 ASTFE_INIT_VAL fe sType sArgs
347 definition ast_to_astfe_retype_init ≝
348 λfe,t.λast:astfe_init fe t.
349 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
350 λdimInv:env_to_flatEnv_inv d e m fe'.
351 λdimLe:le_flatEnv fe fe' = true.
353 return λW.λa:astfe_init fe W.astfe_init fe' W
355 [ ASTFE_INIT_VAR sB sType sVar ⇒
356 ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
358 | ASTFE_INIT_VAL sType sArgs ⇒
359 ASTFE_INIT_VAL fe' sType sArgs
364 ASTFE_STM_ASG: ∀t:ast_type.
365 astfe_var e false t → astfe_expr e t → astfe_stm e
366 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
367 astfe_id e b t → astfe_init e t → astfe_stm e
368 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
369 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
371 let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe)
372 d (e:aux_env_type d) (m:aux_map_type d) fe'
373 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝
375 [ ASTFE_STM_ASG sType sVar sExpr ⇒
376 ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
377 (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
379 | ASTFE_STM_INIT sB sType sId sInit ⇒
380 ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
381 (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
383 | ASTFE_STM_WHILE sExpr sBody ⇒
384 ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
385 (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
387 | ASTFE_STM_IF sNelExprBody sOptBody ⇒
388 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)
389 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
391 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
394 (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
397 ASTFE_BODY: list (astfe_stm e) → astfe_body e
399 and ast_to_astfe_retype_body fe (ast:astfe_body fe)
400 d (e:aux_env_type d) (m:aux_map_type d) fe'
401 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_body fe' ≝
404 ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
407 definition ast_to_astfe_retype_stm_list ≝
408 λfe.λast:list (astfe_stm fe).
409 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
410 λdimInv:env_to_flatEnv_inv d e m fe'.
411 λdimLe:le_flatEnv fe fe' = true.
412 fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
414 definition ast_to_astfe_retype_exprBody_neList ≝
415 λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).
416 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
417 λdimInv:env_to_flatEnv_inv d e m fe'.
418 λdimLe:le_flatEnv fe fe' = true.
419 cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
420 (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
422 «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
425 (* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
426 inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
427 AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
428 env_to_flatEnv_inv d e m fe' →
429 le_flatEnv fe fe' = true →
431 ast_to_astfe_stm_record d e fe.
433 inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
434 AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
435 env_to_flatEnv_inv d e m fe' →
436 le_flatEnv fe fe' = true →
437 ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
438 ast_to_astfe_if_record d e fe.
440 inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
441 AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
442 env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
443 le_flatEnv fe fe' = true →
444 list (astfe_stm fe') →
445 ast_to_astfe_decl_record d e fe.
447 inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
448 AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
449 env_to_flatEnv_inv d e m fe' →
450 le_flatEnv fe fe' = true →
451 list (astfe_stm fe') →
452 ast_to_astfe_decl_aux_record d e fe.
455 AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
456 ast_var d e false t → ast_expr d e t → ast_stm d e
457 | AST_STM_WHILE: ∀d.∀e:aux_env_type d.
458 ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
459 | AST_STM_IF: ∀d.∀e:aux_env_type d.
460 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
462 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.
463 env_to_flatEnv_inv d e m fe →
464 ast_to_astfe_stm_record d e fe ≝
466 return λD.λE.λast:ast_stm D E.
467 Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
469 [ AST_STM_ASG sD sE sType sVar sExpr ⇒
470 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
471 AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
472 (eq_to_leflatenv ?? (refl_eq ??))
473 (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv)
474 (ast_to_astfe_expr sD sE sType sExpr m fe dimInv))
475 | AST_STM_WHILE sD sE sExpr sDecl ⇒
476 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
477 match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
478 (env_map_flatEnv_enter_aux sD sE m fe dimInv) with
479 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
480 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
481 (λenv.ast_to_astfe_stm_record sD env fe)
482 (AST_TO_ASTFE_STM_RECORD sD
483 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
485 (leave_map sD resMap)
487 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
489 (ASTFE_STM_WHILE resFe
490 (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv)
492 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
493 (leave_map sD resMap)
495 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
497 (ASTFE_BODY resFe resLStm)))
498 sE (leave_add_enter_env sD sE resTrsf) ]
500 | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
501 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
502 let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
503 (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
504 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝
507 match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
508 (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
509 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
510 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
511 (λenv.ast_to_astfe_if_record sD env pFe)
512 (AST_TO_ASTFE_IF_RECORD sD
513 (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 «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
521 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
522 (leave_map sD resMap)
524 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
526 (ASTFE_BODY resFe resLStm))»)
527 sE (leave_add_enter_env sD sE resTrsf) ]
530 match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
531 (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
532 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
533 match aux t (leave_map sD resMap) resFe
534 (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
535 (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
536 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
537 sE (leave_add_enter_env sD sE resTrsf)) with
538 [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
539 AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
540 (leflatenv_trans ??? resDimLe resDimLe')
541 («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
542 sD sE resMap' resFe' resDimInv'
543 (leflatenv_trans ??? resDimLe resDimLe'))
544 (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
545 sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
548 match aux sExprDecl m fe dimInv with
549 [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
552 AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
555 match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe
556 (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with
557 [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
558 eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
559 (λenv.ast_to_astfe_stm_record sD env fe)
560 (AST_TO_ASTFE_STM_RECORD sD
561 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
563 (leave_map sD resMap')
565 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
566 (leflatenv_trans ??? resDimLe resDimLe')
568 (ast_to_astfe_retype_exprBody_neList resFe resExprBody
570 (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
571 (leave_map sD resMap')
573 (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
575 (Some ? (ASTFE_BODY resFe' resLStm))))
576 sE (leave_add_enter_env sD sE resTrsf) ]]]
580 AST_NO_DECL: ∀d.∀e:aux_env_type d.
581 list (ast_stm d e) → ast_decl d e
582 | AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
583 (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e
585 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
586 env_to_flatEnv_inv d e m fe →
587 ast_to_astfe_decl_record d e fe ≝
589 return λD.λE.λast:ast_decl D E.
590 Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
592 [ AST_NO_DECL sD sE sLStm ⇒
593 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
594 let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
595 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
598 AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) []
601 match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
602 [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
603 match aux t resMap resFe resDimInv with
604 [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
605 AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
606 (leflatenv_trans ??? resDimLe resDimLe')
607 ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
610 match aux sLStm m fe dimInv with
611 [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
612 AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
613 (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
616 | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
617 λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
618 match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl
619 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
620 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
621 (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with
622 [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
623 AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
624 ([ tripleT ??? sName sB sType ]@resTrsf)
625 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
626 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)
630 [ ASTFE_STM_INIT resFe sB sType
631 (* l'id e' sull'ambiente arricchito *)
632 (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
634 (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType)
636 (newid_from_init sD sE sName sB sType)
637 (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
638 (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
639 (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv))
640 sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
642 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
644 (* l'init e' sull'ambiente non arricchito *)
645 (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
646 sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
648 (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
649 (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe))
655 AST_ROOT: ast_decl O empty_env → ast_root
657 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
658 λast:ast_root.match ast with
659 [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
660 [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].