eliminazione di un passaggio di transitività in ast2astfe

dimostrazione di un assioma in env2flatenv

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 ce2fe1eb2dd70eb3851147c8e57c9f1cb2ce12b9..c6d859c4e207a65c653a3e883af602bdb2bca09a 100755 (executable)
--- 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 c806a04bd3a237df1d31486a92f00ce944cb28b5..2690b2466f8e85895d50f9a0b2574bcf8933a552 100755 (executable)
--- 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 d8805d26991be6a98a9ba024e471a4e9587e7ccd..156d9a8bd6a63b199782ec25086c37ad561c32f4 100755 (executable)
--- 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 2603787beb73a81b3b26211b8ca4177018393b68..590a98d1f390d277f6bc89d3240640be6fe16599 100755 (executable)
--- 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 662d289fb4e15b7280f0d0836220909f296bd792..9a463d1b65cd055541bce891cfd4f2b243ec4a5f 100755 (executable)
--- 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".
 
 (* ****************** *)