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