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 lemma pippo : ∀t1,t2:ast_base_type.
  31               (eq_ast_base_type t1 t2 = true) → (t1 = t2).
  32  unfold eq_ast_base_type;
  33  intros;
  34  elim t1 in H:(%);
  35  elim t2 in H:(%);
  36  normalize in H:(%);
  37  try reflexivity;
  38  destruct H;
  39 qed.
  40
  41 (*
  42  PREAST_EXPR_BYTE8 : byte8 → preast_expr
  43  PREAST_EXPR_WORD16: word16 → preast_expr
  44  PREAST_EXPR_WORD32: word32 → preast_expr
  45  PREAST_EXPR_NEG: preast_expr → preast_expr
  46  PREAST_EXPR_NOT: preast_expr → preast_expr
  47  PREAST_EXPR_COM: preast_expr → preast_expr
  48  PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
  49  PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
  50  PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
  51  PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
  52  PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
  53  PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
  54  PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
  55  PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
  56  PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
  57  PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
  58  PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
  59  PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
  60  PREAST_EXPR_B8toW16 : preast_expr → preast_expr
  61  PREAST_EXPR_B8toW32 : preast_expr → preast_expr
  62  PREAST_EXPR_W16toB8 : preast_expr → preast_expr
  63  PREAST_EXPR_W16toW32: preast_expr → preast_expr
  64  PREAST_EXPR_W32toB8 : preast_expr → preast_expr
  65  PREAST_EXPR_W32toW16: preast_expr → preast_expr
  66  PREAST_EXPR_ID: preast_var → preast_expr
  67 *)
  68 definition preast_to_ast_expr_check ≝
  69  λe:aux_env_type.λv:Σt'.ast_expr e t'.λt:ast_base_type.
  70     match v with
  71      [ sigma_intro t' expr ⇒
  72          match eq_ast_base_type t' t
  73          return λb.eq_ast_base_type t' t = b → option (ast_expr e t)
  74          with
  75           [ true ⇒ λp.Some ? (eq_rect ? t' (λt.ast_expr e t) expr t (pippo ?? p))
  76           | false ⇒ λp.None ?
  77           ] (refl_eq ? (eq_ast_base_type t' t))
  78      ].
  79
  80 let rec preast_to_ast_expr (preast:preast_expr) (e:aux_env_type) on preast : option (Σt:ast_base_type.ast_expr e t) ≝
  81  match preast with
  82    (* in pretty print diventa Some ? "≪AST_BASE_TYPE_BYTE8,AST_EXPR_BYTE8 e val≫" *)
  83   [ PREAST_EXPR_BYTE8 val ⇒ Some ? ≪AST_BASE_TYPE_BYTE8, AST_EXPR_BYTE8 e val≫
  84   | PREAST_EXPR_WORD16 val ⇒ Some ? ≪AST_BASE_TYPE_WORD16, AST_EXPR_WORD16 e val≫
  85   | PREAST_EXPR_WORD32 val ⇒ Some ? ≪AST_BASE_TYPE_WORD32, AST_EXPR_WORD32 e val≫
  86   | PREAST_EXPR_NEG subExpr ⇒
  87    opt_map ?? (preast_to_ast_expr subExpr e)
  88     (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_NEG e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
  89   | PREAST_EXPR_NOT subExpr ⇒
  90    opt_map ?? (preast_to_ast_expr subExpr e)
  91     (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_NOT e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
  92   | PREAST_EXPR_COM subExpr ⇒
  93    opt_map ?? (preast_to_ast_expr subExpr e)
  94     (λsigmaRes:Σt:ast_base_type.ast_expr e t.Some ? ≪sigmaFst ?? sigmaRes, AST_EXPR_COM e (sigmaFst ?? sigmaRes) (sigmaSnd ?? sigmaRes)≫)
  95   | PREAST_EXPR_ADD subExpr1 subExpr2 ⇒
  96    opt_map ?? (preast_to_ast_expr subExpr1 e)
  97     (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
  98      (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
  99      (λres2.Some ? (≪sigmaFst ?? sigmaRes1,AST_EXPR_ADD e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2≫))))
 100   | _ ⇒ None ?
 101   ]
 102
 103 (*
 104  PREAST_VAR_ID: aux_str_type → preast_var
 105  PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
 106  PREAST_VAR_STRUCT: preast_var → nat → preast_var.
 107 *)
 108 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) ≝
 109  None ?.
 110
 111 (*
 112  PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
 113  PREAST_INIT_VAL_WORD16: word16 → preast_init_val
 114  PREAST_INIT_VAL_WORD32: word32 → preast_init_val
 115  PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
 116  PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
 117 *)
 118 let rec preast_to_ast_init_val (preast:preast_init_val) (e:aux_env_type) on preast : option (sigma ast_type (ast_init e)) ≝
 119  None ?.
 120
 121 (*
 122  PREAST_INIT_VAR: preast_var → preast_init
 123  PREAST_INIT_VAL: preast_init_val → preast_init.
 124 *)
 125 definition preast_to_ast_init : preast_init → Πe:aux_env_type.option (sigma ast_type (ast_init e)) ≝
 126 λpreast:preast_init.λe:aux_env_type.None ?.
 127
 128 (*
 129  PREAST_STM_ASG: preast_var → preast_expr → preast_stm
 130  PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
 131  PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
 132 *)
 133 let rec preast_to_ast_stm (preast:preast_stm) (e:aux_env_type) on preast : option (ast_stm e) ≝
 134  None ?
 135 (*
 136  PREAST_NO_DECL: list preast_stm → preast_decl
 137  PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
 138 *)
 139 and preast_to_ast_decl (preast:preast_decl) (e:aux_env_type) on preast : option (ast_decl e) ≝
 140  None ?.
 141
 142 (*
 143  PREAST_ROOT: preast_decl → preast_root.
 144 *)
 145 definition preast_to_ast ≝
 146 λpreast:preast_root.match preast with
 147  [ PREAST_ROOT decl ⇒ opt_map ?? (preast_to_ast_decl decl empty_env)
 148                        (λres.Some ? (AST_ROOT res)) ].