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 (* ************************ *)
29 (* operatore di cast *)
30 definition ast_to_astfe_expr_check : Πfe.Πt.astfe_expr fe t → Πt'.option (astfe_expr fe t') ≝
31 λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_expr fe t.λt':ast_type.
32 match eq_ast_type t t'
33 return λx.(eq_ast_type t t' = x) → ?
35 [ true ⇒ λp:(eq_ast_type t t' = true).
36 Some ? (eq_rect ? t (λt.astfe_expr fe t) ast t' (eqasttype_to_eq ?? p))
37 | false ⇒ λp:(eq_ast_type t t' = false).None ?
38 ] (refl_eq ? (eq_ast_type t t')).
40 definition ast_to_astfe_init_check : Πfe.Πt.astfe_init fe t → Πt'.option (astfe_init fe t') ≝
41 λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λt':ast_type.
42 match eq_ast_type t t'
43 return λx.(eq_ast_type t t' = x) → ?
45 [ true ⇒ λp:(eq_ast_type t t' = true).
46 Some ? (eq_rect ? t (λt.astfe_init fe t) ast t' (eqasttype_to_eq ?? p))
47 | false ⇒ λp:(eq_ast_type t t' = false).None ?
48 ] (refl_eq ? (eq_ast_type t t')).
50 definition ast_to_astfe_var_checkb : Πfe.Πb.Πt.astfe_var fe b t → Πb'.option (astfe_var fe b' t) ≝
51 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.
53 return λx.(eq_bool b b' = x) → ?
55 [ true ⇒ λp:(eq_bool b b' = true).
56 Some ? (eq_rect ? b (λb.astfe_var fe b t) ast b' (eqbool_to_eq ?? p))
57 | false ⇒ λp:(eq_bool b b' = false).None ?
58 ] (refl_eq ? (eq_bool b b')).
60 definition ast_to_astfe_var_checkt : Πfe.Πb.Πt.astfe_var fe b t → Πt'.option (astfe_var fe b t') ≝
61 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λt':ast_type.
62 match eq_ast_type t t'
63 return λx.(eq_ast_type t t' = x) → ?
65 [ true ⇒ λp:(eq_ast_type t t' = true).
66 Some ? (eq_rect ? t (λt.astfe_var fe b t) ast t' (eqasttype_to_eq ?? p))
67 | false ⇒ λp:(eq_ast_type t t' = false).None ?
68 ] (refl_eq ? (eq_ast_type t t')).
70 definition ast_to_astfe_var_check : Πfe.Πb.Πt.astfe_var fe b t → Πb'.Πt'.option (astfe_var fe b' t') ≝
71 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.λt':ast_type.
72 opt_map ?? (ast_to_astfe_var_checkb fe b t ast b')
73 (λres.opt_map ?? (ast_to_astfe_var_checkt fe b' t res t')
76 definition ast_to_astfe_id_checkb : Πfe.Πb.Πt.astfe_id fe b t → Πb'.option (astfe_id fe b' t) ≝
77 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.
79 return λx.(eq_bool b b' = x) → ?
81 [ true ⇒ λp:(eq_bool b b' = true).
82 Some ? (eq_rect ? b (λb.astfe_id fe b t) ast b' (eqbool_to_eq ?? p))
83 | false ⇒ λp:(eq_bool b b' = false).None ?
84 ] (refl_eq ? (eq_bool b b')).
86 definition ast_to_astfe_id_checkt : Πfe.Πb.Πt.astfe_id fe b t → Πt'.option (astfe_id fe b t') ≝
87 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λt':ast_type.
88 match eq_ast_type t t'
89 return λx.(eq_ast_type t t' = x) → ?
91 [ true ⇒ λp:(eq_ast_type t t' = true).
92 Some ? (eq_rect ? t (λt.astfe_id fe b t) ast t' (eqasttype_to_eq ?? p))
93 | false ⇒ λp:(eq_ast_type t t' = false).None ?
94 ] (refl_eq ? (eq_ast_type t t')).
96 definition ast_to_astfe_id_check : Πfe.Πb.Πt.astfe_id fe b t → Πb'.Πt'.option (astfe_id fe b' t') ≝
97 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.λt':ast_type.
98 opt_map ?? (ast_to_astfe_id_checkb fe b t ast b')
99 (λres.opt_map ?? (ast_to_astfe_id_checkt fe b' t res t')
100 (λres'.Some ? res')).
103 AST_ID: ∀str:aux_str_type.
104 (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
106 definition get_name_ast_id ≝
107 λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.
108 match ast with [ AST_ID s _ ⇒ s ].
110 definition ast_to_astfe_id :
111 Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
112 Πmap:aux_trasfMap_type e fe.
114 (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
115 (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) ≝
116 λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
117 ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast))
118 (ast_to_astfe_id_aux e fe map (get_name_ast_id e b t ast)
120 (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:ast_id e Hbeta3 Hbeta2.check_desc_env e (get_name_ast_id e Hbeta3 Hbeta2 Hbeta1))
121 (λa:aux_str_type.λH:check_desc_env e a.H) b t ast)).
123 definition get_name_astfe_id ≝ λfe,b,t.λast:astfe_id fe b t.match ast with [ ASTFE_ID n _ ⇒ n ].
126 : Πfe:aux_flatEnv_type.Πb:bool.Πt:ast_type.Πast:astfe_id fe b t.Πfe':aux_flatEnv_type.le_flatEnv fe fe' = true →
128 (get_const_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast)))
129 (get_type_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) ≝
130 λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
131 ASTFE_ID fe' (get_name_astfe_id fe b t ast)
132 (leflatenv_to_check fe fe' (get_name_astfe_id fe b t ast) dim (astfe_id_ind fe
133 (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:astfe_id fe Hbeta3 Hbeta2.check_desc_flatEnv fe (get_name_astfe_id fe Hbeta3 Hbeta2 Hbeta1))
134 (λa:aux_strId_type.λH:check_desc_flatEnv fe a.H) b t ast)).
137 AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
138 AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
139 AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
141 AST_EXPR_NEG: ∀t:ast_base_type.
142 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
143 AST_EXPR_NOT: ∀t:ast_base_type.
144 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
145 AST_EXPR_COM: ∀t:ast_base_type.
146 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
148 AST_EXPR_ADD: ∀t:ast_base_type.
149 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
150 AST_EXPR_SUB: ∀t:ast_base_type.
151 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
152 AST_EXPR_MUL: ∀t:ast_base_type.
153 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
154 AST_EXPR_DIV: ∀t:ast_base_type.
155 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
156 AST_EXPR_SHR: ∀t:ast_base_type.
157 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
158 AST_EXPR_SHL: ∀t:ast_base_type.
159 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
161 AST_EXPR_GT : ∀t:ast_base_type.
162 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
163 AST_EXPR_GTE: ∀t:ast_base_type.
164 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
165 AST_EXPR_LT : ∀t:ast_base_type.
166 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
167 AST_EXPR_LTE: ∀t:ast_base_type.
168 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
169 AST_EXPR_EQ : ∀t:ast_base_type.
170 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
171 AST_EXPR_NEQ: ∀t:ast_base_type.
172 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
174 AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
175 AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
176 AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
177 AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
178 AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
179 AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
181 AST_EXPR_ID: ∀b:bool.∀t:ast_type.
182 ast_var e b t → ast_expr e t
184 let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_expr fe t) ≝
186 [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
187 | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
188 | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
190 | AST_EXPR_NEG bType subExpr ⇒
191 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
192 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
193 | AST_EXPR_NOT bType subExpr ⇒
194 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
195 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
196 | AST_EXPR_COM bType subExpr ⇒
197 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
198 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
200 | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
201 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
202 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
203 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
204 | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
205 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
206 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
207 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
208 | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
209 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
210 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
211 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
212 | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
213 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
214 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
215 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
216 | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
217 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
218 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
219 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
220 | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
221 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
222 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
223 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
225 | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
226 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
227 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
228 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
229 | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
230 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
231 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
232 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
233 | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
234 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
235 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
236 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
237 | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
238 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
239 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
240 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
241 | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
242 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
243 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
244 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
245 | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
246 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
247 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
248 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
250 | AST_EXPR_B8toW16 subExpr ⇒
251 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
252 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
253 | AST_EXPR_B8toW32 subExpr ⇒
254 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
255 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
256 | AST_EXPR_W16toB8 subExpr ⇒
257 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
258 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
259 | AST_EXPR_W16toW32 subExpr ⇒
260 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
261 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
262 | AST_EXPR_W32toB8 subExpr ⇒
263 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
264 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
265 | AST_EXPR_W32toW16 subExpr ⇒
266 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
267 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
269 | AST_EXPR_ID b subType var ⇒
270 opt_map ?? (ast_to_astfe_var e b subType var fe map)
271 (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
274 AST_VAR_ID: ∀b:bool.∀t:ast_type.
275 ast_id e b t → ast_var e b t
276 AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
277 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
278 AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
279 ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
281 and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_var fe b t) ≝
283 [ AST_VAR_ID subB subType subId ⇒
284 opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType)
285 (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t)
287 | AST_VAR_ARRAY subB subType dim var expr ⇒
288 opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map)
289 (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map)
290 (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t))
292 | AST_VAR_STRUCT subB nelSubType field var _ ⇒
293 opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map)
294 (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t)
297 AST_BASE_EXPR: ∀t:ast_base_type.
298 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
300 and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_base_expr fe) ≝
302 [ AST_BASE_EXPR bType subExpr ⇒
303 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
304 (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
307 let rec retype_expr (fe:aux_flatEnv_type) (t:ast_type) (ast:astfe_expr fe t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_expr fe' t) ≝
309 [ ASTFE_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' val) t
310 | ASTFE_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe' val) t
311 | ASTFE_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe' val) t
313 | ASTFE_EXPR_NEG bType subExpr ⇒
314 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
315 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe' bType res) t)
316 | ASTFE_EXPR_NOT bType subExpr ⇒
317 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
318 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe' bType res) t)
319 | ASTFE_EXPR_COM bType subExpr ⇒
320 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
321 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe' bType res) t)
323 | ASTFE_EXPR_ADD bType subExpr1 subExpr2 ⇒
324 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
325 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
326 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe' bType res1 res2) t))
327 | ASTFE_EXPR_SUB bType subExpr1 subExpr2 ⇒
328 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
329 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
330 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe' bType res1 res2) t))
331 | ASTFE_EXPR_MUL bType subExpr1 subExpr2 ⇒
332 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
333 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
334 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe' bType res1 res2) t))
335 | ASTFE_EXPR_DIV bType subExpr1 subExpr2 ⇒
336 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
337 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
338 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe' bType res1 res2) t))
339 | ASTFE_EXPR_SHR bType subExpr1 subExpr2 ⇒
340 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
341 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
342 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe' bType res1 res2) t))
343 | ASTFE_EXPR_SHL bType subExpr1 subExpr2 ⇒
344 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
345 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
346 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe' bType res1 res2) t))
348 | ASTFE_EXPR_LT bType subExpr1 subExpr2 ⇒
349 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
350 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
351 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe' bType res1 res2) t))
352 | ASTFE_EXPR_LTE bType subExpr1 subExpr2 ⇒
353 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
354 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
355 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe' bType res1 res2) t))
356 | ASTFE_EXPR_GT bType subExpr1 subExpr2 ⇒
357 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
358 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
359 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe' bType res1 res2) t))
360 | ASTFE_EXPR_GTE bType subExpr1 subExpr2 ⇒
361 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
362 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
363 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe' bType res1 res2) t))
364 | ASTFE_EXPR_EQ bType subExpr1 subExpr2 ⇒
365 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
366 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
367 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe' bType res1 res2) t))
368 | ASTFE_EXPR_NEQ bType subExpr1 subExpr2 ⇒
369 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
370 (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
371 (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe' bType res1 res2) t))
373 | ASTFE_EXPR_B8toW16 subExpr ⇒
374 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
375 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe' res) t)
376 | ASTFE_EXPR_B8toW32 subExpr ⇒
377 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
378 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe' res) t)
379 | ASTFE_EXPR_W16toB8 subExpr ⇒
380 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
381 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe' res) t)
382 | ASTFE_EXPR_W16toW32 subExpr ⇒
383 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
384 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe' res) t)
385 | ASTFE_EXPR_W32toB8 subExpr ⇒
386 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
387 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe' res) t)
388 | ASTFE_EXPR_W32toW16 subExpr ⇒
389 opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
390 (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe' res) t)
392 | ASTFE_EXPR_ID b subType var ⇒
393 opt_map ?? (retype_var fe b subType var fe' dim)
394 (λres.ast_to_astfe_expr_check fe' subType (ASTFE_EXPR_ID fe' b subType res) t)
396 and retype_var (fe:aux_flatEnv_type) (b:bool) (t:ast_type) (ast:astfe_var fe b t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_var fe' b t) ≝
398 [ ASTFE_VAR_ID subB subType subId ⇒
399 opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
400 (λresId.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ID fe' subB subType resId) b t)
402 | ASTFE_VAR_ARRAY subB subType n var expr ⇒
403 opt_map ?? (retype_var fe subB (AST_TYPE_ARRAY subType n) var fe' dim)
404 (λresVar.opt_map ?? (retype_base_expr fe expr fe' dim)
405 (λresExpr.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ARRAY fe' subB subType n resVar resExpr) b t))
407 | ASTFE_VAR_STRUCT subB nelSubType field var ⇒
408 opt_map ?? (retype_var fe subB (AST_TYPE_STRUCT nelSubType) var fe' dim)
409 (λres.ast_to_astfe_var_check fe' subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe' subB nelSubType field res) b t)
411 and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_base_expr fe') ≝
413 [ ASTFE_BASE_EXPR bType subExpr ⇒
414 opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
415 (λres.Some ? (ASTFE_BASE_EXPR fe' bType res))
419 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
420 ast_var e b t → ast_init e t
421 AST_INIT_VAL: ∀t:ast_type.
422 aux_ast_init_type t → ast_init e t
424 definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝
425 λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
427 [ AST_INIT_VAR subB subType var ⇒
428 opt_map ?? (ast_to_astfe_var e subB subType var fe map)
429 (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t)
431 | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
434 definition retype_init ≝
435 λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
437 [ ASTFE_INIT_VAR subB subType var ⇒
438 opt_map ?? (retype_var fe subB subType var fe' dim)
439 (λres.ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAR fe' subB subType res) t)
441 | ASTFE_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAL fe' subType args) t
445 ASTFE_STM_ASG: ∀t:ast_type.
446 astfe_var e false t → astfe_expr e t → astfe_stm e
447 ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
448 astfe_id e b t → astfe_init e t → astfe_stm e
449 ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
450 ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
452 let rec retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝
454 [ ASTFE_STM_ASG subType var expr ⇒
455 opt_map ?? (retype_var fe false subType var fe' dim)
456 (λresVar.opt_map ?? (retype_expr fe subType expr fe' dim)
457 (λresExpr.Some ? (ASTFE_STM_ASG fe' subType resVar resExpr)))
459 | ASTFE_STM_INIT subB subType subId init ⇒
460 opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
461 (λresId.opt_map ?? (retype_init fe subType init fe' dim)
462 (λresInit.Some ? (ASTFE_STM_INIT fe' subB subType resId resInit)))
464 | ASTFE_STM_WHILE expr body ⇒
465 opt_map ?? (retype_base_expr fe expr fe' dim)
466 (λresExpr.opt_map ?? (retype_body fe body fe' dim)
467 (λresBody.Some ? (ASTFE_STM_WHILE fe' resExpr resBody)))
469 | ASTFE_STM_IF nelExprBody optBody ⇒
470 opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
471 (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
472 (λresBody.opt_map ?? t
473 (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
474 (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
476 (λres.match optBody with
477 [ None ⇒ Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (None ?))
479 opt_map ?? (retype_body fe body fe' dim)
480 (λresBody.Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (Some ? resBody)))
484 ASTFE_BODY: list (astfe_stm e) → astfe_body e
486 and retype_body (fe:aux_flatEnv_type) (ast:astfe_body fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_body fe') ≝
489 opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
491 (λt'.Some ? ([h']@t')))) (Some ? []) lStm)
492 (λresStm.Some ? (ASTFE_BODY fe' resStm))
495 definition retype_stm_list ≝
496 λfe:aux_flatEnv_type.λast:list (astfe_stm fe).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
497 fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
499 (λt'.Some ? ([h']@t')))) (Some ? []) ast.
501 definition retype_exprAndBody_neList ≝
502 λfe:aux_flatEnv_type.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
503 opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
504 (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
505 (λresBody.opt_map ?? t
506 (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
507 (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
509 (λres.Some ? (cut_last_neList ? res)).
511 (* applicare l'identita' e' inifluente *)
512 lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
513 aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe.
515 apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
519 AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
520 ast_var e false t → ast_expr e t → ast_stm e
521 AST_STM_WHILE: ∀e:aux_env_type.
522 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
523 AST_STM_IF: ∀e:aux_env_type.
524 ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
526 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
527 : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
529 return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
531 [ AST_STM_ASG e' subType var expr ⇒
532 λmap:aux_trasfMap_type e' fe.
533 opt_map ?? (ast_to_astfe_var e' false subType var fe map)
534 (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
535 (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
537 | AST_STM_WHILE e' expr decl ⇒
538 λmap:aux_trasfMap_type e' fe.
539 opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
540 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
541 (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
542 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
543 [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
544 [ pair map' resDecl ⇒
545 match le_flatEnv fe fe'
546 return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
548 [ true ⇒ λp:(le_flatEnv fe fe' = true).
549 opt_map ?? (retype_base_expr fe resExpr fe' p)
550 (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
551 (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
552 | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
553 ] (refl_eq ? (le_flatEnv fe fe'))
556 | AST_STM_IF e' nelExprDecl optDecl ⇒
557 λmap:aux_trasfMap_type e' fe.
558 let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
559 (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
562 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
563 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
564 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
565 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
566 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
568 match le_flatEnv fenv fenv'
569 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'))))
571 [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
572 opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
573 (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
574 «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
575 | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
576 ] (refl_eq ? (le_flatEnv fenv fenv'))
580 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
581 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
582 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
583 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
584 [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
586 opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
587 (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
588 [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
590 match le_flatEnv fenv fenv''
591 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'))))
593 [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
594 match le_flatEnv fenv' fenv''
595 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'))))
597 [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
598 opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
599 (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
601 Some ? (≪fenv'',pair ?? m''
603 (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
604 | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
605 ] (refl_eq ? (le_flatEnv fenv' fenv''))
606 | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
607 ] (refl_eq ? (le_flatEnv fenv fenv''))
610 opt_map ?? (aux fe map nelExprDecl)
611 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
612 [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
613 [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
614 [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
616 opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
617 (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
618 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
619 [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
620 [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
621 match le_flatEnv fe' fe''
622 return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
624 [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
625 opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
626 (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
627 (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
628 (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
629 | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
630 ] (refl_eq ? (le_flatEnv fe' fe''))
634 AST_NO_DECL: ∀e:aux_env_type.
635 list (ast_stm e) → ast_decl e
636 AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
637 (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
639 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
640 : Π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')))) ≝
642 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'))))
644 [ AST_NO_DECL e' lStm ⇒
645 λmap:aux_trasfMap_type e' fe.
646 let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
647 : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
649 [ nil ⇒ let trsf ≝ []
650 in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
651 (list (astfe_stm fenv))
652 (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
655 opt_map ?? (ast_to_astfe_stm e' h fenv m)
656 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
657 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
659 opt_map ?? (aux tl fenv' m')
660 (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
661 [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
662 [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
664 match le_flatEnv fenv' fenv''
665 return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
667 [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
668 opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
669 (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
670 (list (astfe_stm fenv''))
673 | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
674 ] (refl_eq ? (le_flatEnv fenv' fenv''))
678 | AST_DECL e' b name t dim optInit subDecl ⇒
679 λmap:aux_trasfMap_type e' fe.
680 opt_map ?? (match optInit with
683 opt_map ?? (ast_to_astfe_init e' t init fe map)
684 (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
685 (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
686 (next_nameId e' fe map name)
687 (ast_to_astfe_dec_aux e' name b t fe map dim))
689 (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
690 (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
691 (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
693 (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
694 (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
695 (add_maxcur_map e' fe map map name b t))
696 (λ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
697 [ 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
698 [ 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
699 [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
700 match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
701 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'))))
703 [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
704 opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
705 (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
706 in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
707 (list (astfe_stm fe'))
710 | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
711 ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
716 AST_ROOT: ast_decl empty_env → ast_root.
718 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
719 λast:ast_root.match ast with
720 [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
721 (* impossibile: dummy *)
722 [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
723 | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
724 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
725 [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
726 [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
730 include "compiler/preast_tree.ma".
731 include "compiler/preast_to_ast.ma".
734 const byte8[3] b={0,1,2};
752 PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
753 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〉)»))) (
754 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]))) (
758 (PREAST_EXPR_BYTE8 〈xF,x0〉)
759 (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
762 (PREAST_EXPR_BYTE8 〈xF,x1〉)
764 (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
765 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 [])
770 (PREAST_EXPR_BYTE8 〈xF,x2〉)
771 (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 []))
773 » (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 [])))