From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Jul 2008 14:23:01 +0000 (+0000)
Subject: Snapshot.
X-Git-Tag: make_still_working~4911
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4924f99796029eecb58e920ca7a6a366efe2373e;p=helm.git

Snapshot.
---

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
index 381ea92fb..79be3a54e 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -81,29 +81,72 @@ inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
 | AST_EXPR_ID: ∀b:bool.∀t:ast_base_type.
                ast_var e b (AST_TYPE_BASE t) → ast_expr e t
 
-(* espressioni generalizzate: anche non uniformi per tipo *)
-with ast_base_expr : Type ≝
-  AST_BASE_EXPR: ∀t:ast_base_type.
-                 ast_expr e t → ast_base_expr e
-
 (* variabile: modificatori di array/struct dell'id *)
 with ast_var : bool → ast_type → Type ≝
   AST_VAR_ID: ∀b:bool.∀t:ast_type.
               ast_id e b t → ast_var e b t
-                 (* NB: l'index out of bound e' delegato a runtime? *)
 | 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) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n).
+                  ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
+
+(* espressioni generalizzate: anche non uniformi per tipo *)
+with ast_base_expr : Type ≝
+  AST_BASE_EXPR: ∀t:ast_base_type.
+                 ast_expr e t → ast_base_expr e.
+
+(* -------------------------- *)
+
+(* espressioni destre di assegnamento *)
+inductive ast_right_expr (e:aux_env_type) : ast_type → Type ≝
+  AST_RIGHT_EXPR_BASE: ∀t:ast_base_type.
+                       ast_expr e t → ast_right_expr e (AST_TYPE_BASE t)
+| AST_RIGHT_EXPR_VAR: ∀b:bool.∀t:ast_type.
+                      ast_var e b t → ast_right_expr e t.
+
+(* -------------------------- *)
+
+let rec aux_ast_init_type (t:ast_type) on t : Type ≝
+ match t with
+  [ AST_TYPE_BASE bType ⇒ match bType with
+   [ AST_BASE_TYPE_BYTE8 ⇒ byte8
+   | AST_BASE_TYPE_WORD16 ⇒ word16
+   | AST_BASE_TYPE_WORD32 ⇒ word32
+   ] 
+  | AST_TYPE_ARRAY subType dim ⇒
+   let T ≝ aux_ast_init_type subType in
+   let rec aux (n:nat) on n ≝
+    match n with
+     [ O ⇒ T
+     | S n' ⇒ Prod T (aux n')
+     ] in
+   aux dim 
+  | AST_TYPE_STRUCT nelSubType ⇒
+   let rec aux (nel:ne_list ast_type) on nel ≝
+    match nel with
+     [ ne_nil h ⇒ aux_ast_init_type h
+     | ne_cons h t ⇒ Prod (aux_ast_init_type h) (aux t)
+     ] in
+    aux nelSubType 
+  ].
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+  1) var1 = var2
+  2) var = ... valori ...
+*) 
+inductive ast_init (e:aux_env_type) : ast_type → Type ≝
+  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.
 
 (* -------------------------- *)
 
 (* statement: assegnamento/while/if else if else *)
 inductive ast_stm : aux_env_type → Type ≝
-  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_base_type.
-               ast_var e false (AST_TYPE_BASE t) → ast_expr e t → ast_stm e
-| AST_STM_MEMCPY_ASG: ∀e:aux_env_type.∀b:bool.∀t:ast_type.
-                      (* D *) isnt_ast_base_type t → ast_var e false t → ast_var e b t → ast_stm e
+  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
+               ast_var e false t → ast_right_expr e t → ast_stm e
 | AST_STM_WHILE: ∀e:aux_env_type.
                  ast_base_expr e → ast_decl e → ast_stm e
 | AST_STM_IF: ∀e:aux_env_type.
@@ -113,10 +156,8 @@ inductive ast_stm : aux_env_type → Type ≝
 with ast_decl : aux_env_type → Type ≝
   AST_NO_DECL: ∀e:aux_env_type.
                list (ast_stm e) → ast_decl e
-| AST_BASE_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_base_type.
-                 (* D *) (check_not_already_def_env e str) → option (ast_expr e t) → ast_decl (add_desc_env e str c (AST_TYPE_BASE t)) → ast_decl e
 | AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
-            (* D *) (check_not_already_def_env e str) → (* D *) isnt_ast_base_type t → ast_decl (add_desc_env e str c t) → ast_decl e.
+            (* D *) (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e.
 
 (* -------------------------- *)
 
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..49fabf83e 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -21,164 +21,22 @@
 
 include "compiler/preast_tree.ma".
 include "compiler/ast_tree.ma".
-
-(* *********************** *)
-(* PASSO 1 DI COMPILAZIONE *)
-(* *********************** *)
-
-(*
- 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.
-*)
-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 ? ])
-  ].
-
-(*
- 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 evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : option ast_base_type ≝
- 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_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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ]))
-  | 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 ? ])
-  | 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 ? ])
-  | 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 ? ])
-  | 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 ? ])
-  | 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 ? ])
-  | 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 ? ])
-  ].
-
-inductive sigma (A:Type) (P:A \to Type) : Type \def
-    sigma_intro: \forall x:A. P x \to sigma A P.
-
-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}}}.
-
-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)} } }
-       }.
-
-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).
-
-
-interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
-
+include "compiler/sigma.ma".
+
+(* ************************* *)
+(* PASSO 1 : da PREAST a AST *)
+(* ************************* *)
+
+lemma pippo : ∀t1,t2:ast_base_type.
+              (eq_ast_base_type t1 t2 = true) → (t1 = t2).
+ unfold eq_ast_base_type;
+ intros;
+ elim t1 in H:(%);
+ elim t2 in H:(%);
+ normalize in H:(%);
+ try reflexivity;
+ destruct H;
+qed.
 
 (*
  PREAST_EXPR_BYTE8 : byte8 → preast_expr
@@ -207,265 +65,79 @@ interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  PREAST_EXPR_ID: preast_var → preast_expr
 *)
+definition preast_to_ast_expr_check ≝
+ λe:aux_env_type.λv:Σt'.ast_expr e t'.λt:ast_base_type.
+    match v with
+     [ sigma_intro t' expr ⇒
+         match eq_ast_base_type t' t
+         return λb.eq_ast_base_type t' t = b → option (ast_expr e t)
+         with
+          [ true ⇒ λp.Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (pippo ?? p))
+          | false ⇒ λp.None ?
+          ] (refl_eq ? (eq_ast_base_type t' t))
+     ].
+     
 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 ? ]
+   (* in pretty print diventa Some ? "≪AST_BASE_TYPE_BYTE8,AST_EXPR_BYTE8 e val≫" *)
+  [ 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_NEG subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_NEG e t res))
+   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)≫)
   | PREAST_EXPR_NOT subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_NOT e t res))
+   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)≫)
   | PREAST_EXPR_COM subExpr ⇒
-   opt_map ?? (preast_to_ast_expr subExpr e t)
-    (λres.Some ? (AST_EXPR_COM e t res))
+   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)≫)
   | 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)))*)
+   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≫))))
+  | _ ⇒ None ?
   ]
+
 (*
  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) (c:bool) (t:ast_type) on preast : option (ast_var e c t) ≝
- None (ast_var e c t)
+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) ≝
+ None ?.
+
 (*
- 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
+ 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.
 *)
-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).
- 
+let rec preast_to_ast_init_val (preast:preast_init_val) (e:aux_env_type) on preast : option (sigma ast_type (ast_init e)) ≝
+ None ?.
+
+(*
+ PREAST_INIT_VAR: preast_var → preast_init
+ PREAST_INIT_VAL: preast_init_val → preast_init.
+*)
+definition preast_to_ast_init : preast_init → Πe:aux_env_type.option (sigma ast_type (ast_init e)) ≝
+λpreast:preast_init.λe:aux_env_type.None ?.
+
 (*
  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
 *)
 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)))
-     ])
-
-  (* (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)
-     (λ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)
-                                      (λ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 ?)))))
-                                    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)
-      (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
-     ])
-  ]
+ None ?
 (* 
  PREAST_NO_DECL: list preast_stm → preast_decl
  PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → 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))
-
-  (* (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)
-   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))     
-  ].
+ None ?.
 
 (*
  PREAST_ROOT: preast_decl → preast_root.
diff --git a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
index fcc1fbf4a..662d289fb 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
@@ -69,6 +69,25 @@ with preast_var : Type ≝
 
 (* -------------------------- *)
 
+(* inizializzatori: ... valori ... *)
+inductive preast_init_val : Type ≝
+  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.
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+  1) var1 = var2
+  2) var = ... valori ...
+*)
+inductive preast_init : Type ≝
+  PREAST_INIT_VAR: preast_var → preast_init
+| PREAST_INIT_VAL: preast_init_val → preast_init.
+
+(* -------------------------- *)
+
 (* statement: assegnamento/while/if else if else *)
 inductive preast_stm : Type ≝
   PREAST_STM_ASG: preast_var → preast_expr → preast_stm
@@ -78,7 +97,7 @@ inductive preast_stm : Type ≝
 (* dichiarazioni *)
 with preast_decl : Type ≝
   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.
 
 (* -------------------------- *)
 
diff --git a/helm/software/matita/contribs/assembly/compiler/sigma.ma b/helm/software/matita/contribs/assembly/compiler/sigma.ma
new file mode 100755
index 000000000..b43e4bbb1
--- /dev/null
+++ b/helm/software/matita/contribs/assembly/compiler/sigma.ma
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                                                                        *)
+(* Sviluppato da:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+(* coppia dipendente *)
+
+inductive sigma (A:Type) (P:A → Type) : Type ≝
+    sigma_intro: ∀x:A.P x → sigma A P.
+
+notation < "hvbox(\Sigma ident i opt (: tx) break . p)"
+  right associative with precedence 20
+for @{ 'Sigma ${default
+  @{\lambda ${ident i} : $tx. $p}  
+  @{\lambda ${ident i} . $p}}}.
+
+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)} } }
+       }.
+
+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).
+
+interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
+
+definition sigmaFst ≝
+λT:Type.λf:T → Type.λs:sigma T f.match s with [ sigma_intro x _ ⇒ x ].
+definition sigmaSnd ≝
+λT:Type.λf:T → Type.λs:sigma T f.match s return λs.f (sigmaFst ?? s) with [ sigma_intro _ x ⇒ x ].
+
+(* tripla dipendente, suggerimento \SHcy *)
+
+inductive bisigma (A,B:Type) (P:A → B → Type) : Type ≝
+    bisigma_intro: ∀x:A.∀y:B.P x y → bisigma A B P.
+
+definition bisigmaFst ≝
+λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro x _ _ ⇒ x ].
+definition bisigmaSnd ≝
+λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s with [ bisigma_intro _ x _ ⇒ x ].
+definition bisigmaThd ≝
+λT1,T2:Type.λf:T1 → T2 → Type.λs:bisigma T1 T2 f.match s return λs.f (bisigmaFst ??? s) (bisigmaSnd ??? s) with [ bisigma_intro _ _ x ⇒ x ].