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
  24 (* ************************ *)
  25 (* PASSO 2 : da AST a ASTFE *)
  26 (* ************************ *)
  27
  28 (* operatore di cast *)
  29 definition ast_to_astfe_expr_check : Πt.astfe_expr t → Πt'.option (astfe_expr t') ≝
  30 λt:ast_type.λast:astfe_expr t.λt':ast_type.
  31  match eq_ast_type t t'
  32   return λx.(eq_ast_type t t' = x) → ?
  33  with
  34   [ true ⇒ λp:(eq_ast_type t t' = true).
  35    Some ? (eq_rect ? t (λt.astfe_expr t) ast t' (eqasttype_to_eq ?? p))
  36   | false ⇒ λp:(eq_ast_type t t' = false).None ?
  37   ] (refl_eq ? (eq_ast_type t t')).
  38
  39 definition ast_to_astfe_init_check : Πt.astfe_init t → Πt'.option (astfe_init t') ≝
  40 λt:ast_type.λast:astfe_init t.λt':ast_type.
  41  match eq_ast_type t t'
  42   return λx.(eq_ast_type t t' = x) → ?
  43  with
  44   [ true ⇒ λp:(eq_ast_type t t' = true).
  45    Some ? (eq_rect ? t (λt.astfe_init t) ast t' (eqasttype_to_eq ?? p))
  46   | false ⇒ λp:(eq_ast_type t t' = false).None ?
  47   ] (refl_eq ? (eq_ast_type t t')).
  48
  49 definition ast_to_astfe_var_checkb : Πb.Πt.astfe_var b t → Πb'.option (astfe_var b' t) ≝
  50 λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.
  51  match eq_bool b b'
  52   return λx.(eq_bool b b' = x) → ?
  53  with
  54   [ true ⇒ λp:(eq_bool b b' = true).
  55    Some ? (eq_rect ? b (λb.astfe_var b t) ast b' (eqbool_to_eq ?? p))
  56   | false ⇒ λp:(eq_bool b b' = false).None ?
  57   ] (refl_eq ? (eq_bool b b')).
  58
  59 definition ast_to_astfe_var_checkt : Πb.Πt.astfe_var b t → Πt'.option (astfe_var b t') ≝
  60 λb:bool.λt:ast_type.λast:astfe_var b t.λt':ast_type.
  61  match eq_ast_type t t'
  62   return λx.(eq_ast_type t t' = x) → ?
  63  with
  64   [ true ⇒ λp:(eq_ast_type t t' = true).
  65    Some ? (eq_rect ? t (λt.astfe_var b t) ast t' (eqasttype_to_eq ?? p))
  66   | false ⇒ λp:(eq_ast_type t t' = false).None ?
  67   ] (refl_eq ? (eq_ast_type t t')).
  68
  69 definition ast_to_astfe_var_check : Πb.Πt.astfe_var b t → Πb'.Πt'.option (astfe_var b' t') ≝
  70 λb:bool.λt:ast_type.λast:astfe_var b t.λb':bool.λt':ast_type.
  71  opt_map ?? (ast_to_astfe_var_checkb b t ast b')
  72   (λres.opt_map ?? (ast_to_astfe_var_checkt b' t res t')
  73    (λres'.Some ? res')).
  74
  75 (*
  76  AST_ID: ∀str:aux_str_type.
  77          (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)))
  78 *)
  79 definition ast_to_astfe_id ≝
  80 λe:aux_env_type.λb:bool.λt:ast_type.λast:ast_id e b t.λmap:aux_trasfMap_type.match ast with
  81  [ AST_ID str _ ⇒ ASTFE_ID (name_to_nameId map str) b t ].
  82
  83 (*
  84  AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  85  AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  86  AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  87
  88  AST_EXPR_NEG: ∀t:ast_base_type.
  89                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  90  AST_EXPR_NOT: ∀t:ast_base_type.
  91                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  92  AST_EXPR_COM: ∀t:ast_base_type.
  93                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  94
  95  AST_EXPR_ADD: ∀t:ast_base_type.
  96                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  97  AST_EXPR_SUB: ∀t:ast_base_type.
  98                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
  99  AST_EXPR_MUL: ∀t:ast_base_type.
 100                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 101  AST_EXPR_DIV: ∀t:ast_base_type.
 102                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 103  AST_EXPR_SHR: ∀t:ast_base_type.
 104                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
 105  AST_EXPR_SHL: ∀t:ast_base_type.
 106                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
 107
 108  AST_EXPR_GT : ∀t:ast_base_type.
 109                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 110  AST_EXPR_GTE: ∀t:ast_base_type.
 111                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 112  AST_EXPR_LT : ∀t:ast_base_type.
 113                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 114  AST_EXPR_LTE: ∀t:ast_base_type.
 115                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 116  AST_EXPR_EQ : ∀t:ast_base_type.
 117                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 118  AST_EXPR_NEQ: ∀t:ast_base_type.
 119                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 120
 121  AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 122  AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 123  AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 124  AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 125  AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 126  AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 127
 128  AST_EXPR_ID: ∀b:bool.∀t:ast_type.
 129               ast_var e b t → ast_expr e t
 130 *)
 131 let rec ast_to_astfe_expr (e:aux_env_type) (t:ast_type) (ast:ast_expr e t) (map:aux_trasfMap_type) on ast : option (astfe_expr t) ≝
 132  match ast with
 133   [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 val) t
 134   | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 val) t
 135   | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 val) t
 136
 137   | AST_EXPR_NEG bType subExpr ⇒
 138    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
 139     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG bType res) t)
 140   | AST_EXPR_NOT bType subExpr ⇒
 141    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
 142     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT bType res) t)
 143   | AST_EXPR_COM bType subExpr ⇒
 144    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
 145     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_COM bType res) t)
 146
 147   | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
 148    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 149     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 150      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD bType res1 res2) t))
 151   | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
 152    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 153     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 154      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB bType res1 res2) t))
 155   | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
 156    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 157     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 158      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL bType res1 res2) t))
 159   | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
 160    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 161     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 162      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV bType res1 res2) t))
 163   | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
 164    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 165     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
 166      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR bType res1 res2) t))
 167   | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
 168    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 169     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 map)
 170      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL bType res1 res2) t))
 171
 172   | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
 173    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 174     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 175      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT bType res1 res2) t))
 176   | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
 177    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 178     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 179      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE bType res1 res2) t))
 180   | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
 181    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 182     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 183      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT bType res1 res2) t))
 184   | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
 185    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 186     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 187      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE bType res1 res2) t))
 188   | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
 189    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 190     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 191      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ bType res1 res2) t))
 192   | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
 193    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 map)
 194     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 map)
 195      (λres2.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ bType res1 res2) t))
 196
 197   | AST_EXPR_B8toW16 subExpr ⇒
 198    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
 199     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 res) t)
 200   | AST_EXPR_B8toW32 subExpr ⇒
 201    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr map)
 202     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 res) t)
 203   | AST_EXPR_W16toB8 subExpr ⇒
 204    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
 205     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 res) t)
 206   | AST_EXPR_W16toW32 subExpr ⇒
 207    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr map)
 208     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 res) t)
 209   | AST_EXPR_W32toB8 subExpr ⇒
 210    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
 211     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 res) t)
 212   | AST_EXPR_W32toW16 subExpr ⇒
 213    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr map)
 214     (λres.ast_to_astfe_expr_check (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 res) t)
 215
 216   | AST_EXPR_ID b subType var ⇒
 217    opt_map ?? (ast_to_astfe_var e b subType var map)
 218     (λres.ast_to_astfe_expr_check subType (ASTFE_EXPR_ID b subType res) t)
 219   ]
 220 (*
 221  AST_VAR_ID: ∀b:bool.∀t:ast_type.
 222              ast_id e b t → ast_var e b t
 223  AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
 224                 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
 225  AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
 226                  ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
 227 *)
 228 and ast_to_astfe_var (e:aux_env_type) (b:bool) (t:ast_type) (ast:ast_var e b t) (map:aux_trasfMap_type) on ast : option (astfe_var b t) ≝
 229  match ast with
 230   [ AST_VAR_ID subB subType subId ⇒ ast_to_astfe_var_check subB subType (ASTFE_VAR_ID subB subType (ast_to_astfe_id e subB subType subId map)) b t
 231
 232   | AST_VAR_ARRAY subB subType dim var expr ⇒
 233    opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var map)
 234     (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr map)
 235      (λresExpr.ast_to_astfe_var_check subB subType (ASTFE_VAR_ARRAY subB subType dim resVar resExpr) b t))
 236
 237   | AST_VAR_STRUCT subB nelSubType field var _ ⇒
 238    opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var map)
 239     (λres.ast_to_astfe_var_check subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT subB nelSubType field res) b t)
 240   ]
 241 (*
 242  AST_BASE_EXPR: ∀t:ast_base_type.
 243                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
 244 *)
 245 and ast_to_astfe_base_expr (e:aux_env_type) (ast:ast_base_expr e) (map:aux_trasfMap_type) on ast : option astfe_base_expr ≝
 246  match ast with
 247   [ AST_BASE_EXPR bType subExpr ⇒
 248    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr map)
 249     (λres.Some ? (ASTFE_BASE_EXPR bType res))
 250   ].
 251
 252 (*
 253  AST_INIT_VAR: ∀b:bool.∀t:ast_type.
 254                ast_var e b t → ast_init e t
 255  AST_INIT_VAL: ∀t:ast_type.
 256                aux_ast_init_type t → ast_init e t
 257 *)
 258 definition ast_to_astfe_init : Πe.Πt.ast_init e t → aux_trasfMap_type → option (astfe_init t) ≝
 259 λe:aux_env_type.λt:ast_type.λast:ast_init e t.λmap:aux_trasfMap_type.match ast with
 260  [ AST_INIT_VAR subB subType var ⇒
 261   opt_map ?? (ast_to_astfe_var e subB subType var map)
 262    (λres.ast_to_astfe_init_check subType (ASTFE_INIT_VAR subB subType res) t)
 263
 264  | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check subType (ASTFE_INIT_VAL subType args) t
 265  ].
 266
 267 (*
 268  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
 269               ast_var e false t → ast_expr e t → ast_stm e
 270  AST_STM_WHILE: ∀e:aux_env_type.
 271                 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
 272  AST_STM_IF: ∀e:aux_env_type.
 273              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
 274 *)
 275 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T astfe_stm aux_trasfMap_type aux_flatEnv_type) ≝
 276  match ast with
 277   [ AST_STM_ASG e' subType var expr ⇒
 278    opt_map ?? (ast_to_astfe_var e' false subType var map)
 279     (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr map)
 280      (λresExpr.Some ? (tripleT ??? (ASTFE_STM_ASG subType resVar resExpr) map fe)))
 281
 282   | AST_STM_WHILE e' expr decl ⇒
 283    opt_map ?? (ast_to_astfe_base_expr e' expr map)
 284     (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl map fe)
 285      (λtripleRes.match tripleRes with
 286       [ tripleT resDecl map' fe' ⇒
 287        Some ? (tripleT ??? (ASTFE_STM_WHILE resExpr (ASTFE_BODY resDecl)) (rollback_map map' (build_snapshot map)) fe')
 288       ]))
 289
 290   | AST_STM_IF e' nelExprDecl optDecl ⇒
 291    let rec aux (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e'))))
 292                (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on nel ≝
 293     match nel with
 294      [ ne_nil h ⇒
 295       opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
 296        (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
 297         (λtripleRes.match tripleRes with
 298          [ tripleT resDecl m' flatE' ⇒
 299           Some ? (tripleT ??? « pair ?? resExpr (ASTFE_BODY resDecl) £» (rollback_map m' (build_snapshot m)) flatE')
 300          ]))
 301      | ne_cons h tl ⇒
 302       opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) m)
 303        (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) m flatE)
 304         (λtripleRes.match tripleRes with
 305          [ tripleT resDecl m' flatE' ⇒
 306           opt_map ?? (aux tl (rollback_map m' (build_snapshot m)) flatE')
 307            (λtripleRes'.match tripleRes' with
 308             [ tripleT tl' m'' flatE'' ⇒
 309              Some ? (tripleT ??? (« pair ?? resExpr (ASTFE_BODY resDecl) £»&tl') m'' flatE'')
 310             ])]))] in
 311    opt_map ?? (aux nelExprDecl map fe)
 312     (λtRes.match tRes with
 313      [ tripleT resNel resMap resFe ⇒
 314       match optDecl with
 315        [ None ⇒ Some ? (tripleT ??? (ASTFE_STM_IF resNel (None ?)) resMap resFe)
 316        | Some decl ⇒
 317         opt_map ?? (ast_to_astfe_decl (enter_env e') decl resMap resFe)
 318          (λtRes'.match tRes' with
 319           [ tripleT rDecl resMap' resFe' ⇒
 320            Some ? (tripleT ??? (ASTFE_STM_IF resNel (Some ? (ASTFE_BODY rDecl))) (rollback_map resMap' (build_snapshot resMap)) resFe')
 321           ])
 322        ]])
 323   ]
 324 (*
 325  AST_NO_DECL: ∀e:aux_env_type.
 326               list (ast_stm e) → ast_decl e
 327  AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
 328            (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
 329 *)
 330 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (map:aux_trasfMap_type) (fe:aux_flatEnv_type) on ast : option (Prod3T (list astfe_stm) aux_trasfMap_type aux_flatEnv_type) ≝
 331  match ast with
 332   [ AST_NO_DECL e' lStm ⇒
 333    let rec aux (ll:list (ast_stm e')) (m:aux_trasfMap_type) (flatE:aux_flatEnv_type) on ll ≝
 334     match ll with
 335      [ nil ⇒ Some ? (tripleT ??? [] m flatE)
 336      | cons h tl ⇒
 337       opt_map ?? (ast_to_astfe_stm e' h m flatE)
 338        (λtripleRes.match tripleRes with
 339         [ tripleT resStm m' flatE' ⇒
 340          opt_map ?? (aux tl m' flatE')
 341           (λtripleRes'.match tripleRes' with
 342            [ tripleT tl' m'' flatE'' ⇒
 343             Some ? (tripleT ??? ([ resStm ]@tl') m'' flatE'')
 344            ])])] in
 345    aux lStm map fe
 346
 347   | AST_DECL e' b name t _ optInit subDecl ⇒
 348    opt_map ?? (match optInit with
 349                [ None ⇒ Some ? [] | Some init ⇒ opt_map ?? (ast_to_astfe_init e' t init map)
 350                 (λresInit.Some ? [ ASTFE_STM_INIT b t (ASTFE_ID (name_to_nameId (add_maxcur_map map name) name) b t) resInit ])])
 351     (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl (add_maxcur_map map name) (add_desc_flatEnv fe (name_to_nameId (add_maxcur_map map name) name) b t))
 352      (λtripleRes.match tripleRes with
 353       [ tripleT tRes resMap resFe ⇒
 354        Some ? (tripleT ??? (hRes@tRes) resMap resFe)
 355       ]))
 356   ].
 357
 358 (*
 359  AST_ROOT: ast_decl empty_env → ast_root.
 360 *)
 361 definition ast_to_astfe ≝
 362 λast:ast_root.match ast with
 363  [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_trasfMap empty_flatEnv with
 364   (* impossibile: dummy *)
 365   [ None ⇒ empty_astfe_prog
 366   | Some x ⇒ ASTFE_ROOT (thd3T ??? x) (ASTFE_BODY (fst3T ??? x))
 367   ]
 368  ].
 369
 370 (* mini test *)
 371 (*include "compiler/preast_tree.ma".
 372 include "compiler/preast_to_ast.ma".*)
 373
 374 (*
 375 { const byte8 a;
 376   const byte8[3] b={0,1,2};
 377   byte8[3] c=b;
 378
 379   if(0xF0)
 380    { byte8 a=a; }
 381   else if(0xF1)
 382    {
 383    while(0x10)
 384     { byte8[3] b=c; }
 385    }
 386   else if(0xF2)
 387    { byte8 a=b[0]; }
 388   else
 389    { const byte8 a=a; }
 390 }
 391 *)
 392 (*
 393 definition prova ≝
 394 PREAST_ROOT (
 395  PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
 396   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,x2〉)£(PREAST_INIT_VAL_BYTE8 〈x0,x0〉);(PREAST_INIT_VAL_BYTE8 〈x0,x1〉)»))) (
 397    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]))) (
 398     PREAST_NO_DECL [
 399      PREAST_STM_IF «
 400        (pair ??
 401        (PREAST_EXPR_BYTE8 〈xF,x2〉)
 402        (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 []))
 403        )
 404      £ (pair ??
 405        (PREAST_EXPR_BYTE8 〈xF,x0〉)
 406        (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
 407        )
 408      ; (pair ??
 409        (PREAST_EXPR_BYTE8 〈xF,x1〉)
 410        (PREAST_NO_DECL [
 411         (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
 412         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 [])
 413         ))
 414        ])
 415        )
 416      » (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 [])))
 417     ]
 418    )
 419   )
 420  )
 421 ).
 422
 423 lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
 424 normalize;
 425 *)