From: Claudio Sacerdoti Coen Date: Fri, 25 Jul 2008 15:09:36 +0000 (+0000) Subject: AST to ASTFE completed up to a few computational (!!!) axioms. X-Git-Tag: make_still_working~4875 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=05e6e4771934d95be8b4cffcc87eeb7b27250536;p=helm.git AST to ASTFE completed up to a few computational (!!!) axioms. --- 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 054aeedc2..528eeaa47 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -20,65 +20,125 @@ (* ********************************************************************** *) include "compiler/astfe_tree.ma". +include "compiler/sigma.ma". (* ************************ *) (* PASSO 2 : da AST a ASTFE *) (* ************************ *) (* operatore di cast *) -definition ast_to_astfe_expr_check : Πt.astfe_expr t → Πt'.option (astfe_expr t') ≝ -λt:ast_type.λast:astfe_expr t.λt':ast_type. +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 t) ast t' (eqasttype_to_eq ?? p)) + 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 : Πt.astfe_init t → Πt'.option (astfe_init t') ≝ -λt:ast_type.λast:astfe_init t.λt':ast_type. +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 t) ast t' (eqasttype_to_eq ?? p)) + 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 : Πb.Πt.astfe_var b t → Πb'.option (astfe_var b' t) ≝ -λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool. +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 b t) ast b' (eqbool_to_eq ?? p)) + 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 : Πb.Πt.astfe_var b t → Πt'.option (astfe_var b t') ≝ -λb:bool.λt:ast_type.λast:astfe_var b t.λt':ast_type. +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 b t) ast t' (eqasttype_to_eq ?? p)) + 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 : Πb.Πt.astfe_var b t → Πb'.Πt'.option (astfe_var b' t') ≝ -λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.λt':ast_type. - opt_map ?? (ast_to_astfe_var_checkb b t ast b') - (λres.opt_map ?? (ast_to_astfe_var_checkt b' t res 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 ast_to_astfe_id ≝ -λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λmap:aux_trasfMap_type.match ast with - [ AST_ID str _ ⇒ ASTFE_ID (name_to_nameId map str) b t ]. +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 ]. + +(* 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_ax: + Π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. + check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)). + +(* +axiom ax2: + Π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. + get_const_desc + (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) + = b. + +axiom ax3: + Π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. + get_type_desc + (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t. +*) + +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)))). + apply + (λ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)) ?); + apply ast_to_astfe_id_ax. +qed. (* AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) @@ -128,94 +188,94 @@ definition ast_to_astfe_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) (map:aux_trasfMap_type) on ast : option (astfe_expr 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 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 val) t - | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 val) t - | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 val) t + [ 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG bType res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT bType res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_COM bType res) t) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ bType res1 res2) t)) + 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 map) - (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map) - (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ bType res1 res2) t)) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 res) t) + 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 map) - (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 res) t) + 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 map) - (λres.ast_to_astfe_expr_check subType (ASTFE_EXPR_ID b subType res) t) + 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) ] (* AST_VAR_ID: ∀b:bool.∀t:ast_type. @@ -225,28 +285,30 @@ let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (map: 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) (map:aux_trasfMap_type) on ast : option (astfe_var b t) ≝ +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 ⇒ ast_to_astfe_var_check subB subType (ASTFE_VAR_ID subB subType (ast_to_astfe_id e subB subType subId map)) b t + [ 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 map) - (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr map) - (λresExpr.ast_to_astfe_var_check subB subType (ASTFE_VAR_ARRAY subB subType dim resVar resExpr) b t)) + 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 map) - (λres.ast_to_astfe_var_check subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT subB nelSubType field res) b t) + 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) ] (* 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) (map:aux_trasfMap_type) on ast : option astfe_base_expr ≝ +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 map) - (λres.Some ? (ASTFE_BASE_EXPR bType res)) + opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map) + (λres.Some ? (ASTFE_BASE_EXPR fe bType res)) ]. (* @@ -255,14 +317,15 @@ and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (map:aux_trasf 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 → aux_trasfMap_type → option (astfe_init t) ≝ -λe:aux_env_type.λt:ast_type.λast:ast_init e t.λmap:aux_trasfMap_type.match ast with - [ AST_INIT_VAR subB subType var ⇒ - opt_map ?? (ast_to_astfe_var e subB subType var map) - (λres.ast_to_astfe_init_check subType (ASTFE_INIT_VAR subB subType res) 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) - | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL subType args) t - ]. + | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t + ]. (* AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type. @@ -272,54 +335,96 @@ definition ast_to_astfe_init : Πe.Πt.ast_init e t → aux_trasfMap_type → op 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) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T astfe_stm aux_trasfMap_type aux_flatEnv_type) ≝ - match ast with +(* NB: il lemma dovrebbe poi prendere in input la dimostrazione che fe <= fe', cosi' ha senso *) +axiom retype_base_expr: ∀fe,fe'.astfe_base_expr fe → astfe_base_expr fe'. +axiom retype_init: ∀t,fe,fe'.astfe_init fe t → astfe_init fe' t. +axiom retype_list_decl: ∀fe,fe'.list (astfe_stm fe) → list (astfe_stm fe'). +axiom retype_neList_body: ∀fe,fe'.ne_list (Prod (astfe_base_expr fe) (astfe_body fe)) → ne_list (Prod (astfe_base_expr fe') (astfe_body fe')). + +(* 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. + +axiom how_to_build_it : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:aux_env_type → aux_env_type.∀map:aux_trasfMap_type (f e) fe.∀ll:list (astfe_stm fe). + (sigma (aux_env_type\to aux_env_type) + (\lambda f:(aux_env_type\to aux_env_type). + (sigma aux_flatEnv_type + (\lambda fe':aux_flatEnv_type. + (Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe'))))))). + +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')) ≝ + 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')) + with [ AST_STM_ASG e' subType var expr ⇒ - opt_map ?? (ast_to_astfe_var e' false subType var map) - (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr map) - (λresExpr.Some ? (tripleT ??? (ASTFE_STM_ASG subType resVar resExpr) map fe))) + λ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 ⇒ - opt_map ?? (ast_to_astfe_base_expr e' expr map) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl map fe) - (λtripleRes.match tripleRes with - [ tripleT resDecl map' fe' ⇒ - Some ? (tripleT ??? (ASTFE_STM_WHILE resExpr (ASTFE_BODY resDecl)) (rollback_map map' (build_snapshot map)) fe') - ])) + λ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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with + [ pair map' resDecl ⇒ + Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map) + (ASTFE_STM_WHILE fe' (retype_base_expr fe fe' resExpr) (ASTFE_BODY fe' resDecl))≫) + ]]])) | AST_STM_IF e' nelExprDecl optDecl ⇒ - let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) - (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝ - match nel with - [ ne_nil h ⇒ - opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE) - (λtripleRes.match tripleRes with - [ tripleT resDecl m' flatE' ⇒ - Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE') - ])) - | ne_cons h tl ⇒ - opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m) - (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE) - (λtripleRes.match tripleRes with - [ tripleT resDecl m' flatE' ⇒ - opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE') - (λtripleRes'.match tripleRes' with - [ tripleT tl' m'' flatE'' ⇒ - Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'') - ])]))] in - opt_map ?? (aux nelExprDecl map fe) - (λtRes.match tRes with - [ tripleT resNel resMap resFe ⇒ - match optDecl with - [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe) - | Some decl ⇒ - opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe) - (λtRes'.match tRes' with - [ tripleT rDecl resMap' resFe' ⇒ - Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe') - ]) - ]]) + λ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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with + [ pair m' resDecl ⇒ + Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) + « pair ?? (retype_base_expr fenv fenv' resExpr) (ASTFE_BODY fenv' resDecl) £»≫) + ]]])) + + | 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 (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type (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' ⇒ + Some ? (≪fenv'',pair ?? m'' + (« pair ?? (retype_base_expr fenv fenv'' resExpr) + (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫) + ]])]]])) + ] 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 (f' (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with + [ pair (m'':aux_trasfMap_type (f (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒ + 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'' (retype_neList_body fe' fe'' resNel) (Some ? (ASTFE_BODY fe'' resDecl)))≫) + ]]])]]]) ] (* AST_NO_DECL: ∀e:aux_env_type. @@ -327,45 +432,73 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (map:aux_trasfMap_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) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T (list astfe_stm) aux_trasfMap_type aux_flatEnv_type) ≝ - match ast with +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.(Σfe'.Prod (aux_trasfMap_type (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 (f e') fe') (list (astfe_stm fe')))) + with [ AST_NO_DECL e' lStm ⇒ - let rec aux (ll:list (ast_stm e')) (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on ll ≝ - match ll with - [ nil ⇒ Some ? (tripleT ??? [] m flatE) - | cons h tl ⇒ - opt_map ?? (ast_to_astfe_stm e' h m flatE) - (λtripleRes.match tripleRes with - [ tripleT resStm m' flatE' ⇒ - opt_map ?? (aux tl m' flatE') - (λtripleRes'.match tripleRes' with - [ tripleT tl' m'' flatE'' ⇒ - Some ? (tripleT ??? ([ resStm ]@tl') m'' flatE'') - ])])] in - aux lStm map fe + λ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 (f e') fe') (list (astfe_stm fe')))) ≝ + match ll with + [ nil ⇒ Some ? (how_to_build_it e' fenv (λx.x) (retype_map_to_id e' fenv (λx.x) m (refl_eq ??)) []) + | 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 (f e') fe') (list (astfe_stm fe')))).match sigmaRes' with + [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with + [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type (f e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with + [ pair m'' tl' ⇒ + Some ? (how_to_build_it e' fenv'' f m'' + ((retype_list_decl fenv' fenv'' [ resStm ])@tl')) + ]]])]])] in + aux lStm fe map | AST_DECL e' b name t _ optInit subDecl ⇒ - opt_map ?? (match optInit with - [ None ⇒ Some ? [] | Some init ⇒ opt_map ?? (ast_to_astfe_init e' t init map) - (λresInit.Some ? [ ASTFE_STM_INIT b t (ASTFE_ID (name_to_nameId (add_maxcur_map map name) name) b t) resInit ])]) - (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl (add_maxcur_map map name) (add_desc_flatEnv fe (name_to_nameId (add_maxcur_map map name) name) b t)) - (λtripleRes.match tripleRes with - [ tripleT tRes resMap resFe ⇒ - Some ? (tripleT ??? (hRes@tRes) resMap resFe) - ])) + λ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) + (False_rect ? daemon)) + b t) + (λresId.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) + b t resId + (retype_init t fe (add_desc_flatEnv fe (next_nameId e' fe map name) b t) 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 (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 (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with + [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with + [ pair map' tRes ⇒ + Some ? (how_to_build_it e' fe' (λx.f (add_desc_env x name b t)) map' + ((retype_list_decl (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' hRes)@tRes)) + ]]])) ]. (* AST_ROOT: ast_decl empty_env → ast_root. *) -definition ast_to_astfe ≝ +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_trasfMap empty_flatEnv 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_astfe_prog - | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x)) - ] - ]. + [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫ + | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type (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". diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma index 82666acf3..c806a04bd 100755 --- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma @@ -31,74 +31,74 @@ include "compiler/ast_tree.ma". (* **************************** *) (* id: accesso all'ambiente con stringa *) -inductive astfe_id : bool → ast_type → Type ≝ - ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type. - astfe_id b t. +inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝ + ASTFE_ID: ∀str:aux_strId_type. + (* D *) check_desc_flatEnv e str → astfe_id e (get_const_desc (get_desc_flatEnv e str)) (get_type_desc (get_desc_flatEnv e str)). (* -------------------------- *) (* espressioni *) -inductive astfe_expr : ast_type → Type ≝ - ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) -| ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) -| ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝ + ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) | ASTFE_EXPR_NEG: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_NOT: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_COM: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_ADD: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_SUB: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_MUL: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_DIV: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_SHR: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_SHL: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) | ASTFE_EXPR_GT : ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | ASTFE_EXPR_GTE: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | ASTFE_EXPR_LT : ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | ASTFE_EXPR_LTE: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | ASTFE_EXPR_EQ : ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | ASTFE_EXPR_NEQ: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) -| ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) -| ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) -| ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) -| ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) -| ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) -| ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) | ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type. - astfe_var b t → astfe_expr t + astfe_var e b t → astfe_expr e t (* variabile: modificatori di array/struct dell'id *) with astfe_var : bool → ast_type → Type ≝ ASTFE_VAR_ID: ∀b:bool.∀t:ast_type. - astfe_id b t → astfe_var b t + astfe_id e b t → astfe_var e b t | ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. - astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t + astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t | ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. - astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n) + astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n) (* espressioni generalizzate: anche non uniformi per tipo *) with astfe_base_expr : Type ≝ ASTFE_BASE_EXPR: ∀t:ast_base_type. - astfe_expr (AST_TYPE_BASE t) → astfe_base_expr. + astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e. (* -------------------------- *) @@ -107,34 +107,34 @@ with astfe_base_expr : Type ≝ 1) var1 = var2 2) var = ... valori ... *) -inductive astfe_init : ast_type → Type ≝ +inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝ ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type. - astfe_var b t → astfe_init t + astfe_var e b t → astfe_init e t | ASTFE_INIT_VAL: ∀t:ast_type. - aux_ast_init_type t → astfe_init t. + aux_ast_init_type t → astfe_init e t. (* -------------------------- *) (* statement: assegnamento/while/if else if else + conversione di dichiarazione *) -inductive astfe_stm : Type ≝ +inductive astfe_stm (e:aux_flatEnv_type) : Type ≝ ASTFE_STM_ASG: ∀t:ast_type. - astfe_var false t → astfe_expr t → astfe_stm + astfe_var e false t → astfe_expr e t → astfe_stm e | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. - astfe_id b t → astfe_init t → astfe_stm -| ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm -| ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm + 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 (* dichiarazioni *) with astfe_body : Type ≝ - ASTFE_BODY: list astfe_stm → astfe_body. + ASTFE_BODY: list (astfe_stm e) → astfe_body e. (* -------------------------- *) (* programma *) -inductive astfe_root : Type ≝ - ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root. +inductive astfe_root (e:aux_flatEnv_type) : Type ≝ + ASTFE_ROOT: astfe_body e → astfe_root e. (* -------------------------- *) (* programma vuoto *) -definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)). +definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (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 4d3a092c1..bfa77213a 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -41,100 +41,151 @@ definition get_desc_flatVar ≝ λv:flatVar_elem.match v with [ VAR_FLAT_ELEM _ (* ambiente vuoto *) definition empty_flatEnv ≝ nil flatVar_elem. +(* 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 strCmp_strId str (get_nameId_flatVar h) with + [ true ⇒ Some ? (get_desc_flatVar h) + | false ⇒ get_desc_flatEnv_aux tl str ]]. + +definition get_desc_flatEnv ≝ +λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux e 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 checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux e str with [ None ⇒ false | Some _ ⇒ true ]. + +lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str = true → check_desc_flatEnv e str. + unfold checkb_desc_flatEnv; + unfold check_desc_flatEnv; + intros; + letin K ≝ (get_desc_flatEnv_aux e str); + elim K; + [ normalize; autobatch | + normalize; autobatch ] +qed. + +(* aggiungi descrittore ad ambiente: in testa *) +definition add_desc_flatEnv ≝ +λe:aux_flatEnv_type.λstr:aux_strId_type.λb:bool.λt:ast_type. + (VAR_FLAT_ELEM str (DESC_ELEM b t))::e. + (* STRUTTURA MAPPA TRASFORMAZIONE *) -(* elemento: nome + max + cur *) -inductive maxCur_elem : Type ≝ -MAX_CUR_ELEM: aux_str_type → nat → nat → maxCur_elem. +(* 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. (* tipo pubblico *) -definition aux_trasfMap_type ≝ list maxCur_elem. +definition aux_trasfMap_type ≝ λe,fe.list (maxCur_elem e fe). (* getter *) -definition get_name_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM n _ _ ⇒ n ]. -definition get_max_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ m _ ⇒ m ]. -definition get_cur_maxCur ≝ λmc:maxCur_elem.match mc with [ MAX_CUR_ELEM _ _ c ⇒ c ]. +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 ]. (* mappa di trasformazione vuota *) -definition empty_trasfMap ≝ nil maxCur_elem. +definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe). (* INTERAZIONE AMBIENTE FLAT / MAPPA TRASFORMAZIONE *) (* recupera descrittore da mappa trasformazione : dummy se non esiste (impossibile) *) -let rec get_maxcur_from_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (dummy:option maxCur_elem) on map ≝ +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 ≝ match map with - [ nil ⇒ dummy - | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with - [ true ⇒ Some ? h | false ⇒ get_maxcur_from_map_aux tl str dummy ]]. - -definition get_maxcur_from_map ≝ -λmap:aux_trasfMap_type.λstr:aux_str_type. - match get_maxcur_from_map_aux map str (None ?) with - [ None ⇒ MAX_CUR_ELEM str 0 0 | Some x ⇒ x ]. - -(* aggiungi/aggiorna descrittore mappa trasformazione *) -let rec add_maxcur_map_aux (map:aux_trasfMap_type) (str:aux_str_type) (flag:bool) on map ≝ - match map with - [ nil ⇒ match flag with - [ true ⇒ [] - | false ⇒ [MAX_CUR_ELEM str 0 0] - ] - | cons h tl ⇒ match strCmp_str str (get_name_maxCur h) with - [ true ⇒ [MAX_CUR_ELEM str (S (get_max_maxCur h)) (S (get_max_maxCur h))]@(add_maxcur_map_aux tl str true) - | false ⇒ [h]@(add_maxcur_map_aux tl str flag) - ] + [ nil ⇒ None ? + | cons h tl ⇒ match strCmp_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)) ]. -definition add_maxcur_map ≝ -λmap:aux_trasfMap_type.λstr:aux_str_type.add_maxcur_map_aux map str false. - (* nome -> nome + id *) definition name_to_nameId ≝ -λmap:aux_trasfMap_type.λstr:aux_str_type. - STR_ID str (get_cur_maxCur (get_maxcur_from_map map str)). - -(* recupera descrittore da ambiente : dummy se non esiste (impossibile) *) -let rec get_desc_from_flatEnv_aux (e:aux_flatEnv_type) (str:aux_strId_type) (dummy:option desc_elem) on e ≝ -match e with - [ nil ⇒ dummy - | cons h tl ⇒ match strCmp_strId str (get_nameId_flatVar h) with - [ true ⇒ Some ? (get_desc_flatVar h) - | false ⇒ get_desc_from_flatEnv_aux tl str dummy ]]. - -definition get_desc_from_flatEnv ≝ -λe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_from_flatEnv_aux e str (None ?) with - [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. - -(* aggiungi descrittore ad ambiente *) -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) ]. - -(* snapshot della mappa trasformazione *) -let rec build_snapshot (map:aux_trasfMap_type) on map ≝ - match map with - [ nil ⇒ [] - | cons h tl ⇒ [ STR_ID (get_name_maxCur h) (get_cur_maxCur h) ]@(build_snapshot tl) +λ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) ]. -(* uscita da un blocco, rollback di cur in mappa di trasformazione *) -let rec find_in_snapshot (snap:list aux_strId_type) (str:aux_str_type) on snap ≝ - match snap with - [ nil ⇒ None ? - | cons h tl ⇒ match strCmp_str str (get_name_strId h) with - [ true ⇒ Some ? (get_id_strId h) - | false ⇒ find_in_snapshot tl str - ] - ]. +(* 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)) → +(strCmp_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)) → +(strCmp_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))). -let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map ≝ +(* 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 O O (False_rect ? daemon) ] + ] + | cons h tl ⇒ match h with + [ MAX_CUR_ELEM str' cur' max' dim' ⇒ + match strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with + [ true ⇒ λp:(strCmp_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:(strCmp_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 ? (strCmp_str str' str)) + ] + ]. + +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. + +(* NB: leave ... enter e' equivalente a e originale *) +axiom retype_enter_leave_to_e: ∀e,fe,f. aux_trasfMap_type (leave_env (f (enter_env e))) fe → aux_trasfMap_type e fe. +(* NB: enter non cambia fe *) +axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) fe. +(* NB: leave non cambia fe *) +axiom retype_e_to_leave: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) fe. + +let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type → aux_env_type) (map:aux_trasfMap_type (leave_env (f (enter_env e))) fe') + (snap:aux_trasfMap_type e fe) on map : aux_trasfMap_type e fe' ≝ match map with - [ nil ⇒ empty_trasfMap - | cons h tl ⇒ match find_in_snapshot snap (get_name_maxCur h) with - [ None ⇒ [h] - | Some newCur ⇒ [ MAX_CUR_ELEM (get_name_maxCur h) (get_max_maxCur h) newCur ] - ]@(rollback_map tl snap) + [ 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' f [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' f tl snap ]. (* sequenza di utilizzo: @@ -166,48 +217,48 @@ let rec rollback_map (map:aux_trasfMap_type) (snap:list aux_strId_type) on map | ... *) -(* mini test +(* mini test definition pippo ≝ [ ch_P ]. definition pluto ≝ [ ch_Q ]. -definition pippodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8). -definition pippodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_BYTE8). -definition pippodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2). -definition plutodesc1 ≝ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_WORD16). -definition plutodesc2 ≝ DESC_ELEM false (AST_TYPE_BASE AST_BASE_TYPE_WORD16). -definition plutodesc3 ≝ DESC_ELEM false (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_WORD16) 2). - -definition map1 ≝ add_maxcur_map empty_trasfMap pippo. -definition env1 ≝ add_desc_flatEnv empty_flatEnv (name_to_nameId map1 pippo) pippodesc1. -definition map2 ≝ add_maxcur_map map1 pluto. -definition env2 ≝ add_desc_flatEnv env1 (name_to_nameId map2 pluto) plutodesc1. - -definition snap1 ≝ build_snapshot map2. - -definition map3 ≝ add_maxcur_map map2 pippo. -definition env3 ≝ add_desc_flatEnv env2 (name_to_nameId map3 pippo) pippodesc2. -definition map4 ≝ add_maxcur_map map3 pluto. -definition env4 ≝ add_desc_flatEnv env3 (name_to_nameId map4 pluto) plutodesc2. - -definition snap2 ≝ build_snapshot map4. - -definition map5 ≝ add_maxcur_map map4 pippo. -definition env5 ≝ add_desc_flatEnv env4 (name_to_nameId map5 pippo) pippodesc3. -definition map6 ≝ add_maxcur_map map5 pluto. -definition env6 ≝ add_desc_flatEnv env5 (name_to_nameId map6 pluto) plutodesc3. - -definition map7 ≝ rollback_map map6 snap2. - -definition map8 ≝ rollback_map map7 snap1. - -lemma checkenv : None ? = Some ? env6. -normalize; elim daemon. -qed. - -lemma checkmap : None ? = Some ? map8. -normalize; elim daemon. -qed. - -lemma checksnap : None ? = Some ? snap2. -normalize; elim daemon. -qed. +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 (λx.add_desc_env (add_desc_env x pippo false pippodesc3) pluto false plutodesc3) map6' map4. + +definition map7' ≝ retype_e_to_leave env4 fenv6 map7. + +definition map8 ≝ rollback_map env2 fenv2 fenv6 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2. *) diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma index 363716ae8..326ed1d20 100755 --- a/helm/software/matita/contribs/assembly/compiler/environment.ma +++ b/helm/software/matita/contribs/assembly/compiler/environment.ma @@ -48,11 +48,35 @@ definition get_desc_var ≝ λv:var_elem.match v with [ VAR_ELEM _ d ⇒ d ]. (* ambiente vuoto *) definition empty_env ≝ ne_nil ? (nil var_elem ). +(* confronto *) +let rec eq_aux_env_type_aux (subE,subE':list var_elem) on subE ≝ + match subE with + [ nil ⇒ match subE' with + [ nil ⇒ true | cons _ _ ⇒ false ] + | cons h tl ⇒ match subE' with + [ nil ⇒ false | cons h' tl' ⇒ (strCmp_str (get_name_var h) (get_name_var h'))⊗ + (eq_bool (get_const_desc (get_desc_var h)) (get_const_desc (get_desc_var h')))⊗ + (eq_ast_type (get_type_desc (get_desc_var h)) (get_type_desc (get_desc_var h')))⊗ + (eq_aux_env_type_aux tl tl') ] + ]. + +axiom eqbauxenvtypeaux_to_eq : ∀e,e'.eq_aux_env_type_aux e e' = true → e = e'. + +let rec eq_aux_env_type (e,e':aux_env_type) on e ≝ + match e with + [ ne_nil h ⇒ match e' with + [ ne_nil h' ⇒ eq_aux_env_type_aux h h' | ne_cons _ _ ⇒ false ] + | ne_cons h tl ⇒ match e' with + [ ne_nil h' ⇒ false | ne_cons h' tl' ⇒ (eq_aux_env_type_aux h h')⊗(eq_aux_env_type tl tl') ] + ]. + +axiom eqbauxenvtype_to_eq : ∀e,e':aux_env_type.eq_aux_env_type e e' = true → e = e'. + (* setter *) -definition enter_env ≝ λe:aux_env_type.e&empty_env. -definition leave_env ≝ λe:aux_env_type.cut_last_neList ? e. +definition enter_env ≝ λe:aux_env_type.empty_env&e. +definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e. -(* recupera descrittore da ambiente *) +(* 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 ≝ match env with [ nil ⇒ None ? @@ -60,55 +84,55 @@ match env with [ true ⇒ Some ? (get_desc_var h) | false ⇒ get_desc_from_lev_env t str ]]. -(* recupera descrittore da ambiente globale *) -let rec get_desc_env_aux (env:aux_env_type) (res:option desc_elem) (str:aux_str_type) on env ≝ +(* recupera descrittore da ambiente globale: il primo trovato *) +let rec get_desc_env_aux (env:aux_env_type) (str:aux_str_type) on env ≝ match env with - [ ne_nil h ⇒ match get_desc_from_lev_env h str with - [ None ⇒ res | Some res' ⇒ Some ? res' ] - | ne_cons h t ⇒ get_desc_env_aux t (match get_desc_from_lev_env h str with - [ None ⇒ res | Some res' ⇒ Some ? res' ]) str ]. + [ 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' ] + ]. definition check_desc_env ≝ λe:aux_env_type.λstr:aux_str_type. - match get_desc_env_aux e (None ?) str with [ None ⇒ False | Some _ ⇒ True ]. + match get_desc_env_aux 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 (None ?) str with [ None ⇒ false | Some _ ⇒ true ]. + match get_desc_env_aux e str with [ None ⇒ false | Some _ ⇒ true ]. lemma checkbdescenv_to_checkdescenv : ∀e,str.checkb_desc_env e str = true → check_desc_env e str. unfold checkb_desc_env; unfold check_desc_env; intros; - letin K ≝ (get_desc_env_aux e (None ?) str); + letin K ≝ (get_desc_env_aux 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 (None ?) str with + match get_desc_env_aux 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_last_neList ? e) str with [ None ⇒ True | Some _ ⇒ False ]. + match get_desc_from_lev_env (get_first_neList ? 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_last_neList ? e) str with [ None ⇒ true | Some _ ⇒ false ]. + match get_desc_from_lev_env (get_first_neList ? 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. unfold checkb_not_already_def_env; unfold check_not_already_def_env; intros; - letin K ≝ (get_desc_from_lev_env (get_last_neList ? e) str); + letin K ≝ (get_desc_from_lev_env (get_first_neList ? e) str); elim K; [ normalize; autobatch | normalize; autobatch ] qed. -(* aggiungi descrittore ad ambiente globale *) +(* 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. -let var ≝ VAR_ELEM str (DESC_ELEM c desc) in +(*let var ≝ VAR_ELEM str (DESC_ELEM c desc) in*) match e with - [ ne_nil h ⇒ ne_nil ? (var::h) - | ne_cons _ _ ⇒ (cut_last_neList ? e)&«(var::(get_last_neList ? e)) £ » + [ 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 ]. diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma index 4352dc426..aef219e06 100755 --- a/helm/software/matita/contribs/assembly/compiler/utility.ma +++ b/helm/software/matita/contribs/assembly/compiler/utility.ma @@ -40,7 +40,7 @@ notation "hvbox(hd break §§ tl)" right associative with precedence 46 for @{'ne_cons $hd $tl}. -notation "« y £ break list0 x sep ; »" +notation "« y break £ list0 x sep ; break »" non associative with precedence 90 for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}. @@ -134,6 +134,28 @@ definition cut_last_neList ≝ [ ne_nil h ⇒ ne_nil T h | ne_cons _ t ⇒ reverse_neList T t ]. +(* getFirst *) +definition get_first_list ≝ +λT:Type.λl:list T.match l with + [ nil ⇒ None ? + | cons h _ ⇒ Some ? h ]. + +definition get_first_neList ≝ +λT:Type.λl:ne_list T.match l with + [ ne_nil h ⇒ h + | ne_cons h _ ⇒ h ]. + +(* cutFirst *) +definition cut_first_list ≝ +λT:Type.λl:list T.match l with + [ nil ⇒ nil T + | cons _ t ⇒ t ]. + +definition cut_first_neList ≝ +λT:Type.λl:ne_list T.match l with + [ ne_nil h ⇒ ne_nil T h + | ne_cons _ t ⇒ t ]. + (* apply f *) let rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝ match l with diff --git a/helm/software/matita/contribs/assembly/depends b/helm/software/matita/contribs/assembly/depends index 9e0caab22..43de98df7 100644 --- a/helm/software/matita/contribs/assembly/depends +++ b/helm/software/matita/contribs/assembly/depends @@ -31,7 +31,7 @@ freescale/multivm.ma freescale/load_write.ma compiler/environment.ma compiler/ast_type.ma freescale/word32.ma string/string.ma freescale/load_write.ma freescale/model.ma compiler/sigma.ma -compiler/ast_to_astfe.ma compiler/astfe_tree.ma +compiler/ast_to_astfe.ma compiler/astfe_tree.ma compiler/sigma.ma compiler/utility.ma freescale/extra.ma compiler/ast_type.ma compiler/utility.ma freescale/word32.ma compiler/preast_to_ast.ma compiler/ast_tree.ma compiler/preast_tree.ma compiler/sigma.ma diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma index 4c4862928..f60b8a804 100755 --- a/helm/software/matita/contribs/assembly/string/string.ma +++ b/helm/software/matita/contribs/assembly/string/string.ma @@ -48,6 +48,8 @@ let rec strCmp_str (str,str':aux_str_type) ≝ [ true ⇒ strCmp_str t t' | false ⇒ false ] ]]. +axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'. + (* strcat *) definition strCat_str ≝ λstr,str':aux_str_type.str@str'.