From ac9b845041058587b9185af930d2992fd05a501d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Oct 2008 11:31:35 +0000 Subject: [PATCH] New invariant and data structure to represent environments, transformation maps and flat environments (2nd compiler pass). --- .../assembly/compiler/ast_to_astfe1.ma | 749 ++++++++++++++++++ .../contribs/assembly/compiler/astfe_tree1.ma | 140 ++++ .../assembly/compiler/env_to_flatenv1.ma | 616 ++++++++++---- 3 files changed, 1353 insertions(+), 152 deletions(-) create mode 100755 helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma create mode 100755 helm/software/matita/contribs/assembly/compiler/astfe_tree1.ma diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma new file mode 100755 index 000000000..836f6f50f --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma @@ -0,0 +1,749 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* *) +(* Sviluppato da: *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "compiler/astfe_tree1.ma". +include "compiler/sigma.ma". + +(* ************************ *) +(* PASSO 2 : da AST a ASTFE *) +(* ************************ *) + +(* + AST_ID: ∀str:aux_str_type. + (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))) +*) +lemma ast_to_astfe_id : + ∀e,b,t.∀ast:ast_id e b t. + ∀d.∀m:aux_map_type d.∀fe,fe'. + ∀dimInv:env_to_flatEnv_inv d e m fe'. + ∀dimLe:le_flatEnv fe fe' = true. + ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + astfe_id fe' b t . + intros 8; + unfold env_to_flatEnv_inv; + elim a 0; + intros 5; + lapply (ASTFE_ID fe' (STR_ID a1 (get_id_map d m a1)) ?); + [ apply (proj2 ?? (proj1 ?? (dimInv a1 H))) + | rewrite > (proj2 ?? (dimInv a1 H)); + apply Hletin + ]. +qed. + +lemma ast_to_astfe_retype_id : + ∀fe,b,t.∀ast:astfe_id fe b t. + ∀d.∀e.∀m:aux_map_type d.∀fe'. + ∀dimInv:env_to_flatEnv_inv d e m fe'. + ∀dimLe:le_flatEnv fe fe' = true. + ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + astfe_id fe' b t. + intros 8; + unfold env_to_flatEnv_inv; + elim a 0; + intros 5; + lapply (ASTFE_ID fe' a1 ?); + [ apply (leflatenv_to_check fe fe' a1 dimLe H) + | rewrite > (leflatenv_to_get fe fe' a1 dimLe H); + apply Hletin + ]. +qed. + +(* + AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + + AST_EXPR_NEG: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_NOT: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_COM: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + + AST_EXPR_ADD: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_SUB: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_MUL: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_DIV: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_SHR: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) + AST_EXPR_SHL: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t) + + AST_EXPR_GT : ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_GTE: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_LT : ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_LTE: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_EQ : ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_NEQ: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + + AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + + AST_EXPR_ID: ∀b:bool.∀t:ast_type. + ast_var e b t → ast_expr e t +*) +let rec ast_to_astfe_expr e t (ast:ast_expr e t) + d (m:aux_map_type d) fe fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝ + match ast + return λW.λa:ast_expr e W.astfe_expr fe' W + with + [ AST_EXPR_BYTE8 val ⇒ + ASTFE_EXPR_BYTE8 fe' val + | AST_EXPR_WORD16 val ⇒ + ASTFE_EXPR_WORD16 fe' val + | AST_EXPR_WORD32 val ⇒ + ASTFE_EXPR_WORD32 fe' val + + | AST_EXPR_NEG bType sExpr ⇒ + ASTFE_EXPR_NEG fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_NOT bType sExpr ⇒ + ASTFE_EXPR_NOT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_COM bType sExpr ⇒ + ASTFE_EXPR_COM fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe) + + | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_ADD fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SUB fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_MUL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_DIV fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SHR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SHL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe) + + | AST_EXPR_GT bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_GT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_GTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_LT bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_LT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_LTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_EQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe) + + | AST_EXPR_B8toW16 sExpr ⇒ + ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_B8toW32 sExpr ⇒ + ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_W16toB8 sExpr ⇒ + ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_W16toW32 sExpr ⇒ + ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_W32toB8 sExpr ⇒ + ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe) + | AST_EXPR_W32toW16 sExpr ⇒ + ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe) + + | AST_EXPR_ID b sType var ⇒ + ASTFE_EXPR_ID fe' b sType (ast_to_astfe_var e b sType var d m fe fe' dimInv dimLe emfe) + + ] +(* + AST_VAR_ID: ∀b:bool.∀t:ast_type. + ast_id e b t → ast_var e b t + AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. + ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t + AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. + ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n) +*) +and ast_to_astfe_var e b t (ast:ast_var e b t) + d (m:aux_map_type d) fe fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝ + match ast + return λW,X.λa:ast_var e W X.astfe_var fe' W X + with + [ AST_VAR_ID sB sType sId ⇒ + ASTFE_VAR_ID fe' sB sType (ast_to_astfe_id e sB sType sId d m fe fe' dimInv dimLe emfe) + + | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒ + ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_base_expr e sExpr d m fe fe' dimInv dimLe emfe) + + | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒ + ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe fe' dimInv dimLe emfe) + ] +(* + AST_BASE_EXPR: ∀t:ast_base_type. + ast_expr e (AST_TYPE_BASE t) → ast_base_expr e +*) +and ast_to_astfe_base_expr e (ast:ast_base_expr e) + d (m:aux_map_type d) fe fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝ + match ast + return λa:ast_base_expr e.astfe_base_expr fe' + with + [ AST_BASE_EXPR bType sExpr ⇒ + ASTFE_BASE_EXPR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe) + ]. + +let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) + d e (m:aux_map_type d) fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝ + match ast + return λW.λa:astfe_expr fe W.astfe_expr fe' W + with + [ ASTFE_EXPR_BYTE8 val ⇒ + ASTFE_EXPR_BYTE8 fe' val + | ASTFE_EXPR_WORD16 val ⇒ + ASTFE_EXPR_WORD16 fe' val + | ASTFE_EXPR_WORD32 val ⇒ + ASTFE_EXPR_WORD32 fe' val + + | ASTFE_EXPR_NEG bType sExpr ⇒ + ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_NOT bType sExpr ⇒ + ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_COM bType sExpr ⇒ + ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe) + + | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe) + + | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒ + ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe) + + | ASTFE_EXPR_B8toW16 sExpr ⇒ + ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_B8toW32 sExpr ⇒ + ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_W16toB8 sExpr ⇒ + ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_W16toW32 sExpr ⇒ + ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_W32toB8 sExpr ⇒ + ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe emfe) + | ASTFE_EXPR_W32toW16 sExpr ⇒ + ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe emfe) + + | ASTFE_EXPR_ID b sType var ⇒ + ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe emfe) + + ] +and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t) + d e (m:aux_map_type d) fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝ + match ast + return λW,X.λa:astfe_var fe W X.astfe_var fe' W X + with + [ ASTFE_VAR_ID sB sType sId ⇒ + ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe) + + | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒ + ASTFE_VAR_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe) + + | ASTFE_VAR_STRUCT sB sType sField sVar ⇒ + ASTFE_VAR_STRUCT fe' sB sType sField (ast_to_astfe_retype_var fe sB (AST_TYPE_STRUCT sType) sVar d e m fe' dimInv dimLe emfe) + ] +and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe) + d e (m:aux_map_type d) fe' + (dimInv:env_to_flatEnv_inv d e m fe') + (dimLe:le_flatEnv fe fe' = true) + (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝ + match ast + return λa:astfe_base_expr fe.astfe_base_expr fe' + with + [ ASTFE_BASE_EXPR bType sExpr ⇒ + ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe) + ]. + +(* + AST_INIT_VAR: ∀b:bool.∀t:ast_type. + ast_var e b t → ast_init e t + AST_INIT_VAL: ∀t:ast_type. + aux_ast_init_type t → ast_init e t +*) +definition ast_to_astfe_init ≝ +λe,t.λast:ast_init e t. +λd.λm:aux_map_type d.λfe,fe'. +λdimInv:env_to_flatEnv_inv d e m fe'. +λdimLe:le_flatEnv fe fe' = true. +λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + match ast + return λW.λa:ast_init e W.astfe_init fe' W + with + [ AST_INIT_VAR sB sType sVar ⇒ + ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_var e sB sType sVar d m fe fe' dimInv dimLe emfe) + + | AST_INIT_VAL sType sArgs ⇒ + ASTFE_INIT_VAL fe' sType sArgs + + ]. + +definition ast_to_astfe_retype_init ≝ +λfe,t.λast:astfe_init fe t. +λd.λe.λm:aux_map_type d.λfe'. +λdimInv:env_to_flatEnv_inv d e m fe'. +λdimLe:le_flatEnv fe fe' = true. +λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + match ast + return λW.λa:astfe_init fe W.astfe_init fe' W + with + [ ASTFE_INIT_VAR sB sType sVar ⇒ + ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe emfe) + + | ASTFE_INIT_VAL sType sArgs ⇒ + ASTFE_INIT_VAL fe' sType sArgs + + ]. + +(* + 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 +*) +(*lemma ast_to_astfe_stm_aux : + ∀d,e.∀m:aux_map_type d.∀fe,fe',dimInv,dimLe. + ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + ∀ast:astfe_stm fe'. + (ΣD.(ΣE.(ΣM.(ΣFE.(ΣFE'.(ΣDIMINV.(ΣDIMLE.Prod (env_map_flatEnv D E M FE FE' DIMINV DIMLE) (astfe_stm FE')))))))). + elim daemon. +qed.*) +inductive ast_to_astfe_stm_res (d:nat) : Type ≝ +AST_TO_ASTFE_STM_RES: + ∀e.∀m:aux_map_type d.∀fe,fe'. + ∀dimInv:env_to_flatEnv_inv d e m fe'. + ∀dimLe:le_flatEnv fe fe' = true. + ∀trsf:Prod3T aux_str_type bool ast_type. + env_map_flatEnv d e m fe fe' dimInv dimLe → astfe_stm fe' → ast_to_astfe_stm_res d. + +let rec ast_to_astfe_stm e (ast:ast_stm e) on ast ≝ + match ast + return λX.λast:ast_stm X. + Πd.Πm:aux_map_type d.Πfe.Πfe'.ΠdimInv:env_to_flatEnv_inv d X m fe'. + ΠdimLe:le_flatEnv fe fe' = true.env_map_flatEnv d X m fe fe' dimInv dimLe → + ast_to_astfe_stm_res d + with + [ AST_STM_ASG sE sType sVar sExpr ⇒ + λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'. + λdimLe:le_flatEnv fe fe' = true.λemfe:env_map_flatEnv d sE m fe fe' dimInv dimLe. + AST_TO_ASTFE_STM_RES d sE m fe fe' dimInv dimLe emfe [] + (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe fe' dimInv dimLe emfe) + (ast_to_astfe_expr sE sType sExpr d m fe fe' dimInv dimLe emfe)) + + | _ ⇒ False_rect ? daemon + + ]. + + + +let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast + : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝ + match ast + return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) + with + [ AST_STM_ASG e' subType var expr ⇒ + λmap:aux_trasfMap_type e' fe. + opt_map ?? (ast_to_astfe_var e' false subType var fe map) + (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map) + (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫))) + + | AST_STM_WHILE e' expr decl ⇒ + λmap:aux_trasfMap_type e' fe. + opt_map ?? (ast_to_astfe_base_expr e' expr fe map) + (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map)) + (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with + [ pair map' resDecl ⇒ + match le_flatEnv fe fe' + return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) + with + [ true ⇒ λp:(le_flatEnv fe fe' = true). + opt_map ?? (retype_base_expr fe resExpr fe' p) + (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map) + (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫)) + | false ⇒ λp:(le_flatEnv fe fe' = false).None ? + ] (refl_eq ? (le_flatEnv fe fe')) + ]]])) + + | AST_STM_IF e' nelExprDecl optDecl ⇒ + λmap:aux_trasfMap_type e' fe. + let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) + (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝ + match nel with + [ ne_nil h ⇒ + opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m) + (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m)) + (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with + [ pair m' resDecl ⇒ + match le_flatEnv fenv fenv' + return λx.(le_flatEnv fenv fenv' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) + with + [ true ⇒ λp:(le_flatEnv fenv fenv' = true). + opt_map ?? (retype_base_Expr fenv resExpr fenv' p) + (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) + «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫)) + | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ? + ] (refl_eq ? (le_flatEnv fenv fenv')) + ]]])) + + | ne_cons h tl ⇒ + opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m) + (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m)) + (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with + [ pair m' resDecl ⇒ + opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl) + (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with + [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with + [ pair m'' tl' ⇒ + match le_flatEnv fenv fenv'' + return λx.(le_flatEnv fenv fenv'' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) + with + [ true ⇒ λp:(le_flatEnv fenv fenv'' = true). + match le_flatEnv fenv' fenv'' + return λy.(le_flatEnv fenv' fenv'' = y) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) + with + [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true). + opt_map ?? (retype_base_expr fenv resExpr fenv'' p) + (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p') + (λresDecl'. + Some ? (≪fenv'',pair ?? m'' + («£(pair ?? resExpr' + (ASTFE_BODY fenv'' resDecl'))»&tl')≫))) + | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ? + ] (refl_eq ? (le_flatEnv fenv' fenv'')) + | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ? + ] (refl_eq ? (le_flatEnv fenv fenv'')) + ]])]]])) + ] in + opt_map ?? (aux fe map nelExprDecl) + (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with + [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with + [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with + [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫) + | Some decl ⇒ + opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m')) + (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with + [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒ + match le_flatEnv fe' fe'' + return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) + with + [ true ⇒ λp'':(le_flatEnv fe' fe'' = true). + opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'') + (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')) + (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m') + (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫)) + | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ? + ] (refl_eq ? (le_flatEnv fe' fe'')) + ]]])]]]) + ] +(* + AST_NO_DECL: ∀e:aux_env_type. + list (ast_stm e) → ast_decl e + AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type. + (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e +*) +and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast + : Πmap:aux_trasfMap_type e fe.option (Σf:aux_trasfEnv_type.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e) fe') (list (astfe_stm fe')))) ≝ + match ast + return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) + with + [ AST_NO_DECL e' lStm ⇒ + λmap:aux_trasfMap_type e' fe. + let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll + : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝ + match ll with + [ nil ⇒ let trsf ≝ [] + in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv) + (list (astfe_stm fenv)) + (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫ + + | cons h tl ⇒ + opt_map ?? (ast_to_astfe_stm e' h fenv m) + (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with + [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with + [ pair m' resStm ⇒ + opt_map ?? (aux tl fenv' m') + (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with + [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with + [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with + [ pair m'' tl' ⇒ + match le_flatEnv fenv' fenv'' + return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) + with + [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true). + opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p) + (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') + (list (astfe_stm fenv'')) + m'' + (resStm'@tl')≫≫) + | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ? + ] (refl_eq ? (le_flatEnv fenv' fenv'')) + ]]])]])] in + aux lStm fe map + + | AST_DECL e' b name t dim optInit subDecl ⇒ + λmap:aux_trasfMap_type e' fe. + opt_map ?? (match optInit with + [ None ⇒ Some ? [] + | Some init ⇒ + opt_map ?? (ast_to_astfe_init e' t init fe map) + (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ?? + (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t) + (next_nameId e' fe map name) + (ast_to_astfe_dec_aux e' name b t fe map dim)) + b t) + (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t) + (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t)) + (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ])))) + ]) + (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl + (add_desc_flatEnv fe (next_nameId e' fe map name) b t) + (add_maxcur_map e' fe map map name b t)) + (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with + [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with + [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with + [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒ + match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' + return λx.(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = x) → option (Σf'.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f') e') fe') (list (astfe_stm fe')))) + with + [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true). + opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p) + (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f + in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe') + (list (astfe_stm fe')) + map' + (hRes'@tRes)≫≫) + | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ? + ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe')) + ]]])) + ]. + +(* + AST_ROOT: ast_decl empty_env → ast_root. +*) +definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝ +λast:ast_root.match ast with + [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with + (* impossibile: dummy *) + [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫ + | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with + [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with + [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with + [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫ + ]]]]]. + +(* mini test +include "compiler/preast_tree.ma". +include "compiler/preast_to_ast.ma". + +{ const byte8 a; + const byte8[3] b={0,1,2}; + byte8[3] c=b; + + if(0xF0) + { byte8 a=a; } + else if(0xF1) + { + while(0x10) + { byte8[3] b=c; } + } + else if(0xF2) + { byte8 a=b[0]; } + else + { const byte8 a=a; } +} + +definition prova ≝ +PREAST_ROOT ( + PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) ( + PREAST_DECL true [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAL (PREAST_INIT_VAL_ARRAY «(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x2〉)»))) ( + PREAST_DECL false [ch_C] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_B]))) ( + PREAST_NO_DECL [ + PREAST_STM_IF « + (pair ?? + (PREAST_EXPR_BYTE8 〈xF,x0〉) + (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL [])) + ) + ; (pair ?? + (PREAST_EXPR_BYTE8 〈xF,x1〉) + (PREAST_NO_DECL [ + (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) ( + PREAST_DECL false [ch_B] (AST_TYPE_ARRAY (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) 2) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_C]))) (PREAST_NO_DECL []) + )) + ]) + ) + £ (pair ?? + (PREAST_EXPR_BYTE8 〈xF,x2〉) + (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ARRAY (PREAST_VAR_ID [ch_B]) (PREAST_EXPR_BYTE8 〈x0,x0〉)))) (PREAST_NO_DECL [])) + ) + » (Some ? (PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))) + ] + ) + ) + ) +). +*) + + + + + + + + + + + + +(* + ASTFE_STM_ASG: ∀t:ast_type. + astfe_var e false t → astfe_expr e t → astfe_stm e + ASTFE_STM_INIT: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_init e t → astfe_stm e + ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e + ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e +*) +let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_stm fe' ≝ + match ast with + [ ASTFE_STM_ASG sType sVar sExpr ⇒ + ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe emfe) + + | ASTFE_STM_INIT sB sType sId sInit ⇒ + ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe emfe) + + | ASTFE_STM_WHILE sExpr sBody ⇒ + ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe) + + | ASTFE_STM_IF sNelExprBody sOptBody ⇒ + ASTFE_STM_IF fe' (cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe) + )»&t) + «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))» + sNelExprBody)) + (opt_map ?? sOptBody + (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe))) + ] +(* + ASTFE_BODY: list (astfe_stm e) → astfe_body e +*) +and ast_to_astfe_retype_body fe (ast:astfe_body fe) d e m fe' dimInv dimLe (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_body fe' ≝ + match ast with + [ ASTFE_BODY sLStm ⇒ + ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe ]@t) [] sLStm) + ]. + +definition ast_to_astfe_retype_stm_list ≝ +λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe]@t) [] ast. + +definition ast_to_astfe_retype_exprBody_neList ≝ +λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe. + cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe emfe) + (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe) + )»&t) + «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))» + ast). + + + + + + + diff --git a/helm/software/matita/contribs/assembly/compiler/astfe_tree1.ma b/helm/software/matita/contribs/assembly/compiler/astfe_tree1.ma new file mode 100755 index 000000000..c346cb792 --- /dev/null +++ b/helm/software/matita/contribs/assembly/compiler/astfe_tree1.ma @@ -0,0 +1,140 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "string/string.ma". +include "compiler/utility.ma". +include "freescale/word32.ma". +include "compiler/ast_type.ma". +include "compiler/env_to_flatenv1.ma". +include "compiler/ast_tree.ma". + +(* **************************** *) +(* ALBERO DI TOKEN CON FLAT ENV *) +(* **************************** *) + +(* id: accesso all'ambiente con stringa *) +inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝ + ASTFE_ID: ∀str:aux_strId_type. + (* D *) check_desc_flatEnv e str → astfe_id e (get_const_desc (get_desc_flatEnv e str)) (get_type_desc (get_desc_flatEnv e str)). + +(* -------------------------- *) + +(* espressioni *) +inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝ + ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) + +| ASTFE_EXPR_NEG: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_NOT: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_COM: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) + +| ASTFE_EXPR_ADD: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_SUB: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_MUL: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_DIV: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_SHR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) +| ASTFE_EXPR_SHL: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t) + +| ASTFE_EXPR_GT : ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_GTE: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_LT : ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_LTE: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_EQ : ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_NEQ: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) + +| ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) +| ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) +| ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) +| ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) + +| ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type. + astfe_var e b t → astfe_expr e t + +(* variabile: modificatori di array/struct dell'id *) +with astfe_var : bool → ast_type → Type ≝ + ASTFE_VAR_ID: ∀b:bool.∀t:ast_type. + astfe_id e b t → astfe_var e b t +| ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat. + astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t +| ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat. + astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n) + +(* espressioni generalizzate: anche non uniformi per tipo *) +with astfe_base_expr : Type ≝ + ASTFE_BASE_EXPR: ∀t:ast_base_type. + astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e. + +(* -------------------------- *) + +(* + inizializzatori: ammesse solo due forme, no ibridi + 1) var1 = var2 + 2) var = ... valori ... +*) +inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝ + ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type. + astfe_var e b t → astfe_init e t +| ASTFE_INIT_VAL: ∀t:ast_type. + aux_ast_init_type t → astfe_init e t. + +(* -------------------------- *) + +(* statement: assegnamento/while/if else if else + conversione di dichiarazione *) +inductive astfe_stm (e:aux_flatEnv_type) : Type ≝ + 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 + +(* dichiarazioni *) +with astfe_body : Type ≝ + ASTFE_BODY: list (astfe_stm e) → astfe_body e. + +(* -------------------------- *) + +(* programma *) +inductive astfe_root (e:aux_flatEnv_type) : Type ≝ + ASTFE_ROOT: astfe_body e → astfe_root e. + +(* -------------------------- *) + +(* programma vuoto *) +definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (nil ?)). diff --git a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma index 0b3cde19e..8b3b2623d 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma @@ -25,212 +25,524 @@ include "compiler/environment.ma". (* GESTIONE AMBIENTE FLAT *) (* ********************** *) -(* elemento: name + nel curId + nel desc *) +(* ambiente flat *) 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). +VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem. + +definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ]. +definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ]. + +definition aux_flatEnv_type ≝ list var_flatElem. + +definition empty_flatEnv ≝ nil var_flatElem. + +(* mappa: nome + max + cur *) +inductive n_list : nat → Type ≝ + n_nil: n_list O +| n_cons: ∀n.option nat → n_list n → n_list (S n). + +definition defined_nList ≝ +λd.λl:n_list d.match l with [ n_nil ⇒ False | n_cons _ _ _ ⇒ True ]. + +definition cut_first_nList : Πd.n_list d → ? → n_list (pred d) ≝ +λd.λl:n_list d.λp:defined_nList ? l. + let value ≝ + match l + return λX.λY:n_list X.defined_nList X Y → n_list (pred X) + with + [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p + | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).t + ] p in value. + +definition get_first_nList : Πd.n_list d → ? → option nat ≝ +λd.λl:n_list d.λp:defined_nList ? l. + let value ≝ + match l + return λX.λY:n_list X.defined_nList X Y → option nat + with + [ n_nil ⇒ λp:defined_nList O n_nil.False_rect ? p + | n_cons n h t ⇒ λp:defined_nList (S n) (n_cons n h t).h + ] p in value. + +inductive map_elem (d:nat) : Type ≝ +MAP_ELEM: aux_str_type → nat → n_list (S d) → map_elem d. + +definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ]. +definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ]. +definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ]. + +definition aux_map_type ≝ λd.list (map_elem d). + +definition empty_map ≝ nil (map_elem O). + +axiom defined_nList_S_to_true : +∀d.∀l:n_list (S d).defined_nList (S d) l = True. + +lemma defined_get_id : + ∀d.∀h:map_elem d.True → defined_nList (S d) (get_cur_mapElem d h). + intros 3; + rewrite > (defined_nList_S_to_true ? (get_cur_mapElem d h)); + apply H. +qed. -(* ambiente vuoto *) -definition empty_flatEnv ≝ pair ?? O (nil var_flatElem). +(* get_id *) +let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝ + match map with + [ nil ⇒ None ? + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ get_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I) + | false ⇒ get_id_map_aux d t name + ] + ]. -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 ]. +definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. -(* 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) +(* get_max *) +let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝ + match map with + [ nil ⇒ None ? + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ Some ? (get_max_mapElem d h) + | false ⇒ get_max_map_aux d t name + ] ]. -definition enter_flatEnv ≝ -λenv.pair ?? (get_depth_flatEnv env) (enter_flatEnv_aux (get_subEnv_flatEnv env)). +definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ]. -(* 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) - ]. +(* check_id *) +definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ]. + +definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ]. + +lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name. + unfold checkb_id_map; + unfold check_id_map; + intros 3; + elim (get_id_map_aux d map name) 0; + [ simplify; intro; destruct H + | simplify; intros; apply I + ]. +qed. -definition leave_flatEnv ≝ -λenv.pair ?? (get_depth_flatEnv env) (leave_flatEnv_aux (get_subEnv_flatEnv env)). +definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ]. -(* 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 checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type. + match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ]. -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 ]. +lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name. + unfold checknotb_id_map; + unfold checknot_id_map; + intros 3; + elim (get_id_map_aux d map name) 0; + [ simplify; intro; apply I + | simplify; intros; destruct H + ]. +qed. (* get_desc *) -let rec get_desc_flatEnv_aux (subEnv:list var_flatElem) (name:aux_strId_type) on subEnv ≝ - match subEnv with +let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝ + match fe with [ nil ⇒ None ? - | cons h t ⇒ - match (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 - ] + | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with + [ true ⇒ Some ? (get_desc_flatVar h) + | false ⇒ get_desc_flatEnv_aux t name + ] ]. -definition get_desc_flatEnv ≝ λe:aux_flatEnv_type.λstr:aux_strId_type. - match get_desc_flatEnv_aux (get_subEnv_flatEnv e) str with +definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ]. -(* 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 check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ]. -definition checkb_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_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe 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 ] +lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str. + unfold checkb_desc_flatEnv; + unfold check_desc_flatEnv; + intros 2; + elim (get_desc_flatEnv_aux fe str) 0; + [ simplify; intro; destruct H + | simplify; intros; apply I + ]. qed. -definition checknot_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 checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ]. -definition checknotb_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_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type. + match get_desc_flatEnv_aux fe 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 ] +lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str. + unfold checknotb_desc_flatEnv; + unfold checknot_desc_flatEnv; + intros 2; + elim (get_desc_flatEnv_aux fe str) 0; + [ simplify; intro; apply I + | simplify; intros; destruct H + ]. qed. -(* 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 ]. +(* 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) ]]. -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 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 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 ] +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. -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 ]. +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') ] + ]. -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 eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true. + intros 3; + rewrite < H; + elim e1; + [ reflexivity + | simplify; + rewrite > (eq_to_eqflatenv a a (refl_eq ??)); + rewrite > H1; + reflexivity + ]. +qed. -lemma 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 ] +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. -(* 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 ?)» - ]. +lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true. + intros; + elim fe; + [ simplify; + reflexivity + | simplify; + rewrite > (eq_to_eqflatenv a a (refl_eq ??)); + rewrite > H; + reflexivity + ]. +qed. -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)» ] +lemma leflatenv_to_check : ∀fe,fe',str. + (le_flatEnv fe fe' = true) → + (check_desc_flatEnv fe str) → + (check_desc_flatEnv fe' str). + intros 4; + cases (leflatEnv_to_le fe fe' H); + rewrite < H1; + elim fe 0; + [ intro; simplify in H2:(%); elim H2; + | intros 3; + simplify; + cases (eqStrId_str str (get_name_flatVar a)); + [ simplify; intro; apply H3 + | simplify; apply H2 ] - | 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))) - ]. + ]. +qed. -definition add_desc_flatEnv ≝ λenv,str,c,desc.add_desc_flatEnv_aux (get_subEnv_flatEnv env) str c desc (get_depth_flatEnv env) false. +lemma leflatenv_to_get : ∀fe,fe',str. + (le_flatEnv fe fe' = true) → + (check_desc_flatEnv fe str) → + (get_desc_flatEnv fe str = get_desc_flatEnv fe' str). + intros 4; + cases (leflatEnv_to_le fe fe' H); + rewrite < H1; + elim fe 0; + [ intro; + simplify in H2:(%); + elim H2 + | simplify; + intros 2; + cases (eqStrId_str str (get_name_flatVar a)); + [ simplify; + intros; + reflexivity + | simplify; + unfold check_desc_flatEnv; + unfold get_desc_flatEnv; + cases (get_desc_flatEnv_aux l str); + [ simplify; intros; elim H3 + | simplify; intros; rewrite < (H2 H3); reflexivity + ] + ] + ]. +qed. -(* 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)). +(* invariante *) +definition env_to_flatEnv_inv ≝ + λd.λe:aux_env_type.λmap:aux_map_type d.λfe:aux_flatEnv_type. + ∀str. + check_desc_env e str → + (check_id_map d map str ∧ + check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧ + get_desc_env e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))). + +lemma inv_to_checkdescflatenv : + ∀d.∀e.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → + (∀str.check_desc_env e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))). + intros 7; + unfold env_to_flatEnv_inv in H:(%); + lapply (H str H1); + apply (proj2 ?? (proj1 ?? Hletin)); +qed. -lemma empty_env_to_flatEnv : env_to_flatEnv empty_env empty_flatEnv. - unfold env_to_flatEnv; +lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv. + unfold env_to_flatEnv_inv; unfold empty_env; + unfold empty_map; unfold empty_flatEnv; simplify; intros; - reflexivity. + split; + [ split; apply H | 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. +lemma leflatenv_to_inv : + ∀d.∀e.∀map:aux_map_type d.∀fe,fe'. + le_flatEnv fe fe' = true → + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d e map fe'. + intros 6; + unfold env_to_flatEnv_inv; + intros; + split; + [ split; + [ lapply (H1 str H2); + apply (proj1 ?? (proj1 ?? Hletin)) + | lapply (H1 str H2); + apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin))) + ] + | lapply (H1 str H2); + rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin))); + apply (proj2 ?? Hletin) + ]. qed. -lemma 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; +(* enter: propaga in testa la vecchia testa (il "cur" precedente) *) +let rec enter_map d (map:aux_map_type d) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ + (MAP_ELEM (S d) + (get_name_mapElem d h) + (get_max_mapElem d h) + (n_cons (S d) + (get_first_nList ? (get_cur_mapElem d h) (defined_get_id ?? I)) + (get_cur_mapElem d h)) + )::(enter_map d t) + ]. + +lemma getidmap_to_enter : + ∀d.∀m:aux_map_type d.∀str. + get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str. intros; - lapply (H str H1); - [ rewrite < (getdescenv_to_enter e str); - rewrite > Hletin; + elim m; + [ simplify; reflexivity + | simplify; rewrite > H; reflexivity + ] +qed. +lemma env_map_flatEnv_enter_aux : + ∀d.∀e.∀map:aux_map_type d.∀fe. + env_to_flatEnv_inv d e map fe → env_to_flatEnv_inv (S d) (enter_env e) (enter_map d map) fe. + intros 3; + unfold enter_env; + unfold empty_env; + unfold env_to_flatEnv_inv; + simplify; + elim e 0; + [ elim map 0; + [ simplify; intros; split; + [ apply (proj1 ?? (H str H1)) | apply (proj2 ?? (H str H1)); ] + | simplify; intros; split; + [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H1 str H2)) + | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H1 str H2)) + ] + ] + | elim map 0; + [ simplify; intros; split; + [ apply (proj1 ?? (H1 str H2)) | apply (proj2 ?? (H1 str H2)) ] + | simplify; intros; split; + [ rewrite > (getidmap_to_enter d l str); apply (proj1 ?? (H2 str H3)) + | rewrite > (getidmap_to_enter d l str); apply (proj2 ?? (H2 str H3)) + ] + ] + ]. +qed. +(* leave: elimina la testa (il "cur" corrente) *) +let rec leave_map d (map:aux_map_type (S d)) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ + (MAP_ELEM d + (get_name_mapElem (S d) h) + (get_max_mapElem (S d) h) + (cut_first_nList ? (get_cur_mapElem (S d) h) (defined_get_id ?? I)) + )::(leave_map d t) + ]. +(* aggiungi descrittore *) +let rec new_map_elem_from_depth_aux (d:nat) on d ≝ + match d + return λd.n_list d + with + [ O ⇒ n_nil + | S n ⇒ n_cons n (None ?) (new_map_elem_from_depth_aux n) + ]. +let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝ + match map with + [ nil ⇒ [] + | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with + [ true ⇒ MAP_ELEM d name max (n_cons d (Some ? max) (cut_first_nList (S d) (get_cur_mapElem d h) (defined_get_id ?? I))) + | false ⇒ h + ]::(new_max_map_aux d t name max) + ]. +definition add_desc_env_flatEnv_map ≝ +λd.λmap:aux_map_type d.λstr. + match get_max_map_aux d map str with + [ None ⇒ map@[ MAP_ELEM d str O (n_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ] + | Some x ⇒ new_max_map_aux d map str (S x) + ]. +definition add_desc_env_flatEnv_fe ≝ +λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc. + fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)]) + (DESC_ELEM c desc) ]. +let rec build_trasfEnv_env (trsf:list (Prod3T aux_str_type bool ast_type)) e on trsf ≝ + match trsf with + [ nil ⇒ e + | cons h t ⇒ build_trasfEnv_env t (add_desc_env e (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)) + ]. +let rec build_trasfEnv_mapFe (trasf:list ?) d (mfe:Prod (aux_map_type d) aux_flatEnv_type) on trasf ≝ + match trasf with + [ nil ⇒ mfe + | cons h t ⇒ + build_trasfEnv_mapFe t d (pair ?? (add_desc_env_flatEnv_map d (fst ?? mfe) (fst3T ??? h)) + (add_desc_env_flatEnv_fe d (fst ?? mfe) (snd ?? mfe) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))) + ]. +(* avanzamento delle dimostrazioni *) +axiom env_map_flatEnv_add_aux : + ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf. + env_to_flatEnv_inv d e map fe → + env_to_flatEnv_inv d + (build_trasfEnv_env trsf e) + (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))) + (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))). + +axiom env_map_flatEnv_add_aux_fe : + ∀d.∀map:aux_map_type d.∀fe,trsf. + ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? map fe))). + +lemma buildtrasfenvadd_to_le : + ∀d.∀m:aux_map_type d.∀fe,trsf. + le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true. + intros 4; + cases (env_map_flatEnv_add_aux_fe d m fe trsf); + rewrite < H; + rewrite > (le_to_leflatenv fe x); + reflexivity. +qed. +axiom env_map_flatEnv_leave_aux : + ∀d.∀e.∀map:aux_map_type (S d).∀fe. + env_to_flatEnv_inv (S d) e map fe → + env_to_flatEnv_inv d + (leave_env e) + (leave_map d map) + fe. + +(* avanzamento congiunto oggetti + dimostrazioni *) +inductive env_map_flatEnv : + Πd.Πe.Πm:aux_map_type d.Πfe,fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → Type ≝ + ENV_MAP_FLATENV_EMPTY: env_map_flatEnv O + empty_env + empty_map + empty_flatEnv + empty_flatEnv + env_map_flatEnv_empty_aux + (eq_to_leflatenv ?? (refl_eq ??)) +| ENV_MAP_FLATENV_ENTER: ∀d,e.∀m:aux_map_type d.∀fe,fe'. + ∀dimInv:env_to_flatEnv_inv d e m fe'. + ∀dimLe:le_flatEnv fe fe' = true. + env_map_flatEnv d e m fe fe' dimInv dimLe → + env_map_flatEnv (S d) + (enter_env e) + (enter_map d m) + fe' + fe' + (env_map_flatEnv_enter_aux d e m fe' dimInv) + (eq_to_leflatenv ?? (refl_eq ??)) +| ENV_MAP_FLATENV_ADD: ∀d,e.∀m:aux_map_type d.∀fe,fe'. + ∀dimInv:env_to_flatEnv_inv d e m fe'. + ∀dimLe:le_flatEnv fe fe' = true.∀trsf. + env_map_flatEnv d e m fe fe' dimInv dimLe → + env_map_flatEnv d + (build_trasfEnv_env trsf e) + (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe'))) + fe' + (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe'))) + (env_map_flatEnv_add_aux d e m fe' trsf dimInv) + (buildtrasfenvadd_to_le d m fe' trsf) +| ENV_MAP_FLATENV_LEAVE: ∀d,e.∀m:aux_map_type (S d).∀fe,fe'. + ∀dimInv:env_to_flatEnv_inv (S d) e m fe'. + ∀dimLe:le_flatEnv fe fe' = true. + env_map_flatEnv (S d) e m fe fe' dimInv dimLe → + env_map_flatEnv d + (leave_env e) + (leave_map d m) + fe' + fe' + (env_map_flatEnv_leave_aux d e m fe' dimInv) + (eq_to_leflatenv ?? (refl_eq ??)). -- 2.39.2