From 55e5bef77f163b29feeb9ad4e83376c5aa301297 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 1 Oct 2008 12:41:32 +0000 Subject: [PATCH] - setters for data structures now support "commuting conversion"-like operations w.r.t. getters - several axioms have now been proved - new file env_to_flatenv1 showing an alternative representation of the environment --- .../assembly/compiler/ast_to_astfe.ma | 429 +++++++++++---- .../contribs/assembly/compiler/ast_type.ma | 222 +++++++- .../assembly/compiler/env_to_flatenv.ma | 239 +++++++- .../assembly/compiler/env_to_flatenv1.ma | 236 ++++++++ .../contribs/assembly/compiler/environment.ma | 80 ++- .../assembly/compiler/preast_to_ast.ma | 10 +- .../contribs/assembly/compiler/utility.ma | 32 +- .../contribs/assembly/freescale/extra.ma | 34 ++ .../assembly/freescale/medium_tests.ma | 3 +- .../assembly/freescale/medium_tests_lemmas.ma | 12 +- .../contribs/assembly/freescale/status.ma | 508 ++++++++++++++---- .../contribs/assembly/string/ascii_min.ma | 94 ++++ .../matita/contribs/assembly/string/string.ma | 74 ++- 13 files changed, 1675 insertions(+), 298 deletions(-) create mode 100755 helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma 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 528eeaa47..d6eadfdb8 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -107,38 +107,31 @@ 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: +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. + (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)). (* AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) @@ -311,6 +304,117 @@ and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (fe:aux_flatEn (λres.Some ? (ASTFE_BASE_EXPR fe bType res)) ]. +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) + ] +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 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)) + ]. + (* AST_INIT_VAR: ∀b:bool.∀t:ast_type. ast_var e b t → ast_init e t @@ -327,19 +431,82 @@ definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e | 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) + + | ASTFE_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. - 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 + ASTFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → astfe_stm e + ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → astfe_stm e + ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e + ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e +*) +let rec retype_stm (fe:aux_flatEnv_type) (ast:astfe_stm fe) (fe':aux_flatEnv_type) (dim:(le_flatEnv fe fe' = true)) on ast : option (astfe_stm fe') ≝ + 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_BODY: list (astfe_stm e) → astfe_body e *) -(* 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')). +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') ≝ + 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)) + ]. + +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). @@ -348,13 +515,14 @@ lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_ 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'))))))). - +(* + 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 +*) 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 @@ -370,12 +538,19 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) λ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 + (λ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 ⇒ - 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))≫) + 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 ⇒ @@ -386,28 +561,50 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) [ 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 + (λ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 ⇒ - 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) £»≫) + 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 (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 + (λ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 ?? (retype_base_expr fenv fenv'' resExpr) - (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫) + («£(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) @@ -417,13 +614,20 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) [ 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)))≫) + (λ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'')) ]]])]]]) ] (* @@ -433,32 +637,45 @@ let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_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.(Σfe'.Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe')))) ≝ + : Π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 (f e') fe') (list (astfe_stm fe')))) + 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 (f e') fe') (list (astfe_stm fe')))) ≝ + : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv 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 ??)) []) + [ 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 (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 + (λ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' ⇒ - Some ? (how_to_build_it e' fenv'' f m'' - ((retype_list_decl fenv' fenv'' [ resStm ])@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 _ optInit subDecl ⇒ + | AST_DECL e' b name t dim optInit subDecl ⇒ λmap:aux_trasfMap_type e' fe. opt_map ?? (match optInit with [ None ⇒ Some ? [] @@ -467,22 +684,31 @@ and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on (λ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)) + (ast_to_astfe_dec_aux e' name b t fe map dim)) 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) - ]))) + (λ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 (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)) + (λ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')) ]]])) ]. @@ -494,17 +720,16 @@ definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝ [ 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 (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 + | 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".*) +(* 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; @@ -521,20 +746,15 @@ include "compiler/preast_to_ast.ma".*) 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,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) ( + 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,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 [])) - ) - £ (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 [])) ) @@ -545,6 +765,10 @@ PREAST_ROOT ( 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 []))) ] @@ -552,7 +776,4 @@ PREAST_ROOT ( ) ) ). - -lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?. -normalize; *) diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma index b1ad547e9..f1d78197c 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma @@ -57,6 +57,30 @@ lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = tru destruct H. qed. +lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true. + do 2 intro; + elim t1 0; + elim t2 0; + normalize; + intro; + try destruct H; + reflexivity. +qed. + +definition eq_ast_type_aux ≝ +λT:Type.λf:T → T → bool. + let rec aux (nl1,nl2:ne_list T) on nl1 ≝ + match nl1 with + [ ne_nil h ⇒ match nl2 with + [ ne_nil h' ⇒ f h h' + | ne_cons h' _ ⇒ false + ] + | ne_cons h t ⇒ match nl2 with + [ ne_nil h' ⇒ false + | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t') + ] + ] in aux. + let rec eq_ast_type (t1,t2:ast_type) on t1 ≝ match t1 with [ AST_TYPE_BASE bType1 ⇒ match t2 with @@ -64,31 +88,189 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝ | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ] | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with - [ AST_TYPE_STRUCT nelSubType2 ⇒ - fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with - [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with - [ None ⇒ pair ?? false (S (snd ?? t)) - | Some cfr ⇒ match eq_ast_type h cfr with - [ true ⇒ pair ?? true (S (snd ?? t)) - | false ⇒ pair ?? false (S (snd ?? t)) ]] - | false ⇒ t]) (pair ?? true O) nelSubType1) + [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2 | _ ⇒ false ] ]. +lemma eq_ast_type_elim : + ∀P:ast_type → Prop. + (∀x.P (AST_TYPE_BASE x)) → + (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) → + (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) → + (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) → + (∀t.(P t)). + intros; + apply + (let rec aux t ≝ + match t + return λt.P t + with + [ AST_TYPE_BASE b ⇒ H b + | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t) + | AST_TYPE_STRUCT l ⇒ + let rec aux_l (l:ne_list ast_type ) ≝ + match l + return λl.P (AST_TYPE_STRUCT l) + with + [ ne_nil t => H2 t (aux t) + | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl) + ] in aux_l l + ] in aux t); +qed. + lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2). intro; - elim t1 0; [1,3:intros 2 | intros 4] elim t2; - [ 2,5,7,9: normalize in H1; destruct H1; - | 3,4: normalize in H; destruct H; - | 1: simplify in H; - apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H)) - | 8: simplify in H2; - lapply (andb_true_true ? ? H2); - lapply (andb_true_true_r ? ? H2); clear H2; - rewrite > (H ? Hletin); - rewrite > (eqb_true_to_eq ?? Hletin1); - reflexivity - | 6: elim daemon; + elim t1 using eq_ast_type_elim 0; + [ 1: intros 2; + elim t2 using eq_ast_type_elim 0; + [ 1: intros; + simplify in H; + rewrite > (eqastbasetype_to_eq ?? H); + reflexivity + | 2: simplify; + intros; + destruct H1 + | 3: simplify; + intros; + destruct H1 + | 4: simplify; + intros; + destruct H2 + ] + | 2: intros 4; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H1 + | 2: simplify; + intros; + lapply (andb_true_true ?? H2) as H3; + lapply (andb_true_true_r ?? H2) as H4; + rewrite > (H ? H3); + rewrite > (eqb_true_to_eq ?? H4); + reflexivity + | 3: simplify; + intros; + destruct H2 + | 4: simplify; + intros; + destruct H3 + ] + | 3: intros 3; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H1 + | 2: simplify; + intros; + destruct H2 + | 3: intros; + simplify in H2; + rewrite > (H x1); + [ reflexivity + | apply H2 + ] + | 4: intros; + simplify in H3; + destruct H3 + ] + | 4: intros 5; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H2 + | 2: simplify; + intros; + destruct H3 + | 3: simplify; + intros; + destruct H3 + | 4: intros; + simplify in H4; + lapply (andb_true_true ?? H4) as H5; + lapply (andb_true_true_r ?? H4) as H6; + rewrite > (H ? H5); + lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K; + destruct (K ?); + [ apply H6 + | reflexivity + ] + ] + ]. +qed. + +lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true. + intro; + elim t1 using eq_ast_type_elim 0; + [ 1: intros 2; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H; + apply (eq_to_eqastbasetype x x (refl_eq ??)) + | 2: simplify; + intros; + destruct H1 + | 3: simplify; + intros; + destruct H1 + | 4: simplify; + intros; + destruct H2 + ] + | 2: intros 4; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H1 + | 2: intros; + simplify; + destruct H2; + rewrite > (H t (refl_eq ??)); + rewrite > (eq_to_eqb_true n n (refl_eq ??)); + reflexivity + | 3: simplify; + intros; + destruct H2 + | 4: simplify; + intros; + destruct H3 + ] + | 3: intros 3; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H1 + | 2: simplify; + intros; + destruct H2 + | 3: intros; + simplify; + destruct H2; + rewrite > (H x (refl_eq ??)); + reflexivity + | 4: simplify; + intros; + destruct H3 + ] + | 4: intros 5; + elim t2 using eq_ast_type_elim 0; + [ 1: simplify; + intros; + destruct H2 + | 2: simplify; + intros; + destruct H3 + | 3: simplify; + intros; + destruct H3 + | 4: intros; + simplify; + destruct H4; + rewrite > (H x (refl_eq ??)); + rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??)); + reflexivity + ] ]. qed. 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 bfa77213a..865f9e5c9 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -45,7 +45,7 @@ definition empty_flatEnv ≝ nil flatVar_elem. 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 + | 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 ]]. @@ -70,10 +70,98 @@ lemma checkbdescflatenv_to_checkdescflatenv : ∀e,str.checkb_desc_flatEnv e str normalize; autobatch ] qed. -(* aggiungi descrittore ad ambiente: in testa *) +(* aggiungi descrittore ad ambiente: in coda *) 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. + e@[VAR_FLAT_ELEM str (DESC_ELEM b t)]. + +(* controllo 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 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 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_nameId_flatVar a)); + [ simplify; intro; apply H3 + | 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)]); + 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 + ]. +qed. (* STRUTTURA MAPPA TRASFORMAZIONE *) @@ -98,7 +186,7 @@ definition empty_trasfMap ≝ λe,fe.nil (maxCur_elem e fe). 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 ⇒ None ? - | cons h tl ⇒ match strCmp_str str (get_name_maxCur e fe h) with + | 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 *) @@ -121,7 +209,7 @@ definition name_to_nameId ≝ 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) → +(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)). @@ -130,11 +218,24 @@ axiom add_maxcur_map_aux_false : ∀e,fe,str,cur,str',b',desc',map. 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) → +(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 @@ -145,22 +246,22 @@ match map 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) ] + 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 strCmp_str str' str return λx.(strCmp_str str' str = x) → ? with - [ true ⇒ λp:(strCmp_str str' str = true). + 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:(strCmp_str str' str = false). + | 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 ? (strCmp_str str' str)) + ] (refl_eq ? (eqStr_str str' str)) ] ]. @@ -168,24 +269,122 @@ 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. +(* 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). + +let rec build_trasfEnv (trasf:aux_trasfEnv_type) on trasf : aux_env_type → aux_env_type ≝ + match trasf with + [ nil ⇒ (λx.x) + | cons h tl ⇒ (λx.(build_trasfEnv tl) (add_desc_env 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; ] +qed. + +lemma eq_enter_leave : ∀e,trsf.leave_env (build_trasfEnv trsf (enter_env e)) = e. + intros; + change in ⊢ (? ? (? (? ? %)) ?) with ([]§§e); + cases (build_trasfEnv_exists_aux e trsf []); + rewrite > H; + reflexivity. +qed. + (* 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. +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); + intros; + apply H; + apply H1. +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 ⊢ ((?→? ? (? % ?) ?)→?); + intros; + apply H; + apply H1. +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 *) -axiom retype_e_to_enter: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (enter_env e) 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 + ]. +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: ∀e,fe. aux_trasfMap_type e fe → aux_trasfMap_type (leave_env e) 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) + ]]. -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') +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' f [h] + [ 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' f tl snap + ] @ rollback_map e fe fe' trsf tl snap ]. (* sequenza di utilizzo: @@ -217,7 +416,7 @@ let rec rollback_map (e:aux_env_type) (fe,fe':aux_flatEnv_type) (f:aux_env_type | ... *) -(* mini test +(* mini test definition pippo ≝ [ ch_P ]. definition pluto ≝ [ ch_Q ]. definition pippodesc1 ≝ (AST_TYPE_BASE AST_BASE_TYPE_BYTE8). @@ -256,9 +455,9 @@ definition fenv6 ≝ add_desc_flatEnv fenv5 (next_nameId ?? map5 pluto) false pl 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 ≝ 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 (λx.add_desc_env (add_desc_env x pippo true pippodesc2) pluto true plutodesc2) map7' map2. +definition map8 ≝ rollback_map env2 fenv2 fenv6 [ tripleT ??? pluto true plutodesc2 ; tripleT ??? pippo true pippodesc2 ] map7' map2. *) diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma new file mode 100755 index 000000000..0b3cde19e --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma @@ -0,0 +1,236 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* ********************** *) + +(* elemento: name + nel curId + nel desc *) +inductive var_flatElem : Type ≝ +VAR_FLAT_ELEM: aux_str_type → ne_list (option nat) → ne_list desc_elem → var_flatElem. + +definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ _ ⇒ n ]. +definition get_cur_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ c _ ⇒ c ]. +definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ _ d ⇒ d ]. + +(* ambiente globale: descrittori *) +definition aux_flatEnv_type ≝ Prod nat (list var_flatElem). + +(* ambiente vuoto *) +definition empty_flatEnv ≝ pair ?? O (nil var_flatElem). + +definition get_depth_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair d _ ⇒ d ]. +definition get_subEnv_flatEnv ≝ λenv:aux_flatEnv_type.match env with [ pair _ s ⇒ s ]. + +(* enter: propaga in testa la vecchia testa (il "cur" precedente) *) +let rec enter_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝ + match subEnv with + [ nil ⇒ [] + | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h) + ((get_first_neList ? (get_cur_flatVar h))§§(get_cur_flatVar h)) + (get_desc_flatVar h))::(enter_flatEnv_aux t) + ]. + +definition enter_flatEnv ≝ +λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)). + +(* leave: elimina la testa (il "cur" corrente) *) +let rec leave_flatEnv_aux (subEnv:list var_flatElem) on subEnv ≝ + match subEnv with + [ nil ⇒ [] + | cons h t ⇒ (VAR_FLAT_ELEM (get_name_flatVar h) + (cut_first_neList ? (get_cur_flatVar h)) + (get_desc_flatVar h))::(leave_flatEnv_aux t) + ]. + +definition leave_flatEnv ≝ +λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)). + +(* get_id *) +let rec get_id_flatEnv_aux (subEnv:list var_flatElem) (name:aux_str_type) on subEnv ≝ + match subEnv with + [ nil ⇒ None ? + | cons h t ⇒ + match (match eqStr_str name (get_name_flatVar h) with + [ true ⇒ get_first_neList ? (get_cur_flatVar h) + | false ⇒ None ? + ]) with + [ None ⇒ get_id_flatEnv_aux t name + | Some x ⇒ Some ? x + ] + ]. + +definition get_id_flatEnv ≝ +λe:aux_flatEnv_type.λstr:aux_str_type. + match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with + [ None ⇒ O | Some x ⇒ x ]. + +(* get_desc *) +let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝ + match subEnv with + [ nil ⇒ None ? + | cons h t ⇒ + match (match (eqStr_str (get_name_strId name) (get_name_flatVar h))⊗ + (leb (S (get_id_strId name)) (len_neList ? (get_desc_flatVar h))) with + [ true ⇒ nth_neList ? (get_desc_flatVar h) (get_id_strId name) + | false ⇒ None ? + ]) with + [ None ⇒ get_desc_flatEnv_aux t name + | Some x ⇒ Some ? x + ] + ]. + +definition get_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with + [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. + +(* check_id *) +definition check_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type. + match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ]. + +definition checkb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type. + match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ false | Some _ ⇒ true ]. + +lemma checkbidflatenv_to_checkidflatenv : ∀e,str.checkb_id_flatEnv e str = true → check_id_flatEnv e str. + unfold checkb_id_flatEnv; + unfold check_id_flatEnv; + intros; + letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str); + elim K; + [ normalize; autobatch | + normalize; autobatch ] +qed. + +definition checknot_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type. + match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ]. + +definition checknotb_id_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_str_type. + match get_id_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ]. + +lemma checknotbidflatenv_to_checknotidflatenv : ∀e,str.checknotb_id_flatEnv e str = true → checknot_id_flatEnv e str. + unfold checknotb_id_flatEnv; + unfold checknot_id_flatEnv; + intros; + letin K ≝ (get_id_flatEnv_aux (get_subEnv_flatEnv e) str); + elim K; + [ normalize; autobatch | + normalize; autobatch ] +qed. + +(* check_desc *) +definition check_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ False | Some _ ⇒ True ]. + +definition checkb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux (get_subEnv_flatEnv 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 (get_subEnv_flatEnv e) str); + elim K; + [ normalize; autobatch | + normalize; autobatch ] +qed. + +definition checknot_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ True | Some _ ⇒ False ]. + +definition checknotb_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with [ None ⇒ true | Some _ ⇒ false ]. + +lemma checknotbdescflatenv_to_checknotdescflatenv : ∀e,str.checknotb_desc_flatEnv e str = true → checknot_desc_flatEnv e str. + unfold checknotb_desc_flatEnv; + unfold checknot_desc_flatEnv; + intros; + letin K ≝ (get_desc_flatEnv_aux (get_subEnv_flatEnv e) str); + elim K; + [ normalize; autobatch | + normalize; autobatch ] +qed. + +(* aggiungi descrittore : in testa al primo ambiente *) +let rec previous_cur_from_depth (depth:nat) on depth ≝ + match depth with + [ O ⇒ «£(Some ? O)» + | S n ⇒ (previous_cur_from_depth n)&«£(None ?)» + ]. + +let rec add_desc_flatEnv_aux (subEnv:list var_flatElem) (str:aux_str_type) (c:bool) (desc:ast_type) (depth:nat) (flag:bool) on subEnv ≝ + match subEnv with + [ nil ⇒ match flag with + [ true ⇒ [] + | false ⇒ [ VAR_FLAT_ELEM str (previous_cur_from_depth depth) «£(DESC_ELEM c desc)» ] + ] + | cons h t ⇒ (match eqStr_str str (get_name_flatVar h) with + [ true ⇒ VAR_FLAT_ELEM (get_name_flatVar h) + («£(Some ? (len_neList ? (get_desc_flatVar h)))»&(cut_first_neList ? (get_cur_flatVar h))) + ((get_desc_flatVar h)&«£(DESC_ELEM c desc)») + | false ⇒ h + ])::(add_desc_flatEnv_aux t str c desc depth ((eqStr_str str (get_name_flatVar h)⊕flag))) + ]. + +definition add_desc_flatEnv ≝ λenv,str,c,desc.add_desc_flatEnv_aux (get_subEnv_flatEnv env) str c desc (get_depth_flatEnv env) false. + +(* equivalenza *) +definition env_to_flatEnv ≝ + λe,fe.∀str. + check_desc_env e str → + check_id_flatEnv fe str → + check_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)) → + get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_flatEnv fe str)). + +lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv. + unfold env_to_flatEnv; + unfold empty_env; + unfold empty_flatEnv; + simplify; + intros; + reflexivity. +qed. + +lemma getdescenv_to_enter : ∀e,str.get_desc_env e str = get_desc_env (enter_env e) str. + intros 2; + elim e; + reflexivity. +qed. + +lemma enter_env_to_flatEnv : + ∀e,fe.env_to_flatEnv e fe → env_to_flatEnv (enter_env e) (enter_flatEnv fe). + intros 2; + unfold env_to_flatEnv; + intros; + lapply (H str H1); + [ rewrite < (getdescenv_to_enter e str); + rewrite > Hletin; + + + + + + + + + + diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma index 326ed1d20..813157082 100755 --- a/helm/software/matita/contribs/assembly/compiler/environment.ma +++ b/helm/software/matita/contribs/assembly/compiler/environment.ma @@ -42,36 +42,36 @@ definition aux_env_type ≝ ne_list (list var_elem). definition get_const_desc ≝ λd:desc_elem.match d with [ DESC_ELEM c _ ⇒ c ]. definition get_type_desc ≝ λd:desc_elem.match d with [ DESC_ELEM _ t ⇒ t ]. +definition eqDesc_elem ≝ λd,d'.(eq_bool (get_const_desc d) (get_const_desc d'))⊗(eq_ast_type (get_type_desc d) (get_type_desc d')). + +lemma eq_to_eqdescelem : ∀d,d'.d = d' → eqDesc_elem d d' = true. + intros 3; + rewrite < H; + elim d; + simplify; + rewrite > (eq_to_eqbool b b (refl_eq ??)); + rewrite > (eq_to_eqasttype a a (refl_eq ??)); + reflexivity. +qed. + +lemma eqdescelem_to_eq : ∀d,d'.eqDesc_elem d d' = true → d = d'. + intros 2; + elim d 0; + elim d' 0; + intros 4; + simplify; + intro; + rewrite > (eqbool_to_eq b1 b (andb_true_true ?? H)); + rewrite > (eqasttype_to_eq a1 a (andb_true_true_r ?? H)); + reflexivity. +qed. + 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 ). -(* 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.empty_env&e. definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e. @@ -80,7 +80,7 @@ definition leave_env ≝ λe:aux_env_type.cut_first_neList ? e. 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 strCmp_str str (get_name_var h) with + | cons h t ⇒ match eqStr_str str (get_name_var h) with [ true ⇒ Some ? (get_desc_var h) | false ⇒ get_desc_from_lev_env t str ]]. @@ -134,5 +134,33 @@ definition add_desc_env ≝ (*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 + | ne_cons h tl ⇒ «£((VAR_ELEM str (DESC_ELEM c desc))::h)»&tl ]. + +(* controllo e <= e' *) +definition eq_env_elem ≝ +λe1,e2.match e1 with + [ VAR_ELEM s1 d1 ⇒ match e2 with + [ VAR_ELEM s2 d2 ⇒ (eqStr_str s1 s2)⊗(eqDesc_elem d1 d2) ]]. + +lemma eq_to_eqenv : ∀e1,e2.e1 = e2 → eq_env_elem e1 e2 = true. + intros 3; + rewrite < H; + elim e1; + simplify; + rewrite > (eq_to_eqstr a a (refl_eq ??)); + rewrite > (eq_to_eqdescelem d d (refl_eq ??)); + reflexivity. +qed. + +lemma eqenv_to_eq : ∀e1,e2.eq_env_elem e1 e2 = true → e1 = e2. + intros 2; + elim e1 0; + elim e2 0; + intros 4; + simplify; + intro; + rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H)); + rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H)); + reflexivity. +qed. 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 141544c33..49a027ba7 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_to_ast.ma @@ -385,7 +385,7 @@ definition preast_to_ast_init_val_aux_array : λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x. definition preast_to_ast_init_val_aux_struct : -Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («t£»&nel))) ≝ +Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝ λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x. let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝ @@ -439,7 +439,7 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option ( [ ne_nil h ⇒ opt_map ?? (preast_to_ast_init_val_aux h) (λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒ - Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT (« t £»)),res≫ ]) + Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ]) | ne_cons h tl ⇒ opt_map ?? (preast_to_ast_init_val_aux h) (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl) @@ -452,7 +452,7 @@ let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option ( return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t) with [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true). - Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («t1£»&nelSubType)), + Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)), (preast_to_ast_init_val_aux_struct ?? (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType)) res1 @@ -517,7 +517,7 @@ let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : optio 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)) (λresDecl.opt_map ?? t - (λt'.Some ? («(pair ?? resExpr resDecl)£»&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 ?))))) nelExprDecl) (λres.match optDecl with @@ -570,7 +570,7 @@ 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_BYTE8)£(AST_TYPE_BASE AST_BASE_TYPE_WORD16)») (None ?) ( + 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〉))) ] diff --git a/helm/software/matita/contribs/assembly/compiler/utility.ma b/helm/software/matita/contribs/assembly/compiler/utility.ma index aef219e06..c67298d39 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 ; break »" +notation "« list0 x sep ; break £ y break »" non associative with precedence 90 for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}. @@ -61,18 +61,14 @@ let rec neList_to_list (T:Type) (p_l:ne_list T) on p_l ≝ match p_l with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@neList_to_list T t ]. let rec list_to_neList (T:Type) (p_l:list T) on p_l ≝ - match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «h£» | Some t' ⇒ Some ? («h£»&t') ]]. + match p_l with [ nil ⇒ None (ne_list T) | cons h t ⇒ match list_to_neList T t with [ None ⇒ Some ? «£h» | Some t' ⇒ Some ? («£h»&t') ]]. (* listlen *) -let rec len_list_aux (T:Type) (p_l:list T) (c:nat) on p_l ≝ - match p_l with [ nil ⇒ c | cons _ t ⇒ len_list_aux T t (S c) ]. +let rec len_list (T:Type) (p_l:list T) on p_l ≝ + match p_l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ]. -definition len_list ≝ λT:Type.λl:list T.len_list_aux T l O. - -let rec len_neList_aux (T:Type) (p_l:ne_list T) (c:nat) on p_l ≝ - match p_l with [ ne_nil _ ⇒ (S c) | ne_cons _ t ⇒ len_neList_aux T t (S c) ]. - -definition len_neList ≝ λT:Type.λl:ne_list T.len_neList_aux T l O. +let rec len_neList (T:Type) (p_l:ne_list T) on p_l ≝ + match p_l with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ]. (* nth elem *) let rec nth_list (T:Type) (l:list T) (n:nat) on l ≝ @@ -202,6 +198,22 @@ lemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empt normalize; autobatch ] qed. +lemma isempty_to_eq : ∀T,l.isb_empty_list T l = true → l = []. + do 2 intro; + elim l 0; + [ 1: intro; reflexivity + | 2: intros; normalize in H1:(%); destruct H1 + ]. +qed. + +lemma eq_to_isempty : ∀T,l.l = [] → isb_empty_list T l = true. + do 2 intro; + elim l 0; + [ 1: intro; reflexivity + | 2: intros; destruct H1 + ] +qed. + (* ******** *) (* naturali *) (* ******** *) diff --git a/helm/software/matita/contribs/assembly/freescale/extra.ma b/helm/software/matita/contribs/assembly/freescale/extra.ma index 25e0cb6fa..f683ecf8f 100644 --- a/helm/software/matita/contribs/assembly/freescale/extra.ma +++ b/helm/software/matita/contribs/assembly/freescale/extra.ma @@ -54,6 +54,30 @@ definition eq_bool ≝ [ true ⇒ b2 | false ⇒ not_bool b2 ]. +lemma eqbool_switch : ∀b1,b2.eq_bool b1 b2 = eq_bool b2 b1. + do 2 intro; + elim b1; elim b2; + reflexivity. +qed. + +lemma andbool_switch : ∀b1,b2.and_bool b1 b2 = and_bool b2 b1. + do 2 intro; + elim b1; elim b2; + reflexivity. +qed. + +lemma orbool_switch : ∀b1,b2.or_bool b1 b2 = or_bool b2 b1. + do 2 intro; + elim b1; elim b2; + reflexivity. +qed. + +lemma xorbool_switch : ∀b1,b2.xor_bool b1 b2 = xor_bool b2 b1. + do 2 intro; + elim b1; elim b2; + reflexivity. +qed. + lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2). unfold eq_bool; intros; @@ -64,6 +88,16 @@ lemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2). destruct H. qed. +lemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true. + do 2 intro; + elim b1 0; + elim b2 0; + intro; + normalize in H:(%); + try destruct H; + reflexivity. +qed. + (* \ominus *) notation "hvbox(⊖ a)" non associative with precedence 36 for @{ 'not_bool $a }. diff --git a/helm/software/matita/contribs/assembly/freescale/medium_tests.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests.ma index 90762c5fb..75545ac0a 100644 --- a/helm/software/matita/contribs/assembly/freescale/medium_tests.ma +++ b/helm/software/matita/contribs/assembly/freescale/medium_tests.ma @@ -24,7 +24,8 @@ (* data ultima modifica 15/11/2007 *) (* ********************************************************************** *) -include "freescale/medium_tests_lemmas.ma". +(* include "freescale/medium_tests_tools.ma" *) +include "freescale/medium_tests_tools.ma". (* ************************ *) (* HCS08GB60 String Reverse *) diff --git a/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma index 81505ac26..d59e88568 100644 --- a/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma +++ b/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma @@ -147,8 +147,8 @@ lemma execute_HCS08_LDHX_maIMM2 : (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))). - - intros; +elim daemon. +(* intros; whd in ⊢ (? ? % ?); whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); rewrite > H; @@ -245,7 +245,7 @@ lemma execute_HCS08_LDHX_maIMM2 : rewrite > (set_set_clk_desc HCS08 t (set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (None ?)); rewrite > (set_clk_f_set_clk_desc HCS08 t s (λtmps.set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t tmps (set_indX_16_reg_HC08 (alu HCS08 t tmps) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t tmps (get_pc_reg HCS08 t tmps) 3))) in ⊢ (? ? (? ? %) ?); [2: elim H; reflexivity ] - reflexivity. + reflexivity.*) qed. definition execute_HCS08_STHX_maSP1_aux ≝ @@ -283,8 +283,8 @@ lemma execute_HCS08_STHX_maSP1 : (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) = array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE) → (execute HCS08 MEM_TREE (TickOK ? s) 5 = execute_HCS08_STHX_maSP1_aux s blow). - - intros; +elim daemon. +(* intros; whd in ⊢ (? ? % ?); whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?); rewrite > H; @@ -434,5 +434,5 @@ lemma execute_HCS08_STHX_maSP1 : rewrite > (set_clk_f_set_clk_desc HCS08 MEM_TREE s (λs.set_pc_reg HCS08 MEM_TREE (setweak_v_flag HCS08 MEM_TREE (setweak_n_flag HCS08 MEM_TREE (set_z_flag HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s))) (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))) (eq_w16 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_b8 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) false) (filtered_plus_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 3))) in ⊢ (? ? (? ? %) ?); [2: elim H; reflexivity ] - reflexivity. + reflexivity.*) qed. diff --git a/helm/software/matita/contribs/assembly/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma index 4072f445f..e630438dc 100644 --- a/helm/software/matita/contribs/assembly/freescale/status.ma +++ b/helm/software/matita/contribs/assembly/freescale/status.ma @@ -397,44 +397,74 @@ definition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option (* setter forte della ALU *) definition set_alu ≝ -λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.match s with - [ mk_any_status _ mem chk clk ⇒ mk_any_status m t alu' mem chk clk ]. +λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'. + mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s). (* setter forte della memoria *) definition set_mem_desc ≝ -λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.match s with - [ mk_any_status alu _ chk clk ⇒ mk_any_status m t alu mem' chk clk ]. +λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t. + mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s). (* setter forte del descrittore *) definition set_chk_desc ≝ -λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.match s with - [ mk_any_status alu mem _ clk ⇒ mk_any_status m t alu mem chk' clk ]. +λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t. + mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s). (* setter forte del clik *) definition set_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t. -λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).match s with - [ mk_any_status alu mem chk _ ⇒ mk_any_status m t alu mem chk clk' ]. +λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16). + mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'. (* REGISTRO A *) (* setter specifico HC05 di A *) definition set_acc_8_low_reg_HC05 ≝ -λalu.λacclow':byte8.match alu with - [ mk_alu_HC05 _ indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow' indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ]. +λalu.λacclow':byte8. + mk_alu_HC05 + acclow' + (indX_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di A *) definition set_acc_8_low_reg_HC08 ≝ -λalu.λacclow':byte8.match alu with - [ mk_alu_HC08 _ indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow' indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λacclow':byte8. + mk_alu_HC08 + acclow' + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter specifico RS08 di A *) definition set_acc_8_low_reg_RS08 ≝ -λalu.λacclow':byte8.match alu with - [ mk_alu_RS08 _ pc pcm spc xm psm zfl cfl ⇒ - mk_alu_RS08 acclow' pc pcm spc xm psm zfl cfl ]. +λalu.λacclow':byte8. + mk_alu_RS08 + acclow' + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + (x_map_RS08 alu) + (ps_map_RS08 alu) + (z_flag_RS08 alu) + (c_flag_RS08 alu). (* setter forte di A *) definition set_acc_8_low_reg ≝ @@ -451,15 +481,38 @@ definition set_acc_8_low_reg ≝ (* setter specifico HC05 di X *) definition set_indX_8_low_reg_HC05 ≝ -λalu.λindxlow':byte8.match alu with - [ mk_alu_HC05 acclow _ sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow' sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl ]. +λalu.λindxlow':byte8. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + indxlow' + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di X *) definition set_indX_8_low_reg_HC08 ≝ -λalu.λindxlow':byte8.match alu with - [ mk_alu_HC08 acclow _ indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow' indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λindxlow':byte8. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + indxlow' + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di X *) definition set_indX_8_low_reg ≝ @@ -481,9 +534,20 @@ definition setweak_indX_8_low_reg ≝ (* setter specifico HC08/HCS08 di H *) definition set_indX_8_high_reg_HC08 ≝ -λalu.λindxhigh':byte8.match alu with - [ mk_alu_HC08 acclow indxlow _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh' sp pc vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λindxhigh':byte8. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + indxhigh' + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di H *) definition set_indX_8_high_reg ≝ @@ -505,9 +569,20 @@ definition setweak_indX_8_high_reg ≝ (* setter specifico HC08/HCS08 di H:X *) definition set_indX_16_reg_HC08 ≝ -λalu.λindx16:word16.match alu with - [ mk_alu_HC08 acclow _ _ sp pc vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow (w16l indx16) (w16h indx16) sp pc vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λindx16:word16. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (w16l indx16) + (w16h indx16) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di H:X *) definition set_indX_16_reg ≝ @@ -529,15 +604,38 @@ definition setweak_indX_16_reg ≝ (* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *) definition set_sp_reg_HC05 ≝ -λalu.λsp':word16.match alu with - [ mk_alu_HC05 acclow indxlow _ spm spf pc pcm hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow (or_w16 (and_w16 sp' spm) spf) spm spf pc pcm hfl ifl nfl zfl cfl irqfl ]. +λalu.λsp':word16. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu)) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di SP *) definition set_sp_reg_HC08 ≝ -λalu.λsp':word16.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh _ pc vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp' pc vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λsp':word16. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + sp' + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di SP *) definition set_sp_reg ≝ @@ -559,21 +657,51 @@ definition setweak_sp_reg ≝ (* setter specifico HC05 di PC, effettua PC∧mask *) definition set_pc_reg_HC05 ≝ -λalu.λpc':word16.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf _ pcm hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf (and_w16 pc' pcm) pcm hfl ifl nfl zfl cfl irqfl ]. +λalu.λpc':word16. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (and_w16 pc' (pc_mask_HC05 alu)) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di PC *) definition set_pc_reg_HC08 ≝ -λalu.λpc':word16.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp _ vfl hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc' vfl hfl ifl nfl zfl cfl irqfl ]. +λalu.λpc':word16. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + pc' + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter specifico RS08 di PC, effettua PC∧mask *) definition set_pc_reg_RS08 ≝ -λalu.λpc':word16.match alu with - [ mk_alu_RS08 acclow _ pcm spc xm psm zfl cfl ⇒ - mk_alu_RS08 acclow (and_w16 pc' pcm) pcm spc xm psm zfl cfl ]. +λalu.λpc':word16. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (and_w16 pc' (pc_mask_RS08 alu)) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + (x_map_RS08 alu) + (ps_map_RS08 alu) + (z_flag_RS08 alu) + (c_flag_RS08 alu). (* setter forte di PC *) definition set_pc_reg ≝ @@ -590,9 +718,16 @@ definition set_pc_reg ≝ (* setter specifico RS08 di SPC, effettua SPC∧mask *) definition set_spc_reg_RS08 ≝ -λalu.λspc':word16.match alu with - [ mk_alu_RS08 acclow pc pcm _ xm psm zfl cfl ⇒ - mk_alu_RS08 acclow pc pcm (and_w16 spc' pcm) xm psm zfl cfl ]. +λalu.λspc':word16. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (and_w16 spc' (pc_mask_RS08 alu)) + (x_map_RS08 alu) + (ps_map_RS08 alu) + (z_flag_RS08 alu) + (c_flag_RS08 alu). (* setter forte di SPC *) definition set_spc_reg ≝ @@ -614,9 +749,16 @@ definition setweak_spc_reg ≝ (* setter specifico RS08 di memory mapped X *) definition set_x_map_RS08 ≝ -λalu.λxm':byte8.match alu with - [ mk_alu_RS08 acclow pc pcm spc _ psm zfl cfl ⇒ - mk_alu_RS08 acclow pc pcm spc xm' psm zfl cfl ]. +λalu.λxm':byte8. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + xm' + (ps_map_RS08 alu) + (z_flag_RS08 alu) + (c_flag_RS08 alu). (* setter forte di memory mapped X *) definition set_x_map ≝ @@ -638,9 +780,16 @@ definition setweak_x_map ≝ (* setter specifico RS08 di memory mapped PS *) definition set_ps_map_RS08 ≝ -λalu.λpsm':byte8.match alu with - [ mk_alu_RS08 acclow pc pcm spc xm _ zfl cfl ⇒ - mk_alu_RS08 acclow pc pcm spc xm psm' zfl cfl ]. +λalu.λpsm':byte8. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + (x_map_RS08 alu) + psm' + (z_flag_RS08 alu) + (c_flag_RS08 alu). (* setter forte di memory mapped PS *) definition set_ps_map ≝ @@ -662,9 +811,20 @@ definition setweak_ps_map ≝ (* setter specifico HC08/HCS08 di V *) definition set_v_flag_HC08 ≝ -λalu.λvfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc _ hfl ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl' hfl ifl nfl zfl cfl irqfl ]. +λalu.λvfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + vfl' + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di V *) definition set_v_flag ≝ @@ -686,15 +846,38 @@ definition setweak_v_flag ≝ (* setter specifico HC05 di H *) definition set_h_flag_HC05 ≝ -λalu.λhfl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm _ ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl' ifl nfl zfl cfl irqfl ]. +λalu.λhfl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + hfl' + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di H *) definition set_h_flag_HC08 ≝ -λalu.λhfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl _ ifl nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl' ifl nfl zfl cfl irqfl ]. +λalu.λhfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + hfl' + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di H *) definition set_h_flag ≝ @@ -716,15 +899,38 @@ definition setweak_h_flag ≝ (* setter specifico HC05 di I *) definition set_i_flag_HC05 ≝ -λalu.λifl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl _ nfl zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl' nfl zfl cfl irqfl ]. +λalu.λifl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + ifl' + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di I *) definition set_i_flag_HC08 ≝ -λalu.λifl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl _ nfl zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl' nfl zfl cfl irqfl ]. +λalu.λifl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + ifl' + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di I *) definition set_i_flag ≝ @@ -746,15 +952,38 @@ definition setweak_i_flag ≝ (* setter specifico HC05 di N *) definition set_n_flag_HC05 ≝ -λalu.λnfl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl _ zfl cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl' zfl cfl irqfl ]. +λalu.λnfl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + nfl' + (z_flag_HC05 alu) + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di N *) definition set_n_flag_HC08 ≝ -λalu.λnfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl _ zfl cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl' zfl cfl irqfl ]. +λalu.λnfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + nfl' + (z_flag_HC08 alu) + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter forte di N *) definition set_n_flag ≝ @@ -776,21 +1005,51 @@ definition setweak_n_flag ≝ (* setter specifico HC05 di Z *) definition set_z_flag_HC05 ≝ -λalu.λzfl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl _ cfl irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl' cfl irqfl ]. +λalu.λzfl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + zfl' + (c_flag_HC05 alu) + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di Z *) definition set_z_flag_HC08 ≝ -λalu.λzfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl _ cfl irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl' cfl irqfl ]. +λalu.λzfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + zfl' + (c_flag_HC08 alu) + (irq_flag_HC08 alu). (* setter sprcifico RS08 di Z *) definition set_z_flag_RS08 ≝ -λalu.λzfl':bool.match alu with - [ mk_alu_RS08 acclow pc pcm spc xm psm _ cfl ⇒ - mk_alu_RS08 acclow pc pcm spc xm psm zfl' cfl ]. +λalu.λzfl':bool. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + (x_map_RS08 alu) + (ps_map_RS08 alu) + zfl' + (c_flag_RS08 alu). (* setter forte di Z *) definition set_z_flag ≝ @@ -807,21 +1066,51 @@ definition set_z_flag ≝ (* setter specifico HC05 di C *) definition set_c_flag_HC05 ≝ -λalu.λcfl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl _ irqfl ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl' irqfl ]. +λalu.λcfl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + cfl' + (irq_flag_HC05 alu). (* setter specifico HC08/HCS08 di C *) definition set_c_flag_HC08 ≝ -λalu.λcfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl _ irqfl ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl' irqfl ]. +λalu.λcfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + cfl' + (irq_flag_HC08 alu). (* setter specifico RS08 di C *) definition set_c_flag_RS08 ≝ -λalu.λcfl':bool.match alu with - [ mk_alu_RS08 acclow pc pcm spc xm psm zfl _ ⇒ - mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl' ]. +λalu.λcfl':bool. + mk_alu_RS08 + (acc_low_reg_RS08 alu) + (pc_reg_RS08 alu) + (pc_mask_RS08 alu) + (spc_reg_RS08 alu) + (x_map_RS08 alu) + (ps_map_RS08 alu) + (z_flag_RS08 alu) + cfl'. (* setter forte di C *) definition set_c_flag ≝ @@ -838,15 +1127,38 @@ definition set_c_flag ≝ (* setter specifico HC05 di IRQ *) definition set_irq_flag_HC05 ≝ -λalu.λirqfl':bool.match alu with - [ mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl _ ⇒ - mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl' ]. +λalu.λirqfl':bool. + mk_alu_HC05 + (acc_low_reg_HC05 alu) + (indx_low_reg_HC05 alu) + (sp_reg_HC05 alu) + (sp_mask_HC05 alu) + (sp_fix_HC05 alu) + (pc_reg_HC05 alu) + (pc_mask_HC05 alu) + (h_flag_HC05 alu) + (i_flag_HC05 alu) + (n_flag_HC05 alu) + (z_flag_HC05 alu) + (c_flag_HC05 alu) + irqfl'. (* setter specifico HC08/HCS08 di IRQ *) definition set_irq_flag_HC08 ≝ -λalu.λirqfl':bool.match alu with - [ mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl _ ⇒ - mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl' ]. +λalu.λirqfl':bool. + mk_alu_HC08 + (acc_low_reg_HC08 alu) + (indX_low_reg_HC08 alu) + (indX_high_reg_HC08 alu) + (sp_reg_HC08 alu) + (pc_reg_HC08 alu) + (v_flag_HC08 alu) + (h_flag_HC08 alu) + (i_flag_HC08 alu) + (n_flag_HC08 alu) + (z_flag_HC08 alu) + (c_flag_HC08 alu) + irqfl'. (* setter forte di IRQ *) definition set_irq_flag ≝ diff --git a/helm/software/matita/contribs/assembly/string/ascii_min.ma b/helm/software/matita/contribs/assembly/string/ascii_min.ma index 8871397c8..b3a247ab5 100755 --- a/helm/software/matita/contribs/assembly/string/ascii_min.ma +++ b/helm/software/matita/contribs/assembly/string/ascii_min.ma @@ -175,3 +175,97 @@ definition magic_of_ascii_min ≝ (* confronto fra ascii_min *) definition eqAsciiMin ≝ λc,c':ascii_min.(eq_b8 (magic_of_ascii_min c) (magic_of_ascii_min c')). + +lemma eq_to_eqasciimin : ∀a1,a2.a1 = a2 → eqAsciiMin a1 a2 = true. + do 3 intro; + unfold eqAsciiMin; + rewrite > H; + elim a2; + reflexivity. +qed. + +(* 63^2 casi... *) +lemma eqasciimin_to_eq_00 : ∀a.eqAsciiMin ch_0 a = true → ch_0 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_01 : ∀a.eqAsciiMin ch_1 a = true → ch_1 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_02 : ∀a.eqAsciiMin ch_2 a = true → ch_2 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_03 : ∀a.eqAsciiMin ch_3 a = true → ch_3 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_04 : ∀a.eqAsciiMin ch_4 a = true → ch_4 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_05 : ∀a.eqAsciiMin ch_5 a = true → ch_5 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_06 : ∀a.eqAsciiMin ch_6 a = true → ch_6 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_07 : ∀a.eqAsciiMin ch_7 a = true → ch_7 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_08 : ∀a.eqAsciiMin ch_8 a = true → ch_8 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_09 : ∀a.eqAsciiMin ch_9 a = true → ch_9 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_10 : ∀a.eqAsciiMin ch__ a = true → ch__ = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_11 : ∀a.eqAsciiMin ch_A a = true → ch_A = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_12 : ∀a.eqAsciiMin ch_B a = true → ch_B = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_13 : ∀a.eqAsciiMin ch_C a = true → ch_C = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_14 : ∀a.eqAsciiMin ch_D a = true → ch_D = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_15 : ∀a.eqAsciiMin ch_E a = true → ch_E = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_16 : ∀a.eqAsciiMin ch_F a = true → ch_F = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_17 : ∀a.eqAsciiMin ch_G a = true → ch_G = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_18 : ∀a.eqAsciiMin ch_H a = true → ch_H = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_19 : ∀a.eqAsciiMin ch_I a = true → ch_I = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_20 : ∀a.eqAsciiMin ch_J a = true → ch_J = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_21 : ∀a.eqAsciiMin ch_K a = true → ch_K = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_22 : ∀a.eqAsciiMin ch_L a = true → ch_L = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_23 : ∀a.eqAsciiMin ch_M a = true → ch_M = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_24 : ∀a.eqAsciiMin ch_N a = true → ch_N = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_25 : ∀a.eqAsciiMin ch_O a = true → ch_O = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_26 : ∀a.eqAsciiMin ch_P a = true → ch_P = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_27 : ∀a.eqAsciiMin ch_Q a = true → ch_Q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_28 : ∀a.eqAsciiMin ch_R a = true → ch_R = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_29 : ∀a.eqAsciiMin ch_S a = true → ch_S = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_30 : ∀a.eqAsciiMin ch_T a = true → ch_T = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_31 : ∀a.eqAsciiMin ch_U a = true → ch_U = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_32 : ∀a.eqAsciiMin ch_V a = true → ch_V = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_33 : ∀a.eqAsciiMin ch_W a = true → ch_W = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_34 : ∀a.eqAsciiMin ch_X a = true → ch_X = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_35 : ∀a.eqAsciiMin ch_Y a = true → ch_Y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_36 : ∀a.eqAsciiMin ch_Z a = true → ch_Z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_37 : ∀a.eqAsciiMin ch_a a = true → ch_a = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_38 : ∀a.eqAsciiMin ch_b a = true → ch_b = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_39 : ∀a.eqAsciiMin ch_c a = true → ch_c = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_40 : ∀a.eqAsciiMin ch_d a = true → ch_d = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_41 : ∀a.eqAsciiMin ch_e a = true → ch_e = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_42 : ∀a.eqAsciiMin ch_f a = true → ch_f = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_43 : ∀a.eqAsciiMin ch_g a = true → ch_g = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_44 : ∀a.eqAsciiMin ch_h a = true → ch_h = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_45 : ∀a.eqAsciiMin ch_i a = true → ch_i = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_46 : ∀a.eqAsciiMin ch_j a = true → ch_j = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_47 : ∀a.eqAsciiMin ch_k a = true → ch_k = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_48 : ∀a.eqAsciiMin ch_l a = true → ch_l = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_49 : ∀a.eqAsciiMin ch_m a = true → ch_m = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_50 : ∀a.eqAsciiMin ch_n a = true → ch_n = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_51 : ∀a.eqAsciiMin ch_o a = true → ch_o = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_52 : ∀a.eqAsciiMin ch_p a = true → ch_p = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_53 : ∀a.eqAsciiMin ch_q a = true → ch_q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_54 : ∀a.eqAsciiMin ch_r a = true → ch_r = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_55 : ∀a.eqAsciiMin ch_s a = true → ch_s = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_56 : ∀a.eqAsciiMin ch_t a = true → ch_t = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_57 : ∀a.eqAsciiMin ch_u a = true → ch_u = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_58 : ∀a.eqAsciiMin ch_v a = true → ch_v = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_59 : ∀a.eqAsciiMin ch_w a = true → ch_w = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_60 : ∀a.eqAsciiMin ch_x a = true → ch_x = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_61 : ∀a.eqAsciiMin ch_y a = true → ch_y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. +lemma eqasciimin_to_eq_62 : ∀a.eqAsciiMin ch_z a = true → ch_z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed. + +lemma eqasciimin_to_eq : ∀a1.∀a2.eqAsciiMin a1 a2 = true → a1 = a2. + do 1 intro; + elim a1 0; + [ 1: apply eqasciimin_to_eq_00 | 2: apply eqasciimin_to_eq_01 | 3: apply eqasciimin_to_eq_02 | 4: apply eqasciimin_to_eq_03 + | 5: apply eqasciimin_to_eq_04 | 6: apply eqasciimin_to_eq_05 | 7: apply eqasciimin_to_eq_06 | 8: apply eqasciimin_to_eq_07 + | 9: apply eqasciimin_to_eq_08 | 10: apply eqasciimin_to_eq_09 | 11: apply eqasciimin_to_eq_10 | 12: apply eqasciimin_to_eq_11 + | 13: apply eqasciimin_to_eq_12 | 14: apply eqasciimin_to_eq_13 | 15: apply eqasciimin_to_eq_14 | 16: apply eqasciimin_to_eq_15 + | 17: apply eqasciimin_to_eq_16 | 18: apply eqasciimin_to_eq_17 | 19: apply eqasciimin_to_eq_18 | 20: apply eqasciimin_to_eq_19 + | 21: apply eqasciimin_to_eq_20 | 22: apply eqasciimin_to_eq_21 | 23: apply eqasciimin_to_eq_22 | 24: apply eqasciimin_to_eq_23 + | 25: apply eqasciimin_to_eq_24 | 26: apply eqasciimin_to_eq_25 | 27: apply eqasciimin_to_eq_26 | 28: apply eqasciimin_to_eq_27 + | 29: apply eqasciimin_to_eq_28 | 30: apply eqasciimin_to_eq_29 | 31: apply eqasciimin_to_eq_30 | 32: apply eqasciimin_to_eq_31 + | 33: apply eqasciimin_to_eq_32 | 34: apply eqasciimin_to_eq_33 | 35: apply eqasciimin_to_eq_34 | 36: apply eqasciimin_to_eq_35 + | 37: apply eqasciimin_to_eq_36 | 38: apply eqasciimin_to_eq_37 | 39: apply eqasciimin_to_eq_38 | 40: apply eqasciimin_to_eq_39 + | 41: apply eqasciimin_to_eq_40 | 42: apply eqasciimin_to_eq_41 | 43: apply eqasciimin_to_eq_42 | 44: apply eqasciimin_to_eq_43 + | 45: apply eqasciimin_to_eq_44 | 46: apply eqasciimin_to_eq_45 | 47: apply eqasciimin_to_eq_46 | 48: apply eqasciimin_to_eq_47 + | 49: apply eqasciimin_to_eq_48 | 50: apply eqasciimin_to_eq_49 | 51: apply eqasciimin_to_eq_50 | 52: apply eqasciimin_to_eq_51 + | 53: apply eqasciimin_to_eq_52 | 54: apply eqasciimin_to_eq_53 | 55: apply eqasciimin_to_eq_54 | 56: apply eqasciimin_to_eq_55 + | 57: apply eqasciimin_to_eq_56 | 58: apply eqasciimin_to_eq_57 | 59: apply eqasciimin_to_eq_58 | 60: apply eqasciimin_to_eq_59 + | 61: apply eqasciimin_to_eq_60 | 62: apply eqasciimin_to_eq_61 | 63: apply eqasciimin_to_eq_62 ]. +qed. diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma index f60b8a804..7681c112e 100755 --- a/helm/software/matita/contribs/assembly/string/string.ma +++ b/helm/software/matita/contribs/assembly/string/string.ma @@ -38,17 +38,53 @@ definition isNull_str ≝ [ nil ⇒ true | cons _ _ ⇒ false ]. (* strcmp *) -let rec strCmp_str (str,str':aux_str_type) ≝ +let rec eqStr_str (str,str':aux_str_type) ≝ match str with [ nil ⇒ match str' with - [ nil ⇒ true | cons _ _ ⇒ false ] + [ nil => true + | cons _ _ => false ] | cons h t ⇒ match str' with [ nil ⇒ false - | cons h' t' ⇒ match eqAsciiMin h h' with - [ true ⇒ strCmp_str t t' | false ⇒ false ] - ]]. + | cons h' t' ⇒ (eqAsciiMin h h')⊗(eqStr_str t t') + ] + ]. -axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'. +lemma eq_to_eqstr : ∀s,s'.s = s' → eqStr_str s s' = true. + do 2 intro; + intro; + rewrite < H; + elim s; + [ 1: reflexivity + | 2: simplify; + rewrite > (eq_to_eqasciimin a a (refl_eq ??)); + rewrite > H1; + reflexivity + ]. +qed. + +lemma eqstr_to_eq : ∀s,s'.eqStr_str s s' = true → s = s'. + intros 1; + elim s 0; + intros; + [ simplify in H:(%); + cases s' in H; + simplify; + intros; + [ reflexivity + | destruct H + ] + | elim s' in H1; + [ simplify in H1; + destruct H1 + | simplify in H2; + lapply (andb_true_true ?? H2); + lapply (andb_true_true_r ?? H2); + rewrite > (H ? Hletin1); + rewrite > (eqasciimin_to_eq ?? Hletin); + reflexivity + ] + ]. +qed. (* strcat *) definition strCat_str ≝ @@ -70,5 +106,27 @@ definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ]. (* confronto *) -definition strCmp_strId ≝ -λsid,sid':aux_strId_type.(strCmp_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')). +definition eqStrId_str ≝ +λsid,sid':aux_strId_type.(eqStr_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')). + +lemma eq_to_eqstrid : ∀s,s'.s = s' → eqStrId_str s s' = true. + intros 3; + rewrite < H; + elim s; + simplify; + rewrite > (eq_to_eqstr a a (refl_eq ??)); + rewrite > (eq_to_eqb_true n n (refl_eq ??)); + reflexivity. +qed. + +lemma eqstrid_to_eq : ∀s,s'.eqStrId_str s s' = true → s = s'. + intros 2; + elim s 0; + elim s' 0; + intros 4; + simplify; + intro; + rewrite > (eqstr_to_eq a1 a (andb_true_true ?? H)); + rewrite > (eqb_true_to_eq n1 n (andb_true_true_r ?? H)); + reflexivity. +qed. -- 2.39.2