X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fpreast_to_ast.ma;h=49a027ba7d18e951365c04bc47f5fe831909d743;hb=55e5bef77f163b29feeb9ad4e83376c5aa301297;hp=58496cb7dab15c322348a632313a12a677a865f4;hpb=130f4d89a3c3d00840f584e7ab0c0dd87d27f91e;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 58496cb7d..49a027ba7 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -21,35 +21,74 @@
 
 include "compiler/preast_tree.ma".
 include "compiler/ast_tree.ma".
+include "compiler/sigma.ma".
 
-(* *********************** *)
-(* PASSO 1 DI COMPILAZIONE *)
-(* *********************** *)
+(* ************************* *)
+(* PASSO 1 : da PREAST a AST *)
+(* ************************* *)
 
-(*
- PREAST_VAR_ID: aux_str_type → preast_var
- PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
- PREAST_VAR_STRUCT: ne_list preast_var → nat → preast_var.
+(* 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, ...
 *)
-let rec evaluate_var_type (preast:preast_var) (e:aux_env_type) on preast : option (Prod bool ast_type) ≝
- match preast with
-  [ PREAST_VAR_ID name ⇒
-   opt_map ?? (get_desc_env_aux e (None ?) name)
-    (λdesc.Some ? (pair ?? (get_const_desc desc) (get_type_desc desc)))
-  | PREAST_VAR_ARRAY subVar expr ⇒
-   opt_map ?? (evaluate_var_type subVar e)
-    (λcDesc.match snd ?? cDesc with
-     [ AST_TYPE_ARRAY subType dim ⇒ Some ? (pair ?? (fst ?? cDesc) subType)
-     | _ ⇒ None ? ])
-  | PREAST_VAR_STRUCT subVar field ⇒
-   opt_map ?? (evaluate_var_type subVar e)
-    (λcDesc.match snd ?? cDesc with
-     [ AST_TYPE_STRUCT nelSubType ⇒
-      opt_map ?? (nth_neList ? nelSubType field)
-       (λsubType.Some ? (pair ?? (fst ?? cDesc) subType))
-     | _ ⇒ None ? ])
+
+(* operatore di cast *)
+definition preast_to_ast_expr_check ≝
+λ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_expr e t)
+  with
+   [ 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))
   ].
 
+definition preast_to_ast_init_check ≝
+λe:aux_env_type.λsig:Σt'.ast_init 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_init e t)
+  with
+   [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init e t) expr t (eqasttype_to_eq ?? p))
+   | false ⇒ λp:(eq_ast_type t' t = false).None ?
+   ] (refl_eq ? (eq_ast_type t' t))
+  ].
+
+definition preast_to_ast_var_checkb ≝
+λ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)
+  with
+   [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var e b t) var b (eqbool_to_eq ?? p))
+   | false ⇒ λp:(eq_bool b' b = false).None ?
+   ] (refl_eq ? (eq_bool b' b))
+  ].
+
+definition preast_to_ast_var_checkt ≝
+λ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)
+  with
+   [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var e b t) var t (eqasttype_to_eq ?? p))
+   | false ⇒ λp:(eq_ast_type t' t = false).None ?
+   ] (refl_eq ? (eq_ast_type t' t))
+  ].
+
+definition preast_to_ast_var_check ≝
+λ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)).
+
 (*
  PREAST_EXPR_BYTE8 : byte8 → preast_expr
  PREAST_EXPR_WORD16: word16 → preast_expr
@@ -77,400 +116,470 @@ let rec evaluate_var_type (preast:preast_var) (e:aux_env_type) on preast : optio
  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  PREAST_EXPR_ID: preast_var → preast_expr
 *)
-let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : option ast_base_type ≝
+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 _ ⇒ Some ? AST_BASE_TYPE_BYTE8
-  | PREAST_EXPR_WORD16 _ ⇒ Some ? AST_BASE_TYPE_WORD16
-  | PREAST_EXPR_WORD32 _ ⇒ Some ? AST_BASE_TYPE_WORD32
-  | PREAST_EXPR_NEG subExpr ⇒ evaluate_expr_type subExpr e
-  | PREAST_EXPR_NOT subExpr ⇒ evaluate_expr_type subExpr e
-  | PREAST_EXPR_COM subExpr ⇒ evaluate_expr_type subExpr e
+  [ 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_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_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_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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr1 e)
-    (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
-     (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
+   opt_map ?? (preast_to_ast_expr subExpr1 e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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 ?? (evaluate_expr_type subExpr e)
-    (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
-  | PREAST_EXPR_ID var ⇒
-   opt_map ?? (evaluate_var_type var e)
-    (λcDesc.match snd ?? cDesc with [ AST_TYPE_BASE bType ⇒ Some ? bType | _ ⇒ None ? ])
-  ].
+   opt_map ?? (preast_to_ast_expr subExpr e)
+    (λ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)≫))
 
-inductive sigma (A:Type) (P:A \to Type) : Type \def
-    sigma_intro: \forall x:A. P x \to sigma A P.
+   | PREAST_EXPR_ID var ⇒
+   opt_map ?? (preast_to_ast_var var e)
+    (λsigmaRes:(Σb.(Σt.ast_var e b t)).
+     match sigmaRes with [ sigma_intro b sigmaRes' ⇒
+      match sigmaRes' with [ sigma_intro t _ ⇒
+        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.(Σ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.(Σt.ast_var e b t))
+   with
+    [ true ⇒ λp:(checkb_desc_env e name = true).
+     let desc ≝ get_desc_env e name in
+     let b ≝ get_const_desc desc in
+     let t ≝ get_type_desc desc in
+     Some ? ≪b,≪t,(AST_VAR_ID e b t (AST_ID e name (checkbdescenv_to_checkdescenv e name p)))≫≫     
+    | false ⇒ λp:(checkb_desc_env e name = false).None ?
+    ] (refl_eq ? (checkb_desc_env e name))
 
-notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
-  right associative with precedence 20
-for @{ 'Sigma ${default
-  @{\lambda ${ident i} : $ty. $p}
-  @{\lambda ${ident i} . $p}}}.
+  | PREAST_VAR_ARRAY subVar expr ⇒
+   opt_map ?? (preast_to_ast_var subVar e)
+    (λ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 sigmaResV b (AST_TYPE_ARRAY subType dim))
+          (λresVar.
+           (* ASSERTO:
+              1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
+                 stato fatto dal parser, e qui controllo la condizione OUT_OF_BOUND
+              2) se l'indice non e' un'espressione riducibile ad un valore il controllo
+                 OUT_OF_BOUND sara' fatto a run time
+           *)
+           match (match expr with
+                  [ 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)
+              (λ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 ? ]]])
 
-notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
-  with precedence 20
-  for ${ default
-          @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}:$T.$acc)} } }
-          @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}.$acc)} } }
-       }.
+  | PREAST_VAR_STRUCT subVar field ⇒
+   opt_map ?? (preast_to_ast_var subVar e)
+    (λ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_STRUCT nelSubType ⇒
+         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.(Σ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)≫≫
+            | false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ?
+            ] (refl_eq ? (ltb field (len_neList ? nelSubType)))
+          )
+        | _ ⇒ None ? ]]])
+  ].
 
-notation "\ll term 19 a, break term 19 b \gg"
-with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
-interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
+(*
+ PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
+ PREAST_INIT_VAL_WORD16: word16 → preast_init_val
+ PREAST_INIT_VAL_WORD32: word32 → preast_init_val
+ PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
+ PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val
+*)
+definition preast_to_ast_init_val_aux_array :
+Πt.Πn.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)) → (aux_ast_init_type (AST_TYPE_ARRAY t (S n))) ≝
+λ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:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
 
-interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
+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.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
+  | PREAST_INIT_VAL_WORD16 val ⇒
+   Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
+  | PREAST_INIT_VAL_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.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.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.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.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.aux_ast_init_type t)
+               with
+                [ true ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = true).
+                 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 ?
+              ] (refl_eq ? (eq_ast_type t1 bType))
+            | _ ⇒ None ?
+            ]]]))
+     ] in aux nelSubVal
+
+  | PREAST_INIT_VAL_STRUCT nelSubVal ⇒
+   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.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.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.aux_ast_init_type t)
+             with
+              [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
+               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 ? ]]]))
+     ] in aux nelSubVal
+  ].
 
 (*
- PREAST_EXPR_BYTE8 : byte8 → preast_expr
- PREAST_EXPR_WORD16: word16 → preast_expr
- PREAST_EXPR_WORD32: word32 → preast_expr
- PREAST_EXPR_NEG: preast_expr → preast_expr
- PREAST_EXPR_NOT: preast_expr → preast_expr
- PREAST_EXPR_COM: preast_expr → preast_expr
- PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_B8toW16 : preast_expr → preast_expr
- PREAST_EXPR_B8toW32 : preast_expr → preast_expr
- PREAST_EXPR_W16toB8 : preast_expr → preast_expr
- PREAST_EXPR_W16toW32: preast_expr → preast_expr
- PREAST_EXPR_W32toB8 : preast_expr → preast_expr
- 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) ≝
- match preast with
-  [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8,AST_EXPR_BYTE8 e val≫
-  | _ ⇒ None ? (*
-  match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ Some ? (AST_EXPR_BYTE8 e val) | false ⇒ None ? ]
-  | PREAST_EXPR_WORD16 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
-   [ true ⇒ Some ? (AST_EXPR_WORD16 e val) | false ⇒ None ? ]
-  | PREAST_EXPR_WORD32 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
-   [ true ⇒ Some ? (AST_EXPR_WORD32 e val) | false ⇒ None ? ]
-  | PREAST_EXPR_NEG subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_NEG e t res))
-  | PREAST_EXPR_NOT subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_NOT e t res))
-  | PREAST_EXPR_COM subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_COM e t res))
-  | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
-     (λres2.Some ? (AST_EXPR_ADD e t res1 res2)))
-  | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
-     (λres2.Some ? (AST_EXPR_SUB e t res1 res2)))
-  | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
-     (λres2.Some ? (AST_EXPR_MUL e t res1 res2)))
-  | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
-     (λres2.Some ? (AST_EXPR_DIV e t res1 res2)))
-  | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
-     (λres2.Some ? (AST_EXPR_SHR e t res1 res2)))
-  | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
-   opt_map ?? (preast_to_ast_expr subExpr1 e t)
-    (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
-     (λres2.Some ? (AST_EXPR_SHL e t res1 res2)))
-  | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_GT e resType res1 res2))))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_GTE e resType res1 res2))))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_LT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_LT e resType res1 res2))))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_LTE e resType res1 res2))))   
-   | false ⇒ None ? ]
-  | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_EQ e resType res1 res2))))   
-   | false ⇒ None ? ]
-  | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
-             (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
-              (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
-               (λres2.Some ? (AST_EXPR_NEQ e resType res1 res2))))   
-   | false ⇒ None ? ]
-  | PREAST_EXPR_B8toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
-    (λres.Some ? (AST_EXPR_B8toW16 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_B8toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
-    (λres.Some ? (AST_EXPR_B8toW32 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_W16toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
-    (λres.Some ? (AST_EXPR_W16toB8 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_W16toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
-    (λres.Some ? (AST_EXPR_W16toW32 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_W32toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
-    (λres.Some ? (AST_EXPR_W32toB8 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_W32toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
-   [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
-    (λres.Some ? (AST_EXPR_W32toW16 e res))
-   | false ⇒ None ? ]
-  | PREAST_EXPR_ID var ⇒
-   opt_map ?? (evaluate_var_type var e)
-    (λcDesc.opt_map ?? (preast_to_ast_var var e (fst ?? cDesc) (AST_TYPE_BASE t))
-     (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t 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.
+ PREAST_INIT_VAR: preast_var → preast_init
+ PREAST_INIT_VAL: preast_init_val → preast_init
 *)
-and preast_to_ast_var (preast:preast_var) (e:aux_env_type) (c:bool) (t:ast_type) on preast : option (ast_var e c t) ≝
- None (ast_var e c t)
-(*
- PREAST_EXPR_BYTE8 : byte8 → preast_expr
- PREAST_EXPR_WORD16: word16 → preast_expr
- PREAST_EXPR_WORD32: word32 → preast_expr
- PREAST_EXPR_NEG: preast_expr → preast_expr
- PREAST_EXPR_NOT: preast_expr → preast_expr
- PREAST_EXPR_COM: preast_expr → preast_expr
- PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
- PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
- PREAST_EXPR_B8toW16 : preast_expr → preast_expr
- PREAST_EXPR_B8toW32 : preast_expr → preast_expr
- PREAST_EXPR_W16toB8 : preast_expr → preast_expr
- PREAST_EXPR_W16toW32: preast_expr → preast_expr
- PREAST_EXPR_W32toB8 : preast_expr → preast_expr
- PREAST_EXPR_W32toW16: preast_expr → preast_expr
- PREAST_EXPR_ID: preast_var → preast_expr
-*)
-and preast_to_ast_base_expr (preast:preast_expr) (e:aux_env_type) on preast : option (ast_base_expr e) ≝
- None (ast_base_expr e).
- 
+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.(Σ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.aux_ast_init_type t).
+    Some ? ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫)
+ ].
+
 (*
  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
  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_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_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
-  (* (A) assegnamento *)
   [ PREAST_STM_ASG var expr ⇒
-   opt_map ?? (evaluate_var_type var e)
-    (λcDesc.match fst ?? cDesc with
-     (* NO: left non deve essere read only *)
-     [ true ⇒ None ?
-     (* OK: left e' read write *)
-     | false ⇒
-      match isntb_ast_base_type (snd ?? cDesc)
-       return λx.(isntb_ast_base_type (snd ?? cDesc)) = x → option (ast_stm e)
-      with
-      (* (A.1) memcpy *)
-      [ true ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = true.match expr with
-       (* OK: right deve essere una var *)
-       [ PREAST_EXPR_ID subVar ⇒ opt_map ?? (evaluate_var_type subVar e)
-        (λcDesc'.opt_map ?? (preast_to_ast_var var e false (snd ?? cDesc))
-         (λresVar.opt_map ?? (preast_to_ast_var subVar e (fst ?? cDesc') (snd ?? cDesc))
-          (λresVar'.Some ? (AST_STM_MEMCPY_ASG e (fst ?? cDesc') (snd ?? cDesc)
-                                               (isntbastbasetype_to_isntastbasetype (snd ?? cDesc) p)
-                                               resVar resVar'))))
-       (* NO: right non e' una var *)
-       | _ ⇒ None ? ]
-      (* (A.2) variabile *)
-      | false ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = false.match snd ?? cDesc with
-       [ AST_TYPE_BASE bType ⇒ opt_map ?? (preast_to_ast_expr expr e bType)
-       (λresExpr.opt_map ?? (preast_to_ast_var var e false (AST_TYPE_BASE bType))
-        (λresVar.Some ? (AST_STM_ASG e bType resVar resExpr)))
-       | _ ⇒ None ? ]] (refl_eq ? (isntb_ast_base_type (snd ?? cDesc)))
-     ])
+   opt_map ?? (preast_to_ast_var var e)
+    (λ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_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)
+         )))]])
 
-  (* (B) while *)
   | 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)))
 
-  (* (C) if *)
   | 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)))
      ])
   ]
 (* 
  PREAST_NO_DECL: list preast_stm → preast_decl
- PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
+ PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
 *)
 and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
  match preast with
-  (* (A) nessuna dichiarazione, solo statement *)
   [ PREAST_NO_DECL lPreastStm ⇒
-   opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
-                                   (λh'.opt_map ?? t
-                                    (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)  
-    (λres.Some ? (AST_NO_DECL e res))
+    opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
+                                    (λh'.opt_map ?? t
+                                     (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)  
+     (λres.Some ? (AST_NO_DECL e res))
 
-  (* (B) dichiarazione *)
   | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
-   match checkb_not_already_def_env e decName 
-    return λx.(checkb_not_already_def_env e decName) = x → option (ast_decl e)
+   match checkb_not_already_def_env e decName
+    return λx.(checkb_not_already_def_env e decName = x) → option (ast_decl e)
    with
-    (* OK: non era gia' dichiarata *)
-    [ true ⇒ λp:(checkb_not_already_def_env e decName) = true.
-     match decType with
-      (* (B.1) dichiarazione tipo base *)
-      [ AST_TYPE_BASE decBaseType ⇒ match optInitExpr with
-       (* (B.1.1) tipo base senza inizializzazione *)
-       [ None ⇒ opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
-                 (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
-                                                (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
-                                                (None ?) subRes))
-       (* (B.1.2) tipo base con inizializzazione *)
-       | Some initExpr ⇒ opt_map ?? (preast_to_ast_expr initExpr e decBaseType)
-                          (λinitRes.opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
-                           (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
-                                                          (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
-                                                          (None ?) subRes)))
-       ]
-      (* (B.2) dichiarazione record/struttura *)
-      | _ ⇒ match optInitExpr with
-       (* OK: senza inizializzazione *)
-       [ None ⇒ match isntb_ast_base_type decType
-                 return λy.(isntb_ast_base_type decType) = y → option (ast_decl e)
-                with
-                 [ true ⇒ λp':(isntb_ast_base_type decType) = true.
-                  opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
-                 (λsubRes.Some ? (AST_DECL e constFlag decName decType
-                                           (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
-                                           (isntbastbasetype_to_isntastbasetype decType p')
-                                           subRes))
-                 | false ⇒ λp':(isntb_ast_base_type decType) = false.None ?
-                 ] (refl_eq ? (isntb_ast_base_type decType))
-       (* NO: con inizializzazione *)
-       | Some _ ⇒ None ?
-       ]
-      ]
-    (* NO: era gia' dichiarata *)
-    | false ⇒ λp:(checkb_not_already_def_env e decName) = false.None ?     
-    ] (refl_eq ? (checkb_not_already_def_env e decName))     
+    [ true ⇒ λp:(checkb_not_already_def_env e decName = true).
+     opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
+      (λdecl.match optInitExpr with
+       [ None ⇒ Some ? (AST_DECL e constFlag decName decType
+                                 (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (None ?) decl)
+       | Some initExpr ⇒
+        opt_map ?? (preast_to_ast_init initExpr e)
+         (λsigmaRes:(Σt:ast_type.ast_init e t).opt_map ?? (preast_to_ast_init_check e sigmaRes decType)
+          (λresInit.Some ? (AST_DECL e constFlag decName decType
+                                     (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (Some ? resInit) decl)))])
+    | false ⇒ λp:(checkb_not_already_def_env e decName = false).None ?
+    ] (refl_eq ? (checkb_not_already_def_env e decName))
   ].
 
 (*
- PREAST_ROOT: preast_decl → preast_root.
+ PREAST_ROOT: preast_decl → preast_root
 *)
 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;
+*)