--- /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 "string/string.ma".
+include "compiler/utility.ma".
+include "freescale/word32.ma".
+include "compiler/ast_type.ma".
+include "compiler/env_to_flatenv.ma".
+include "compiler/ast_tree.ma".
+
+(* **************************** *)
+(* ALBERO DI TOKEN CON FLAT ENV *)
+(* **************************** *)
+
+(* id: accesso all'ambiente con stringa *)
+inductive astfe_id : bool → ast_type → Type ≝
+ ASTFE_ID: ∀str:aux_strId_type.∀b:bool.∀t:ast_type.
+ astfe_id b t.
+
+(* -------------------------- *)
+
+(* espressioni *)
+inductive astfe_expr : ast_type → Type ≝
+ ASTFE_EXPR_BYTE8 : byte8 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_WORD16: word16 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_WORD32: word32 → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+
+| ASTFE_EXPR_NEG: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_NOT: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_COM: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+
+| ASTFE_EXPR_ADD: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SUB: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_MUL: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_DIV: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SHR: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+| ASTFE_EXPR_SHL: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE t)
+
+| ASTFE_EXPR_GT : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_GTE: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_LT : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_LTE: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_EQ : ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_NEQ: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE t) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+
+| ASTFE_EXPR_B8toW16 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+| ASTFE_EXPR_B8toW32 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W16toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W16toW32: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
+| ASTFE_EXPR_W32toB8 : astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+| ASTFE_EXPR_W32toW16: astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
+
+| ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
+ astfe_var b t → astfe_expr t
+
+(* variabile: modificatori di array/struct dell'id *)
+with astfe_var : bool → ast_type → Type ≝
+ ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
+ astfe_id b t → astfe_var b t
+| ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
+ astfe_var b (AST_TYPE_ARRAY t n) → astfe_base_expr → astfe_var b t
+| ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
+ astfe_var b (AST_TYPE_STRUCT nel) → astfe_var b (abs_nth_neList ? nel n)
+
+(* espressioni generalizzate: anche non uniformi per tipo *)
+with astfe_base_expr : Type ≝
+ ASTFE_BASE_EXPR: ∀t:ast_base_type.
+ astfe_expr (AST_TYPE_BASE t) → astfe_base_expr.
+
+(* -------------------------- *)
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+ 1) var1 = var2
+ 2) var = ... valori ...
+*)
+inductive astfe_init : ast_type → Type ≝
+ ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
+ astfe_var b t → astfe_init t
+| ASTFE_INIT_VAL: ∀t:ast_type.
+ aux_ast_init_type t → astfe_init t.
+
+(* -------------------------- *)
+
+(* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
+inductive astfe_stm : Type ≝
+ ASTFE_STM_ASG: ∀t:ast_type.
+ astfe_var false t → astfe_expr t → astfe_stm
+| ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
+ astfe_id b t → astfe_init t → astfe_stm
+| ASTFE_STM_WHILE: astfe_base_expr → astfe_body → astfe_stm
+| ASTFE_STM_IF: ne_list (Prod astfe_base_expr astfe_body) → option astfe_body → astfe_stm
+
+(* dichiarazioni *)
+with astfe_body : Type ≝
+ ASTFE_BODY: list astfe_stm → astfe_body.
+
+(* -------------------------- *)
+
+(* programma *)
+inductive astfe_root : Type ≝
+ ASTFE_ROOT: aux_flatEnv_type → astfe_body → astfe_root.
+
+(* -------------------------- *)
+
+(* programma vuoto *)
+definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY (nil ?)).