X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fast_to_astfe.ma;h=90a59130a9e1064b1baaf6972ee175cd544892c9;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=d6eadfdb82820b41bca28456742a59bdad6e9fb2;hpb=55e5bef77f163b29feeb9ad4e83376c5aa301297;p=helm.git diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma index d6eadfdb8..90a59130a 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -26,754 +26,692 @@ include "compiler/sigma.ma". (* PASSO 2 : da AST a ASTFE *) (* ************************ *) -(* operatore di cast *) -definition ast_to_astfe_expr_check : Πfe.Πt.astfe_expr fe t → Πt'.option (astfe_expr fe t') ≝ -λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_expr fe t.λt':ast_type. - match eq_ast_type t t' - return λx.(eq_ast_type t t' = x) → ? - with - [ true ⇒ λp:(eq_ast_type t t' = true). - Some ? (eq_rect ? t (λt.astfe_expr fe t) ast t' (eqasttype_to_eq ?? p)) - | false ⇒ λp:(eq_ast_type t t' = false).None ? - ] (refl_eq ? (eq_ast_type t t')). - -definition ast_to_astfe_init_check : Πfe.Πt.astfe_init fe t → Πt'.option (astfe_init fe t') ≝ -λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λt':ast_type. - match eq_ast_type t t' - return λx.(eq_ast_type t t' = x) → ? - with - [ true ⇒ λp:(eq_ast_type t t' = true). - Some ? (eq_rect ? t (λt.astfe_init fe t) ast t' (eqasttype_to_eq ?? p)) - | false ⇒ λp:(eq_ast_type t t' = false).None ? - ] (refl_eq ? (eq_ast_type t t')). - -definition ast_to_astfe_var_checkb : Πfe.Πb.Πt.astfe_var fe b t → Πb'.option (astfe_var fe b' t) ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool. - match eq_bool b b' - return λx.(eq_bool b b' = x) → ? - with - [ true ⇒ λp:(eq_bool b b' = true). - Some ? (eq_rect ? b (λb.astfe_var fe b t) ast b' (eqbool_to_eq ?? p)) - | false ⇒ λp:(eq_bool b b' = false).None ? - ] (refl_eq ? (eq_bool b b')). - -definition ast_to_astfe_var_checkt : Πfe.Πb.Πt.astfe_var fe b t → Πt'.option (astfe_var fe b t') ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λt':ast_type. - match eq_ast_type t t' - return λx.(eq_ast_type t t' = x) → ? - with - [ true ⇒ λp:(eq_ast_type t t' = true). - Some ? (eq_rect ? t (λt.astfe_var fe b t) ast t' (eqasttype_to_eq ?? p)) - | false ⇒ λp:(eq_ast_type t t' = false).None ? - ] (refl_eq ? (eq_ast_type t t')). - -definition ast_to_astfe_var_check : Πfe.Πb.Πt.astfe_var fe b t → Πb'.Πt'.option (astfe_var fe b' t') ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_var fe b t.λb':bool.λt':ast_type. - opt_map ?? (ast_to_astfe_var_checkb fe b t ast b') - (λres.opt_map ?? (ast_to_astfe_var_checkt fe b' t res t') - (λres'.Some ? res')). - -definition ast_to_astfe_id_checkb : Πfe.Πb.Πt.astfe_id fe b t → Πb'.option (astfe_id fe b' t) ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool. - match eq_bool b b' - return λx.(eq_bool b b' = x) → ? - with - [ true ⇒ λp:(eq_bool b b' = true). - Some ? (eq_rect ? b (λb.astfe_id fe b t) ast b' (eqbool_to_eq ?? p)) - | false ⇒ λp:(eq_bool b b' = false).None ? - ] (refl_eq ? (eq_bool b b')). - -definition ast_to_astfe_id_checkt : Πfe.Πb.Πt.astfe_id fe b t → Πt'.option (astfe_id fe b t') ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λt':ast_type. - match eq_ast_type t t' - return λx.(eq_ast_type t t' = x) → ? - with - [ true ⇒ λp:(eq_ast_type t t' = true). - Some ? (eq_rect ? t (λt.astfe_id fe b t) ast t' (eqasttype_to_eq ?? p)) - | false ⇒ λp:(eq_ast_type t t' = false).None ? - ] (refl_eq ? (eq_ast_type t t')). - -definition ast_to_astfe_id_check : Πfe.Πb.Πt.astfe_id fe b t → Πb'.Πt'.option (astfe_id fe b' t') ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λb':bool.λt':ast_type. - opt_map ?? (ast_to_astfe_id_checkb fe b t ast b') - (λres.opt_map ?? (ast_to_astfe_id_checkt fe b' t res t') - (λres'.Some ? res')). - (* - AST_ID: ∀str:aux_str_type. - (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))) + AST_ID: ∀str:aux_str_type. + (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str))) *) -definition get_name_ast_id ≝ -λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t. - match ast with [ AST_ID s _ ⇒ s ]. - -definition ast_to_astfe_id : - Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type. - Πmap:aux_trasfMap_type e fe. - astfe_id fe - (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) - (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))) ≝ -λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe. - ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast)) - (ast_to_astfe_id_aux e fe map (get_name_ast_id e b t ast) - (ast_id_ind e - (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:ast_id e Hbeta3 Hbeta2.check_desc_env e (get_name_ast_id e Hbeta3 Hbeta2 Hbeta1)) - (λa:aux_str_type.λH:check_desc_env e a.H) b t ast)). - -definition get_name_astfe_id ≝ λfe,b,t.λast:astfe_id fe b t.match ast with [ ASTFE_ID n _ ⇒ n ]. - -definition retype_id -: Πfe:aux_flatEnv_type.Πb:bool.Πt:ast_type.Πast:astfe_id fe b t.Πfe':aux_flatEnv_type.le_flatEnv fe fe' = true → - astfe_id fe' - (get_const_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) - (get_type_desc (get_desc_flatEnv fe' (get_name_astfe_id fe b t ast))) ≝ -λfe:aux_flatEnv_type.λb:bool.λt:ast_type.λast:astfe_id fe b t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true). - ASTFE_ID fe' (get_name_astfe_id fe b t ast) - (leflatenv_to_check fe fe' (get_name_astfe_id fe b t ast) dim (astfe_id_ind fe - (λHbeta3:bool.λHbeta2:ast_type.λHbeta1:astfe_id fe Hbeta3 Hbeta2.check_desc_flatEnv fe (get_name_astfe_id fe Hbeta3 Hbeta2 Hbeta1)) - (λa:aux_strId_type.λH:check_desc_flatEnv fe a.H) b t ast)). +lemma ast_to_astfe_id : + ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t. + ∀m:aux_map_type d.∀fe. + ∀dimInv:env_to_flatEnv_inv d e m fe. + astfe_id fe b t. + intros 7; + elim a 0; + intros 3; + lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?); + [ apply (proj2 ?? (proj1 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H))) + | rewrite > (proj2 ?? ((env_to_flatEnv_inv_last ???? H1) a1 H)); + apply Hletin + ]. +qed. + +lemma ast_to_astfe_retype_id : + ∀fe,b,t.∀ast:astfe_id 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. + astfe_id fe' b t. + intros 8; + elim a 0; + intros 4; + lapply (ASTFE_ID fe' a1 ?); + [ apply (leflatenv_to_check fe fe' a1 H2 H) + | rewrite > (leflatenv_to_get fe fe' a1 H2 H); + apply Hletin + ]. +qed. (* - AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - - AST_EXPR_NEG: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_NOT: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_COM: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - - AST_EXPR_ADD: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SUB: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_MUL: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_DIV: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SHR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SHL: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) - - AST_EXPR_GT : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_GTE: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_LT : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_LTE: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_EQ : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_NEQ: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - - AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - - AST_EXPR_ID: ∀b:bool.∀t:ast_type. - ast_var e b t → ast_expr e t + AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + +| AST_EXPR_NEG: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_NOT: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_COM: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) + +| AST_EXPR_ADD: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SUB: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_MUL: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_DIV: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SHR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SHL: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_AND: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_OR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_XOR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) + +| AST_EXPR_GT : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_GTE: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_LT : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_LTE: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_EQ : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_NEQ: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + +| AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + +| AST_EXPR_ID: ∀b:bool.∀t:ast_type. + ast_var d e b t → ast_expr d e t *) -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) + ] (* - AST_VAR_ID: ∀b:bool.∀t:ast_type. - ast_id e b t → ast_var e b t - AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. - ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t - AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. - ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n) + AST_VAR_ID: ∀b:bool.∀t:ast_type. + ast_id d e b t → ast_var d e b t +| AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. + ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t +| AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. + ast_var d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n) *) -and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_var fe b t) ≝ - match ast with - [ AST_VAR_ID subB subType subId ⇒ - opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType) - (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t) - - | AST_VAR_ARRAY subB subType dim var expr ⇒ - opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map) - (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map) - (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t)) - - | AST_VAR_STRUCT subB nelSubType field var _ ⇒ - opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map) - (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t) +and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t) + (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝ + match ast + return λW,X.λa:ast_var d e W X.astfe_var fe W X + with + [ AST_VAR_ID sB sType sId ⇒ + ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv) + + | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒ + ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv) + (ast_to_astfe_base_expr d e sExpr m fe dimInv) + + | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒ + ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv) ] (* - AST_BASE_EXPR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_base_expr e + AST_BASE_EXPR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e + *) -and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on ast : option (astfe_base_expr fe) ≝ - match ast with - [ AST_BASE_EXPR bType subExpr ⇒ - opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map) - (λres.Some ? (ASTFE_BASE_EXPR fe bType res)) +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 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) +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 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 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 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)) +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) ]. (* - AST_INIT_VAR: ∀b:bool.∀t:ast_type. - ast_var e b t → ast_init e t - AST_INIT_VAL: ∀t:ast_type. - aux_ast_init_type t → ast_init e t + AST_INIT_VAR: ∀b:bool.∀t:ast_type. + ast_var d e b t → ast_init d e t +| AST_INIT_VAL: ∀t:ast_type. + aux_ast_init_type t → ast_init d e t *) -definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝ -λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe. - match ast with - [ AST_INIT_VAR subB subType var ⇒ - opt_map ?? (ast_to_astfe_var e subB subType var fe map) - (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t) +definition ast_to_astfe_init ≝ +λd.λe:aux_env_type d.λt.λast:ast_init d e t. +λm:aux_map_type d.λfe. +λdimInv:env_to_flatEnv_inv d e m fe. + match ast + return λW.λa:ast_init d e W.astfe_init fe W + with + [ AST_INIT_VAR sB sType sVar ⇒ + ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv) + + | AST_INIT_VAL sType sArgs ⇒ + ASTFE_INIT_VAL fe sType sArgs - | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t ]. -definition retype_init ≝ -λfe:aux_flatEnv_type.λt:ast_type.λast:astfe_init fe t.λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true). - match ast with - [ ASTFE_INIT_VAR subB subType var ⇒ - opt_map ?? (retype_var fe subB subType var fe' dim) - (λres.ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAR fe' subB subType res) t) +definition ast_to_astfe_retype_init ≝ +λfe,t.λast:astfe_init 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. + match ast + return λW.λa:astfe_init fe W.astfe_init fe' W + with + [ ASTFE_INIT_VAR sB sType sVar ⇒ + ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe) + + | ASTFE_INIT_VAL sType sArgs ⇒ + ASTFE_INIT_VAL fe' sType sArgs - | ASTFE_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe' subType (ASTFE_INIT_VAL fe' subType args) t ]. (* - ASTFE_STM_ASG: ∀t:ast_type. - astfe_var e false t → astfe_expr e t → astfe_stm e - ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. - astfe_id e b t → astfe_init e t → astfe_stm e - ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e - ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e + ASTFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → astfe_stm e +| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → astfe_stm e +| ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e +| ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e *) -let rec retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝ +let rec ast_to_astfe_retype_stm fe (ast:astfe_stm 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_stm fe' ≝ match ast with - [ ASTFE_STM_ASG subType var expr ⇒ - opt_map ?? (retype_var fe false subType var fe' dim) - (λresVar.opt_map ?? (retype_expr fe subType expr fe' dim) - (λresExpr.Some ? (ASTFE_STM_ASG fe' subType resVar resExpr))) - - | ASTFE_STM_INIT subB subType subId init ⇒ - opt_map ?? (ast_to_astfe_id_check fe' ?? (retype_id fe subB subType subId fe' dim) subB subType) - (λresId.opt_map ?? (retype_init fe subType init fe' dim) - (λresInit.Some ? (ASTFE_STM_INIT fe' subB subType resId resInit))) - - | ASTFE_STM_WHILE expr body ⇒ - opt_map ?? (retype_base_expr fe expr fe' dim) - (λresExpr.opt_map ?? (retype_body fe body fe' dim) - (λresBody.Some ? (ASTFE_STM_WHILE fe' resExpr resBody))) - - | ASTFE_STM_IF nelExprBody optBody ⇒ - opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim) - (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim) - (λresBody.opt_map ?? t - (λt'.Some ? («£(pair ?? resExpr resBody)»&t'))))) - (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' [])))) - nelExprBody) - (λres.match optBody with - [ None ⇒ Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (None ?)) - | Some body ⇒ - opt_map ?? (retype_body fe body fe' dim) - (λresBody.Some ? (ASTFE_STM_IF fe' (cut_last_neList ? res) (Some ? resBody))) - ]) + [ ASTFE_STM_ASG sType sVar sExpr ⇒ + ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe) + + | ASTFE_STM_INIT sB sType sId sInit ⇒ + ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe) + (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe) + + | ASTFE_STM_WHILE sExpr sBody ⇒ + ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe) + (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe) + + | ASTFE_STM_IF sNelExprBody sOptBody ⇒ + ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe) + (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe) + )»&t) + «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))» + sNelExprBody)) + (opt_map ?? sOptBody + (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe))) ] (* - ASTFE_BODY: list (astfe_stm e) → astfe_body e + ASTFE_BODY: list (astfe_stm e) → astfe_body e *) -and retype_body (fe:aux_flatEnv_type) (ast:astfe_body fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_body fe') ≝ +and ast_to_astfe_retype_body fe (ast:astfe_body 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_body fe' ≝ match ast with - [ ASTFE_BODY lStm ⇒ - opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim) - (λh'.opt_map ?? t - (λt'.Some ? ([h']@t')))) (Some ? []) lStm) - (λresStm.Some ? (ASTFE_BODY fe' resStm)) + [ ASTFE_BODY sLStm ⇒ + ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm) ]. -definition retype_stm_list ≝ -λfe:aux_flatEnv_type.λast:list (astfe_stm fe).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true). - fold_right_list ?? (λh,t.opt_map ?? (retype_stm fe h fe' dim) - (λh'.opt_map ?? t - (λt'.Some ? ([h']@t')))) (Some ? []) ast. - -definition retype_exprAndBody_neList ≝ -λfe:aux_flatEnv_type.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λfe':aux_flatEnv_type.λdim:(le_flatEnv fe fe' = true). - opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (retype_base_expr fe (fst ?? h) fe' dim) - (λresExpr.opt_map ?? (retype_body fe (snd ?? h) fe' dim) - (λresBody.opt_map ?? t - (λt'.Some ? («£(pair ?? resExpr resBody)»&t'))))) - (Some ? (ne_nil ? (pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' [])))) - ast) - (λres.Some ? (cut_last_neList ? res)). - -(* applicare l'identita' e' inifluente *) -lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type). - aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe. - intros; - apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H); -qed. +definition ast_to_astfe_retype_stm_list ≝ +λfe.λast:list (astfe_stm 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. + fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast. + +definition ast_to_astfe_retype_exprBody_neList ≝ +λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body 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. + cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe) + (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe) + )»&t) + «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))» + ast). + +(* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *) +inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + astfe_stm fe' → + ast_to_astfe_stm_record d e fe. + +inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) → + ast_to_astfe_if_record d e fe. + +inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type). + env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' → + le_flatEnv fe fe' = true → + list (astfe_stm fe') → + ast_to_astfe_decl_record d e fe. + +inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + list (astfe_stm fe') → + ast_to_astfe_decl_aux_record d e fe. (* - AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type. - ast_var e false t → ast_expr e t → ast_stm e - AST_STM_WHILE: ∀e:aux_env_type. - ast_base_expr e → ast_decl (enter_env e) → ast_stm e - AST_STM_IF: ∀e:aux_env_type. - ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e + AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type. + ast_var d e false t → ast_expr d e t → ast_stm d e +| AST_STM_WHILE: ∀d.∀e:aux_env_type d. + ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e +| AST_STM_IF: ∀d.∀e:aux_env_type d. + ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e *) -let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast - : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝ +let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe. + env_to_flatEnv_inv d e m fe → + ast_to_astfe_stm_record d e fe ≝ match ast - return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) + return λD.λE.λast:ast_stm D E. + Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe with - [ AST_STM_ASG e' subType var expr ⇒ - λmap:aux_trasfMap_type e' fe. - opt_map ?? (ast_to_astfe_var e' false subType var fe map) - (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map) - (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫))) - - | AST_STM_WHILE e' expr decl ⇒ - λmap:aux_trasfMap_type e' fe. - opt_map ?? (ast_to_astfe_base_expr e' expr fe map) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map)) - (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with - [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with - [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with - [ pair map' resDecl ⇒ - match le_flatEnv fe fe' - return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) - with - [ true ⇒ λp:(le_flatEnv fe fe' = true). - opt_map ?? (retype_base_expr fe resExpr fe' p) - (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map) - (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫)) - | false ⇒ λp:(le_flatEnv fe fe' = false).None ? - ] (refl_eq ? (le_flatEnv fe fe')) - ]]])) - - | AST_STM_IF e' nelExprDecl optDecl ⇒ - λmap:aux_trasfMap_type e' fe. - let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) - (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝ - match nel with - [ ne_nil h ⇒ - opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m)) - (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with - [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with - [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with - [ pair m' resDecl ⇒ - match le_flatEnv fenv fenv' - return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) - with - [ true ⇒ λp:(le_flatEnv fenv fenv' = true). - opt_map ?? (retype_base_Expr fenv resExpr fenv' p) - (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) - «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫)) - | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ? - ] (refl_eq ? (le_flatEnv fenv fenv')) - ]]])) - - | ne_cons h tl ⇒ - opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m)) - (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with - [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with - [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with - [ pair m' resDecl ⇒ - opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl) - (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with - [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with - [ pair m'' tl' ⇒ - match le_flatEnv fenv fenv'' - return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) - with - [ true ⇒ λp:(le_flatEnv fenv fenv'' = true). - match le_flatEnv fenv' fenv'' - return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) - with - [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true). - opt_map ?? (retype_base_expr fenv resExpr fenv'' p) - (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p') - (λresDecl'. - Some ? (≪fenv'',pair ?? m'' - («£(pair ?? resExpr' - (ASTFE_BODY fenv'' resDecl'))»&tl')≫))) - | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ? - ] (refl_eq ? (le_flatEnv fenv' fenv'')) - | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ? - ] (refl_eq ? (le_flatEnv fenv fenv'')) - ]])]]])) - ] in - opt_map ?? (aux fe map nelExprDecl) - (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with - [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with - [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with - [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫) - | Some decl ⇒ - opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m')) - (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with - [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with - [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with - [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒ - match le_flatEnv fe' fe'' - return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) - with - [ true ⇒ λp'':(le_flatEnv fe' fe'' = true). - opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'') - (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) - (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m') - (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫)) - | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ? - ] (refl_eq ? (le_flatEnv fe' fe'')) - ]]])]]]) + [ AST_STM_ASG sD sE sType sVar sExpr ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv + (eq_to_leflatenv ?? (refl_eq ??)) + (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv) + (ast_to_astfe_expr sD sE sType sExpr m fe dimInv)) + | AST_STM_WHILE sD sE sExpr sDecl ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe + (env_map_flatEnv_enter_aux sD sE m fe dimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (λenv.ast_to_astfe_stm_record sD env fe) + (AST_TO_ASTFE_STM_RECORD sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + fe + (leave_map sD resMap) + resFe + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) + resDimLe + (ASTFE_STM_WHILE resFe + (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv) + sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (leave_map sD resMap) + resFe + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) + resDimLe) + (ASTFE_BODY resFe resLStm))) + sE (leave_add_enter_env sD sE resTrsf) ] + + | AST_STM_IF sD sE sExprDecl sOptDecl ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE)))) + (pMap:aux_map_type sD) (pFe:aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝ + match nel with + [ ne_nil h ⇒ + match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe + (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (λenv.ast_to_astfe_if_record sD env pFe) + (AST_TO_ASTFE_IF_RECORD sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + pFe + (leave_map sD resMap) + resFe + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) + resDimLe + «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv) + sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (leave_map sD resMap) + resFe + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) + resDimLe) + (ASTFE_BODY resFe resLStm))») + sE (leave_add_enter_env sD sE resTrsf) ] + + | ne_cons h t ⇒ + match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe + (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + match aux t (leave_map sD resMap) resFe + (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe) + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) + sE (leave_add_enter_env sD sE resTrsf)) with + [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒ + AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv' + (leflatenv_trans ??? resDimLe resDimLe') + («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv) + sD sE resMap' resFe' resDimInv' + (leflatenv_trans ??? resDimLe resDimLe')) + (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm) + sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]] + + ] in + match aux sExprDecl m fe dimInv with + [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒ + match sOptDecl with + [ None ⇒ + AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?)) + + | Some sDecl ⇒ + match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe + (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒ + eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (λenv.ast_to_astfe_stm_record sD env fe) + (AST_TO_ASTFE_STM_RECORD sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + fe + (leave_map sD resMap') + resFe' + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv') + (leflatenv_trans ??? resDimLe resDimLe') + (ASTFE_STM_IF resFe' + (ast_to_astfe_retype_exprBody_neList resFe resExprBody + sD + (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) + (leave_map sD resMap') + resFe' + (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv') + resDimLe') + (Some ? (ASTFE_BODY resFe' resLStm)))) + sE (leave_add_enter_env sD sE resTrsf) ]]] + ] (* - AST_NO_DECL: ∀e:aux_env_type. - list (ast_stm e) → ast_decl e - AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type. - (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e + AST_NO_DECL: ∀d.∀e:aux_env_type d. + list (ast_stm d e) → ast_decl d e +| AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e +| AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e *) -and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast - : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝ +and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe. + env_to_flatEnv_inv d e m fe → + ast_to_astfe_decl_record d e fe ≝ match ast - return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) - with - [ AST_NO_DECL e' lStm ⇒ - λmap:aux_trasfMap_type e' fe. - let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll - : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝ - match ll with - [ nil ⇒ let trsf ≝ [] - in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv) - (list (astfe_stm fenv)) - (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫ - - | cons h tl ⇒ - opt_map ?? (ast_to_astfe_stm e' h fenv m) - (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with - [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with - [ pair m' resStm ⇒ - opt_map ?? (aux tl fenv' m') - (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with - [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with - [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with - [ pair m'' tl' ⇒ - match le_flatEnv fenv' fenv'' - return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) - with - [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true). - opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p) - (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') - (list (astfe_stm fenv'')) - m'' - (resStm'@tl')≫≫) - | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ? - ] (refl_eq ? (le_flatEnv fenv' fenv'')) - ]]])]])] in - aux lStm fe map - - | AST_DECL e' b name t dim optInit subDecl ⇒ - λmap:aux_trasfMap_type e' fe. - opt_map ?? (match optInit with - [ None ⇒ Some ? [] - | Some init ⇒ - opt_map ?? (ast_to_astfe_init e' t init fe map) - (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ?? - (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t) - (next_nameId e' fe map name) - (ast_to_astfe_dec_aux e' name b t fe map dim)) - b t) - (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t) - (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t)) - (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ])))) - ]) - (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl - (add_desc_flatEnv fe (next_nameId e' fe map name) b t) - (add_maxcur_map e' fe map map name b t)) - (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with - [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with - [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with - [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒ - match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' - return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe')))) - with - [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true). - opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p) - (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f - in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe') - (list (astfe_stm fe')) - map' - (hRes'@tRes)≫≫) - | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ? - ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe')) - ]]])) - ]. + return λD.λE.λast:ast_decl D E. + Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe + with + [ AST_NO_DECL sD sE sLStm ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝ + match l with + [ nil ⇒ + AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) [] + + | cons h t ⇒ + match ast_to_astfe_stm sD sE h pMap pFe pDimInv with + [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒ + match aux t resMap resFe resDimInv with + [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒ + AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv' + (leflatenv_trans ??? resDimLe resDimLe') + ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]] + + ] in + match aux sLStm m fe dimInv with + [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe [] + (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv) + resDimLe resLStm ] + + | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe + ([ tripleT ??? sName true sType ]@resTrsf) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe) + ([ ASTFE_STM_INIT resFe true sType + (* l'id e' sull'ambiente arricchito *) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + true sType + (ast_to_astfe_id sD (add_desc_env sD sE sName true sType) + true sType + (newid_from_init sD sE sName true sType) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv)) + sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + resDimLe) + (* l'init e' sull'ambiente non arricchito *) + (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv) + sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)) + ]@resLStm) ] + + | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe + ([ tripleT ??? sName false sType ]@resTrsf) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe) + (match sOptInit with + [ None ⇒ [] + | Some init ⇒ + [ ASTFE_STM_INIT resFe false sType + (* l'id e' sull'ambiente arricchito *) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + false sType + (ast_to_astfe_id sD (add_desc_env sD sE sName false sType) + false sType + (newid_from_init sD sE sName false sType) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv)) + sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) + resDimLe) + (* l'init e' sull'ambiente non arricchito *) + (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv) + sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)) + ]]@resLStm) ] + + ]. (* - AST_ROOT: ast_decl empty_env → ast_root. + AST_ROOT: ast_decl O empty_env → ast_root *) definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝ λast:ast_root.match ast with - [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with - (* impossibile: dummy *) - [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫ - | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with - [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with - [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with - [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫ - ]]]]]. - -(* mini test -include "compiler/preast_tree.ma". -include "compiler/preast_to_ast.ma". - -{ const byte8 a; - const byte8[3] b={0,1,2}; - byte8[3] c=b; - - if(0xF0) - { byte8 a=a; } - else if(0xF1) - { - while(0x10) - { byte8[3] b=c; } - } - else if(0xF2) - { byte8 a=b[0]; } - else - { const byte8 a=a; } -} - -definition prova ≝ -PREAST_ROOT ( - PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) ( - PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) ( - PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) ( - PREAST_NO_DECL [ - PREAST_STM_IF « - (pair ?? - (PREAST_EXPR_BYTE8 〈xF,x0〉) - (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])) - ) - ; (pair ?? - (PREAST_EXPR_BYTE8 〈xF,x1〉) - (PREAST_NO_DECL [ - (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) ( - PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL []) - )) - ]) - ) - £ (pair ?? - (PREAST_EXPR_BYTE8 〈xF,x2〉) - (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL [])) - ) - » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))) - ] - ) - ) - ) -). -*) + [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with + [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].