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