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

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
index 054aeedc2..d6eadfdb8 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -20,65 +20,118 @@
 (* ********************************************************************** *)
 
 include "compiler/astfe_tree.ma".
+include "compiler/sigma.ma".
 
 (* ************************ *)
 (* PASSO 2 : da AST a ASTFE *)
 (* ************************ *)
 
 (* operatore di cast *)
-definition ast_to_astfe_expr_check : Πt.astfe_expr t → Πt'.option (astfe_expr t') ≝
-λt:ast_type.λast:astfe_expr t.λt':ast_type.
+definition ast_to_astfe_expr_check : Πfe.Πt.astfe_expr fe t → Πt'.option (astfe_expr fe t') ≝
+λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_expr fe t.λt':ast_type.
  match eq_ast_type t t'
   return λx.(eq_ast_type t t' = x) → ?
  with
   [ true ⇒ λp:(eq_ast_type t t' = true).
-   Some ? (eq_rect ? t (λt.astfe_expr t) ast t' (eqasttype_to_eq ?? p))
+   Some ? (eq_rect ? t (λt.astfe_expr fe t) ast t' (eqasttype_to_eq ?? p))
   | false ⇒ λp:(eq_ast_type t t' = false).None ?
   ] (refl_eq ? (eq_ast_type t t')).
 
-definition ast_to_astfe_init_check : Πt.astfe_init t → Πt'.option (astfe_init t') ≝
-λt:ast_type.λast:astfe_init t.λt':ast_type.
+definition ast_to_astfe_init_check : Πfe.Πt.astfe_init fe t → Πt'.option (astfe_init fe t') ≝
+λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λt':ast_type.
  match eq_ast_type t t'
   return λx.(eq_ast_type t t' = x) → ?
  with
   [ true ⇒ λp:(eq_ast_type t t' = true).
-   Some ? (eq_rect ? t (λt.astfe_init t) ast t' (eqasttype_to_eq ?? p))
+   Some ? (eq_rect ? t (λt.astfe_init fe t) ast t' (eqasttype_to_eq ?? p))
   | false ⇒ λp:(eq_ast_type t t' = false).None ?
   ] (refl_eq ? (eq_ast_type t t')).
 
-definition ast_to_astfe_var_checkb : Πb.Πt.astfe_var b t → Πb'.option (astfe_var b' t) ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.
+definition ast_to_astfe_var_checkb : Πfe.Πb.Πt.astfe_var fe b t → Πb'.option (astfe_var fe b' t) ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.
  match eq_bool b b'
   return λx.(eq_bool b b' = x) → ?
  with
   [ true ⇒ λp:(eq_bool b b' = true).
-   Some ? (eq_rect ? b (λb.astfe_var b t) ast b' (eqbool_to_eq ?? p))
+   Some ? (eq_rect ? b (λb.astfe_var fe b t) ast b' (eqbool_to_eq ?? p))
   | false ⇒ λp:(eq_bool b b' = false).None ?
   ] (refl_eq ? (eq_bool b b')).
 
-definition ast_to_astfe_var_checkt : Πb.Πt.astfe_var b t → Πt'.option (astfe_var b t') ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λt':ast_type.
+definition ast_to_astfe_var_checkt : Πfe.Πb.Πt.astfe_var fe b t → Πt'.option (astfe_var fe b t') ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λt':ast_type.
  match eq_ast_type t t'
   return λx.(eq_ast_type t t' = x) → ?
  with
   [ true ⇒ λp:(eq_ast_type t t' = true).
-   Some ? (eq_rect ? t (λt.astfe_var b t) ast t' (eqasttype_to_eq ?? p))
+   Some ? (eq_rect ? t (λt.astfe_var fe b t) ast t' (eqasttype_to_eq ?? p))
   | false ⇒ λp:(eq_ast_type t t' = false).None ?
   ] (refl_eq ? (eq_ast_type t t')).
 
-definition ast_to_astfe_var_check : Πb.Πt.astfe_var b t → Πb'.Πt'.option (astfe_var b' t') ≝
-λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.λt':ast_type.
- opt_map ?? (ast_to_astfe_var_checkb b t ast b')
-  (λres.opt_map ?? (ast_to_astfe_var_checkt b' t res t')
+definition ast_to_astfe_var_check : Πfe.Πb.Πt.astfe_var fe b t → Πb'.Πt'.option (astfe_var fe b' t') ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.λt':ast_type.
+ opt_map ?? (ast_to_astfe_var_checkb fe b t ast b')
+  (λres.opt_map ?? (ast_to_astfe_var_checkt fe b' t res t')
+   (λres'.Some ? res')).
+
+definition ast_to_astfe_id_checkb : Πfe.Πb.Πt.astfe_id fe b t → Πb'.option (astfe_id fe b' t) ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.
+ match eq_bool b b'
+  return λx.(eq_bool b b' = x) → ?
+ with
+  [ true ⇒ λp:(eq_bool b b' = true).
+   Some ? (eq_rect ? b (λb.astfe_id fe b t) ast b' (eqbool_to_eq ?? p))
+  | false ⇒ λp:(eq_bool b b' = false).None ?
+  ] (refl_eq ? (eq_bool b b')).
+
+definition ast_to_astfe_id_checkt : Πfe.Πb.Πt.astfe_id fe b t → Πt'.option (astfe_id fe b t') ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λt':ast_type.
+ match eq_ast_type t t'
+  return λx.(eq_ast_type t t' = x) → ?
+ with
+  [ true ⇒ λp:(eq_ast_type t t' = true).
+   Some ? (eq_rect ? t (λt.astfe_id fe b t) ast t' (eqasttype_to_eq ?? p))
+  | false ⇒ λp:(eq_ast_type t t' = false).None ?
+  ] (refl_eq ? (eq_ast_type t t')).
+
+definition ast_to_astfe_id_check : Πfe.Πb.Πt.astfe_id fe b t → Πb'.Πt'.option (astfe_id fe b' t') ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.λt':ast_type.
+ opt_map ?? (ast_to_astfe_id_checkb fe b t ast b')
+  (λres.opt_map ?? (ast_to_astfe_id_checkt fe b' t res t')
    (λres'.Some ? res')).
 
 (*
  AST_ID: ∀str:aux_str_type.
          (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
 *)
-definition ast_to_astfe_id ≝
-λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λmap:aux_trasfMap_type.match ast with
- [ AST_ID str _ ⇒ ASTFE_ID (name_to_nameId map str) b t ].
+definition get_name_ast_id ≝
+λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.
+ match ast with [ AST_ID s _ ⇒ s ].
+
+definition ast_to_astfe_id :
+ Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
+  Πmap:aux_trasfMap_type e fe.
+   astfe_id fe
+    (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
+    (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) ≝
+λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
+ ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast))
+             (ast_to_astfe_id_aux e fe map (get_name_ast_id e b t ast)
+                                           (ast_id_ind e
+                                            (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:ast_id e Hbeta3 Hbeta2.check_desc_env e (get_name_ast_id e Hbeta3 Hbeta2 Hbeta1))
+                                            (λa:aux_str_type.λH:check_desc_env e a.H) b t ast)).
+
+definition get_name_astfe_id ≝ λfe,b,t.λast:astfe_id fe b t.match ast with [ ASTFE_ID n _ ⇒ n ].
+
+definition retype_id
+: Πfe:aux_flatEnv_type.Πb:bool.Πt:ast_type.Πast:astfe_id fe b t.Πfe':aux_flatEnv_type.le_flatEnv fe fe' = true →
+  astfe_id fe'
+    (get_const_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast)))
+    (get_type_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) ≝
+λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ ASTFE_ID fe' (get_name_astfe_id fe b t ast)
+              (leflatenv_to_check fe fe' (get_name_astfe_id fe b t ast) dim (astfe_id_ind fe
+                                                                             (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:astfe_id fe Hbeta3 Hbeta2.check_desc_flatEnv fe (get_name_astfe_id fe Hbeta3 Hbeta2 Hbeta1))
+                                                                             (λa:aux_strId_type.λH:check_desc_flatEnv fe a.H) b t ast)).
 
 (*
  AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
@@ -128,94 +181,94 @@ definition ast_to_astfe_id ≝
  AST_EXPR_ID: ∀b:bool.∀t:ast_type.
               ast_var e b t → ast_expr e t
 *)
-let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (map:aux_trasfMap_type) on ast : option (astfe_expr t) ≝
+let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_expr fe t) ≝
  match ast with
-  [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 val) t
-  | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 val) t
-  | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 val) t
+  [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
+  | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
+  | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
 
   | AST_EXPR_NEG bType subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG bType res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
   | AST_EXPR_NOT bType subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT bType res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
   | AST_EXPR_COM bType subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_COM bType res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
 
   | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
   | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
   | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
   | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
   | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
   | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
 
   | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
   | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
   | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
   | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
   | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
   | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
-    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
-     (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ bType res1 res2) t))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
+    (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
+     (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
 
   | AST_EXPR_B8toW16 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
   | AST_EXPR_B8toW32 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
   | AST_EXPR_W16toB8 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
   | AST_EXPR_W16toW32 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
   | AST_EXPR_W32toB8 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
   | AST_EXPR_W32toW16 subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
-    (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 res) t)
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
+    (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
 
   | AST_EXPR_ID b subType var ⇒
-   opt_map ?? (ast_to_astfe_var e b subType var map)
-    (λres.ast_to_astfe_expr_check subType (ASTFE_EXPR_ID b subType res) t)
+   opt_map ?? (ast_to_astfe_var e b subType var fe map)
+    (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
   ]
 (*
  AST_VAR_ID: ∀b:bool.∀t:ast_type.
@@ -225,28 +278,141 @@ let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (map:
  AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
                  ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
 *)
-and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (map:aux_trasfMap_type) on ast : option (astfe_var b t) ≝
+and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_var fe b t) ≝
  match ast with
-  [ AST_VAR_ID subB subType subId ⇒ ast_to_astfe_var_check subB subType (ASTFE_VAR_ID subB subType (ast_to_astfe_id e subB subType subId map)) b t
+  [ AST_VAR_ID subB subType subId ⇒
+   opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType)
+    (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t)
 
   | AST_VAR_ARRAY subB subType dim var expr ⇒
-   opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var map)
-    (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr map)
-     (λresExpr.ast_to_astfe_var_check subB subType (ASTFE_VAR_ARRAY subB subType dim resVar resExpr) b t))
+   opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map)
+    (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map)
+     (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t))
 
   | AST_VAR_STRUCT subB nelSubType field var _ ⇒
-   opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var map)
-    (λres.ast_to_astfe_var_check subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT subB nelSubType field res) b t)
+   opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map)
+    (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t)
   ]
 (*
  AST_BASE_EXPR: ∀t:ast_base_type.
                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
 *)
-and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (map:aux_trasfMap_type) on ast : option astfe_base_expr ≝
+and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_base_expr fe) ≝
  match ast with
   [ AST_BASE_EXPR bType subExpr ⇒
-   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
-    (λres.Some ? (ASTFE_BASE_EXPR bType res))
+   opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
+    (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
+  ].
+
+let rec retype_expr (fe:aux_flatEnv_type) (t:ast_type) (ast:astfe_expr fe t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_expr fe' t) ≝
+ match ast with
+  [ ASTFE_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' val) t
+  | ASTFE_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe' val) t
+  | ASTFE_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe' val) t
+
+  | ASTFE_EXPR_NEG bType subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe' bType res) t)
+  | ASTFE_EXPR_NOT bType subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe' bType res) t)
+  | ASTFE_EXPR_COM bType subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe' bType res) t)
+
+  | ASTFE_EXPR_ADD bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe' bType res1 res2) t))
+  | ASTFE_EXPR_SUB bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe' bType res1 res2) t))
+  | ASTFE_EXPR_MUL bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe' bType res1 res2) t))
+  | ASTFE_EXPR_DIV bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe' bType res1 res2) t))
+  | ASTFE_EXPR_SHR bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe' bType res1 res2) t))
+  | ASTFE_EXPR_SHL bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe' bType res1 res2) t))
+
+  | ASTFE_EXPR_LT bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe' bType res1 res2) t))
+  | ASTFE_EXPR_LTE bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe' bType res1 res2) t))
+  | ASTFE_EXPR_GT bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe' bType res1 res2) t))
+  | ASTFE_EXPR_GTE bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe' bType res1 res2) t))
+  | ASTFE_EXPR_EQ bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe' bType res1 res2) t))
+  | ASTFE_EXPR_NEQ bType subExpr1 subExpr2 ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+    (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+     (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe' bType res1 res2) t))
+
+  | ASTFE_EXPR_B8toW16 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe' res) t)
+  | ASTFE_EXPR_B8toW32 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe' res) t)
+  | ASTFE_EXPR_W16toB8 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe' res) t)
+  | ASTFE_EXPR_W16toW32 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe' res) t)
+  | ASTFE_EXPR_W32toB8 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe' res) t)
+  | ASTFE_EXPR_W32toW16 subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+    (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe' res) t)
+
+  | ASTFE_EXPR_ID b subType var ⇒
+   opt_map ?? (retype_var fe b subType var fe' dim)
+    (λres.ast_to_astfe_expr_check fe' subType (ASTFE_EXPR_ID fe' b subType res) t)
+  ]
+and retype_var (fe:aux_flatEnv_type) (b:bool) (t:ast_type) (ast:astfe_var fe b t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_var fe' b t) ≝
+ match ast with
+  [ ASTFE_VAR_ID subB subType subId ⇒
+   opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
+    (λresId.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ID fe' subB subType resId) b t)
+
+  | ASTFE_VAR_ARRAY subB subType n var expr ⇒
+   opt_map ?? (retype_var fe subB (AST_TYPE_ARRAY subType n) var fe' dim)
+    (λresVar.opt_map ?? (retype_base_expr fe expr fe' dim)
+     (λresExpr.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ARRAY fe' subB subType n resVar resExpr) b t))
+
+  | ASTFE_VAR_STRUCT subB nelSubType field var ⇒
+   opt_map ?? (retype_var fe subB (AST_TYPE_STRUCT nelSubType) var fe' dim)
+    (λres.ast_to_astfe_var_check fe' subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe' subB nelSubType field res) b t)
+  ]
+and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_base_expr fe') ≝
+ match ast with
+  [ ASTFE_BASE_EXPR bType subExpr ⇒
+   opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+    (λres.Some ? (ASTFE_BASE_EXPR fe' bType res))
   ].
 
 (*
@@ -255,14 +421,99 @@ and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (map:aux_trasf
  AST_INIT_VAL: ∀t:ast_type.
                aux_ast_init_type t → ast_init e t
 *)
-definition ast_to_astfe_init : Πe.Πt.ast_init e t → aux_trasfMap_type → option (astfe_init t) ≝
-λe:aux_env_type.λt:ast_type.λast:ast_init e t.λmap:aux_trasfMap_type.match ast with
- [ AST_INIT_VAR subB subType var ⇒
-  opt_map ?? (ast_to_astfe_var e subB subType var map)
-   (λres.ast_to_astfe_init_check subType (ASTFE_INIT_VAR subB subType res) t)
+definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝
+λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
+ match ast with
+  [ AST_INIT_VAR subB subType var ⇒
+   opt_map ?? (ast_to_astfe_var e subB subType var fe map)
+    (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t)
+
+  | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
+  ].
 
- | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL subType args) t
- ].
+definition retype_init ≝
+λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ match ast with
+  [ ASTFE_INIT_VAR subB subType var ⇒
+   opt_map ?? (retype_var fe subB subType var fe' dim)
+    (λres.ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAR fe' subB subType res) t)
+
+  | ASTFE_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAL fe' subType args) t
+  ].
+
+(*
+ ASTFE_STM_ASG: ∀t:ast_type.
+                astfe_var e false t → astfe_expr e t → astfe_stm e
+ ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
+                 astfe_id e b t → astfe_init e t → astfe_stm e
+ ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
+ ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
+*)
+let rec retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝
+ match ast with
+  [ ASTFE_STM_ASG subType var expr ⇒
+   opt_map ?? (retype_var fe false subType var fe' dim)
+    (λresVar.opt_map ?? (retype_expr fe subType expr fe' dim)
+     (λresExpr.Some ? (ASTFE_STM_ASG fe' subType resVar resExpr)))
+
+  | ASTFE_STM_INIT subB subType subId init ⇒
+   opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
+    (λresId.opt_map ?? (retype_init fe subType init fe' dim)
+     (λresInit.Some ? (ASTFE_STM_INIT fe' subB subType resId resInit)))
+
+  | ASTFE_STM_WHILE expr body ⇒
+   opt_map ?? (retype_base_expr fe expr fe' dim)
+    (λresExpr.opt_map ?? (retype_body fe body fe' dim)
+     (λresBody.Some ? (ASTFE_STM_WHILE fe' resExpr resBody)))
+
+  | ASTFE_STM_IF nelExprBody optBody ⇒
+   opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
+                                     (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
+                                      (λresBody.opt_map ?? t
+                                       (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
+                                    (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
+                                    nelExprBody)
+    (λres.match optBody with
+     [ None ⇒ Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (None ?))
+     | Some body ⇒
+      opt_map ?? (retype_body fe body fe' dim)
+       (λresBody.Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (Some ? resBody)))
+     ])
+  ]
+(*
+ ASTFE_BODY: list (astfe_stm e) → astfe_body e
+*)
+and retype_body (fe:aux_flatEnv_type) (ast:astfe_body fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_body fe') ≝
+ match ast with
+  [ ASTFE_BODY lStm ⇒
+   opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
+                                   (λh'.opt_map ?? t
+                                    (λt'.Some ? ([h']@t')))) (Some ? []) lStm)
+    (λresStm.Some ? (ASTFE_BODY fe' resStm))
+  ].
+
+definition retype_stm_list ≝
+λfe:aux_flatEnv_type.λast:list (astfe_stm fe).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim)
+                     (λh'.opt_map ?? t
+                      (λt'.Some ? ([h']@t')))) (Some ? []) ast.
+
+definition retype_exprAndBody_neList ≝
+λfe:aux_flatEnv_type.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true).
+ opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim)
+                                   (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim)
+                                    (λresBody.opt_map ?? t
+                                     (λt'.Some ? («£(pair ?? resExpr resBody)»&t')))))
+                                  (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))))
+                                  ast)
+  (λres.Some ? (cut_last_neList ? res)).
+
+(* applicare l'identita' e' inifluente *)
+lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
+                         aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe.
+ intros;
+ apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
+qed.
 
 (*
  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
@@ -272,54 +523,112 @@ definition ast_to_astfe_init : Πe.Πt.ast_init e t → aux_trasfMap_type → op
  AST_STM_IF: ∀e:aux_env_type.
              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
 *)
-let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T astfe_stm aux_trasfMap_type aux_flatEnv_type) ≝
- match ast with
+let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
+ : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
+ match ast
+  return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+ with
   [ AST_STM_ASG e' subType var expr ⇒
-   opt_map ?? (ast_to_astfe_var e' false subType var map)
-    (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr map)
-     (λresExpr.Some ? (tripleT ??? (ASTFE_STM_ASG subType resVar resExpr) map fe)))
+   λmap:aux_trasfMap_type e' fe.
+    opt_map ?? (ast_to_astfe_var e' false subType var fe map)
+     (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
+      (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
 
   | AST_STM_WHILE e' expr decl ⇒
-   opt_map ?? (ast_to_astfe_base_expr e' expr map)
-    (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl map fe)
-     (λtripleRes.match tripleRes with
-      [ tripleT resDecl map' fe' ⇒
-       Some ? (tripleT ??? (ASTFE_STM_WHILE resExpr (ASTFE_BODY resDecl)) (rollback_map map' (build_snapshot map)) fe')
-      ]))
+   λmap:aux_trasfMap_type e' fe.
+    opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
+     (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
+      (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+       [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+        [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
+         [ pair map' resDecl ⇒
+          match le_flatEnv fe fe'
+           return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+          with
+           [ true ⇒ λp:(le_flatEnv fe fe' = true).
+                     opt_map ?? (retype_base_expr fe resExpr fe' p)
+                      (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
+                                                    (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
+          | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
+          ] (refl_eq ? (le_flatEnv fe fe'))
+         ]]]))
 
   | AST_STM_IF e' nelExprDecl optDecl ⇒
-   let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e'))))
-               (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝
-    match nel with
-     [ ne_nil h ⇒
-      opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
-       (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
-        (λtripleRes.match tripleRes with
-         [ tripleT resDecl m' flatE' ⇒
-          Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE')
-         ]))
-     | ne_cons h tl ⇒
-      opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
-       (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
-        (λtripleRes.match tripleRes with
-         [ tripleT resDecl m' flatE' ⇒
-          opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE')
-           (λtripleRes'.match tripleRes' with
-            [ tripleT tl' m'' flatE'' ⇒
-             Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'')
-            ])]))] in
-   opt_map ?? (aux nelExprDecl map fe)
-    (λtRes.match tRes with
-     [ tripleT resNel resMap resFe ⇒
-      match optDecl with
-       [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe)
-       | Some decl ⇒
-        opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe)
-         (λtRes'.match tRes' with
-          [ tripleT rDecl resMap' resFe' ⇒
-           Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe')
-          ])
-       ]])
+   λmap:aux_trasfMap_type e' fe.
+    let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
+                (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
+     match nel with
+      [ ne_nil h ⇒
+       opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
+        (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
+         (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+          [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+           [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
+            [ pair m' resDecl ⇒
+             match le_flatEnv fenv fenv'
+              return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+             with
+              [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
+               opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
+                (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
+                                                   «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
+              | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
+              ] (refl_eq ? (le_flatEnv fenv fenv'))
+            ]]]))
+
+      | ne_cons h tl ⇒
+       opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
+        (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
+         (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
+          [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+           [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
+            [ pair m' resDecl ⇒
+             opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
+              (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
+               [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
+                [ pair m'' tl' ⇒
+                 match le_flatEnv fenv fenv''
+                  return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+                 with
+                  [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
+                   match le_flatEnv fenv' fenv''
+                    return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe'))))
+                   with
+                    [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
+                     opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
+                      (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
+                       (λresDecl'.
+                 Some ? (≪fenv'',pair ?? m''
+                                          («£(pair ?? resExpr'
+                                                     (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
+                    | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
+                    ] (refl_eq ? (le_flatEnv fenv' fenv''))
+                  | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
+                  ] (refl_eq ? (le_flatEnv fenv fenv''))
+                ]])]]]))
+      ] in
+    opt_map ?? (aux fe map nelExprDecl)
+     (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
+      [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
+       [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
+        [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
+        | Some decl ⇒
+         opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
+          (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
+           [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+            [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
+             [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
+              match le_flatEnv fe' fe''
+               return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+              with
+               [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
+                opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
+                 (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
+                            (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
+                                            (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
+               | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
+               ] (refl_eq ? (le_flatEnv fe' fe''))
+             ]]])]]])
   ]
 (*
  AST_NO_DECL: ∀e:aux_env_type.
@@ -327,51 +636,100 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (map:aux_trasfMap_type
  AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
            (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
 *)
-and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T (list astfe_stm) aux_trasfMap_type aux_flatEnv_type) ≝
- match ast with
+and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
+ : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝ 
+ match ast
+  return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
+ with
   [ AST_NO_DECL e' lStm ⇒
-   let rec aux (ll:list (ast_stm e')) (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on ll ≝
-    match ll with
-     [ nil ⇒ Some ? (tripleT ??? [] m flatE)
-     | cons h tl ⇒
-      opt_map ?? (ast_to_astfe_stm e' h m flatE)
-       (λtripleRes.match tripleRes with
-        [ tripleT resStm m' flatE' ⇒
-         opt_map ?? (aux tl m' flatE')
-          (λtripleRes'.match tripleRes' with
-           [ tripleT tl' m'' flatE'' ⇒
-            Some ? (tripleT ??? ([ resStm ]@tl') m'' flatE'')
-           ])])] in
-   aux lStm map fe
-
-  | AST_DECL e' b name t _ optInit subDecl ⇒
-   opt_map ?? (match optInit with
-               [ None ⇒ Some ? [] | Some init ⇒ opt_map ?? (ast_to_astfe_init e' t init map)
-                (λresInit.Some ? [ ASTFE_STM_INIT b t (ASTFE_ID (name_to_nameId (add_maxcur_map map name) name) b t) resInit ])])
-    (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl (add_maxcur_map map name) (add_desc_flatEnv fe (name_to_nameId (add_maxcur_map map name) name) b t))
-     (λtripleRes.match tripleRes with
-      [ tripleT tRes resMap resFe ⇒
-       Some ? (tripleT ??? (hRes@tRes) resMap resFe)
-      ]))
+   λmap:aux_trasfMap_type e' fe.
+    let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
+     : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
+     match ll with
+      [ nil ⇒ let trsf ≝ []
+              in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
+                                           (list (astfe_stm fenv))
+                                           (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
+
+      | cons h tl ⇒
+       opt_map ?? (ast_to_astfe_stm e' h fenv m)
+        (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
+         [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
+          [ pair m' resStm ⇒
+           opt_map ?? (aux tl fenv' m')
+            (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
+             [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+              [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
+               [ pair m'' tl' ⇒
+                match le_flatEnv fenv' fenv''
+                 return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
+                with
+                 [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
+                  opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
+                   (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
+                                                      (list (astfe_stm fenv''))
+                                                      m''
+                                                      (resStm'@tl')≫≫)
+                 | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
+                 ] (refl_eq ? (le_flatEnv fenv' fenv''))
+               ]]])]])] in
+    aux lStm fe map
+
+  | AST_DECL e' b name t dim optInit subDecl ⇒
+   λmap:aux_trasfMap_type e' fe.
+    opt_map ?? (match optInit with
+                [ None ⇒ Some ? []
+                | Some init ⇒
+                 opt_map ?? (ast_to_astfe_init e' t init fe map)
+                  (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
+                                                              (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
+                                                                        (next_nameId e' fe map name)
+                                                                        (ast_to_astfe_dec_aux e' name b t fe map dim))
+                                                              b t)
+                   (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
+                                                   (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
+                    (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
+                ])
+     (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
+                                          (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
+                                          (add_maxcur_map e' fe map map name b t))
+      (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
+       [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
+        [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
+         [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
+          match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
+           return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe'))))
+          with
+           [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
+            opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
+             (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
+                     in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
+                                                 (list (astfe_stm fe'))
+                                                 map'
+                                                 (hRes'@tRes)≫≫)
+           | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
+           ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
+         ]]]))
   ].
 
 (*
  AST_ROOT: ast_decl empty_env → ast_root.
 *)
-definition ast_to_astfe ≝
+definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
 λast:ast_root.match ast with
- [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_trasfMap empty_flatEnv with
+ [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
   (* impossibile: dummy *)
-  [ None ⇒ empty_astfe_prog
-  | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x))
-  ]
- ].
+  [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
+  | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
+   [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
+    [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
+     [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
+     ]]]]].
 
-(* mini test *)
-(*include "compiler/preast_tree.ma".
-include "compiler/preast_to_ast.ma".*)
+(* mini test 
+include "compiler/preast_tree.ma".
+include "compiler/preast_to_ast.ma".
 
-(*
 { const byte8 a;
   const byte8[3] b={0,1,2};
   byte8[3] c=b;
@@ -388,20 +746,15 @@ include "compiler/preast_to_ast.ma".*)
   else
    { const byte8 a=a; }
 }
-*)
-(*
+
 definition prova ≝
 PREAST_ROOT (
  PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
-  PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
+  PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) (
    PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) (
     PREAST_NO_DECL [
      PREAST_STM_IF «
        (pair ??
-       (PREAST_EXPR_BYTE8 〈xF,x2〉)
-       (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
-       )
-     £ (pair ??
        (PREAST_EXPR_BYTE8 〈xF,x0〉)
        (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
        )
@@ -412,6 +765,10 @@ PREAST_ROOT (
         PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL [])
         ))
        ])
+       )
+     £ (pair ??
+       (PREAST_EXPR_BYTE8 〈xF,x2〉)
+       (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL []))
        ) 
      » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])))
     ]
@@ -419,7 +776,4 @@ PREAST_ROOT (
   )   
  )
 ).
-
-lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
-normalize;
 *)