From: Claudio Sacerdoti Coen Date: Fri, 31 Oct 2008 15:11:45 +0000 (+0000) Subject: - New dependency for environments on the nesting depth. X-Git-Tag: make_still_working~4612 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa9c56aecab7c7f52de13fb1af9696446bccb047;p=helm.git - New dependency for environments on the nesting depth. - New invariant that tightly binds the list of identifiers in scope with the list of mappings in an environment transformation map - Second pass of the compiler finally complited --- 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..ce2fe1eb2 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -26,112 +26,42 @@ 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))) *) -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; + unfold env_to_flatEnv_inv; + elim a 0; + intros 3; + lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?); + [ apply (proj2 ?? (proj1 ?? (H1 a1 H))) + | rewrite > (proj2 ?? (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; + unfold env_to_flatEnv_inv; + 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) @@ -181,94 +111,80 @@ definition retype_id AST_EXPR_ID: ∀b:bool.∀t:ast_type. ast_var e b t → ast_expr 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_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. @@ -278,141 +194,138 @@ let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (fe:a 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) *) -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 *) -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_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) ]. (* @@ -421,24 +334,35 @@ and retype_base_expr (fe:aux_flatEnv_type) (ast:astfe_base_expr fe) (fe':aux_fla AST_INIT_VAL: ∀t:ast_type. aux_ast_init_type t → ast_init 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 ]. (* @@ -449,71 +373,49 @@ definition retype_init ≝ 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 fe' dimInv dimLe 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 *) -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 fe' dimInv dimLe 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,fe',dimInv,dimLe. + 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,fe',dimInv,dimLe. + 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). (* AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type. @@ -523,112 +425,157 @@ qed. 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 *) -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')) ≝ +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. + +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.Πfe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + 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.Πfe'. + env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → 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,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + AST_TO_ASTFE_STM_RECORD sD sE fe m fe' dimInv dimLe + (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,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe' fe' + (env_map_flatEnv_enter_aux sD sE m fe' dimInv) + (eq_to_leflatenv ?? (refl_eq ??)) 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 ??? dimLe 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,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + 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,pFe':aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe') + (pDimLe:le_flatEnv pFe pFe' = true) 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' pFe' + (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv) + (eq_to_leflatenv ?? (refl_eq ??)) 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) + (leflatenv_trans ??? pDimLe 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' pFe' + (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv) + (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + match aux t (leave_map sD resMap) resFe 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)) + (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒ + AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv' + (leflatenv_trans ??? pDimLe (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 fe' dimInv dimLe 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 resFe + (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) + (eq_to_leflatenv ?? (refl_eq ??)) 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. @@ -636,144 +583,84 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) 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 *) -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.Πfe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + 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.Πfe'. + env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record D E fe + with + [ AST_NO_DECL sD sE sLStm ⇒ + λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe,pFe':aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe') + (pDimLe:le_flatEnv pFe pFe' = true) 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 pDimLe [] + + | cons h t ⇒ + match ast_to_astfe_stm sD sE h pMap pFe' pFe' pDimInv (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒ + match aux t resMap resFe resFe resDimInv (eq_to_leflatenv ?? (refl_eq ??)) 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 ??? pDimLe (leflatenv_trans ??? resDimLe resDimLe')) + ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]] + + ] in + match aux sLStm m fe fe' dimInv dimLe 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_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒ + λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (env_map_flatEnv_addSingle_aux sD sE m fe' sName sB sType dimInv) + (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe + ([ tripleT ??? sName sB sType ]@resTrsf) + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) + (leflatenv_trans ??? dimLe (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe' [ tripleT ??? sName sB sType ]) resDimLe)) + (match sOptInit with + [ None ⇒ [] + | Some init ⇒ + [ ASTFE_STM_INIT resFe sB sType + (* l'id e' sull'ambiente arricchito *) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + sB sType + (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType) + sB sType + (newid_from_init sD sE sName sB sType) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (env_map_flatEnv_addSingle_aux sD sE m fe' sName sB sType dimInv)) + sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB 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 sB sType ]@resTrsf) sE) + resMap resFe + (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe' [ tripleT ??? sName sB sType ]) resDimLe)) + ]]@resLStm) ] + + ]. (* AST_ROOT: ast_decl 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 empty_flatEnv env_map_flatEnv_empty_aux (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]]. diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma deleted file mode 100755 index e75401979..000000000 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma +++ /dev/null @@ -1,775 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* ********************************************************************** *) -(* *) -(* Sviluppato da: *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) -(* *) -(* ********************************************************************** *) - -include "compiler/astfe_tree1.ma". - -(* ************************ *) -(* PASSO 2 : da AST a ASTFE *) -(* ************************ *) - -(* - 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))) -*) -lemma ast_to_astfe_id : - ∀e,b,t.∀ast:ast_id e b t. - ∀d.∀m:aux_map_type d.∀fe. - ∀dimInv:env_to_flatEnv_inv d e m fe. - astfe_id fe b t . - intros 7; - unfold env_to_flatEnv_inv; - elim a 0; - intros 3; - lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?); - [ apply (proj2 ?? (proj1 ?? (H1 a1 H))) - | rewrite > (proj2 ?? (H1 a1 H)); - apply Hletin - ]. -qed. - -lemma ast_to_astfe_retype_id : - ∀fe,b,t.∀ast:astfe_id fe b t. - ∀d.∀e.∀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; - unfold env_to_flatEnv_inv; - 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 -*) -let rec ast_to_astfe_expr e t (ast:ast_expr e t) - d (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 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 e (AST_TYPE_BASE bType) sExpr d m fe dimInv) - | AST_EXPR_NOT bType sExpr ⇒ - ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) - | AST_EXPR_COM bType sExpr ⇒ - ASTFE_EXPR_COM fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) - - | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv) - | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv) - - | AST_EXPR_GT bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_GT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_LT bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_LT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒ - ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) - (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) - - | AST_EXPR_B8toW16 sExpr ⇒ - ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv) - | AST_EXPR_B8toW32 sExpr ⇒ - ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv) - | AST_EXPR_W16toB8 sExpr ⇒ - ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv) - | AST_EXPR_W16toW32 sExpr ⇒ - ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv) - | AST_EXPR_W32toB8 sExpr ⇒ - ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv) - | AST_EXPR_W32toW16 sExpr ⇒ - ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv) - - | AST_EXPR_ID b sType var ⇒ - ASTFE_EXPR_ID fe b sType (ast_to_astfe_var e b sType var d 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) -*) -and ast_to_astfe_var e b t (ast:ast_var e b t) - d (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 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 e sB sType sId d m fe dimInv) - - | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒ - ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe dimInv) - (ast_to_astfe_base_expr e sExpr d m fe dimInv) - - | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒ - ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe dimInv) - ] -(* - AST_BASE_EXPR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_base_expr e -*) -and ast_to_astfe_base_expr e (ast:ast_base_expr e) - d (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 e.astfe_base_expr fe - with - [ AST_BASE_EXPR bType sExpr ⇒ - ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) - ]. - -let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) - d e (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_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 (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 (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 -*) -definition ast_to_astfe_init ≝ -λe,t.λast:ast_init e t. -λd.λm:aux_map_type d.λfe. -λdimInv:env_to_flatEnv_inv d e m fe. - match ast - return λW.λa:ast_init e W.astfe_init fe W - with - [ AST_INIT_VAR sB sType sVar ⇒ - ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var e sB sType sVar d m fe dimInv) - - | AST_INIT_VAL sType sArgs ⇒ - ASTFE_INIT_VAL fe sType sArgs - - ]. - -definition ast_to_astfe_retype_init ≝ -λfe,t.λast:astfe_init fe t. -λd.λe.λ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_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 ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe on ast : astfe_stm fe' ≝ - match ast with - [ 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 -*) -and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe on ast : astfe_body fe' ≝ - match ast with - [ 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 ast_to_astfe_retype_stm_list ≝ -λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe. - 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,m,fe',dimInv,dimLe. - 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). - -(* - 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 -*) -inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type) (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) (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) (m:aux_map_type d) (fe:aux_flatEnv_type) : Type ≝ -AST_TO_ASTFE_DECL_RECORD: ∀trsf:list (Prod3T aux_str_type bool ast_type). - env_to_flatEnv_inv d - (build_trasfEnv_env trsf e) - (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) - (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) → - le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true → - list (astfe_stm (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))) → - ast_to_astfe_decl_record d e m fe. - -let rec ast_to_astfe_stm e (ast:ast_stm e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d e m fe' → - le_flatEnv fe fe' = true → - ast_to_astfe_stm_record d e fe ≝ - match ast - return λX.λast:ast_stm X. - Πd.Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record d X fe - with - [ AST_STM_ASG sE sType sVar sExpr ⇒ - λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. - AST_TO_ASTFE_STM_RECORD d sE fe m fe' dimInv dimLe - (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe' dimInv) - (ast_to_astfe_expr sE sType sExpr d m fe' dimInv)) - - | AST_STM_WHILE sE sExpr sDecl ⇒ - λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. - (* in sostanza - 1) eseguo decl su ENTER dell'invariante - 2) decl restituisce ADD+ENTER dell'invariante - 3) eseguo base_expr sull'invariante - 4) retipo base_expr su LEAVE+ADD+ENTER dell'invariante - 5) retituisco su LEAVE+ADD+ENTER dell'invariante *) - match ast_to_astfe_decl (enter_env sE) sDecl (S d) (enter_map d m) fe fe' (env_map_flatEnv_enter_aux d sE m fe' dimInv) dimLe with - [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ - AST_TO_ASTFE_STM_RECORD d sE fe - (* m'' *) - (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))) - (* fe'' *) - (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) - (* leave_add_enter(dimInv) *) - (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv) - (* fe ≤ fe' ∧ fe' ≤ fe'' → fe ≤ fe'' *) - (leflatenv_trans ??? dimLe resDimLe) - (* risultato su fe'' *) - (ASTFE_STM_WHILE (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) - (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sE sExpr d m fe' dimInv) - d sE - (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))) - (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) - (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv) - resDimLe) - (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) resLStm)) ] - - | AST_STM_IF sE sExprDecl sOptDecl ⇒ - λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. - let rec aux (nel:ne_list (Prod (ast_base_expr sE) (ast_decl (enter_env sE)))) - (pMap:aux_map_type d) (pFe,pFe':aux_flatEnv_type) - (pDimInv:env_to_flatEnv_inv d sE pMap pFe') - (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record d sE pFe ≝ - match nel with - [ ne_nil h ⇒ - match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with - [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ - AST_TO_ASTFE_IF_RECORD d sE pFe - (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) - (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) - (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) - (leflatenv_trans ??? pDimLe resDimLe) - «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sE (fst ?? h) d pMap pFe' pDimInv) - d sE - (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) - (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) - (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) - resDimLe) - (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) resLStm))» ] - - | ne_cons h t ⇒ (False_rect ? daemon) - (*match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with - [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ - match aux t (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) - pFe (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) - (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) - (leflatenv_trans ??? pDimLe resDimLe) with - [ AST_TO_ASTFE_IF_RECORD iMap iFe' iDimInv iDimLe iNelExprDecl ⇒ - AST_TO_ASTFE_IF_RECORD d sE pFe iMap iFe' iDimInv iDimLe - (False_rect ? daemon) ]]*) - - - ] in (False_rect ? daemon) - - ] -and ast_to_astfe_decl e (ast:ast_decl e) on ast : Πd.Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d e m fe' → - le_flatEnv fe fe' = true → - ast_to_astfe_decl_record d e m fe' ≝ - match ast - return λX.λast:ast_decl X. - Πd.Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record d X m fe' - with - [ AST_NO_DECL sE sLStm ⇒ - λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. - False_rect ? daemon - - | _ ⇒ False_rect ? daemon - - ]. - -FINQUI - - | 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_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 -*) -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')))) ≝ - 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')) - ]]])) - ]. - -(* - AST_ROOT: ast_decl 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 []))) - ] - ) - ) - ) -). -*) diff --git a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma index 6ba41f18c..553991bd7 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_tree.ma @@ -26,74 +26,74 @@ include "compiler/environment.ma". (* *************** *) (* id: accesso all'ambiente con stringa *) -inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝ +inductive ast_id (d:nat) (e:aux_env_type d) : bool → ast_type → Type ≝ AST_ID: ∀str:aux_str_type. - (* D *) (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))). + (* D *) (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))). (* -------------------------- *) (* espressioni *) -inductive ast_expr (e:aux_env_type) : ast_type → Type ≝ - 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) +inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝ + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr 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 d 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 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_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 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + 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 e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + 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 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_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 e b t → ast_expr e t + ast_var d e b t → ast_expr d e t (* variabile: modificatori di array/struct dell'id *) with ast_var : bool → ast_type → Type ≝ AST_VAR_ID: ∀b:bool.∀t:ast_type. - ast_id e b t → ast_var e b t + ast_id d e b t → ast_var d 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 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 e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n) + ast_var d e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n) (* espressioni generalizzate: anche non uniformi per tipo *) with ast_base_expr : Type ≝ AST_BASE_EXPR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_base_expr e. + ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e. (* -------------------------- *) @@ -126,37 +126,37 @@ let rec aux_ast_init_type (t:ast_type) on t : Type ≝ 1) var1 = var2 2) var = ... valori ... *) -inductive ast_init (e:aux_env_type) : ast_type → Type ≝ +inductive ast_init (d:nat) (e:aux_env_type d) : ast_type → Type ≝ AST_INIT_VAR: ∀b:bool.∀t:ast_type. - ast_var e b t → ast_init e t + ast_var d e b t → ast_init d e t | AST_INIT_VAL: ∀t:ast_type. - aux_ast_init_type t → ast_init e t. + aux_ast_init_type t → ast_init d e t. (* -------------------------- *) (* statement: assegnamento/while/if else if else *) -inductive ast_stm : aux_env_type → Type ≝ - 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 +inductive ast_stm : Πd:nat.aux_env_type d → Type ≝ + 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 (* dichiarazioni *) -with ast_decl : aux_env_type → Type ≝ - 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. - (* D *) (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e. +with ast_decl : Πd:nat.aux_env_type d → Type ≝ + AST_NO_DECL: ∀d.∀e:aux_env_type d. + list (ast_stm d e) → ast_decl d e +| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type. + (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e. (* -------------------------- *) (* programma *) inductive ast_root : Type ≝ - AST_ROOT: ast_decl empty_env → ast_root. + AST_ROOT: ast_decl O empty_env → ast_root. (* -------------------------- *) (* programma vuoto *) -definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)). +definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL O empty_env (nil ?)). diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma index 865f9e5c9..9f489b792 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -20,62 +20,184 @@ (* ********************************************************************** *) include "compiler/environment.ma". +include "compiler/ast_tree.ma". (* ********************** *) (* GESTIONE AMBIENTE FLAT *) (* ********************** *) -(* STRUTTURA AMBIENTE FLAT *) +(* ambiente flat *) +inductive var_flatElem : Type ≝ +VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem. -(* elemento: name + desc *) -inductive flatVar_elem : Type ≝ -VAR_FLAT_ELEM: aux_strId_type → desc_elem → flatVar_elem. +definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ]. +definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ]. -(* tipo pubblico *) -definition aux_flatEnv_type ≝ list flatVar_elem. +definition aux_flatEnv_type ≝ list var_flatElem. -(* getter *) -definition get_nameId_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ]. -definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ]. +definition empty_flatEnv ≝ nil var_flatElem. -(* ambiente vuoto *) -definition empty_flatEnv ≝ nil flatVar_elem. +(* mappa: nome + max + cur *) +inductive map_list : nat → Type ≝ + map_nil: map_list O +| map_cons: ∀n.option nat → map_list n → map_list (S n). -(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *) -let rec get_desc_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) on e ≝ -match e with - [ nil ⇒ None ? - | cons h tl ⇒ match eqStrId_str str (get_nameId_flatVar h) with - [ true ⇒ Some ? (get_desc_flatVar h) - | false ⇒ get_desc_flatEnv_aux tl str ]]. +definition defined_mapList ≝ +λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ]. -definition get_desc_flatEnv ≝ -λe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux e str with +definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝ +λd.λl:map_list d.λp:defined_mapList ? l. + let value ≝ + match l + return λX.λY:map_list X.defined_mapList X Y → map_list (pred X) + with + [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p + | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t + ] p in value. + +definition get_first_mapList : Πd.map_list d → ? → option nat ≝ +λd.λl:map_list d.λp:defined_mapList ? l. + let value ≝ + match l + return λX.λY:map_list X.defined_mapList X Y → option nat + with + [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p + | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h + ] p in value. + +inductive map_elem (d:nat) : Type ≝ +MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d. + +definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ]. +definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ]. +definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ]. + +definition aux_map_type ≝ λd.list (map_elem d). + +definition empty_map ≝ nil (map_elem O). + +lemma defined_mapList_S_to_true : +∀d.∀l:map_list (S d).defined_mapList (S d) l = True. + intros; + inversion l; + [ intros; destruct H + | intros; simplify; reflexivity + ] +qed. + +lemma defined_mapList_get : + ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h). + intros 2; + rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h)); + apply I. +qed. + +(* get_id *) +let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝ + match map with + [ nil ⇒ None ? + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??) + | false ⇒ get_id_map_aux d t name + ] + ]. + +definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. + +(* get_max *) +let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝ + match map with + [ nil ⇒ None ? + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ Some ? (get_max_mapElem d h) + | false ⇒ get_max_map_aux d t name + ] + ]. + +definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. + +(* check_id *) +definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ]. + +definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ]. + +lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name. + unfold checkb_id_map; + unfold check_id_map; + intros 3; + elim (get_id_map_aux d map name) 0; + [ simplify; intro; destruct H + | simplify; intros; apply I + ]. +qed. + +definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ]. + +definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ]. + +lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name. + unfold checknotb_id_map; + unfold checknot_id_map; + intros 3; + elim (get_id_map_aux d map name) 0; + [ simplify; intro; apply I + | simplify; intros; destruct H + ]. +qed. + +(* get_desc *) +let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝ + match fe with + [ nil ⇒ None ? + | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with + [ true ⇒ Some ? (get_desc_flatVar h) + | false ⇒ get_desc_flatEnv_aux t name + ] + ]. + +definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. -definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux e str with [ None ⇒ False | Some _ ⇒ True ]. +definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ]. -definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ]. +definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ]. -lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str. +lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str. unfold checkb_desc_flatEnv; unfold check_desc_flatEnv; - intros; - letin K ≝ (get_desc_flatEnv_aux e str); - elim K; - [ normalize; autobatch | - normalize; autobatch ] + intros 2; + elim (get_desc_flatEnv_aux fe str) 0; + [ simplify; intro; destruct H + | simplify; intros; apply I + ]. qed. -(* aggiungi descrittore ad ambiente: in coda *) -definition add_desc_flatEnv ≝ -λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type. - e@[VAR_FLAT_ELEM str (DESC_ELEM b t)]. +definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ]. + +definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ]. -(* controllo fe <= fe' *) +lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str. + unfold checknotb_desc_flatEnv; + unfold checknot_desc_flatEnv; + intros 2; + elim (get_desc_flatEnv_aux fe str) 0; + [ simplify; intro; apply I + | simplify; intros; destruct H + ]. +qed. + +(* fe <= fe' *) definition eq_flatEnv_elem ≝ λe1,e2.match e1 with [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with @@ -110,7 +232,19 @@ match fe with [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ] ]. -lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'. +lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true. + intros 3; + rewrite < H; + elim e1; + [ reflexivity + | simplify; + rewrite > (eq_to_eqflatenv a a (refl_eq ??)); + rewrite > H1; + reflexivity + ]. +qed. + +lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'. intro; elim fe 0; [ intros; exists; [ apply fe' | reflexivity ] @@ -126,338 +260,437 @@ lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'. ]. qed. +lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true. + intros; + elim fe; + [ simplify; + reflexivity + | simplify; + rewrite > (eq_to_eqflatenv a a (refl_eq ??)); + rewrite > H; + reflexivity + ]. +qed. + lemma leflatenv_to_check : ∀fe,fe',str. (le_flatEnv fe fe' = true) → (check_desc_flatEnv fe str) → (check_desc_flatEnv fe' str). intros 4; - cases (leflatEnv_to_le fe fe' H); + cases (leflatenv_to_le fe fe' H); rewrite < H1; elim fe 0; [ intro; simplify in H2:(%); elim H2; | intros 3; simplify; - cases (eqStrId_str str (get_nameId_flatVar a)); + cases (eqStrId_str str (get_name_flatVar a)); [ simplify; intro; apply H3 - | simplify; - apply H2 + | simplify; apply H2 ] ]. qed. -lemma adddescflatenv_to_leflatenv : ∀fe,n,b,t.le_flatEnv fe (add_desc_flatEnv fe n b t) = true. -intros; - change in ⊢ (? ? (? ? %) ?) with (fe@[VAR_FLAT_ELEM n (DESC_ELEM b t)]); +lemma leflatenv_to_get : ∀fe,fe',str. + (le_flatEnv fe fe' = true) → + (check_desc_flatEnv fe str) → + (get_desc_flatEnv fe str = get_desc_flatEnv fe' str). + intros 4; + cases (leflatenv_to_le fe fe' H); + rewrite < H1; elim fe 0; - [ 1: reflexivity - | 2: do 3 intro; - unfold le_flatEnv; - change in ⊢ (? ? % ?) with ((eq_flatEnv_elem a a)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)]))); - unfold eq_flatEnv_elem; - elim a; - change in ⊢ (? ? % ?) with ((eqStrId_str a1 a1)⊗(eqDesc_elem d d)⊗(le_flatEnv l (l@[VAR_FLAT_ELEM n (DESC_ELEM b t)]))); - rewrite > (eq_to_eqstrid a1 a1 (refl_eq ??)); - rewrite > (eq_to_eqdescelem d d (refl_eq ??)); - rewrite > H; - reflexivity + [ intro; + simplify in H2:(%); + elim H2 + | simplify; + intros 2; + cases (eqStrId_str str (get_name_flatVar a)); + [ simplify; + intros; + reflexivity + | simplify; + unfold check_desc_flatEnv; + unfold get_desc_flatEnv; + cases (get_desc_flatEnv_aux l str); + [ simplify; intros; elim H3 + | simplify; intros; rewrite < (H2 H3); reflexivity + ] + ] ]. qed. -(* STRUTTURA MAPPA TRASFORMAZIONE *) +(* controllo di coerenza env <-> map *) +let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝ + match e with + [ env_nil h ⇒ λf.f h + | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h) + ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]). + +let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝ + match map with + [ map_nil ⇒ eqb res O + | map_cons d' h t ⇒ match eqb res O with + [ true ⇒ match h with + [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ] + | false ⇒ match h with + [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ] + ] + ]. -(* elemento: nome + cur + max + dimostrazione *) -inductive maxCur_elem (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝ -MAX_CUR_ELEM: ∀str:aux_str_type.∀cur:nat.nat → (check_desc_env e str → get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → maxCur_elem e fe. +(* esprimendolo in lingua umana il vincolo che controlla e': + ∀name ϵ map. + la map_list "cur" deve avere la seguente struttura + - Some _ ; ... ; Some _ ; None ; ... None + - il numero di Some _ deve essere pari a (d + 1 - x) con x + ricavato scandendo in avanti tutti gli ambienti e + numerando quanti ambienti CONSECUTIVI non contengono la definizione di name + + ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo" + no si no si NO NO + quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2 + sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti + Some _ ; Some _ ; Some _ ; Some _ ; None ; None + cioe' 5+1-2 Some seguiti da solo None + + NB: e' solo meta' perche' cosi' si asserisce map ≤ env + +*) +let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝ + match map with + [ nil ⇒ true + | cons h t ⇒ (check_map_env_align_auxMap (S d) (get_cur_mapElem d h) (d + 1 - (check_map_env_align_auxEnv d e (get_name_mapElem d h) O)))⊗ + (check_map_env_align d e t) + ]. -(* tipo pubblico *) -definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe). +let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝ + match le with + [ nil ⇒ true + | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with + [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ] + ]. -(* getter *) -definition get_name_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM n _ _ _ ⇒ n ]. -definition get_cur_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ c _ _ ⇒ c ]. -definition get_max_maxCur ≝ λe,fe.λmc:maxCur_elem e fe.match mc with [ MAX_CUR_ELEM _ _ m _ ⇒ m ]. +(* esprimendolo in lingua umana il vincolo che controlla e': + ∀name ϵ e.name ϵ map + + NB: e' l'altra meta' perche' cosi' asserisce env ≤ map +*) +let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝ + match e with + [ env_nil h ⇒ check_env_map_align_aux dm map h + | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map) + ]. -(* mappa di trasformazione vuota *) -definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe). +(* invariante *) +definition env_to_flatEnv_inv ≝ + λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type. + ∀str. + check_desc_env d e str → + (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧ + check_id_map d map str ∧ + check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧ + get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))). + +lemma inv_to_checkdescflatenv : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → + (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))). + intros 7; + unfold env_to_flatEnv_inv in H:(%); + lapply (H str H1); + apply (proj2 ?? (proj1 ?? Hletin)); +qed. -(* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *) +lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv. + unfold env_to_flatEnv_inv; + unfold empty_env; + unfold empty_map; + unfold empty_flatEnv; + simplify; + intros; + elim H. +qed. -(* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *) -let rec get_maxcur_map (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) (str:aux_str_type) on map ≝ +lemma leflatenv_to_inv : + ∀d.∀e.∀map:aux_map_type d.∀fe,fe'. + le_flatEnv fe fe' = true → + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d e map fe'. + intros 6; + unfold env_to_flatEnv_inv; + intros; + split; + [ split; + [ lapply (H1 str H2); + apply (proj1 ?? (proj1 ?? Hletin)) + | lapply (H1 str H2); + apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin))) + ] + | lapply (H1 str H2); + rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin))); + apply (proj2 ?? Hletin) + ]. +qed. + +lemma leflatenv_trans : + ∀fe,fe',fe''. + le_flatEnv fe fe' = true → + le_flatEnv fe' fe'' = true → + le_flatEnv fe fe'' = true. + intros 4; + cases (leflatenv_to_le fe ? H); + rewrite < H1; + intro; + cases (leflatenv_to_le (fe@x) fe'' H2); + rewrite < H3; + rewrite > associative_append; + apply (le_to_leflatenv fe ?). +qed. + +(* enter: propaga in testa la vecchia testa (il "cur" precedente) *) +let rec enter_map d (map:aux_map_type d) on map ≝ match map with - [ nil ⇒ None ? - | cons h tl ⇒ match eqStr_str str (get_name_maxCur e fe h) with - [ true ⇒ Some ? h | false ⇒ get_maxcur_map e fe tl str ]]. - -(* prossimo nome *) -definition next_nameId ≝ -λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type. - match get_maxcur_map e fe map str with - [ None ⇒ STR_ID str 0 - | Some maxcur ⇒ STR_ID str (S (get_max_maxCur e fe maxcur)) + [ nil ⇒ [] + | cons h t ⇒ + (MAP_ELEM (S d) + (get_name_mapElem d h) + (get_max_mapElem d h) + (map_cons (S d) + (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??)) + (get_cur_mapElem d h)) + )::(enter_map d t) ]. -(* nome -> nome + id *) -definition name_to_nameId ≝ -λe,fe.λmap:aux_trasfMap_type e fe.λstr:aux_str_type. - match get_maxcur_map e fe map str with - [ None ⇒ STR_ID str 0 - | Some maxcur ⇒ STR_ID str (get_cur_maxCur e fe maxcur) +lemma getidmap_to_enter : + ∀d.∀m:aux_map_type d.∀str. + get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str. + intros; + elim m; + [ simplify; reflexivity + | simplify; rewrite > H; reflexivity + ] +qed. + +(* leave: elimina la testa (il "cur" corrente) *) +let rec leave_map d (map:aux_map_type (S d)) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ + (MAP_ELEM d + (get_name_mapElem (S d) h) + (get_max_mapElem (S d) h) + (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??)) + )::(leave_map d t) ]. -(* NB: se cerco qualcos'altro il risultato e' invariato *) -axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map. -(check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → -(eqStr_str str str' = false) → -(check_desc_env (add_desc_env e str' b' desc') str → - get_desc_env (add_desc_env e str' b' desc') str = - get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str cur)). - -(* NB: se cerco cio' che e' appena stato aggiunto, deve essere uguale *) -axiom add_maxcur_map_aux_true : ∀e,fe,str,cur,max,str',b',desc',map. -(check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → -(eqStr_str str str' = true) → -(check_desc_env (add_desc_env e str' b' desc') str → - get_desc_env (add_desc_env e str' b' desc') str = - get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str') b' desc') (STR_ID str (S max))). - -axiom add_maxcur_map_aux_new : ∀e,fe,str,b,desc,map. - check_desc_env (add_desc_env e str b desc) str → - get_desc_env (add_desc_env e str b desc) str = - get_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b desc) (STR_ID str 0). - -(* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *) -axiom ast_to_astfe_id_aux : ∀e,fe.∀map:aux_trasfMap_type e fe.∀str. - check_desc_env e str → check_desc_flatEnv fe (name_to_nameId e fe map str). - -axiom ast_to_astfe_dec_aux : ∀e,str,b,t,fe,map. - check_not_already_def_env e str → - check_desc_flatEnv (add_desc_flatEnv fe (next_nameId e fe map str) b t) (next_nameId e fe map str). - -(* aggiungi/aggiorna descrittore mappa trasformazione *) -let rec add_maxcur_map_aux (e:aux_env_type) (fe:aux_flatEnv_type) (map,fMap:aux_trasfMap_type e fe) - (str:aux_str_type) (b:bool) (desc:ast_type) (flag:bool) on map - : aux_trasfMap_type (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) ≝ -match map with - [ nil ⇒ - match flag with - [ true ⇒ [] - | false ⇒ - [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) - str 0 0 (add_maxcur_map_aux_new e fe str b desc fMap) ] - ] - | cons h tl ⇒ match h with - [ MAX_CUR_ELEM str' cur' max' dim' ⇒ - match eqStr_str str' str return λx.(eqStr_str str' str = x) → ? with - [ true ⇒ λp:(eqStr_str str' str = true). - [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) - str' (S max') (S max') - (add_maxcur_map_aux_true e fe str' cur' max' str b desc fMap dim' p) - ]@(add_maxcur_map_aux e fe tl fMap str b desc true) - | false ⇒ λp:(eqStr_str str' str = false). - [ MAX_CUR_ELEM (add_desc_env e str b desc) (add_desc_flatEnv fe (next_nameId e fe fMap str) b desc) - str' cur' max' - (add_maxcur_map_aux_false e fe str' cur' str b desc fMap dim' p) - ]@(add_maxcur_map_aux e fe tl fMap str b desc flag) - ] (refl_eq ? (eqStr_str str' str)) - ] - ]. +(* aggiungi descrittore *) +let rec new_map_elem_from_depth_aux (d:nat) on d ≝ + match d + return λd.map_list d + with + [ O ⇒ map_nil + | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n) + ]. -definition add_maxcur_map ≝ -λe:aux_env_type.λfe:aux_flatEnv_type.λmap,fMap:aux_trasfMap_type e fe.λstr:aux_str_type.λb:bool.λdesc:ast_type. -add_maxcur_map_aux e fe map fMap str b desc false. +let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??))) + | false ⇒ h + ]::(new_max_map_aux d t name max) + ]. -(* composizione di funzioni generata da una lista di nome x const x tipo *) -definition aux_trasfEnv_type ≝ list (Prod3T aux_str_type bool ast_type). +definition add_desc_env_flatEnv_map ≝ +λd.λmap:aux_map_type d.λstr. + match get_max_map_aux d map str with + [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ] + | Some x ⇒ new_max_map_aux d map str (S x) + ]. -let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝ - match trasf with +definition add_desc_env_flatEnv_fe ≝ +λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc. + fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)]) + (DESC_ELEM c desc) ]. + +let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝ + match trsf with [ nil ⇒ (λx.x) - | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))) + | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))) ]. -lemma build_trasfEnv_exists_aux : ∀a.∀trsf:aux_trasfEnv_type.∀c. - ∃b.build_trasfEnv trsf (c§§a) = (b§§a). - intros 2; - elim trsf; - [ simplify; exists; [apply c | reflexivity] - | simplify; apply H; ] +let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : + Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝ + match trsf with + [ nil ⇒ (λx.x) + | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t) + (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h)) + (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))) + ]. + +(* avanzamento dell'invariante *) +axiom env_map_flatEnv_enter_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe. + +axiom env_map_flatEnv_add_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d + (build_trasfEnv_env d trsf e) + (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))) + (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))). + +lemma env_map_flatEnv_addNil_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d + (build_trasfEnv_env d [] e) + (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))) + (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))). + intros; + simplify; + apply H. qed. -lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e. +lemma env_map_flatEnv_addSingle_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d + (add_desc_env d e name const desc) + (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))) + (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))). intros; - change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e); - cases (build_trasfEnv_exists_aux e trsf []); - rewrite > H; - reflexivity. + apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]); + apply H. qed. -(* NB: leave ... enter e' equivalente a e originale *) -lemma retype_enter_leave_to_e_aux : ∀e,fe,str,cur,trsf. - (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str → - get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)) → - (check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)). - intros 5; - rewrite > (eq_enter_leave e trsf); +lemma env_map_flatEnv_addJoin_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf. + env_to_flatEnv_inv d + (build_trasfEnv_env d trsf (add_desc_env d e name const desc)) + map fe → + env_to_flatEnv_inv d + (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e) + map fe. intros; - apply H; - apply H1. + simplify; + apply H. qed. -let rec retype_enter_leave_to_e (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type) - (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe) on map : aux_trasfMap_type e fe ≝ - match map with - [ nil ⇒ [] - | cons h tl ⇒ match h with - [ MAX_CUR_ELEM str cur max dim ⇒ - [MAX_CUR_ELEM e fe str cur max (retype_enter_leave_to_e_aux e fe str cur trsf dim)]@(retype_enter_leave_to_e e fe trsf tl) - ]]. - -lemma retype_e_to_enter_leave_aux : ∀e,fe,str,cur,trsf. - (check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → - (check_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str → - get_desc_env (leave_env ((build_trasfEnv trsf) (enter_env e))) str = get_desc_flatEnv fe (STR_ID str cur)). - intros 5; - rewrite < (eq_enter_leave e trsf) in ⊢ ((? % ?→?)→?); - rewrite < (eq_enter_leave e trsf) in ⊢ ((?→? ? (? % ?) ?)→?); +lemma env_map_flatEnv_add_aux_fe_al : + ∀trsf.∀d.∀m:aux_map_type d.∀a,l. + snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) = + a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))). + intro; + elim trsf; + [ simplify; reflexivity + | simplify; + elim a; + simplify; + rewrite > (H ????); + reflexivity + ]. +qed. + +lemma env_map_flatEnv_add_aux_fe_l : + ∀trsf.∀d.∀m:aux_map_type d.∀l. + snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) = + l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))). intros; - apply H; - apply H1. + elim l; + [ simplify; reflexivity + | rewrite > (env_map_flatEnv_add_aux_fe_al ????); + rewrite > H; + reflexivity + ]. qed. -let rec retype_e_to_enter_leave (e:aux_env_type) (fe:aux_flatEnv_type) (trsf:aux_trasfEnv_type) - (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe ≝ - match map with - [ nil ⇒ [] - | cons h tl ⇒ match h with - [ MAX_CUR_ELEM str cur max dim ⇒ - [MAX_CUR_ELEM (leave_env ((build_trasfEnv trsf) (enter_env e))) fe str cur max (retype_e_to_enter_leave_aux e fe str cur trsf dim)]@(retype_e_to_enter_leave e fe trsf tl) - ]]. - -(* NB: enter non cambia fe *) -lemma retype_e_to_enter_aux : ∀e,fe,str,cur. - (check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → - (check_desc_env (enter_env e) str → - get_desc_env (enter_env e) str = get_desc_flatEnv fe (STR_ID str cur)). - intros 6; - rewrite > H; - [ reflexivity - | apply H1 +lemma env_map_flatEnv_add_aux_fe : + ∀d.∀map:aux_map_type d.∀fe,trsf. + ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))). + intros 3; + elim fe 0; + [ simplify; + intro; + exists; + [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map []))) + | reflexivity + ] + | intros 4; + exists; + [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map []))) + | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l); + rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l); + rewrite < (cons_append_commute ????); + reflexivity + ] ]. qed. -let rec retype_e_to_enter (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (enter_env e) fe ≝ - match map with - [ nil ⇒ [] - | cons h tl ⇒ match h with - [ MAX_CUR_ELEM str cur max dim ⇒ - [MAX_CUR_ELEM (enter_env e) fe str cur max (retype_e_to_enter_aux e fe str cur dim)]@(retype_e_to_enter e fe tl) - ]]. - -(* NB: leave non cambia fe *) -axiom retype_e_to_leave_aux : ∀e,fe,str,cur. - (check_desc_env e str → - get_desc_env e str = get_desc_flatEnv fe (STR_ID str cur)) → - (check_desc_env (leave_env e) str → - get_desc_env (leave_env e) str = get_desc_flatEnv fe (STR_ID str cur)). - -let rec retype_e_to_leave (e:aux_env_type) (fe:aux_flatEnv_type) (map:aux_trasfMap_type e fe) on map : aux_trasfMap_type (leave_env e) fe ≝ - match map with - [ nil ⇒ [] - | cons h tl ⇒ match h with - [ MAX_CUR_ELEM str cur max dim ⇒ - [MAX_CUR_ELEM (leave_env e) fe str cur max (retype_e_to_leave_aux e fe str cur dim)]@(retype_e_to_leave e fe tl) - ]]. +lemma buildtrasfenvadd_to_le : + ∀d.∀m:aux_map_type d.∀fe,trsf. + le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true. + intros 4; + cases (env_map_flatEnv_add_aux_fe d m fe trsf); + rewrite < H; + rewrite > (le_to_leflatenv fe x); + reflexivity. +qed. -let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (trsf:aux_trasfEnv_type) (map:aux_trasfMap_type (leave_env ((build_trasfEnv trsf) (enter_env e))) fe') - (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝ - match map with - [ nil ⇒ empty_trasfMap e fe' - | cons h tl ⇒ - match get_maxcur_map e fe snap (get_name_maxCur ?? h) with - [ None ⇒ retype_enter_leave_to_e e fe' trsf [h] - | Some new ⇒ - [ MAX_CUR_ELEM ?? (get_name_maxCur ?? h) (get_cur_maxCur ?? new) - (get_max_maxCur ?? h) (False_rect ? daemon) ] - ] @ rollback_map e fe fe' trsf tl snap - ]. +axiom env_map_flatEnv_leave_aux : + ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf. + env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe → + env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe. -(* sequenza di utilizzo: - -[BLOCCO ESTERNO] - -|DICHIARAZIONE "pippo": -| -) MAP1 <- add_maxcur_map MAP0 "pippo" -| -) ENV1 <- add_desc_flatEnv ENV0 (name_to_nameId MAP1 "pippo") DESC -| -|ACCESSO "pippo": -| -) name_to_nameId MAP1 "pippo" -| -|PREPARAZIONE ENTRATA BLOCCO INTERNO: -| -) SNAP <- build_snapshot MAP1 - - |[BLOCCO INTERNO] - | - |DICHIARAZIONE "pippo": - | -) MAP2 <- add_maxcur_map MAP1 "pippo" - | -) ENV2 <- add_desc_flatEnv ENV (name_to_nameId MAP2 "pippo") DESC - | - |ACCESSO "pippo": - | -) name_to_nameId MAP2 "pippo" - | - |PREPARAZIONE USCITA BLOCCO INTERNO: - | -) MAP3 <- rollback_map MAP2 SNAP - -| ... -*) +lemma leave_add_enter_env_aux : + ∀d.∀a:aux_env_type d.∀trsf.∀c. + ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a). + intros 3; + elim trsf; + [ simplify; exists; [ apply c | reflexivity ] + | simplify; apply H + ]. +qed. -(* mini test -definition pippo ≝ [ ch_P ]. -definition pluto ≝ [ ch_Q ]. -definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8). -definition pippodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16). -definition pippodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32). -definition plutodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8). -definition plutodesc2 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD16). -definition plutodesc3 ≝ (AST_TYPE_BASE AST_BASE_TYPE_WORD32). - -definition map1 ≝ add_maxcur_map empty_env empty_flatEnv (empty_trasfMap ??) (empty_trasfMap ??) pippo false pippodesc1. -definition env1 ≝ add_desc_env empty_env pippo false pippodesc1. -definition fenv1 ≝ add_desc_flatEnv empty_flatEnv (next_nameId empty_env empty_flatEnv (empty_trasfMap ??) pippo) false pippodesc1. -definition map2 ≝ add_maxcur_map env1 fenv1 map1 map1 pluto false plutodesc1. -definition env2 ≝ add_desc_env env1 pluto false plutodesc1. -definition fenv2 ≝ add_desc_flatEnv fenv1 (next_nameId ?? map1 pluto) false plutodesc1. - -definition env2' ≝ enter_env env2. -definition map2' ≝ retype_e_to_enter env2 fenv2 map2. - -definition map3 ≝ add_maxcur_map env2' fenv2 map2' map2' pippo true pippodesc2. -definition env3 ≝ add_desc_env env2' pippo true pippodesc2. -definition fenv3 ≝ add_desc_flatEnv fenv2 (next_nameId ?? map2' pippo) true pippodesc2. -definition map4 ≝ add_maxcur_map env3 fenv3 map3 map3 pluto true plutodesc2. -definition env4 ≝ add_desc_env env3 pluto true plutodesc2. -definition fenv4 ≝ add_desc_flatEnv fenv3 (next_nameId ?? map3 pluto) true plutodesc2. - -definition env4' ≝ enter_env env4. -definition map4' ≝ retype_e_to_enter env4 fenv4 map4. - -definition map5 ≝ add_maxcur_map env4' fenv4 map4' map4' pippo false pippodesc3. -definition env5 ≝ add_desc_env env4' pippo false pippodesc3. -definition fenv5 ≝ add_desc_flatEnv fenv4 (next_nameId ?? map4' pippo) false pippodesc3. -definition map6 ≝ add_maxcur_map env5 fenv5 map5 map5 pluto false plutodesc3. -definition env6 ≝ add_desc_env env5 pluto false plutodesc3. -definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false plutodesc3. - -definition map6' ≝ retype_e_to_leave env6 fenv6 map6. - -definition map7 ≝ rollback_map env4 fenv4 fenv6 [ tripleT ??? pluto false plutodesc3 ; tripleT ??? pippo false pippodesc3 ] map6' map4. - -definition map7' ≝ retype_e_to_leave env4 fenv6 map7. - -definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2. -*) +lemma leave_add_enter_env : + ∀d.∀e:aux_env_type d.∀trsf. + leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e. + intros; + unfold enter_env; + lapply (leave_add_enter_env_aux d e trsf []); + cases Hletin; + rewrite > H; + simplify; + reflexivity. +qed. + +lemma newid_from_init : + ∀d.∀e:aux_env_type d.∀name,const,desc. + ast_id d (add_desc_env d e name const desc) const desc. + intros; + lapply (AST_ID d (add_desc_env d e name const desc) name ?); + [ elim e; + simplify; + rewrite > (eq_to_eqstr ?? (refl_eq ??)); + simplify; + apply I + | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧ + desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name)); + [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?); + rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %); + apply Hletin + | split; + [ elim e; + simplify; + rewrite > (eq_to_eqstr ?? (refl_eq ??)); + simplify; + reflexivity + | elim e; + simplify; + rewrite > (eq_to_eqstr ?? (refl_eq ??)); + simplify; + reflexivity + ] + ] + ]. +qed. diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma deleted file mode 100755 index 9202ff86d..000000000 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma +++ /dev/null @@ -1,526 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* ********************************************************************** *) -(* *) -(* Sviluppato da: *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) -(* *) -(* ********************************************************************** *) - -include "compiler/environment.ma". - -(* ********************** *) -(* GESTIONE AMBIENTE FLAT *) -(* ********************** *) - -(* ambiente flat *) -inductive var_flatElem : Type ≝ -VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem. - -definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ]. -definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ]. - -definition aux_flatEnv_type ≝ list var_flatElem. - -definition empty_flatEnv ≝ nil var_flatElem. - -(* mappa: nome + max + cur *) -inductive n_list : nat → Type ≝ - n_nil: n_list O -| n_cons: ∀n.option nat → n_list n → n_list (S n). - -definition defined_nList ≝ -λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ]. - -definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝ -λd.λl:n_list d.λp:defined_nList ? l. - let value ≝ - match l - return λX.λY:n_list X.defined_nList X Y → n_list (pred X) - with - [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p - | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t - ] p in value. - -definition get_first_nList : Πd.n_list d → ? → option nat ≝ -λd.λl:n_list d.λp:defined_nList ? l. - let value ≝ - match l - return λX.λY:n_list X.defined_nList X Y → option nat - with - [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p - | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h - ] p in value. - -inductive map_elem (d:nat) : Type ≝ -MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d. - -definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ]. -definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ]. -definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ]. - -definition aux_map_type ≝ λd.list (map_elem d). - -definition empty_map ≝ nil (map_elem O). - -lemma defined_nList_S_to_true : -∀d.∀l:n_list (S d).defined_nList (S d) l = True. - intros; - inversion l; - [ intros; destruct H - | intros; simplify; reflexivity - ] -qed. - -lemma defined_get_id : - ∀d.∀h:map_elem d.defined_nList (S d) (get_cur_mapElem d h). - intros 2; - rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h)); - apply I. -qed. - -(* get_id *) -let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝ - match map with - [ nil ⇒ None ? - | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with - [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??) - | false ⇒ get_id_map_aux d t name - ] - ]. - -definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. - -(* get_max *) -let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝ - match map with - [ nil ⇒ None ? - | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with - [ true ⇒ Some ? (get_max_mapElem d h) - | false ⇒ get_max_map_aux d t name - ] - ]. - -definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. - -(* check_id *) -definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ]. - -definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ]. - -lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name. - unfold checkb_id_map; - unfold check_id_map; - intros 3; - elim (get_id_map_aux d map name) 0; - [ simplify; intro; destruct H - | simplify; intros; apply I - ]. -qed. - -definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ]. - -definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. - match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ]. - -lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name. - unfold checknotb_id_map; - unfold checknot_id_map; - intros 3; - elim (get_id_map_aux d map name) 0; - [ simplify; intro; apply I - | simplify; intros; destruct H - ]. -qed. - -(* get_desc *) -let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝ - match fe with - [ nil ⇒ None ? - | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with - [ true ⇒ Some ? (get_desc_flatVar h) - | false ⇒ get_desc_flatEnv_aux t name - ] - ]. - -definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux fe str with - [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. - -definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ]. - -definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ]. - -lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str. - unfold checkb_desc_flatEnv; - unfold check_desc_flatEnv; - intros 2; - elim (get_desc_flatEnv_aux fe str) 0; - [ simplify; intro; destruct H - | simplify; intros; apply I - ]. -qed. - -definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ]. - -definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ]. - -lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str. - unfold checknotb_desc_flatEnv; - unfold checknot_desc_flatEnv; - intros 2; - elim (get_desc_flatEnv_aux fe str) 0; - [ simplify; intro; apply I - | simplify; intros; destruct H - ]. -qed. - -(* fe <= fe' *) -definition eq_flatEnv_elem ≝ -λe1,e2.match e1 with - [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with - [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]]. - -lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true. - intros 3; - rewrite < H; - elim e1; - simplify; - rewrite > (eq_to_eqstrid a a (refl_eq ??)); - rewrite > (eq_to_eqdescelem d d (refl_eq ??)); - reflexivity. -qed. - -lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2. - intros 2; - elim e1 0; - elim e2 0; - intros 4; - simplify; - intro; - rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H)); - rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H)); - reflexivity. -qed. - -let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝ -match fe with - [ nil ⇒ true - | cons h tl ⇒ match fe' with - [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ] - ]. - -lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true. - intros 3; - rewrite < H; - elim e1; - [ reflexivity - | simplify; - rewrite > (eq_to_eqflatenv a a (refl_eq ??)); - rewrite > H1; - reflexivity - ]. -qed. - -lemma leflatEnv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'. - intro; - elim fe 0; - [ intros; exists; [ apply fe' | reflexivity ] - | intros 4; elim fe'; - [ simplify in H1:(%); destruct H1 - | simplify in H2:(%); - rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2)); - cases (H l1 (andb_true_true_r ?? H2)); - simplify; - rewrite < H3; - exists; [ apply x | reflexivity ] - ] - ]. -qed. - -lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true. - intros; - elim fe; - [ simplify; - reflexivity - | simplify; - rewrite > (eq_to_eqflatenv a a (refl_eq ??)); - rewrite > H; - reflexivity - ]. -qed. - -lemma leflatenv_to_check : ∀fe,fe',str. - (le_flatEnv fe fe' = true) → - (check_desc_flatEnv fe str) → - (check_desc_flatEnv fe' str). - intros 4; - cases (leflatEnv_to_le fe fe' H); - rewrite < H1; - elim fe 0; - [ intro; simplify in H2:(%); elim H2; - | intros 3; - simplify; - cases (eqStrId_str str (get_name_flatVar a)); - [ simplify; intro; apply H3 - | simplify; apply H2 - ] - ]. -qed. - -lemma leflatenv_to_get : ∀fe,fe',str. - (le_flatEnv fe fe' = true) → - (check_desc_flatEnv fe str) → - (get_desc_flatEnv fe str = get_desc_flatEnv fe' str). - intros 4; - cases (leflatEnv_to_le fe fe' H); - rewrite < H1; - elim fe 0; - [ intro; - simplify in H2:(%); - elim H2 - | simplify; - intros 2; - cases (eqStrId_str str (get_name_flatVar a)); - [ simplify; - intros; - reflexivity - | simplify; - unfold check_desc_flatEnv; - unfold get_desc_flatEnv; - cases (get_desc_flatEnv_aux l str); - [ simplify; intros; elim H3 - | simplify; intros; rewrite < (H2 H3); reflexivity - ] - ] - ]. -qed. - -(* invariante *) -definition env_to_flatEnv_inv ≝ - λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type. - ∀str. - check_desc_env e str → - (check_id_map d map str ∧ - check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧ - get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))). - -lemma inv_to_checkdescflatenv : - ∀d.∀e.∀map:aux_map_type d.∀fe. - env_to_flatEnv_inv d e map fe → - (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))). - intros 7; - unfold env_to_flatEnv_inv in H:(%); - lapply (H str H1); - apply (proj2 ?? (proj1 ?? Hletin)); -qed. - -lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv. - unfold env_to_flatEnv_inv; - unfold empty_env; - unfold empty_map; - unfold empty_flatEnv; - simplify; - intros; - split; - [ split; apply H | reflexivity ]. -qed. - -lemma leflatenv_to_inv : - ∀d.∀e.∀map:aux_map_type d.∀fe,fe'. - le_flatEnv fe fe' = true → - env_to_flatEnv_inv d e map fe → - env_to_flatEnv_inv d e map fe'. - intros 6; - unfold env_to_flatEnv_inv; - intros; - split; - [ split; - [ lapply (H1 str H2); - apply (proj1 ?? (proj1 ?? Hletin)) - | lapply (H1 str H2); - apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin))) - ] - | lapply (H1 str H2); - rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin))); - apply (proj2 ?? Hletin) - ]. -qed. - -lemma leflatenv_trans : - ∀fe,fe',fe''. - le_flatEnv fe fe' = true → - le_flatEnv fe' fe'' = true → - le_flatEnv fe fe'' = true. - intros 4; - cases (leflatenv_to_le fe ? H); - rewrite < H1; - intro; - cases (leflatenv_to_le (fe@x) fe'' H2); - rewrite < H3; - rewrite > associative_append; - apply (le_to_leflatenv fe ?). -qed. - -(* enter: propaga in testa la vecchia testa (il "cur" precedente) *) -let rec enter_map d (map:aux_map_type d) on map ≝ - match map with - [ nil ⇒ [] - | cons h t ⇒ - (MAP_ELEM (S d) - (get_name_mapElem d h) - (get_max_mapElem d h) - (n_cons (S d) - (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ??)) - (get_cur_mapElem d h)) - )::(enter_map d t) - ]. - -lemma getidmap_to_enter : - ∀d.∀m:aux_map_type d.∀str. - get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str. - intros; - elim m; - [ simplify; reflexivity - | simplify; rewrite > H; reflexivity - ] -qed. - -lemma env_map_flatEnv_enter_aux : - ∀d.∀e.∀map:aux_map_type d.∀fe. - env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe. - intros 3; - unfold enter_env; - unfold empty_env; - unfold env_to_flatEnv_inv; - simplify; - elim e 0; - [ elim map 0; - [ simplify; intros; split; - [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ] - | simplify; intros; split; - [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2)) - | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2)) - ] - ] - | elim map 0; - [ simplify; intros; split; - [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ] - | simplify; intros; split; - [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3)) - | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3)) - ] - ] - ]. -qed. - -(* leave: elimina la testa (il "cur" corrente) *) -let rec leave_map d (map:aux_map_type (S d)) on map ≝ - match map with - [ nil ⇒ [] - | cons h t ⇒ - (MAP_ELEM d - (get_name_mapElem (S d) h) - (get_max_mapElem (S d) h) - (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ??)) - )::(leave_map d t) - ]. - -(* aggiungi descrittore *) -let rec new_map_elem_from_depth_aux (d:nat) on d ≝ - match d - return λd.n_list d - with - [ O ⇒ n_nil - | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n) - ]. - -let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝ - match map with - [ nil ⇒ [] - | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with - [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ??))) - | false ⇒ h - ]::(new_max_map_aux d t name max) - ]. - -definition add_desc_env_flatEnv_map ≝ -λd.λmap:aux_map_type d.λstr. - match get_max_map_aux d map str with - [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ] - | Some x ⇒ new_max_map_aux d map str (S x) - ]. - -definition add_desc_env_flatEnv_fe ≝ -λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc. - fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)]) - (DESC_ELEM c desc) ]. - -let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝ - match trsf with - [ nil ⇒ e - | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)) - ]. - -let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝ - match trasf with - [ nil ⇒ mfe - | cons h t ⇒ - build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h)) - (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))) - ]. - -(* avanzamento delle dimostrazioni *) -axiom env_map_flatEnv_add_aux : - ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf. - env_to_flatEnv_inv d e map fe → - env_to_flatEnv_inv d - (build_trasfEnv_env trsf e) - (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))) - (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))). - -axiom env_map_flatEnv_add_aux_fe : - ∀d.∀map:aux_map_type d.∀fe,trsf. - ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))). - -lemma buildtrasfenvadd_to_le : - ∀d.∀m:aux_map_type d.∀fe,trsf. - le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true. - intros 4; - cases (env_map_flatEnv_add_aux_fe d m fe trsf); - rewrite < H; - rewrite > (le_to_leflatenv fe x); - reflexivity. -qed. - -axiom env_map_flatEnv_leave_aux : - ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf. - env_to_flatEnv_inv (S d) - (build_trasfEnv_env trsf (enter_env e)) - (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))) - (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))) → - env_to_flatEnv_inv d - e - (leave_map d (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe)))) - (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))). diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma index 813157082..2603787be 100755 --- a/helm/software/matita/contribs/assembly/compiler/environment.ma +++ b/helm/software/matita/contribs/assembly/compiler/environment.ma @@ -36,7 +36,40 @@ inductive var_elem : Type ≝ VAR_ELEM: aux_str_type → desc_elem → var_elem. (* ambiente globale: (ambiente base + ambienti annidati) *) -definition aux_env_type ≝ ne_list (list var_elem). +inductive env_list : nat → Type ≝ + env_nil: list var_elem → env_list O +| env_cons: ∀n.list var_elem → env_list n → env_list (S n). + +definition defined_envList ≝ +λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ]. + +definition cut_first_envList : Πd.env_list d → ? → env_list (pred d) ≝ +λd.λl:env_list d.λp:defined_envList ? l. + let value ≝ + match l + return λX.λY:env_list X.defined_envList X Y → env_list (pred X) + with + [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect ? p + | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t + ] p in value. + +definition get_first_envList ≝ +λd.λl:env_list d. + match l with + [ env_nil h ⇒ h + | env_cons _ h _ ⇒ h + ]. + +lemma defined_envList_S : +∀d.∀l:env_list (S d).defined_envList (S d) l. + intros; + inversion l; + [ intros; destruct H + | intros; simplify; apply I + ] +qed. + +definition aux_env_type ≝ λd.env_list d. (* getter *) definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ]. @@ -70,14 +103,14 @@ definition get_name_var ≝ λv:var_elem.match v with [ VAR_ELEM n _ ⇒ n ]. definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ]. (* ambiente vuoto *) -definition empty_env ≝ ne_nil ? (nil var_elem ). +definition empty_env ≝ env_nil []. (* setter *) -definition enter_env ≝ λe:aux_env_type.empty_env&e. -definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e. +definition enter_env ≝ λd.λe:aux_env_type d.env_cons d [] e. +definition leave_env ≝ λd.λe:aux_env_type (S d).cut_first_envList (S d) e (defined_envList_S ??). (* recupera descrittore da ambiente: il primo trovato, ma e' anche l'unico *) -let rec get_desc_from_lev_env (env:list var_elem ) (str:aux_str_type) on env ≝ +let rec get_desc_from_lev_env (env:list var_elem) (str:aux_str_type) on env ≝ match env with [ nil ⇒ None ? | cons h t ⇒ match eqStr_str str (get_name_var h) with @@ -85,44 +118,44 @@ match env with | false ⇒ get_desc_from_lev_env t str ]]. (* recupera descrittore da ambiente globale: il primo trovato *) -let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝ +let rec get_desc_env_aux d (env:aux_env_type d) (str:aux_str_type) on env ≝ match env with - [ ne_nil h ⇒ get_desc_from_lev_env h str - | ne_cons h t ⇒ match get_desc_from_lev_env h str with - [ None ⇒ get_desc_env_aux t str | Some res' ⇒ Some ? res' ] + [ env_nil h ⇒ get_desc_from_lev_env h str + | env_cons n h t ⇒ match get_desc_from_lev_env h str with + [ None ⇒ get_desc_env_aux n t str | Some res' ⇒ Some ? res' ] ]. -definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_env_aux e str with [ None ⇒ False | Some _ ⇒ True ]. +definition check_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type. + match get_desc_env_aux d e str with [ None ⇒ False | Some _ ⇒ True ]. -definition checkb_desc_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_env_aux e str with [ None ⇒ false | Some _ ⇒ true ]. +definition checkb_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type. + match get_desc_env_aux d e str with [ None ⇒ false | Some _ ⇒ true ]. -lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str. +lemma checkbdescenv_to_checkdescenv : ∀d.∀e:aux_env_type d.∀str.checkb_desc_env d e str = true → check_desc_env d e str. unfold checkb_desc_env; unfold check_desc_env; intros; - letin K ≝ (get_desc_env_aux e str); + letin K ≝ (get_desc_env_aux d e str); elim K; [ normalize; autobatch | normalize; autobatch ] qed. -definition get_desc_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_env_aux e str with +definition get_desc_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type. + match get_desc_env_aux d e str with [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. -definition check_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ]. +definition check_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type. + match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ True | Some _ ⇒ False ]. -definition checkb_not_already_def_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_from_lev_env (get_first_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ]. +definition checkb_not_already_def_env ≝ λd.λe:aux_env_type d.λstr:aux_str_type. + match get_desc_from_lev_env (get_first_envList d e) str with [ None ⇒ true | Some _ ⇒ false ]. -lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀e,str.checkb_not_already_def_env e str = true → check_not_already_def_env e str. +lemma checkbnotalreadydefenv_to_checknotalreadydefenv : ∀d.∀e:aux_env_type d.∀str.checkb_not_already_def_env d e str = true → check_not_already_def_env d e str. unfold checkb_not_already_def_env; unfold check_not_already_def_env; intros; - letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str); + letin K ≝ (get_desc_from_lev_env (get_first_envList d e) str); elim K; [ normalize; autobatch | normalize; autobatch ] @@ -130,11 +163,13 @@ qed. (* aggiungi descrittore ad ambiente globale: in testa al primo ambiente *) definition add_desc_env ≝ -λe:aux_env_type.λstr:aux_str_type.λc:bool.λdesc:ast_type. +λd.λe:aux_env_type d.λstr:aux_str_type.λc:bool.λdesc:ast_type. (*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*) - match e with - [ ne_nil h ⇒ ne_nil ? ((VAR_ELEM str (DESC_ELEM c desc))::h) - | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl + match e + return λX.λe:aux_env_type X.aux_env_type X + with + [ env_nil h ⇒ env_nil ((VAR_ELEM str (DESC_ELEM c desc))::h) + | env_cons n h t ⇒ env_cons n ((VAR_ELEM str (DESC_ELEM c desc))::h) t ]. (* controllo e <= e' *) diff --git a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma index 49a027ba7..a5db9536b 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma @@ -40,53 +40,53 @@ include "compiler/sigma.ma". (* operatore di cast *) definition preast_to_ast_expr_check ≝ -λe:aux_env_type.λsig:(Σt'.ast_expr e t').λt:ast_type. +λd.λe:aux_env_type d.λsig:(Σt'.ast_expr d e t').λt:ast_type. match sig with [ sigma_intro t' expr ⇒ match eq_ast_type t' t - return λx.eq_ast_type t' t = x → option (ast_expr e t) + return λx.eq_ast_type t' t = x → option (ast_expr d e t) with - [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (eqasttype_to_eq ?? p)) + [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr d e t) expr t (eqasttype_to_eq ?? p)) | false ⇒ λp:(eq_ast_type t' t = false).None ? ] (refl_eq ? (eq_ast_type t' t)) ]. definition preast_to_ast_init_check ≝ -λe:aux_env_type.λsig:Σt'.ast_init e t'.λt:ast_type. +λd.λe:aux_env_type d.λsig:Σt'.ast_init d e t'.λt:ast_type. match sig with [ sigma_intro t' expr ⇒ match eq_ast_type t' t - return λx.eq_ast_type t' t = x → option (ast_init e t) + return λx.eq_ast_type t' t = x → option (ast_init d e t) with - [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init e t) expr t (eqasttype_to_eq ?? p)) + [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init d e t) expr t (eqasttype_to_eq ?? p)) | false ⇒ λp:(eq_ast_type t' t = false).None ? ] (refl_eq ? (eq_ast_type t' t)) ]. definition preast_to_ast_var_checkb ≝ -λe:aux_env_type.λt:ast_type.λsig:(Σb'.ast_var e b' t).λb:bool. +λd.λe:aux_env_type d.λt:ast_type.λsig:(Σb'.ast_var d e b' t).λb:bool. match sig with [ sigma_intro b' var ⇒ match eq_bool b' b - return λx.eq_bool b' b = x → option (ast_var e b t) + return λx.eq_bool b' b = x → option (ast_var d e b t) with - [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var e b t) var b (eqbool_to_eq ?? p)) + [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var d e b t) var b (eqbool_to_eq ?? p)) | false ⇒ λp:(eq_bool b' b = false).None ? ] (refl_eq ? (eq_bool b' b)) ]. definition preast_to_ast_var_checkt ≝ -λe:aux_env_type.λb:bool.λsig:(Σt'.ast_var e b t').λt:ast_type. +λd.λe:aux_env_type d.λb:bool.λsig:(Σt'.ast_var d e b t').λt:ast_type. match sig with [ sigma_intro t' var ⇒ match eq_ast_type t' t - return λx.eq_ast_type t' t = x → option (ast_var e b t) + return λx.eq_ast_type t' t = x → option (ast_var d e b t) with - [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var e b t) var t (eqasttype_to_eq ?? p)) + [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var d e b t) var t (eqasttype_to_eq ?? p)) | false ⇒ λp:(eq_ast_type t' t = false).None ? ] (refl_eq ? (eq_ast_type t' t)) ]. definition preast_to_ast_var_check ≝ -λe:aux_env_type.λsig:(Σb'.(Σt'.ast_var e b' t')).λb:bool.λt:ast_type. - opt_map ?? (preast_to_ast_var_checkt e (sigmaFst ?? sig) (sigmaSnd ?? sig) t) - (λres1.opt_map ?? (preast_to_ast_var_checkb e t ≪(sigmaFst ?? sig),res1≫ b) +λd.λe:aux_env_type d.λsig:(Σb'.(Σt'.ast_var d e b' t')).λb:bool.λt:ast_type. + opt_map ?? (preast_to_ast_var_checkt d e (sigmaFst ?? sig) (sigmaSnd ?? sig) t) + (λres1.opt_map ?? (preast_to_ast_var_checkb d e t ≪(sigmaFst ?? sig),res1≫ b) (λres2.Some ? res2)). (* @@ -116,220 +116,220 @@ definition preast_to_ast_var_check ≝ PREAST_EXPR_W32toW16: preast_expr → preast_expr PREAST_EXPR_ID: preast_var → preast_expr *) -let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt.ast_expr e t) ≝ +let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on preast : option (Σt.ast_expr d e t) ≝ match preast with - [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 e val)≫ - | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 e val)≫ - | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 e val)≫ + [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 d e val)≫ + | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 d e val)≫ + | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 d e val)≫ | PREAST_EXPR_NEG subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType)) - (λres.Some ? ≪?,(AST_EXPR_NEG e ? res)≫) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType)) + (λres.Some ? ≪?,(AST_EXPR_NEG d e ? res)≫) | _ ⇒ None ? ]) | PREAST_EXPR_NOT subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType)) - (λres.Some ? ≪?,(AST_EXPR_NOT e ? res)≫) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType)) + (λres.Some ? ≪?,(AST_EXPR_NOT d e ? res)≫) | _ ⇒ None ? ]) | PREAST_EXPR_COM subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType)) - (λres.Some ? ≪?,(AST_EXPR_COM e ? res)≫) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType)) + (λres.Some ? ≪?,(AST_EXPR_COM d e ? res)≫) | _ ⇒ None ? ]) | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_ADD e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_ADD d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_SUB e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_SUB d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_MUL e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_MUL d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_DIV e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_DIV d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) - (λres2.Some ? ≪?,(AST_EXPR_SHR e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) + (λres2.Some ? ≪?,(AST_EXPR_SHR d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) - (λres2.Some ? ≪?,(AST_EXPR_SHL e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) + (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_GT e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_GT d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_GTE e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_GTE d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_LT subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_LT e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_LT d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_LTE e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_LTE d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_EQ e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_EQ d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒ - opt_map ?? (preast_to_ast_expr subExpr1 e) - (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e) - (λsigmaRes2:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr subExpr1 d e) + (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e) + (λsigmaRes2:(Σt.ast_expr d e t). match (sigmaFst ?? sigmaRes1) with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType)) - (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType)) - (λres2.Some ? ≪?,(AST_EXPR_NEQ e ? res1 res2)≫)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType)) + (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType)) + (λres2.Some ? ≪?,(AST_EXPR_NEQ d e ? res1 res2)≫)) | _ ⇒ None ? ])) | PREAST_EXPR_B8toW16 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) - (λres.Some ? ≪?,(AST_EXPR_B8toW16 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) + (λres.Some ? ≪?,(AST_EXPR_B8toW16 d e res)≫)) | PREAST_EXPR_B8toW32 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) - (λres.Some ? ≪?,(AST_EXPR_B8toW32 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)) + (λres.Some ? ≪?,(AST_EXPR_B8toW32 d e res)≫)) | PREAST_EXPR_W16toB8 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16)) - (λres.Some ? ≪?,(AST_EXPR_W16toB8 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16)) + (λres.Some ? ≪?,(AST_EXPR_W16toB8 d e res)≫)) | PREAST_EXPR_W16toW32 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16)) - (λres.Some ? ≪?,(AST_EXPR_W16toW32 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16)) + (λres.Some ? ≪?,(AST_EXPR_W16toW32 d e res)≫)) | PREAST_EXPR_W32toB8 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32)) - (λres.Some ? ≪?,(AST_EXPR_W32toB8 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32)) + (λres.Some ? ≪?,(AST_EXPR_W32toB8 d e res)≫)) | PREAST_EXPR_W32toW16 subExpr ⇒ - opt_map ?? (preast_to_ast_expr subExpr e) - (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32)) - (λres.Some ? ≪?,(AST_EXPR_W32toW16 e res)≫)) + opt_map ?? (preast_to_ast_expr subExpr d e) + (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32)) + (λres.Some ? ≪?,(AST_EXPR_W32toW16 d e res)≫)) | PREAST_EXPR_ID var ⇒ - opt_map ?? (preast_to_ast_var var e) - (λsigmaRes:(Σb.(Σt.ast_var e b t)). + opt_map ?? (preast_to_ast_var var d e) + (λsigmaRes:(Σb.(Σt.ast_var d e b t)). match sigmaRes with [ sigma_intro b sigmaRes' ⇒ match sigmaRes' with [ sigma_intro t _ ⇒ - opt_map ?? (preast_to_ast_var_check e sigmaRes b t) - (λres.Some ? ≪?,(AST_EXPR_ID e ?? res)≫)]]) + opt_map ?? (preast_to_ast_var_check d e sigmaRes b t) + (λres.Some ? ≪?,(AST_EXPR_ID d e ?? res)≫)]]) ] (* PREAST_VAR_ID: aux_str_type → preast_var PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var PREAST_VAR_STRUCT: preast_var → nat → preast_var *) -and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option (Σb.(Σt.ast_var e b t)) ≝ +and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast : option (Σb.(Σt.ast_var d e b t)) ≝ match preast with [ PREAST_VAR_ID name ⇒ - match checkb_desc_env e name - return λx.checkb_desc_env e name = x → option (Σb.(Σt.ast_var e b t)) + match checkb_desc_env d e name + return λx.checkb_desc_env d e name = x → option (Σb.(Σt.ast_var d e b t)) with - [ true ⇒ λp:(checkb_desc_env e name = true). - let desc ≝ get_desc_env e name in + [ true ⇒ λp:(checkb_desc_env d e name = true). + let desc ≝ get_desc_env d e name in let b ≝ get_const_desc desc in let t ≝ get_type_desc desc in - Some ? ≪b,≪t,(AST_VAR_ID e b t (AST_ID e name (checkbdescenv_to_checkdescenv e name p)))≫≫ - | false ⇒ λp:(checkb_desc_env e name = false).None ? - ] (refl_eq ? (checkb_desc_env e name)) + Some ? ≪b,≪t,(AST_VAR_ID d e b t (AST_ID d e name (checkbdescenv_to_checkdescenv d e name p)))≫≫ + | false ⇒ λp:(checkb_desc_env d e name = false).None ? + ] (refl_eq ? (checkb_desc_env d e name)) | PREAST_VAR_ARRAY subVar expr ⇒ - opt_map ?? (preast_to_ast_var subVar e) - (λsigmaResV:(Σb.(Σt.ast_var e b t)). + opt_map ?? (preast_to_ast_var subVar d e) + (λsigmaResV:(Σb.(Σt.ast_var d e b t)). match sigmaResV with [ sigma_intro b sigmaResV' ⇒ match sigmaResV' with [ sigma_intro t _ ⇒ match t with [ AST_TYPE_ARRAY subType dim ⇒ - opt_map ?? (preast_to_ast_var_check e sigmaResV b (AST_TYPE_ARRAY subType dim)) + opt_map ?? (preast_to_ast_var_check d e sigmaResV b (AST_TYPE_ARRAY subType dim)) (λresVar. (* ASSERTO: 1) se l'indice e' un'espressione riducibile ad un valore deve essere gia' @@ -343,30 +343,30 @@ and preast_to_ast_var (preast:preast_var) (e:aux_env_type) on preast : option ( | PREAST_EXPR_WORD32 val ⇒ (λx.ltb (nat_of_word32 val) dim) | _ ⇒ (λx.true) ]) expr with [ true ⇒ - opt_map ?? (preast_to_ast_expr expr e) - (λsigmaResE:(Σt.ast_expr e t). + opt_map ?? (preast_to_ast_expr expr d e) + (λsigmaResE:(Σt.ast_expr d e t). match sigmaFst ?? sigmaResE with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaResE (AST_TYPE_BASE bType)) - (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY e b subType dim resVar (AST_BASE_EXPR e bType resExpr))≫≫) + opt_map ?? (preast_to_ast_expr_check d e sigmaResE (AST_TYPE_BASE bType)) + (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY d e b subType dim resVar (AST_BASE_EXPR d e bType resExpr))≫≫) | _ ⇒ None ? ]) | false ⇒ None ? ]) | _ ⇒ None ? ]]]) | PREAST_VAR_STRUCT subVar field ⇒ - opt_map ?? (preast_to_ast_var subVar e) - (λsigmaRes:(Σb.(Σt.ast_var e b t)). + opt_map ?? (preast_to_ast_var subVar d e) + (λsigmaRes:(Σb.(Σt.ast_var d e b t)). match sigmaRes with [ sigma_intro b sigmaRes' ⇒ match sigmaRes' with [ sigma_intro t _ ⇒ match t with [ AST_TYPE_STRUCT nelSubType ⇒ - opt_map ?? (preast_to_ast_var_check e sigmaRes b (AST_TYPE_STRUCT nelSubType)) + opt_map ?? (preast_to_ast_var_check d e sigmaRes b (AST_TYPE_STRUCT nelSubType)) (λresVar. match ltb field (len_neList ? nelSubType) - return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var e b t)) + return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var d e b t)) with [ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true). - Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT e b nelSubType field resVar p)≫≫ + Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT d e b nelSubType field resVar p)≫≫ | false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ? ] (refl_eq ? (ltb field (len_neList ? nelSubType))) ) @@ -467,17 +467,17 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option ( PREAST_INIT_VAR: preast_var → preast_init PREAST_INIT_VAL: preast_init_val → preast_init *) -definition preast_to_ast_init : preast_init → Πe.option (Σt.ast_init e t) ≝ -λpreast:preast_init.λe:aux_env_type.match preast with +definition preast_to_ast_init : preast_init → Πd.Πe:aux_env_type d.option (Σt.ast_init d e t) ≝ +λpreast:preast_init.λd.λe:aux_env_type d.match preast with [ PREAST_INIT_VAR var ⇒ - opt_map ?? (preast_to_ast_var var e) - (λsigmaRes:(Σb.(Σt.ast_var e b t)). - Some ? ≪?,(AST_INIT_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫) + opt_map ?? (preast_to_ast_var var d e) + (λsigmaRes:(Σb.(Σt.ast_var d e b t)). + Some ? ≪?,(AST_INIT_VAR d e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫) | PREAST_INIT_VAL val ⇒ opt_map ?? (preast_to_ast_init_val_aux val) (λsigmaRes:(Σt.aux_ast_init_type t). - Some ? ≪?,(AST_INIT_VAL e ? (sigmaSnd ?? sigmaRes))≫) + Some ? ≪?,(AST_INIT_VAL d e ? (sigmaSnd ?? sigmaRes))≫) ]. (* @@ -485,75 +485,75 @@ definition preast_to_ast_init : preast_init → Πe.option (Σt.ast_init e t) PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm *) -definition preast_to_ast_base_expr : preast_expr → Πe.option (ast_base_expr e) ≝ -λpreast:preast_expr.λe:aux_env_type. - opt_map ?? (preast_to_ast_expr preast e) - (λsigmaRes:(Σt.ast_expr e t). +definition preast_to_ast_base_expr : preast_expr → Πd.Πe:aux_env_type d.option (ast_base_expr d e) ≝ +λpreast:preast_expr.λd.λe:aux_env_type d. + opt_map ?? (preast_to_ast_expr preast d e) + (λsigmaRes:(Σt.ast_expr d e t). match sigmaFst ?? sigmaRes with [ AST_TYPE_BASE bType ⇒ - opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE bType)) - (λres.Some ? (AST_BASE_EXPR e ? res)) + opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType)) + (λres.Some ? (AST_BASE_EXPR d e ? res)) | _ ⇒ None ? ]). -let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝ +let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on preast : option (ast_stm d e) ≝ match preast with [ PREAST_STM_ASG var expr ⇒ - opt_map ?? (preast_to_ast_var var e) - (λsigmaResV:(Σb.(Σt.ast_var e b t)). + opt_map ?? (preast_to_ast_var var d e) + (λsigmaResV:(Σb.(Σt.ast_var d e b t)). match sigmaResV with [ sigma_intro _ sigmaResV' ⇒ match sigmaResV' with [ sigma_intro t _ ⇒ - opt_map ?? (preast_to_ast_var_check e sigmaResV false t) - (λresVar.opt_map ?? (preast_to_ast_expr expr e) - (λsigmaResE:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaResE t) - (λresExpr.Some ? (AST_STM_ASG e t resVar resExpr) + opt_map ?? (preast_to_ast_var_check d e sigmaResV false t) + (λresVar.opt_map ?? (preast_to_ast_expr expr d e) + (λsigmaResE:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaResE t) + (λresExpr.Some ? (AST_STM_ASG d e t resVar resExpr) )))]]) | PREAST_STM_WHILE expr decl ⇒ - opt_map ?? (preast_to_ast_base_expr expr e) - (λresExpr.opt_map ?? (preast_to_ast_decl decl (enter_env e)) - (λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl))) + opt_map ?? (preast_to_ast_base_expr expr d e) + (λresExpr.opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e)) + (λresDecl.Some ? (AST_STM_WHILE d e resExpr resDecl))) | PREAST_STM_IF nelExprDecl optDecl ⇒ - opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e) - (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (enter_env e)) + opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) d e) + (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (S d) (enter_env d e)) (λresDecl.opt_map ?? t (λt'.Some ? («£(pair ?? resExpr resDecl)»&t'))))) - (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL (enter_env e) (nil ?))))) + (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR d e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 d e 〈x0,x0〉)) (AST_NO_DECL (S d) (enter_env d e) (nil ?))))) nelExprDecl) (λres.match optDecl with - [ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?)) - | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (enter_env e)) - (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl))) + [ None ⇒ Some ? (AST_STM_IF d e (cut_last_neList ? res) (None ?)) + | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e)) + (λresDecl.Some ? (AST_STM_IF d e (cut_last_neList ? res) (Some ? resDecl))) ]) ] (* PREAST_NO_DECL: list preast_stm → preast_decl PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl *) -and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝ +and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝ match preast with [ PREAST_NO_DECL lPreastStm ⇒ - opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e) + opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h d e) (λh'.opt_map ?? t (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm) - (λres.Some ? (AST_NO_DECL e res)) + (λres.Some ? (AST_NO_DECL d e res)) | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒ - match checkb_not_already_def_env e decName - return λx.(checkb_not_already_def_env e decName = x) → option (ast_decl e) + match checkb_not_already_def_env d e decName + return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e) with - [ true ⇒ λp:(checkb_not_already_def_env e decName = true). - opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType)) + [ true ⇒ λp:(checkb_not_already_def_env d e decName = true). + opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName constFlag decType)) (λdecl.match optInitExpr with - [ None ⇒ Some ? (AST_DECL e constFlag decName decType - (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (None ?) decl) + [ None ⇒ Some ? (AST_DECL d e constFlag decName decType + (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl) | Some initExpr ⇒ - opt_map ?? (preast_to_ast_init initExpr e) - (λsigmaRes:(Σt:ast_type.ast_init e t).opt_map ?? (preast_to_ast_init_check e sigmaRes decType) - (λresInit.Some ? (AST_DECL e constFlag decName decType - (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p) (Some ? resInit) decl)))]) - | false ⇒ λp:(checkb_not_already_def_env e decName = false).None ? - ] (refl_eq ? (checkb_not_already_def_env e decName)) + opt_map ?? (preast_to_ast_init initExpr d e) + (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType) + (λresInit.Some ? (AST_DECL d e constFlag decName decType + (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))]) + | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ? + ] (refl_eq ? (checkb_not_already_def_env d e decName)) ]. (* @@ -561,25 +561,5 @@ and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option *) definition preast_to_ast ≝ λpreast:preast_root.match preast with - [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env) + [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl O empty_env) (λres.Some ? (AST_ROOT res)) ]. - -(* mini test -definition prova ≝ -PREAST_ROOT ( - PREAST_DECL true [ ch_Q ] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (None ?) ( - PREAST_NO_DECL [ - PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x0,x0〉) ( - PREAST_DECL false [ ch_P ] (AST_TYPE_STRUCT «(AST_TYPE_BASE AST_BASE_TYPE_WORD16)£(AST_TYPE_BASE AST_BASE_TYPE_BYTE8)») (None ?) ( - PREAST_NO_DECL [ - PREAST_STM_ASG (PREAST_VAR_STRUCT (PREAST_VAR_ID [ ch_P ]) 1) (PREAST_EXPR_ID (PREAST_VAR_ARRAY (PREAST_VAR_ID [ ch_Q ]) (PREAST_EXPR_BYTE8 〈x0,x1〉))) - ] - ) - ) - ] - ) -). - -lemma checkprova : None ? = preast_to_ast prova. -normalize; -*)