helm/software/matita/contribs/assembly/compiler/ast_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/environment.ma".
  23
  24 (* *************** *)
  25 (* ALBERO DI TOKEN *)
  26 (* *************** *)
  27
  28 (* id: accesso all'ambiente con stringa *)
  29 inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
  30   AST_ID: ∀str:aux_str_type.
  31           (* D *) check_desc_env e str → ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str)).
  32
  33 (* -------------------------- *)
  34
  35 (* espressioni *)
  36 inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
  37   AST_EXPR_BYTE8 : byte8 → ast_expr e AST_BASE_TYPE_BYTE8
  38 | AST_EXPR_WORD16: word16 → ast_expr e AST_BASE_TYPE_WORD16
  39 | AST_EXPR_WORD32: word32 → ast_expr e AST_BASE_TYPE_WORD32
  40
  41 | AST_EXPR_NEG: ∀t:ast_base_type.
  42                 ast_expr e t → ast_expr e t
  43 | AST_EXPR_NOT: ∀t:ast_base_type.
  44                 ast_expr e t → ast_expr e t
  45 | AST_EXPR_COM: ∀t:ast_base_type.
  46                 ast_expr e t → ast_expr e t
  47
  48 | AST_EXPR_ADD: ∀t:ast_base_type.
  49                 ast_expr e t → ast_expr e t → ast_expr e t
  50 | AST_EXPR_SUB: ∀t:ast_base_type.
  51                 ast_expr e t → ast_expr e t → ast_expr e t
  52 | AST_EXPR_MUL: ∀t:ast_base_type.
  53                 ast_expr e t → ast_expr e t → ast_expr e t
  54 | AST_EXPR_DIV: ∀t:ast_base_type.
  55                 ast_expr e t → ast_expr e t → ast_expr e t
  56 | AST_EXPR_SHR: ∀t:ast_base_type.
  57                 ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
  58 | AST_EXPR_SHL: ∀t:ast_base_type.
  59                 ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
  60
  61 | AST_EXPR_GT : ∀t:ast_base_type.
  62                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  63 | AST_EXPR_GTE: ∀t:ast_base_type.
  64                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  65 | AST_EXPR_LT : ∀t:ast_base_type.
  66                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  67 | AST_EXPR_LTE: ∀t:ast_base_type.
  68                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  69 | AST_EXPR_EQ : ∀t:ast_base_type.
  70                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  71 | AST_EXPR_NEQ: ∀t:ast_base_type.
  72                 ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
  73
  74 | AST_EXPR_B8toW16 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD16
  75 | AST_EXPR_B8toW32 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD32
  76 | AST_EXPR_W16toB8 : ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_BYTE8
  77 | AST_EXPR_W16toW32: ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_WORD32
  78 | AST_EXPR_W32toB8 : ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_BYTE8
  79 | AST_EXPR_W32toW16: ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_WORD16
  80
  81 | AST_EXPR_ID: ∀b:bool.∀t:ast_base_type.
  82                ast_var e b (AST_TYPE_BASE t) → ast_expr e t
  83
  84 (* espressioni generalizzate: anche non uniformi per tipo *)
  85 with ast_base_expr : Type ≝
  86   AST_BASE_EXPR: ∀t:ast_base_type.
  87                  ast_expr e t → ast_base_expr e
  88
  89 (* variabile: modificatori di array/struct dell'id *)
  90 with ast_var : bool → ast_type → Type ≝
  91   AST_VAR_ID: ∀b:bool.∀t:ast_type.
  92               ast_id e b t → ast_var e b t
  93                  (* NB: l'index out of bound e' delegato a runtime? *)
  94 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
  95                  ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
  96 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
  97                   ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n).
  98
  99 (* -------------------------- *)
 100
 101 (* statement: assegnamento/while/if else if else *)
 102 inductive ast_stm : aux_env_type → Type ≝
 103   AST_STM_ASG: ∀e:aux_env_type.∀t:ast_base_type.
 104                ast_var e false (AST_TYPE_BASE t) → ast_expr e t → ast_stm e
 105 | AST_STM_MEMCPY_ASG: ∀e:aux_env_type.∀b:bool.∀t:ast_type.
 106                       (* D *) isnt_ast_base_type t → ast_var e false t → ast_var e b t → ast_stm e
 107 | AST_STM_WHILE: ∀e:aux_env_type.
 108                  ast_base_expr e → ast_decl e → ast_stm e
 109 | AST_STM_IF: ∀e:aux_env_type.
 110               ne_list (Prod (ast_base_expr e) (ast_decl e)) → option (ast_decl e) → ast_stm e
 111
 112 (* dichiarazioni *)
 113 with ast_decl : aux_env_type → Type ≝
 114   AST_NO_DECL: ∀e:aux_env_type.
 115                list (ast_stm e) → ast_decl e
 116 | AST_BASE_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_base_type.
 117                  (* D *) (check_not_already_def_env e str) → option (ast_expr e t) → ast_decl (add_desc_env e str c (AST_TYPE_BASE t)) → ast_decl e
 118 | AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
 119             (* D *) (check_not_already_def_env e str) → (* D *) isnt_ast_base_type t → ast_decl (add_desc_env e str c t) → ast_decl e.
 120
 121 (* -------------------------- *)
 122
 123 (* programma *)
 124 inductive ast_root : Type ≝
 125   AST_ROOT: ast_decl empty_env → ast_root.
 126
 127 (* -------------------------- *)
 128
 129 (* programma vuoto *)
 130 definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).