helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/environment.ma".
  23
  24 (* ********************** *)
  25 (* GESTIONE AMBIENTE FLAT *)
  26 (* ********************** *)
  27
  28 (* STRUTTURA AMBIENTE FLAT *)
  29
  30 (* elemento: name + desc *)
  31 inductive flatVar_elem : Type ≝
  32 VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
  33
  34 (* tipo pubblico *)
  35 definition aux_flatEnv_type ≝ list flatVar_elem.
  36
  37 (* getter *)
  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 ].
  40
  41 (* ambiente vuoto *)
  42 definition empty_flatEnv ≝ nil flatVar_elem.
  43
  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 ≝
  46 match e with
  47  [ nil ⇒ None ?
  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 ]].
  51
  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 ].
  56
  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 ].
  59
  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 ].
  62
  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;
  66  intros;
  67  letin K ≝ (get_desc_flatEnv_aux e str);
  68  elim K;
  69  [ normalize; autobatch |
  70    normalize; autobatch ]
  71 qed.
  72
  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)].
  77
  78 (* controllo fe <= fe' *)
  79 definition eq_flatEnv_elem ≝
  80 λe1,e2.match e1 with
  81  [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
  82   [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
  83
  84 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
  85  intros 3;
  86  rewrite < H;
  87  elim e1;
  88  simplify;
  89  rewrite > (eq_to_eqstrid a a (refl_eq ??));
  90  rewrite > (eq_to_eqdescelem d d (refl_eq ??));
  91  reflexivity.
  92 qed.
  93
  94 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
  95  intros 2;
  96  elim e1 0;
  97  elim e2 0;
  98  intros 4;
  99  simplify;
 100  intro;
 101  rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
 102  rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
 103  reflexivity.
 104 qed.
 105
 106 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
 107 match fe with
 108   [ nil ⇒ true
 109   | cons h tl ⇒ match fe' with
 110    [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
 111   ].
 112
 113 lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
 114  intro;
 115  elim fe 0;
 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));
 122      simplify;
 123      rewrite < H3;
 124      exists; [ apply x | reflexivity ]
 125    ]
 126  ].
 127 qed.
 128
 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).
 133  intros 4;
 134  cases (leflatEnv_to_le fe fe' H);
 135  rewrite < H1;
 136  elim fe 0;
 137  [ intro; simplify in H2:(%); elim H2;
 138  | intros 3;
 139    simplify;
 140    cases (eqStrId_str str (get_nameId_flatVar a));
 141    [ simplify; intro; apply H3
 142    | simplify;
 143      apply H2
 144    ]
 145  ].
 146 qed.
 147
 148 lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
 149 intros;
 150  change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
 151  elim fe 0;
 152  [ 1: reflexivity
 153  | 2: do 3 intro;
 154       unfold le_flatEnv;
 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;
 157       elim a;
 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 ??));
 161       rewrite > H;
 162       reflexivity
 163  ].
 164 qed.
 165
 166 (* STRUTTURA MAPPA TRASFORMAZIONE *)
 167
 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.
 171
 172 (* tipo pubblico *)
 173 definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
 174
 175 (* getter *)
 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 ].
 179
 180 (* mappa di trasformazione vuota *)
 181 definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
 182
 183 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
 184
 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 ≝
 187  match map with
 188   [ nil ⇒ None ?
 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 ]].
 191
 192 (* prossimo nome *)
 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))
 198   ].
 199
 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)
 206   ].
 207
 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)).
 216
 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))).
 225
 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).
 230
 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).
 234
 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).
 238
 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) ≝
 243 match map with
 244  [ nil ⇒
 245     match flag with
 246      [ true ⇒ []
 247      | false ⇒
 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) ]
 250      ]
 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)
 261                             str' cur' max'
 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))
 265   ]
 266  ].
 267
 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.
 271
 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).
 274
 275 let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
 276  match trasf with
 277   [ nil ⇒ (λx.x)
 278   | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
 279   ].
 280
 281 lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
 282  ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
 283  intros 2;
 284  elim trsf;
 285   [ simplify; exists; [apply c | reflexivity]
 286   | simplify; apply H; ]
 287 qed.
 288
 289 lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
 290  intros;
 291  change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
 292  cases (build_trasfEnv_exists_aux e trsf []);
 293  rewrite > H;
 294  reflexivity.
 295 qed.
 296
 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)).
 303  intros 5;
 304  rewrite > (eq_enter_leave e trsf);
 305  intros;
 306  apply H;
 307  apply H1.
 308 qed.
 309
 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 ≝
 312  match map with
 313   [ nil ⇒ []
 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)
 317    ]].
 318
 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)).
 324  intros 5;
 325  rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
 326  rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
 327  intros;
 328  apply H;
 329  apply H1.
 330 qed.
 331
 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 ≝
 334  match map with
 335   [ nil ⇒ []
 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)
 339    ]].
 340
 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)).
 347  intros 6;
 348  rewrite > H;
 349  [ reflexivity
 350  | apply H1
 351  ].
 352 qed.
 353
 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 ≝
 355  match map with
 356   [ nil ⇒ []
 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)
 360    ]].
 361
 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)).
 368
 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 ≝
 370  match map with
 371   [ nil ⇒ []
 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)
 375    ]].
 376
 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' ≝
 379  match map with
 380   [ nil ⇒ empty_trasfMap e fe'
 381   | cons h tl ⇒
 382      match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
 383    [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
 384    | Some new ⇒
 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
 388   ].
 389
 390 (* sequenza di utilizzo:
 391
 392 [BLOCCO ESTERNO]
 393
 394 |DICHIARAZIONE "pippo":
 395 | -) MAP1 <- add_maxcur_map MAP0 "pippo"
 396 | -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
 397 |
 398 |ACCESSO "pippo":
 399 | -) name_to_nameId MAP1 "pippo"
 400 |
 401 |PREPARAZIONE ENTRATA BLOCCO INTERNO:
 402 | -) SNAP <- build_snapshot MAP1
 403
 404   |[BLOCCO INTERNO]
 405   |
 406   |DICHIARAZIONE "pippo":
 407   |  -) MAP2 <- add_maxcur_map MAP1 "pippo"
 408   |  -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
 409   |
 410   |ACCESSO "pippo":
 411   | -) name_to_nameId MAP2 "pippo"
 412   |
 413   |PREPARAZIONE USCITA BLOCCO INTERNO:
 414   | -) MAP3 <- rollback_map MAP2 SNAP
 415
 416 | ...
 417 *)
 418
 419 (* mini test
 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).
 428
 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.
 435
 436 definition env2' ≝ enter_env env2.
 437 definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
 438
 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.
 445
 446 definition env4' ≝ enter_env env4.
 447 definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
 448
 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.
 455
 456 definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
 457
 458 definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4.
 459
 460 definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
 461
 462 definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.
 463 *)