]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/compiler/ast_tree.ma
- exclusion binder in local environments allows to complete lfsx_lfsx !
[helm.git] / matita / matita / contribs / assembly / compiler / ast_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 (*                                                                        *)
17 (* Sviluppato da:                                                         *)
18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
19 (*                                                                        *)
20 (* ********************************************************************** *)
21
22 include "compiler/environment.ma".
23
24 (* *************** *)
25 (* ALBERO DI TOKEN *)
26 (* *************** *)
27
28 (* id: accesso all'ambiente con stringa *)
29 inductive ast_id (d:nat) (e:aux_env_type d) : bool → ast_type → Type ≝
30   AST_ID: ∀str:aux_str_type.
31           (* D *) (check_desc_env d e str) → (ast_id d e (get_const_desc (get_desc_env d e str)) (get_type_desc (get_desc_env d e str))).
32
33 (* -------------------------- *)
34
35 (* espressioni *)
36 inductive ast_expr (d:nat) (e:aux_env_type d) : ast_type → Type ≝
37   AST_EXPR_BYTE8 : byte8 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
38 | AST_EXPR_WORD16: word16 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
39 | AST_EXPR_WORD32: word32 → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
40
41 | AST_EXPR_NEG: ∀t:ast_base_type.
42                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
43 | AST_EXPR_NOT: ∀t:ast_base_type.
44                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
45 | AST_EXPR_COM: ∀t:ast_base_type.
46                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
47
48 | AST_EXPR_ADD: ∀t:ast_base_type.
49                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
50 | AST_EXPR_SUB: ∀t:ast_base_type.
51                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
52 | AST_EXPR_MUL: ∀t:ast_base_type.
53                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
54 | AST_EXPR_DIV: ∀t:ast_base_type.
55                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
56 | AST_EXPR_SHR: ∀t:ast_base_type.
57                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
58 | AST_EXPR_SHL: ∀t:ast_base_type.
59                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE t)
60 | AST_EXPR_AND: ∀t:ast_base_type.
61                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
62 | AST_EXPR_OR:  ∀t:ast_base_type.
63                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
64 | AST_EXPR_XOR: ∀t:ast_base_type.
65                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t)
66
67 | AST_EXPR_GT : ∀t:ast_base_type.
68                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
69 | AST_EXPR_GTE: ∀t:ast_base_type.
70                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
71 | AST_EXPR_LT : ∀t:ast_base_type.
72                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
73 | AST_EXPR_LTE: ∀t:ast_base_type.
74                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
75 | AST_EXPR_EQ : ∀t:ast_base_type.
76                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
77 | AST_EXPR_NEQ: ∀t:ast_base_type.
78                 ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE t) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
79
80 | AST_EXPR_B8toW16 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
81 | AST_EXPR_B8toW32 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
82 | AST_EXPR_W16toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
83 | AST_EXPR_W16toW32: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
84 | AST_EXPR_W32toB8 : ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
85 | AST_EXPR_W32toW16: ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr d e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
86
87 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
88                ast_var d e b t → ast_expr d e t
89
90 (* variabile: modificatori di array/struct dell'id *)
91 with ast_var : bool → ast_type → Type ≝
92   AST_VAR_ID: ∀b:bool.∀t:ast_type.
93               ast_id d e b t → ast_var d e b t
94 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
95                  ast_var d e b (AST_TYPE_ARRAY t n) → ast_base_expr d e → ast_var d e b t
96 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
97                   ast_var d e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var d e b (abs_nth_neList ? nel n)
98
99 (* espressioni generalizzate: anche non uniformi per tipo *)
100 with ast_base_expr : Type ≝
101   AST_BASE_EXPR: ∀t:ast_base_type.
102                  ast_expr d e (AST_TYPE_BASE t) → ast_base_expr d e.
103
104 (* -------------------------- *)
105
106 let rec aux_ast_init_type (t:ast_type) on t : Type ≝
107  match t with
108   [ AST_TYPE_BASE bType ⇒ match bType with
109    [ AST_BASE_TYPE_BYTE8 ⇒ byte8
110    | AST_BASE_TYPE_WORD16 ⇒ word16
111    | AST_BASE_TYPE_WORD32 ⇒ word32
112    ] 
113   | AST_TYPE_ARRAY subType dim ⇒
114    let T ≝ aux_ast_init_type subType in
115    let rec aux (n:nat) on n ≝
116     match n with
117      [ O ⇒ T
118      | S n' ⇒ Prod T (aux n')
119      ] in
120    aux dim 
121   | AST_TYPE_STRUCT nelSubType ⇒
122    let rec aux (nel:ne_list ast_type) on nel ≝
123     match nel with
124      [ ne_nil h ⇒ aux_ast_init_type h
125      | ne_cons h t ⇒ Prod (aux_ast_init_type h) (aux t)
126      ] in
127     aux nelSubType 
128   ].
129
130 (*
131  inizializzatori: ammesse solo due forme, no ibridi
132   1) var1 = var2
133   2) var = ... valori ...
134 *) 
135 inductive ast_init (d:nat) (e:aux_env_type d) : ast_type → Type ≝
136   AST_INIT_VAR: ∀b:bool.∀t:ast_type.
137                 ast_var d e b t → ast_init d e t
138 | AST_INIT_VAL: ∀t:ast_type.
139                 aux_ast_init_type t → ast_init d e t.
140
141 (* -------------------------- *)
142
143 (* statement: assegnamento/while/if else if else *)
144 inductive ast_stm : Πd:nat.aux_env_type d → Type ≝
145   AST_STM_ASG: ∀d.∀e:aux_env_type d.∀t:ast_type.
146                ast_var d e false t → ast_expr d e t → ast_stm d e
147 | AST_STM_WHILE: ∀d.∀e:aux_env_type d.
148                  ast_base_expr d e → ast_decl (S d) (enter_env d e) → ast_stm d e
149 | AST_STM_IF: ∀d.∀e:aux_env_type d.
150               ne_list (Prod (ast_base_expr d e) (ast_decl (S d) (enter_env d e))) → option (ast_decl (S d) (enter_env d e)) → ast_stm d e
151
152 (* dichiarazioni *)
153 with ast_decl : Πd:nat.aux_env_type d → Type ≝
154   AST_NO_DECL: ∀d.∀e:aux_env_type d.
155                list (ast_stm d e) → ast_decl d e
156 | AST_CONST_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
157                   (* D *) (check_not_already_def_env d e str) → ast_init d e t → ast_decl d (add_desc_env d e str true t) → ast_decl d e
158 | AST_VAR_DECL: ∀d.∀e:aux_env_type d.∀str:aux_str_type.∀t:ast_type.
159                 (* D *) (check_not_already_def_env d e str) → option (ast_init d e t) → ast_decl d (add_desc_env d e str false t) → ast_decl d e.
160
161 (* -------------------------- *)
162
163 (* programma *)
164 inductive ast_root : Type ≝
165   AST_ROOT: ast_decl O empty_env → ast_root.
166
167 (* -------------------------- *)
168
169 (* programma vuoto *)
170 definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL O empty_env (nil ?)).