X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_to_astfe.ma;h=c6d859c4e207a65c653a3e883af602bdb2bca09a;hb=92c1b82f32dd0db6af3cb1f56af23b78144fae9a;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..c6d859c4e 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -20,406 +20,641 @@
 (* ********************************************************************** *)
 
 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.
- 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))
-  | 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.
- 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))
-  | 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.
- 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))
-  | 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.
- 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))
-  | 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')
-   (λ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)))
+  AST_ID: ∀str:aux_str_type.
+          (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d 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 ].
+lemma ast_to_astfe_id :
+ ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t.
+ ∀m:aux_map_type d.∀fe.
+ ∀dimInv:env_to_flatEnv_inv d e m fe.
+ astfe_id fe b t.
+ intros 7;
+ unfold env_to_flatEnv_inv;
+ elim a 0;
+ intros 3;
+ lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
+ [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
+ | rewrite > (proj2 ?? (H1 a1 H));
+   apply Hletin
+ ].
+qed.
+
+lemma ast_to_astfe_retype_id :
+ ∀fe,b,t.∀ast:astfe_id fe b t.
+ ∀d.∀e:aux_env_type d.∀m:aux_map_type d.∀fe'.
+ ∀dimInv:env_to_flatEnv_inv d e m fe'.
+ ∀dimLe:le_flatEnv fe fe' = true.
+ astfe_id fe' b t.
+ intros 8;
+ unfold env_to_flatEnv_inv;
+ elim a 0;
+ intros 4;
+ lapply (ASTFE_ID fe' a1 ?);
+ [ apply (leflatenv_to_check fe fe' a1 H2 H)
+ | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
+   apply Hletin
+ ].
+qed.
 
 (*
- AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
- AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
-
- AST_EXPR_NEG: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_NOT: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_COM: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
-
- AST_EXPR_ADD: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_SUB: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_MUL: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_DIV: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_SHR: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
- AST_EXPR_SHL: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
-
- AST_EXPR_GT : ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_GTE: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_LT : ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_LTE: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_EQ : ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_NEQ: ∀t:ast_base_type.
-               ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
-
- AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
- AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
- AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
- AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
- AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
-
- AST_EXPR_ID: ∀b:bool.∀t:ast_type.
-              ast_var e b t → ast_expr e t
+  AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+
+| AST_EXPR_NEG: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_NOT: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_COM: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+
+| AST_EXPR_ADD: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SUB: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_MUL: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_DIV: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SHR: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_SHL: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+
+| AST_EXPR_GT : ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_GTE: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_LT : ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_LTE: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_EQ : ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_NEQ: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+
+| AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+
+| AST_EXPR_ID: ∀b:bool.∀t:ast_type.
+               ast_var d e b t → ast_expr d 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) ≝
- 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_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)
-  | 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)
-  | 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)
-
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-  | 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))
-
-  | 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)
-  | 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)
-  | 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)
-  | 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)
-  | 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)
-  | 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)
-
-  | 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)
+let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
+                          (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
+ match ast
+  return λW.λa:ast_expr d e W.astfe_expr fe W
+ with
+  [ AST_EXPR_BYTE8 val ⇒
+   ASTFE_EXPR_BYTE8 fe val
+  | AST_EXPR_WORD16 val ⇒
+   ASTFE_EXPR_WORD16 fe val
+  | AST_EXPR_WORD32 val ⇒
+   ASTFE_EXPR_WORD32 fe val
+
+  | AST_EXPR_NEG bType sExpr ⇒
+   ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+  | AST_EXPR_NOT bType sExpr ⇒
+   ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+  | AST_EXPR_COM bType sExpr ⇒
+   ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+
+  | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+  | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+
+  | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                          (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_LT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                          (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                          (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+
+  | AST_EXPR_B8toW16 sExpr ⇒
+   ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+  | AST_EXPR_B8toW32 sExpr ⇒
+   ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+  | AST_EXPR_W16toB8 sExpr ⇒
+   ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+  | AST_EXPR_W16toW32 sExpr ⇒
+   ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+  | AST_EXPR_W32toB8 sExpr ⇒
+   ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+  | AST_EXPR_W32toW16 sExpr ⇒
+   ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+
+  | AST_EXPR_ID b sType var ⇒
+   ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
+
   ]
 (*
- AST_VAR_ID: ∀b:bool.∀t:ast_type.
-             ast_id e b t → ast_var e b t
- AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
-                ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
- 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)
+  AST_VAR_ID: ∀b:bool.∀t:ast_type.
+              ast_id d e b t → ast_var d e b t
+| AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+                 ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
+| AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
+                  ast_var d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d 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) ≝
- 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
+and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
+                     (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
+ match ast
+  return λW,X.λa:ast_var d e W X.astfe_var fe W X
+ with
+  [ AST_VAR_ID sB sType sId ⇒
+   ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
 
-  | 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))
+  | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
+   ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
+                                    (ast_to_astfe_base_expr d e sExpr m fe dimInv)
 
-  | 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)
+  | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
+   ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)                                                                                    
   ]
 (*
- AST_BASE_EXPR: ∀t:ast_base_type.
-                ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
+  AST_BASE_EXPR: ∀t:ast_base_type.
+                 ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d 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 ≝
- 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))
+and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
+                           (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
+ match ast
+  return λa:ast_base_expr d e.astfe_base_expr fe
+ with
+  [ AST_BASE_EXPR bType sExpr ⇒
+   ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+  ].
+
+let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
+                                 d (e:aux_env_type d) (m:aux_map_type d) fe'
+                                 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
+ match ast
+  return λW.λa:astfe_expr fe W.astfe_expr fe' W
+ with
+  [ ASTFE_EXPR_BYTE8 val ⇒
+   ASTFE_EXPR_BYTE8 fe' val
+  | ASTFE_EXPR_WORD16 val ⇒
+   ASTFE_EXPR_WORD16 fe' val
+  | ASTFE_EXPR_WORD32 val ⇒
+   ASTFE_EXPR_WORD32 fe' val
+
+  | ASTFE_EXPR_NEG bType sExpr ⇒
+   ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_NOT bType sExpr ⇒
+   ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_COM bType sExpr ⇒
+   ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+
+  | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+
+  | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                           (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                           (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                           (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+
+  | ASTFE_EXPR_B8toW16 sExpr ⇒
+   ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_B8toW32 sExpr ⇒
+   ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_W16toB8 sExpr ⇒
+   ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_W16toW32 sExpr ⇒
+   ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_W32toB8 sExpr ⇒
+   ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_W32toW16 sExpr ⇒
+   ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+
+  | ASTFE_EXPR_ID b sType var ⇒
+   ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
+
+  ]
+and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
+                            d (e:aux_env_type d) (m:aux_map_type d) fe'
+                            (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
+ match ast
+  return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
+ with
+  [ ASTFE_VAR_ID sB sType sId ⇒
+   ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+
+  | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
+   ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe)
+                                     (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+
+  | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
+   ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe)                                                                                    
+  ]
+and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
+                                  d (e:aux_env_type d) (m:aux_map_type d) fe'
+                                  (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
+ match ast
+  return λa:astfe_base_expr fe.astfe_base_expr fe'
+ with
+  [ ASTFE_BASE_EXPR bType sExpr ⇒
+   ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
   ].
 
 (*
- AST_INIT_VAR: ∀b:bool.∀t:ast_type.
-               ast_var e b t → ast_init e t
- AST_INIT_VAL: ∀t:ast_type.
-               aux_ast_init_type t → ast_init e t
+  AST_INIT_VAR: ∀b:bool.∀t:ast_type.
+                ast_var d e b t → ast_init d e t
+| AST_INIT_VAL: ∀t:ast_type.
+                aux_ast_init_type t → ast_init d 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 ≝
+λd.λe:aux_env_type d.λt.λast:ast_init d e t.
+λm:aux_map_type d.λfe.
+λdimInv:env_to_flatEnv_inv d e m fe.
+ match ast
+  return λW.λa:ast_init d e W.astfe_init fe W
+ with
+  [ AST_INIT_VAR sB sType sVar ⇒
+   ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
 
- | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL subType args) t
- ].
+  | AST_INIT_VAL sType sArgs ⇒
+   ASTFE_INIT_VAL fe sType sArgs
+
+  ].
+
+definition ast_to_astfe_retype_init ≝
+λfe,t.λast:astfe_init fe t.
+λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
+λdimInv:env_to_flatEnv_inv d e m fe'.
+λdimLe:le_flatEnv fe fe' = true.
+ match ast
+  return λW.λa:astfe_init fe W.astfe_init fe' W
+ with
+  [ ASTFE_INIT_VAR sB sType sVar ⇒
+   ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
+
+  | ASTFE_INIT_VAL sType sArgs ⇒
+   ASTFE_INIT_VAL fe' sType sArgs
+
+  ].
 
 (*
- AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
-              ast_var e false t → ast_expr e t → ast_stm e
- AST_STM_WHILE: ∀e:aux_env_type.
-                ast_base_expr e → ast_decl (enter_env e) → ast_stm e
- 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
+  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 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) ≝
+let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe)
+                                d (e:aux_env_type d) (m:aux_map_type d) fe'
+                                (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝
  match ast 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)))
-
-  | 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')
-      ]))
-
-  | 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')
-          ])
-       ]])
+  [ ASTFE_STM_ASG sType sVar sExpr ⇒
+   ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
+                           (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
+
+  | ASTFE_STM_INIT sB sType sId sInit ⇒
+   ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+                               (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
+
+  | ASTFE_STM_WHILE sExpr sBody ⇒
+   ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+                       (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
+
+  | ASTFE_STM_IF sNelExprBody sOptBody ⇒
+   ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+                                                                              (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+                                                                              )»&t)
+                                                             «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+                                                             sNelExprBody))
+                    (opt_map ?? sOptBody
+                      (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
   ]
 (*
- AST_NO_DECL: ∀e:aux_env_type.
-              list (ast_stm e) → ast_decl e
- 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
+  ASTFE_BODY: list (astfe_stm e) → astfe_body 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) ≝
+and ast_to_astfe_retype_body fe (ast:astfe_body fe)
+                             d (e:aux_env_type d) (m:aux_map_type d) fe'
+                             (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_body fe' ≝
  match ast 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)
-      ]))
+  [ ASTFE_BODY sLStm ⇒
+   ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
   ].
 
+definition ast_to_astfe_retype_stm_list ≝
+λfe.λast:list (astfe_stm fe).
+λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
+λdimInv:env_to_flatEnv_inv d e m fe'.
+λdimLe:le_flatEnv fe fe' = true.
+ fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
+
+definition ast_to_astfe_retype_exprBody_neList ≝
+λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).
+λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
+λdimInv:env_to_flatEnv_inv d e m fe'.
+λdimLe:le_flatEnv fe fe' = true.
+ cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
+                                                          (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
+                                                          )»&t)
+                                         «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
+                                         ast).
+
+(* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
+inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
+                         env_to_flatEnv_inv d e m fe' →
+                         le_flatEnv fe fe' = true →
+                         astfe_stm fe' →
+                         ast_to_astfe_stm_record d e fe.
+
+inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
+                        env_to_flatEnv_inv d e m fe' →
+                        le_flatEnv fe fe' = true →
+                        ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
+                        ast_to_astfe_if_record d e fe.
+
+inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
+                          env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
+                          le_flatEnv fe fe' = true →
+                          list (astfe_stm fe') →
+                          ast_to_astfe_decl_record d e fe.
+
+inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
+AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
+                              env_to_flatEnv_inv d e m fe' →
+                              le_flatEnv fe fe' = true →
+                              list (astfe_stm fe') →
+                              ast_to_astfe_decl_aux_record d e fe.
+
 (*
- AST_ROOT: ast_decl empty_env → ast_root.
+  AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
+               ast_var d e false t → ast_expr d e t → ast_stm d e
+| AST_STM_WHILE: ∀d.∀e:aux_env_type d.
+                 ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
+| AST_STM_IF: ∀d.∀e:aux_env_type d.
+              ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
 *)
-definition ast_to_astfe ≝
-λast:ast_root.match ast with
- [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_trasfMap empty_flatEnv with
-  (* impossibile: dummy *)
-  [ None ⇒ empty_astfe_prog
-  | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x))
-  ]
- ].
-
-(* mini test *)
-(*include "compiler/preast_tree.ma".
-include "compiler/preast_to_ast.ma".*)
+let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe.
+                                                                         env_to_flatEnv_inv d e m fe →
+                                                                         ast_to_astfe_stm_record d e fe ≝
+ match ast
+  return λD.λE.λast:ast_stm D E.
+         Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
+ with
+  [ AST_STM_ASG sD sE sType sVar sExpr ⇒
+   λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+   AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
+                           (eq_to_leflatenv ?? (refl_eq ??))
+                           (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv)
+                                                   (ast_to_astfe_expr sD sE sType sExpr m fe dimInv))
+  | AST_STM_WHILE sD sE sExpr sDecl ⇒
+   λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+   match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
+         (env_map_flatEnv_enter_aux sD sE m fe dimInv) with
+    [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+     eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+             (λenv.ast_to_astfe_stm_record sD env fe)
+             (AST_TO_ASTFE_STM_RECORD sD
+                                      (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                      fe
+                                      (leave_map sD resMap)
+                                      resFe
+                                      (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+                                      resDimLe
+                                      (ASTFE_STM_WHILE resFe
+                                                       (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv)
+                                                                                      sD
+                                                                                      (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                                                                      (leave_map sD resMap)
+                                                                                      resFe
+                                                                                      (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+                                                                                      resDimLe)                                                       
+                                                       (ASTFE_BODY resFe resLStm)))                       
+             sE (leave_add_enter_env sD sE resTrsf) ]
+
+  | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
+   λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+   let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
+               (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
+               (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝
+    match nel with
+     [ ne_nil h ⇒
+      match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
+            (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
+       [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+        eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                (λenv.ast_to_astfe_if_record sD env pFe)
+                (AST_TO_ASTFE_IF_RECORD sD
+                                        (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                        pFe
+                                        (leave_map sD resMap)
+                                        resFe
+                                        (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+                                        resDimLe
+                                        «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
+                                                                                  sD
+                                                                                  (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                                                                  (leave_map sD resMap)
+                                                                                  resFe
+                                                                                  (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+                                                                                  resDimLe)
+                                                   (ASTFE_BODY resFe resLStm))»)
+                sE (leave_add_enter_env sD sE resTrsf) ]
+
+     | ne_cons h t ⇒
+      match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
+            (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
+       [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+        match aux t (leave_map sD resMap) resFe
+                  (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                           (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
+                           (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
+                           sE (leave_add_enter_env sD sE resTrsf)) with
+        [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
+         AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
+                                (leflatenv_trans ??? resDimLe resDimLe')
+                                («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
+                                                                           sD sE resMap' resFe' resDimInv'
+                                                                           (leflatenv_trans ??? resDimLe resDimLe'))
+                                            (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
+                                                                      sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
+
+     ] in
+   match aux sExprDecl m fe dimInv with
+    [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
+     match sOptDecl with
+      [ None ⇒
+       AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
+
+      | Some sDecl ⇒
+       match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe
+             (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with
+        [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
+         eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                 (λenv.ast_to_astfe_stm_record sD env fe)
+                 (AST_TO_ASTFE_STM_RECORD sD
+                                          (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                          fe
+                                          (leave_map sD resMap')
+                                          resFe'
+                                          (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
+                                          (leflatenv_trans ??? resDimLe resDimLe')
+                                          (ASTFE_STM_IF resFe'
+                                                        (ast_to_astfe_retype_exprBody_neList resFe resExprBody
+                                                                                             sD
+                                                                                             (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
+                                                                                             (leave_map sD resMap')
+                                                                                             resFe'
+                                                                                             (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
+                                                                                             resDimLe')
+                                                        (Some ? (ASTFE_BODY resFe' resLStm))))
+                 sE (leave_add_enter_env sD sE resTrsf) ]]]
 
+  ]
 (*
-{ const byte8 a;
-  const byte8[3] b={0,1,2};
-  byte8[3] c=b;
-  
-  if(0xF0)
-   { byte8 a=a; }
-  else if(0xF1)
-   {
-   while(0x10)
-    { byte8[3] b=c; }
-   }
-  else if(0xF2)
-   { byte8 a=b[0]; }
-  else
-   { const byte8 a=a; }
-}
+  AST_NO_DECL: ∀d.∀e:aux_env_type d.
+               list (ast_stm d e) → ast_decl d e
+| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
+            (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e
 *)
+and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
+                                                                       env_to_flatEnv_inv d e m fe →
+                                                                       ast_to_astfe_decl_record d e fe ≝
+ match ast
+  return λD.λE.λast:ast_decl D E.
+         Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
+  with
+   [ AST_NO_DECL sD sE sLStm ⇒
+    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+    let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
+                (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
+     match l with
+      [ nil ⇒
+       AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) []
+
+      | cons h t ⇒
+       match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
+        [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
+         match aux t resMap resFe resDimInv with
+          [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
+           AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
+                                        (leflatenv_trans ??? resDimLe resDimLe')
+                                        ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
+
+      ] in
+   match aux sLStm m fe dimInv with
+    [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
+     AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
+                              (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
+                              resDimLe resLStm ]
+
+   | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
+    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+    match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl
+          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
+          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
+          (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with
+     [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+      AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+                               ([ tripleT ??? sName sB sType ]@resTrsf)
+                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
+                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)
+                               (match sOptInit with
+                                [ None ⇒ []
+                                | Some init ⇒
+                                 [ ASTFE_STM_INIT resFe sB sType
+                                                  (* l'id e' sull'ambiente arricchito *)
+                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
+                                                                          sB sType
+                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType)
+                                                                                           sB sType
+                                                                                           (newid_from_init sD sE sName sB sType)
+                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
+                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
+                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv))
+                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                                          resMap resFe
+                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
+                                                                          resDimLe)
+                                                  (* l'init e' sull'ambiente non arricchito *)
+                                                  (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
+                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                                            resMap resFe
+                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
+                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe))
+                                 ]]@resLStm) ]          
+
+   ].
+
 (*
-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 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 []))
-       )
-     ; (pair ??
-       (PREAST_EXPR_BYTE8 〈xF,x1〉)
-       (PREAST_NO_DECL [
-        (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
-        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 [])
-        ))
-       ])
-       ) 
-     » (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 [])))
-    ]
-   )
-  )   
- )
-).
-
-lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
-normalize;
+  AST_ROOT: ast_decl O empty_env → ast_root
 *)
+definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
+λast:ast_root.match ast with
+ [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
+  [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].