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 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/list_utility.ma".
25 (* ************************* *)
26 (* dimensioni degli elementi *)
27 (* ************************* *)
29 (* usato per definire nell'ast *)
30 ninductive 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 ninductive 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 (* principio di eliminazione arricchito *)
41 nlet rec ast_type_index_aux (P:ast_type → Prop)
42 (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
43 (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
45 (t:ne_list ast_type) on t ≝
46 match t return λt.P (AST_TYPE_STRUCT t) with
47 [ ne_nil h ⇒ f h (f2 h)
48 | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
51 nlet rec ast_type_index (P:ast_type → Prop)
52 (f:Πb.P (AST_TYPE_BASE b))
53 (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
54 (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
55 (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
56 (t:ast_type) on t : P t ≝
57 match t return λt.P t with
58 [ AST_TYPE_BASE b ⇒ f b
59 | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
60 | AST_TYPE_STRUCT nl ⇒ match nl with
61 [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
62 | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t)
66 nlet rec ast_type_rectex_aux (P:ast_type → Type)
67 (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
68 (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
70 (t:ne_list ast_type) on t ≝
71 match t return λt.P (AST_TYPE_STRUCT t) with
72 [ ne_nil h ⇒ f h (f2 h)
73 | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
76 nlet rec ast_type_rectex (P:ast_type → Type)
77 (f:Πb.P (AST_TYPE_BASE b))
78 (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
79 (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
80 (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
81 (t:ast_type) on t : P t ≝
82 match t return λt.P t with
83 [ AST_TYPE_BASE b ⇒ f b
84 | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
85 | AST_TYPE_STRUCT nl ⇒ match nl with
86 [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
87 | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t)
91 ndefinition eq_astbasetype ≝
92 λt1,t2:ast_base_type.match t1 with
93 [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
94 | AST_BASE_TYPE_WORD16 ⇒ match t2 with [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
95 | AST_BASE_TYPE_WORD32 ⇒ match t2 with [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
98 nlet rec eq_asttype (t1,t2:ast_type) on t1 ≝
100 [ AST_TYPE_BASE bType1 ⇒ match t2 with
101 [ AST_TYPE_BASE bType2 ⇒ eq_astbasetype bType1 bType2
103 | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
104 [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_asttype subType1 subType2) ⊗ (eq_nat dim1 dim2)
106 | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
107 [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) nelSubType1 nelSubType2
112 ndefinition is_ast_base_type ≝
113 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
115 ndefinition isb_ast_base_type ≝
116 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
118 ndefinition isnt_ast_base_type ≝
119 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
121 ndefinition isntb_ast_base_type ≝
122 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
124 ndefinition eval_size_base_type ≝
125 λast:ast_base_type.match ast with
126 [ AST_BASE_TYPE_BYTE8 ⇒ nat1
127 | AST_BASE_TYPE_WORD16 ⇒ nat2
128 | AST_BASE_TYPE_WORD32 ⇒ nat4
131 nlet rec eval_size_type (ast:ast_type) on ast ≝
133 [ AST_TYPE_BASE b ⇒ eval_size_base_type b
134 | AST_TYPE_ARRAY sub_ast dim ⇒ (dim + nat1)*(eval_size_type sub_ast)
135 | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast