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/ast_type.ma".
25 (* ****************** *)
26 (* PREALBERO DI TOKEN *)
27 (* ****************** *)
30 inductive preast_expr : Type ≝
31 PREAST_EXPR_BYTE8 : byte8 → preast_expr
32 | PREAST_EXPR_WORD16: word16 → preast_expr
33 | PREAST_EXPR_WORD32: word32 → preast_expr
35 | PREAST_EXPR_NEG: preast_expr → preast_expr
36 | PREAST_EXPR_NOT: preast_expr → preast_expr
37 | PREAST_EXPR_COM: preast_expr → preast_expr
39 | PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
40 | PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
41 | PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
42 | PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
43 | PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
44 | PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
46 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
47 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
48 | PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
49 | PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
50 | PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
51 | PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
53 | PREAST_EXPR_B8toW16 : preast_expr → preast_expr
54 | PREAST_EXPR_B8toW32 : preast_expr → preast_expr
55 | PREAST_EXPR_W16toB8 : preast_expr → preast_expr
56 | PREAST_EXPR_W16toW32: preast_expr → preast_expr
57 | PREAST_EXPR_W32toB8 : preast_expr → preast_expr
58 | PREAST_EXPR_W32toW16: preast_expr → preast_expr
60 | PREAST_EXPR_ID: preast_var → preast_expr
62 (* variabile: modificatori di array/struct dell'id *)
63 with preast_var : Type ≝
64 PREAST_VAR_ID: aux_str_type → preast_var
65 | PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
66 | PREAST_VAR_STRUCT: preast_var → nat → preast_var.
68 (* -------------------------- *)
70 (* inizializzatori: ... valori ... *)
71 inductive preast_init_val : Type ≝
72 PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
73 | PREAST_INIT_VAL_WORD16: word16 → preast_init_val
74 | PREAST_INIT_VAL_WORD32: word32 → preast_init_val
75 | PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
76 | PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
79 inizializzatori: ammesse solo due forme, no ibridi
81 2) var = ... valori ...
83 inductive preast_init : Type ≝
84 PREAST_INIT_VAR: preast_var → preast_init
85 | PREAST_INIT_VAL: preast_init_val → preast_init.
87 (* -------------------------- *)
89 (* statement: assegnamento/while/if else if else *)
90 inductive preast_stm : Type ≝
91 PREAST_STM_ASG: preast_var → preast_expr → preast_stm
92 | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
93 | PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
96 with preast_decl : Type ≝
97 PREAST_NO_DECL: list preast_stm → preast_decl
98 | PREAST_DECL: bool → aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
100 (* -------------------------- *)
103 inductive preast_root : Type ≝
104 PREAST_ROOT: preast_decl → preast_root.
106 (* -------------------------- *)
108 (* programma vuoto *)
109 definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).