From f2d9db85559c7a8db11aae1153495fae4a258d54 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Jul 2008 10:11:49 +0000
Subject: [PATCH] Semantic analysis implemented (sort of).

---
 .../contribs/assembly/compiler/ast_tree.ma    |   2 +-
 .../contribs/assembly/compiler/ast_type.ma    |  47 ++
 .../assembly/compiler/preast_to_ast.ma        | 445 ++++++++++++++++--
 .../contribs/assembly/compiler/sigma.ma       |  12 -
 .../contribs/assembly/freescale/extra.ma      |  10 +
 5 files changed, 458 insertions(+), 58 deletions(-)

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
index 79be3a54e..6fa1b3ffd 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -28,7 +28,7 @@ include "compiler/environment.ma".
 (* id: accesso all'ambiente con stringa *)
 inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
   AST_ID: ∀str:aux_str_type.
-          (* D *) check_desc_env e str → ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)).
+          (* D *) (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))).
 
 (* -------------------------- *)
 
diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
index 5939fe4f4..8ad0220ff 100755
--- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
@@ -47,6 +47,16 @@ definition eq_ast_base_type ≝
   [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
  ].
 
+lemma eqastbasetype_to_eq : ∀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.
+
 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
  match t1 with
   [ AST_TYPE_BASE bType1 ⇒ match t2 with
@@ -65,6 +75,43 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
    | _ ⇒ false ]
   ].
 
+lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
+ do 2 intro;
+ cases t1; cases t2;
+ [ 2,3,4,6,7,8: normalize; intro; destruct H
+ | 1: change in ⊢ (? ? % ?→?) with (eq_ast_base_type a a1);
+      intro;
+      apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
+ | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1));
+      intro;
+      cut (a = a1 ∧ n = n1);
+      elim daemon.
+ | 9: elim daemon
+ ].
+qed.
+
+(* PERCHE' ??
+ se in testa includo
+ include "demo/natural_deduction.ma".
+ la dimostrazione va fino in fondo ma poi impazzisce ast_tree.ma
+ dicendo che la dichiarazione ast_id e' scorretta
+ 
+      [ 1: alias id "And_elim_l" = "cic:/matita/demo/natural_deduction/And_elim_l.con".
+           alias id "And_elim_r" = "cic:/matita/demo/natural_deduction/And_elim_r.con".
+           apply (eq_f2 ??? (λx.λy.? x y) a a1 n n1 (And_elim_l ?? Hcut) (And_elim_r ?? Hcut))
+      | 2: split;
+           [ 2: apply (eqb_true_to_eq n n1 (andb_true_true_r ?? H))
+           | 1: cut (eq_ast_Type a a1 = true);
+                [ 2: apply (andb_true_true ?? H)
+                | 1: TODO elim daemon
+                ]
+           ]
+      ]
+ | 9: TODO elim daemon
+ ]
+qed.
+*)
+
 definition is_ast_base_type ≝
 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
 
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 49fabf83e..27c1e5477 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -27,16 +27,67 @@ 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.
+(* 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.
+ 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)
+  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))
+   | 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
@@ -65,82 +116,386 @@ qed.
  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
-   (* 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_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)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_NEG e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
+    (λ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)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_NOT e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
+    (λ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)
-    (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_COM e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
+    (λ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)
     (λ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 ?
-  ]
+      (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_ADD e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+  | 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)≫)))
+  | 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)≫)))
+  | 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)≫)))
+
+  | 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)≫)))
+  | 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)≫)))
+
+  | 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)≫)))
+  | 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)≫)))
+  | 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)≫)))
+  | 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)≫)))
+  | 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)≫)))
+  | 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)≫)))
 
+  | 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)≫))
+  | 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)≫))
+  | 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)≫))
+  | 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)≫))
+  | 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)≫))
+  | 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)≫))
+
+  | PREAST_EXPR_ID var ⇒
+   opt_map ?? (preast_to_ast_var var 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 _ ⇒
+       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 ? ]]])
+  ]
 (*
  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_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) ≝
- None ?.
+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)) ≝
+ 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))
+   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))
+
+  | 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 _ ⇒
+       match t with
+        [ AST_TYPE_ARRAY subType dim ⇒
+         opt_map ?? (preast_to_ast_var_check e sigmaRes 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.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)
+                  | _ ⇒ (λ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))≫≫ ])
+            | 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)).
+     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:bool.(Σt:ast_type.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 ? ]]])
+  ].
 
 (*
  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.
+ PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val
 *)
-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 ?.
+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.
+
+let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt:ast_type.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≫
+  | PREAST_INIT_VAL_WORD16 val ⇒
+   Some (Σt:ast_type.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≫
+
+  | 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) ≝
+    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≫ ])
+     | 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).
+         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)
+             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)
+               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'))))≫
+                | 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:ast_type.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≫ ])
+     | 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).
+         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)
+             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))))≫
+              | 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_INIT_VAR: preast_var → preast_init
- PREAST_INIT_VAL: preast_init_val → 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 ?.
+definition preast_to_ast_init : preast_init → Πe.option (Σt:ast_type.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)))≫)
+
+ | 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))≫)
+ ].
 
 (*
  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_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))).
+
 let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
- None ?
+ 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)).
+    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)
+         (λ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)
+     (λ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)
+                                      (λ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)))
+     ])
+  ]
 (* 
  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) ≝
- None ?.
+ match preast with
+  [ 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))
+
+  | 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
+    [ 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
diff --git a/helm/software/matita/contribs/assembly/compiler/sigma.ma b/helm/software/matita/contribs/assembly/compiler/sigma.ma
index b43e4bbb1..491d31e00 100755
--- a/helm/software/matita/contribs/assembly/compiler/sigma.ma
+++ b/helm/software/matita/contribs/assembly/compiler/sigma.ma
@@ -47,15 +47,3 @@ 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 ].
diff --git a/helm/software/matita/contribs/assembly/freescale/extra.ma b/helm/software/matita/contribs/assembly/freescale/extra.ma
index bc76c4d6b..25e0cb6fa 100644
--- a/helm/software/matita/contribs/assembly/freescale/extra.ma
+++ b/helm/software/matita/contribs/assembly/freescale/extra.ma
@@ -54,6 +54,16 @@ definition eq_bool ≝
  [ true ⇒ b2
  | false ⇒ not_bool b2 ].
 
+lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
+ unfold eq_bool;
+ intros;
+ elim b1 in H:(%);
+ elim b2 in H:(%);
+ normalize in H:(%);
+ try reflexivity;
+ destruct H.
+qed.
+
 (* \ominus *)
 notation "hvbox(⊖ a)" non associative with precedence 36
  for @{ 'not_bool $a }.
-- 
2.39.2