+let rec retype_expr (fe:aux_flatEnv_type) (t:ast_type) (ast:astfe_expr fe t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_expr fe' t) ≝
+ match ast with
+ [ ASTFE_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' val) t
+ | ASTFE_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe' val) t
+ | ASTFE_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe' val) t
+
+ | ASTFE_EXPR_NEG bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe' bType res) t)
+ | ASTFE_EXPR_NOT bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe' bType res) t)
+ | ASTFE_EXPR_COM bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe' bType res) t)
+
+ | ASTFE_EXPR_ADD bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe' bType res1 res2) t))
+ | ASTFE_EXPR_SUB bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe' bType res1 res2) t))
+ | ASTFE_EXPR_MUL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe' bType res1 res2) t))
+ | ASTFE_EXPR_DIV bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe' bType res1 res2) t))
+ | ASTFE_EXPR_SHR bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe' bType res1 res2) t))
+ | ASTFE_EXPR_SHL bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe' bType res1 res2) t))
+
+ | ASTFE_EXPR_LT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe' bType res1 res2) t))
+ | ASTFE_EXPR_LTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe' bType res1 res2) t))
+ | ASTFE_EXPR_GT bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe' bType res1 res2) t))
+ | ASTFE_EXPR_GTE bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe' bType res1 res2) t))
+ | ASTFE_EXPR_EQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe' bType res1 res2) t))
+ | ASTFE_EXPR_NEQ bType subExpr1 subExpr2 ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr1 fe' dim)
+ (λres1.opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr2 fe' dim)
+ (λres2.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe' bType res1 res2) t))
+
+ | ASTFE_EXPR_B8toW16 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe' res) t)
+ | ASTFE_EXPR_B8toW32 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe' res) t)
+ | ASTFE_EXPR_W16toB8 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe' res) t)
+ | ASTFE_EXPR_W16toW32 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe' res) t)
+ | ASTFE_EXPR_W32toB8 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe' res) t)
+ | ASTFE_EXPR_W32toW16 subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe' dim)
+ (λres.ast_to_astfe_expr_check fe' (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe' res) t)
+
+ | ASTFE_EXPR_ID b subType var ⇒
+ opt_map ?? (retype_var fe b subType var fe' dim)
+ (λres.ast_to_astfe_expr_check fe' subType (ASTFE_EXPR_ID fe' b subType res) t)
+ ]
+and retype_var (fe:aux_flatEnv_type) (b:bool) (t:ast_type) (ast:astfe_var fe b t) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_var fe' b t) ≝
+ match ast with
+ [ ASTFE_VAR_ID subB subType subId ⇒
+ opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType)
+ (λresId.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ID fe' subB subType resId) b t)
+
+ | ASTFE_VAR_ARRAY subB subType n var expr ⇒
+ opt_map ?? (retype_var fe subB (AST_TYPE_ARRAY subType n) var fe' dim)
+ (λresVar.opt_map ?? (retype_base_expr fe expr fe' dim)
+ (λresExpr.ast_to_astfe_var_check fe' subB subType (ASTFE_VAR_ARRAY fe' subB subType n resVar resExpr) b t))
+
+ | ASTFE_VAR_STRUCT subB nelSubType field var ⇒
+ opt_map ?? (retype_var fe subB (AST_TYPE_STRUCT nelSubType) var fe' dim)
+ (λres.ast_to_astfe_var_check fe' subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe' subB nelSubType field res) b t)
+ ]
+and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_base_expr fe') ≝
+ match ast with
+ [ ASTFE_BASE_EXPR bType subExpr ⇒
+ opt_map ?? (retype_expr fe (AST_TYPE_BASE bType) subExpr fe' dim)
+ (λres.Some ? (ASTFE_BASE_EXPR fe' bType res))
+ ].
+