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/ast_to_astfe.ma".
23 include "compiler/preast_to_ast.ma".
25 definition parsingResult \def
33 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
37 (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
39 (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
45 (PREAST_INIT_VAL_ARRAY
47 (PREAST_INIT_VAL_STRUCT
49 (PREAST_INIT_VAL_ARRAY
51 (PREAST_INIT_VAL_BYTE8 (\langle x0,x0 \rangle))
53 (PREAST_INIT_VAL_BYTE8 (\langle x0,x1 \rangle))
57 (PREAST_INIT_VAL_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle))
59 (PREAST_INIT_VAL_WORD32 (\langle \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle . \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle \rangle))
63 (PREAST_INIT_VAL_STRUCT
65 (PREAST_INIT_VAL_ARRAY
67 (PREAST_INIT_VAL_BYTE8 (\langle x0,x2 \rangle))
69 (PREAST_INIT_VAL_BYTE8 (\langle x0,x3 \rangle))
73 (PREAST_INIT_VAL_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle))
75 (PREAST_INIT_VAL_WORD32 (\langle \langle \langle x0,x0 \rangle : \langle x0,x0 \rangle \rangle . \langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle \rangle))
83 (AST_TYPE_BASE AST_BASE_TYPE_WORD16)
88 (PREAST_VAR_ID ([ch_n;ch_1]))
89 (PREAST_EXPR_BYTE8 (\langle x0,x0 \rangle))
97 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
103 (PREAST_VAR_ID ([ch_n;ch_2]))
107 (AST_TYPE_BASE AST_BASE_TYPE_WORD32)
112 (PREAST_VAR_ID ([ch_n;ch_1]))
114 (PREAST_VAR_ID ([ch_n;ch_2]))
129 (PREAST_VAR_ID ([ch_n;ch_1]))
131 (PREAST_EXPR_WORD32 (\langle \langle \langle x1,x2 \rangle : \langle x3,x4 \rangle \rangle . \langle \langle xA,xB \rangle : \langle xC,xD \rangle \rangle \rangle))
136 (PREAST_VAR_ID ([ch_n;ch_3]))
146 (PREAST_EXPR_W16toW32
149 (PREAST_VAR_ID ([ch_n;ch_3]))
154 (PREAST_EXPR_BYTE8 (\langle x0,x1 \rangle))
158 (PREAST_EXPR_BYTE8 (\langle x0,x2 \rangle))
159 (PREAST_EXPR_BYTE8 (\langle x0,x3 \rangle))
161 (PREAST_EXPR_BYTE8 (\langle x0,x4 \rangle))
165 (PREAST_EXPR_BYTE8 (\langle x0,x5 \rangle))
166 (PREAST_EXPR_BYTE8 (\langle x0,x6 \rangle))
169 (PREAST_EXPR_BYTE8 (\langle x0,x7 \rangle))
172 (PREAST_EXPR_BYTE8 (\langle x0,x8 \rangle))
173 (PREAST_EXPR_BYTE8 (\langle x0,x9 \rangle))
188 (PREAST_VAR_ID ([ch_n;ch_2]))
191 (PREAST_VAR_ID ([ch_n;ch_2]))
193 (PREAST_EXPR_WORD16 (\langle \langle x0,x0 \rangle : \langle x0,x1 \rangle \rangle))
202 (PREAST_VAR_ID ([ch_n;ch_3]))
207 (PREAST_VAR_ID ([ch_n;ch_1]))
208 (PREAST_EXPR_BYTE8 (\langle x0,x1 \rangle))
212 (PREAST_EXPR_BYTE8 (\langle x0,x0 \rangle))
223 lemma pippo : ∃b.preast_to_ast parsingResult = Some ? b.
226 [ apply (match preast_to_ast parsingResult with [ None ⇒ AST_ROOT (AST_NO_DECL O empty_env []) | Some x ⇒ x]);