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 (* NB: avendo poi in input la dimostrazione "check_desc_env e (get_name_ast_id e b t ast)" ha senso *)
 111 axiom ast_to_astfe_id_ax:
 112  Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
 113   Πmap:aux_trasfMap_type e fe.
 114    check_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)).
 115
 116 (*
 117 axiom ax2:
 118  Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
 119   Πmap:aux_trasfMap_type e fe.
 120    get_const_desc
 121     (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))
 122    = b.
 123
 124 axiom ax3:
 125  Πe:aux_env_type.Πb:bool.Πt:ast_type. Πast:ast_id e b t. Πfe:aux_flatEnv_type.
 126   Πmap:aux_trasfMap_type e fe.
 127    get_type_desc
 128     (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))) = t.
 129 *)
 130
 131 definition ast_to_astfe_id:
 132  Πe:aux_env_type.Πb:bool.Πt:ast_type.Πast:ast_id e b t.Πfe:aux_flatEnv_type.
 133   Πmap:aux_trasfMap_type e fe.
 134    astfe_id fe
 135     (get_const_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast))))
 136     (get_type_desc (get_desc_flatEnv fe (name_to_nameId e fe map (get_name_ast_id e b t ast)))).
 137  apply
 138   (λ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.
 139     ASTFE_ID fe (name_to_nameId e fe map (get_name_ast_id e b t ast)) ?);
 140  apply ast_to_astfe_id_ax.
 141 qed.
 142
 143 (*
 144  AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 145  AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 146  AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 147
 148  AST_EXPR_NEG: ∀t:ast_base_type.
 149                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 150  AST_EXPR_NOT: ∀t:ast_base_type.
 151                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 152  AST_EXPR_COM: ∀t:ast_base_type.
 153                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 154
 155  AST_EXPR_ADD: ∀t:ast_base_type.
 156                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 157  AST_EXPR_SUB: ∀t:ast_base_type.
 158                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 159  AST_EXPR_MUL: ∀t:ast_base_type.
 160                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
 161  AST_EXPR_DIV: ∀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 t)
 163  AST_EXPR_SHR: ∀t:ast_base_type.
 164                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
 165  AST_EXPR_SHL: ∀t:ast_base_type.
 166                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
 167
 168  AST_EXPR_GT : ∀t:ast_base_type.
 169                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 170  AST_EXPR_GTE: ∀t:ast_base_type.
 171                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 172  AST_EXPR_LT : ∀t:ast_base_type.
 173                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 174  AST_EXPR_LTE: ∀t:ast_base_type.
 175                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 176  AST_EXPR_EQ : ∀t:ast_base_type.
 177                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 178  AST_EXPR_NEQ: ∀t:ast_base_type.
 179                ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 180
 181  AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 182  AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 183  AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 184  AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
 185  AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
 186  AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
 187
 188  AST_EXPR_ID: ∀b:bool.∀t:ast_type.
 189               ast_var e b t → ast_expr e t
 190 *)
 191 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) ≝
 192  match ast with
 193   [ AST_EXPR_BYTE8 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_BYTE8 fe val) t
 194   | AST_EXPR_WORD16 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_WORD16 fe val) t
 195   | AST_EXPR_WORD32 val ⇒ ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_WORD32 fe val) t
 196
 197   | AST_EXPR_NEG bType subExpr ⇒
 198    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
 199     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NEG fe bType res) t)
 200   | AST_EXPR_NOT bType subExpr ⇒
 201    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
 202     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_NOT fe bType res) t)
 203   | AST_EXPR_COM bType subExpr ⇒
 204    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
 205     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_COM fe bType res) t)
 206
 207   | AST_EXPR_ADD bType subExpr1 subExpr2 ⇒
 208    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 209     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 210      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_ADD fe bType res1 res2) t))
 211   | AST_EXPR_SUB bType subExpr1 subExpr2 ⇒
 212    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 213     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 214      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SUB fe bType res1 res2) t))
 215   | AST_EXPR_MUL bType subExpr1 subExpr2 ⇒
 216    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 217     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 218      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_MUL fe bType res1 res2) t))
 219   | AST_EXPR_DIV bType subExpr1 subExpr2 ⇒
 220    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 221     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 222      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_DIV fe bType res1 res2) t))
 223   | AST_EXPR_SHR bType subExpr1 subExpr2 ⇒
 224    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 225     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
 226      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHR fe bType res1 res2) t))
 227   | AST_EXPR_SHL bType subExpr1 subExpr2 ⇒
 228    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 229     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr2 fe map)
 230      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE bType) (ASTFE_EXPR_SHL fe bType res1 res2) t))
 231
 232   | AST_EXPR_LT bType subExpr1 subExpr2 ⇒
 233    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 234     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 235      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LT fe bType res1 res2) t))
 236   | AST_EXPR_LTE bType subExpr1 subExpr2 ⇒
 237    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 238     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 239      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_LTE fe bType res1 res2) t))
 240   | AST_EXPR_GT bType subExpr1 subExpr2 ⇒
 241    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 242     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 243      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GT fe bType res1 res2) t))
 244   | AST_EXPR_GTE bType subExpr1 subExpr2 ⇒
 245    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 246     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 247      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_GTE fe bType res1 res2) t))
 248   | AST_EXPR_EQ bType subExpr1 subExpr2 ⇒
 249    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 250     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 251      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_EQ fe bType res1 res2) t))
 252   | AST_EXPR_NEQ bType subExpr1 subExpr2 ⇒
 253    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr1 fe map)
 254     (λres1.opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr2 fe map)
 255      (λres2.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_NEQ fe bType res1 res2) t))
 256
 257   | AST_EXPR_B8toW16 subExpr ⇒
 258    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
 259     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_B8toW16 fe res) t)
 260   | AST_EXPR_B8toW32 subExpr ⇒
 261    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) subExpr fe map)
 262     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_B8toW32 fe res) t)
 263   | AST_EXPR_W16toB8 subExpr ⇒
 264    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
 265     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W16toB8 fe res) t)
 266   | AST_EXPR_W16toW32 subExpr ⇒
 267    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) subExpr fe map)
 268     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD32) (ASTFE_EXPR_W16toW32 fe res) t)
 269   | AST_EXPR_W32toB8 subExpr ⇒
 270    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
 271     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (ASTFE_EXPR_W32toB8 fe res) t)
 272   | AST_EXPR_W32toW16 subExpr ⇒
 273    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) subExpr fe map)
 274     (λres.ast_to_astfe_expr_check fe (AST_TYPE_BASE AST_BASE_TYPE_WORD16) (ASTFE_EXPR_W32toW16 fe res) t)
 275
 276   | AST_EXPR_ID b subType var ⇒
 277    opt_map ?? (ast_to_astfe_var e b subType var fe map)
 278     (λres.ast_to_astfe_expr_check fe subType (ASTFE_EXPR_ID fe b subType res) t)
 279   ]
 280 (*
 281  AST_VAR_ID: ∀b:bool.∀t:ast_type.
 282              ast_id e b t → ast_var e b t
 283  AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
 284                 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
 285  AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
 286                  ast_var e b (AST_TYPE_STRUCT nel) → (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
 287 *)
 288 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) ≝
 289  match ast with
 290   [ AST_VAR_ID subB subType subId ⇒
 291    opt_map ?? (ast_to_astfe_id_check fe ?? (ast_to_astfe_id e subB subType subId fe map) subB subType)
 292     (λresId.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ID fe subB subType resId) b t)
 293
 294   | AST_VAR_ARRAY subB subType dim var expr ⇒
 295    opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_ARRAY subType dim) var fe map)
 296     (λresVar.opt_map ?? (ast_to_astfe_base_expr e expr fe map)
 297      (λresExpr.ast_to_astfe_var_check fe subB subType (ASTFE_VAR_ARRAY fe subB subType dim resVar resExpr) b t))
 298
 299   | AST_VAR_STRUCT subB nelSubType field var _ ⇒
 300    opt_map ?? (ast_to_astfe_var e subB (AST_TYPE_STRUCT nelSubType) var fe map)
 301     (λres.ast_to_astfe_var_check fe subB (abs_nth_neList ? nelSubType field) (ASTFE_VAR_STRUCT fe subB nelSubType field res) b t)
 302   ]
 303 (*
 304  AST_BASE_EXPR: ∀t:ast_base_type.
 305                 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e
 306 *)
 307 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) ≝
 308  match ast with
 309   [ AST_BASE_EXPR bType subExpr ⇒
 310    opt_map ?? (ast_to_astfe_expr e (AST_TYPE_BASE bType) subExpr fe map)
 311     (λres.Some ? (ASTFE_BASE_EXPR fe bType res))
 312   ].
 313
 314 (*
 315  AST_INIT_VAR: ∀b:bool.∀t:ast_type.
 316                ast_var e b t → ast_init e t
 317  AST_INIT_VAL: ∀t:ast_type.
 318                aux_ast_init_type t → ast_init e t
 319 *)
 320 definition ast_to_astfe_init : Πe.Πt.ast_init e t → Πfe.aux_trasfMap_type e fe → option (astfe_init fe t) ≝
 321 λe:aux_env_type.λt:ast_type.λast:ast_init e t.λfe:aux_flatEnv_type.λmap:aux_trasfMap_type e fe.
 322  match ast with
 323   [ AST_INIT_VAR subB subType var ⇒
 324    opt_map ?? (ast_to_astfe_var e subB subType var fe map)
 325     (λres.ast_to_astfe_init_check fe subType (ASTFE_INIT_VAR fe subB subType res) t)
 326
 327   | AST_INIT_VAL subType args ⇒ ast_to_astfe_init_check fe subType (ASTFE_INIT_VAL fe subType args) t
 328   ].
 329
 330 (*
 331  AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
 332               ast_var e false t → ast_expr e t → ast_stm e
 333  AST_STM_WHILE: ∀e:aux_env_type.
 334                 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
 335  AST_STM_IF: ∀e:aux_env_type.
 336              ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
 337 *)
 338 (* NB: il lemma dovrebbe poi prendere in input la dimostrazione che fe <= fe', cosi' ha senso *)
 339 axiom retype_base_expr: ∀fe,fe'.astfe_base_expr fe → astfe_base_expr fe'.
 340 axiom retype_init: ∀t,fe,fe'.astfe_init fe t → astfe_init fe' t.
 341 axiom retype_list_decl: ∀fe,fe'.list (astfe_stm fe) → list (astfe_stm fe').
 342 axiom retype_neList_body: ∀fe,fe'.ne_list (Prod (astfe_base_expr fe) (astfe_body fe)) → ne_list (Prod (astfe_base_expr fe') (astfe_body fe')).
 343
 344 (* applicare l'identita' e' inifluente *)
 345 lemma retype_map_to_id : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:(aux_env_type → aux_env_type).
 346                          aux_trasfMap_type e fe → e = f e → aux_trasfMap_type (f e) fe.
 347  intros;
 348  apply (eq_rect ? e (λHbeta1:aux_env_type.aux_trasfMap_type Hbeta1 fe) a (f e) H);
 349 qed.
 350
 351 axiom how_to_build_it : ∀e:aux_env_type.∀fe:aux_flatEnv_type.∀f:aux_env_type → aux_env_type.∀map:aux_trasfMap_type (f e) fe.∀ll:list (astfe_stm fe).
 352  (sigma (aux_env_type\to aux_env_type)
 353   (\lambda f:(aux_env_type\to aux_env_type).
 354    (sigma aux_flatEnv_type
 355     (\lambda fe':aux_flatEnv_type.
 356      (Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe'))))))).
 357
 358 let rec ast_to_astfe_stm (e:aux_env_type) (ast:ast_stm e) (fe:aux_flatEnv_type) on ast
 359  : Πmap:aux_trasfMap_type e fe.option (Σfe'.Prod (aux_trasfMap_type e fe') (astfe_stm fe')) ≝
 360  match ast
 361   return λe':aux_env_type.λ_:ast_stm e'.aux_trasfMap_type e' fe → option (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 362  with
 363   [ AST_STM_ASG e' subType var expr ⇒
 364    λmap:aux_trasfMap_type e' fe.
 365     opt_map ?? (ast_to_astfe_var e' false subType var fe map)
 366      (λresVar.opt_map ?? (ast_to_astfe_expr e' subType expr fe map)
 367       (λresExpr.Some ? (≪fe,(pair ?? map (ASTFE_STM_ASG fe subType resVar resExpr))≫)))
 368
 369   | AST_STM_WHILE e' expr decl ⇒
 370    λmap:aux_trasfMap_type e' fe.
 371     opt_map ?? (ast_to_astfe_base_expr e' expr fe map)
 372      (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe (retype_e_to_enter e' fe map))
 373       (λsigmaRes:(Σf.(Σfe'. Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 374        [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 375         [ sigma_intro fe' mapAndStm ⇒ match mapAndStm with
 376          [ pair map' resDecl ⇒
 377           Some ? (≪fe',pair ?? (rollback_map e' fe fe' f (retype_e_to_leave ?? map') map)
 378                                 (ASTFE_STM_WHILE fe' (retype_base_expr fe fe' resExpr) (ASTFE_BODY fe' resDecl))≫)
 379          ]]]))
 380
 381   | AST_STM_IF e' nelExprDecl optDecl ⇒
 382    λmap:aux_trasfMap_type e' fe.
 383     let rec aux (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv)
 384                 (nel:ne_list (Prod (ast_base_expr e') (ast_decl (enter_env e')))) on nel ≝
 385      match nel with
 386       [ ne_nil h ⇒
 387        opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
 388         (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
 389          (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 390           [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 391            [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
 392             [ pair m' resDecl ⇒
 393              Some ? (≪fenv',pair ?? (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m)
 394                                      « pair ?? (retype_base_expr fenv fenv' resExpr) (ASTFE_BODY fenv' resDecl) £»≫)
 395             ]]]))
 396
 397       | ne_cons h tl ⇒
 398        opt_map ?? (ast_to_astfe_base_expr e' (fst ?? h) fenv m)
 399         (λresExpr.opt_map ?? (ast_to_astfe_decl (enter_env e') (snd ?? h) fenv (retype_e_to_enter e' fenv m))
 400          (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes with
 401           [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 402            [ sigma_intro fenv' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fenv') (list (astfe_stm fenv'))) ⇒ match mapAndStm with
 403             [ pair m' resDecl ⇒
 404              opt_map ?? (aux fenv' (rollback_map e' fenv fenv' f (retype_e_to_leave ?? m') m) tl)
 405               (λsigmaRes':(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes' with
 406                [ sigma_intro fenv'' mapAndProd ⇒ match mapAndProd with
 407                 [ pair m'' tl' ⇒
 408                  Some ? (≪fenv'',pair ?? m''
 409                                           (« pair ?? (retype_base_expr fenv fenv'' resExpr)
 410                                                      (ASTFE_BODY fenv'' (retype_list_decl fenv' fenv'' resDecl)) £»&tl')≫)
 411                 ]])]]]))
 412       ] in
 413     opt_map ?? (aux fe map nelExprDecl)
 414      (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))).match sigmaRes with
 415       [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type e' fe') (ne_list (Prod (astfe_base_expr fe') (astfe_body fe')))) ⇒ match mapAndStm with
 416        [ pair (m':aux_trasfMap_type e' fe') resNel ⇒ match optDecl with
 417         [ None ⇒ Some ? (≪fe',pair ?? m' (ASTFE_STM_IF fe' resNel (None ?))≫)
 418         | Some decl ⇒
 419          opt_map ?? (ast_to_astfe_decl (enter_env e') decl fe' (retype_e_to_enter e' fe' m'))
 420           (λsigmaRes':(Σf'.(Σfe'.Prod (aux_trasfMap_type (f' (enter_env e')) fe') (list (astfe_stm fe')))).match sigmaRes' with
 421            [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f (enter_env e')) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 422             [ sigma_intro fe'' (mapAndStm:Prod (aux_trasfMap_type (f (enter_env e')) fe'') (list (astfe_stm fe''))) ⇒ match mapAndStm with
 423              [ pair (m'':aux_trasfMap_type (f (enter_env e')) fe'') (resDecl:list (astfe_stm fe'')) ⇒
 424               Some (Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe'))
 425                (≪fe'',pair ?? (rollback_map e' fe' fe'' f (retype_e_to_leave ?? m'') m')
 426                                (ASTFE_STM_IF fe'' (retype_neList_body fe' fe'' resNel) (Some ? (ASTFE_BODY fe'' resDecl)))≫)
 427              ]]])]]])
 428   ]
 429 (*
 430  AST_NO_DECL: ∀e:aux_env_type.
 431               list (ast_stm e) → ast_decl e
 432  AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
 433            (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e
 434 *)
 435 and ast_to_astfe_decl (e:aux_env_type) (ast:ast_decl e) (fe:aux_flatEnv_type) on ast
 436  : Πmap:aux_trasfMap_type e fe.option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e) fe') (list (astfe_stm fe')))) ≝
 437  match ast
 438   return λe':aux_env_type.λ_:ast_decl e'.aux_trasfMap_type e' fe → option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe'))))
 439  with
 440   [ AST_NO_DECL e' lStm ⇒
 441    λmap:aux_trasfMap_type e' fe.
 442     let rec aux (ll:list (ast_stm e')) (fenv:aux_flatEnv_type) (m:aux_trasfMap_type e' fenv) on ll
 443      : option (Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ≝
 444      match ll with
 445       [ nil ⇒ Some ? (how_to_build_it e' fenv (λx.x) (retype_map_to_id e' fenv (λx.x) m (refl_eq ??)) [])
 446       | cons h tl ⇒
 447        opt_map ?? (ast_to_astfe_stm e' h fenv m)
 448         (λsigmaRes:(Σfe'.Prod (aux_trasfMap_type e' fe') (astfe_stm fe')).match sigmaRes with
 449          [ sigma_intro fenv' mapAndStm ⇒ match mapAndStm with
 450           [ pair m' resStm ⇒
 451            opt_map ?? (aux tl fenv' m')
 452             (λsigmaRes':(Σf.(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))).match sigmaRes' with
 453              [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f e') fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
 454               [ sigma_intro fenv'' (mapAndStm':Prod (aux_trasfMap_type (f e') fenv'') (list (astfe_stm fenv''))) ⇒ match mapAndStm' with
 455                [ pair m'' tl' ⇒
 456                Some ? (how_to_build_it e' fenv'' f m''
 457                                        ((retype_list_decl fenv' fenv'' [ resStm ])@tl'))
 458                ]]])]])] in
 459     aux lStm fe map
 460
 461   | AST_DECL e' b name t _ optInit subDecl ⇒
 462    λmap:aux_trasfMap_type e' fe.
 463     opt_map ?? (match optInit with
 464                 [ None ⇒ Some ? []
 465                 | Some init ⇒
 466                  opt_map ?? (ast_to_astfe_init e' t init fe map)
 467                   (λresInit.opt_map ?? (ast_to_astfe_id_check (add_desc_flatEnv fe (next_nameId e' fe map name) b t) ??
 468                                                               (ASTFE_ID (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 469                                                                         (next_nameId e' fe map name)
 470                                                                         (False_rect ? daemon))
 471                                                               b t)
 472                    (λresId.Some ? ([ ASTFE_STM_INIT (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 473                                                      b t resId
 474                                                      (retype_init t fe (add_desc_flatEnv fe (next_nameId e' fe map name) b t) resInit)
 475                                                      ])))
 476                 ])
 477      (λhRes.opt_map ?? (ast_to_astfe_decl (add_desc_env e' name b t) subDecl
 478                                           (add_desc_flatEnv fe (next_nameId e' fe map name) b t)
 479                                           (add_maxcur_map e' fe map map name b t))
 480       (λsigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))).match sigmaRes with
 481        [ sigma_intro f (feAndMapStm:(Σfe'.Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe')))) ⇒ match feAndMapStm with
 482         [ sigma_intro fe' (mapAndStm:Prod (aux_trasfMap_type (f (add_desc_env e' name b t)) fe') (list (astfe_stm fe'))) ⇒ match mapAndStm with
 483          [ pair map' tRes ⇒
 484           Some ? (how_to_build_it e' fe' (λx.f (add_desc_env x name b t)) map'
 485                                   ((retype_list_decl (add_desc_flatEnv fe (next_nameId e' fe map name) b t) fe' hRes)@tRes))
 486          ]]]))
 487   ].
 488
 489 (*
 490  AST_ROOT: ast_decl empty_env → ast_root.
 491 *)
 492 definition ast_to_astfe : ast_root → (Σfe.astfe_root fe) ≝
 493 λast:ast_root.match ast with
 494  [ AST_ROOT decl ⇒ match ast_to_astfe_decl empty_env decl empty_flatEnv (empty_trasfMap empty_env empty_flatEnv) with
 495   (* impossibile: dummy *)
 496   [ None ⇒ ≪empty_flatEnv,empty_astfe_prog≫
 497   | Some (sigmaRes:(Σf.(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe'))))) ⇒ match sigmaRes with
 498    [ sigma_intro f (feMapAndStm:(Σfe'.Prod (aux_trasfMap_type (f empty_env) fe') (list (astfe_stm fe')))) ⇒ match feMapAndStm with
 499     [ sigma_intro fe (mapAndStm:Prod (aux_trasfMap_type (f empty_env) fe) (list (astfe_stm fe))) ⇒ match mapAndStm with
 500      [ pair map resStm ⇒ ≪fe,(ASTFE_ROOT fe (ASTFE_BODY fe resStm))≫
 501      ]]]]].
 502
 503 (* mini test *)
 504 (*include "compiler/preast_tree.ma".
 505 include "compiler/preast_to_ast.ma".*)
 506
 507 (*
 508 { const byte8 a;
 509   const byte8[3] b={0,1,2};
 510   byte8[3] c=b;
 511
 512   if(0xF0)
 513    { byte8 a=a; }
 514   else if(0xF1)
 515    {
 516    while(0x10)
 517     { byte8[3] b=c; }
 518    }
 519   else if(0xF2)
 520    { byte8 a=b[0]; }
 521   else
 522    { const byte8 a=a; }
 523 }
 524 *)
 525 (*
 526 definition prova ≝
 527 PREAST_ROOT (
 528  PREAST_DECL true [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (None ?) (
 529   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〉)»))) (
 530    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]))) (
 531     PREAST_NO_DECL [
 532      PREAST_STM_IF «
 533        (pair ??
 534        (PREAST_EXPR_BYTE8 〈xF,x2〉)
 535        (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 []))
 536        )
 537      £ (pair ??
 538        (PREAST_EXPR_BYTE8 〈xF,x0〉)
 539        (PREAST_DECL false [ch_A] (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) (Some ? (PREAST_INIT_VAR (PREAST_VAR_ID [ch_A]))) (PREAST_NO_DECL []))
 540        )
 541      ; (pair ??
 542        (PREAST_EXPR_BYTE8 〈xF,x1〉)
 543        (PREAST_NO_DECL [
 544         (PREAST_STM_WHILE (PREAST_EXPR_BYTE8 〈x1,x0〉) (
 545         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 [])
 546         ))
 547        ])
 548        )
 549      » (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 [])))
 550     ]
 551    )
 552   )
 553  )
 554 ).
 555
 556 lemma provacheck : opt_map ?? (preast_to_ast prova) (λres.Some ? (ast_to_astfe res)) = None ?.
 557 normalize;
 558 *)