--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/environment.ma".
+
+(* *************** *)
+(* ALBERO DI TOKEN *)
+(* *************** *)
+
+(* id: accesso all'ambiente con stringa *)
+inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
+ AST_ID: ∀str:aux_str_type.
+ (* 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)).
+
+(* -------------------------- *)
+
+(* espressioni *)
+inductive ast_expr (e:aux_env_type) : ast_base_type → Type ≝
+ AST_EXPR_BYTE8 : byte8 → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_WORD16: word16 → ast_expr e AST_BASE_TYPE_WORD16
+| AST_EXPR_WORD32: word32 → ast_expr e AST_BASE_TYPE_WORD32
+
+| AST_EXPR_NEG: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t
+| AST_EXPR_NOT: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t
+| AST_EXPR_COM: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t
+
+| AST_EXPR_ADD: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e t
+| AST_EXPR_SUB: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e t
+| AST_EXPR_MUL: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e t
+| AST_EXPR_DIV: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e t
+| AST_EXPR_SHR: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+| AST_EXPR_SHL: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e t
+
+| AST_EXPR_GT : ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_GTE: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_LT : ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_LTE: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_EQ : ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_NEQ: ∀t:ast_base_type.
+ ast_expr e t → ast_expr e t → ast_expr e AST_BASE_TYPE_BYTE8
+
+| AST_EXPR_B8toW16 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD16
+| AST_EXPR_B8toW32 : ast_expr e AST_BASE_TYPE_BYTE8 → ast_expr e AST_BASE_TYPE_WORD32
+| AST_EXPR_W16toB8 : ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_W16toW32: ast_expr e AST_BASE_TYPE_WORD16 → ast_expr e AST_BASE_TYPE_WORD32
+| AST_EXPR_W32toB8 : ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_BYTE8
+| AST_EXPR_W32toW16: ast_expr e AST_BASE_TYPE_WORD32 → ast_expr e AST_BASE_TYPE_WORD16
+
+| AST_EXPR_ID: ∀b:bool.∀t:ast_base_type.
+ ast_var e b (AST_TYPE_BASE t) → ast_expr e t
+
+(* espressioni generalizzate: anche non uniformi per tipo *)
+with ast_base_expr : Type ≝
+ AST_BASE_EXPR: ∀t:ast_base_type.
+ ast_expr e t → ast_base_expr e
+
+(* variabile: modificatori di array/struct dell'id *)
+with ast_var : bool → ast_type → Type ≝
+ AST_VAR_ID: ∀b:bool.∀t:ast_type.
+ ast_id e b t → ast_var e b t
+ (* NB: l'index out of bound e' delegato a runtime? *)
+| AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+ ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
+| AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
+ ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n).
+
+(* -------------------------- *)
+
+(* statement: assegnamento/while/if else if else *)
+inductive ast_stm : aux_env_type → Type ≝
+ AST_STM_ASG: ∀e:aux_env_type.∀t:ast_base_type.
+ ast_var e false (AST_TYPE_BASE t) → ast_expr e t → ast_stm e
+| AST_STM_MEMCPY_ASG: ∀e:aux_env_type.∀b:bool.∀t:ast_type.
+ (* D *) isnt_ast_base_type t → ast_var e false t → ast_var e b t → ast_stm e
+| AST_STM_WHILE: ∀e:aux_env_type.
+ ast_base_expr e → ast_decl e → ast_stm e
+| AST_STM_IF: ∀e:aux_env_type.
+ ne_list (Prod (ast_base_expr e) (ast_decl e)) → option (ast_decl e) → ast_stm e
+
+(* dichiarazioni *)
+with ast_decl : aux_env_type → Type ≝
+ AST_NO_DECL: ∀e:aux_env_type.
+ list (ast_stm e) → ast_decl e
+| AST_BASE_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_base_type.
+ (* 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
+| AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
+ (* 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.
+
+(* -------------------------- *)
+
+(* programma *)
+inductive ast_root : Type ≝
+ AST_ROOT: ast_decl empty_env → ast_root.
+
+(* -------------------------- *)
+
+(* programma vuoto *)
+definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).