X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fpreast_to_ast.ma;h=49a027ba7d18e951365c04bc47f5fe831909d743;hb=aba1baf85bb8e6b3ea3e66a8c2d07601066d26bc;hp=27c1e547768d9fb3155d10e1372c3893d0f2fc02;hpb=f2d9db85559c7a8db11aae1153495fae4a258d54;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
index 27c1e5477..49a027ba7 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -27,25 +27,25 @@ include "compiler/sigma.ma".
 (* PASSO 1 : da PREAST a AST *)
 (* ************************* *)
 
+(* NB: ASSERTO
+   al parser spetta il compito di rigettare le condizioni statiche verificabili
+    - divisione per valore 0
+   al parser spetta il compito di collassare le espressioni statiche
+    - val1+val2 -> val3, ...
+   al parser spetta il compito di collassare gli statement con condizioni statiche
+    - if(true) { b1 } else { b2 } -> b1, ...
+   al parser spetta il compito di individuare divergenza e dead code
+    - while(true) { b1 } -> loop infinito, ...
+*)
+
 (* operatore di cast *)
 definition preast_to_ast_expr_check ≝
-λe:aux_env_type.λsig:Σt'.ast_expr e t'.λt:ast_base_type.
- match sig with [ sigma_intro t' expr ⇒
-  match eq_ast_base_type t' t
-   return λx.eq_ast_base_type t' t = x → option (ast_expr e t)
-  with
-   [ true ⇒ λp:(eq_ast_base_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqastbasetype_to_eq ?? p))
-   | false ⇒ λp:(eq_ast_base_type t' t = false).None ?
-   ] (refl_eq ? (eq_ast_base_type t' t))
-  ].
-
-definition preast_to_ast_right_expr_check ≝
-λe:aux_env_type.λsig:Σt'.ast_right_expr e t'.λt:ast_type.
+λe:aux_env_type.λsig:(Σt'.ast_expr e t').λt:ast_type.
  match sig with [ sigma_intro t' expr ⇒
   match eq_ast_type t' t
-   return λx.eq_ast_type t' t = x → option (ast_right_expr e t)
+   return λx.eq_ast_type t' t = x → option (ast_expr e t)
   with
-   [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_right_expr e t) expr t (eqasttype_to_eq ?? p))
+   [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqasttype_to_eq ?? p))
    | false ⇒ λp:(eq_ast_type t' t = false).None ?
    ] (refl_eq ? (eq_ast_type t' t))
   ].
@@ -62,7 +62,7 @@ definition preast_to_ast_init_check ≝
   ].
 
 definition preast_to_ast_var_checkb ≝
-λe:aux_env_type.λt:ast_type.λsig:Σb'.ast_var e b' t.λb:bool.
+λe:aux_env_type.λt:ast_type.λsig:(Σb'.ast_var e b' t).λb:bool.
  match sig with [ sigma_intro b' var ⇒
   match eq_bool b' b
    return λx.eq_bool b' b = x → option (ast_var e b t)
@@ -73,7 +73,7 @@ definition preast_to_ast_var_checkb ≝
   ].
 
 definition preast_to_ast_var_checkt ≝
-λe:aux_env_type.λb:bool.λsig:Σt'.ast_var e b t'.λt:ast_type.
+λe:aux_env_type.λb:bool.λsig:(Σt'.ast_var e b t').λt:ast_type.
  match sig with [ sigma_intro t' var ⇒
   match eq_ast_type t' t
    return λx.eq_ast_type t' t = x → option (ast_var e b t)
@@ -84,7 +84,7 @@ definition preast_to_ast_var_checkt ≝
   ].
 
 definition preast_to_ast_var_check ≝
-λe:aux_env_type.λsig:Σb'.(Σt'.ast_var e b' t').λb:bool.λt:ast_type.
+λe:aux_env_type.λsig:(Σb'.(Σt'.ast_var e b' t')).λb:bool.λt:ast_type.
  opt_map ?? (preast_to_ast_var_checkt e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
   (λres1.opt_map ?? (preast_to_ast_var_checkb e t ≪(sigmaFst ?? sig),res1≫ b)
    (λres2.Some ? res2)).
@@ -116,134 +116,203 @@ definition preast_to_ast_var_check ≝
  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  PREAST_EXPR_ID: preast_var → preast_expr
 *)
-let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
+let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt.ast_expr e t) ≝
  match preast with
-  [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_BYTE8 e val)≫
-  | PREAST_EXPR_WORD16 val ⇒ Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_WORD16 e val)≫
-  | PREAST_EXPR_WORD32 val ⇒ Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_WORD32 e val)≫
+  [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 e val)≫
+  | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 e val)≫
+  | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 e val)≫
 
   | PREAST_EXPR_NEG subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.
-     Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_NEG e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+    (λsigmaRes:(Σt.ast_expr e t).
+     match (sigmaFst ?? sigmaRes) with
+      [ AST_TYPE_BASE bType ⇒
+       opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+        (λres.Some ? ≪?,(AST_EXPR_NEG e ? res)≫)
+      | _ ⇒ None ? ])
   | PREAST_EXPR_NOT subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.
-     Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_NOT e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+    (λsigmaRes:(Σt.ast_expr e t).
+     match (sigmaFst ?? sigmaRes) with
+      [ AST_TYPE_BASE bType ⇒
+       opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+        (λres.Some ? ≪?,(AST_EXPR_NOT e ? res)≫)
+      | _ ⇒ None ? ])
   | PREAST_EXPR_COM subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.
-     Some ? ≪(sigmaFst ?? sigmaRes),(AST_EXPR_COM e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes))≫)
+    (λsigmaRes:(Σt.ast_expr e t).
+     match (sigmaFst ?? sigmaRes) with
+      [ AST_TYPE_BASE bType ⇒
+       opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+        (λres.Some ? ≪?,(AST_EXPR_COM e ? res)≫)
+      | _ ⇒ None ? ])
 
   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_ADD e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_ADD e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SUB e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_SUB e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_MUL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_MUL e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_DIV e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_DIV e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
 
   | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHR e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+          (λres2.Some ? ≪?,(AST_EXPR_SHR e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
-      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+          (λres2.Some ? ≪?,(AST_EXPR_SHL e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
 
   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_GT e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_GTE e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_LT e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_LTE e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_EQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_EQ e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
   | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 e)
-    (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
-     (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
-      (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_NEQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+    (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+     (λsigmaRes2:(Σt.ast_expr e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_NEQ e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
 
   | PREAST_EXPR_B8toW16 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_BYTE8)
-     (λres.Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_B8toW16 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+     (λres.Some ? ≪?,(AST_EXPR_B8toW16 e res)≫))
   | PREAST_EXPR_B8toW32 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_BYTE8)
-     (λres.Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_B8toW32 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+     (λres.Some ? ≪?,(AST_EXPR_B8toW32 e res)≫))
   | PREAST_EXPR_W16toB8 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD16)
-     (λres.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_W16toB8 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+     (λres.Some ? ≪?,(AST_EXPR_W16toB8 e res)≫))
   | PREAST_EXPR_W16toW32 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD16)
-     (λres.Some ? ≪AST_BASE_TYPE_WORD32,(AST_EXPR_W16toW32 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+     (λres.Some ? ≪?,(AST_EXPR_W16toW32 e res)≫))
   | PREAST_EXPR_W32toB8 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD32)
-     (λres.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_W32toB8 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+     (λres.Some ? ≪?,(AST_EXPR_W32toB8 e res)≫))
   | PREAST_EXPR_W32toW16 subExpr ⇒
    opt_map ?? (preast_to_ast_expr subExpr e)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr_check e sigmaRes AST_BASE_TYPE_WORD32)
-     (λres.Some ? ≪AST_BASE_TYPE_WORD16,(AST_EXPR_W32toW16 e res)≫))
+    (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+     (λres.Some ? ≪?,(AST_EXPR_W32toW16 e res)≫))
 
-  | PREAST_EXPR_ID var ⇒
+   | PREAST_EXPR_ID var ⇒
    opt_map ?? (preast_to_ast_var var e)
-    (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+    (λsigmaRes:(Σb.(Σt.ast_var e b t)).
      match sigmaRes with [ sigma_intro b sigmaRes' ⇒
       match sigmaRes' with [ sigma_intro t _ ⇒
-       match t with
-        [ AST_TYPE_BASE bType ⇒
-         opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_BASE bType))
-          (λres.Some ? ≪bType,(AST_EXPR_ID e b bType res)≫)
-        | _ ⇒ None ? ]]])
+        opt_map ?? (preast_to_ast_var_check e sigmaRes b t)
+         (λres.Some ? ≪?,(AST_EXPR_ID e ?? res)≫)]])
   ]
 (*
  PREAST_VAR_ID: aux_str_type → preast_var
  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
  PREAST_VAR_STRUCT: preast_var → nat → preast_var
 *)
-and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb:bool.(Σt:ast_type.ast_var e b t)) ≝
+and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb.(Σt.ast_var e b t)) ≝
  match preast with
   [ PREAST_VAR_ID name ⇒
    match checkb_desc_env e name
-    return λx.checkb_desc_env e name = x → option (Σb:bool.(Σt:ast_type.ast_var e b t))
+    return λx.checkb_desc_env e name = x → option (Σb.(Σt.ast_var e b t))
    with
     [ true ⇒ λp:(checkb_desc_env e name = true).
      let desc ≝ get_desc_env e name in
@@ -255,12 +324,12 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (
 
   | PREAST_VAR_ARRAY subVar expr ⇒
    opt_map ?? (preast_to_ast_var subVar e)
-    (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
-     match sigmaRes with [ sigma_intro b sigmaRes' ⇒
-      match sigmaRes' with [ sigma_intro t _ ⇒
+    (λsigmaResV:(Σb.(Σt.ast_var e b t)).
+     match sigmaResV with [ sigma_intro b sigmaResV' ⇒
+      match sigmaResV' with [ sigma_intro t _ ⇒
        match t with
         [ AST_TYPE_ARRAY subType dim ⇒
-         opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_ARRAY subType dim))
+         opt_map ?? (preast_to_ast_var_check e sigmaResV b (AST_TYPE_ARRAY subType dim))
           (λresVar.
            (* ASSERTO:
               1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
@@ -269,21 +338,24 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (
                  OUT_OF_BOUND sara' fatto a run time
            *)
            match (match expr with
-                  [ PREAST_EXPR_BYTE8 val ⇒ (λx.leb (nat_of_byte8 val) dim)
-                  | PREAST_EXPR_WORD16 val ⇒ (λx.leb (nat_of_word16 val) dim)
-                  | PREAST_EXPR_WORD32 val ⇒ (λx.leb (nat_of_word32 val) dim)
+                  [ PREAST_EXPR_BYTE8 val ⇒ (λx.ltb (nat_of_byte8 val) dim)
+                  | PREAST_EXPR_WORD16 val ⇒ (λx.ltb (nat_of_word16 val) dim)
+                  | PREAST_EXPR_WORD32 val ⇒ (λx.ltb (nat_of_word32 val) dim)
                   | _ ⇒ (λx.true) ]) expr with
             [ true ⇒
              opt_map ?? (preast_to_ast_expr expr e)
-              (λsigmaRes:Σt:ast_base_type.ast_expr e t.
-               match sigmaRes with [ sigma_intro t resExpr ⇒
-                Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e t resExpr))≫≫ ])
+              (λsigmaResE:(Σt.ast_expr e t).
+               match sigmaFst ?? sigmaResE with
+                [ AST_TYPE_BASE bType ⇒
+                 opt_map ?? (preast_to_ast_expr_check e sigmaResE (AST_TYPE_BASE bType))
+                  (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e bType resExpr))≫≫)
+                | _ ⇒ None ? ])
             | false ⇒ None ? ])
         | _ ⇒ None ? ]]])
 
   | PREAST_VAR_STRUCT subVar field ⇒
    opt_map ?? (preast_to_ast_var subVar e)
-    (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+    (λsigmaRes:(Σb.(Σt.ast_var e b t)).
      match sigmaRes with [ sigma_intro b sigmaRes' ⇒
       match sigmaRes' with [ sigma_intro t _ ⇒
        match t with
@@ -291,7 +363,7 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (
          opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_STRUCT nelSubType))
           (λresVar.
            match ltb field (len_neList ? nelSubType)
-            return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb:bool.(Σt:ast_type.ast_var e b t))
+            return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var e b t))
            with
             [ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true).
              Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT e b nelSubType field resVar p)≫≫
@@ -313,46 +385,46 @@ definition preast_to_ast_init_val_aux_array :
 λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
 
 definition preast_to_ast_init_val_aux_struct :
-Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («t£»&nel))) ≝
+Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝
 λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
 
-let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt:ast_type.aux_ast_init_type t) ≝
+let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
  match preast with
   [ PREAST_INIT_VAL_BYTE8 val ⇒
-   Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
+   Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
   | PREAST_INIT_VAL_WORD16 val ⇒
-   Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
+   Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
   | PREAST_INIT_VAL_WORD32 val ⇒
-   Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
+   Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
 
   | PREAST_INIT_VAL_ARRAY nelSubVal ⇒
-   let rec aux (nel:ne_list preast_init_val) on nel : option (Σt:ast_type.aux_ast_init_type t) ≝
+   let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
     match nel with
      [ ne_nil h ⇒
       opt_map ?? (preast_to_ast_init_val_aux h)
        (λsigmaRes.match sigmaRes with [ sigma_intro t res ⇒
-        Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
+        Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
      | ne_cons h tl ⇒
       opt_map ?? (preast_to_ast_init_val_aux h)
-       (λsigmaRes1:(Σt:ast_type.aux_ast_init_type t).opt_map ?? (aux tl)
-        (λsigmaRes2:(Σt:ast_type.aux_ast_init_type t).
+       (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
+        (λsigmaRes2:(Σt.aux_ast_init_type t).
          match sigmaRes1 with [ sigma_intro t1 res1 ⇒
           match sigmaRes2 with [ sigma_intro t2 res2 ⇒
            match t2 with
             [ AST_TYPE_ARRAY bType dim ⇒
              match eq_ast_type t1 bType
-              return λx.(eq_ast_type t1 bType = x) → option (Σt:ast_type.aux_ast_init_type t)
+              return λx.(eq_ast_type t1 bType = x) → option (Σt.aux_ast_init_type t)
              with
               [ true ⇒ λp:(eq_ast_type t1 bType = true).
                match eq_ast_type t2 (AST_TYPE_ARRAY bType dim)
-                return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt:ast_type.aux_ast_init_type t)
+                return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt.aux_ast_init_type t)
                with
                 [ true ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = true).
-                 Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
-                                                        (preast_to_ast_init_val_aux_array bType dim                                                               
-                                                         (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
-                                                               (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
-                                                               (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
+                 Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
+                                               (preast_to_ast_init_val_aux_array bType dim                                                               
+                                                (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
+                                                      (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
+                                                         (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
                 | false ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = false).None ?
                 ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_ARRAY bType dim)))
               | false ⇒ λp:(eq_ast_type t1 bType = false).None ?
@@ -362,29 +434,29 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (
      ] in aux nelSubVal
 
   | PREAST_INIT_VAL_STRUCT nelSubVal ⇒
-   let rec aux (nel:ne_list preast_init_val) on nel : option (Σt:ast_type.aux_ast_init_type t) ≝
+   let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
     match nel with
      [ ne_nil h ⇒
       opt_map ?? (preast_to_ast_init_val_aux h)
-       (λsigmaRes:(Σt:ast_type.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
-        Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_STRUCT (« t £»)),res≫ ])
+       (λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
+        Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ])
      | ne_cons h tl ⇒ 
       opt_map ?? (preast_to_ast_init_val_aux h)
-       (λsigmaRes1:(Σt:ast_type.aux_ast_init_type t).opt_map ?? (aux tl)
-        (λsigmaRes2:(Σt:ast_type.aux_ast_init_type t).
+       (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
+        (λsigmaRes2:(Σt.aux_ast_init_type t).
          match sigmaRes1 with [ sigma_intro t1 res1 ⇒
           match sigmaRes2 with [ sigma_intro t2 res2 ⇒
            match t2 with
             [ AST_TYPE_STRUCT nelSubType ⇒
              match eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)
-              return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt:ast_type.aux_ast_init_type t)
+              return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t)
              with
               [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
-               Some (Σt:ast_type.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («t1£»&nelSubType)),
-                                                       (preast_to_ast_init_val_aux_struct ??
-                                                        (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
-                                                              res1
-                                                              (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
+               Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)),
+                                              (preast_to_ast_init_val_aux_struct ??
+                                               (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
+                                                     res1
+                                                     (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
               | false ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = false).None ?
               ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)))
             | _ ⇒ None ? ]]]))
@@ -395,17 +467,17 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (
  PREAST_INIT_VAR: preast_var → preast_init
  PREAST_INIT_VAL: preast_init_val → preast_init
 *)
-definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.ast_init e t) ≝
+definition preast_to_ast_init : preast_init → Πe.option (Σt.ast_init e t) ≝
 λpreast:preast_init.λe:aux_env_type.match preast with
  [ PREAST_INIT_VAR var ⇒
   opt_map ?? (preast_to_ast_var var e)
-   (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
-    Some (Σt:ast_type.ast_init e t) ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
+   (λsigmaRes:(Σb.(Σt.ast_var e b t)).
+    Some ? ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
 
  | PREAST_INIT_VAL val ⇒
   opt_map ?? (preast_to_ast_init_val_aux val)
-   (λsigmaRes:(Σt:ast_type.aux_ast_init_type t).
-    Some (Σt:ast_type.ast_init e t) ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
+   (λsigmaRes:(Σt.aux_ast_init_type t).
+    Some ? ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
  ].
 
 (*
@@ -413,54 +485,44 @@ definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.ast_ini
  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
  PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
 *)
-definition preast_to_ast_right_expr : preast_expr → Πe.option (Σt:ast_type.ast_right_expr e t) ≝
-λpreast:preast_expr.λe:aux_env_type.match preast with
- (* NB: PREAST_EXPR_ID viene sempre tradotto come AST_RIGHT_EXPR_VAR *)
- [ PREAST_EXPR_ID var ⇒
-    opt_map ?? (preast_to_ast_var var e)
-     (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
-      Some (Σt:ast_type.ast_right_expr e t) ≪?,(AST_RIGHT_EXPR_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
-
- | _ ⇒
-  opt_map ?? (preast_to_ast_expr preast e)
-   (λsigmaRes:(Σt:ast_base_type.ast_expr e t).
-    Some (Σt:ast_type.ast_right_expr e t) ≪ (AST_TYPE_BASE ?),(AST_RIGHT_EXPR_BASE e ? (sigmaSnd ?? sigmaRes))≫)
- ].
-
 definition preast_to_ast_base_expr : preast_expr → Πe.option (ast_base_expr e) ≝
 λpreast:preast_expr.λe:aux_env_type.
  opt_map ?? (preast_to_ast_expr preast e)
-  (λsigmaRes:(Σt:ast_base_type.ast_expr e t).
-   Some (ast_base_expr e) (AST_BASE_EXPR e ? (sigmaSnd ?? sigmaRes))).
+  (λsigmaRes:(Σt.ast_expr e t).
+   match sigmaFst ?? sigmaRes with
+    [ AST_TYPE_BASE bType ⇒
+     opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType))
+      (λres.Some ? (AST_BASE_EXPR e ? res))
+    | _ ⇒ None ? ]).
 
 let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
  match preast with
   [ PREAST_STM_ASG var expr ⇒
    opt_map ?? (preast_to_ast_var var e)
-    (λsigmaResV:(Σb:bool.(Σt:ast_type.ast_var e b t)).
+    (λsigmaResV:(Σb.(Σt.ast_var e b t)).
     match sigmaResV with [ sigma_intro _ sigmaResV' ⇒
      match sigmaResV' with [ sigma_intro t _ ⇒
       opt_map ?? (preast_to_ast_var_check e sigmaResV false t)
-       (λresVar.opt_map ?? (preast_to_ast_right_expr expr e)
-        (λsigmaResE:(Σt:ast_type.ast_right_expr e t).opt_map ?? (preast_to_ast_right_expr_check e sigmaResE t)
+       (λresVar.opt_map ?? (preast_to_ast_expr expr e)
+        (λsigmaResE:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaResE t)
          (λresExpr.Some ? (AST_STM_ASG e t resVar resExpr)
          )))]])
 
   | PREAST_STM_WHILE expr decl ⇒
    opt_map ?? (preast_to_ast_base_expr expr e)
-    (λresExpr.opt_map ?? (preast_to_ast_decl decl e)
+    (λresExpr.opt_map ?? (preast_to_ast_decl decl (enter_env e))
      (λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
-  
+
   | PREAST_STM_IF nelExprDecl optDecl ⇒
    opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
-                                     (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) e)
+                                     (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e))
                                       (λresDecl.opt_map ?? t
-                                       (λt'.Some ? («(pair ?? resExpr resDecl)£»&t')))))
-                                    (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL e (nil ?)))))
+                                       (λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
+                                    (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL (enter_env e) (nil ?)))))
                                     nelExprDecl)
     (λres.match optDecl with
      [ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?))
-     | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl e)
+     | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (enter_env e))
       (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
      ])
   ]
@@ -501,3 +563,23 @@ definition preast_to_ast ≝
 λpreast:preast_root.match preast with
  [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
                        (λres.Some ? (AST_ROOT res)) ].
+
+(* mini test
+definition prova ≝
+PREAST_ROOT (
+ PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) (
+  PREAST_NO_DECL [
+   PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) (
+    PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) (
+     PREAST_NO_DECL [
+      PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉))) 
+     ]
+    )
+   )
+  ]
+ )
+).
+
+lemma checkprova : None ? = preast_to_ast prova.
+normalize;
+*)