+ ast_var d e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n)
+
+(* espressioni generalizzate: anche non uniformi per tipo *)
+with ast_base_expr : Type ≝
+ AST_BASE_EXPR: ∀t:ast_base_type.
+ ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e.
+
+(* -------------------------- *)
+
+let rec aux_ast_init_type (t:ast_type) on t : Type ≝
+ match t with
+ [ AST_TYPE_BASE bType ⇒ match bType with
+ [ AST_BASE_TYPE_BYTE8 ⇒ byte8
+ | AST_BASE_TYPE_WORD16 ⇒ word16
+ | AST_BASE_TYPE_WORD32 ⇒ word32
+ ]
+ | AST_TYPE_ARRAY subType dim ⇒
+ let T ≝ aux_ast_init_type subType in
+ let rec aux (n:nat) on n ≝
+ match n with
+ [ O ⇒ T
+ | S n' ⇒ Prod T (aux n')
+ ] in
+ aux dim
+ | AST_TYPE_STRUCT nelSubType ⇒
+ let rec aux (nel:ne_list ast_type) on nel ≝
+ match nel with
+ [ ne_nil h ⇒ aux_ast_init_type h
+ | ne_cons h t ⇒ Prod (aux_ast_init_type h) (aux t)
+ ] in
+ aux nelSubType
+ ].
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+ 1) var1 = var2
+ 2) var = ... valori ...
+*)
+inductive ast_init (d:nat) (e:aux_env_type d) : ast_type → Type ≝
+ AST_INIT_VAR: ∀b:bool.∀t:ast_type.
+ ast_var d e b t → ast_init d e t
+| AST_INIT_VAL: ∀t:ast_type.
+ aux_ast_init_type t → ast_init d e t.