From 80430f28a23d8d643126917e14896482198c24d1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 Oct 2008 08:40:21 +0000 Subject: [PATCH] leave-environment axiom made true --- .../assembly/compiler/ast_to_astfe1.ma | 530 +++++++++--------- .../assembly/compiler/env_to_flatenv1.ma | 76 +-- 2 files changed, 302 insertions(+), 304 deletions(-) diff --git a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma index 836f6f50f..e75401979 100755 --- a/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma +++ b/helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma @@ -20,7 +20,6 @@ (* ********************************************************************** *) include "compiler/astfe_tree1.ma". -include "compiler/sigma.ma". (* ************************ *) (* PASSO 2 : da AST a ASTFE *) @@ -32,18 +31,16 @@ include "compiler/sigma.ma". *) 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; + ∀d.∀m:aux_map_type d.∀fe. + ∀dimInv:env_to_flatEnv_inv d e m fe. + astfe_id fe b t . + intros 7; 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)); + intros 3; + lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?); + [ apply (proj2 ?? (proj1 ?? (H1 a1 H))) + | rewrite > (proj2 ?? (H1 a1 H)); apply Hletin ]. qed. @@ -53,15 +50,14 @@ lemma ast_to_astfe_retype_id : ∀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; + intros 4; lapply (ASTFE_ID fe' a1 ?); - [ apply (leflatenv_to_check fe fe' a1 dimLe H) - | rewrite > (leflatenv_to_get fe fe' a1 dimLe H); + [ apply (leflatenv_to_check fe fe' a1 H2 H) + | rewrite > (leflatenv_to_get fe fe' a1 H2 H); apply Hletin ]. qed. @@ -115,80 +111,78 @@ qed. 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 ≝ + d (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 e W.astfe_expr fe' W + return λW.λa:ast_expr e W.astfe_expr fe W with [ AST_EXPR_BYTE8 val ⇒ - ASTFE_EXPR_BYTE8 fe' val + ASTFE_EXPR_BYTE8 fe val | AST_EXPR_WORD16 val ⇒ - ASTFE_EXPR_WORD16 fe' val + ASTFE_EXPR_WORD16 fe val | AST_EXPR_WORD32 val ⇒ - ASTFE_EXPR_WORD32 fe' 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) + ASTFE_EXPR_NEG fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_COM fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_GT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_LT fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe dimInv) + (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe dimInv) | 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) + ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe dimInv) | 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) + ASTFE_EXPR_ID fe b sType (ast_to_astfe_var e b sType var d m fe dimInv) ] (* @@ -200,44 +194,39 @@ let rec ast_to_astfe_expr e t (ast:ast_expr e t) 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 ≝ + d (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 e W X.astfe_var fe' W X + 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) + ASTFE_VAR_ID fe sB sType (ast_to_astfe_id e sB sType sId d m fe dimInv) | 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) + ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var e sB (AST_TYPE_ARRAY sType sDim) sVar d m fe dimInv) + (ast_to_astfe_base_expr e sExpr d m fe dimInv) | 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) + ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var e sB (AST_TYPE_STRUCT sType) sVar d m fe dimInv) ] (* 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' ≝ + d (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 e.astfe_base_expr fe' + 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) + ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe dimInv) ]. 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 ≝ + (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 @@ -249,95 +238,93 @@ let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t) 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_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe) | 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_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe) | 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_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe) | 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_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe) | 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_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe) | 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_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe) + (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe) | 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_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe) | 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_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe) | 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_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe) | 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_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe) | 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_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe) | 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_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe) | 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) + ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe) ] 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 ≝ + (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 [ 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_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe) | 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_ARRAY fe' sB sType sDim (ast_to_astfe_retype_var fe sB (AST_TYPE_ARRAY sType sDim) sVar d e m fe' dimInv dimLe) + (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe) | 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) + 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) ] 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' ≝ + (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 [ 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) + ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe) ]. (* @@ -348,18 +335,16 @@ and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe) *) 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. +λd.λm:aux_map_type d.λfe. +λdimInv:env_to_flatEnv_inv d e m fe. match ast - return λW.λa:ast_init e W.astfe_init fe' W + 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) + ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var e sB sType sVar d m fe dimInv) | AST_INIT_VAL sType sArgs ⇒ - ASTFE_INIT_VAL fe' sType sArgs + ASTFE_INIT_VAL fe sType sArgs ]. @@ -368,18 +353,69 @@ definition ast_to_astfe_retype_init ≝ λ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_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe) | ASTFE_INIT_VAL sType sArgs ⇒ ASTFE_INIT_VAL fe' sType sArgs ]. +(* + 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 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) + (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe) + + | 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) + (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe) + + | ASTFE_STM_WHILE sExpr sBody ⇒ + ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe) + (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe) + + | 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) + (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' []))» + sNelExprBody)) + (opt_map ?? sOptBody + (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe))) + ] +(* + 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 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,m,fe',dimInv,dimLe. + 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,m,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) + (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 @@ -388,70 +424,130 @@ definition ast_to_astfe_retype_init ≝ 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 ≝ +inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + astfe_stm fe' → + ast_to_astfe_stm_record d e fe. + +inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'. + env_to_flatEnv_inv d e m fe' → + le_flatEnv fe fe' = true → + ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) → + ast_to_astfe_if_record d e fe. + +inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type) (m:aux_map_type d) (fe:aux_flatEnv_type) : Type ≝ +AST_TO_ASTFE_DECL_RECORD: ∀trsf:list (Prod3T aux_str_type bool ast_type). + env_to_flatEnv_inv d + (build_trasfEnv_env trsf e) + (fst ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) + (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) → + le_flatEnv fe (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe))) = true → + list (astfe_stm (snd ?? (build_trasfEnv_mapFe trsf d (pair ?? m fe)))) → + ast_to_astfe_decl_record d e m fe. + +let rec ast_to_astfe_stm e (ast:ast_stm e) on ast : Πd.Π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 ≝ 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 + Πd.Πm:aux_map_type d.Πfe.Πfe'. + env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_stm_record d X fe 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 + λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. + AST_TO_ASTFE_STM_RECORD d sE fe m fe' dimInv dimLe + (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe' dimInv) + (ast_to_astfe_expr sE sType sExpr d m fe' dimInv)) + + | AST_STM_WHILE sE sExpr sDecl ⇒ + λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. + (* in sostanza + 1) eseguo decl su ENTER dell'invariante + 2) decl restituisce ADD+ENTER dell'invariante + 3) eseguo base_expr sull'invariante + 4) retipo base_expr su LEAVE+ADD+ENTER dell'invariante + 5) retituisco su LEAVE+ADD+ENTER dell'invariante *) + match ast_to_astfe_decl (enter_env sE) sDecl (S d) (enter_map d m) fe fe' (env_map_flatEnv_enter_aux d sE m fe' dimInv) dimLe with + [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_STM_RECORD d sE fe + (* m'' *) + (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))) + (* fe'' *) + (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) + (* leave_add_enter(dimInv) *) + (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv) + (* fe ≤ fe' ∧ fe' ≤ fe'' → fe ≤ fe'' *) + (leflatenv_trans ??? dimLe resDimLe) + (* risultato su fe'' *) + (ASTFE_STM_WHILE (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) + (ast_to_astfe_retype_base_expr fe' (ast_to_astfe_base_expr sE sExpr d m fe' dimInv) + d sE + (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe')))) + (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) + (env_map_flatEnv_leave_aux d sE m fe' resTrsf resDimInv) + resDimLe) + (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d m) fe'))) resLStm)) ] + + | AST_STM_IF sE sExprDecl sOptDecl ⇒ + λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. + let rec aux (nel:ne_list (Prod (ast_base_expr sE) (ast_decl (enter_env sE)))) + (pMap:aux_map_type d) (pFe,pFe':aux_flatEnv_type) + (pDimInv:env_to_flatEnv_inv d sE pMap pFe') + (pDimLe:le_flatEnv pFe pFe' = true) on nel : ast_to_astfe_if_record d sE pFe ≝ + match nel with + [ ne_nil h ⇒ + match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with + [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ + AST_TO_ASTFE_IF_RECORD d sE pFe + (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) + (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) + (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) + (leflatenv_trans ??? pDimLe resDimLe) + «£(pair ?? (ast_to_astfe_retype_base_expr pFe' (ast_to_astfe_base_expr sE (fst ?? h) d pMap pFe' pDimInv) + d sE + (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) + (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) + (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) + resDimLe) + (ASTFE_BODY (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) resLStm))» ] + + | ne_cons h t ⇒ (False_rect ? daemon) + (*match ast_to_astfe_decl (enter_env sE) (snd ?? h) (S d) (enter_map d pMap) pFe pFe' (env_map_flatEnv_enter_aux d sE pMap pFe' pDimInv) pDimLe with + [ AST_TO_ASTFE_DECL_RECORD resTrsf resDimInv resDimLe resLStm ⇒ + match aux t (leave_map d (fst ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe')))) + pFe (snd ?? (build_trasfEnv_mapFe resTrsf (S d) (pair ?? (enter_map d pMap) pFe'))) + (env_map_flatEnv_leave_aux d sE pMap pFe' resTrsf resDimInv) + (leflatenv_trans ??? pDimLe resDimLe) with + [ AST_TO_ASTFE_IF_RECORD iMap iFe' iDimInv iDimLe iNelExprDecl ⇒ + AST_TO_ASTFE_IF_RECORD d sE pFe iMap iFe' iDimInv iDimLe + (False_rect ? daemon) ]]*) + + + ] in (False_rect ? daemon) - ]. + ] +and ast_to_astfe_decl e (ast:ast_decl e) on ast : Πd.Π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 m fe' ≝ + match ast + return λX.λast:ast_decl X. + Πd.Πm:aux_map_type d.Πfe.Πfe'. + env_to_flatEnv_inv d X m fe' → le_flatEnv fe fe' = true → ast_to_astfe_decl_record d X m fe' + with + [ AST_NO_DECL sE sLStm ⇒ + λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.λdimLe:le_flatEnv fe fe' = true. + False_rect ? daemon + | _ ⇒ 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')) - ]]])) +FINQUI | AST_STM_IF e' nelExprDecl optDecl ⇒ λmap:aux_trasfMap_type e' fe. @@ -677,73 +773,3 @@ PREAST_ROOT ( ) ). *) - - - - - - - - - - - - -(* - 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/env_to_flatenv1.ma b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma index f341480d7..9202ff86d 100755 --- a/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma +++ b/helm/software/matita/contribs/assembly/compiler/env_to_flatenv1.ma @@ -75,7 +75,7 @@ definition aux_map_type ≝ λd.list (map_elem d). definition empty_map ≝ nil (map_elem O). -theorem defined_nList_S_to_true : +lemma defined_nList_S_to_true : ∀d.∀l:n_list (S d).defined_nList (S d) l = True. intros; inversion l; @@ -368,6 +368,21 @@ lemma leflatenv_to_inv : ]. qed. +lemma leflatenv_trans : + ∀fe,fe',fe''. + le_flatEnv fe fe' = true → + le_flatEnv fe' fe'' = true → + le_flatEnv fe fe'' = true. + intros 4; + cases (leflatenv_to_le fe ? H); + rewrite < H1; + intro; + cases (leflatenv_to_le (fe@x) fe'' H2); + rewrite < H3; + rewrite > associative_append; + apply (le_to_leflatenv fe ?). +qed. + (* 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 @@ -500,55 +515,12 @@ lemma buildtrasfenvadd_to_le : 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 → + ∀d.∀e.∀map:aux_map_type d.∀fe.∀trsf. + env_to_flatEnv_inv (S d) + (build_trasfEnv_env trsf (enter_env e)) + (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))) + (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d 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 ??)). + e + (leave_map d (fst ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe)))) + (snd ?? (build_trasfEnv_mapFe trsf (S d) (pair ?? (enter_map d map) fe))). -- 2.39.2