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