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/utility.ma".
23 include "freescale/word32.ma".
25 (* ************************* *)
26 (* dimensioni degli elementi *)
27 (* ************************* *)
29 (* usato per definire nell'ast *)
30 inductive ast_base_type : Type ≝
31 AST_BASE_TYPE_BYTE8: ast_base_type
32 | AST_BASE_TYPE_WORD16: ast_base_type
33 | AST_BASE_TYPE_WORD32: ast_base_type.
35 inductive ast_type : Type ≝
36 AST_TYPE_BASE: ast_base_type → ast_type
37 | AST_TYPE_ARRAY: ast_type → nat → ast_type
38 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
40 definition eq_ast_base_type ≝
41 λt1,t2:ast_base_type.match t1 with
42 [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with
43 [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
44 | AST_BASE_TYPE_WORD16 ⇒ match t2 with
45 [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
46 | AST_BASE_TYPE_WORD32 ⇒ match t2 with
47 [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
50 lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = true) → (t1 = t2).
51 unfold eq_ast_base_type;
60 lemma eq_to_eqastbasetype : ∀t1,t2.t1 = t2 → eq_ast_base_type t1 t2 = true.
70 definition eq_ast_type_aux ≝
71 λT:Type.λf:T → T → bool.
72 let rec aux (nl1,nl2:ne_list T) on nl1 ≝
74 [ ne_nil h ⇒ match nl2 with
76 | ne_cons h' _ ⇒ false
78 | ne_cons h t ⇒ match nl2 with
80 | ne_cons h' t' ⇒ (f h h') ⊗ (aux t t')
84 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
86 [ AST_TYPE_BASE bType1 ⇒ match t2 with
87 [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 | _ ⇒ false ]
88 | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
89 [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
90 | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
91 [ AST_TYPE_STRUCT nelSubType2 ⇒ eq_ast_type_aux ? eq_ast_type nelSubType1 nelSubType2
95 lemma eq_ast_type_elim :
97 (∀x.P (AST_TYPE_BASE x)) →
98 (∀t:ast_type.∀n.(P t) → (P (AST_TYPE_ARRAY t n))) →
99 (∀x.(P x) → (P (AST_TYPE_STRUCT (ne_nil ? x)))) →
100 (∀x,l.(P x) → (P (AST_TYPE_STRUCT l)) → (P (AST_TYPE_STRUCT (ne_cons ? x l)))) →
108 [ AST_TYPE_BASE b ⇒ H b
109 | AST_TYPE_ARRAY t n ⇒ H1 t n (aux t)
110 | AST_TYPE_STRUCT l ⇒
111 let rec aux_l (l:ne_list ast_type ) ≝
113 return λl.P (AST_TYPE_STRUCT l)
115 [ ne_nil t => H2 t (aux t)
116 | ne_cons hd tl => H3 hd tl (aux hd) (aux_l tl)
121 lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
123 elim t1 using eq_ast_type_elim 0;
125 elim t2 using eq_ast_type_elim 0;
128 rewrite > (eqastbasetype_to_eq ?? H);
141 elim t2 using eq_ast_type_elim 0;
147 lapply (andb_true_true ?? H2) as H3;
148 lapply (andb_true_true_r ?? H2) as H4;
150 rewrite > (eqb_true_to_eq ?? H4);
160 elim t2 using eq_ast_type_elim 0;
178 elim t2 using eq_ast_type_elim 0;
190 lapply (andb_true_true ?? H4) as H5;
191 lapply (andb_true_true_r ?? H4) as H6;
193 lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
202 lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
204 elim t1 using eq_ast_type_elim 0;
206 elim t2 using eq_ast_type_elim 0;
210 apply (eq_to_eqastbasetype x x (refl_eq ??))
222 elim t2 using eq_ast_type_elim 0;
229 rewrite > (H t (refl_eq ??));
230 rewrite > (eq_to_eqb_true n n (refl_eq ??));
240 elim t2 using eq_ast_type_elim 0;
250 rewrite > (H x (refl_eq ??));
257 elim t2 using eq_ast_type_elim 0;
270 rewrite > (H x (refl_eq ??));
271 rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
277 definition is_ast_base_type ≝
278 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
280 definition isb_ast_base_type ≝
281 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
283 lemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
284 unfold isb_ast_base_type;
285 unfold is_ast_base_type;
288 [ normalize; autobatch |
289 normalize; autobatch |
290 normalize; autobatch ]
293 definition isnt_ast_base_type ≝
294 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
296 definition isntb_ast_base_type ≝
297 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
299 lemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
300 unfold isntb_ast_base_type;
301 unfold isnt_ast_base_type;
304 [ normalize; autobatch |
305 normalize; autobatch |
306 normalize; autobatch ]
309 definition eval_size_base_type ≝
310 λast:ast_base_type.match ast with
311 [ AST_BASE_TYPE_BYTE8 ⇒ 1
312 | AST_BASE_TYPE_WORD16 ⇒ 2
313 | AST_BASE_TYPE_WORD32 ⇒ 4
316 let rec eval_size_type (ast:ast_type) on ast ≝
318 [ AST_TYPE_BASE b ⇒ eval_size_base_type b
319 | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
320 | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast