helm/software/matita/contribs/assembly/compiler/preast_to_ast.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/preast_tree.ma".
  23 include "compiler/ast_tree.ma".
  24
  25 (* *********************** *)
  26 (* PASSO 1 DI COMPILAZIONE *)
  27 (* *********************** *)
  28
  29 (*
  30  PREAST_VAR_ID: aux_str_type → preast_var
  31  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
  32  PREAST_VAR_STRUCT: ne_list preast_var → nat → preast_var.
  33 *)
  34 let rec evaluate_var_type (preast:preast_var) (e:aux_env_type) on preast : option (Prod bool ast_type) ≝
  35  match preast with
  36   [ PREAST_VAR_ID name ⇒
  37    opt_map ?? (get_desc_env_aux e (None ?) name)
  38     (λdesc.Some ? (pair ?? (get_const_desc desc) (get_type_desc desc)))
  39   | PREAST_VAR_ARRAY subVar expr ⇒
  40    opt_map ?? (evaluate_var_type subVar e)
  41     (λcDesc.match snd ?? cDesc with
  42      [ AST_TYPE_ARRAY subType dim ⇒ Some ? (pair ?? (fst ?? cDesc) subType)
  43      | _ ⇒ None ? ])
  44   | PREAST_VAR_STRUCT subVar field ⇒
  45    opt_map ?? (evaluate_var_type subVar e)
  46     (λcDesc.match snd ?? cDesc with
  47      [ AST_TYPE_STRUCT nelSubType ⇒
  48       opt_map ?? (nth_neList ? nelSubType field)
  49        (λsubType.Some ? (pair ?? (fst ?? cDesc) subType))
  50      | _ ⇒ None ? ])
  51   ].
  52
  53 (*
  54  PREAST_EXPR_BYTE8 : byte8 → preast_expr
  55  PREAST_EXPR_WORD16: word16 → preast_expr
  56  PREAST_EXPR_WORD32: word32 → preast_expr
  57  PREAST_EXPR_NEG: preast_expr → preast_expr
  58  PREAST_EXPR_NOT: preast_expr → preast_expr
  59  PREAST_EXPR_COM: preast_expr → preast_expr
  60  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
  61  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
  62  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
  63  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
  64  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
  65  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
  66  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
  67  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
  68  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
  69  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
  70  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
  71  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
  72  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
  73  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
  74  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
  75  PREAST_EXPR_W16toW32: preast_expr → preast_expr
  76  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
  77  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  78  PREAST_EXPR_ID: preast_var → preast_expr
  79 *)
  80 let rec evaluate_expr_type (preast:preast_expr) (e:aux_env_type) on preast : option ast_base_type ≝
  81  match preast with
  82   [ PREAST_EXPR_BYTE8 _ ⇒ Some ? AST_BASE_TYPE_BYTE8
  83   | PREAST_EXPR_WORD16 _ ⇒ Some ? AST_BASE_TYPE_WORD16
  84   | PREAST_EXPR_WORD32 _ ⇒ Some ? AST_BASE_TYPE_WORD32
  85   | PREAST_EXPR_NEG subExpr ⇒ evaluate_expr_type subExpr e
  86   | PREAST_EXPR_NOT subExpr ⇒ evaluate_expr_type subExpr e
  87   | PREAST_EXPR_COM subExpr ⇒ evaluate_expr_type subExpr e
  88   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
  89    opt_map ?? (evaluate_expr_type subExpr1 e)
  90     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
  91      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
  92   | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
  93    opt_map ?? (evaluate_expr_type subExpr1 e)
  94     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
  95      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
  96   | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
  97    opt_map ?? (evaluate_expr_type subExpr1 e)
  98     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
  99      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
 100   | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
 101    opt_map ?? (evaluate_expr_type subExpr1 e)
 102     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 103      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
 104   | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
 105    opt_map ?? (evaluate_expr_type subExpr1 e)
 106     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 107      (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
 108   | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
 109    opt_map ?? (evaluate_expr_type subExpr1 e)
 110     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 111      (λt2.match eq_ast_base_type t2 AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? t1 | false ⇒ None ? ]))
 112   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
 113    opt_map ?? (evaluate_expr_type subExpr1 e)
 114     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 115      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 116   | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
 117    opt_map ?? (evaluate_expr_type subExpr1 e)
 118     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 119      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 120   | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
 121    opt_map ?? (evaluate_expr_type subExpr1 e)
 122     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 123      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 124   | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
 125    opt_map ?? (evaluate_expr_type subExpr1 e)
 126     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 127      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 128   | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
 129    opt_map ?? (evaluate_expr_type subExpr1 e)
 130     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 131      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 132   | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
 133    opt_map ?? (evaluate_expr_type subExpr1 e)
 134     (λt1.opt_map ?? (evaluate_expr_type subExpr2 e)
 135      (λt2.match eq_ast_base_type t1 t2 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ]))
 136   | PREAST_EXPR_B8toW16 subExpr ⇒
 137    opt_map ?? (evaluate_expr_type subExpr e)
 138     (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
 139   | PREAST_EXPR_B8toW32 subExpr ⇒
 140    opt_map ?? (evaluate_expr_type subExpr e)
 141     (λt.match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
 142   | PREAST_EXPR_W16toB8 subExpr ⇒
 143    opt_map ?? (evaluate_expr_type subExpr e)
 144     (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
 145   | PREAST_EXPR_W16toW32 subExpr ⇒
 146    opt_map ?? (evaluate_expr_type subExpr e)
 147     (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD16 with [ true ⇒ Some ? AST_BASE_TYPE_WORD32 | false ⇒ None ? ])
 148   | PREAST_EXPR_W32toB8 subExpr ⇒
 149    opt_map ?? (evaluate_expr_type subExpr e)
 150     (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_BYTE8 | false ⇒ None ? ])
 151   | PREAST_EXPR_W32toW16 subExpr ⇒
 152    opt_map ?? (evaluate_expr_type subExpr e)
 153     (λt.match eq_ast_base_type t AST_BASE_TYPE_WORD32 with [ true ⇒ Some ? AST_BASE_TYPE_WORD16 | false ⇒ None ? ])
 154   | PREAST_EXPR_ID var ⇒
 155    opt_map ?? (evaluate_var_type var e)
 156     (λcDesc.match snd ?? cDesc with [ AST_TYPE_BASE bType ⇒ Some ? bType | _ ⇒ None ? ])
 157   ].
 158
 159 (*
 160  PREAST_EXPR_BYTE8 : byte8 → preast_expr
 161  PREAST_EXPR_WORD16: word16 → preast_expr
 162  PREAST_EXPR_WORD32: word32 → preast_expr
 163  PREAST_EXPR_NEG: preast_expr → preast_expr
 164  PREAST_EXPR_NOT: preast_expr → preast_expr
 165  PREAST_EXPR_COM: preast_expr → preast_expr
 166  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
 167  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
 168  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
 169  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 170  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 171  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
 172  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 173  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
 174  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
 175  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
 176  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
 177  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
 178  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
 179  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
 180  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
 181  PREAST_EXPR_W16toW32: preast_expr → preast_expr
 182  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
 183  PREAST_EXPR_W32toW16: preast_expr → preast_expr
 184  PREAST_EXPR_ID: preast_var → preast_expr
 185 *)
 186 let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) (t:ast_base_type) on preast : option (ast_expr e t) ≝
 187  (*match preast
 188   return λpr:preast_expr.λen:aux_env_type.λtp:ast_base_type.(match pr with
 189    [ PREAST_EXPR_BYTE8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 190    | PREAST_EXPR_WORD16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
 191    | PREAST_EXPR_WORD32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
 192    | PREAST_EXPR_NEG _ ⇒ option (ast_expr en tp)
 193    | PREAST_EXPR_NOT _ ⇒ option (ast_expr en tp)
 194    | PREAST_EXPR_COM _ ⇒ option (ast_expr en tp)
 195    | PREAST_EXPR_ADD _ ⇒ option (ast_expr en tp)
 196    | PREAST_EXPR_SUB _ ⇒ option (ast_expr en tp)
 197    | PREAST_EXPR_MUL _ ⇒ option (ast_expr en tp)
 198    | PREAST_EXPR_DIV _ ⇒ option (ast_expr en tp)
 199    | PREAST_EXPR_SHR _ ⇒ option (ast_expr en tp)
 200    | PREAST_EXPR_SHL _ ⇒ option (ast_expr en tp)
 201    | PREAST_EXPR_GT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 202    | PREAST_EXPR_GTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 203    | PREAST_EXPR_LT _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 204    | PREAST_EXPR_LTE _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 205    | PREAST_EXPR_EQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 206    | PREAST_EXPR_NEQ _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 207    | PREAST_EXPR_B8toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
 208    | PREAST_EXPR_B8toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
 209    | PREAST_EXPR_W16toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 210    | PREAST_EXPR_W16toW32 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD32)
 211    | PREAST_EXPR_W32toB8 _ ⇒ option (ast_expr en AST_BASE_TYPE_BYTE8)
 212    | PREAST_EXPR_W32toW16 _ ⇒ option (ast_expr en AST_BASE_TYPE_WORD16)
 213    | PREAST_EXPR_ID _ ⇒ option (ast_expr en tp)
 214    | _ ⇒ option (ast_expr en tp)
 215    ])
 216  with
 217   [ PREAST_EXPR_BYTE8 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 218    [ true ⇒ Some ? (AST_EXPR_BYTE8 e val) | false ⇒ None ? ]
 219   | PREAST_EXPR_WORD16 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 220    [ true ⇒ Some ? (AST_EXPR_WORD16 e val) | false ⇒ None ? ]
 221   | PREAST_EXPR_WORD32 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 222    [ true ⇒ Some ? (AST_EXPR_WORD32 e val) | false ⇒ None ? ]
 223   | PREAST_EXPR_NEG subExpr ⇒
 224    opt_map ?? (preast_to_ast_expr subExpr e t)
 225     (λres.Some ? (AST_EXPR_NEG e t res))
 226   | PREAST_EXPR_NOT subExpr ⇒
 227    opt_map ?? (preast_to_ast_expr subExpr e t)
 228     (λres.Some ? (AST_EXPR_NOT e t res))
 229   | PREAST_EXPR_COM subExpr ⇒
 230    opt_map ?? (preast_to_ast_expr subExpr e t)
 231     (λres.Some ? (AST_EXPR_COM e t res))
 232   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
 233    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 234     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 235      (λres2.Some ? (AST_EXPR_ADD e t res1 res2)))
 236   | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
 237    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 238     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 239      (λres2.Some ? (AST_EXPR_SUB e t res1 res2)))
 240   | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
 241    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 242     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 243      (λres2.Some ? (AST_EXPR_MUL e t res1 res2)))
 244   | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
 245    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 246     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 247      (λres2.Some ? (AST_EXPR_DIV e t res1 res2)))
 248   | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
 249    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 250     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
 251      (λres2.Some ? (AST_EXPR_SHR e t res1 res2)))
 252   | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
 253    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 254     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
 255      (λres2.Some ? (AST_EXPR_SHL e t res1 res2)))
 256   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 257    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 258              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 259               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 260                (λres2.Some ? (AST_EXPR_GT e resType res1 res2))))
 261    | false ⇒ None ? ]
 262   | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 263    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 264              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 265               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 266                (λres2.Some ? (AST_EXPR_GTE e resType res1 res2))))
 267    | false ⇒ None ? ]
 268   | PREAST_EXPR_LT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 269    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 270              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 271               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 272                (λres2.Some ? (AST_EXPR_LT e resType res1 res2))))
 273    | false ⇒ None ? ]
 274   | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 275    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 276              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 277               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 278                (λres2.Some ? (AST_EXPR_LTE e resType res1 res2))))
 279    | false ⇒ None ? ]
 280   | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 281    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 282              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 283               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 284                (λres2.Some ? (AST_EXPR_EQ e resType res1 res2))))
 285    | false ⇒ None ? ]
 286   | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 287    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 288              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 289               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 290                (λres2.Some ? (AST_EXPR_NEQ e resType res1 res2))))
 291    | false ⇒ None ? ]
 292   | PREAST_EXPR_B8toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 293    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
 294     (λres.Some ? (AST_EXPR_B8toW16 e res))
 295    | false ⇒ None ? ]
 296   | PREAST_EXPR_B8toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 297    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
 298     (λres.Some ? (AST_EXPR_B8toW32 e res))
 299    | false ⇒ None ? ]
 300   | PREAST_EXPR_W16toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 301    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
 302     (λres.Some ? (AST_EXPR_W16toB8 e res))
 303    | false ⇒ None ? ]
 304   | PREAST_EXPR_W16toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 305    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
 306     (λres.Some ? (AST_EXPR_W16toW32 e res))
 307    | false ⇒ None ? ]
 308   | PREAST_EXPR_W32toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 309    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
 310     (λres.Some ? (AST_EXPR_W32toB8 e res))
 311    | false ⇒ None ? ]
 312   | PREAST_EXPR_W32toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 313    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
 314     (λres.Some ? (AST_EXPR_W32toW16 e res))
 315    | false ⇒ None ? ]
 316   | PREAST_EXPR_ID var ⇒
 317    opt_map ?? (evaluate_var_type var e)
 318     (λcDesc.opt_map ?? (preast_to_ast_var var e (fst ?? cDesc) (AST_TYPE_BASE t))
 319      (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t res)))
 320   ]*)
 321  None (ast_expr e t)
 322 (*
 323  PREAST_VAR_ID: aux_str_type → preast_var
 324  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
 325  PREAST_VAR_STRUCT: preast_var → nat → preast_var.
 326 *)
 327 and preast_to_ast_var (preast:preast_var) (e:aux_env_type) (c:bool) (t:ast_type) on preast : option (ast_var e c t) ≝
 328  None (ast_var e c t)
 329 (*
 330  PREAST_EXPR_BYTE8 : byte8 → preast_expr
 331  PREAST_EXPR_WORD16: word16 → preast_expr
 332  PREAST_EXPR_WORD32: word32 → preast_expr
 333  PREAST_EXPR_NEG: preast_expr → preast_expr
 334  PREAST_EXPR_NOT: preast_expr → preast_expr
 335  PREAST_EXPR_COM: preast_expr → preast_expr
 336  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
 337  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
 338  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
 339  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 340  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 341  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
 342  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 343  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
 344  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
 345  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
 346  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
 347  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
 348  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
 349  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
 350  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
 351  PREAST_EXPR_W16toW32: preast_expr → preast_expr
 352  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
 353  PREAST_EXPR_W32toW16: preast_expr → preast_expr
 354  PREAST_EXPR_ID: preast_var → preast_expr
 355 *)
 356 and preast_to_ast_base_expr (preast:preast_expr) (e:aux_env_type) on preast : option (ast_base_expr e) ≝
 357  None (ast_base_expr e).
 358
 359 (*
 360  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
 361  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
 362  PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
 363 *)
 364 let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
 365  match preast with
 366   (* (A) assegnamento *)
 367   [ PREAST_STM_ASG var expr ⇒
 368    opt_map ?? (evaluate_var_type var e)
 369     (λcDesc.match fst ?? cDesc with
 370      (* NO: left non deve essere read only *)
 371      [ true ⇒ None ?
 372      (* OK: left e' read write *)
 373      | false ⇒
 374       match isntb_ast_base_type (snd ?? cDesc)
 375        return λx.(isntb_ast_base_type (snd ?? cDesc)) = x → option (ast_stm e)
 376       with
 377       (* (A.1) memcpy *)
 378       [ true ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = true.match expr with
 379        (* OK: right deve essere una var *)
 380        [ PREAST_EXPR_ID subVar ⇒ opt_map ?? (evaluate_var_type subVar e)
 381         (λcDesc'.opt_map ?? (preast_to_ast_var var e false (snd ?? cDesc))
 382          (λresVar.opt_map ?? (preast_to_ast_var subVar e (fst ?? cDesc') (snd ?? cDesc))
 383           (λresVar'.Some ? (AST_STM_MEMCPY_ASG e (fst ?? cDesc') (snd ?? cDesc)
 384                                                (isntbastbasetype_to_isntastbasetype (snd ?? cDesc) p)
 385                                                resVar resVar'))))
 386        (* NO: right non e' una var *)
 387        | _ ⇒ None ? ]
 388       (* (A.2) variabile *)
 389       | false ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = false.match snd ?? cDesc with
 390        [ AST_TYPE_BASE bType ⇒ opt_map ?? (preast_to_ast_expr expr e bType)
 391        (λresExpr.opt_map ?? (preast_to_ast_var var e false (AST_TYPE_BASE bType))
 392         (λresVar.Some ? (AST_STM_ASG e bType resVar resExpr)))
 393        | _ ⇒ None ? ]] (refl_eq ? (isntb_ast_base_type (snd ?? cDesc)))
 394      ])
 395
 396   (* (B) while *)
 397   | PREAST_STM_WHILE expr decl ⇒
 398    opt_map ?? (preast_to_ast_base_expr expr e)
 399     (λresExpr.opt_map ?? (preast_to_ast_decl decl e)
 400      (λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
 401
 402   (* (C) if *)
 403   | PREAST_STM_IF nelExprDecl optDecl ⇒
 404    opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
 405                                      (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) e)
 406                                       (λresDecl.opt_map ?? t
 407                                        (λt'.Some ? («(pair ?? resExpr resDecl)£»&t')))))
 408                                     (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL e (nil ?)))))
 409                                     nelExprDecl)
 410     (λres.match optDecl with
 411      [ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?))
 412      | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl e)
 413       (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
 414      ])
 415   ]
 416 (*
 417  PREAST_NO_DECL: list preast_stm → preast_decl
 418  PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
 419 *)
 420 and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
 421  match preast with
 422   (* (A) nessuna dichiarazione, solo statement *)
 423   [ PREAST_NO_DECL lPreastStm ⇒
 424    opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
 425                                    (λh'.opt_map ?? t
 426                                     (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
 427     (λres.Some ? (AST_NO_DECL e res))
 428
 429   (* (B) dichiarazione *)
 430   | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
 431    match checkb_not_already_def_env e decName
 432     return λx.(checkb_not_already_def_env e decName) = x → option (ast_decl e)
 433    with
 434     (* OK: non era gia' dichiarata *)
 435     [ true ⇒ λp:(checkb_not_already_def_env e decName) = true.
 436      match decType with
 437       (* (B.1) dichiarazione tipo base *)
 438       [ AST_TYPE_BASE decBaseType ⇒ match optInitExpr with
 439        (* (B.1.1) tipo base senza inizializzazione *)
 440        [ None ⇒ opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
 441                  (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
 442                                                 (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 443                                                 (None ?) subRes))
 444        (* (B.1.2) tipo base con inizializzazione *)
 445        | Some initExpr ⇒ opt_map ?? (preast_to_ast_expr initExpr e decBaseType)
 446                           (λinitRes.opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
 447                            (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
 448                                                           (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 449                                                           (None ?) subRes)))
 450        ]
 451       (* (B.2) dichiarazione record/struttura *)
 452       | _ ⇒ match optInitExpr with
 453        (* OK: senza inizializzazione *)
 454        [ None ⇒ match isntb_ast_base_type decType
 455                  return λy.(isntb_ast_base_type decType) = y → option (ast_decl e)
 456                 with
 457                  [ true ⇒ λp':(isntb_ast_base_type decType) = true.
 458                   opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
 459                  (λsubRes.Some ? (AST_DECL e constFlag decName decType
 460                                            (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 461                                            (isntbastbasetype_to_isntastbasetype decType p')
 462                                            subRes))
 463                  | false ⇒ λp':(isntb_ast_base_type decType) = false.None ?
 464                  ] (refl_eq ? (isntb_ast_base_type decType))
 465        (* NO: con inizializzazione *)
 466        | Some _ ⇒ None ?
 467        ]
 468       ]
 469     (* NO: era gia' dichiarata *)
 470     | false ⇒ λp:(checkb_not_already_def_env e decName) = false.None ?
 471     ] (refl_eq ? (checkb_not_already_def_env e decName))
 472   ].
 473
 474 (*
 475  PREAST_ROOT: preast_decl → preast_root.
 476 *)
 477 definition preast_to_ast ≝
 478 λpreast:preast_root.match preast with
 479  [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
 480                        (λres.Some ? (AST_ROOT res)) ].