1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "string/string.ma".
23 include "compiler/utility.ma".
24 include "freescale/word32.ma".
25 include "compiler/ast_type.ma".
27 (* ****************** *)
28 (* PREALBERO DI TOKEN *)
29 (* ****************** *)
32 inductive preast_expr : Type ≝
33 PREAST_EXPR_BYTE8 : byte8 → preast_expr
34 | PREAST_EXPR_WORD16: word16 → preast_expr
35 | PREAST_EXPR_WORD32: word32 → preast_expr
37 | PREAST_EXPR_NEG: preast_expr → preast_expr
38 | PREAST_EXPR_NOT: preast_expr → preast_expr
39 | PREAST_EXPR_COM: preast_expr → preast_expr
41 | PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
42 | PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
43 | PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
44 | PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
45 | PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
46 | PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
48 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
49 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
50 | PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
51 | PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
52 | PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
53 | PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
55 | PREAST_EXPR_B8toW16 : preast_expr → preast_expr
56 | PREAST_EXPR_B8toW32 : preast_expr → preast_expr
57 | PREAST_EXPR_W16toB8 : preast_expr → preast_expr
58 | PREAST_EXPR_W16toW32: preast_expr → preast_expr
59 | PREAST_EXPR_W32toB8 : preast_expr → preast_expr
60 | PREAST_EXPR_W32toW16: preast_expr → preast_expr
62 | PREAST_EXPR_ID: preast_var → preast_expr
64 (* variabile: modificatori di array/struct dell'id *)
65 with preast_var : Type ≝
66 PREAST_VAR_ID: aux_str_type → preast_var
67 | PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
68 | PREAST_VAR_STRUCT: preast_var → nat → preast_var.
70 (* -------------------------- *)
72 (* statement: assegnamento/while/if else if else *)
73 inductive preast_stm : Type ≝
74 PREAST_STM_ASG: preast_var → preast_expr → preast_stm
75 | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
76 | PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
79 with preast_decl : Type ≝
80 PREAST_NO_DECL: list preast_stm → preast_decl
81 | PREAST_DECL: bool → aux_str_type → ast_type → option preast_expr → preast_decl → preast_decl.
83 (* -------------------------- *)
86 inductive preast_root : Type ≝
87 PREAST_ROOT: preast_decl → preast_root.
89 (* -------------------------- *)
92 definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).