matita/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 include "compiler/sigma.ma".
  25
  26 (* ************************* *)
  27 (* PASSO 1 : da PREAST a AST *)
  28 (* ************************* *)
  29
  30 (* NB: ASSERTO
  31    al parser spetta il compito di rigettare le condizioni statiche verificabili
  32     - divisione per valore 0
  33    al parser spetta il compito di collassare le espressioni statiche
  34     - val1+val2 -> val3, ...
  35    al parser spetta il compito di collassare gli statement con condizioni statiche
  36     - if(true) { b1 } else { b2 } -> b1, ...
  37    al parser spetta il compito di individuare divergenza e dead code
  38     - while(true) { b1 } -> loop infinito, ...
  39 *)
  40
  41 (* operatore di cast *)
  42 definition preast_to_ast_expr_check ≝
  43 λd.λe:aux_env_type d.λsig:(Σt'.ast_expr d e t').λt:ast_type.
  44  match sig with [ sigma_intro t' expr ⇒
  45   match eq_ast_type t' t
  46    return λx.eq_ast_type t' t = x → option (ast_expr d e t)
  47   with
  48    [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_expr d e t) expr t (eqasttype_to_eq ?? p))
  49    | false ⇒ λp:(eq_ast_type t' t = false).None ?
  50    ] (refl_eq ? (eq_ast_type t' t))
  51   ].
  52
  53 definition preast_to_ast_init_check ≝
  54 λd.λe:aux_env_type d.λsig:Σt'.ast_init d e t'.λt:ast_type.
  55  match sig with [ sigma_intro t' expr ⇒
  56   match eq_ast_type t' t
  57    return λx.eq_ast_type t' t = x → option (ast_init d e t)
  58   with
  59    [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_init d e t) expr t (eqasttype_to_eq ?? p))
  60    | false ⇒ λp:(eq_ast_type t' t = false).None ?
  61    ] (refl_eq ? (eq_ast_type t' t))
  62   ].
  63
  64 definition preast_to_ast_var_checkb ≝
  65 λd.λe:aux_env_type d.λt:ast_type.λsig:(Σb'.ast_var d e b' t).λb:bool.
  66  match sig with [ sigma_intro b' var ⇒
  67   match eq_bool b' b
  68    return λx.eq_bool b' b = x → option (ast_var d e b t)
  69   with
  70    [ true ⇒ λp:(eq_bool b' b = true).Some ? (eq_rect ? b' (λb.ast_var d e b t) var b (eqbool_to_eq ?? p))
  71    | false ⇒ λp:(eq_bool b' b = false).None ?
  72    ] (refl_eq ? (eq_bool b' b))
  73   ].
  74
  75 definition preast_to_ast_var_checkt ≝
  76 λd.λe:aux_env_type d.λb:bool.λsig:(Σt'.ast_var d e b t').λt:ast_type.
  77  match sig with [ sigma_intro t' var ⇒
  78   match eq_ast_type t' t
  79    return λx.eq_ast_type t' t = x → option (ast_var d e b t)
  80   with
  81    [ true ⇒ λp:(eq_ast_type t' t = true).Some ? (eq_rect ? t' (λt.ast_var d e b t) var t (eqasttype_to_eq ?? p))
  82    | false ⇒ λp:(eq_ast_type t' t = false).None ?
  83    ] (refl_eq ? (eq_ast_type t' t))
  84   ].
  85
  86 definition preast_to_ast_var_check ≝
  87 λd.λe:aux_env_type d.λsig:(Σb'.(Σt'.ast_var d e b' t')).λb:bool.λt:ast_type.
  88  opt_map ?? (preast_to_ast_var_checkt d e (sigmaFst ?? sig) (sigmaSnd ?? sig) t)
  89   (λres1.opt_map ?? (preast_to_ast_var_checkb d e t ≪(sigmaFst ?? sig),res1≫ b)
  90    (λres2.Some ? res2)).
  91
  92 (*
  93  PREAST_EXPR_BYTE8 : byte8 → preast_expr
  94  PREAST_EXPR_WORD16: word16 → preast_expr
  95  PREAST_EXPR_WORD32: word32 → preast_expr
  96  PREAST_EXPR_NEG: preast_expr → preast_expr
  97  PREAST_EXPR_NOT: preast_expr → preast_expr
  98  PREAST_EXPR_COM: preast_expr → preast_expr
  99  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
 100  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
 101  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
 102  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 103  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 104  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
 105  PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr
 106  PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr
 107  PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
 108  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 109  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
 110  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
 111  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
 112  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
 113  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
 114  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
 115  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
 116  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
 117  PREAST_EXPR_W16toW32: preast_expr → preast_expr
 118  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
 119  PREAST_EXPR_W32toW16: preast_expr → preast_expr
 120  PREAST_EXPR_ID: preast_var → preast_expr
 121 *)
 122 let rec preast_to_ast_expr (preast:preast_expr) (d:nat) (e:aux_env_type d) on preast : option (Σt.ast_expr d e t) ≝
 123  match preast with
 124   [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪?,(AST_EXPR_BYTE8 d e val)≫
 125   | PREAST_EXPR_WORD16 val ⇒ Some ? ≪?,(AST_EXPR_WORD16 d e val)≫
 126   | PREAST_EXPR_WORD32 val ⇒ Some ? ≪?,(AST_EXPR_WORD32 d e val)≫
 127
 128   | PREAST_EXPR_NEG subExpr ⇒
 129    opt_map ?? (preast_to_ast_expr subExpr d e)
 130     (λsigmaRes:(Σt.ast_expr d e t).
 131      match (sigmaFst ?? sigmaRes) with
 132       [ AST_TYPE_BASE bType ⇒
 133        opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
 134         (λres.Some ? ≪?,(AST_EXPR_NEG d e ? res)≫)
 135       | _ ⇒ None ? ])
 136   | PREAST_EXPR_NOT subExpr ⇒
 137    opt_map ?? (preast_to_ast_expr subExpr d e)
 138     (λsigmaRes:(Σt.ast_expr d e t).
 139      match (sigmaFst ?? sigmaRes) with
 140       [ AST_TYPE_BASE bType ⇒
 141        opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
 142         (λres.Some ? ≪?,(AST_EXPR_NOT d e ? res)≫)
 143       | _ ⇒ None ? ])
 144   | PREAST_EXPR_COM subExpr ⇒
 145    opt_map ?? (preast_to_ast_expr subExpr d e)
 146     (λsigmaRes:(Σt.ast_expr d e t).
 147      match (sigmaFst ?? sigmaRes) with
 148       [ AST_TYPE_BASE bType ⇒
 149        opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
 150         (λres.Some ? ≪?,(AST_EXPR_COM d e ? res)≫)
 151       | _ ⇒ None ? ])
 152
 153   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
 154    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 155     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 156      (λsigmaRes2:(Σt.ast_expr d e t).
 157       match (sigmaFst ?? sigmaRes1) with
 158        [ AST_TYPE_BASE bType ⇒
 159         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 160          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 161           (λres2.Some ? ≪?,(AST_EXPR_ADD d e ? res1 res2)≫))
 162        | _ ⇒ None ? ]))
 163   | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
 164    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 165     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 166      (λsigmaRes2:(Σt.ast_expr d e t).
 167       match (sigmaFst ?? sigmaRes1) with
 168        [ AST_TYPE_BASE bType ⇒
 169         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 170          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 171           (λres2.Some ? ≪?,(AST_EXPR_SUB d e ? res1 res2)≫))
 172        | _ ⇒ None ? ]))
 173   | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
 174    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 175     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 176      (λsigmaRes2:(Σt.ast_expr d e t).
 177       match (sigmaFst ?? sigmaRes1) with
 178        [ AST_TYPE_BASE bType ⇒
 179         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 180          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 181           (λres2.Some ? ≪?,(AST_EXPR_MUL d e ? res1 res2)≫))
 182        | _ ⇒ None ? ]))
 183   | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
 184    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 185     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 186      (λsigmaRes2:(Σt.ast_expr d e t).
 187       match (sigmaFst ?? sigmaRes1) with
 188        [ AST_TYPE_BASE bType ⇒
 189         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 190          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 191           (λres2.Some ? ≪?,(AST_EXPR_DIV d e ? res1 res2)≫))
 192        | _ ⇒ None ? ]))
 193
 194   | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
 195    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 196     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 197      (λsigmaRes2:(Σt.ast_expr d e t).
 198       match (sigmaFst ?? sigmaRes1) with
 199        [ AST_TYPE_BASE bType ⇒
 200         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 201          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
 202           (λres2.Some ? ≪?,(AST_EXPR_SHR d e ? res1 res2)≫))
 203        | _ ⇒ None ? ]))
 204   | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
 205    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 206     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 207      (λsigmaRes2:(Σt.ast_expr d e t).
 208       match (sigmaFst ?? sigmaRes1) with
 209        [ AST_TYPE_BASE bType ⇒
 210         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 211          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
 212           (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫))
 213        | _ ⇒ None ? ]))
 214   | PREAST_EXPR_AND subExpr1 subExpr2 ⇒
 215    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 216     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 217      (λsigmaRes2:(Σt.ast_expr d e t).
 218       match (sigmaFst ?? sigmaRes1) with
 219        [ AST_TYPE_BASE bType ⇒
 220         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 221          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 222           (λres2.Some ? ≪?,(AST_EXPR_AND d e ? res1 res2)≫))
 223        | _ ⇒ None ? ]))
 224   | PREAST_EXPR_OR subExpr1 subExpr2 ⇒
 225    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 226     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 227      (λsigmaRes2:(Σt.ast_expr d e t).
 228       match (sigmaFst ?? sigmaRes1) with
 229        [ AST_TYPE_BASE bType ⇒
 230         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 231          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 232           (λres2.Some ? ≪?,(AST_EXPR_OR d e ? res1 res2)≫))
 233        | _ ⇒ None ? ]))
 234   | PREAST_EXPR_XOR subExpr1 subExpr2 ⇒
 235    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 236     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 237      (λsigmaRes2:(Σt.ast_expr d e t).
 238       match (sigmaFst ?? sigmaRes1) with
 239        [ AST_TYPE_BASE bType ⇒
 240         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 241          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 242           (λres2.Some ? ≪?,(AST_EXPR_XOR d e ? res1 res2)≫))
 243        | _ ⇒ None ? ]))
 244
 245   | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
 246    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 247     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 248      (λsigmaRes2:(Σt.ast_expr d e t).
 249       match (sigmaFst ?? sigmaRes1) with
 250        [ AST_TYPE_BASE bType ⇒
 251         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 252          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 253           (λres2.Some ? ≪?,(AST_EXPR_GT d e ? res1 res2)≫))
 254        | _ ⇒ None ? ]))
 255   | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
 256    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 257     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 258      (λsigmaRes2:(Σt.ast_expr d e t).
 259       match (sigmaFst ?? sigmaRes1) with
 260        [ AST_TYPE_BASE bType ⇒
 261         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 262          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 263           (λres2.Some ? ≪?,(AST_EXPR_GTE d e ? res1 res2)≫))
 264        | _ ⇒ None ? ]))
 265   | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
 266    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 267     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 268      (λsigmaRes2:(Σt.ast_expr d e t).
 269       match (sigmaFst ?? sigmaRes1) with
 270        [ AST_TYPE_BASE bType ⇒
 271         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 272          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 273           (λres2.Some ? ≪?,(AST_EXPR_LT d e ? res1 res2)≫))
 274        | _ ⇒ None ? ]))
 275   | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
 276    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 277     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 278      (λsigmaRes2:(Σt.ast_expr d e t).
 279       match (sigmaFst ?? sigmaRes1) with
 280        [ AST_TYPE_BASE bType ⇒
 281         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 282          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 283           (λres2.Some ? ≪?,(AST_EXPR_LTE d e ? res1 res2)≫))
 284        | _ ⇒ None ? ]))
 285   | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
 286    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 287     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 288      (λsigmaRes2:(Σt.ast_expr d e t).
 289       match (sigmaFst ?? sigmaRes1) with
 290        [ AST_TYPE_BASE bType ⇒
 291         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 292          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 293           (λres2.Some ? ≪?,(AST_EXPR_EQ d e ? res1 res2)≫))
 294        | _ ⇒ None ? ]))
 295   | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
 296    opt_map ?? (preast_to_ast_expr subExpr1 d e)
 297     (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
 298      (λsigmaRes2:(Σt.ast_expr d e t).
 299       match (sigmaFst ?? sigmaRes1) with
 300        [ AST_TYPE_BASE bType ⇒
 301         opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
 302          (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
 303           (λres2.Some ? ≪?,(AST_EXPR_NEQ d e ? res1 res2)≫))
 304        | _ ⇒ None ? ]))
 305
 306   | PREAST_EXPR_B8toW16 subExpr ⇒
 307    opt_map ?? (preast_to_ast_expr subExpr d e)
 308     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
 309      (λres.Some ? ≪?,(AST_EXPR_B8toW16 d e res)≫))
 310   | PREAST_EXPR_B8toW32 subExpr ⇒
 311    opt_map ?? (preast_to_ast_expr subExpr d e)
 312     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
 313      (λres.Some ? ≪?,(AST_EXPR_B8toW32 d e res)≫))
 314   | PREAST_EXPR_W16toB8 subExpr ⇒
 315    opt_map ?? (preast_to_ast_expr subExpr d e)
 316     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
 317      (λres.Some ? ≪?,(AST_EXPR_W16toB8 d e res)≫))
 318   | PREAST_EXPR_W16toW32 subExpr ⇒
 319    opt_map ?? (preast_to_ast_expr subExpr d e)
 320     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
 321      (λres.Some ? ≪?,(AST_EXPR_W16toW32 d e res)≫))
 322   | PREAST_EXPR_W32toB8 subExpr ⇒
 323    opt_map ?? (preast_to_ast_expr subExpr d e)
 324     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
 325      (λres.Some ? ≪?,(AST_EXPR_W32toB8 d e res)≫))
 326   | PREAST_EXPR_W32toW16 subExpr ⇒
 327    opt_map ?? (preast_to_ast_expr subExpr d e)
 328     (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
 329      (λres.Some ? ≪?,(AST_EXPR_W32toW16 d e res)≫))
 330
 331    | PREAST_EXPR_ID var ⇒
 332    opt_map ?? (preast_to_ast_var var d e)
 333     (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
 334      match sigmaRes with [ sigma_intro b sigmaRes' ⇒
 335       match sigmaRes' with [ sigma_intro t _ ⇒
 336         opt_map ?? (preast_to_ast_var_check d e sigmaRes b t)
 337          (λres.Some ? ≪?,(AST_EXPR_ID d e ?? res)≫)]])
 338   ]
 339 (*
 340  PREAST_VAR_ID: aux_str_type → preast_var
 341  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
 342  PREAST_VAR_STRUCT: preast_var → nat → preast_var
 343 *)
 344 and preast_to_ast_var (preast:preast_var) (d:nat) (e:aux_env_type d) on preast : option (Σb.(Σt.ast_var d e b t)) ≝
 345  match preast with
 346   [ PREAST_VAR_ID name ⇒
 347    match checkb_desc_env d e name
 348     return λx.checkb_desc_env d e name = x → option (Σb.(Σt.ast_var d e b t))
 349    with
 350     [ true ⇒ λp:(checkb_desc_env d e name = true).
 351      let desc ≝ get_desc_env d e name in
 352      let b ≝ get_const_desc desc in
 353      let t ≝ get_type_desc desc in
 354      Some ? ≪b,≪t,(AST_VAR_ID d e b t (AST_ID d e name (checkbdescenv_to_checkdescenv d e name p)))≫≫
 355     | false ⇒ λp:(checkb_desc_env d e name = false).None ?
 356     ] (refl_eq ? (checkb_desc_env d e name))
 357
 358   | PREAST_VAR_ARRAY subVar expr ⇒
 359    opt_map ?? (preast_to_ast_var subVar d e)
 360     (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
 361      match sigmaResV with [ sigma_intro b sigmaResV' ⇒
 362       match sigmaResV' with [ sigma_intro t _ ⇒
 363        match t with
 364         [ AST_TYPE_ARRAY subType dim ⇒
 365          opt_map ?? (preast_to_ast_var_check d e sigmaResV b (AST_TYPE_ARRAY subType dim))
 366           (λresVar.
 367            (* ASSERTO:
 368               1) se l'indice e' un'espressione riducibile ad un valore deve essere gia'
 369                  stato fatto dal parser, e qui controllo la condizione OUT_OF_BOUND
 370               2) se l'indice non e' un'espressione riducibile ad un valore il controllo
 371                  OUT_OF_BOUND sara' fatto a run time
 372            *)
 373            match (match expr with
 374                   [ PREAST_EXPR_BYTE8 val ⇒ (λx.leb (nat_of_byte8 val) dim)
 375                   | PREAST_EXPR_WORD16 val ⇒ (λx.leb (nat_of_word16 val) dim)
 376                   | PREAST_EXPR_WORD32 val ⇒ (λx.leb (nat_of_word32 val) dim)
 377                   | _ ⇒ (λx.true) ]) expr with
 378             [ true ⇒
 379              opt_map ?? (preast_to_ast_expr expr d e)
 380               (λsigmaResE:(Σt.ast_expr d e t).
 381                match sigmaFst ?? sigmaResE with
 382                 [ AST_TYPE_BASE bType ⇒
 383                  opt_map ?? (preast_to_ast_expr_check d e sigmaResE (AST_TYPE_BASE bType))
 384                   (λresExpr.Some ? ≪b,≪subType,(AST_VAR_ARRAY d e b subType dim resVar (AST_BASE_EXPR d e bType resExpr))≫≫)
 385                 | _ ⇒ None ? ])
 386             | false ⇒ None ? ])
 387         | _ ⇒ None ? ]]])
 388
 389   | PREAST_VAR_STRUCT subVar field ⇒
 390    opt_map ?? (preast_to_ast_var subVar d e)
 391     (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
 392      match sigmaRes with [ sigma_intro b sigmaRes' ⇒
 393       match sigmaRes' with [ sigma_intro t _ ⇒
 394        match t with
 395         [ AST_TYPE_STRUCT nelSubType ⇒
 396          opt_map ?? (preast_to_ast_var_check d e sigmaRes b (AST_TYPE_STRUCT nelSubType))
 397           (λresVar.
 398            match ltb field (len_neList ? nelSubType)
 399             return λx.(ltb field (len_neList ? nelSubType) = x) → option (Σb.(Σt.ast_var d e b t))
 400            with
 401             [ true ⇒ λp:(ltb field (len_neList ? nelSubType) = true).
 402              Some ? ≪b,≪(abs_nth_neList ? nelSubType field),(AST_VAR_STRUCT d e b nelSubType field resVar p)≫≫
 403             | false ⇒ λp:(ltb field (len_neList ? nelSubType) = false).None ?
 404             ] (refl_eq ? (ltb field (len_neList ? nelSubType)))
 405           )
 406         | _ ⇒ None ? ]]])
 407   ].
 408
 409 (*
 410  PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
 411  PREAST_INIT_VAL_WORD16: word16 → preast_init_val
 412  PREAST_INIT_VAL_WORD32: word32 → preast_init_val
 413  PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
 414  PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val
 415 *)
 416 definition preast_to_ast_init_val_aux_array :
 417 Πt.Πn.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)) → (aux_ast_init_type (AST_TYPE_ARRAY t (S n))) ≝
 418 λt:ast_type.λn:nat.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_ARRAY t n)).x.
 419
 420 definition preast_to_ast_init_val_aux_struct :
 421 Πt.Πnel.Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)) → (aux_ast_init_type (AST_TYPE_STRUCT («£t»&nel))) ≝
 422 λt:ast_type.λnel:ne_list ast_type.λx:Prod (aux_ast_init_type t) (aux_ast_init_type (AST_TYPE_STRUCT nel)).x.
 423
 424 let rec preast_to_ast_init_val_aux (preast:preast_init_val) on preast : option (Σt.aux_ast_init_type t) ≝
 425  match preast with
 426   [ PREAST_INIT_VAL_BYTE8 val ⇒
 427    Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_BYTE8),val≫
 428   | PREAST_INIT_VAL_WORD16 val ⇒
 429    Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD16),val≫
 430   | PREAST_INIT_VAL_WORD32 val ⇒
 431    Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_BASE AST_BASE_TYPE_WORD32),val≫
 432
 433   | PREAST_INIT_VAL_ARRAY nelSubVal ⇒
 434    let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
 435     match nel with
 436      [ ne_nil h ⇒
 437       opt_map ?? (preast_to_ast_init_val_aux h)
 438        (λsigmaRes.match sigmaRes with [ sigma_intro t res ⇒
 439         Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY t 0),res≫ ])
 440      | ne_cons h tl ⇒
 441       opt_map ?? (preast_to_ast_init_val_aux h)
 442        (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
 443         (λsigmaRes2:(Σt.aux_ast_init_type t).
 444          match sigmaRes1 with [ sigma_intro t1 res1 ⇒
 445           match sigmaRes2 with [ sigma_intro t2 res2 ⇒
 446            match t2 with
 447             [ AST_TYPE_ARRAY bType dim ⇒
 448              match eq_ast_type t1 bType
 449               return λx.(eq_ast_type t1 bType = x) → option (Σt.aux_ast_init_type t)
 450              with
 451               [ true ⇒ λp:(eq_ast_type t1 bType = true).
 452                match eq_ast_type t2 (AST_TYPE_ARRAY bType dim)
 453                 return λy.(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = y) → option (Σt.aux_ast_init_type t)
 454                with
 455                 [ true ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = true).
 456                  Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_ARRAY bType (S dim)),
 457                                                (preast_to_ast_init_val_aux_array bType dim
 458                                                 (pair (aux_ast_init_type bType) (aux_ast_init_type (AST_TYPE_ARRAY bType dim))
 459                                                       (eq_rect ? t1 (λw.aux_ast_init_type w) res1 bType (eqasttype_to_eq ?? p))
 460                                                          (eq_rect ? t2 (λz.aux_ast_init_type z) res2 (AST_TYPE_ARRAY bType dim) (eqasttype_to_eq ?? p'))))≫
 461                 | false ⇒ λp':(eq_ast_type t2 (AST_TYPE_ARRAY bType dim) = false).None ?
 462                 ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_ARRAY bType dim)))
 463               | false ⇒ λp:(eq_ast_type t1 bType = false).None ?
 464               ] (refl_eq ? (eq_ast_type t1 bType))
 465             | _ ⇒ None ?
 466             ]]]))
 467      ] in aux nelSubVal
 468
 469   | PREAST_INIT_VAL_STRUCT nelSubVal ⇒
 470    let rec aux (nel:ne_list preast_init_val) on nel : option (Σt.aux_ast_init_type t) ≝
 471     match nel with
 472      [ ne_nil h ⇒
 473       opt_map ?? (preast_to_ast_init_val_aux h)
 474        (λsigmaRes:(Σt.aux_ast_init_type t).match sigmaRes with [ sigma_intro t res ⇒
 475         Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t»)),res≫ ])
 476      | ne_cons h tl ⇒
 477       opt_map ?? (preast_to_ast_init_val_aux h)
 478        (λsigmaRes1:(Σt.aux_ast_init_type t).opt_map ?? (aux tl)
 479         (λsigmaRes2:(Σt.aux_ast_init_type t).
 480          match sigmaRes1 with [ sigma_intro t1 res1 ⇒
 481           match sigmaRes2 with [ sigma_intro t2 res2 ⇒
 482            match t2 with
 483             [ AST_TYPE_STRUCT nelSubType ⇒
 484              match eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)
 485               return λx.(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = x) → option (Σt.aux_ast_init_type t)
 486              with
 487               [ true ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = true).
 488                Some (Σt.aux_ast_init_type t) ≪(AST_TYPE_STRUCT («£t1»&nelSubType)),
 489                                               (preast_to_ast_init_val_aux_struct ??
 490                                                (pair (aux_ast_init_type t1) (aux_ast_init_type (AST_TYPE_STRUCT nelSubType))
 491                                                      res1
 492                                                      (eq_rect ? t2 (λy.aux_ast_init_type y) res2 (AST_TYPE_STRUCT nelSubType) (eqasttype_to_eq ?? p))))≫
 493               | false ⇒ λp:(eq_ast_type t2 (AST_TYPE_STRUCT nelSubType) = false).None ?
 494               ] (refl_eq ? (eq_ast_type t2 (AST_TYPE_STRUCT nelSubType)))
 495             | _ ⇒ None ? ]]]))
 496      ] in aux nelSubVal
 497   ].
 498
 499 (*
 500  PREAST_INIT_VAR: preast_var → preast_init
 501  PREAST_INIT_VAL: preast_init_val → preast_init
 502 *)
 503 definition preast_to_ast_init : preast_init → Πd.Πe:aux_env_type d.option (Σt.ast_init d e t) ≝
 504 λpreast:preast_init.λd.λe:aux_env_type d.match preast with
 505  [ PREAST_INIT_VAR var ⇒
 506   opt_map ?? (preast_to_ast_var var d e)
 507    (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
 508     Some ? ≪?,(AST_INIT_VAR d e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
 509
 510  | PREAST_INIT_VAL val ⇒
 511   opt_map ?? (preast_to_ast_init_val_aux val)
 512    (λsigmaRes:(Σt.aux_ast_init_type t).
 513     Some ? ≪?,(AST_INIT_VAL d e ? (sigmaSnd ?? sigmaRes))≫)
 514  ].
 515
 516 (*
 517  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
 518  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
 519  PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
 520 *)
 521 definition preast_to_ast_base_expr : preast_expr → Πd.Πe:aux_env_type d.option (ast_base_expr d e) ≝
 522 λpreast:preast_expr.λd.λe:aux_env_type d.
 523  opt_map ?? (preast_to_ast_expr preast d e)
 524   (λsigmaRes:(Σt.ast_expr d e t).
 525    match sigmaFst ?? sigmaRes with
 526     [ AST_TYPE_BASE bType ⇒
 527      opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE bType))
 528       (λres.Some ? (AST_BASE_EXPR d e ? res))
 529     | _ ⇒ None ? ]).
 530
 531 let rec preast_to_ast_stm (preast:preast_stm) (d:nat) (e:aux_env_type d) on preast : option (ast_stm d e) ≝
 532  match preast with
 533   [ PREAST_STM_ASG var expr ⇒
 534    opt_map ?? (preast_to_ast_var var d e)
 535     (λsigmaResV:(Σb.(Σt.ast_var d e b t)).
 536     match sigmaResV with [ sigma_intro _ sigmaResV' ⇒
 537      match sigmaResV' with [ sigma_intro t _ ⇒
 538       opt_map ?? (preast_to_ast_var_check d e sigmaResV false t)
 539        (λresVar.opt_map ?? (preast_to_ast_expr expr d e)
 540         (λsigmaResE:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaResE t)
 541          (λresExpr.Some ? (AST_STM_ASG d e t resVar resExpr)
 542          )))]])
 543
 544   | PREAST_STM_WHILE expr decl ⇒
 545    opt_map ?? (preast_to_ast_base_expr expr d e)
 546     (λresExpr.opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
 547      (λresDecl.Some ? (AST_STM_WHILE d e resExpr resDecl)))
 548
 549   | PREAST_STM_IF nelExprDecl optDecl ⇒
 550    opt_map ?? (fold_right_neList ?? (λh,t.opt_map ?? (preast_to_ast_base_expr (fst ?? h) d e)
 551                                      (λresExpr.opt_map ?? (preast_to_ast_decl (snd ?? h) (S d) (enter_env d e))
 552                                       (λresDecl.opt_map ?? t
 553                                        (λt'.Some ? («£(pair ?? resExpr resDecl)»&t')))))
 554                                     (Some ? (ne_nil ? (pair ?? (AST_BASE_EXPR d e AST_BASE_TYPE_BYTE8 (AST_EXPR_BYTE8 d e 〈x0,x0〉)) (AST_NO_DECL (S d) (enter_env d e) (nil ?)))))
 555                                     nelExprDecl)
 556     (λres.match optDecl with
 557      [ None ⇒ Some ? (AST_STM_IF d e (cut_last_neList ? res) (None ?))
 558      | Some decl ⇒ opt_map ?? (preast_to_ast_decl decl (S d) (enter_env d e))
 559       (λresDecl.Some ? (AST_STM_IF d e (cut_last_neList ? res) (Some ? resDecl)))
 560      ])
 561   ]
 562 (*
 563  PREAST_NO_DECL: list preast_stm → preast_decl
 564  PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
 565  PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl
 566 *)
 567 and preast_to_ast_decl (preast:preast_decl) (d:nat) (e:aux_env_type d) on preast : option (ast_decl d e) ≝
 568  match preast with
 569   [ PREAST_NO_DECL lPreastStm ⇒
 570     opt_map ?? (fold_right_list ?? (λh,t.opt_map ?? (preast_to_ast_stm h d e)
 571                                     (λh'.opt_map ?? t
 572                                      (λt'.Some ? ([h']@t')))) (Some ? (nil ?)) lPreastStm)
 573      (λres.Some ? (AST_NO_DECL d e res))
 574
 575   | PREAST_CONST_DECL decName decType initExpr subPreastDecl ⇒
 576    match checkb_not_already_def_env d e decName
 577     return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
 578    with
 579     [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
 580      opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName true decType))
 581       (λdecl.opt_map ?? (preast_to_ast_init initExpr d e)
 582        (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
 583         (λresInit.Some ? (AST_CONST_DECL d e decName decType
 584                                          (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) resInit decl))))
 585     | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
 586     ] (refl_eq ? (checkb_not_already_def_env d e decName))
 587
 588   | PREAST_VAR_DECL decName decType optInitExpr subPreastDecl ⇒
 589    match checkb_not_already_def_env d e decName
 590     return λx.(checkb_not_already_def_env d e decName = x) → option (ast_decl d e)
 591    with
 592     [ true ⇒ λp:(checkb_not_already_def_env d e decName = true).
 593      opt_map ?? (preast_to_ast_decl subPreastDecl d (add_desc_env d e decName false decType))
 594       (λdecl.match optInitExpr with
 595        [ None ⇒ Some ? (AST_VAR_DECL d e decName decType
 596                                      (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (None ?) decl)
 597        | Some initExpr ⇒
 598         opt_map ?? (preast_to_ast_init initExpr d e)
 599          (λsigmaRes:(Σt:ast_type.ast_init d e t).opt_map ?? (preast_to_ast_init_check d e sigmaRes decType)
 600           (λresInit.Some ? (AST_VAR_DECL d e decName decType
 601                                          (checkbnotalreadydefenv_to_checknotalreadydefenv d e decName p) (Some ? resInit) decl)))])
 602     | false ⇒ λp:(checkb_not_already_def_env d e decName = false).None ?
 603     ] (refl_eq ? (checkb_not_already_def_env d e decName))
 604   ].
 605
 606 (*
 607  PREAST_ROOT: preast_decl → preast_root
 608 *)
 609 definition preast_to_ast ≝
 610 λpreast:preast_root.match preast with
 611  [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl O empty_env)
 612                        (λres.Some ? (AST_ROOT res)) ].