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 "compiler/environment.ma".
28 (* id: accesso all'ambiente con stringa *)
29 inductive ast_id (e:aux_env_type) : bool → ast_type → Type ≝
30 AST_ID: ∀str:aux_str_type.
31 (* D *) (check_desc_env e str) → (ast_id e (get_const_desc (get_desc_env e str)) (get_type_desc (get_desc_env e str))).
33 (* -------------------------- *)
36 inductive ast_expr (e:aux_env_type) : ast_type → Type ≝
37 AST_EXPR_BYTE8 : byte8 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
38 | AST_EXPR_WORD16: word16 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
39 | AST_EXPR_WORD32: word32 → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
41 | AST_EXPR_NEG: ∀t:ast_base_type.
42 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
43 | AST_EXPR_NOT: ∀t:ast_base_type.
44 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
45 | AST_EXPR_COM: ∀t:ast_base_type.
46 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
48 | AST_EXPR_ADD: ∀t:ast_base_type.
49 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
50 | AST_EXPR_SUB: ∀t:ast_base_type.
51 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
52 | AST_EXPR_MUL: ∀t:ast_base_type.
53 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
54 | AST_EXPR_DIV: ∀t:ast_base_type.
55 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t)
56 | AST_EXPR_SHR: ∀t:ast_base_type.
57 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
58 | AST_EXPR_SHL: ∀t:ast_base_type.
59 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE t)
61 | AST_EXPR_GT : ∀t:ast_base_type.
62 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
63 | AST_EXPR_GTE: ∀t:ast_base_type.
64 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
65 | AST_EXPR_LT : ∀t:ast_base_type.
66 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
67 | AST_EXPR_LTE: ∀t:ast_base_type.
68 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
69 | AST_EXPR_EQ : ∀t:ast_base_type.
70 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
71 | AST_EXPR_NEQ: ∀t:ast_base_type.
72 ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE t) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
74 | AST_EXPR_B8toW16 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
75 | AST_EXPR_B8toW32 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
76 | AST_EXPR_W16toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
77 | AST_EXPR_W16toW32: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
78 | AST_EXPR_W32toB8 : ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
79 | AST_EXPR_W32toW16: ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD32) → ast_expr e (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
81 | AST_EXPR_ID: ∀b:bool.∀t:ast_type.
82 ast_var e b t → ast_expr e t
84 (* variabile: modificatori di array/struct dell'id *)
85 with ast_var : bool → ast_type → Type ≝
86 AST_VAR_ID: ∀b:bool.∀t:ast_type.
87 ast_id e b t → ast_var e b t
88 | AST_VAR_ARRAY: ∀b:bool.∀t:ast_type.∀n:nat.
89 ast_var e b (AST_TYPE_ARRAY t n) → ast_base_expr e → ast_var e b t
90 | AST_VAR_STRUCT: ∀b:bool.∀nel:ne_list ast_type.∀n:nat.
91 ast_var e b (AST_TYPE_STRUCT nel) → (* D *) (ltb n (len_neList ? nel) = true) → ast_var e b (abs_nth_neList ? nel n)
93 (* espressioni generalizzate: anche non uniformi per tipo *)
94 with ast_base_expr : Type ≝
95 AST_BASE_EXPR: ∀t:ast_base_type.
96 ast_expr e (AST_TYPE_BASE t) → ast_base_expr e.
98 (* -------------------------- *)
100 let rec aux_ast_init_type (t:ast_type) on t : Type ≝
102 [ AST_TYPE_BASE bType ⇒ match bType with
103 [ AST_BASE_TYPE_BYTE8 ⇒ byte8
104 | AST_BASE_TYPE_WORD16 ⇒ word16
105 | AST_BASE_TYPE_WORD32 ⇒ word32
107 | AST_TYPE_ARRAY subType dim ⇒
108 let T ≝ aux_ast_init_type subType in
109 let rec aux (n:nat) on n ≝
112 | S n' ⇒ Prod T (aux n')
115 | AST_TYPE_STRUCT nelSubType ⇒
116 let rec aux (nel:ne_list ast_type) on nel ≝
118 [ ne_nil h ⇒ aux_ast_init_type h
119 | ne_cons h t ⇒ Prod (aux_ast_init_type h) (aux t)
125 inizializzatori: ammesse solo due forme, no ibridi
127 2) var = ... valori ...
129 inductive ast_init (e:aux_env_type) : ast_type → Type ≝
130 AST_INIT_VAR: ∀b:bool.∀t:ast_type.
131 ast_var e b t → ast_init e t
132 | AST_INIT_VAL: ∀t:ast_type.
133 aux_ast_init_type t → ast_init e t.
135 (* -------------------------- *)
137 (* statement: assegnamento/while/if else if else *)
138 inductive ast_stm : aux_env_type → Type ≝
139 AST_STM_ASG: ∀e:aux_env_type.∀t:ast_type.
140 ast_var e false t → ast_expr e t → ast_stm e
141 | AST_STM_WHILE: ∀e:aux_env_type.
142 ast_base_expr e → ast_decl (enter_env e) → ast_stm e
143 | AST_STM_IF: ∀e:aux_env_type.
144 ne_list (Prod (ast_base_expr e) (ast_decl (enter_env e))) → option (ast_decl (enter_env e)) → ast_stm e
147 with ast_decl : aux_env_type → Type ≝
148 AST_NO_DECL: ∀e:aux_env_type.
149 list (ast_stm e) → ast_decl e
150 | AST_DECL: ∀e:aux_env_type.∀c:bool.∀str:aux_str_type.∀t:ast_type.
151 (* D *) (check_not_already_def_env e str) → option (ast_init e t) → ast_decl (add_desc_env e str c t) → ast_decl e.
153 (* -------------------------- *)
156 inductive ast_root : Type ≝
157 AST_ROOT: ast_decl empty_env → ast_root.
159 (* -------------------------- *)
161 (* programma vuoto *)
162 definition empty_ast_prog ≝ AST_ROOT (AST_NO_DECL empty_env (nil ?)).