X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fenv_to_flatenv.ma;h=865f9e5c9fc5c7dc8a80fb77254dd584212804be;hb=7ec26dcce747c05e2f0d12940d7d92237dbe9146;hp=4d3a092c1e482961bd51fae2a9c258bc8b8bdd29;hpb=a8ad55eb789b38c85c5581089308e349e4b0f1a3;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
index 4d3a092c1..865f9e5c9 100755
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -41,100 +41,350 @@ definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _
 (* ambiente vuoto *)
 definition empty_flatEnv ≝ nil flatVar_elem.
 
+(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
+let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝
+match e with
+ [ nil ⇒ None ?
+ | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with
+  [ true ⇒ Some ? (get_desc_flatVar h)
+  | false ⇒ get_desc_flatEnv_aux tl str ]].
+
+definition get_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with
+  [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+
+definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+ unfold checkb_desc_flatEnv;
+ unfold check_desc_flatEnv;
+ intros;
+ letin K ≝ (get_desc_flatEnv_aux e str);
+ elim K;
+ [ normalize; autobatch |
+   normalize; autobatch ]
+qed.
+
+(* aggiungi descrittore ad ambiente: in coda *)
+definition add_desc_flatEnv ≝
+λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
+ e@[VAR_FLAT_ELEM str (DESC_ELEM b t)].
+
+(* controllo fe <= fe' *)
+definition eq_flatEnv_elem ≝
+λe1,e2.match e1 with
+ [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
+  [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
+
+lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ simplify;
+ rewrite > (eq_to_eqstrid a a (refl_eq ??));
+ rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+ reflexivity.
+qed.
+
+lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
+ intros 2;
+ elim e1 0;
+ elim e2 0;
+ intros 4;
+ simplify;
+ intro;
+ rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
+ rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
+ reflexivity.
+qed.
+
+let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
+match fe with
+  [ nil ⇒ true
+  | cons h tl ⇒ match fe' with
+   [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
+  ].
+
+lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
+ intro;
+ elim fe 0;
+ [ intros; exists; [ apply fe' | reflexivity ]
+ | intros 4; elim fe';
+   [ simplify in H1:(%); destruct H1
+   | simplify in H2:(%);
+     rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
+     cases (H l1 (andb_true_true_r ?? H2));
+     simplify;
+     rewrite < H3;
+     exists; [ apply x | reflexivity ]
+   ]
+ ].
+qed.
+
+lemma leflatenv_to_check : ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (check_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatEnv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro; simplify in H2:(%); elim H2;
+ | intros 3;
+   simplify;
+   cases (eqStrId_str str (get_nameId_flatVar a));
+   [ simplify; intro; apply H3
+   | simplify;
+     apply H2
+   ]
+ ].
+qed.
+
+lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true.
+intros;
+ change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]);
+ elim fe 0;
+ [ 1: reflexivity
+ | 2: do 3 intro;
+      unfold le_flatEnv;
+      change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+      unfold eq_flatEnv_elem;
+      elim a;
+      change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)])));
+      rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??));
+      rewrite > (eq_to_eqdescelem d d (refl_eq ??));
+      rewrite > H;
+      reflexivity
+ ].
+qed.
+
 (* STRUTTURA MAPPA TRASFORMAZIONE *)
 
-(* elemento: nome + max + cur *)
-inductive maxCur_elem : Type ≝
-MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem.
+(* elemento: nome + cur + max + dimostrazione *)
+inductive maxCur_elem (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝
+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.
 
 (* tipo pubblico *)
-definition aux_trasfMap_type ≝ list maxCur_elem.
+definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
 
 (* getter *)
-definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ].
-definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ].
-definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ].
+definition get_name_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM n _ _ _ ⇒ n ].
+definition get_cur_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ c _ _ ⇒ c ].
+definition get_max_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ _ m _ ⇒ m ].
 
 (* mappa di trasformazione vuota *)
-definition empty_trasfMap ≝ nil maxCur_elem.
+definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
 
 (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
 
 (* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
-let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝
+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 ≝
  match map with
-  [ nil ⇒ dummy
-  | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
-   [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]].
+  [ nil ⇒ None ?
+  | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with
+   [ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]].
+
+(* prossimo nome *)
+definition next_nameId ≝
+λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
+ match get_maxcur_map e fe map str with
+  [ None ⇒ STR_ID str 0
+  | Some maxcur ⇒ STR_ID str (S (get_max_maxCur e fe maxcur))
+  ].
 
-definition get_maxcur_from_map ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.
- match get_maxcur_from_map_aux map str (None ?) with
-  [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ].
+(* nome -> nome + id *)
+definition name_to_nameId ≝
+λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type.
+ match get_maxcur_map e fe map str with
+  [ None ⇒ STR_ID str 0
+  | Some maxcur ⇒ STR_ID str (get_cur_maxCur e fe maxcur)
+  ].
+
+(* NB: se cerco qualcos'altro il risultato e' invariato *)
+axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map.
+(check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+(eqStr_str str str' = false) →
+(check_desc_env (add_desc_env e str' b' desc') str →
+ get_desc_env (add_desc_env e str' b' desc') str =
+ get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)).
+
+(* NB: se cerco cio' che e' appena stato aggiunto, deve essere uguale *)
+axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map.
+(check_desc_env e str →
+ get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+(eqStr_str str str' = true) →
+(check_desc_env (add_desc_env e str' b' desc') str →
+ get_desc_env (add_desc_env e str' b' desc') str =
+ get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))).
+
+axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map.
+ check_desc_env (add_desc_env e str b desc) str →
+  get_desc_env (add_desc_env e str b desc) str =
+  get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0).
+
+(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
+axiom ast_to_astfe_id_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str.
+ check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str).
+
+axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map.
+ check_not_already_def_env e str →
+ check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str).
 
 (* aggiungi/aggiorna descrittore mappa trasformazione *)
-let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝
- match map with
-  [ nil ⇒ match flag with
-    [ true ⇒ []
-    | false ⇒ [MAX_CUR_ELEM str 0 0]
-    ]
-  | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with
-   [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true)
-   | false ⇒ [h]@(add_maxcur_map_aux tl str flag)
-   ]
-  ].
+let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe)
+                           (str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map
+ : aux_trasfMap_type (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) ≝
+match map with
+ [ nil ⇒
+    match flag with
+     [ true ⇒ []
+     | false ⇒
+        [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
+           str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ]
+     ]
+ | cons h tl ⇒ match h with
+  [ MAX_CUR_ELEM str' cur' max' dim' ⇒
+     match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with
+      [ true ⇒ λp:(eqStr_str str' str = true).
+            [ MAX_CUR_ELEM  (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
+                            str' (S max') (S max')
+                            (add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p)
+            ]@(add_maxcur_map_aux e fe tl fMap str b desc true)
+      | false ⇒ λp:(eqStr_str str' str = false).
+             [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc)
+                            str' cur' max'
+                            (add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p)
+             ]@(add_maxcur_map_aux e fe tl fMap str b desc flag)
+      ] (refl_eq ? (eqStr_str str' str))
+  ]
+ ].
 
 definition add_maxcur_map ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false.
+λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type.
+add_maxcur_map_aux e fe map fMap str b desc false.
 
-(* nome -> nome + id *)
-definition name_to_nameId ≝
-λmap:aux_trasfMap_type.λstr:aux_str_type.
- STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)).
+(* composizione di funzioni generata da una lista di nome x const x tipo *)
+definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type).
 
-(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *)
-let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝
-match e with
- [ nil ⇒ dummy
- | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with
-  [ true ⇒ Some ? (get_desc_flatVar h)
-  | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]].
+let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝
+ match trasf with
+  [ nil ⇒ (λx.x)
+  | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+  ].
 
-definition get_desc_from_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_from_flatEnv_aux e str (None ?) with
-  [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
+lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c.
+ ∃b.build_trasfEnv trsf (c§§a) = (b§§a).
+ intros 2;
+ elim trsf;
+  [ simplify; exists; [apply c | reflexivity]
+  | simplify; apply H; ]
+qed.
 
-(* aggiungi descrittore ad ambiente *)
-definition add_desc_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
- e@[ VAR_FLAT_ELEM str (DESC_ELEM b t) ].
+lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e.
+ intros;
+ change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e);
+ cases (build_trasfEnv_exists_aux e trsf []);
+ rewrite > H;
+ reflexivity.
+qed.
 
-(* snapshot della mappa trasformazione *)
-let rec build_snapshot (map:aux_trasfMap_type) on map ≝
+(* NB: leave ... enter e' equivalente a e originale *)
+lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+  get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env e str →
+  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite > (eq_enter_leave e trsf);
+ intros;
+ apply H;
+ apply H1.
+qed.
+
+let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+                                (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝
  match map with
   [ nil ⇒ []
-  | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl)
-  ].
+  | cons h tl ⇒ match h with
+   [ MAX_CUR_ELEM str cur max dim ⇒
+    [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)
+   ]].
+
+lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf.
+ (check_desc_env e str →
+  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str →
+  get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 5;
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?);
+ rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?);
+ intros;
+ apply H;
+ apply H1.
+qed.
 
-(* uscita da un blocco, rollback di cur in mappa di trasformazione *)
-let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝
- match snap with
-  [ nil ⇒ None ?
-  | cons h tl ⇒ match strCmp_str str (get_name_strId h) with
-   [ true ⇒ Some ? (get_id_strId h)
-   | false ⇒ find_in_snapshot tl str
-   ]
-  ].
+let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type)
+                                (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝
+ match map with
+  [ nil ⇒ []
+  | cons h tl ⇒ match h with
+   [ MAX_CUR_ELEM str cur max dim ⇒
+    [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)
+   ]].
+
+(* NB: enter non cambia fe *)
+lemma retype_e_to_enter_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (enter_env e) str →
+  get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+ intros 6;
+ rewrite > H;
+ [ reflexivity
+ | apply H1
+ ].
+qed.
+
+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 ≝
+ match map with
+  [ nil ⇒ []
+  | cons h tl ⇒ match h with
+   [ MAX_CUR_ELEM str cur max dim ⇒
+    [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)
+   ]].
+
+(* NB: leave non cambia fe *)
+axiom retype_e_to_leave_aux : ∀e,fe,str,cur.
+ (check_desc_env e str →
+  get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) →
+ (check_desc_env (leave_env e) str →
+  get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)).
+
+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 ≝
+ match map with
+  [ nil ⇒ []
+  | cons h tl ⇒ match h with
+   [ MAX_CUR_ELEM str cur max dim ⇒
+    [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)
+   ]].
 
-let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝
+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')
+ (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
  match map with
-  [ nil ⇒ empty_trasfMap
-  | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with
-   [ None ⇒ [h]
-   | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ]
-   ]@(rollback_map tl snap)
+  [ nil ⇒ empty_trasfMap e fe'
+  | cons h tl ⇒ 
+     match get_maxcur_map e fe snap (get_name_maxCur ?? h) with
+   [ None ⇒ retype_enter_leave_to_e e fe' trsf [h]
+   | Some new ⇒
+      [ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new)
+        (get_max_maxCur ?? h) (False_rect ? daemon) ]
+   ] @ rollback_map e fe fe' trsf tl snap
   ].
 
 (* sequenza di utilizzo:
@@ -169,45 +419,45 @@ let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map 
 (* mini test
 definition pippo ≝ [ ch_P ].
 definition pluto ≝ [ ch_Q ].
-definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
-definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2).
-definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
-definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2).
-
-definition map1 ≝ add_maxcur_map empty_trasfMap pippo.
-definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1.
-definition map2 ≝ add_maxcur_map map1 pluto.
-definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1.
-
-definition snap1 ≝ build_snapshot map2.
-
-definition map3 ≝ add_maxcur_map map2 pippo.
-definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2.
-definition map4 ≝ add_maxcur_map map3 pluto.
-definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2.
-
-definition snap2 ≝ build_snapshot map4.
-
-definition map5 ≝ add_maxcur_map map4 pippo.
-definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3.
-definition map6 ≝ add_maxcur_map map5 pluto.
-definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3.
-
-definition map7 ≝ rollback_map map6 snap2.
-
-definition map8 ≝ rollback_map map7 snap1.
-
-lemma checkenv : None ? = Some ? env6.
-normalize; elim daemon.
-qed.
-
-lemma checkmap : None ? = Some ? map8.
-normalize; elim daemon.
-qed.
-
-lemma checksnap : None ? = Some ? snap2.
-normalize; elim daemon.
-qed.
+definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
+definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8).
+definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16).
+definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32).
+
+definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1.
+definition env1 ≝ add_desc_env empty_env pippo false pippodesc1.
+definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1.
+definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1.
+definition env2 ≝ add_desc_env env1 pluto false plutodesc1.
+definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1.
+
+definition env2' ≝ enter_env env2.
+definition map2' ≝ retype_e_to_enter env2 fenv2 map2.
+
+definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2.
+definition env3 ≝ add_desc_env env2' pippo true pippodesc2.
+definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2.
+definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2.
+definition env4 ≝ add_desc_env env3 pluto true plutodesc2.
+definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2.
+
+definition env4' ≝ enter_env env4.
+definition map4' ≝ retype_e_to_enter env4 fenv4 map4.
+
+definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3.
+definition env5 ≝ add_desc_env env4' pippo false pippodesc3.
+definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3.
+definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3.
+definition env6 ≝ add_desc_env env5 pluto false plutodesc3.
+definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3.
+
+definition map6' ≝ retype_e_to_leave env6 fenv6 map6.
+
+definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4.
+
+definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
+
+definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2.
 *)