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