]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly2/compiler/preast_tree.ma
milestone update in ground
[helm.git] / matitaB / matita / contribs / ng_assembly2 / compiler / preast_tree.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/string.ma".
24 include "compiler/ast_type.ma".
25 include "num/word32.ma".
26
27 (* ****************** *)
28 (* PREALBERO DI TOKEN *)
29 (* ****************** *)
30
31 (* espressioni *)
32 ninductive preast_expr : Type ≝
33   PREAST_EXPR_BYTE8 : byte8 → preast_expr
34 | PREAST_EXPR_WORD16: word16 → preast_expr
35 | PREAST_EXPR_WORD32: word32 → preast_expr
36
37 | PREAST_EXPR_NEG: preast_expr → preast_expr
38 | PREAST_EXPR_NOT: preast_expr → preast_expr
39 | PREAST_EXPR_COM: preast_expr → preast_expr
40
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
47 | PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr
48 | PREAST_EXPR_OR:  preast_expr → preast_expr → preast_expr
49 | PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
50
51 | PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
52 | PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
53 | PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
54 | PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
55 | PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
56 | PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
57
58 | PREAST_EXPR_B8toW16 : preast_expr → preast_expr
59 | PREAST_EXPR_B8toW32 : preast_expr → preast_expr
60 | PREAST_EXPR_W16toB8 : preast_expr → preast_expr
61 | PREAST_EXPR_W16toW32: preast_expr → preast_expr
62 | PREAST_EXPR_W32toB8 : preast_expr → preast_expr
63 | PREAST_EXPR_W32toW16: preast_expr → preast_expr
64
65 | PREAST_EXPR_ID: preast_var → preast_expr
66
67 (* variabile: modificatori di array/struct dell'id *)
68 with preast_var : Type ≝
69   PREAST_VAR_ID: aux_str_type → preast_var
70 | PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
71 | PREAST_VAR_STRUCT: preast_var → nat → preast_var.
72
73 (* -------------------------- *)
74
75 (* inizializzatori: ... valori ... *)
76 ninductive preast_init_val : Type ≝
77   PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
78 | PREAST_INIT_VAL_WORD16: word16 → preast_init_val
79 | PREAST_INIT_VAL_WORD32: word32 → preast_init_val
80 | PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
81 | PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
82
83 (*
84  inizializzatori: ammesse solo due forme, no ibridi
85   1) var1 = var2
86   2) var = ... valori ...
87 *)
88 ninductive preast_init : Type ≝
89   PREAST_INIT_VAR: preast_var → preast_init
90 | PREAST_INIT_VAL: preast_init_val → preast_init.
91
92 (* -------------------------- *)
93
94 (* statement: assegnamento/while/if else if else *)
95 ninductive preast_stm : Type ≝
96   PREAST_STM_ASG: preast_var → preast_expr → preast_stm
97 | PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
98 | PREAST_STM_IF: ne_list (ProdT preast_expr preast_decl) → option preast_decl → preast_stm
99
100 (* dichiarazioni *)
101 with preast_decl : Type ≝
102   PREAST_NO_DECL: list preast_stm → preast_decl
103 | PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
104 | PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
105
106 (* -------------------------- *)
107
108 (* programma *)
109 ninductive preast_root : Type ≝
110   PREAST_ROOT: preast_decl → preast_root.
111
112 (* -------------------------- *)
113
114 (* programma vuoto *)
115 ndefinition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).