--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+
+
+
+
+
+
+
(* 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 ??)).
projects / helm.git / commitdiff