From 5688b80cf330cc66038720e04cf7c0293630c163 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 4 Nov 2008 15:23:36 +0000 Subject: [PATCH] =?utf8?q?eliminazione=20di=20un=20passaggio=20di=20transi?= =?utf8?q?tivit=C3=A0=20in=20ast2astfe=20dimostrazione=20di=20un=20assioma?= =?utf8?q?=20in=20env2flatenv?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit --- .../assembly/compiler/ast_to_astfe.ma | 316 +++++++++--------- .../contribs/assembly/compiler/astfe_tree.ma | 5 - .../assembly/compiler/env_to_flatenv.ma | 130 +++++-- .../contribs/assembly/compiler/environment.ma | 1 - .../contribs/assembly/compiler/preast_tree.ma | 2 - 5 files changed, 254 insertions(+), 200 deletions(-) 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 ce2fe1eb2..c6d859c4e 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe.ma @@ -27,8 +27,8 @@ include "compiler/sigma.ma". (* ************************ *) (* - AST_ID: ∀str:aux_str_type. - (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))) + AST_ID: ∀str:aux_str_type. + (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str))) *) lemma ast_to_astfe_id : ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t. @@ -64,56 +64,55 @@ lemma ast_to_astfe_retype_id : qed. (* - AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - - AST_EXPR_NEG: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_NOT: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_COM: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - - AST_EXPR_ADD: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SUB: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_MUL: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_DIV: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SHR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) - AST_EXPR_SHL: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) - - AST_EXPR_GT : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_GTE: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_LT : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_LTE: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_EQ : ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_NEQ: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - - AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) - AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) - AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) - - AST_EXPR_ID: ∀b:bool.∀t:ast_type. - ast_var e b t → ast_expr e t + AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + +| AST_EXPR_NEG: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_NOT: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_COM: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) + +| AST_EXPR_ADD: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SUB: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_MUL: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_DIV: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SHR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) +| AST_EXPR_SHL: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t) + +| AST_EXPR_GT : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_GTE: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_LT : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_LTE: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_EQ : ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_NEQ: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + +| AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + +| AST_EXPR_ID: ∀b:bool.∀t:ast_type. + ast_var d e b t → ast_expr d e t *) let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t) - (m:aux_map_type d) fe - (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝ + (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝ match ast return λW.λa:ast_expr d e W.astfe_expr fe W with @@ -187,16 +186,15 @@ let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t) ] (* - AST_VAR_ID: ∀b:bool.∀t:ast_type. - ast_id e b t → ast_var e b t - AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. - ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t - AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. - ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n) + AST_VAR_ID: ∀b:bool.∀t:ast_type. + ast_id d e b t → ast_var d e b t +| AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. + ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t +| AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. + ast_var d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n) *) and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t) - (m:aux_map_type d) fe - (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝ + (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝ match ast return λW,X.λa:ast_var d e W X.astfe_var fe W X with @@ -211,12 +209,12 @@ and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t) ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv) ] (* - AST_BASE_EXPR: ∀t:ast_base_type. - ast_expr e (AST_TYPE_BASE t) → ast_base_expr e + AST_BASE_EXPR: ∀t:ast_base_type. + ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e + *) and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e) - (m:aux_map_type d) fe - (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝ + (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝ match ast return λa:ast_base_expr d e.astfe_base_expr fe with @@ -226,8 +224,7 @@ and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e) let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) d (e:aux_env_type d) (m:aux_map_type d) fe' - (dimInv:env_to_flatEnv_inv d e m fe') - (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝ + (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝ match ast return λW.λa:astfe_expr fe W.astfe_expr fe' W with @@ -302,8 +299,7 @@ let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) ] and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t) d (e:aux_env_type d) (m:aux_map_type d) fe' - (dimInv:env_to_flatEnv_inv d e m fe') - (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝ + (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝ match ast return λW,X.λa:astfe_var fe W X.astfe_var fe' W X with @@ -319,8 +315,7 @@ and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t) ] and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe) d (e:aux_env_type d) (m:aux_map_type d) fe' - (dimInv:env_to_flatEnv_inv d e m fe') - (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝ + (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝ match ast return λa:astfe_base_expr fe.astfe_base_expr fe' with @@ -329,10 +324,10 @@ and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe) ]. (* - AST_INIT_VAR: ∀b:bool.∀t:ast_type. - ast_var e b t → ast_init e t - AST_INIT_VAL: ∀t:ast_type. - aux_ast_init_type t → ast_init e t + AST_INIT_VAR: ∀b:bool.∀t:ast_type. + ast_var d e b t → ast_init d e t +| AST_INIT_VAL: ∀t:ast_type. + aux_ast_init_type t → ast_init d e t *) definition ast_to_astfe_init ≝ λd.λe:aux_env_type d.λt.λast:ast_init d e t. @@ -366,14 +361,16 @@ definition ast_to_astfe_retype_init ≝ ]. (* - ASTFE_STM_ASG: ∀t:ast_type. - astfe_var e false t → astfe_expr e t → astfe_stm e - ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. - astfe_id e b t → astfe_init e t → astfe_stm e - ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e - ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e + ASTFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → astfe_stm e +| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → astfe_stm e +| ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e +| ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e *) -let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d (e:aux_env_type d) m fe' dimInv dimLe on ast : astfe_stm fe' ≝ +let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) + d (e:aux_env_type d) (m:aux_map_type d) fe' + (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝ match ast with [ ASTFE_STM_ASG sType sVar sExpr ⇒ ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe) @@ -397,34 +394,35 @@ let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d (e:aux_env_type d) m fe' (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe))) ] (* - ASTFE_BODY: list (astfe_stm e) → astfe_body e + ASTFE_BODY: list (astfe_stm e) → astfe_body e *) -and ast_to_astfe_retype_body fe (ast:astfe_body fe) d (e:aux_env_type d) m fe' dimInv dimLe on ast : astfe_body fe' ≝ +and ast_to_astfe_retype_body fe (ast:astfe_body fe) + d (e:aux_env_type d) (m:aux_map_type d) fe' + (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_body fe' ≝ match ast with [ ASTFE_BODY sLStm ⇒ ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm) ]. definition ast_to_astfe_retype_stm_list ≝ -λfe.λast:list (astfe_stm fe).λd.λe:aux_env_type d.λm,fe',dimInv,dimLe. +λfe.λast:list (astfe_stm fe). +λd.λe:aux_env_type d.λm:aux_map_type d.λfe'. +λdimInv:env_to_flatEnv_inv d e m fe'. +λdimLe:le_flatEnv fe fe' = true. fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast. definition ast_to_astfe_retype_exprBody_neList ≝ -λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd.λe:aux_env_type d.λm,fe',dimInv,dimLe. +λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)). +λd.λe:aux_env_type d.λm:aux_map_type d.λfe'. +λdimInv:env_to_flatEnv_inv d e m fe'. +λdimLe:le_flatEnv fe fe' = true. cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe) (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe) )»&t) «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))» ast). -(* - 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 -*) +(* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *) inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝ AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'. env_to_flatEnv_inv d e m fe' → @@ -453,26 +451,31 @@ AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'. list (astfe_stm fe') → ast_to_astfe_decl_aux_record d e fe. -let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d e m fe' → - le_flatEnv fe fe' = true → +(* + AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type. + ast_var d e false t → ast_expr d e t → ast_stm d e +| AST_STM_WHILE: ∀d.∀e:aux_env_type d. + ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e +| AST_STM_IF: ∀d.∀e:aux_env_type d. + ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e +*) +let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe. + env_to_flatEnv_inv d e m fe → ast_to_astfe_stm_record d e fe ≝ match ast return λD.λE.λast:ast_stm D E. - Πm:aux_map_type D.Πfe.Πfe'. - env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record D E fe + Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe with [ AST_STM_ASG sD sE sType sVar sExpr ⇒ - λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. - AST_TO_ASTFE_STM_RECORD sD sE fe m fe' dimInv dimLe - (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sD sE false sType sVar m fe' dimInv) - (ast_to_astfe_expr sD sE sType sExpr m fe' dimInv)) - + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv + (eq_to_leflatenv ?? (refl_eq ??)) + (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv) + (ast_to_astfe_expr sD sE sType sExpr m fe dimInv)) | AST_STM_WHILE sD sE sExpr sDecl ⇒ - λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. - match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe' fe' - (env_map_flatEnv_enter_aux sD sE m fe' dimInv) - (eq_to_leflatenv ?? (refl_eq ??)) with + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe + (env_map_flatEnv_enter_aux sD sE m fe dimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (λenv.ast_to_astfe_stm_record sD env fe) @@ -482,9 +485,9 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux (leave_map sD resMap) resFe (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) - (leflatenv_trans ??? dimLe resDimLe) + resDimLe (ASTFE_STM_WHILE resFe - (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sD sE sExpr m fe' dimInv) + (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv) sD (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (leave_map sD resMap) @@ -495,16 +498,14 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux sE (leave_add_enter_env sD sE resTrsf) ] | AST_STM_IF sD sE sExprDecl sOptDecl ⇒ - λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE)))) - (pMap:aux_map_type sD) (pFe,pFe':aux_flatEnv_type) - (pDimInv:env_to_flatEnv_inv sD sE pMap pFe') - (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record sD sE pFe ≝ + (pMap:aux_map_type sD) (pFe:aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝ match nel with [ ne_nil h ⇒ - match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe' pFe' - (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv) - (eq_to_leflatenv ?? (refl_eq ??)) with + match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe + (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (λenv.ast_to_astfe_if_record sD env pFe) @@ -514,8 +515,8 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux (leave_map sD resMap) resFe (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) - (leflatenv_trans ??? pDimLe resDimLe) - «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe' pDimInv) + resDimLe + «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv) sD (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (leave_map sD resMap) @@ -526,36 +527,33 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux sE (leave_add_enter_env sD sE resTrsf) ] | ne_cons h t ⇒ - match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe' pFe' - (env_map_flatEnv_enter_aux sD sE pMap pFe' pDimInv) - (eq_to_leflatenv ?? (refl_eq ??)) with + match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe + (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ - match aux t (leave_map sD resMap) resFe resFe + match aux t (leave_map sD resMap) resFe (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe) (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv) - sE (leave_add_enter_env sD sE resTrsf)) - (eq_to_leflatenv ?? (refl_eq ??)) with + sE (leave_add_enter_env sD sE resTrsf)) with [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒ AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv' - (leflatenv_trans ??? pDimLe (leflatenv_trans ??? resDimLe resDimLe')) - («£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe' pDimInv) + (leflatenv_trans ??? resDimLe resDimLe') + («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv) sD sE resMap' resFe' resDimInv' (leflatenv_trans ??? resDimLe resDimLe')) (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm) sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]] ] in - match aux sExprDecl m fe fe' dimInv dimLe with + match aux sExprDecl m fe dimInv with [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒ match sOptDecl with [ None ⇒ AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?)) | Some sDecl ⇒ - match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe resFe - (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) - (eq_to_leflatenv ?? (refl_eq ??)) with + match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe + (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒ eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE))) (λenv.ast_to_astfe_stm_record sD env fe) @@ -576,91 +574,87 @@ let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux resDimLe') (Some ? (ASTFE_BODY resFe' resLStm)))) sE (leave_add_enter_env sD sE resTrsf) ]]] + ] (* - AST_NO_DECL: ∀e:aux_env_type. - list (ast_stm e) → ast_decl e - AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type. - (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e + AST_NO_DECL: ∀d.∀e:aux_env_type d. + list (ast_stm d e) → ast_decl d e +| AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e *) -and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.Πfe'. - env_to_flatEnv_inv d e m fe' → - le_flatEnv fe fe' = true → +and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe. + env_to_flatEnv_inv d e m fe → ast_to_astfe_decl_record d e fe ≝ match ast return λD.λE.λast:ast_decl D E. - Πm:aux_map_type D.Πfe.Πfe'. - env_to_flatEnv_inv D E m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record D E fe + Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe with [ AST_NO_DECL sD sE sLStm ⇒ - λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. - let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe,pFe':aux_flatEnv_type) - (pDimInv:env_to_flatEnv_inv sD sE pMap pFe') - (pDimLe:le_flatEnv pFe pFe' = true) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝ + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. + let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝ match l with [ nil ⇒ - AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe' pDimInv pDimLe [] + AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) [] | cons h t ⇒ - match ast_to_astfe_stm sD sE h pMap pFe' pFe' pDimInv (eq_to_leflatenv ?? (refl_eq ??)) with + match ast_to_astfe_stm sD sE h pMap pFe pDimInv with [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒ - match aux t resMap resFe resFe resDimInv (eq_to_leflatenv ?? (refl_eq ??)) with + match aux t resMap resFe resDimInv with [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒ AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv' - (leflatenv_trans ??? pDimLe (leflatenv_trans ??? resDimLe resDimLe')) + (leflatenv_trans ??? resDimLe resDimLe') ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]] ] in - match aux sLStm m fe fe' dimInv dimLe with + match aux sLStm m fe dimInv with [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe [] (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv) resDimLe resLStm ] | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒ - λm:aux_map_type sD.λfe,fe'.λdimInv:env_to_flatEnv_inv sD sE m fe'.λdimLe:le_flatEnv fe fe' = true. + λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe. match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl - (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) - (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) - (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) - (env_map_flatEnv_addSingle_aux sD sE m fe' sName sB sType dimInv) - (eq_to_leflatenv ?? (refl_eq ??)) with + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒ AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe ([ tripleT ??? sName sB sType ]@resTrsf) (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) - (leflatenv_trans ??? dimLe (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe' [ tripleT ??? sName sB sType ]) resDimLe)) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe) (match sOptInit with [ None ⇒ [] | Some init ⇒ [ ASTFE_STM_INIT resFe sB sType (* l'id e' sull'ambiente arricchito *) - (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) + (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) sB sType (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType) sB sType (newid_from_init sD sE sName sB sType) - (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) - (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe'))) - (env_map_flatEnv_addSingle_aux sD sE m fe' sName sB sType dimInv)) + (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe))) + (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv)) sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE) resMap resFe (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) resDimLe) (* l'init e' sull'ambiente non arricchito *) - (ast_to_astfe_retype_init fe' sType (ast_to_astfe_init sD sE sType init m fe' dimInv) + (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv) sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE) resMap resFe (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv) - (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe' [ tripleT ??? sName sB sType ]) resDimLe)) + (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)) ]]@resLStm) ] ]. (* - AST_ROOT: ast_decl empty_env → ast_root. + AST_ROOT: ast_decl O empty_env → ast_root *) definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝ λast:ast_root.match ast with - [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv empty_flatEnv env_map_flatEnv_empty_aux (eq_to_leflatenv ?? (refl_eq ??)) with + [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]]. diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma index c806a04bd..2690b2466 100755 --- a/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree.ma @@ -19,12 +19,7 @@ (* *) (* ********************************************************************** *) -include "string/string.ma". -include "compiler/utility.ma". -include "freescale/word32.ma". -include "compiler/ast_type.ma". include "compiler/env_to_flatenv.ma". -include "compiler/ast_tree.ma". (* **************************** *) (* ALBERO DI TOKEN CON FLAT ENV *) 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 d8805d269..156d9a8bd 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv.ma @@ -469,17 +469,87 @@ lemma getidmap_to_enter : ] qed. -(* leave: elimina la testa (il "cur" corrente) *) -let rec leave_map d (map:aux_map_type (S d)) on map ≝ - match map with - [ nil ⇒ [] - | cons h t ⇒ - (MAP_ELEM d - (get_name_mapElem (S d) h) - (get_max_mapElem (S d) h) - (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??)) - )::(leave_map d t) - ]. +lemma checkdescenter_to_checkdesc : + ∀d.∀e:aux_env_type d.∀str. + check_desc_env (S d) (enter_env d e) str → + check_desc_env d e str. + intros; + unfold enter_env in H:(%); + simplify in H:(%); + apply H. +qed. + +lemma checkenvmapalign_to_enter : + ∀de.∀e:aux_env_type de.∀dm.∀m:aux_map_type dm. + check_env_map_align de e dm m = + check_env_map_align (S de) (enter_env de e) (S dm) (enter_map dm m). + intros 4; + unfold enter_env; + simplify; + elim e 0; + [ simplify; + intro; + elim l 0; + [ simplify; + reflexivity + | simplify; + intros; + rewrite > (getidmap_to_enter ???); + rewrite < H; + cases (get_id_map_aux dm m (get_name_var a)); + [ simplify; + reflexivity + | simplify; + rewrite > H; + reflexivity + ] + ] + | simplify; + intros 2; + elim l 0; + [ simplify; + intros; + apply H + | intros; + simplify; + rewrite > (getidmap_to_enter ???); + cases (get_id_map_aux dm m (get_name_var a)); + [ simplify; + reflexivity + | simplify; + apply (H e1 H1) + ] + ] + ]. +qed. + +lemma env_map_flatEnv_enter_aux : + ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe. + unfold env_to_flatEnv_inv; + intros; + split; + [ split; + [ split; + [ split; + [ rewrite < (checkenvmapalign_to_enter ???); + apply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))))) + | (* TO DO !!! *) elim daemon; + ] + | unfold check_id_map; + rewrite > (getidmap_to_enter ???); + apply (proj2 ?? (proj1 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1))))) + ] + | unfold get_id_map; + rewrite > (getidmap_to_enter ???); + apply (proj2 ?? (proj1 ?? (H str (checkdescenter_to_checkdesc ??? H1)))) + ] + | unfold get_id_map; + rewrite > (getidmap_to_enter ???); + apply (proj2 ?? (H str (checkdescenter_to_checkdesc ??? H1))) + ]. +qed. (* aggiungi descrittore *) let rec new_map_elem_from_depth_aux (d:nat) on d ≝ @@ -526,22 +596,7 @@ let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_ty (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))) ]. -(* avanzamento dell'invariante *) -lemma env_map_flatEnv_enter_aux : - ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe. - env_to_flatEnv_inv d e map fe → - env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe. - unfold env_to_flatEnv_inv; - intros; - split; [ split [ split [ split | ] | ] | ] - [ elim daemon - | elim daemon; - | elim daemon; - | elim daemon; - | elim daemon; - ] -qed. - +(* TO DO !!! *) axiom env_map_flatEnv_add_aux : ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf. env_to_flatEnv_inv d e map fe → @@ -647,10 +702,17 @@ lemma buildtrasfenvadd_to_le : reflexivity. qed. -axiom env_map_flatEnv_leave_aux : - ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf. - env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe → - env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe. +(* leave: elimina la testa (il "cur" corrente) *) +let rec leave_map d (map:aux_map_type (S d)) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ + (MAP_ELEM d + (get_name_mapElem (S d) h) + (get_max_mapElem (S d) h) + (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??)) + )::(leave_map d t) + ]. lemma leave_add_enter_env_aux : ∀d.∀a:aux_env_type d.∀trsf.∀c. @@ -674,6 +736,12 @@ lemma leave_add_enter_env : reflexivity. qed. +(* TO DO !!! *) +axiom env_map_flatEnv_leave_aux : + ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf. + env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe → + env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe. + lemma newid_from_init : ∀d.∀e:aux_env_type d.∀name,const,desc. ast_id d (add_desc_env d e name const desc) const desc. diff --git a/helm/software/matita/contribs/assembly/compiler/environment.ma b/helm/software/matita/contribs/assembly/compiler/environment.ma index 2603787be..590a98d1f 100755 --- a/helm/software/matita/contribs/assembly/compiler/environment.ma +++ b/helm/software/matita/contribs/assembly/compiler/environment.ma @@ -20,7 +20,6 @@ (* ********************************************************************** *) include "string/string.ma". -include "freescale/word32.ma". include "compiler/ast_type.ma". (* ***************** *) diff --git a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma index 662d289fb..9a463d1b6 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma @@ -20,8 +20,6 @@ (* ********************************************************************** *) include "string/string.ma". -include "compiler/utility.ma". -include "freescale/word32.ma". include "compiler/ast_type.ma". (* ****************** *) -- 2.39.2