helm/software/matita/contribs/assembly/compiler/ast_to_astfe.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_tree.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 d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str)))
  32 *)
  33 lemma ast_to_astfe_id :
  34  ∀d.∀e:aux_env_type d.∀b,t.∀ast:ast_id d e b t.
  35  ∀m:aux_map_type d.∀fe.
  36  ∀dimInv:env_to_flatEnv_inv d e m fe.
  37  astfe_id fe b t.
  38  intros 7;
  39  unfold env_to_flatEnv_inv;
  40  elim a 0;
  41  intros 3;
  42  lapply (ASTFE_ID fe (STR_ID a1 (get_id_map d m a1)) ?);
  43  [ apply (proj2 ?? (proj1 ?? (H1 a1 H)))
  44  | rewrite > (proj2 ?? (H1 a1 H));
  45    apply Hletin
  46  ].
  47 qed.
  48
  49 lemma ast_to_astfe_retype_id :
  50  ∀fe,b,t.∀ast:astfe_id fe b t.
  51  ∀d.∀e:aux_env_type d.∀m:aux_map_type d.∀fe'.
  52  ∀dimInv:env_to_flatEnv_inv d e m fe'.
  53  ∀dimLe:le_flatEnv fe fe' = true.
  54  astfe_id fe' b t.
  55  intros 8;
  56  unfold env_to_flatEnv_inv;
  57  elim a 0;
  58  intros 4;
  59  lapply (ASTFE_ID fe' a1 ?);
  60  [ apply (leflatenv_to_check fe fe' a1 H2 H)
  61  | rewrite > (leflatenv_to_get fe fe' a1 H2 H);
  62    apply Hletin
  63  ].
  64 qed.
  65
  66 (*
  67   AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  68 | AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  69 | AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  70
  71 | AST_EXPR_NEG: ∀t:ast_base_type.
  72                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  73 | AST_EXPR_NOT: ∀t:ast_base_type.
  74                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  75 | AST_EXPR_COM: ∀t:ast_base_type.
  76                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  77
  78 | AST_EXPR_ADD: ∀t:ast_base_type.
  79                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  80 | AST_EXPR_SUB: ∀t:ast_base_type.
  81                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  82 | AST_EXPR_MUL: ∀t:ast_base_type.
  83                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  84 | AST_EXPR_DIV: ∀t:ast_base_type.
  85                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  86 | AST_EXPR_SHR: ∀t:ast_base_type.
  87                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
  88 | AST_EXPR_SHL: ∀t:ast_base_type.
  89                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
  90 | AST_EXPR_AND: ∀t:ast_base_type.
  91                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  92 | AST_EXPR_OR:  ∀t:ast_base_type.
  93                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  94 | AST_EXPR_XOR: ∀t:ast_base_type.
  95                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
  96
  97 | AST_EXPR_GT : ∀t:ast_base_type.
  98                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  99 | AST_EXPR_GTE: ∀t:ast_base_type.
 100                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 101 | AST_EXPR_LT : ∀t:ast_base_type.
 102                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 103 | AST_EXPR_LTE: ∀t:ast_base_type.
 104                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 105 | AST_EXPR_EQ : ∀t:ast_base_type.
 106                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 107 | AST_EXPR_NEQ: ∀t:ast_base_type.
 108                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 109
 110 | AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 111 | AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 112 | AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 113 | AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 114 | AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 115 | AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 116
 117 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
 118                ast_var d e b t → ast_expr d e t
 119 *)
 120 let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
 121                           (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
 122  match ast
 123   return λW.λa:ast_expr d 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 d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 134   | AST_EXPR_NOT bType sExpr ⇒
 135    ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 136   | AST_EXPR_COM bType sExpr ⇒
 137    ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 138
 139   | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
 140    ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 141                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 142   | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
 143    ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 144                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 145   | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
 146    ASTFE_EXPR_MUL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 147                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 148   | AST_EXPR_DIV bType sExpr1 sExpr2 ⇒
 149    ASTFE_EXPR_DIV fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 150                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 151   | AST_EXPR_SHR bType sExpr1 sExpr2 ⇒
 152    ASTFE_EXPR_SHR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 153                            (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
 154   | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
 155    ASTFE_EXPR_SHL fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 156                            (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
 157   | AST_EXPR_AND bType sExpr1 sExpr2 ⇒
 158    ASTFE_EXPR_AND fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 159                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 160   | AST_EXPR_OR bType sExpr1 sExpr2 ⇒
 161    ASTFE_EXPR_OR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 162                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 163   | AST_EXPR_XOR bType sExpr1 sExpr2 ⇒
 164    ASTFE_EXPR_XOR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 165                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 166
 167   | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
 168    ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 169                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 170   | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
 171    ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 172                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 173   | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
 174    ASTFE_EXPR_LT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 175                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 176   | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
 177    ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 178                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 179   | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
 180    ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 181                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 182   | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 183    ASTFE_EXPR_NEQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 184                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 185
 186   | AST_EXPR_B8toW16 sExpr ⇒
 187    ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
 188   | AST_EXPR_B8toW32 sExpr ⇒
 189    ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
 190   | AST_EXPR_W16toB8 sExpr ⇒
 191    ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
 192   | AST_EXPR_W16toW32 sExpr ⇒
 193    ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
 194   | AST_EXPR_W32toB8 sExpr ⇒
 195    ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
 196   | AST_EXPR_W32toW16 sExpr ⇒
 197    ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
 198
 199   | AST_EXPR_ID b sType var ⇒
 200    ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
 201
 202   ]
 203 (*
 204   AST_VAR_ID: ∀b:bool.∀t:ast_type.
 205               ast_id d e b t → ast_var d e b t
 206 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
 207                  ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
 208 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
 209                   ast_var d e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n)
 210 *)
 211 and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
 212                      (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
 213  match ast
 214   return λW,X.λa:ast_var d e W X.astfe_var fe W X
 215  with
 216   [ AST_VAR_ID sB sType sId ⇒
 217    ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
 218
 219   | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 220    ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
 221                                     (ast_to_astfe_base_expr d e sExpr m fe dimInv)
 222
 223   | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
 224    ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)
 225   ]
 226 (*
 227   AST_BASE_EXPR: ∀t:ast_base_type.
 228                  ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e
 229
 230 *)
 231 and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
 232                            (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
 233  match ast
 234   return λa:ast_base_expr d e.astfe_base_expr fe
 235  with
 236   [ AST_BASE_EXPR bType sExpr ⇒
 237    ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 238   ].
 239
 240 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
 241                                  d (e:aux_env_type d) (m:aux_map_type d) fe'
 242                                  (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
 243  match ast
 244   return λW.λa:astfe_expr fe W.astfe_expr fe' W
 245  with
 246   [ ASTFE_EXPR_BYTE8 val ⇒
 247    ASTFE_EXPR_BYTE8 fe' val
 248   | ASTFE_EXPR_WORD16 val ⇒
 249    ASTFE_EXPR_WORD16 fe' val
 250   | ASTFE_EXPR_WORD32 val ⇒
 251    ASTFE_EXPR_WORD32 fe' val
 252
 253   | ASTFE_EXPR_NEG bType sExpr ⇒
 254    ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 255   | ASTFE_EXPR_NOT bType sExpr ⇒
 256    ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 257   | ASTFE_EXPR_COM bType sExpr ⇒
 258    ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 259
 260   | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
 261    ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 262                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 263   | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
 264    ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 265                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 266   | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
 267    ASTFE_EXPR_MUL 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_DIV bType sExpr1 sExpr2 ⇒
 270    ASTFE_EXPR_DIV 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_SHR bType sExpr1 sExpr2 ⇒
 273    ASTFE_EXPR_SHR 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 AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
 275   | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
 276    ASTFE_EXPR_SHL 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 AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
 278   | ASTFE_EXPR_AND bType sExpr1 sExpr2 ⇒
 279    ASTFE_EXPR_AND 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_OR bType sExpr1 sExpr2 ⇒
 282    ASTFE_EXPR_OR 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   | ASTFE_EXPR_XOR bType sExpr1 sExpr2 ⇒
 285    ASTFE_EXPR_XOR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 286                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 287
 288   | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
 289    ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 290                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 291   | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
 292    ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 293                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 294   | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
 295    ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 296                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 297   | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
 298    ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 299                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 300   | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
 301    ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 302                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 303   | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 304    ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 305                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 306
 307   | ASTFE_EXPR_B8toW16 sExpr ⇒
 308    ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
 309   | ASTFE_EXPR_B8toW32 sExpr ⇒
 310    ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
 311   | ASTFE_EXPR_W16toB8 sExpr ⇒
 312    ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
 313   | ASTFE_EXPR_W16toW32 sExpr ⇒
 314    ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
 315   | ASTFE_EXPR_W32toB8 sExpr ⇒
 316    ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
 317   | ASTFE_EXPR_W32toW16 sExpr ⇒
 318    ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
 319
 320   | ASTFE_EXPR_ID b sType var ⇒
 321    ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
 322
 323   ]
 324 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
 325                             d (e:aux_env_type d) (m:aux_map_type d) fe'
 326                             (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
 327  match ast
 328   return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
 329  with
 330   [ ASTFE_VAR_ID sB sType sId ⇒
 331    ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
 332
 333   | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 334    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)
 335                                      (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
 336
 337   | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
 338    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)
 339   ]
 340 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
 341                                   d (e:aux_env_type d) (m:aux_map_type d) fe'
 342                                   (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
 343  match ast
 344   return λa:astfe_base_expr fe.astfe_base_expr fe'
 345  with
 346   [ ASTFE_BASE_EXPR bType sExpr ⇒
 347    ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 348   ].
 349
 350 (*
 351   AST_INIT_VAR: ∀b:bool.∀t:ast_type.
 352                 ast_var d e b t → ast_init d e t
 353 | AST_INIT_VAL: ∀t:ast_type.
 354                 aux_ast_init_type t → ast_init d e t
 355 *)
 356 definition ast_to_astfe_init ≝
 357 λd.λe:aux_env_type d.λt.λast:ast_init d e t.
 358 λm:aux_map_type d.λfe.
 359 λdimInv:env_to_flatEnv_inv d e m fe.
 360  match ast
 361   return λW.λa:ast_init d e W.astfe_init fe W
 362  with
 363   [ AST_INIT_VAR sB sType sVar ⇒
 364    ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
 365
 366   | AST_INIT_VAL sType sArgs ⇒
 367    ASTFE_INIT_VAL fe sType sArgs
 368
 369   ].
 370
 371 definition ast_to_astfe_retype_init ≝
 372 λfe,t.λast:astfe_init fe t.
 373 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 374 λdimInv:env_to_flatEnv_inv d e m fe'.
 375 λdimLe:le_flatEnv fe fe' = true.
 376  match ast
 377   return λW.λa:astfe_init fe W.astfe_init fe' W
 378  with
 379   [ ASTFE_INIT_VAR sB sType sVar ⇒
 380    ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
 381
 382   | ASTFE_INIT_VAL sType sArgs ⇒
 383    ASTFE_INIT_VAL fe' sType sArgs
 384
 385   ].
 386
 387 (*
 388   ASTFE_STM_ASG: ∀t:ast_type.
 389                  astfe_var e false t → astfe_expr e t → astfe_stm e
 390 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
 391                   astfe_id e b t → astfe_init e t → astfe_stm e
 392 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
 393 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
 394 *)
 395 let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe)
 396                                 d (e:aux_env_type d) (m:aux_map_type d) fe'
 397                                 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝
 398  match ast with
 399   [ ASTFE_STM_ASG sType sVar sExpr ⇒
 400    ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
 401                            (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
 402
 403   | ASTFE_STM_INIT sB sType sId sInit ⇒
 404    ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
 405                                (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
 406
 407   | ASTFE_STM_WHILE sExpr sBody ⇒
 408    ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
 409                        (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
 410
 411   | ASTFE_STM_IF sNelExprBody sOptBody ⇒
 412    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)
 413                                                                               (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
 414                                                                               )»&t)
 415                                                              «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 416                                                              sNelExprBody))
 417                     (opt_map ?? sOptBody
 418                       (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
 419   ]
 420 (*
 421   ASTFE_BODY: list (astfe_stm e) → astfe_body e
 422 *)
 423 and ast_to_astfe_retype_body fe (ast:astfe_body fe)
 424                              d (e:aux_env_type d) (m:aux_map_type d) fe'
 425                              (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_body fe' ≝
 426  match ast with
 427   [ ASTFE_BODY sLStm ⇒
 428    ASTFE_BODY fe' (fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] sLStm)
 429   ].
 430
 431 definition ast_to_astfe_retype_stm_list ≝
 432 λfe.λast:list (astfe_stm fe).
 433 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 434 λdimInv:env_to_flatEnv_inv d e m fe'.
 435 λdimLe:le_flatEnv fe fe' = true.
 436  fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
 437
 438 definition ast_to_astfe_retype_exprBody_neList ≝
 439 λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).
 440 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 441 λdimInv:env_to_flatEnv_inv d e m fe'.
 442 λdimLe:le_flatEnv fe fe' = true.
 443  cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
 444                                                           (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
 445                                                           )»&t)
 446                                          «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 447                                          ast).
 448
 449 (* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
 450 inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 451 AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
 452                          env_to_flatEnv_inv d e m fe' →
 453                          le_flatEnv fe fe' = true →
 454                          astfe_stm fe' →
 455                          ast_to_astfe_stm_record d e fe.
 456
 457 inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 458 AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
 459                         env_to_flatEnv_inv d e m fe' →
 460                         le_flatEnv fe fe' = true →
 461                         ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
 462                         ast_to_astfe_if_record d e fe.
 463
 464 inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 465 AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
 466                           env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
 467                           le_flatEnv fe fe' = true →
 468                           list (astfe_stm fe') →
 469                           ast_to_astfe_decl_record d e fe.
 470
 471 inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 472 AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
 473                               env_to_flatEnv_inv d e m fe' →
 474                               le_flatEnv fe fe' = true →
 475                               list (astfe_stm fe') →
 476                               ast_to_astfe_decl_aux_record d e fe.
 477
 478 (*
 479   AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
 480                ast_var d e false t → ast_expr d e t → ast_stm d e
 481 | AST_STM_WHILE: ∀d.∀e:aux_env_type d.
 482                  ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
 483 | AST_STM_IF: ∀d.∀e:aux_env_type d.
 484               ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
 485 *)
 486 let rec ast_to_astfe_stm d (e:aux_env_type d) (ast:ast_stm d e) on ast : Πm:aux_map_type d.Πfe.
 487                                                                          env_to_flatEnv_inv d e m fe →
 488                                                                          ast_to_astfe_stm_record d e fe ≝
 489  match ast
 490   return λD.λE.λast:ast_stm D E.
 491          Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
 492  with
 493   [ AST_STM_ASG sD sE sType sVar sExpr ⇒
 494    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 495    AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
 496                            (eq_to_leflatenv ?? (refl_eq ??))
 497                            (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv)
 498                                                    (ast_to_astfe_expr sD sE sType sExpr m fe dimInv))
 499   | AST_STM_WHILE sD sE sExpr sDecl ⇒
 500    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 501    match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
 502          (env_map_flatEnv_enter_aux sD sE m fe dimInv) with
 503     [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 504      eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 505              (λenv.ast_to_astfe_stm_record sD env fe)
 506              (AST_TO_ASTFE_STM_RECORD sD
 507                                       (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 508                                       fe
 509                                       (leave_map sD resMap)
 510                                       resFe
 511                                       (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 512                                       resDimLe
 513                                       (ASTFE_STM_WHILE resFe
 514                                                        (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv)
 515                                                                                       sD
 516                                                                                       (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 517                                                                                       (leave_map sD resMap)
 518                                                                                       resFe
 519                                                                                       (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 520                                                                                       resDimLe)
 521                                                        (ASTFE_BODY resFe resLStm)))
 522              sE (leave_add_enter_env sD sE resTrsf) ]
 523
 524   | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
 525    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 526    let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
 527                (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
 528                (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝
 529     match nel with
 530      [ ne_nil h ⇒
 531       match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
 532             (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
 533        [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 534         eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 535                 (λenv.ast_to_astfe_if_record sD env pFe)
 536                 (AST_TO_ASTFE_IF_RECORD sD
 537                                         (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 538                                         pFe
 539                                         (leave_map sD resMap)
 540                                         resFe
 541                                         (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 542                                         resDimLe
 543                                         «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
 544                                                                                   sD
 545                                                                                   (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 546                                                                                   (leave_map sD resMap)
 547                                                                                   resFe
 548                                                                                   (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 549                                                                                   resDimLe)
 550                                                    (ASTFE_BODY resFe resLStm))»)
 551                 sE (leave_add_enter_env sD sE resTrsf) ]
 552
 553      | ne_cons h t ⇒
 554       match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
 555             (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
 556        [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 557         match aux t (leave_map sD resMap) resFe
 558                   (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 559                            (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
 560                            (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 561                            sE (leave_add_enter_env sD sE resTrsf)) with
 562         [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
 563          AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
 564                                 (leflatenv_trans ??? resDimLe resDimLe')
 565                                 («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
 566                                                                            sD sE resMap' resFe' resDimInv'
 567                                                                            (leflatenv_trans ??? resDimLe resDimLe'))
 568                                             (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
 569                                                                       sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
 570
 571      ] in
 572    match aux sExprDecl m fe dimInv with
 573     [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
 574      match sOptDecl with
 575       [ None ⇒
 576        AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
 577
 578       | Some sDecl ⇒
 579        match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe
 580              (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with
 581         [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
 582          eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 583                  (λenv.ast_to_astfe_stm_record sD env fe)
 584                  (AST_TO_ASTFE_STM_RECORD sD
 585                                           (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 586                                           fe
 587                                           (leave_map sD resMap')
 588                                           resFe'
 589                                           (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
 590                                           (leflatenv_trans ??? resDimLe resDimLe')
 591                                           (ASTFE_STM_IF resFe'
 592                                                         (ast_to_astfe_retype_exprBody_neList resFe resExprBody
 593                                                                                              sD
 594                                                                                              (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 595                                                                                              (leave_map sD resMap')
 596                                                                                              resFe'
 597                                                                                              (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
 598                                                                                              resDimLe')
 599                                                         (Some ? (ASTFE_BODY resFe' resLStm))))
 600                  sE (leave_add_enter_env sD sE resTrsf) ]]]
 601
 602   ]
 603 (*
 604   AST_NO_DECL: ∀d.∀e:aux_env_type d.
 605                list (ast_stm d e) → ast_decl d e
 606 | AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
 607                   (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
 608 | AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
 609                 (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e
 610 *)
 611 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
 612                                                                        env_to_flatEnv_inv d e m fe →
 613                                                                        ast_to_astfe_decl_record d e fe ≝
 614  match ast
 615   return λD.λE.λast:ast_decl D E.
 616          Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
 617   with
 618    [ AST_NO_DECL sD sE sLStm ⇒
 619     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 620     let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
 621                 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
 622      match l with
 623       [ nil ⇒
 624        AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) []
 625
 626       | cons h t ⇒
 627        match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
 628         [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
 629          match aux t resMap resFe resDimInv with
 630           [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
 631            AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
 632                                         (leflatenv_trans ??? resDimLe resDimLe')
 633                                         ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
 634
 635       ] in
 636    match aux sLStm m fe dimInv with
 637     [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
 638      AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
 639                               (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
 640                               resDimLe resLStm ]
 641
 642    | AST_CONST_DECL sD sE sName sType sDim sInit sDecl ⇒
 643     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 644     match ast_to_astfe_decl sD (add_desc_env sD sE sName true sType) sDecl
 645           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
 646           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
 647           (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv) with
 648      [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 649       AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
 650                                ([ tripleT ??? sName true sType ]@resTrsf)
 651                                (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
 652                                (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe)
 653                                ([ ASTFE_STM_INIT resFe true sType
 654                                                  (* l'id e' sull'ambiente arricchito *)
 655                                                  (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
 656                                                                          true sType
 657                                                                          (ast_to_astfe_id sD (add_desc_env sD sE sName true sType)
 658                                                                                           true sType
 659                                                                                           (newid_from_init sD sE sName true sType)
 660                                                                                           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
 661                                                                                           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName true sType ] (pair ?? m fe)))
 662                                                                                           (env_map_flatEnv_addSingle_aux sD sE m fe sName true sType dimInv))
 663                                                                          sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
 664                                                                          resMap resFe
 665                                                                          (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
 666                                                                          resDimLe)
 667                                                  (* l'init e' sull'ambiente non arricchito *)
 668                                                  (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType sInit m fe dimInv)
 669                                                                            sD (build_trasfEnv_env sD ([ tripleT ??? sName true sType ]@resTrsf) sE)
 670                                                                            resMap resFe
 671                                                                            (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName true sType resTrsf resDimInv)
 672                                                                            (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName true sType ]) resDimLe))
 673                                 ]@resLStm) ]
 674
 675    | AST_VAR_DECL sD sE sName sType sDim sOptInit sDecl ⇒
 676     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 677     match ast_to_astfe_decl sD (add_desc_env sD sE sName false sType) sDecl
 678           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
 679           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
 680           (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv) with
 681      [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 682       AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
 683                                ([ tripleT ??? sName false sType ]@resTrsf)
 684                                (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
 685                                (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe)
 686                                (match sOptInit with
 687                                 [ None ⇒ []
 688                                 | Some init ⇒
 689                                  [ ASTFE_STM_INIT resFe false sType
 690                                                   (* l'id e' sull'ambiente arricchito *)
 691                                                   (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
 692                                                                           false sType
 693                                                                           (ast_to_astfe_id sD (add_desc_env sD sE sName false sType)
 694                                                                                            false sType
 695                                                                                            (newid_from_init sD sE sName false sType)
 696                                                                                            (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
 697                                                                                            (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName false sType ] (pair ?? m fe)))
 698                                                                                            (env_map_flatEnv_addSingle_aux sD sE m fe sName false sType dimInv))
 699                                                                           sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
 700                                                                           resMap resFe
 701                                                                           (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
 702                                                                           resDimLe)
 703                                                   (* l'init e' sull'ambiente non arricchito *)
 704                                                   (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
 705                                                                             sD (build_trasfEnv_env sD ([ tripleT ??? sName false sType ]@resTrsf) sE)
 706                                                                             resMap resFe
 707                                                                             (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName false sType resTrsf resDimInv)
 708                                                                             (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName false sType ]) resDimLe))
 709                                  ]]@resLStm) ]
 710
 711    ].
 712
 713 (*
 714   AST_ROOT: ast_decl O empty_env → ast_root
 715 *)
 716 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
 717 λast:ast_root.match ast with
 718  [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
 719   [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].