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/environment.ma".
24 (* ********************** *)
25 (* GESTIONE AMBIENTE FLAT *)
26 (* ********************** *)
28 (* STRUTTURA AMBIENTE FLAT *)
30 (* elemento: name + desc *)
31 inductive flatVar_elem : Type ≝
32 VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
35 definition aux_flatEnv_type ≝ list flatVar_elem.
38 definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
39 definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
42 definition empty_flatEnv ≝ nil flatVar_elem.
44 (* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
45 let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
48 | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
49 [ true ⇒ Some ? (get_desc_flatVar h)
50 | false ⇒ get_desc_flatEnv_aux tl str ]].
52 definition get_desc_flatEnv ≝
53 λe:aux_flatEnv_type.λstr:aux_strId_type.
54 match get_desc_flatEnv_aux e str with
55 [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
57 definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
58 match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ].
60 definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
61 match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
63 lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
64 unfold checkb_desc_flatEnv;
65 unfold check_desc_flatEnv;
67 letin K ≝ (get_desc_flatEnv_aux e str);
69 [ normalize; autobatch |
70 normalize; autobatch ]
73 (* aggiungi descrittore ad ambiente: in coda *)
74 definition add_desc_flatEnv ≝
75 λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
76 e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
78 (* controllo fe <= fe' *)
79 definition eq_flatEnv_elem ≝
81 [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
82 [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
84 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
89 rewrite > (eq_to_eqstrid a a (refl_eq ??));
90 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
94 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
101 rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
102 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
106 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
109 | cons h tl ⇒ match fe' with
110 [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
113 lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
116 [ intros; exists; [ apply fe' | reflexivity ]
117 | intros 4; elim fe';
118 [ simplify in H1:(%); destruct H1
119 | simplify in H2:(%);
120 rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
121 cases (H l1 (andb_true_true_r ?? H2));
124 exists; [ apply x | reflexivity ]
129 lemma leflatenv_to_check : ∀fe,fe',str.
130 (le_flatEnv fe fe' = true) →
131 (check_desc_flatEnv fe str) →
132 (check_desc_flatEnv fe' str).
134 cases (leflatEnv_to_le fe fe' H);
137 [ intro; simplify in H2:(%); elim H2;
140 cases (eqStrId_str str (get_nameId_flatVar a));
141 [ simplify; intro; apply H3
148 lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
150 change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
155 change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
156 unfold eq_flatEnv_elem;
158 change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
159 rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
160 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
166 (* STRUTTURA MAPPA TRASFORMAZIONE *)
168 (* elemento: nome + cur + max + dimostrazione *)
169 inductive maxCur_elem (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
170 MAX_CUR_ELEM: ∀str:aux_str_type.∀cur:nat.nat → (check_desc_env e str → get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → maxCur_elem e fe.
173 definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
176 definition get_name_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM n _ _ _ ⇒ n ].
177 definition get_cur_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ c _ _ ⇒ c ].
178 definition get_max_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ _ m _ ⇒ m ].
180 (* mappa di trasformazione vuota *)
181 definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
183 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
185 (* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
186 let rec get_maxcur_map (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) (str:aux_str_type) on map ≝
189 | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with
190 [ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
193 definition next_nameId ≝
194 λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
195 match get_maxcur_map e fe map str with
196 [ None ⇒ STR_ID str 0
197 | Some maxcur ⇒ STR_ID str (S (get_max_maxCur e fe maxcur))
200 (* nome -> nome + id *)
201 definition name_to_nameId ≝
202 λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
203 match get_maxcur_map e fe map str with
204 [ None ⇒ STR_ID str 0
205 | Some maxcur ⇒ STR_ID str (get_cur_maxCur e fe maxcur)
208 (* NB: se cerco qualcos'altro il risultato e' invariato *)
209 axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
210 (check_desc_env e str →
211 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
212 (eqStr_str str str' = false) →
213 (check_desc_env (add_desc_env e str' b' desc') str →
214 get_desc_env (add_desc_env e str' b' desc') str =
215 get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
217 (* NB: se cerco cio' che e' appena stato aggiunto, deve essere uguale *)
218 axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
219 (check_desc_env e str →
220 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
221 (eqStr_str str str' = true) →
222 (check_desc_env (add_desc_env e str' b' desc') str →
223 get_desc_env (add_desc_env e str' b' desc') str =
224 get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
226 axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map.
227 check_desc_env (add_desc_env e str b desc) str →
228 get_desc_env (add_desc_env e str b desc) str =
229 get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0).
231 (* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
232 axiom ast_to_astfe_id_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str.
233 check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str).
235 axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map.
236 check_not_already_def_env e str →
237 check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str).
239 (* aggiungi/aggiorna descrittore mappa trasformazione *)
240 let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
241 (str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
242 : aux_trasfMap_type (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) ≝
248 [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
249 str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ]
251 | cons h tl ⇒ match h with
252 [ MAX_CUR_ELEM str' cur' max' dim' ⇒
253 match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with
254 [ true ⇒ λp:(eqStr_str str' str = true).
255 [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
256 str' (S max') (S max')
257 (add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
258 ]@(add_maxcur_map_aux e fe tl fMap str b desc true)
259 | false ⇒ λp:(eqStr_str str' str = false).
260 [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
262 (add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
263 ]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
264 ] (refl_eq ? (eqStr_str str' str))
268 definition add_maxcur_map ≝
269 λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
270 add_maxcur_map_aux e fe map fMap str b desc false.
272 (* composizione di funzioni generata da una lista di nome x const x tipo *)
273 definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type).
275 let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
278 | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
281 lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
282 ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
285 [ simplify; exists; [apply c | reflexivity]
286 | simplify; apply H; ]
289 lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
291 change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
292 cases (build_trasfEnv_exists_aux e trsf []);
297 (* NB: leave ... enter e' equivalente a e originale *)
298 lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf.
299 (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
300 get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) →
301 (check_desc_env e str →
302 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)).
304 rewrite > (eq_enter_leave e trsf);
310 let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
311 (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝
314 | cons h tl ⇒ match h with
315 [ MAX_CUR_ELEM str cur max dim ⇒
316 [MAX_CUR_ELEM e fe str cur max (retype_enter_leave_to_e_aux e fe str cur trsf dim)]@(retype_enter_leave_to_e e fe trsf tl)
319 lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf.
320 (check_desc_env e str →
321 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
322 (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
323 get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)).
325 rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
326 rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
332 let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
333 (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝
336 | cons h tl ⇒ match h with
337 [ MAX_CUR_ELEM str cur max dim ⇒
338 [MAX_CUR_ELEM (leave_env ((build_trasfEnv trsf) (enter_env e))) fe str cur max (retype_e_to_enter_leave_aux e fe str cur trsf dim)]@(retype_e_to_enter_leave e fe trsf tl)
341 (* NB: enter non cambia fe *)
342 lemma retype_e_to_enter_aux : ∀e,fe,str,cur.
343 (check_desc_env e str →
344 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
345 (check_desc_env (enter_env e) str →
346 get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
354 let rec retype_e_to_enter (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (enter_env e) fe ≝
357 | cons h tl ⇒ match h with
358 [ MAX_CUR_ELEM str cur max dim ⇒
359 [MAX_CUR_ELEM (enter_env e) fe str cur max (retype_e_to_enter_aux e fe str cur dim)]@(retype_e_to_enter e fe tl)
362 (* NB: leave non cambia fe *)
363 axiom retype_e_to_leave_aux : ∀e,fe,str,cur.
364 (check_desc_env e str →
365 get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
366 (check_desc_env (leave_env e) str →
367 get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
369 let rec retype_e_to_leave (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env e) fe ≝
372 | cons h tl ⇒ match h with
373 [ MAX_CUR_ELEM str cur max dim ⇒
374 [MAX_CUR_ELEM (leave_env e) fe str cur max (retype_e_to_leave_aux e fe str cur dim)]@(retype_e_to_leave e fe tl)
377 let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (trsf:aux_trasfEnv_type) (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe')
378 (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
380 [ nil ⇒ empty_trasfMap e fe'
382 match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
383 [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
385 [ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
386 (get_max_maxCur ?? h) (False_rect ? daemon) ]
387 ] @ rollback_map e fe fe' trsf tl snap
390 (* sequenza di utilizzo:
394 |DICHIARAZIONE "pippo":
395 | -) MAP1 <- add_maxcur_map MAP0 "pippo"
396 | -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
399 | -) name_to_nameId MAP1 "pippo"
401 |PREPARAZIONE ENTRATA BLOCCO INTERNO:
402 | -) SNAP <- build_snapshot MAP1
406 |DICHIARAZIONE "pippo":
407 | -) MAP2 <- add_maxcur_map MAP1 "pippo"
408 | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
411 | -) name_to_nameId MAP2 "pippo"
413 |PREPARAZIONE USCITA BLOCCO INTERNO:
414 | -) MAP3 <- rollback_map MAP2 SNAP
420 definition pippo ≝ [ ch_P ].
421 definition pluto ≝ [ ch_Q ].
422 definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
423 definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
424 definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
425 definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
426 definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
427 definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
429 definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
430 definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
431 definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
432 definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
433 definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
434 definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
436 definition env2' ≝ enter_env env2.
437 definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
439 definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
440 definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
441 definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
442 definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
443 definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
444 definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
446 definition env4' ≝ enter_env env4.
447 definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
449 definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
450 definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
451 definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
452 definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
453 definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
454 definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
456 definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
458 definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4.
460 definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
462 definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.