matita/matita/contribs/assembly/compiler/preast_tree.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 "string/string.ma".
  23 include "compiler/ast_type.ma".
  24
  25 (* ****************** *)
  26 (* PREALBERO DI TOKEN *)
  27 (* ****************** *)
  28
  29 (* espressioni *)
  30 inductive preast_expr : Type ≝
  31   PREAST_EXPR_BYTE8 : byte8 → preast_expr
  32 | PREAST_EXPR_WORD16: word16 → preast_expr
  33 | PREAST_EXPR_WORD32: word32 → preast_expr
  34
  35 | PREAST_EXPR_NEG: preast_expr → preast_expr
  36 | PREAST_EXPR_NOT: preast_expr → preast_expr
  37 | PREAST_EXPR_COM: preast_expr → preast_expr
  38
  39 | PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
  40 | PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
  41 | PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
  42 | PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
  43 | PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
  44 | PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
  45 | PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr
  46 | PREAST_EXPR_OR:  preast_expr → preast_expr → preast_expr
  47 | PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
  48
  49 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
  50 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
  51 | PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
  52 | PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
  53 | PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
  54 | PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
  55
  56 | PREAST_EXPR_B8toW16 : preast_expr → preast_expr
  57 | PREAST_EXPR_B8toW32 : preast_expr → preast_expr
  58 | PREAST_EXPR_W16toB8 : preast_expr → preast_expr
  59 | PREAST_EXPR_W16toW32: preast_expr → preast_expr
  60 | PREAST_EXPR_W32toB8 : preast_expr → preast_expr
  61 | PREAST_EXPR_W32toW16: preast_expr → preast_expr
  62
  63 | PREAST_EXPR_ID: preast_var → preast_expr
  64
  65 (* variabile: modificatori di array/struct dell'id *)
  66 with preast_var : Type ≝
  67   PREAST_VAR_ID: aux_str_type → preast_var
  68 | PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
  69 | PREAST_VAR_STRUCT: preast_var → nat → preast_var.
  70
  71 (* -------------------------- *)
  72
  73 (* inizializzatori: ... valori ... *)
  74 inductive preast_init_val : Type ≝
  75   PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
  76 | PREAST_INIT_VAL_WORD16: word16 → preast_init_val
  77 | PREAST_INIT_VAL_WORD32: word32 → preast_init_val
  78 | PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
  79 | PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
  80
  81 (*
  82  inizializzatori: ammesse solo due forme, no ibridi
  83   1) var1 = var2
  84   2) var = ... valori ...
  85 *)
  86 inductive preast_init : Type ≝
  87   PREAST_INIT_VAR: preast_var → preast_init
  88 | PREAST_INIT_VAL: preast_init_val → preast_init.
  89
  90 (* -------------------------- *)
  91
  92 (* statement: assegnamento/while/if else if else *)
  93 inductive preast_stm : Type ≝
  94   PREAST_STM_ASG: preast_var → preast_expr → preast_stm
  95 | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
  96 | PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
  97
  98 (* dichiarazioni *)
  99 with preast_decl : Type ≝
 100   PREAST_NO_DECL: list preast_stm → preast_decl
 101 | PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
 102 | PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
 103
 104 (* -------------------------- *)
 105
 106 (* programma *)
 107 inductive preast_root : Type ≝
 108   PREAST_ROOT: preast_decl → preast_root.
 109
 110 (* -------------------------- *)
 111
 112 (* programma vuoto *)
 113 definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).