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