X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fenv_to_flatenv.ma;h=1339f4f9d3aeceda13f57533bf6c26fbeea77bdb;hb=57003fb8f7c54191f61585b9b7f067c3aab666e4;hp=bfa77213a07ae3b255c0dba5675fd26fc5f5183f;hpb=05e6e4771934d95be8b4cffcc87eeb7b27250536;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 bfa77213a..1339f4f9d 100755
--- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
+++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma
@@ -20,245 +20,763 @@
 (* ********************************************************************** *)
 
 include "compiler/environment.ma".
+include "compiler/ast_tree.ma".
 
 (* ********************** *)
 (* GESTIONE AMBIENTE FLAT *)
 (* ********************** *)
 
-(* STRUTTURA AMBIENTE FLAT *)
+(* ambiente flat *)
+inductive var_flatElem : Type ≝
+VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
 
-(* elemento: name + desc *)
-inductive flatVar_elem : Type ≝
-VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem.
+definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
+definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
 
-(* tipo pubblico *)
-definition aux_flatEnv_type ≝ list flatVar_elem.
+definition aux_flatEnv_type ≝ list var_flatElem.
 
-(* getter *)
-definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
-definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
+definition empty_flatEnv ≝ nil var_flatElem.
 
-(* ambiente vuoto *)
-definition empty_flatEnv ≝ nil flatVar_elem.
+(* mappa: nome + max + cur *)
+inductive map_list : nat → Type ≝
+  map_nil: map_list O
+| map_cons: ∀n.option nat → map_list n → map_list (S n).
 
-(* 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 strCmp_strId str (get_nameId_flatVar h) with
-  [ true ⇒ Some ? (get_desc_flatVar h)
-  | false ⇒ get_desc_flatEnv_aux tl str ]].
+definition defined_mapList ≝
+λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ].
 
-definition get_desc_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.
- match get_desc_flatEnv_aux e str with
+definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+  match l
+   return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
+  with
+   [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+   | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t
+   ] p in value.
+
+definition get_first_mapList : Πd.map_list d → ? → option nat ≝
+λd.λl:map_list d.λp:defined_mapList ? l.
+ let value ≝
+  match l
+   return λX.λY:map_list X.defined_mapList X Y → option nat
+  with
+   [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
+   | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h
+   ] p in value.
+
+inductive map_elem (d:nat) : Type ≝
+MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
+
+definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
+definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
+definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
+
+definition aux_map_type ≝ λd.list (map_elem d).
+
+definition empty_map ≝ nil (map_elem O).
+
+lemma defined_mapList_S_to_true :
+∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
+ intros;
+ inversion l;
+  [ intros; destruct H
+  | intros; simplify; reflexivity
+  ]
+qed.
+
+lemma defined_mapList_get :
+ ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
+ intros 2;
+ rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
+ apply I.
+qed.
+
+(* get_id *)
+let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
+ match map with
+  [ nil ⇒ None ?
+  | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+                [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)
+                | false ⇒ get_id_map_aux d t name
+                ]
+  ].
+
+definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* get_max *)
+let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
+ match map with
+  [ nil ⇒ None ?
+  | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+                [ true ⇒ Some ? (get_max_mapElem d h)
+                | false ⇒ get_max_map_aux d t name
+                ]
+  ].
+
+definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
+
+(* check_id *)
+definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
+
+definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
+
+lemma checkbidmap_to_checkidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+  checkb_id_map d map name = true → check_id_map d map name.
+ unfold checkb_id_map;
+ unfold check_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; destruct H
+ | simplify; intros; apply I
+ ].
+qed.
+
+definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
+ match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbidmap_to_checknotidmap :
+ ∀d.∀map:aux_map_type d.∀name.
+  checknotb_id_map d map name = true → checknot_id_map d map name.
+ unfold checknotb_id_map;
+ unfold checknot_id_map;
+ intros 3;
+ elim (get_id_map_aux d map name) 0;
+ [ simplify; intro; apply I
+ | simplify; intros; destruct H
+ ].
+qed.
+
+(* get_desc *)
+let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
+ match fe with
+  [ nil ⇒ None ?
+  | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
+               [ true ⇒ Some ? (get_desc_flatVar h)
+               | false ⇒ get_desc_flatEnv_aux t name
+               ]
+  ].
+
+definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe 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 check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe 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 ].
+definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
 
-lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str.
+lemma checkbdescflatenv_to_checkdescflatenv :
+ ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
  unfold checkb_desc_flatEnv;
  unfold check_desc_flatEnv;
- intros;
- letin K ≝ (get_desc_flatEnv_aux e str);
- elim K;
- [ normalize; autobatch |
-   normalize; autobatch ]
+ intros 2;
+ elim (get_desc_flatEnv_aux fe str) 0;
+ [ simplify; intro; destruct H
+ | simplify; intros; apply I
+ ].
+qed.
+
+definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
+
+definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
+ match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
+
+lemma checknotbdescflatenv_to_checknotdescflatenv :
+ ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
+ unfold checknotb_desc_flatEnv;
+ unfold checknot_desc_flatEnv;
+ intros 2;
+ elim (get_desc_flatEnv_aux fe str) 0;
+ [ simplify; intro; apply I
+ | simplify; intros; destruct H
+ ].
 qed.
 
-(* aggiungi descrittore ad ambiente: in testa *)
-definition add_desc_flatEnv ≝
-λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type.
- (VAR_FLAT_ELEM str (DESC_ELEM b t))::e.
+(* 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.
 
-(* STRUTTURA MAPPA TRASFORMAZIONE *)
+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.
 
-(* 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.
+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 eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
+ intros 3;
+ rewrite < H;
+ elim e1;
+ [ reflexivity
+ | simplify;
+   rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+   rewrite > H1;
+   reflexivity
+ ].
+qed.
 
-(* tipo pubblico *)
-definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe).
+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 le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
+ intros;
+ elim fe;
+ [ simplify;
+   reflexivity
+ | simplify;
+   rewrite > (eq_to_eqflatenv a a (refl_eq ??));
+   rewrite > H;
+   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_name_flatVar a));
+   [ simplify; intro; apply H3
+   | simplify; apply H2
+   ]
+ ].
+qed.
 
-(* getter *)
-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 ].
+lemma leflatenv_to_get : ∀fe,fe',str.
+ (le_flatEnv fe fe' = true) →
+ (check_desc_flatEnv fe str) →
+ (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
+ intros 4;
+ cases (leflatenv_to_le fe fe' H);
+ rewrite < H1;
+ elim fe 0;
+ [ intro;
+   simplify in H2:(%);
+   elim H2
+ | simplify;
+   intros 2;
+   cases (eqStrId_str str (get_name_flatVar a));
+   [ simplify;
+     intros;
+     reflexivity
+   | simplify;
+     unfold check_desc_flatEnv;
+     unfold get_desc_flatEnv;
+     cases (get_desc_flatEnv_aux l str);
+     [ simplify; intros; elim H3
+     | simplify; intros; rewrite < (H2 H3); reflexivity
+     ]
+   ]
+ ].
+qed.
 
-(* mappa di trasformazione vuota *)
-definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe).
+(* controllo di coerenza env <-> map *)
+let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝
+ match e with
+  [ env_nil h ⇒ λf.f h
+  | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h)
+  ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]).
 
-(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *)
+let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
+ match map with
+  [ map_nil ⇒ eqb res O
+  | map_cons d' h t ⇒ match eqb res O with
+   [ true ⇒ match h with
+    [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ]
+   | false ⇒ match h with
+    [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ]
+   ]
+  ].
 
-(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *)
-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 ≝
+(* esprimendolo in lingua umana il vincolo che controlla e':
+   ∀name ϵ map.
+    la map_list "cur" deve avere la seguente struttura
+     - Some _ ; ... ; Some _ ; None ; ... None
+     - il numero di Some _ deve essere pari a (d + 1 - x) con x
+       ricavato scandendo in avanti tutti gli ambienti e
+       numerando quanti ambienti CONSECUTIVI non contengono la definizione di name
+
+   ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
+       no si no si NO NO
+       quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2
+       sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti
+       Some _ ; Some _ ; Some _ ; Some _ ; None ; None
+       cioe' 5+1-2 Some seguiti da solo None
+
+   NB: e' solo meta' perche' cosi' si asserisce map ≤ env
+   
+*)
+let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
  match map with
-  [ nil ⇒ None ?
-  | cons h tl ⇒ match strCmp_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))
+  [ nil ⇒ true
+  | cons h t ⇒ (check_map_env_align_auxMap (S d) (get_cur_mapElem d h) (d + 1 - (check_map_env_align_auxEnv d e (get_name_mapElem d h) O)))⊗
+               (check_map_env_align d e t)
   ].
 
-(* 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)
+let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
+ match le with
+  [ nil ⇒ true
+  | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with
+   [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ]
+  ].
+
+(* esprimendolo in lingua umana il vincolo che controlla e':
+   ∀name ϵ e.name ϵ map
+   
+   NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
+*)
+let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
+ match e with
+  [ env_nil h ⇒ check_env_map_align_aux dm map h
+  | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map)
+  ].
+
+(* invariante *)
+definition env_to_flatEnv_inv ≝
+ λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
+  ∀str.
+   check_desc_env d e str →
+    check_env_map_align d e d map = true ∧ check_map_env_align d e map = true ∧
+    check_id_map d map str ∧
+    check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
+    get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str)).
+
+lemma inv_to_checkdescflatenv :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+ env_to_flatEnv_inv d e map fe →
+ (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
+ intros 7;
+ unfold env_to_flatEnv_inv in H:(%); 
+ lapply (H str H1);
+ apply (proj2 ?? (proj1 ?? Hletin));
+qed.
+
+lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
+ unfold env_to_flatEnv_inv;
+ unfold empty_env;
+ unfold empty_map;
+ unfold empty_flatEnv;
+ simplify;
+ intros;
+ elim H.
+qed.
+
+lemma leflatenv_to_inv :
+ ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
+  le_flatEnv fe fe' = true →
+  env_to_flatEnv_inv d e map fe →
+  env_to_flatEnv_inv d e map fe'.
+ intros 6;
+ unfold env_to_flatEnv_inv;
+ intros;
+ split;
+ [ split;
+   [ lapply (H1 str H2);
+     apply (proj1 ?? (proj1 ?? Hletin))
+   | lapply (H1 str H2);
+     apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
+   ]
+ | lapply (H1 str H2);
+   rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
+   apply (proj2 ?? Hletin)
+ ].
+qed.
+
+lemma leflatenv_trans :
+ ∀fe,fe',fe''.
+  le_flatEnv fe fe' = true →
+  le_flatEnv fe' fe'' = true →
+  le_flatEnv fe fe'' = true.
+ intros 4;
+ cases (leflatenv_to_le fe ? H);
+ rewrite < H1;
+ intro;
+ cases (leflatenv_to_le (fe@x) fe'' H2);
+ rewrite < H3;
+ rewrite > associative_append;
+ apply (le_to_leflatenv fe ?).
+qed.
+
+(* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
+let rec enter_map d (map:aux_map_type d) on map ≝
+ match map with
+  [ nil ⇒ []
+  | cons h t ⇒
+   (MAP_ELEM (S d)
+             (get_name_mapElem d h)
+             (get_max_mapElem d h)
+             (map_cons (S d)
+                       (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
+                       (get_cur_mapElem d h))
+   )::(enter_map d t)
   ].
 
-(* 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)) →
-(strCmp_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)) →
-(strCmp_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))).
-
-(* aggiungi/aggiorna descrittore mappa trasformazione *)
-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 O O (False_rect ? daemon) ]
+lemma getidmap_to_enter :
+ ∀d.∀m:aux_map_type d.∀str.
+  get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
+ intros;
+ elim m;
+ [ simplify; reflexivity
+ | simplify; rewrite > H; reflexivity
+ ]
+qed.
+
+lemma checkdescenter_to_checkdesc :
+ ∀d.∀e:aux_env_type d.∀str.
+  check_desc_env (S d) (enter_env d e) str →
+  check_desc_env d e str.
+ intros;
+ unfold enter_env in H:(%);
+ simplify in H:(%);
+ apply H.
+qed.
+
+lemma checkenvmapalign_to_enter :
+ ∀de.∀e:aux_env_type de.∀dm.∀m:aux_map_type dm.
+  check_env_map_align de e dm m =
+  check_env_map_align (S de) (enter_env de e) (S dm) (enter_map dm m).
+ intros 4;
+ unfold enter_env;
+ simplify;
+ elim e 0;
+ [ simplify;
+   intro;
+   elim l 0;
+   [ simplify;
+     reflexivity
+   | simplify;
+     intros;
+     rewrite > (getidmap_to_enter ???);
+     rewrite < H;
+     cases (get_id_map_aux dm m (get_name_var a));
+     [ simplify;
+       reflexivity
+     | simplify;
+       rewrite > H;
+       reflexivity
      ]
- | cons h tl ⇒ match h with
-  [ MAX_CUR_ELEM str' cur' max' dim' ⇒
-     match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with
-      [ true ⇒ λp:(strCmp_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:(strCmp_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 ? (strCmp_str str' str))
-  ]
+   ]
+ | simplify;
+   intros 2;
+   elim l 0;
+   [ simplify;
+     intros;
+     apply H
+   | intros;
+     simplify;
+     rewrite > (getidmap_to_enter ???);
+     cases (get_id_map_aux dm m (get_name_var a));
+     [ simplify;
+       reflexivity
+     | simplify;
+       apply (H e1 H1)
+     ]
+   ]
  ].
+qed.
 
-definition add_maxcur_map ≝
-λ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.
+lemma env_map_flatEnv_enter_aux : 
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+  env_to_flatEnv_inv d e map fe →
+  env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
+ unfold env_to_flatEnv_inv;
+ intros;
+ split;
+ [ split;
+   [ split;
+     [ split;
+       [ rewrite < (checkenvmapalign_to_enter ???); 
+         apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))))
+       | (* TO DO !!! *) elim daemon
+       ]
+     | unfold check_id_map;
+       rewrite > (getidmap_to_enter ???);
+       apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))
+     ]
+   | unfold get_id_map;
+     rewrite > (getidmap_to_enter ???);
+     apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))
+   ]
+ | unfold get_id_map;
+   rewrite > (getidmap_to_enter ???);
+   apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1)))
+ ].
+qed.
 
-(* NB: leave ... enter e' equivalente a e originale *)
-axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe.
-(* NB: enter non cambia fe *)
-axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe.
-(* NB: leave non cambia fe *)
-axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe.
+(* aggiungi descrittore *)
+let rec new_map_elem_from_depth_aux (d:nat) on d ≝
+ match d
+  return λd.map_list d
+ with
+  [ O ⇒ map_nil
+  | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
+  ].
 
-let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type → aux_env_type) (map:aux_trasfMap_type (leave_env (f (enter_env e))) fe')
- (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝
+let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
  match map with
-  [ 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' f [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' f tl snap
+  [ nil ⇒ []
+  | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
+                [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)))
+                | false ⇒ h
+                ]::(new_max_map_aux d t name max) 
   ].
 
-(* sequenza di utilizzo:
-
-[BLOCCO ESTERNO]
-
-|DICHIARAZIONE "pippo":
-| -) MAP1 <- add_maxcur_map MAP0 "pippo"
-| -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC
-|
-|ACCESSO "pippo":
-| -) name_to_nameId MAP1 "pippo"
-|
-|PREPARAZIONE ENTRATA BLOCCO INTERNO:
-| -) SNAP <- build_snapshot MAP1
-
-  |[BLOCCO INTERNO]
-  |
-  |DICHIARAZIONE "pippo":
-  |  -) MAP2 <- add_maxcur_map MAP1 "pippo"
-  |  -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC
-  |
-  |ACCESSO "pippo":
-  | -) name_to_nameId MAP2 "pippo"
-  |
-  |PREPARAZIONE USCITA BLOCCO INTERNO:
-  | -) MAP3 <- rollback_map MAP2 SNAP
-
-| ...
-*)
+definition add_desc_env_flatEnv_map ≝
+λd.λmap:aux_map_type d.λstr.
+ match get_max_map_aux d map str with
+  [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
+  | Some x ⇒ new_max_map_aux d map str (S x)
+  ].
 
-(* mini test 
-definition pippo ≝ [ ch_P ].
-definition pluto ≝ [ ch_Q ].
-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 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4.
-
-definition map7' ≝ retype_e_to_leave env4 fenv6 map7.
-
-definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2.
-*)
+definition add_desc_env_flatEnv_fe ≝
+λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
+ fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
+                    (DESC_ELEM c desc) ].
+
+let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
+ match trsf with
+  [ nil ⇒ (λx.x)
+  | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
+  ].
+
+let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
+ Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
+ match trsf with
+  [ nil ⇒ (λx.x)
+  | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
+                   (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
+                            (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
+  ].
+
+lemma env_map_flatEnv_add_aux : 
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
+  env_to_flatEnv_inv d e map fe →
+  env_to_flatEnv_inv d
+                     (build_trasfEnv_env d trsf e)
+                     (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
+                     (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ (* TO DO !!! *) elim daemon.
+qed.
+
+lemma env_map_flatEnv_addNil_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
+  env_to_flatEnv_inv d e map fe →
+  env_to_flatEnv_inv d
+                     (build_trasfEnv_env d [] e)
+                     (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
+                     (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
+ intros;
+ simplify;
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addSingle_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
+  env_to_flatEnv_inv d e map fe →
+  env_to_flatEnv_inv d
+                     (add_desc_env d e name const desc)
+                     (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
+                     (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
+ intros;
+ apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
+ apply H.
+qed.
+
+lemma env_map_flatEnv_addJoin_aux :
+ ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
+  env_to_flatEnv_inv d
+                     (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
+                     map fe →
+  env_to_flatEnv_inv d
+                     (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
+                     map fe.
+ intros;
+ simplify;
+ apply H.
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_al :
+ ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
+  snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
+  a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
+ intro;
+ elim trsf;
+ [ simplify; reflexivity
+ | simplify;
+   elim a;
+   simplify;
+   rewrite > (H ????);
+   reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe_l :
+ ∀trsf.∀d.∀m:aux_map_type d.∀l.
+  snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
+  l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
+ intros;
+ elim l;
+ [ simplify; reflexivity
+ | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
+   rewrite > H;
+   reflexivity
+ ].
+qed.
+
+lemma env_map_flatEnv_add_aux_fe :
+ ∀d.∀map:aux_map_type d.∀fe,trsf.
+  ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
+ intros 3;
+ elim fe 0;
+ [ simplify;
+   intro;
+   exists;
+   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+   | reflexivity
+   ]
+ | intros 4;
+   exists;
+   [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
+   | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
+     rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
+     rewrite < (cons_append_commute ????);
+     reflexivity
+   ]
+ ].
+qed.
+
+lemma buildtrasfenvadd_to_le :
+ ∀d.∀m:aux_map_type d.∀fe,trsf.
+  le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
+ intros 4;
+  cases (env_map_flatEnv_add_aux_fe d m fe trsf);
+ rewrite < H;
+ rewrite > (le_to_leflatenv fe x);
+ reflexivity.
+qed.
+
+(* leave: elimina la testa (il "cur" corrente) *)
+let rec leave_map d (map:aux_map_type (S d)) on map ≝
+ match map with
+  [ nil ⇒ []
+  | cons h t ⇒
+   (MAP_ELEM d
+             (get_name_mapElem (S d) h)
+             (get_max_mapElem (S d) h)
+             (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
+   )::(leave_map d t)
+  ].
+
+lemma leave_add_enter_env_aux :
+ ∀d.∀a:aux_env_type d.∀trsf.∀c.
+  ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
+ intros 3;
+ elim trsf;
+ [ simplify; exists; [ apply c | reflexivity ]
+ | simplify; apply H
+ ].
+qed.
+
+lemma leave_add_enter_env :
+ ∀d.∀e:aux_env_type d.∀trsf.
+  leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
+ intros;
+ unfold enter_env;
+ lapply (leave_add_enter_env_aux d e trsf []);
+ cases Hletin;
+ rewrite > H;
+ simplify;
+ reflexivity.
+qed.
+
+lemma env_map_flatEnv_leave_aux :
+ ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
+  env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
+  env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
+ (* TO DO !!! *) elim daemon.
+qed.
+
+lemma newid_from_init :
+ ∀d.∀e:aux_env_type d.∀name,const,desc.
+  ast_id d (add_desc_env d e name const desc) const desc.
+ intros;
+ lapply (AST_ID d (add_desc_env d e name const desc) name ?);
+ [ elim e;
+   simplify;
+   rewrite > (eq_to_eqstr ?? (refl_eq ??));
+   simplify;
+   apply I
+ | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
+        desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
+   [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
+     rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
+     apply Hletin
+   | split;
+     [ elim e;
+       simplify;
+       rewrite > (eq_to_eqstr ?? (refl_eq ??));
+       simplify;
+       reflexivity
+     | elim e;
+       simplify;
+       rewrite > (eq_to_eqstr ?? (refl_eq ??));
+       simplify;
+       reflexivity
+     ]
+   ]
+ ].
+qed.