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 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
62 [ AST_TYPE_BASE bType1 ⇒ match t2 with
63 [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 | _ ⇒ false ]
64 | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
65 [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
66 | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
67 [ AST_TYPE_STRUCT nelSubType2 ⇒
68 fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
69 [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
70 [ None ⇒ pair ?? false (S (snd ?? t))
71 | Some cfr ⇒ match eq_ast_type h cfr with
72 [ true ⇒ pair ?? true (S (snd ?? t))
73 | false ⇒ pair ?? false (S (snd ?? t)) ]]
74 | false ⇒ t]) (pair ?? true O) nelSubType1)
78 lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
80 elim t1 0; [1,3:intros 2 | intros 4] elim t2;
81 [ 2,5,7,9: normalize in H1; destruct H1;
82 | 3,4: normalize in H; destruct H;
84 apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
86 lapply (andb_true_true ? ? H2);
87 lapply (andb_true_true_r ? ? H2); clear H2;
88 rewrite > (H ? Hletin);
89 rewrite > (eqb_true_to_eq ?? Hletin1);
95 definition is_ast_base_type ≝
96 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
98 definition isb_ast_base_type ≝
99 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
101 lemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
102 unfold isb_ast_base_type;
103 unfold is_ast_base_type;
106 [ normalize; autobatch |
107 normalize; autobatch |
108 normalize; autobatch ]
111 definition isnt_ast_base_type ≝
112 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
114 definition isntb_ast_base_type ≝
115 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
117 lemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
118 unfold isntb_ast_base_type;
119 unfold isnt_ast_base_type;
122 [ normalize; autobatch |
123 normalize; autobatch |
124 normalize; autobatch ]
127 definition eval_size_base_type ≝
128 λast:ast_base_type.match ast with
129 [ AST_BASE_TYPE_BYTE8 ⇒ 1
130 | AST_BASE_TYPE_WORD16 ⇒ 2
131 | AST_BASE_TYPE_WORD32 ⇒ 4
134 let rec eval_size_type (ast:ast_type) on ast ≝
136 [ AST_TYPE_BASE b ⇒ eval_size_base_type b
137 | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
138 | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast