-let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) (t:ast_base_type) on preast : option (ast_expr e t) ≝
- (*match preast
- return λpr:preast_expr.λen:aux_env_type.λtp:ast_base_type.(match pr with
- [ PREAST_EXPR_BYTE8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_WORD16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_WORD32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_NEG _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_NOT _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_COM _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_ADD _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SUB _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_MUL _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_DIV _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SHR _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_SHL _ ⇒ option (ast_expr en tp)
- | PREAST_EXPR_GT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_GTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_LT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_LTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_EQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_NEQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_B8toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_B8toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_W16toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_W16toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
- | PREAST_EXPR_W32toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
- | PREAST_EXPR_W32toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
- | PREAST_EXPR_ID _ ⇒ option (ast_expr en tp)
- | _ ⇒ option (ast_expr en tp)
- ])
- with
- [ PREAST_EXPR_BYTE8 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with