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".
26 include "compiler/env_to_flatenv1.ma".
27 include "compiler/ast_tree.ma".
29 (* **************************** *)
30 (* ALBERO DI TOKEN CON FLAT ENV *)
31 (* **************************** *)
33 (* id: accesso all'ambiente con stringa *)
34 inductive astfe_id (e:aux_flatEnv_type) : bool → ast_type → Type ≝
35 ASTFE_ID: ∀str:aux_strId_type.
36 (* 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)).
38 (* -------------------------- *)
41 inductive astfe_expr (e:aux_flatEnv_type) : ast_type → Type ≝
42 ASTFE_EXPR_BYTE8 : byte8 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
43 | ASTFE_EXPR_WORD16: word16 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
44 | ASTFE_EXPR_WORD32: word32 → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
46 | ASTFE_EXPR_NEG: ∀t:ast_base_type.
47 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
48 | ASTFE_EXPR_NOT: ∀t:ast_base_type.
49 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
50 | ASTFE_EXPR_COM: ∀t:ast_base_type.
51 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
53 | ASTFE_EXPR_ADD: ∀t:ast_base_type.
54 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
55 | ASTFE_EXPR_SUB: ∀t:ast_base_type.
56 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
57 | ASTFE_EXPR_MUL: ∀t:ast_base_type.
58 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
59 | ASTFE_EXPR_DIV: ∀t:ast_base_type.
60 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t)
61 | ASTFE_EXPR_SHR: ∀t:ast_base_type.
62 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
63 | ASTFE_EXPR_SHL: ∀t:ast_base_type.
64 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE t)
66 | ASTFE_EXPR_GT : ∀t:ast_base_type.
67 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
68 | ASTFE_EXPR_GTE: ∀t:ast_base_type.
69 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
70 | ASTFE_EXPR_LT : ∀t:ast_base_type.
71 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
72 | ASTFE_EXPR_LTE: ∀t:ast_base_type.
73 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
74 | ASTFE_EXPR_EQ : ∀t:ast_base_type.
75 astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE t) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
76 | ASTFE_EXPR_NEQ: ∀t:ast_base_type.
77 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 | ASTFE_EXPR_B8toW16 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
80 | ASTFE_EXPR_B8toW32 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
81 | ASTFE_EXPR_W16toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
82 | ASTFE_EXPR_W16toW32: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
83 | ASTFE_EXPR_W32toB8 : astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
84 | ASTFE_EXPR_W32toW16: astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → astfe_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
86 | ASTFE_EXPR_ID: ∀b:bool.∀t:ast_type.
87 astfe_var e b t → astfe_expr e t
89 (* variabile: modificatori di array/struct dell'id *)
90 with astfe_var : bool → ast_type → Type ≝
91 ASTFE_VAR_ID: ∀b:bool.∀t:ast_type.
92 astfe_id e b t → astfe_var e b t
93 | ASTFE_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
94 astfe_var e b (AST_TYPE_ARRAY t n) → astfe_base_expr e → astfe_var e b t
95 | ASTFE_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
96 astfe_var e b (AST_TYPE_STRUCT nel) → astfe_var e b (abs_nth_neList ? nel n)
98 (* espressioni generalizzate: anche non uniformi per tipo *)
99 with astfe_base_expr : Type ≝
100 ASTFE_BASE_EXPR: ∀t:ast_base_type.
101 astfe_expr e (AST_TYPE_BASE t) → astfe_base_expr e.
103 (* -------------------------- *)
106 inizializzatori: ammesse solo due forme, no ibridi
108 2) var = ... valori ...
110 inductive astfe_init (e:aux_flatEnv_type) : ast_type → Type ≝
111 ASTFE_INIT_VAR: ∀b:bool.∀t:ast_type.
112 astfe_var e b t → astfe_init e t
113 | ASTFE_INIT_VAL: ∀t:ast_type.
114 aux_ast_init_type t → astfe_init e t.
116 (* -------------------------- *)
118 (* statement: assegnamento/while/if else if else + conversione di dichiarazione *)
119 inductive astfe_stm (e:aux_flatEnv_type) : Type ≝
120 ASTFE_STM_ASG: ∀t:ast_type.
121 astfe_var e false t → astfe_expr e t → astfe_stm e
122 | ASTFE_STM_INIT: ∀b:bool.∀t:ast_type.
123 astfe_id e b t → astfe_init e t → astfe_stm e
124 | ASTFE_STM_WHILE: astfe_base_expr e → astfe_body e → astfe_stm e
125 | ASTFE_STM_IF: ne_list (Prod (astfe_base_expr e) (astfe_body e)) → option (astfe_body e) → astfe_stm e
128 with astfe_body : Type ≝
129 ASTFE_BODY: list (astfe_stm e) → astfe_body e.
131 (* -------------------------- *)
134 inductive astfe_root (e:aux_flatEnv_type) : Type ≝
135 ASTFE_ROOT: astfe_body e → astfe_root e.
137 (* -------------------------- *)
139 (* programma vuoto *)
140 definition empty_astfe_prog ≝ ASTFE_ROOT empty_flatEnv (ASTFE_BODY empty_flatEnv (nil ?)).