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