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 inductive sigma (A:Type) (P:A \to Type) : Type \def
 160     sigma_intro: \forall x:A. P x \to sigma A P.
 161
 162 notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
 163   right associative with precedence 20
 164 for @{ 'Sigma ${default
 165   @{\lambda ${ident i} : $ty. $p}
 166   @{\lambda ${ident i} . $p}}}.
 167
 168 notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
 169   with precedence 20
 170   for ${ default
 171           @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}:$T.$acc)} } }
 172           @{ ${ fold right @{$Px} rec acc @{'Sigma (λ${ident x}.$acc)} } }
 173        }.
 174
 175 notation "\ll term 19 a, break term 19 b \gg"
 176 with precedence 90 for @{'dependent_pair (λx:?.? x) $a $b}.
 177 interpretation "dependent pair" 'dependent_pair \eta.c a b = (sigma_intro _ c a b).
 178
 179
 180 interpretation "sigma" 'Sigma \eta.x = (sigma _ x).
 181
 182
 183 (*
 184  PREAST_EXPR_BYTE8 : byte8 → preast_expr
 185  PREAST_EXPR_WORD16: word16 → preast_expr
 186  PREAST_EXPR_WORD32: word32 → preast_expr
 187  PREAST_EXPR_NEG: preast_expr → preast_expr
 188  PREAST_EXPR_NOT: preast_expr → preast_expr
 189  PREAST_EXPR_COM: preast_expr → preast_expr
 190  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
 191  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
 192  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
 193  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 194  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 195  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
 196  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 197  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
 198  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
 199  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
 200  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
 201  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
 202  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
 203  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
 204  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
 205  PREAST_EXPR_W16toW32: preast_expr → preast_expr
 206  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
 207  PREAST_EXPR_W32toW16: preast_expr → preast_expr
 208  PREAST_EXPR_ID: preast_var → preast_expr
 209 *)
 210 let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
 211  match preast with
 212   [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8,AST_EXPR_BYTE8 e val≫
 213   | _ ⇒ None ? (*
 214   match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 215    [ true ⇒ Some ? (AST_EXPR_BYTE8 e val) | false ⇒ None ? ]
 216   | PREAST_EXPR_WORD16 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 217    [ true ⇒ Some ? (AST_EXPR_WORD16 e val) | false ⇒ None ? ]
 218   | PREAST_EXPR_WORD32 val ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 219    [ true ⇒ Some ? (AST_EXPR_WORD32 e val) | false ⇒ None ? ]
 220   | PREAST_EXPR_NEG subExpr ⇒
 221    opt_map ?? (preast_to_ast_expr subExpr e t)
 222     (λres.Some ? (AST_EXPR_NEG e t res))
 223   | PREAST_EXPR_NOT subExpr ⇒
 224    opt_map ?? (preast_to_ast_expr subExpr e t)
 225     (λres.Some ? (AST_EXPR_NOT e t res))
 226   | PREAST_EXPR_COM subExpr ⇒
 227    opt_map ?? (preast_to_ast_expr subExpr e t)
 228     (λres.Some ? (AST_EXPR_COM e t res))
 229   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
 230    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 231     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 232      (λres2.Some ? (AST_EXPR_ADD e t res1 res2)))
 233   | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
 234    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 235     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 236      (λres2.Some ? (AST_EXPR_SUB e t res1 res2)))
 237   | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
 238    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 239     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 240      (λres2.Some ? (AST_EXPR_MUL e t res1 res2)))
 241   | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
 242    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 243     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e t)
 244      (λres2.Some ? (AST_EXPR_DIV e t res1 res2)))
 245   | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
 246    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 247     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
 248      (λres2.Some ? (AST_EXPR_SHR e t res1 res2)))
 249   | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
 250    opt_map ?? (preast_to_ast_expr subExpr1 e t)
 251     (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e AST_BASE_TYPE_BYTE8)
 252      (λres2.Some ? (AST_EXPR_SHL e t res1 res2)))
 253   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 254    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 255              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 256               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 257                (λres2.Some ? (AST_EXPR_GT e resType res1 res2))))
 258    | false ⇒ None ? ]
 259   | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 260    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 261              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 262               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 263                (λres2.Some ? (AST_EXPR_GTE e resType res1 res2))))
 264    | false ⇒ None ? ]
 265   | PREAST_EXPR_LT subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 266    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 267              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 268               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 269                (λres2.Some ? (AST_EXPR_LT e resType res1 res2))))
 270    | false ⇒ None ? ]
 271   | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 272    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 273              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 274               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 275                (λres2.Some ? (AST_EXPR_LTE e resType res1 res2))))
 276    | false ⇒ None ? ]
 277   | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 278    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 279              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 280               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 281                (λres2.Some ? (AST_EXPR_EQ e resType res1 res2))))
 282    | false ⇒ None ? ]
 283   | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 284    [ true ⇒ opt_map ?? (evaluate_expr_type subExpr1 e)
 285              (λresType.opt_map ?? (preast_to_ast_expr subExpr1 e resType)
 286               (λres1.opt_map ?? (preast_to_ast_expr subExpr2 e resType)
 287                (λres2.Some ? (AST_EXPR_NEQ e resType res1 res2))))
 288    | false ⇒ None ? ]
 289   | PREAST_EXPR_B8toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 290    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
 291     (λres.Some ? (AST_EXPR_B8toW16 e res))
 292    | false ⇒ None ? ]
 293   | PREAST_EXPR_B8toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 294    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_BYTE8)
 295     (λres.Some ? (AST_EXPR_B8toW32 e res))
 296    | false ⇒ None ? ]
 297   | PREAST_EXPR_W16toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 298    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
 299     (λres.Some ? (AST_EXPR_W16toB8 e res))
 300    | false ⇒ None ? ]
 301   | PREAST_EXPR_W16toW32 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD32 with
 302    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD16)
 303     (λres.Some ? (AST_EXPR_W16toW32 e res))
 304    | false ⇒ None ? ]
 305   | PREAST_EXPR_W32toB8 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_BYTE8 with
 306    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
 307     (λres.Some ? (AST_EXPR_W32toB8 e res))
 308    | false ⇒ None ? ]
 309   | PREAST_EXPR_W32toW16 subExpr ⇒ match eq_ast_base_type t AST_BASE_TYPE_WORD16 with
 310    [ true ⇒ opt_map ?? (preast_to_ast_expr subExpr e AST_BASE_TYPE_WORD32)
 311     (λres.Some ? (AST_EXPR_W32toW16 e res))
 312    | false ⇒ None ? ]
 313   | PREAST_EXPR_ID var ⇒
 314    opt_map ?? (evaluate_var_type var e)
 315     (λcDesc.opt_map ?? (preast_to_ast_var var e (fst ?? cDesc) (AST_TYPE_BASE t))
 316      (λres.Some ? (AST_EXPR_ID e (fst ?? cDesc) t res)))*)
 317   ]
 318 (*
 319  PREAST_VAR_ID: aux_str_type → preast_var
 320  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
 321  PREAST_VAR_STRUCT: preast_var → nat → preast_var.
 322 *)
 323 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) ≝
 324  None (ast_var e c t)
 325 (*
 326  PREAST_EXPR_BYTE8 : byte8 → preast_expr
 327  PREAST_EXPR_WORD16: word16 → preast_expr
 328  PREAST_EXPR_WORD32: word32 → preast_expr
 329  PREAST_EXPR_NEG: preast_expr → preast_expr
 330  PREAST_EXPR_NOT: preast_expr → preast_expr
 331  PREAST_EXPR_COM: preast_expr → preast_expr
 332  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
 333  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
 334  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
 335  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 336  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 337  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
 338  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 339  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
 340  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
 341  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
 342  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
 343  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
 344  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
 345  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
 346  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
 347  PREAST_EXPR_W16toW32: preast_expr → preast_expr
 348  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
 349  PREAST_EXPR_W32toW16: preast_expr → preast_expr
 350  PREAST_EXPR_ID: preast_var → preast_expr
 351 *)
 352 and preast_to_ast_base_expr (preast:preast_expr) (e:aux_env_type) on preast : option (ast_base_expr e) ≝
 353  None (ast_base_expr e).
 354
 355 (*
 356  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
 357  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
 358  PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
 359 *)
 360 let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
 361  match preast with
 362   (* (A) assegnamento *)
 363   [ PREAST_STM_ASG var expr ⇒
 364    opt_map ?? (evaluate_var_type var e)
 365     (λcDesc.match fst ?? cDesc with
 366      (* NO: left non deve essere read only *)
 367      [ true ⇒ None ?
 368      (* OK: left e' read write *)
 369      | false ⇒
 370       match isntb_ast_base_type (snd ?? cDesc)
 371        return λx.(isntb_ast_base_type (snd ?? cDesc)) = x → option (ast_stm e)
 372       with
 373       (* (A.1) memcpy *)
 374       [ true ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = true.match expr with
 375        (* OK: right deve essere una var *)
 376        [ PREAST_EXPR_ID subVar ⇒ opt_map ?? (evaluate_var_type subVar e)
 377         (λcDesc'.opt_map ?? (preast_to_ast_var var e false (snd ?? cDesc))
 378          (λresVar.opt_map ?? (preast_to_ast_var subVar e (fst ?? cDesc') (snd ?? cDesc))
 379           (λresVar'.Some ? (AST_STM_MEMCPY_ASG e (fst ?? cDesc') (snd ?? cDesc)
 380                                                (isntbastbasetype_to_isntastbasetype (snd ?? cDesc) p)
 381                                                resVar resVar'))))
 382        (* NO: right non e' una var *)
 383        | _ ⇒ None ? ]
 384       (* (A.2) variabile *)
 385       | false ⇒ λp:(isntb_ast_base_type (snd ?? cDesc)) = false.match snd ?? cDesc with
 386        [ AST_TYPE_BASE bType ⇒ opt_map ?? (preast_to_ast_expr expr e bType)
 387        (λresExpr.opt_map ?? (preast_to_ast_var var e false (AST_TYPE_BASE bType))
 388         (λresVar.Some ? (AST_STM_ASG e bType resVar resExpr)))
 389        | _ ⇒ None ? ]] (refl_eq ? (isntb_ast_base_type (snd ?? cDesc)))
 390      ])
 391
 392   (* (B) while *)
 393   | PREAST_STM_WHILE expr decl ⇒
 394    opt_map ?? (preast_to_ast_base_expr expr e)
 395     (λresExpr.opt_map ?? (preast_to_ast_decl decl e)
 396      (λresDecl.Some ? (AST_STM_WHILE e resExpr resDecl)))
 397
 398   (* (C) if *)
 399   | PREAST_STM_IF nelExprDecl optDecl ⇒
 400    opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) e)
 401                                      (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) e)
 402                                       (λresDecl.opt_map ?? t
 403                                        (λt'.Some ? («(pair ?? resExpr resDecl)£»&t')))))
 404                                     (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 e 〈x0,x0〉)) (AST_NO_DECL e (nil ?)))))
 405                                     nelExprDecl)
 406     (λres.match optDecl with
 407      [ None ⇒ Some ? (AST_STM_IF e (cut_last_neList ? res) (None ?))
 408      | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl e)
 409       (λresDecl.Some ? (AST_STM_IF e (cut_last_neList ? res) (Some ? resDecl)))
 410      ])
 411   ]
 412 (*
 413  PREAST_NO_DECL: list preast_stm → preast_decl
 414  PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
 415 *)
 416 and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
 417  match preast with
 418   (* (A) nessuna dichiarazione, solo statement *)
 419   [ PREAST_NO_DECL lPreastStm ⇒
 420    opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h e)
 421                                    (λh'.opt_map ?? t
 422                                     (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
 423     (λres.Some ? (AST_NO_DECL e res))
 424
 425   (* (B) dichiarazione *)
 426   | PREAST_DECL constFlag decName decType optInitExpr subPreastDecl ⇒
 427    match checkb_not_already_def_env e decName
 428     return λx.(checkb_not_already_def_env e decName) = x → option (ast_decl e)
 429    with
 430     (* OK: non era gia' dichiarata *)
 431     [ true ⇒ λp:(checkb_not_already_def_env e decName) = true.
 432      match decType with
 433       (* (B.1) dichiarazione tipo base *)
 434       [ AST_TYPE_BASE decBaseType ⇒ match optInitExpr with
 435        (* (B.1.1) tipo base senza inizializzazione *)
 436        [ None ⇒ opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
 437                  (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
 438                                                 (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 439                                                 (None ?) subRes))
 440        (* (B.1.2) tipo base con inizializzazione *)
 441        | Some initExpr ⇒ opt_map ?? (preast_to_ast_expr initExpr e decBaseType)
 442                           (λinitRes.opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag (AST_TYPE_BASE decBaseType)))
 443                            (λsubRes.Some ? (AST_BASE_DECL e constFlag decName decBaseType
 444                                                           (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 445                                                           (None ?) subRes)))
 446        ]
 447       (* (B.2) dichiarazione record/struttura *)
 448       | _ ⇒ match optInitExpr with
 449        (* OK: senza inizializzazione *)
 450        [ None ⇒ match isntb_ast_base_type decType
 451                  return λy.(isntb_ast_base_type decType) = y → option (ast_decl e)
 452                 with
 453                  [ true ⇒ λp':(isntb_ast_base_type decType) = true.
 454                   opt_map ?? (preast_to_ast_decl subPreastDecl (add_desc_env e decName constFlag decType))
 455                  (λsubRes.Some ? (AST_DECL e constFlag decName decType
 456                                            (checkbnotalreadydefenv_to_checknotalreadydefenv e decName p)
 457                                            (isntbastbasetype_to_isntastbasetype decType p')
 458                                            subRes))
 459                  | false ⇒ λp':(isntb_ast_base_type decType) = false.None ?
 460                  ] (refl_eq ? (isntb_ast_base_type decType))
 461        (* NO: con inizializzazione *)
 462        | Some _ ⇒ None ?
 463        ]
 464       ]
 465     (* NO: era gia' dichiarata *)
 466     | false ⇒ λp:(checkb_not_already_def_env e decName) = false.None ?
 467     ] (refl_eq ? (checkb_not_already_def_env e decName))
 468   ].
 469
 470 (*
 471  PREAST_ROOT: preast_decl → preast_root.
 472 *)
 473 definition preast_to_ast ≝
 474 λpreast:preast_root.match preast with
 475  [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
 476                        (λres.Some ? (AST_ROOT res)) ].