1. new expressions AND, OR, XOR

[helm.git] / helm / software / matita / contribs / assembly / compiler / preast_to_ast.ma

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))
   ].