X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Fcompiler%2Fpreast_tree.ma;h=6ad8c3d62e8834a1f6c65a8a900277a7f4701d63;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=662d289fb4e15b7280f0d0836220909f296bd792;hpb=4924f99796029eecb58e920ca7a6a366efe2373e;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 662d289fb..6ad8c3d62 100755 --- a/helm/software/matita/contribs/assembly/compiler/preast_tree.ma +++ b/helm/software/matita/contribs/assembly/compiler/preast_tree.ma @@ -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. (* -------------------------- *)