1. new expressions AND, OR, XOR

2. constants must be initialized
3. bug fixed: the size n of an array means that the array
   has (n+1) elements. Thus the last valid index is n.

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
index c6d859c4e207a65c653a3e883af602bdb2bca09a..5d7a6a622a8ee0626614cc2294d2d9e009576e99 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma
@@ -87,6 +87,12 @@ qed.
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_SHL: ∀t:ast_base_type.
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_AND: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_OR:  ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_XOR: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 
 | AST_EXPR_GT : ∀t:ast_base_type.
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
@@ -148,6 +154,15 @@ let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
   | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
                            (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+  | AST_EXPR_AND bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+  | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 
   | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
@@ -260,6 +275,15 @@ let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
   | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+  | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
+   ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 
   | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
    ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
@@ -579,8 +603,10 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux
 (*
   AST_NO_DECL: ∀d.∀e:aux_env_type d.
                list (ast_stm d e) → ast_decl d e
-| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
-            (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e
+| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                  (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
+| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e
 *)
 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
                                                                        env_to_flatEnv_inv d e m fe →
@@ -613,40 +639,73 @@ and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_m
                               (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
                               resDimLe resLStm ]
 
-   | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
+   | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
+    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
+    match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
+          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+          (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
+     [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
+      AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
+                               ([ tripleT ??? sName true sType ]@resTrsf)
+                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
+                               ([ ASTFE_STM_INIT resFe true sType
+                                                 (* l'id e' sull'ambiente arricchito *)
+                                                 (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                         true sType
+                                                                         (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
+                                                                                          true sType
+                                                                                          (newid_from_init sD sE sName true sType)
+                                                                                          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                                          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
+                                                                                          (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
+                                                                         sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+                                                                         resMap resFe
+                                                                         (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                                                                         resDimLe)
+                                                 (* l'init e' sull'ambiente non arricchito *)
+                                                 (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
+                                                                           sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
+                                                                           resMap resFe
+                                                                           (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
+                                                                           (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
+                                ]@resLStm) ]
+
+   | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒
     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
-    match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl
-          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-          (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with
+    match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl
+          (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+          (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+          (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with
      [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
       AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
-                               ([ tripleT ??? sName sB sType ]@resTrsf)
-                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
-                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)
+                               ([ tripleT ??? sName false sType ]@resTrsf)
+                               (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+                               (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)
                                (match sOptInit with
                                 [ None ⇒ []
                                 | Some init ⇒
-                                 [ ASTFE_STM_INIT resFe sB sType
+                                 [ ASTFE_STM_INIT resFe false sType
                                                   (* l'id e' sull'ambiente arricchito *)
-                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                          sB sType
-                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType)
-                                                                                           sB sType
-                                                                                           (newid_from_init sD sE sName sB sType)
-                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
-                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv))
-                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                          false sType
+                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName false sType)
+                                                                                           false sType
+                                                                                           (newid_from_init sD sE sName false sType)
+                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
+                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv))
+                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
                                                                           resMap resFe
-                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
+                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
                                                                           resDimLe)
                                                   (* l'init e' sull'ambiente non arricchito *)
                                                   (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
-                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
+                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
                                                                             resMap resFe
-                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
-                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe))
+                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
+                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe))
                                  ]]@resLStm) ]          
 
    ].

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
index 553991bd79c53c5b08bd04f61b1dc25ee31af9f6..8ee77aeb12d70e9272d7353ee5131e206dafea89 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma
@@ -57,6 +57,12 @@ inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
 | AST_EXPR_SHL: ∀t:ast_base_type.
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_AND: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_OR:  ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
+| AST_EXPR_XOR: ∀t:ast_base_type.
+                ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
 
 | AST_EXPR_GT : ∀t:ast_base_type.
                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
@@ -147,8 +153,10 @@ inductive ast_stm : Πd:nat.aux_env_type d → Type ≝
 with ast_decl : Πd:nat.aux_env_type d → Type ≝
   AST_NO_DECL: ∀d.∀e:aux_env_type d.
                list (ast_stm d e) → ast_decl d e
-| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
-            (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e.
+| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                  (* D *) (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
+| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
+                (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e.
 
 (* -------------------------- *)
 

diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
index 2690b2466f8e85895d50f9a0b2574bcf8933a552..626248685c758df6a297f36644b091ee913861c1 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma
@@ -57,6 +57,12 @@ inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝
                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
 | ASTFE_EXPR_SHL: ∀t:ast_base_type.
                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_AND: ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_OR:  ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
+| ASTFE_EXPR_XOR: ∀t:ast_base_type.
+                  astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
 
 | ASTFE_EXPR_GT : ∀t:ast_base_type.
                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)

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 a5db9536b9bfbb31c284fb9b65e7791ac3a87962..d129991687ec5a66ec9b0971834937a748a79b76 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma
@@ -102,6 +102,9 @@ definition preast_to_ast_var_check ≝
  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_AND: preast_expr → preast_expr → preast_expr
+ PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr
+ PREAST_EXPR_XOR: 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
@@ -208,6 +211,36 @@ let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on pr
          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
           (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫))
        | _ ⇒ None ? ]))
+  | PREAST_EXPR_AND subExpr1 subExpr2 ⇒
+   opt_map ?? (preast_to_ast_expr subExpr1 d e)
+    (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+     (λsigmaRes2:(Σt.ast_expr d e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_AND d e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
+  | PREAST_EXPR_OR subExpr1 subExpr2 ⇒
+   opt_map ?? (preast_to_ast_expr subExpr1 d e)
+    (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+     (λsigmaRes2:(Σt.ast_expr d e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_OR d e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
+  | PREAST_EXPR_XOR subExpr1 subExpr2 ⇒
+   opt_map ?? (preast_to_ast_expr subExpr1 d e)
+    (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+     (λsigmaRes2:(Σt.ast_expr d e t).
+      match (sigmaFst ?? sigmaRes1) with
+       [ AST_TYPE_BASE bType ⇒
+        opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+         (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+          (λres2.Some ? ≪?,(AST_EXPR_XOR d e ? res1 res2)≫))
+       | _ ⇒ None ? ]))
 
   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
    opt_map ?? (preast_to_ast_expr subExpr1 d e)
@@ -338,9 +371,9 @@ and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast :
                  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)
+                  [ 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 d e)
@@ -528,7 +561,8 @@ let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on prea
   ]
 (* 
  PREAST_NO_DECL: list preast_stm → preast_decl
- PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
+ PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
+ PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
 *)
 and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝
  match preast with
@@ -538,20 +572,33 @@ and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast
                                      (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)  
      (λres.Some ? (AST_NO_DECL d e res))
 
-  | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
+  | PREAST_CONST_DECL decName decType initExpr subPreastDecl ⇒
+   match checkb_not_already_def_env d e decName
+    return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
+   with
+    [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
+     opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName true decType))
+      (λdecl.opt_map ?? (preast_to_ast_init initExpr d e)
+       (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
+        (λresInit.Some ? (AST_CONST_DECL d e decName decType
+                                         (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) resInit decl))))
+    | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
+    ] (refl_eq ? (checkb_not_already_def_env d e decName))
+
+  | PREAST_VAR_DECL decName decType optInitExpr subPreastDecl ⇒
    match checkb_not_already_def_env d e decName
     return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
    with
     [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
-     opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName constFlag decType))
+     opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName false decType))
       (λdecl.match optInitExpr with
-       [ None ⇒ Some ? (AST_DECL d e constFlag decName decType
-                                 (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl)
+       [ None ⇒ Some ? (AST_VAR_DECL d e decName decType
+                                     (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl)
        | Some initExpr ⇒
         opt_map ?? (preast_to_ast_init initExpr d e)
          (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
-          (λresInit.Some ? (AST_DECL d e constFlag decName decType
-                                     (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))])
+          (λresInit.Some ? (AST_VAR_DECL d e decName decType
+                                         (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))])
     | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
     ] (refl_eq ? (checkb_not_already_def_env d e decName))
   ].

diff --git a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
index 9a463d1b65cd055541bce891cfd4f2b243ec4a5f..6ad8c3d62e8834a1f6c65a8a900277a7f4701d63 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
@@ -42,6 +42,9 @@ inductive preast_expr : Type ≝
 | 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_AND: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_OR:  preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
 
 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
@@ -95,7 +98,8 @@ 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_init → preast_decl → preast_decl.
+| PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
+| PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
 
 (* -------------------------- *)