]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/assembly/compiler/astfe_tree.ma
- exclusion binder in local environments allows to complete lfsx_lfsx !
[helm.git] / matita / matita / contribs / assembly / compiler / astfe_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/env_to_flatenv.ma".
23
24 (* **************************** *)
25 (* ALBERO DI TOKEN CON FLAT ENV *)
26 (* **************************** *)
27
28 (* id: accesso all'ambiente con stringa *)
29 inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝
30   ASTFE_ID: ∀str:aux_strId_type.
31             (* D *) check_desc_flatEnv e str → astfe_id e (get_const_desc (get_desc_flatEnv e str)) (get_type_desc (get_desc_flatEnv e str)).
32
33 (* -------------------------- *)
34
35 (* espressioni *)
36 inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝
37   ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
38 | ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
39 | ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
40
41 | ASTFE_EXPR_NEG: ∀t:ast_base_type.
42                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
43 | ASTFE_EXPR_NOT: ∀t:ast_base_type.
44                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
45 | ASTFE_EXPR_COM: ∀t:ast_base_type.
46                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
47
48 | ASTFE_EXPR_ADD: ∀t:ast_base_type.
49                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
50 | ASTFE_EXPR_SUB: ∀t:ast_base_type.
51                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
52 | ASTFE_EXPR_MUL: ∀t:ast_base_type.
53                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
54 | ASTFE_EXPR_DIV: ∀t:ast_base_type.
55                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
56 | ASTFE_EXPR_SHR: ∀t:ast_base_type.
57                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
58 | ASTFE_EXPR_SHL: ∀t:ast_base_type.
59                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
60 | ASTFE_EXPR_AND: ∀t:ast_base_type.
61                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
62 | ASTFE_EXPR_OR:  ∀t:ast_base_type.
63                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
64 | ASTFE_EXPR_XOR: ∀t:ast_base_type.
65                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
66
67 | ASTFE_EXPR_GT : ∀t:ast_base_type.
68                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
69 | ASTFE_EXPR_GTE: ∀t:ast_base_type.
70                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
71 | ASTFE_EXPR_LT : ∀t:ast_base_type.
72                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
73 | ASTFE_EXPR_LTE: ∀t:ast_base_type.
74                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
75 | ASTFE_EXPR_EQ : ∀t:ast_base_type.
76                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
77 | ASTFE_EXPR_NEQ: ∀t:ast_base_type.
78                   astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
79
80 | ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
81 | ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
82 | ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
83 | ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
84 | ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
85 | ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
86
87 | ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
88                  astfe_var e b t → astfe_expr e t
89
90 (* variabile: modificatori di array/struct dell'id *)
91 with astfe_var : bool → ast_type → Type ≝
92   ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
93                 astfe_id e b t → astfe_var e b t
94 | ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
95                    astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t
96 | ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
97                     astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n)
98
99 (* espressioni generalizzate: anche non uniformi per tipo *)
100 with astfe_base_expr : Type ≝
101   ASTFE_BASE_EXPR: ∀t:ast_base_type.
102                    astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e.
103
104 (* -------------------------- *)
105
106 (*
107  inizializzatori: ammesse solo due forme, no ibridi
108   1) var1 = var2
109   2) var = ... valori ...
110 *) 
111 inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝
112   ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
113                   astfe_var e b t → astfe_init e t
114 | ASTFE_INIT_VAL: ∀t:ast_type.
115                   aux_ast_init_type t → astfe_init e t.
116
117 (* -------------------------- *)
118
119 (* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
120 inductive astfe_stm (e:aux_flatEnv_type) : Type ≝
121   ASTFE_STM_ASG: ∀t:ast_type.
122                  astfe_var e false t → astfe_expr e t → astfe_stm e
123 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
124                   astfe_id e b t → astfe_init e t → astfe_stm e
125 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
126 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
127
128 (* dichiarazioni *)
129 with astfe_body : Type ≝
130   ASTFE_BODY: list (astfe_stm e) → astfe_body e.
131
132 (* -------------------------- *)
133
134 (* programma *)
135 inductive astfe_root (e:aux_flatEnv_type) : Type ≝
136   ASTFE_ROOT: astfe_body e → astfe_root e.
137
138 (* -------------------------- *)
139
140 (* programma vuoto *)
141 definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (nil ?)).