helm/software/matita/contribs/assembly/compiler/astfe_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/utility.ma".
  24 include "freescale/word32.ma".
  25 include "compiler/ast_type.ma".
  26 include "compiler/env_to_flatenv.ma".
  27 include "compiler/ast_tree.ma".
  28
  29 (* **************************** *)
  30 (* ALBERO DI TOKEN CON FLAT ENV *)
  31 (* **************************** *)
  32
  33 (* id: accesso all'ambiente con stringa *)
  34 inductive astfe_id : bool → ast_type → Type ≝
  35   ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type.
  36             astfe_id b t.
  37
  38 (* -------------------------- *)
  39
  40 (* espressioni *)
  41 inductive astfe_expr : ast_type → Type ≝
  42   ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  43 | ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  44 | ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  45
  46 | ASTFE_EXPR_NEG: ∀t:ast_base_type.
  47                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  48 | ASTFE_EXPR_NOT: ∀t:ast_base_type.
  49                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  50 | ASTFE_EXPR_COM: ∀t:ast_base_type.
  51                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  52
  53 | ASTFE_EXPR_ADD: ∀t:ast_base_type.
  54                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  55 | ASTFE_EXPR_SUB: ∀t:ast_base_type.
  56                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  57 | ASTFE_EXPR_MUL: ∀t:ast_base_type.
  58                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  59 | ASTFE_EXPR_DIV: ∀t:ast_base_type.
  60                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
  61 | ASTFE_EXPR_SHR: ∀t:ast_base_type.
  62                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
  63 | ASTFE_EXPR_SHL: ∀t:ast_base_type.
  64                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
  65
  66 | ASTFE_EXPR_GT : ∀t:ast_base_type.
  67                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  68 | ASTFE_EXPR_GTE: ∀t:ast_base_type.
  69                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  70 | ASTFE_EXPR_LT : ∀t:ast_base_type.
  71                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  72 | ASTFE_EXPR_LTE: ∀t:ast_base_type.
  73                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  74 | ASTFE_EXPR_EQ : ∀t:ast_base_type.
  75                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  76 | ASTFE_EXPR_NEQ: ∀t:ast_base_type.
  77                   astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  78
  79 | ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  80 | ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  81 | ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  82 | ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
  83 | ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
  84 | ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
  85
  86 | ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
  87                  astfe_var b t → astfe_expr t
  88
  89 (* variabile: modificatori di array/struct dell'id *)
  90 with astfe_var : bool → ast_type → Type ≝
  91   ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
  92                 astfe_id b t → astfe_var b t
  93 | ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
  94                    astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t
  95 | ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
  96                     astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n)
  97
  98 (* espressioni generalizzate: anche non uniformi per tipo *)
  99 with astfe_base_expr : Type ≝
 100   ASTFE_BASE_EXPR: ∀t:ast_base_type.
 101                    astfe_expr (AST_TYPE_BASE t) → astfe_base_expr.
 102
 103 (* -------------------------- *)
 104
 105 (*
 106  inizializzatori: ammesse solo due forme, no ibridi
 107   1) var1 = var2
 108   2) var = ... valori ...
 109 *)
 110 inductive astfe_init : ast_type → Type ≝
 111   ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
 112                   astfe_var b t → astfe_init t
 113 | ASTFE_INIT_VAL: ∀t:ast_type.
 114                   aux_ast_init_type t → astfe_init t.
 115
 116 (* -------------------------- *)
 117
 118 (* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
 119 inductive astfe_stm : Type ≝
 120   ASTFE_STM_ASG: ∀t:ast_type.
 121                  astfe_var false t → astfe_expr t → astfe_stm
 122 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
 123                   astfe_id b t → astfe_init t → astfe_stm
 124 | ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm
 125 | ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm
 126
 127 (* dichiarazioni *)
 128 with astfe_body : Type ≝
 129   ASTFE_BODY: list astfe_stm → astfe_body.
 130
 131 (* -------------------------- *)
 132
 133 (* programma *)
 134 inductive astfe_root : Type ≝
 135   ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root.
 136
 137 (* -------------------------- *)
 138
 139 (* programma vuoto *)
 140 definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)).