X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fpreast_tree.ma;h=662d289fb4e15b7280f0d0836220909f296bd792;hb=db1552c8344acc3de1f0596d999170046eb0c8fa;hp=fcc1fbf4a7edea1690fe76bc262e2efba9770ca6;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
index fcc1fbf4a..662d289fb 100755
--- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
+++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma
@@ -69,6 +69,25 @@ with preast_var : Type ≝
 
 (* -------------------------- *)
 
+(* inizializzatori: ... valori ... *)
+inductive preast_init_val : Type ≝
+  PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
+| PREAST_INIT_VAL_WORD16: word16 → preast_init_val
+| PREAST_INIT_VAL_WORD32: word32 → preast_init_val
+| PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
+| PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+  1) var1 = var2
+  2) var = ... valori ...
+*)
+inductive preast_init : Type ≝
+  PREAST_INIT_VAR: preast_var → preast_init
+| PREAST_INIT_VAL: preast_init_val → preast_init.
+
+(* -------------------------- *)
+
 (* statement: assegnamento/while/if else if else *)
 inductive preast_stm : Type ≝
   PREAST_STM_ASG: preast_var → preast_expr → preast_stm
@@ -78,7 +97,7 @@ inductive preast_stm : Type ≝
 (* dichiarazioni *)
 with preast_decl : Type ≝
   PREAST_NO_DECL: list preast_stm → preast_decl
-| PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
+| PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
 
 (* -------------------------- *)