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 (* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
111 axiom ast_to_astfe_id_ax:
112 Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
113 Πmap:aux_trasfMap_type e fe.
114 check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)).
118 Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
119 Πmap:aux_trasfMap_type e fe.
121 (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))
125 Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
126 Πmap:aux_trasfMap_type e fe.
128 (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t.
131 definition ast_to_astfe_id:
132 Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
133 Πmap:aux_trasfMap_type e fe.
135 (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
136 (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))).
138 (λ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.
139 ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast)) ?);
140 apply ast_to_astfe_id_ax.
144 AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
145 AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
146 AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
148 AST_EXPR_NEG: ∀t:ast_base_type.
149 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
150 AST_EXPR_NOT: ∀t:ast_base_type.
151 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
152 AST_EXPR_COM: ∀t:ast_base_type.
153 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
155 AST_EXPR_ADD: ∀t:ast_base_type.
156 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
157 AST_EXPR_SUB: ∀t:ast_base_type.
158 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
159 AST_EXPR_MUL: ∀t:ast_base_type.
160 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
161 AST_EXPR_DIV: ∀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 t)
163 AST_EXPR_SHR: ∀t:ast_base_type.
164 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
165 AST_EXPR_SHL: ∀t:ast_base_type.
166 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
168 AST_EXPR_GT : ∀t:ast_base_type.
169 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
170 AST_EXPR_GTE: ∀t:ast_base_type.
171 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
172 AST_EXPR_LT : ∀t:ast_base_type.
173 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_LTE: ∀t:ast_base_type.
175 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
176 AST_EXPR_EQ : ∀t:ast_base_type.
177 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
178 AST_EXPR_NEQ: ∀t:ast_base_type.
179 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
181 AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
182 AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
183 AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
184 AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
185 AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
186 AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
188 AST_EXPR_ID: ∀b:bool.∀t:ast_type.
189 ast_var e b t → ast_expr e t
191 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) ≝
193 [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
194 | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
195 | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
197 | AST_EXPR_NEG bType subExpr ⇒
198 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
199 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
200 | AST_EXPR_NOT bType subExpr ⇒
201 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
202 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
203 | AST_EXPR_COM bType subExpr ⇒
204 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
205 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
207 | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
208 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
209 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
210 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
211 | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
212 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
213 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
214 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
215 | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
216 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
217 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
218 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
219 | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
220 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
221 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
222 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
223 | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
224 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
225 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
226 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
227 | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
228 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
229 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
230 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
232 | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
233 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
234 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
235 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
236 | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
237 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
238 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
239 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
240 | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
241 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
242 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
243 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
244 | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
245 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
246 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
247 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
248 | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
249 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
250 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
251 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
252 | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
253 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
254 (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
255 (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
257 | AST_EXPR_B8toW16 subExpr ⇒
258 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
259 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
260 | AST_EXPR_B8toW32 subExpr ⇒
261 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
262 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
263 | AST_EXPR_W16toB8 subExpr ⇒
264 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
265 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
266 | AST_EXPR_W16toW32 subExpr ⇒
267 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
268 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
269 | AST_EXPR_W32toB8 subExpr ⇒
270 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
271 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
272 | AST_EXPR_W32toW16 subExpr ⇒
273 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
274 (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
276 | AST_EXPR_ID b subType var ⇒
277 opt_map ?? (ast_to_astfe_var e b subType var fe map)
278 (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
281 AST_VAR_ID: ∀b:bool.∀t:ast_type.
282 ast_id e b t → ast_var e b t
283 AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
284 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
285 AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
286 ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
288 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) ≝
290 [ AST_VAR_ID subB subType subId ⇒
291 opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType)
292 (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t)
294 | AST_VAR_ARRAY subB subType dim var expr ⇒
295 opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map)
296 (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map)
297 (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t))
299 | AST_VAR_STRUCT subB nelSubType field var _ ⇒
300 opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map)
301 (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t)
304 AST_BASE_EXPR: ∀t:ast_base_type.
305 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
307 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) ≝
309 [ AST_BASE_EXPR bType subExpr ⇒
310 opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
311 (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
315 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
316 ast_var e b t → ast_init e t
317 AST_INIT_VAL: ∀t:ast_type.
318 aux_ast_init_type t → ast_init e t
320 definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝
321 λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
323 [ AST_INIT_VAR subB subType var ⇒
324 opt_map ?? (ast_to_astfe_var e subB subType var fe map)
325 (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t)
327 | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
331 AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
332 ast_var e false t → ast_expr e t → ast_stm e
333 AST_STM_WHILE: ∀e:aux_env_type.
334 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
335 AST_STM_IF: ∀e:aux_env_type.
336 ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
338 (* NB: il lemma dovrebbe poi prendere in input la dimostrazione che fe <= fe', cosi' ha senso *)
339 axiom retype_base_expr: ∀fe,fe'.astfe_base_expr fe → astfe_base_expr fe'.
340 axiom retype_init: ∀t,fe,fe'.astfe_init fe t → astfe_init fe' t.
341 axiom retype_list_decl: ∀fe,fe'.list (astfe_stm fe) → list (astfe_stm fe').
342 axiom retype_neList_body: ∀fe,fe'.ne_list (Prod (astfe_base_expr fe) (astfe_body fe)) → ne_list (Prod (astfe_base_expr fe') (astfe_body fe')).
344 (* applicare l'identita' e' inifluente *)
345 lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
346 aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe.
348 apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
351 axiom how_to_build_it : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:aux_env_type → aux_env_type.∀map:aux_trasfMap_type (f e) fe.∀ll:list (astfe_stm fe).
352 (sigma (aux_env_type\to aux_env_type)
353 (\lambda f:(aux_env_type\to aux_env_type).
354 (sigma aux_flatEnv_type
355 (\lambda fe':aux_flatEnv_type.
356 (Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe'))))))).
358 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
359 : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
361 return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
363 [ AST_STM_ASG e' subType var expr ⇒
364 λmap:aux_trasfMap_type e' fe.
365 opt_map ?? (ast_to_astfe_var e' false subType var fe map)
366 (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
367 (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
369 | AST_STM_WHILE e' expr decl ⇒
370 λmap:aux_trasfMap_type e' fe.
371 opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
372 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
373 (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
374 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
375 [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
376 [ pair map' resDecl ⇒
377 Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
378 (ASTFE_STM_WHILE fe' (retype_base_expr fe fe' resExpr) (ASTFE_BODY fe' resDecl))≫)
381 | AST_STM_IF e' nelExprDecl optDecl ⇒
382 λmap:aux_trasfMap_type e' fe.
383 let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
384 (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
387 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
388 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
389 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
390 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
391 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
393 Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
394 « pair ?? (retype_base_expr fenv fenv' resExpr) (ASTFE_BODY fenv' resDecl) £»≫)
398 opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
399 (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
400 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
401 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
402 [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
404 opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
405 (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
406 [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
408 Some ? (≪fenv'',pair ?? m''
409 (« pair ?? (retype_base_expr fenv fenv'' resExpr)
410 (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫)
413 opt_map ?? (aux fe map nelExprDecl)
414 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
415 [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
416 [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
417 [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
419 opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
420 (λsigmaRes':(Σf'.(Σfe'.Prod (aux_trasfMap_type (f' (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
421 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
422 [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
423 [ pair (m'':aux_trasfMap_type (f (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
424 Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
425 (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
426 (ASTFE_STM_IF fe'' (retype_neList_body fe' fe'' resNel) (Some ? (ASTFE_BODY fe'' resDecl)))≫)
430 AST_NO_DECL: ∀e:aux_env_type.
431 list (ast_stm e) → ast_decl e
432 AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
433 (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
435 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
436 : Πmap:aux_trasfMap_type e fe.option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe')))) ≝
438 return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe'))))
440 [ AST_NO_DECL e' lStm ⇒
441 λmap:aux_trasfMap_type e' fe.
442 let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
443 : option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ≝
445 [ nil ⇒ Some ? (how_to_build_it e' fenv (λx.x) (retype_map_to_id e' fenv (λx.x) m (refl_eq ??)) [])
447 opt_map ?? (ast_to_astfe_stm e' h fenv m)
448 (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
449 [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
451 opt_map ?? (aux tl fenv' m')
452 (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))).match sigmaRes' with
453 [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
454 [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type (f e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
456 Some ? (how_to_build_it e' fenv'' f m''
457 ((retype_list_decl fenv' fenv'' [ resStm ])@tl'))
461 | AST_DECL e' b name t _ optInit subDecl ⇒
462 λmap:aux_trasfMap_type e' fe.
463 opt_map ?? (match optInit with
466 opt_map ?? (ast_to_astfe_init e' t init fe map)
467 (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
468 (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
469 (next_nameId e' fe map name)
470 (False_rect ? daemon))
472 (λresId.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
474 (retype_init t fe (add_desc_flatEnv fe (next_nameId e' fe map name) b t) resInit)
477 (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
478 (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
479 (add_maxcur_map e' fe map map name b t))
480 (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
481 [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
482 [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
484 Some ? (how_to_build_it e' fe' (λx.f (add_desc_env x name b t)) map'
485 ((retype_list_decl (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' hRes)@tRes))
490 AST_ROOT: ast_decl empty_env → ast_root.
492 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
493 λast:ast_root.match ast with
494 [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
495 (* impossibile: dummy *)
496 [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
497 | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
498 [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
499 [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type (f empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
500 [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
504 (*include "compiler/preast_tree.ma".
505 include "compiler/preast_to_ast.ma".*)
509 const byte8[3] b={0,1,2};
528 PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
529 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,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
530 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]))) (
534 (PREAST_EXPR_BYTE8 〈xF,x2〉)
535 (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 []))
538 (PREAST_EXPR_BYTE8 〈xF,x0〉)
539 (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
542 (PREAST_EXPR_BYTE8 〈xF,x1〉)
544 (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
545 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 [])
549 » (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 [])))
556 lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.