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
  91 | AST_EXPR_GT : ∀t:ast_base_type.
  92                 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)
  93 | AST_EXPR_GTE: ∀t:ast_base_type.
  94                 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)
  95 | AST_EXPR_LT : ∀t:ast_base_type.
  96                 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)
  97 | AST_EXPR_LTE: ∀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_EQ : ∀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_NEQ: ∀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
 104 | 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)
 105 | 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)
 106 | 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)
 107 | 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)
 108 | 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)
 109 | 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)
 110
 111 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
 112                ast_var d e b t → ast_expr d e t
 113 *)
 114 let rec ast_to_astfe_expr d (e:aux_env_type d) t (ast:ast_expr d e t)
 115                           (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_expr fe t ≝
 116  match ast
 117   return λW.λa:ast_expr d 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 d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 128   | AST_EXPR_NOT bType sExpr ⇒
 129    ASTFE_EXPR_NOT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 130   | AST_EXPR_COM bType sExpr ⇒
 131    ASTFE_EXPR_COM fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 132
 133   | AST_EXPR_ADD bType sExpr1 sExpr2 ⇒
 134    ASTFE_EXPR_ADD fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 135                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 136   | AST_EXPR_SUB bType sExpr1 sExpr2 ⇒
 137    ASTFE_EXPR_SUB fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 138                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 139   | AST_EXPR_MUL bType sExpr1 sExpr2 ⇒
 140    ASTFE_EXPR_MUL 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_DIV bType sExpr1 sExpr2 ⇒
 143    ASTFE_EXPR_DIV 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_SHR bType sExpr1 sExpr2 ⇒
 146    ASTFE_EXPR_SHR 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 AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
 148   | AST_EXPR_SHL bType sExpr1 sExpr2 ⇒
 149    ASTFE_EXPR_SHL 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 AST_BASE_TYPE_BYTE8) sExpr2 m fe dimInv)
 151
 152   | AST_EXPR_GT bType sExpr1 sExpr2 ⇒
 153    ASTFE_EXPR_GT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 154                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 155   | AST_EXPR_GTE bType sExpr1 sExpr2 ⇒
 156    ASTFE_EXPR_GTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 157                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 158   | AST_EXPR_LT bType sExpr1 sExpr2 ⇒
 159    ASTFE_EXPR_LT fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 160                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 161   | AST_EXPR_LTE bType sExpr1 sExpr2 ⇒
 162    ASTFE_EXPR_LTE fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 163                            (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 164   | AST_EXPR_EQ bType sExpr1 sExpr2 ⇒
 165    ASTFE_EXPR_EQ fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr1 m fe dimInv)
 166                           (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr2 m fe dimInv)
 167   | AST_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 168    ASTFE_EXPR_NEQ 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
 171   | AST_EXPR_B8toW16 sExpr ⇒
 172    ASTFE_EXPR_B8toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
 173   | AST_EXPR_B8toW32 sExpr ⇒
 174    ASTFE_EXPR_B8toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr m fe dimInv)
 175   | AST_EXPR_W16toB8 sExpr ⇒
 176    ASTFE_EXPR_W16toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
 177   | AST_EXPR_W16toW32 sExpr ⇒
 178    ASTFE_EXPR_W16toW32 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr m fe dimInv)
 179   | AST_EXPR_W32toB8 sExpr ⇒
 180    ASTFE_EXPR_W32toB8 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
 181   | AST_EXPR_W32toW16 sExpr ⇒
 182    ASTFE_EXPR_W32toW16 fe (ast_to_astfe_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr m fe dimInv)
 183
 184   | AST_EXPR_ID b sType var ⇒
 185    ASTFE_EXPR_ID fe b sType (ast_to_astfe_var d e b sType var m fe dimInv)
 186
 187   ]
 188 (*
 189   AST_VAR_ID: ∀b:bool.∀t:ast_type.
 190               ast_id d e b t → ast_var d e b t
 191 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
 192                  ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
 193 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
 194                   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)
 195 *)
 196 and ast_to_astfe_var d (e:aux_env_type d) b t (ast:ast_var d e b t)
 197                      (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_var fe b t ≝
 198  match ast
 199   return λW,X.λa:ast_var d e W X.astfe_var fe W X
 200  with
 201   [ AST_VAR_ID sB sType sId ⇒
 202    ASTFE_VAR_ID fe sB sType (ast_to_astfe_id d e sB sType sId m fe dimInv)
 203
 204   | AST_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 205    ASTFE_VAR_ARRAY fe sB sType sDim (ast_to_astfe_var d e sB (AST_TYPE_ARRAY sType sDim) sVar m fe dimInv)
 206                                     (ast_to_astfe_base_expr d e sExpr m fe dimInv)
 207
 208   | AST_VAR_STRUCT sB sType sField sVar sLtb ⇒
 209    ASTFE_VAR_STRUCT fe sB sType sField (ast_to_astfe_var d e sB (AST_TYPE_STRUCT sType) sVar m fe dimInv)
 210   ]
 211 (*
 212   AST_BASE_EXPR: ∀t:ast_base_type.
 213                  ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e
 214
 215 *)
 216 and ast_to_astfe_base_expr d (e:aux_env_type d) (ast:ast_base_expr d e)
 217                            (m:aux_map_type d) fe (dimInv:env_to_flatEnv_inv d e m fe) on ast : astfe_base_expr fe ≝
 218  match ast
 219   return λa:ast_base_expr d e.astfe_base_expr fe
 220  with
 221   [ AST_BASE_EXPR bType sExpr ⇒
 222    ASTFE_BASE_EXPR fe bType (ast_to_astfe_expr d e (AST_TYPE_BASE bType) sExpr m fe dimInv)
 223   ].
 224
 225 let rec ast_to_astfe_retype_expr fe t (ast:astfe_expr fe t)
 226                                  d (e:aux_env_type d) (m:aux_map_type d) fe'
 227                                  (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_expr fe' t ≝
 228  match ast
 229   return λW.λa:astfe_expr fe W.astfe_expr fe' W
 230  with
 231   [ ASTFE_EXPR_BYTE8 val ⇒
 232    ASTFE_EXPR_BYTE8 fe' val
 233   | ASTFE_EXPR_WORD16 val ⇒
 234    ASTFE_EXPR_WORD16 fe' val
 235   | ASTFE_EXPR_WORD32 val ⇒
 236    ASTFE_EXPR_WORD32 fe' val
 237
 238   | ASTFE_EXPR_NEG bType sExpr ⇒
 239    ASTFE_EXPR_NEG fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 240   | ASTFE_EXPR_NOT bType sExpr ⇒
 241    ASTFE_EXPR_NOT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 242   | ASTFE_EXPR_COM bType sExpr ⇒
 243    ASTFE_EXPR_COM fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 244
 245   | ASTFE_EXPR_ADD bType sExpr1 sExpr2 ⇒
 246    ASTFE_EXPR_ADD fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 247                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 248   | ASTFE_EXPR_SUB bType sExpr1 sExpr2 ⇒
 249    ASTFE_EXPR_SUB fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 250                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 251   | ASTFE_EXPR_MUL bType sExpr1 sExpr2 ⇒
 252    ASTFE_EXPR_MUL fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 253                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 254   | ASTFE_EXPR_DIV bType sExpr1 sExpr2 ⇒
 255    ASTFE_EXPR_DIV fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 256                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 257   | ASTFE_EXPR_SHR bType sExpr1 sExpr2 ⇒
 258    ASTFE_EXPR_SHR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 259                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
 260   | ASTFE_EXPR_SHL bType sExpr1 sExpr2 ⇒
 261    ASTFE_EXPR_SHL 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 AST_BASE_TYPE_BYTE8) sExpr2 d e m fe' dimInv dimLe)
 263
 264   | ASTFE_EXPR_GT bType sExpr1 sExpr2 ⇒
 265    ASTFE_EXPR_GT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 266                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 267   | ASTFE_EXPR_GTE bType sExpr1 sExpr2 ⇒
 268    ASTFE_EXPR_GTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 269                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 270   | ASTFE_EXPR_LT bType sExpr1 sExpr2 ⇒
 271    ASTFE_EXPR_LT fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 272                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 273   | ASTFE_EXPR_LTE bType sExpr1 sExpr2 ⇒
 274    ASTFE_EXPR_LTE fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 275                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 276   | ASTFE_EXPR_EQ bType sExpr1 sExpr2 ⇒
 277    ASTFE_EXPR_EQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 278                            (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 279   | ASTFE_EXPR_NEQ bType sExpr1 sExpr2 ⇒
 280    ASTFE_EXPR_NEQ fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr1 d e m fe' dimInv dimLe)
 281                             (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr2 d e m fe' dimInv dimLe)
 282
 283   | ASTFE_EXPR_B8toW16 sExpr ⇒
 284    ASTFE_EXPR_B8toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
 285   | ASTFE_EXPR_B8toW32 sExpr ⇒
 286    ASTFE_EXPR_B8toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) sExpr d e m fe' dimInv dimLe)
 287   | ASTFE_EXPR_W16toB8 sExpr ⇒
 288    ASTFE_EXPR_W16toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
 289   | ASTFE_EXPR_W16toW32 sExpr ⇒
 290    ASTFE_EXPR_W16toW32 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) sExpr d e m fe' dimInv dimLe)
 291   | ASTFE_EXPR_W32toB8 sExpr ⇒
 292    ASTFE_EXPR_W32toB8 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
 293   | ASTFE_EXPR_W32toW16 sExpr ⇒
 294    ASTFE_EXPR_W32toW16 fe' (ast_to_astfe_retype_expr fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) sExpr d e m fe' dimInv dimLe)
 295
 296   | ASTFE_EXPR_ID b sType var ⇒
 297    ASTFE_EXPR_ID fe' b sType (ast_to_astfe_retype_var fe b sType var d e m fe' dimInv dimLe)
 298
 299   ]
 300 and ast_to_astfe_retype_var fe b t (ast:astfe_var fe b t)
 301                             d (e:aux_env_type d) (m:aux_map_type d) fe'
 302                             (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_var fe' b t ≝
 303  match ast
 304   return λW,X.λa:astfe_var fe W X.astfe_var fe' W X
 305  with
 306   [ ASTFE_VAR_ID sB sType sId ⇒
 307    ASTFE_VAR_ID fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
 308
 309   | ASTFE_VAR_ARRAY sB sType sDim sVar sExpr ⇒
 310    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)
 311                                      (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
 312
 313   | ASTFE_VAR_STRUCT sB sType sField sVar ⇒
 314    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)
 315   ]
 316 and ast_to_astfe_retype_base_expr fe (ast:astfe_base_expr fe)
 317                                   d (e:aux_env_type d) (m:aux_map_type d) fe'
 318                                   (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_base_expr fe' ≝
 319  match ast
 320   return λa:astfe_base_expr fe.astfe_base_expr fe'
 321  with
 322   [ ASTFE_BASE_EXPR bType sExpr ⇒
 323    ASTFE_BASE_EXPR fe' bType (ast_to_astfe_retype_expr fe (AST_TYPE_BASE bType) sExpr d e m fe' dimInv dimLe)
 324   ].
 325
 326 (*
 327   AST_INIT_VAR: ∀b:bool.∀t:ast_type.
 328                 ast_var d e b t → ast_init d e t
 329 | AST_INIT_VAL: ∀t:ast_type.
 330                 aux_ast_init_type t → ast_init d e t
 331 *)
 332 definition ast_to_astfe_init ≝
 333 λd.λe:aux_env_type d.λt.λast:ast_init d e t.
 334 λm:aux_map_type d.λfe.
 335 λdimInv:env_to_flatEnv_inv d e m fe.
 336  match ast
 337   return λW.λa:ast_init d e W.astfe_init fe W
 338  with
 339   [ AST_INIT_VAR sB sType sVar ⇒
 340    ASTFE_INIT_VAR fe sB sType (ast_to_astfe_var d e sB sType sVar m fe dimInv)
 341
 342   | AST_INIT_VAL sType sArgs ⇒
 343    ASTFE_INIT_VAL fe sType sArgs
 344
 345   ].
 346
 347 definition ast_to_astfe_retype_init ≝
 348 λfe,t.λast:astfe_init fe t.
 349 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 350 λdimInv:env_to_flatEnv_inv d e m fe'.
 351 λdimLe:le_flatEnv fe fe' = true.
 352  match ast
 353   return λW.λa:astfe_init fe W.astfe_init fe' W
 354  with
 355   [ ASTFE_INIT_VAR sB sType sVar ⇒
 356    ASTFE_INIT_VAR fe' sB sType (ast_to_astfe_retype_var fe sB sType sVar d e m fe' dimInv dimLe)
 357
 358   | ASTFE_INIT_VAL sType sArgs ⇒
 359    ASTFE_INIT_VAL fe' sType sArgs
 360
 361   ].
 362
 363 (*
 364   ASTFE_STM_ASG: ∀t:ast_type.
 365                  astfe_var e false t → astfe_expr e t → astfe_stm e
 366 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
 367                   astfe_id e b t → astfe_init e t → astfe_stm e
 368 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
 369 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
 370 *)
 371 let rec ast_to_astfe_retype_stm fe (ast:astfe_stm fe)
 372                                 d (e:aux_env_type d) (m:aux_map_type d) fe'
 373                                 (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) on ast : astfe_stm fe' ≝
 374  match ast with
 375   [ ASTFE_STM_ASG sType sVar sExpr ⇒
 376    ASTFE_STM_ASG fe' sType (ast_to_astfe_retype_var fe false sType sVar d e m fe' dimInv dimLe)
 377                            (ast_to_astfe_retype_expr fe sType sExpr d e m fe' dimInv dimLe)
 378
 379   | ASTFE_STM_INIT sB sType sId sInit ⇒
 380    ASTFE_STM_INIT fe' sB sType (ast_to_astfe_retype_id fe sB sType sId d e m fe' dimInv dimLe)
 381                                (ast_to_astfe_retype_init fe sType sInit d e m fe' dimInv dimLe)
 382
 383   | ASTFE_STM_WHILE sExpr sBody ⇒
 384    ASTFE_STM_WHILE fe' (ast_to_astfe_retype_base_expr fe sExpr d e m fe' dimInv dimLe)
 385                        (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)
 386
 387   | ASTFE_STM_IF sNelExprBody sOptBody ⇒
 388    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)
 389                                                                               (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
 390                                                                               )»&t)
 391                                                              «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 392                                                              sNelExprBody))
 393                     (opt_map ?? sOptBody
 394                       (λsBody.Some ? (ast_to_astfe_retype_body fe sBody d e m fe' dimInv dimLe)))
 395   ]
 396 (*
 397   ASTFE_BODY: list (astfe_stm e) → astfe_body e
 398 *)
 399 and ast_to_astfe_retype_body fe (ast:astfe_body fe)
 400                              d (e:aux_env_type d) (m:aux_map_type d) fe'
 401                              (dimInv:env_to_flatEnv_inv d e m fe') (dimLe:le_flatEnv fe fe' = true) 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).
 409 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 410 λdimInv:env_to_flatEnv_inv d e m fe'.
 411 λdimLe:le_flatEnv fe fe' = true.
 412  fold_right_list ?? (λh,t.[ ast_to_astfe_retype_stm fe h d e m fe' dimInv dimLe ]@t) [] ast.
 413
 414 definition ast_to_astfe_retype_exprBody_neList ≝
 415 λfe.λast:ne_list (Prod (astfe_base_expr fe) (astfe_body fe)).
 416 λd.λe:aux_env_type d.λm:aux_map_type d.λfe'.
 417 λdimInv:env_to_flatEnv_inv d e m fe'.
 418 λdimLe:le_flatEnv fe fe' = true.
 419  cut_last_neList ? (fold_right_neList ?? (λh,t.«£(pair ?? (ast_to_astfe_retype_base_expr fe (fst ?? h) d e m fe' dimInv dimLe)
 420                                                           (ast_to_astfe_retype_body fe (snd ?? h) d e m fe' dimInv dimLe)
 421                                                           )»&t)
 422                                          «£(pair ?? (ASTFE_BASE_EXPR fe' (AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe' 〈x0,x0〉)) (ASTFE_BODY fe' []))»
 423                                          ast).
 424
 425 (* multi-sigma per incapsulare i risultati della trasformazione sugli stm/decl *)
 426 inductive ast_to_astfe_stm_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 427 AST_TO_ASTFE_STM_RECORD: ∀m:aux_map_type d.∀fe'.
 428                          env_to_flatEnv_inv d e m fe' →
 429                          le_flatEnv fe fe' = true →
 430                          astfe_stm fe' →
 431                          ast_to_astfe_stm_record d e fe.
 432
 433 inductive ast_to_astfe_if_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 434 AST_TO_ASTFE_IF_RECORD: ∀m:aux_map_type d.∀fe'.
 435                         env_to_flatEnv_inv d e m fe' →
 436                         le_flatEnv fe fe' = true →
 437                         ne_list (Prod (astfe_base_expr fe') (astfe_body fe')) →
 438                         ast_to_astfe_if_record d e fe.
 439
 440 inductive ast_to_astfe_decl_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 441 AST_TO_ASTFE_DECL_RECORD: ∀m:aux_map_type d.∀fe'.∀trsf:list (Prod3T aux_str_type bool ast_type).
 442                           env_to_flatEnv_inv d (build_trasfEnv_env d trsf e) m fe' →
 443                           le_flatEnv fe fe' = true →
 444                           list (astfe_stm fe') →
 445                           ast_to_astfe_decl_record d e fe.
 446
 447 inductive ast_to_astfe_decl_aux_record (d:nat) (e:aux_env_type d) (fe:aux_flatEnv_type) : Type ≝
 448 AST_TO_ASTFE_DECL_AUX_RECORD: ∀m:aux_map_type d.∀fe'.
 449                               env_to_flatEnv_inv d e m fe' →
 450                               le_flatEnv fe fe' = true →
 451                               list (astfe_stm fe') →
 452                               ast_to_astfe_decl_aux_record d e fe.
 453
 454 (*
 455   AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
 456                ast_var d e false t → ast_expr d e t → ast_stm d e
 457 | AST_STM_WHILE: ∀d.∀e:aux_env_type d.
 458                  ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
 459 | AST_STM_IF: ∀d.∀e:aux_env_type d.
 460               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
 461 *)
 462 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.
 463                                                                          env_to_flatEnv_inv d e m fe →
 464                                                                          ast_to_astfe_stm_record d e fe ≝
 465  match ast
 466   return λD.λE.λast:ast_stm D E.
 467          Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_stm_record D E fe
 468  with
 469   [ AST_STM_ASG sD sE sType sVar sExpr ⇒
 470    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 471    AST_TO_ASTFE_STM_RECORD sD sE fe m fe dimInv
 472                            (eq_to_leflatenv ?? (refl_eq ??))
 473                            (ASTFE_STM_ASG fe sType (ast_to_astfe_var sD sE false sType sVar m fe dimInv)
 474                                                    (ast_to_astfe_expr sD sE sType sExpr m fe dimInv))
 475   | AST_STM_WHILE sD sE sExpr sDecl ⇒
 476    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 477    match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD m) fe
 478          (env_map_flatEnv_enter_aux sD sE m fe dimInv) with
 479     [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 480      eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 481              (λenv.ast_to_astfe_stm_record sD env fe)
 482              (AST_TO_ASTFE_STM_RECORD sD
 483                                       (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 484                                       fe
 485                                       (leave_map sD resMap)
 486                                       resFe
 487                                       (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 488                                       resDimLe
 489                                       (ASTFE_STM_WHILE resFe
 490                                                        (ast_to_astfe_retype_base_expr fe (ast_to_astfe_base_expr sD sE sExpr m fe dimInv)
 491                                                                                       sD
 492                                                                                       (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 493                                                                                       (leave_map sD resMap)
 494                                                                                       resFe
 495                                                                                       (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 496                                                                                       resDimLe)
 497                                                        (ASTFE_BODY resFe resLStm)))
 498              sE (leave_add_enter_env sD sE resTrsf) ]
 499
 500   | AST_STM_IF sD sE sExprDecl sOptDecl ⇒
 501    λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 502    let rec aux (nel:ne_list (Prod (ast_base_expr sD sE) (ast_decl (S sD) (enter_env sD sE))))
 503                (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
 504                (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on nel : ast_to_astfe_if_record sD sE pFe ≝
 505     match nel with
 506      [ ne_nil h ⇒
 507       match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
 508             (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
 509        [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 510         eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 511                 (λenv.ast_to_astfe_if_record sD env pFe)
 512                 (AST_TO_ASTFE_IF_RECORD sD
 513                                         (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 514                                         pFe
 515                                         (leave_map sD resMap)
 516                                         resFe
 517                                         (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 518                                         resDimLe
 519                                         «£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
 520                                                                                   sD
 521                                                                                   (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 522                                                                                   (leave_map sD resMap)
 523                                                                                   resFe
 524                                                                                   (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 525                                                                                   resDimLe)
 526                                                    (ASTFE_BODY resFe resLStm))»)
 527                 sE (leave_add_enter_env sD sE resTrsf) ]
 528
 529      | ne_cons h t ⇒
 530       match ast_to_astfe_decl (S sD) (enter_env sD sE) (snd ?? h) (enter_map sD pMap) pFe
 531             (env_map_flatEnv_enter_aux sD sE pMap pFe pDimInv) with
 532        [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 533         match aux t (leave_map sD resMap) resFe
 534                   (eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 535                            (λenv.env_to_flatEnv_inv sD env (leave_map sD resMap) resFe)
 536                            (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap resFe resTrsf resDimInv)
 537                            sE (leave_add_enter_env sD sE resTrsf)) with
 538         [ AST_TO_ASTFE_IF_RECORD resMap' resFe' resDimInv' resDimLe' resExprBody ⇒
 539          AST_TO_ASTFE_IF_RECORD sD sE pFe resMap' resFe' resDimInv'
 540                                 (leflatenv_trans ??? resDimLe resDimLe')
 541                                 («£(pair ?? (ast_to_astfe_retype_base_expr pFe (ast_to_astfe_base_expr sD sE (fst ?? h) pMap pFe pDimInv)
 542                                                                            sD sE resMap' resFe' resDimInv'
 543                                                                            (leflatenv_trans ??? resDimLe resDimLe'))
 544                                             (ast_to_astfe_retype_body resFe (ASTFE_BODY resFe resLStm)
 545                                                                       sD sE resMap' resFe' resDimInv' resDimLe'))»&resExprBody) ]]
 546
 547      ] in
 548    match aux sExprDecl m fe dimInv with
 549     [ AST_TO_ASTFE_IF_RECORD resMap resFe resDimInv resDimLe resExprBody ⇒
 550      match sOptDecl with
 551       [ None ⇒
 552        AST_TO_ASTFE_STM_RECORD sD sE fe resMap resFe resDimInv resDimLe (ASTFE_STM_IF resFe resExprBody (None ?))
 553
 554       | Some sDecl ⇒
 555        match ast_to_astfe_decl (S sD) (enter_env sD sE) sDecl (enter_map sD resMap) resFe
 556              (env_map_flatEnv_enter_aux sD sE resMap resFe resDimInv) with
 557         [ AST_TO_ASTFE_DECL_RECORD resMap' resFe' resTrsf resDimInv' resDimLe' resLStm ⇒
 558          eq_rect ? (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 559                  (λenv.ast_to_astfe_stm_record sD env fe)
 560                  (AST_TO_ASTFE_STM_RECORD sD
 561                                           (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 562                                           fe
 563                                           (leave_map sD resMap')
 564                                           resFe'
 565                                           (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
 566                                           (leflatenv_trans ??? resDimLe resDimLe')
 567                                           (ASTFE_STM_IF resFe'
 568                                                         (ast_to_astfe_retype_exprBody_neList resFe resExprBody
 569                                                                                              sD
 570                                                                                              (leave_env sD (build_trasfEnv_env (S sD) resTrsf (enter_env sD sE)))
 571                                                                                              (leave_map sD resMap')
 572                                                                                              resFe'
 573                                                                                              (env_map_flatEnv_leave_aux sD (enter_env sD sE) resMap' resFe' resTrsf resDimInv')
 574                                                                                              resDimLe')
 575                                                         (Some ? (ASTFE_BODY resFe' resLStm))))
 576                  sE (leave_add_enter_env sD sE resTrsf) ]]]
 577
 578   ]
 579 (*
 580   AST_NO_DECL: ∀d.∀e:aux_env_type d.
 581                list (ast_stm d e) → ast_decl d e
 582 | AST_DECL: ∀d.∀e:aux_env_type d.∀c:bool.∀str:aux_str_type.∀t:ast_type.
 583             (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str c t) → ast_decl d e
 584 *)
 585 and ast_to_astfe_decl d (e:aux_env_type d) (ast:ast_decl d e) on ast : Πm:aux_map_type d.Πfe.
 586                                                                        env_to_flatEnv_inv d e m fe →
 587                                                                        ast_to_astfe_decl_record d e fe ≝
 588  match ast
 589   return λD.λE.λast:ast_decl D E.
 590          Πm:aux_map_type D.Πfe.env_to_flatEnv_inv D E m fe → ast_to_astfe_decl_record D E fe
 591   with
 592    [ AST_NO_DECL sD sE sLStm ⇒
 593     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 594     let rec aux (l:list (ast_stm sD sE)) (pMap:aux_map_type sD) (pFe:aux_flatEnv_type)
 595                 (pDimInv:env_to_flatEnv_inv sD sE pMap pFe) on l : ast_to_astfe_decl_aux_record sD sE pFe ≝
 596      match l with
 597       [ nil ⇒
 598        AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe pMap pFe pDimInv (eq_to_leflatenv ?? (refl_eq ??)) []
 599
 600       | cons h t ⇒
 601        match ast_to_astfe_stm sD sE h pMap pFe pDimInv with
 602         [ AST_TO_ASTFE_STM_RECORD resMap resFe resDimInv resDimLe resStm ⇒
 603          match aux t resMap resFe resDimInv with
 604           [ AST_TO_ASTFE_DECL_AUX_RECORD resMap' resFe' resDimInv' resDimLe' resLStm ⇒
 605            AST_TO_ASTFE_DECL_AUX_RECORD sD sE pFe resMap' resFe' resDimInv'
 606                                         (leflatenv_trans ??? resDimLe resDimLe')
 607                                         ([ ast_to_astfe_retype_stm resFe resStm sD sE resMap' resFe' resDimInv' resDimLe' ]@resLStm) ]]
 608
 609       ] in
 610    match aux sLStm m fe dimInv with
 611     [ AST_TO_ASTFE_DECL_AUX_RECORD resMap resFe resDimInv resDimLe resLStm ⇒
 612      AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe []
 613                               (env_map_flatEnv_addNil_aux sD sE resMap resFe resDimInv)
 614                               resDimLe resLStm ]
 615
 616    | AST_DECL sD sE sB sName sType sDim sOptInit sDecl ⇒
 617     λm:aux_map_type sD.λfe.λdimInv:env_to_flatEnv_inv sD sE m fe.
 618     match ast_to_astfe_decl sD (add_desc_env sD sE sName sB sType) sDecl
 619           (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
 620           (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
 621           (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv) with
 622      [ AST_TO_ASTFE_DECL_RECORD resMap resFe resTrsf resDimInv resDimLe resLStm ⇒
 623       AST_TO_ASTFE_DECL_RECORD sD sE fe resMap resFe
 624                                ([ tripleT ??? sName sB sType ]@resTrsf)
 625                                (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
 626                                (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe)
 627                                (match sOptInit with
 628                                 [ None ⇒ []
 629                                 | Some init ⇒
 630                                  [ ASTFE_STM_INIT resFe sB sType
 631                                                   (* l'id e' sull'ambiente arricchito *)
 632                                                   (ast_to_astfe_retype_id (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
 633                                                                           sB sType
 634                                                                           (ast_to_astfe_id sD (add_desc_env sD sE sName sB sType)
 635                                                                                            sB sType
 636                                                                                            (newid_from_init sD sE sName sB sType)
 637                                                                                            (fst ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
 638                                                                                            (snd ?? (build_trasfEnv_mapFe sD [ tripleT ??? sName sB sType ] (pair ?? m fe)))
 639                                                                                            (env_map_flatEnv_addSingle_aux sD sE m fe sName sB sType dimInv))
 640                                                                           sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
 641                                                                           resMap resFe
 642                                                                           (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
 643                                                                           resDimLe)
 644                                                   (* l'init e' sull'ambiente non arricchito *)
 645                                                   (ast_to_astfe_retype_init fe sType (ast_to_astfe_init sD sE sType init m fe dimInv)
 646                                                                             sD (build_trasfEnv_env sD ([ tripleT ??? sName sB sType ]@resTrsf) sE)
 647                                                                             resMap resFe
 648                                                                             (env_map_flatEnv_addJoin_aux sD sE resMap resFe sName sB sType resTrsf resDimInv)
 649                                                                             (leflatenv_trans ??? (buildtrasfenvadd_to_le sD m fe [ tripleT ??? sName sB sType ]) resDimLe))
 650                                  ]]@resLStm) ]
 651
 652    ].
 653
 654 (*
 655   AST_ROOT: ast_decl O empty_env → ast_root
 656 *)
 657 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
 658 λast:ast_root.match ast with
 659  [ AST_ROOT decl ⇒ match ast_to_astfe_decl O empty_env decl empty_map empty_flatEnv env_map_flatEnv_empty_aux with
 660   [ AST_TO_ASTFE_DECL_RECORD _ resFe _ _ _ resLStm ⇒ ≪resFe,ASTFE_ROOT resFe (ASTFE_BODY resFe resLStm)≫ ]].