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
(λ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)
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)
]
(*
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
(λ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))
].