- 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 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 ? ]
- | PREAST_EXPR_NEG subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_NEG e t res))
- | PREAST_EXPR_NOT subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_NOT e t res))
- | PREAST_EXPR_COM subExpr ⇒
- opt_map ?? (preast_to_ast_expr subExpr e t)
- (λres.Some ? (AST_EXPR_COM e t res))
- | 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)))*)
- ]
-(*
- 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.