]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/assembly/compiler/preast_tree.ma
update in groud_2 and models
[helm.git] / helm / software / matita / contribs / assembly / compiler / preast_tree.ma
index 662d289fb4e15b7280f0d0836220909f296bd792..6ad8c3d62e8834a1f6c65a8a900277a7f4701d63 100755 (executable)
@@ -20,8 +20,6 @@
 (* ********************************************************************** *)
 
 include "string/string.ma".
-include "compiler/utility.ma".
-include "freescale/word32.ma".
 include "compiler/ast_type.ma".
 
 (* ****************** *)
@@ -44,6 +42,9 @@ inductive preast_expr : Type ≝
 | PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
 | PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
 | PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_OR:  preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
 
 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
@@ -97,7 +98,8 @@ 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_init → preast_decl → preast_decl.
+| PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
+| PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
 
 (* -------------------------- *)