-let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_expr fe t) ≝
- match ast with
- [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
- | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
- | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
-
- | AST_EXPR_NEG bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
- | AST_EXPR_NOT bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
- | AST_EXPR_COM bType subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
-
- | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
- | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
- | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
- | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
- | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
- | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
-
- | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
- | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
- | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
- | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
- | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
- | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
- (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
- (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
-
- | AST_EXPR_B8toW16 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
- | AST_EXPR_B8toW32 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
- | AST_EXPR_W16toB8 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
- | AST_EXPR_W16toW32 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
- | AST_EXPR_W32toB8 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
- | AST_EXPR_W32toW16 subExpr ⇒
- opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
- (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
-
- | AST_EXPR_ID b subType var ⇒
- opt_map ?? (ast_to_astfe_var e b subType var fe map)
- (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
+let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
+ (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
+ match ast
+ return λW.λa:ast_expr d e W.astfe_expr fe W
+ with
+ [ AST_EXPR_BYTE8 val ⇒
+ ASTFE_EXPR_BYTE8 fe val
+ | AST_EXPR_WORD16 val ⇒
+ ASTFE_EXPR_WORD16 fe val
+ | AST_EXPR_WORD32 val ⇒
+ ASTFE_EXPR_WORD32 fe val
+
+ | AST_EXPR_NEG bType sExpr ⇒
+ ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+ | AST_EXPR_NOT bType sExpr ⇒
+ ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+ | AST_EXPR_COM bType sExpr ⇒
+ ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
+
+ | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+ | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
+ | AST_EXPR_AND bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+
+ | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+ | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
+ ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
+ (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
+
+ | AST_EXPR_B8toW16 sExpr ⇒
+ ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+ | AST_EXPR_B8toW32 sExpr ⇒
+ ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
+ | AST_EXPR_W16toB8 sExpr ⇒
+ ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+ | AST_EXPR_W16toW32 sExpr ⇒
+ ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
+ | AST_EXPR_W32toB8 sExpr ⇒
+ ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+ | AST_EXPR_W32toW16 sExpr ⇒
+ ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
+
+ | AST_EXPR_ID b sType var ⇒
+ ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
+