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