+and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
+ (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
+ match ast
+ return λa:ast_base_expr d e.astfe_base_expr fe
+ with
+ [ AST_BASE_EXPR bType sExpr ⇒
+ ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+ ].
+
+let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
+ match ast
+ return λW.λa:astfe_expr fe W.astfe_expr fe' W
+ with
+ [ ASTFE_EXPR_BYTE8 val ⇒
+ ASTFE_EXPR_BYTE8 fe' val
+ | ASTFE_EXPR_WORD16 val ⇒
+ ASTFE_EXPR_WORD16 fe' val
+ | ASTFE_EXPR_WORD32 val ⇒
+ ASTFE_EXPR_WORD32 fe' val
+
+ | ASTFE_EXPR_NEG bType sExpr ⇒
+ ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_NOT bType sExpr ⇒
+ ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_COM bType sExpr ⇒
+ ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_AND fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_OR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_OR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_B8toW16 sExpr ⇒
+ ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_B8toW32 sExpr ⇒
+ ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W16toB8 sExpr ⇒
+ ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W16toW32 sExpr ⇒
+ ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W32toB8 sExpr ⇒
+ ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+ | ASTFE_EXPR_W32toW16 sExpr ⇒
+ ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_EXPR_ID b sType var ⇒
+ ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
+
+ ]
+and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
+ match ast
+ return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
+ with
+ [ ASTFE_VAR_ID sB sType sId ⇒
+ ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
+
+ | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
+ ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe)
+ (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
+
+ | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
+ ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe)
+ ]
+and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
+ d (e:aux_env_type d) (m:aux_map_type d) fe'
+ (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
+ match ast
+ return λa:astfe_base_expr fe.astfe_base_expr fe'
+ with
+ [ ASTFE_BASE_EXPR bType sExpr ⇒
+ ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)