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 "compiler/ast_base_type.ma".
24 include "common/nelist.ma".
26 (* ************************* *)
27 (* dimensioni degli elementi *)
28 (* ************************* *)
30 ninductive ast_type : Type ≝
31 AST_TYPE_BASE: ast_base_type → ast_type
32 | AST_TYPE_ARRAY: ast_type → nat → ast_type
33 | AST_TYPE_STRUCT: ne_list ast_type → ast_type.
35 (* principio di eliminazione arricchito *)
36 nlet rec ast_type_index_aux (P:ast_type → Prop)
37 (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
38 (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
40 (t:ne_list ast_type) on t ≝
41 match t return λt.P (AST_TYPE_STRUCT t) with
42 [ ne_nil h ⇒ f h (f2 h)
43 | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
46 nlet rec ast_type_index (P:ast_type → Prop)
47 (f:Πb.P (AST_TYPE_BASE b))
48 (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
49 (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
50 (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
51 (t:ast_type) on t : P t ≝
52 match t return λt.P t with
53 [ AST_TYPE_BASE b ⇒ f b
54 | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
55 | AST_TYPE_STRUCT nl ⇒ match nl with
56 [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
57 | 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)
61 nlet rec ast_type_rectex_aux (P:ast_type → Type)
62 (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
63 (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
65 (t:ne_list ast_type) on t ≝
66 match t return λt.P (AST_TYPE_STRUCT t) with
67 [ ne_nil h ⇒ f h (f2 h)
68 | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
71 nlet rec ast_type_rectex (P:ast_type → Type)
72 (f:Πb.P (AST_TYPE_BASE b))
73 (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
74 (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
75 (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
76 (t:ast_type) on t : P t ≝
77 match t return λt.P t with
78 [ AST_TYPE_BASE b ⇒ f b
79 | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
80 | AST_TYPE_STRUCT nl ⇒ match nl with
81 [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
82 | 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)
86 nlet rec eq_asttype (t1,t2:ast_type) on t1 ≝
88 [ AST_TYPE_BASE bType1 ⇒ match t2 with
89 [ AST_TYPE_BASE bType2 ⇒ eqc ? bType1 bType2
91 | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
92 [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_asttype subType1 subType2) ⊗ (eqc ? dim1 dim2)
94 | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
95 [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) nelSubType1 nelSubType2
100 ndefinition is_ast_base_type ≝
101 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
103 ndefinition isb_ast_base_type ≝
104 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
106 ndefinition isnt_ast_base_type ≝
107 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
109 ndefinition isntb_ast_base_type ≝
110 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
112 ndefinition eval_size_base_type ≝
113 λast:ast_base_type.match ast with
114 [ AST_BASE_TYPE_BYTE8 ⇒ nat1
115 | AST_BASE_TYPE_WORD16 ⇒ nat2
116 | AST_BASE_TYPE_WORD32 ⇒ nat4
119 nlet rec eval_size_type (ast:ast_type) on ast ≝
121 [ AST_TYPE_BASE b ⇒ eval_size_base_type b
122 | AST_TYPE_ARRAY sub_ast dim ⇒ (dim + nat1)*(eval_size_type sub_ast)
123 | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast