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 let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
52 [ AST_TYPE_BASE bType1 ⇒ match t2 with
53 [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 | _ ⇒ false ]
54 | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
55 [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eqb dim1 dim2) | _ ⇒ false ]
56 | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
57 [ AST_TYPE_STRUCT nelSubType2 ⇒
58 fst ?? (fold_right_neList ?? (λh,t.match fst ?? t with
59 [ true ⇒ match nth_neList ? nelSubType2 ((len_neList ? nelSubType2)-(snd ?? t)-1) with
60 [ None ⇒ pair ?? false (S (snd ?? t))
61 | Some cfr ⇒ match eq_ast_type h cfr with
62 [ true ⇒ pair ?? true (S (snd ?? t))
63 | false ⇒ pair ?? false (S (snd ?? t)) ]]
64 | false ⇒ t]) (pair ?? true O) nelSubType1)
68 definition is_ast_base_type ≝
69 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
71 definition isb_ast_base_type ≝
72 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
74 lemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
75 unfold isb_ast_base_type;
76 unfold is_ast_base_type;
79 [ normalize; autobatch |
80 normalize; autobatch |
81 normalize; autobatch ]
84 definition isnt_ast_base_type ≝
85 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
87 definition isntb_ast_base_type ≝
88 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
90 lemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
91 unfold isntb_ast_base_type;
92 unfold isnt_ast_base_type;
95 [ normalize; autobatch |
96 normalize; autobatch |
97 normalize; autobatch ]
100 definition eval_size_base_type ≝
101 λast:ast_base_type.match ast with
102 [ AST_BASE_TYPE_BYTE8 ⇒ 1
103 | AST_BASE_TYPE_WORD16 ⇒ 2
104 | AST_BASE_TYPE_WORD32 ⇒ 4
107 let rec eval_size_type (ast:ast_type) on ast ≝
109 [ AST_TYPE_BASE b ⇒ eval_size_base_type b
110 | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast)
111 | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast