helm/software/matita/contribs/assembly/compiler/ast_to_astfe1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "compiler/astfe_tree1.ma".
  23 include "compiler/sigma.ma".
  24
  25 (* ************************ *)
  26 (* PASSO 2 : da AST a ASTFE *)
  27 (* ************************ *)
  28
  29 (*
  30  AST_ID: ∀str:aux_str_type.
  31          (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
  32 *)
  33 lemma ast_to_astfe_id :
  34  ∀e,b,t.∀ast:ast_id e b t.
  35  ∀d.∀m:aux_map_type d.∀fe,fe'.
  36  ∀dimInv:env_to_flatEnv_inv d e m fe'.
  37  ∀dimLe:le_flatEnv fe fe' = true.
  38  ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
  39  astfe_id fe' b t .
  40  intros 8;
  41  unfold env_to_flatEnv_inv;
  42  elim a 0;
  43  intros 5;
  44  lapply (ASTFE_ID fe' (STR_ID a1 (get_id_map d m a1)) ?);
  45  [ apply (proj2 ?? (proj1 ?? (dimInv a1 H)))
  46  | rewrite > (proj2 ?? (dimInv a1 H));
  47    apply Hletin
  48  ].
  49 qed.
  50
  51 lemma ast_to_astfe_retype_id :
  52  ∀fe,b,t.∀ast:astfe_id fe b t.
  53  ∀d.∀e.∀m:aux_map_type d.∀fe'.
  54  ∀dimInv:env_to_flatEnv_inv d e m fe'.
  55  ∀dimLe:le_flatEnv fe fe' = true.
  56  ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
  57  astfe_id fe' b t.
  58  intros 8;
  59  unfold env_to_flatEnv_inv;
  60  elim a 0;
  61  intros 5;
  62  lapply (ASTFE_ID fe' a1 ?);
  63  [ apply (leflatenv_to_check fe fe' a1 dimLe H)
  64  | rewrite > (leflatenv_to_get fe fe' a1 dimLe H);
  65    apply Hletin
  66  ].
  67 qed.
  68
  69 (*
  70  AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  71  AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  72  AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  73
  74  AST_EXPR_NEG: ∀t:ast_base_type.
  75                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  76  AST_EXPR_NOT: ∀t:ast_base_type.
  77                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  78  AST_EXPR_COM: ∀t:ast_base_type.
  79                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  80
  81  AST_EXPR_ADD: ∀t:ast_base_type.
  82                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  83  AST_EXPR_SUB: ∀t:ast_base_type.
  84                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  85  AST_EXPR_MUL: ∀t:ast_base_type.
  86                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  87  AST_EXPR_DIV: ∀t:ast_base_type.
  88                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  89  AST_EXPR_SHR: ∀t:ast_base_type.
  90                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
  91  AST_EXPR_SHL: ∀t:ast_base_type.
  92                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
  93
  94  AST_EXPR_GT : ∀t:ast_base_type.
  95                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  96  AST_EXPR_GTE: ∀t:ast_base_type.
  97                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  98  AST_EXPR_LT : ∀t:ast_base_type.
  99                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 100  AST_EXPR_LTE: ∀t:ast_base_type.
 101                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 102  AST_EXPR_EQ : ∀t:ast_base_type.
 103                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 104  AST_EXPR_NEQ: ∀t:ast_base_type.
 105                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 106
 107  AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 108  AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 109  AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 110  AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 111  AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 112  AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 113
 114  AST_EXPR_ID: ∀b:bool.∀t:ast_type.
 115               ast_var e b t → ast_expr e t
 116 *)
 117 let rec ast_to_astfe_expr e t (ast:ast_expr e t)
 118                           d (m:aux_map_type d) fe fe'
 119                           (dimInv:env_to_flatEnv_inv d e m fe')
 120                           (dimLe:le_flatEnv fe fe' = true)
 121                           (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
 122  match ast
 123   return λW.λa:ast_expr e W.astfe_expr fe' W
 124  with
 125   [ AST_EXPR_BYTE8 val ⇒
 126    ASTFE_EXPR_BYTE8 fe' val
 127   | AST_EXPR_WORD16 val ⇒
 128    ASTFE_EXPR_WORD16 fe' val
 129   | AST_EXPR_WORD32 val ⇒
 130    ASTFE_EXPR_WORD32 fe' val
 131
 132   | AST_EXPR_NEG bType sExpr ⇒
 133    ASTFE_EXPR_NEG fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
 134   | AST_EXPR_NOT bType sExpr ⇒
 135    ASTFE_EXPR_NOT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
 136   | AST_EXPR_COM bType sExpr ⇒
 137    ASTFE_EXPR_COM fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
 138
 139   | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
 140    ASTFE_EXPR_ADD fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 141                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 142   | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
 143    ASTFE_EXPR_SUB fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 144                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 145   | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
 146    ASTFE_EXPR_MUL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 147                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 148   | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
 149    ASTFE_EXPR_DIV fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 150                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 151   | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
 152    ASTFE_EXPR_SHR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 153                             (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
 154   | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
 155    ASTFE_EXPR_SHL fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 156                             (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d m fe fe' dimInv dimLe emfe)
 157
 158   | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
 159    ASTFE_EXPR_GT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 160                            (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 161   | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
 162    ASTFE_EXPR_GTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 163                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 164   | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
 165    ASTFE_EXPR_LT fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 166                            (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 167   | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
 168    ASTFE_EXPR_LTE fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 169                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 170   | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
 171    ASTFE_EXPR_EQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 172                            (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 173   | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 174    ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr1 d m fe fe' dimInv dimLe emfe)
 175                             (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr2 d m fe fe' dimInv dimLe emfe)
 176
 177   | AST_EXPR_B8toW16 sExpr ⇒
 178    ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
 179   | AST_EXPR_B8toW32 sExpr ⇒
 180    ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d m fe fe' dimInv dimLe emfe)
 181   | AST_EXPR_W16toB8 sExpr ⇒
 182    ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
 183   | AST_EXPR_W16toW32 sExpr ⇒
 184    ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d m fe fe' dimInv dimLe emfe)
 185   | AST_EXPR_W32toB8 sExpr ⇒
 186    ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
 187   | AST_EXPR_W32toW16 sExpr ⇒
 188    ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d m fe fe' dimInv dimLe emfe)
 189
 190   | AST_EXPR_ID b sType var ⇒
 191    ASTFE_EXPR_ID fe' b sType (ast_to_astfe_var e b sType var d m fe fe' dimInv dimLe emfe)
 192
 193   ]
 194 (*
 195  AST_VAR_ID: ∀b:bool.∀t:ast_type.
 196              ast_id e b t → ast_var e b t
 197  AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
 198                 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
 199  AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
 200                  ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
 201 *)
 202 and ast_to_astfe_var e b t (ast:ast_var e b t)
 203                      d (m:aux_map_type d) fe fe'
 204                      (dimInv:env_to_flatEnv_inv d e m fe')
 205                      (dimLe:le_flatEnv fe fe' = true)
 206                      (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
 207  match ast
 208   return λW,X.λa:ast_var e W X.astfe_var fe' W X
 209  with
 210   [ AST_VAR_ID sB sType sId ⇒
 211    ASTFE_VAR_ID fe' sB sType (ast_to_astfe_id e sB sType sId d m fe fe' dimInv dimLe emfe)
 212
 213   | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 214    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)
 215                                      (ast_to_astfe_base_expr e sExpr d m fe fe' dimInv dimLe emfe)
 216
 217   | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
 218    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)
 219   ]
 220 (*
 221  AST_BASE_EXPR: ∀t:ast_base_type.
 222                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
 223 *)
 224 and ast_to_astfe_base_expr e (ast:ast_base_expr e)
 225                            d (m:aux_map_type d) fe fe'
 226                            (dimInv:env_to_flatEnv_inv d e m fe')
 227                            (dimLe:le_flatEnv fe fe' = true)
 228                            (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝
 229  match ast
 230   return λa:ast_base_expr e.astfe_base_expr fe'
 231  with
 232   [ AST_BASE_EXPR bType sExpr ⇒
 233    ASTFE_BASE_EXPR fe' bType (ast_to_astfe_expr e (AST_TYPE_BASE bType) sExpr d m fe fe' dimInv dimLe emfe)
 234   ].
 235
 236 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
 237                                  d e (m:aux_map_type d) fe'
 238                                  (dimInv:env_to_flatEnv_inv d e m fe')
 239                                  (dimLe:le_flatEnv fe fe' = true)
 240                                  (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_expr fe' t ≝
 241  match ast
 242   return λW.λa:astfe_expr fe W.astfe_expr fe' W
 243  with
 244   [ ASTFE_EXPR_BYTE8 val ⇒
 245    ASTFE_EXPR_BYTE8 fe' val
 246   | ASTFE_EXPR_WORD16 val ⇒
 247    ASTFE_EXPR_WORD16 fe' val
 248   | ASTFE_EXPR_WORD32 val ⇒
 249    ASTFE_EXPR_WORD32 fe' val
 250
 251   | ASTFE_EXPR_NEG bType sExpr ⇒
 252    ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
 253   | ASTFE_EXPR_NOT bType sExpr ⇒
 254    ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
 255   | ASTFE_EXPR_COM bType sExpr ⇒
 256    ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
 257
 258   | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
 259    ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 260                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 261   | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
 262    ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 263                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 264   | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
 265    ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 266                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 267   | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
 268    ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 269                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 270   | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
 271    ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 272                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
 273   | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
 274    ASTFE_EXPR_SHL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 275                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe emfe)
 276
 277   | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
 278    ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 279                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 280   | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
 281    ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 282                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 283   | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
 284    ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 285                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 286   | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
 287    ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 288                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 289   | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
 290    ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 291                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 292   | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 293    ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe emfe)
 294                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe emfe)
 295
 296   | ASTFE_EXPR_B8toW16 sExpr ⇒
 297    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)
 298   | ASTFE_EXPR_B8toW32 sExpr ⇒
 299    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)
 300   | ASTFE_EXPR_W16toB8 sExpr ⇒
 301    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)
 302   | ASTFE_EXPR_W16toW32 sExpr ⇒
 303    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)
 304   | ASTFE_EXPR_W32toB8 sExpr ⇒
 305    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)
 306   | ASTFE_EXPR_W32toW16 sExpr ⇒
 307    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)
 308
 309   | ASTFE_EXPR_ID b sType var ⇒
 310    ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe emfe)
 311
 312   ]
 313 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
 314                             d e (m:aux_map_type d) fe'
 315                             (dimInv:env_to_flatEnv_inv d e m fe')
 316                             (dimLe:le_flatEnv fe fe' = true)
 317                             (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_var fe' b t ≝
 318  match ast
 319   return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
 320  with
 321   [ ASTFE_VAR_ID sB sType sId ⇒
 322    ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe)
 323
 324   | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 325    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)
 326                                      (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
 327
 328   | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
 329    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)
 330   ]
 331 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
 332                                   d e (m:aux_map_type d) fe'
 333                                   (dimInv:env_to_flatEnv_inv d e m fe')
 334                                   (dimLe:le_flatEnv fe fe' = true)
 335                                   (emfe:env_map_flatEnv d e m fe fe' dimInv dimLe) on ast : astfe_base_expr fe' ≝
 336  match ast
 337   return λa:astfe_base_expr fe.astfe_base_expr fe'
 338  with
 339   [ ASTFE_BASE_EXPR bType sExpr ⇒
 340    ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe emfe)
 341   ].
 342
 343 (*
 344  AST_INIT_VAR: ∀b:bool.∀t:ast_type.
 345                ast_var e b t → ast_init e t
 346  AST_INIT_VAL: ∀t:ast_type.
 347                aux_ast_init_type t → ast_init e t
 348 *)
 349 definition ast_to_astfe_init ≝
 350 λe,t.λast:ast_init e t.
 351 λd.λm:aux_map_type d.λfe,fe'.
 352 λdimInv:env_to_flatEnv_inv d e m fe'.
 353 λdimLe:le_flatEnv fe fe' = true.
 354 λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
 355  match ast
 356   return λW.λa:ast_init e W.astfe_init fe' W
 357  with
 358   [ AST_INIT_VAR sB sType sVar ⇒
 359    ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_var e sB sType sVar d m fe fe' dimInv dimLe emfe)
 360
 361   | AST_INIT_VAL sType sArgs ⇒
 362    ASTFE_INIT_VAL fe' sType sArgs
 363
 364   ].
 365
 366 definition ast_to_astfe_retype_init ≝
 367 λfe,t.λast:astfe_init fe t.
 368 λd.λe.λm:aux_map_type d.λfe'.
 369 λdimInv:env_to_flatEnv_inv d e m fe'.
 370 λdimLe:le_flatEnv fe fe' = true.
 371 λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
 372  match ast
 373   return λW.λa:astfe_init fe W.astfe_init fe' W
 374  with
 375   [ ASTFE_INIT_VAR sB sType sVar ⇒
 376    ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe emfe)
 377
 378   | ASTFE_INIT_VAL sType sArgs ⇒
 379    ASTFE_INIT_VAL fe' sType sArgs
 380
 381   ].
 382
 383 (*
 384  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
 385               ast_var e false t → ast_expr e t → ast_stm e
 386  AST_STM_WHILE: ∀e:aux_env_type.
 387                 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
 388  AST_STM_IF: ∀e:aux_env_type.
 389              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
 390 *)
 391 (*lemma ast_to_astfe_stm_aux :
 392  ∀d,e.∀m:aux_map_type d.∀fe,fe',dimInv,dimLe.
 393  ∀emfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
 394  ∀ast:astfe_stm fe'.
 395   (ΣD.(ΣE.(ΣM.(ΣFE.(ΣFE'.(ΣDIMINV.(ΣDIMLE.Prod (env_map_flatEnv D E M FE FE' DIMINV DIMLE) (astfe_stm FE')))))))).
 396  elim daemon.
 397 qed.*)
 398 inductive ast_to_astfe_stm_res (d:nat) : Type ≝
 399 AST_TO_ASTFE_STM_RES:
 400  ∀e.∀m:aux_map_type d.∀fe,fe'.
 401  ∀dimInv:env_to_flatEnv_inv d e m fe'.
 402  ∀dimLe:le_flatEnv fe fe' = true.
 403  ∀trsf:Prod3T aux_str_type bool ast_type.
 404  env_map_flatEnv d e m fe fe' dimInv dimLe → astfe_stm fe' → ast_to_astfe_stm_res d.
 405
 406 let rec ast_to_astfe_stm e (ast:ast_stm e) on ast ≝
 407  match ast
 408   return λX.λast:ast_stm X.
 409          Πd.Πm:aux_map_type d.Πfe.Πfe'.ΠdimInv:env_to_flatEnv_inv d X m fe'.
 410          ΠdimLe:le_flatEnv fe fe' = true.env_map_flatEnv d X m fe fe' dimInv dimLe →
 411          ast_to_astfe_stm_res d
 412  with
 413   [ AST_STM_ASG sE sType sVar sExpr ⇒
 414    λd.λm:aux_map_type d.λfe,fe'.λdimInv:env_to_flatEnv_inv d sE m fe'.
 415    λdimLe:le_flatEnv fe fe' = true.λemfe:env_map_flatEnv d sE m fe fe' dimInv dimLe.
 416    AST_TO_ASTFE_STM_RES d sE m fe fe' dimInv dimLe emfe []
 417                         (ASTFE_STM_ASG fe' sType (ast_to_astfe_var sE false sType sVar d m fe fe' dimInv dimLe emfe)
 418                                                  (ast_to_astfe_expr sE sType sExpr d m fe fe' dimInv dimLe emfe))
 419
 420   | _ ⇒ False_rect ? daemon
 421
 422   ].
 423
 424
 425
 426 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
 427  : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
 428  match ast
 429   return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 430  with
 431   [ AST_STM_ASG e' subType var expr ⇒
 432    λmap:aux_trasfMap_type e' fe.
 433     opt_map ?? (ast_to_astfe_var e' false subType var fe map)
 434      (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
 435       (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
 436
 437   | AST_STM_WHILE e' expr decl ⇒
 438    λmap:aux_trasfMap_type e' fe.
 439     opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
 440      (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
 441       (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 442        [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 443         [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
 444          [ pair map' resDecl ⇒
 445           match le_flatEnv fe fe'
 446            return λx.(le_flatEnv fe fe' = x) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 447           with
 448            [ true ⇒ λp:(le_flatEnv fe fe' = true).
 449                      opt_map ?? (retype_base_expr fe resExpr fe' p)
 450                       (λresExpr'.Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
 451                                                     (ASTFE_STM_WHILE fe' resExpr' (ASTFE_BODY fe' resDecl))≫))
 452           | false ⇒ λp:(le_flatEnv fe fe' = false).None ?
 453           ] (refl_eq ? (le_flatEnv fe fe'))
 454          ]]]))
 455
 456   | AST_STM_IF e' nelExprDecl optDecl ⇒
 457    λmap:aux_trasfMap_type e' fe.
 458     let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
 459                 (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
 460      match nel with
 461       [ ne_nil h ⇒
 462        opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
 463         (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
 464          (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 465           [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 466            [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
 467             [ pair m' resDecl ⇒
 468              match le_flatEnv fenv fenv'
 469               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'))))
 470              with
 471               [ true ⇒ λp:(le_flatEnv fenv fenv' = true).
 472                opt_map ?? (retype_base_Expr fenv resExpr fenv' p)
 473                 (λresExpr'.Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
 474                                                    «£(pair ?? resExpr' (ASTFE_BODY fenv' resDecl))»≫))
 475               | false ⇒ λp:(le_flatEnv fenv fenv' = false).None ?
 476               ] (refl_eq ? (le_flatEnv fenv fenv'))
 477             ]]]))
 478
 479       | ne_cons h tl ⇒
 480        opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
 481         (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
 482          (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 483           [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 484            [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
 485             [ pair m' resDecl ⇒
 486              opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
 487               (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
 488                [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
 489                 [ pair m'' tl' ⇒
 490                  match le_flatEnv fenv fenv''
 491                   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'))))
 492                  with
 493                   [ true ⇒ λp:(le_flatEnv fenv fenv'' = true).
 494                    match le_flatEnv fenv' fenv''
 495                     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'))))
 496                    with
 497                     [ true ⇒ λp':(le_flatEnv fenv' fenv'' = true).
 498                      opt_map ?? (retype_base_expr fenv resExpr fenv'' p)
 499                       (λresExpr'.opt_map ?? (retype_stm_list fenv' resDecl fenv'' p')
 500                        (λresDecl'.
 501                  Some ? (≪fenv'',pair ?? m''
 502                                           («£(pair ?? resExpr'
 503                                                      (ASTFE_BODY fenv'' resDecl'))»&tl')≫)))
 504                     | false ⇒ λp':(le_flatEnv fenv' fenv'' = false).None ?
 505                     ] (refl_eq ? (le_flatEnv fenv' fenv''))
 506                   | false ⇒ λp:(le_flatEnv fenv fenv'' = false).None ?
 507                   ] (refl_eq ? (le_flatEnv fenv fenv''))
 508                 ]])]]]))
 509       ] in
 510     opt_map ?? (aux fe map nelExprDecl)
 511      (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
 512       [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
 513        [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
 514         [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
 515         | Some decl ⇒
 516          opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
 517           (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
 518            [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 519             [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
 520              [ pair (m'':aux_trasfMap_type ((build_trasfEnv f) (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
 521               match le_flatEnv fe' fe''
 522                return λz.(le_flatEnv fe' fe'' = z) → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 523               with
 524                [ true ⇒ λp'':(le_flatEnv fe' fe'' = true).
 525                 opt_map ?? (retype_exprAndBody_neList fe' resNel fe'' p'')
 526                  (λresNel'.Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 527                             (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
 528                                             (ASTFE_STM_IF fe'' resNel' (Some ? (ASTFE_BODY fe'' resDecl)))≫))
 529                | false ⇒ λp'':(le_flatEnv fe' fe'' = false).None ?
 530                ] (refl_eq ? (le_flatEnv fe' fe''))
 531              ]]])]]])
 532   ]
 533 (*
 534  AST_NO_DECL: ∀e:aux_env_type.
 535               list (ast_stm e) → ast_decl e
 536  AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
 537            (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
 538 *)
 539 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
 540  : Π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')))) ≝
 541  match ast
 542   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'))))
 543  with
 544   [ AST_NO_DECL e' lStm ⇒
 545    λmap:aux_trasfMap_type e' fe.
 546     let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
 547      : option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ≝
 548      match ll with
 549       [ nil ⇒ let trsf ≝ []
 550               in Some ? ≪trsf,≪fenv,pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fenv)
 551                                            (list (astfe_stm fenv))
 552                                            (retype_map_to_id e' fenv (build_trasfEnv trsf) m (refl_eq ? e')) []≫≫
 553
 554       | cons h tl ⇒
 555        opt_map ?? (ast_to_astfe_stm e' h fenv m)
 556         (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
 557          [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
 558           [ pair m' resStm ⇒
 559            opt_map ?? (aux tl fenv' m')
 560             (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))).match sigmaRes' with
 561              [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
 562               [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type ((build_trasfEnv f) e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
 563                [ pair m'' tl' ⇒
 564                 match le_flatEnv fenv' fenv''
 565                  return λx.(le_flatEnv fenv' fenv'' = x) → option (Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) e') fe') (list (astfe_stm fe'))))
 566                 with
 567                  [ true ⇒ λp:(le_flatEnv fenv' fenv'' = true).
 568                   opt_map ?? (retype_stm_list fenv' [resStm] fenv'' p)
 569                    (λresStm'.Some ? ≪f,≪fenv'',pair (aux_trasfMap_type ((build_trasfEnv f) e') fenv'')
 570                                                       (list (astfe_stm fenv''))
 571                                                       m''
 572                                                       (resStm'@tl')≫≫)
 573                  | false ⇒ λp:(le_flatEnv fenv' fenv'' = false).None ?
 574                  ] (refl_eq ? (le_flatEnv fenv' fenv''))
 575                ]]])]])] in
 576     aux lStm fe map
 577
 578   | AST_DECL e' b name t dim optInit subDecl ⇒
 579    λmap:aux_trasfMap_type e' fe.
 580     opt_map ?? (match optInit with
 581                 [ None ⇒ Some ? []
 582                 | Some init ⇒
 583                  opt_map ?? (ast_to_astfe_init e' t init fe map)
 584                   (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
 585                                                               (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 586                                                                         (next_nameId e' fe map name)
 587                                                                         (ast_to_astfe_dec_aux e' name b t fe map dim))
 588                                                               b t)
 589                    (λresId.opt_map ?? (retype_init fe t resInit (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 590                                                    (adddescflatenv_to_leflatenv fe (next_nameId e' fe map name) b t))
 591                     (λresInit'.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t) b t resId resInit' ]))))
 592                 ])
 593      (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
 594                                           (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 595                                           (add_maxcur_map e' fe map map name b t))
 596       (λ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
 597        [ 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
 598         [ 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
 599          [ pair (map':aux_trasfMap_type ((build_trasfEnv f) (add_desc_env e' name b t)) fe') tRes ⇒
 600           match le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'
 601            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'))))
 602           with
 603            [ true ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = true).
 604             opt_map ?? (retype_stm_list (add_desc_flatEnv fe (next_nameId e' fe map name) b t) hRes fe' p)
 605              (λhRes'.let trsf ≝ [ tripleT ??? name b t ]@f
 606                      in Some ? ≪trsf,≪fe',pair (aux_trasfMap_type ((build_trasfEnv trsf) e') fe')
 607                                                  (list (astfe_stm fe'))
 608                                                  map'
 609                                                  (hRes'@tRes)≫≫)
 610            | false ⇒ λp:(le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' = false).None ?
 611            ] (refl_eq ? (le_flatEnv (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe'))
 612          ]]]))
 613   ].
 614
 615 (*
 616  AST_ROOT: ast_decl empty_env → ast_root.
 617 *)
 618 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
 619 λast:ast_root.match ast with
 620  [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
 621   (* impossibile: dummy *)
 622   [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
 623   | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
 624    [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 625     [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type ((build_trasfEnv f) empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
 626      [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
 627      ]]]]].
 628
 629 (* mini test
 630 include "compiler/preast_tree.ma".
 631 include "compiler/preast_to_ast.ma".
 632
 633 { const byte8 a;
 634   const byte8[3] b={0,1,2};
 635   byte8[3] c=b;
 636
 637   if(0xF0)
 638    { byte8 a=a; }
 639   else if(0xF1)
 640    {
 641    while(0x10)
 642     { byte8[3] b=c; }
 643    }
 644   else if(0xF2)
 645    { byte8 a=b[0]; }
 646   else
 647    { const byte8 a=a; }
 648 }
 649
 650 definition prova ≝
 651 PREAST_ROOT (
 652  PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
 653   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〉)»))) (
 654    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]))) (
 655     PREAST_NO_DECL [
 656      PREAST_STM_IF «
 657        (pair ??
 658        (PREAST_EXPR_BYTE8 〈xF,x0〉)
 659        (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
 660        )
 661      ; (pair ??
 662        (PREAST_EXPR_BYTE8 〈xF,x1〉)
 663        (PREAST_NO_DECL [
 664         (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
 665         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 [])
 666         ))
 667        ])
 668        )
 669      £ (pair ??
 670        (PREAST_EXPR_BYTE8 〈xF,x2〉)
 671        (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 []))
 672        )
 673      » (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 [])))
 674     ]
 675    )
 676   )
 677  )
 678 ).
 679 *)
 680
 681
 682
 683
 684
 685
 686
 687
 688
 689
 690
 691
 692 (*
 693  ASTFE_STM_ASG: ∀t:ast_type.
 694                 astfe_var e false t → astfe_expr e t → astfe_stm e
 695  ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
 696                  astfe_id e b t → astfe_init e t → astfe_stm e
 697  ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
 698  ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
 699 *)
 700 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' ≝
 701  match ast with
 702   [ ASTFE_STM_ASG sType sVar sExpr ⇒
 703    ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe emfe)
 704                            (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe emfe)
 705
 706   | ASTFE_STM_INIT sB sType sId sInit ⇒
 707    ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe emfe)
 708                                (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe emfe)
 709
 710   | ASTFE_STM_WHILE sExpr sBody ⇒
 711    ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe emfe)
 712                        (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe)
 713
 714   | ASTFE_STM_IF sNelExprBody sOptBody ⇒
 715    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)
 716                                                                               (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
 717                                                                               )»&t)
 718                                                              «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 719                                                              sNelExprBody))
 720                     (opt_map ?? sOptBody
 721                       (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe emfe)))
 722   ]
 723 (*
 724  ASTFE_BODY: list (astfe_stm e) → astfe_body e
 725 *)
 726 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' ≝
 727  match ast with
 728   [ ASTFE_BODY sLStm ⇒
 729    ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe ]@t) [] sLStm)
 730   ].
 731
 732 definition ast_to_astfe_retype_stm_list ≝
 733 λfe.λast:list (astfe_stm fe).λd,e,m,fe',dimInv,dimLe.λemfe:env_map_flatEnv d e m fe fe' dimInv dimLe.
 734  fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe emfe]@t) [] ast.
 735
 736 definition ast_to_astfe_retype_exprBody_neList ≝
 737 λ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.
 738  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)
 739                                                           (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe emfe)
 740                                                           )»&t)
 741                                          «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 742                                          ast).
 743
 744
 745
 746
 747
 748
 749