-
Notifications
You must be signed in to change notification settings - Fork 9
/
Types.v
378 lines (314 loc) · 11.8 KB
/
Types.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
(*! Language | Types used by Kôika programs !*)
Require Export Coq.Strings.String.
Require Export Koika.Common Koika.IndexUtils.
(** * Definitions **)
Record struct_sig' {A} :=
{ struct_name: string;
struct_fields: list (string * A) }.
Arguments struct_sig' : clear implicits.
Record enum_sig :=
{ enum_name: string;
enum_size: nat;
enum_bitsize: nat;
enum_members: vect string enum_size;
enum_bitpatterns: vect (bits enum_bitsize) enum_size }.
Record array_sig' {A} :=
{ array_type: A;
array_len: nat }.
Arguments array_sig' : clear implicits.
Inductive type : Type :=
| bits_t (sz: nat)
| enum_t (sig: enum_sig)
| struct_t (sig: struct_sig' type)
| array_t (sig: array_sig' type).
Notation unit_t := (bits_t 0).
Notation struct_sig := (struct_sig' type).
Notation array_sig := (array_sig' type).
Inductive type_kind :=
| kind_bits
| kind_enum (sig: option enum_sig)
| kind_struct (sig: option struct_sig)
| kind_array (sig: option array_sig).
Definition kind_of_type (tau: type) :=
match tau with
| bits_t sz => kind_bits
| enum_t sig => kind_enum (Some sig)
| struct_t sig => kind_struct (Some sig)
| array_t sig => kind_array (Some sig)
end.
Definition struct_fields_sz' (type_sz: type -> nat) (fields: list (string * type)) :=
list_sum (List.map (fun nm_tau => type_sz (snd nm_tau)) fields).
Fixpoint type_sz tau :=
match tau with
| bits_t sz => sz
| enum_t sig => sig.(enum_bitsize)
| struct_t sig => struct_fields_sz' type_sz sig.(struct_fields)
| array_t sig => Bits.rmul sig.(array_len) (type_sz sig.(array_type))
end.
Notation struct_fields_sz := (struct_fields_sz' type_sz).
Definition struct_index (sig: struct_sig) :=
Vect.index (List.length sig.(struct_fields)).
Definition struct_sz sig :=
type_sz (struct_t sig).
Definition field_type (sig: struct_sig) idx :=
snd (List_nth sig.(struct_fields) idx).
Definition field_sz (sig: struct_sig) idx :=
type_sz (field_type sig idx).
Definition field_offset_left (sig: struct_sig) (idx: struct_index sig) :=
let prev_fields := List.firstn (index_to_nat idx) sig.(struct_fields) in
struct_fields_sz prev_fields.
Definition field_offset_right (sig: struct_sig) (idx: struct_index sig) :=
let next_fields := List.skipn (S (index_to_nat idx)) sig.(struct_fields) in
struct_fields_sz next_fields.
Definition array_index (sig: array_sig) :=
Vect.index sig.(array_len).
Definition array_sz sig :=
type_sz (array_t sig).
Definition element_sz (sig: array_sig) :=
type_sz sig.(array_type).
Definition element_offset_right (sig: array_sig) (idx: array_index sig) :=
Bits.rmul (sig.(array_len) - S (Vect.index_to_nat idx)) (element_sz sig).
Notation struct_bits_t sig :=
(bits_t (struct_sz sig)).
Notation field_bits_t sig idx :=
(bits_t (field_sz sig idx)).
Inductive Port :=
P0 | P1.
(** * Denotations *)
Definition struct_denote' (type_denote: type -> Type) (fields: list (string * type)) :=
List.fold_right (fun k_tau acc => type_denote (snd k_tau) * acc)%type unit fields.
Fixpoint type_denote tau : Type :=
match tau with
| bits_t sz => bits sz
| enum_t sig => bits sig.(enum_bitsize)
| struct_t sig => struct_denote' type_denote sig.(struct_fields)
| array_t sig => vect (type_denote sig.(array_type)) sig.(array_len)
end.
Notation struct_denote := (struct_denote' type_denote).
(** * Bit representations **)
Fixpoint bits_of_value {tau: type} (x: type_denote tau) {struct tau} : bits (type_sz tau) :=
let bits_of_struct_value :=
(fix bits_of_struct_value
{fields}
(x: struct_denote fields)
: bits (struct_fields_sz fields) :=
match fields return struct_denote fields -> bits (struct_fields_sz fields) with
| [] => fun _ => vect_nil
| (nm, tau) :: fields => fun '(x, xs) => Bits.app (bits_of_value x) (bits_of_struct_value xs)
end x) in
match tau return type_denote tau -> bits (type_sz tau) with
| bits_t _ => fun bs => bs
| enum_t _ => fun bs => bs
| struct_t _ => fun str => bits_of_struct_value str
| array_t _ => fun v => Bits.appn (vect_map bits_of_value v)
end x.
Fixpoint value_of_bits {tau: type} (bs: bits (type_sz tau)) {struct tau}: type_denote tau :=
let value_of_struct_bits :=
(fix value_of_struct_bits
{fields: list (string * type)}
(bs: bits (struct_fields_sz fields))
: struct_denote fields :=
match fields return bits (struct_fields_sz fields) -> struct_denote fields with
| [] => fun bs => tt
| (nm, tau) :: fields =>
fun bs =>
let splt := Bits.split bs in
let hd := value_of_bits (snd splt) in
let tl := value_of_struct_bits (fst splt) in
(hd, tl)
end bs) in
match tau return bits (type_sz tau) -> type_denote tau with
| bits_t _ => fun bs => bs
| enum_t _ => fun bs => bs
| struct_t _ => fun bs => value_of_struct_bits bs
| array_t _ => fun bs => vect_map value_of_bits (Bits.splitn bs)
end bs.
Example ex__bits_of_value :=
Eval simpl in
let t := struct_t
{| struct_name := "xyz";
struct_fields :=
[("mm_typ", bits_t 2);
("addr", bits_t 8);
("data", array_t {| array_type := bits_t 2;
array_len := 3 |})] |}%string in
let mm_typ := Ob~0~1 in
let mm_addr := Ob~1~1~1~1~0~0~0~0 in
let mm_data := [Ob~1~0; Ob~0~0; Ob~1~1]%vect in
bits_of_value ((mm_typ, (mm_addr, (mm_data, tt))): type_denote t).
(* [ex__bits_of_value = Ob~0~1~1~1~1~1~0~0~0~0~1~0~0~0~1~1 : bits 16] *)
Definition bits_of_value_of_bits :
forall tau (bs: bits (type_sz tau)),
bits_of_value (value_of_bits bs) = bs.
Proof.
fix IHtau 1; destruct tau as [sz | sig | sig | sig]; cbn.
- reflexivity.
- reflexivity.
- destruct sig; cbn.
revert struct_fields0.
fix IHfields 1. destruct struct_fields0 as [ | (nm & tau) struct_fields0 ]; cbn.
+ destruct bs; reflexivity.
+ intros; rewrite IHtau, IHfields; apply vect_app_split.
- intros;
erewrite vect_map_map, (vect_map_id _ (IHtau _)), Bits.appn_splitn;
reflexivity.
Qed.
Definition value_of_bits_of_value :
forall tau (v: type_denote tau),
(value_of_bits (bits_of_value v)) = v.
Proof.
fix IHt 1; destruct tau as [sz | sig | sig | sig]; cbn.
- reflexivity.
- reflexivity.
- destruct sig; cbn.
revert struct_fields0.
fix IH 1. destruct struct_fields0 as [ | (nm & tau) struct_fields0 ]; cbn.
+ destruct v; reflexivity.
+ cbn.
intros.
rewrite (surjective_pairing v).
unfold Bits.split.
rewrite vect_split_app.
cbn.
rewrite IH, IHt.
reflexivity.
- intros;
erewrite Bits.splitn_appn, vect_map_map, (vect_map_id _ (IHt _));
reflexivity.
Qed.
Lemma bits_of_value_inj :
forall {tau: type} (x y: type_denote tau),
bits_of_value x = bits_of_value y ->
x = y.
Proof.
intros * H%(f_equal value_of_bits);
rewrite !value_of_bits_of_value in H;
auto.
Qed.
Lemma value_of_bits_inj :
forall {tau: type} (bs0 bs1: bits (type_sz tau)),
value_of_bits bs0 = value_of_bits bs1 ->
bs0 = bs1.
Proof.
intros * H%(f_equal bits_of_value);
rewrite !bits_of_value_of_bits in H;
auto.
Qed.
(** * Coercions **)
Coercion type_denote : type >-> Sortclass.
(** * Anonymous function signatures **)
Record _Sig {argKind: Type} {nArgs: nat} :=
{ argSigs : vect argKind nArgs; retSig : argKind }.
Arguments _Sig : clear implicits.
Fixpoint _Sig_denote {nArgs argKind} (type_of_argKind: argKind -> Type)
(args: vect argKind nArgs) (ret: argKind) :=
match nArgs return vect argKind nArgs -> Type with
| 0 => fun _ => type_of_argKind ret
| S n => fun arg => type_of_argKind (vect_hd arg) ->
_Sig_denote type_of_argKind (vect_tl arg) ret
end args.
Notation Sig n := (_Sig type n).
Notation CSig n := (_Sig nat n).
Definition CSig_denote {n} (sg: CSig n) :=
_Sig_denote (@Bits.bits) sg.(argSigs) sg.(retSig).
Definition Sig_denote {n} (sg: Sig n) :=
_Sig_denote type_denote sg.(argSigs) sg.(retSig).
Definition CSig_of_Sig {n} (sig: Sig n) : CSig n :=
{| argSigs := vect_map type_sz sig.(argSigs);
retSig := type_sz sig.(retSig) |}.
Definition Sig_of_CSig {n} (sig: CSig n) : Sig n :=
{| argSigs := vect_map bits_t sig.(argSigs);
retSig := bits_t sig.(retSig) |}.
Notation arg1Sig fsig := (vect_hd fsig.(argSigs)).
Notation arg2Sig fsig := (vect_hd (vect_tl fsig.(argSigs))).
Module SigNotations.
Notation "{$ a1 ~> ret $}" :=
{| argSigs := vect_cons a1 vect_nil;
retSig := ret |}.
Notation "{$ a1 ~> a2 ~> ret $}" :=
{| argSigs := vect_cons a1 (vect_cons a2 vect_nil);
retSig := ret |}.
End SigNotations.
(** * External functions **)
Definition ExternalSignature := Sig 1.
Definition CExternalSignature := CSig 1.
(** * Internal functions **)
Definition tsig var_t := list (var_t * type).
Definition lsig := list nat.
Record InternalFunction {var_t fn_name_t action: Type} :=
{ int_name : fn_name_t;
int_argspec : tsig var_t;
int_retSig : type;
int_body : action }.
Arguments InternalFunction : clear implicits.
Arguments Build_InternalFunction {var_t fn_name_t action}
int_name int_argspec int_retSig int_body : assert.
Definition map_intf_body {var_t fn_name_t action action': Type}
(f: action -> action') (fn: InternalFunction var_t fn_name_t action) :=
{| int_name := fn.(int_name);
int_argspec := fn.(int_argspec);
int_retSig := fn.(int_retSig);
int_body := f fn.(int_body) |}.
Record arg_sig {var_t} :=
{ arg_name: var_t;
arg_type: type }.
Arguments arg_sig : clear implicits.
Definition prod_of_argsig {var_t} (a: @arg_sig var_t) :=
(a.(arg_name), a.(arg_type)).
(** * Debugging and disambiguation of type names **)
Fixpoint type_id (tau: type) : string :=
match tau with
| bits_t sz => "bits_" ++ show sz
| enum_t sig => sig.(enum_name)
| struct_t sig => sig.(struct_name)
| array_t sig => "array_" ++ show sig.(array_len) ++ "_" ++ type_id sig.(array_type)
end.
(** * Equalities **)
Ltac existT_dec :=
repeat match goal with
| [ H: existT _ _ ?x = existT _ _ ?y |- _ ] =>
apply Eqdep_dec.inj_pair2_eq_dec in H; [ | apply eq_dec ]
end.
Ltac simple_eq :=
first [ left; solve[eauto] | right; inversion 1; existT_dec; subst; solve[congruence] ].
Instance EqDec_type : EqDec type.
Proof.
econstructor.
fix IHtau 1;
destruct t1 as [ sz1 | en1 | fs1 | as1 ];
destruct t2 as [ sz2 | en2 | fs2 | as2 ]; cbn;
try simple_eq.
- destruct (eq_dec sz1 sz2); subst;
simple_eq.
- destruct en1 as [en1 es1 ebsz1 em1 ebp1];
destruct en2 as [en2 es2 ebsz2 em2 ebp2].
destruct (eq_dec en1 en2); subst; try simple_eq.
destruct (eq_dec es1 es2); subst; try simple_eq.
destruct (eq_dec ebsz1 ebsz2); subst; try simple_eq.
destruct (eq_dec em1 em2); subst; try simple_eq.
destruct (eq_dec ebp1 ebp2); subst; try simple_eq.
- destruct fs1 as [ nm1 f1 ];
destruct fs2 as [ nm2 f2 ]; cbn.
destruct (eq_dec nm1 nm2); subst; try simple_eq.
destruct (eq_dec (EqDec := _) f1 f2); subst; try simple_eq.
- destruct as1 as [ tau1 len1 ];
destruct as2 as [ tau2 len2 ]; cbn.
destruct (IHtau tau1 tau2); subst; try simple_eq.
destruct (eq_dec len1 len2); subst; try simple_eq.
Defined.
Instance EqDec_type_denote {tau: type} : EqDec (type_denote tau).
Proof.
econstructor.
revert tau; fix eq_dec_td 1;
destruct tau as [ ? | ? | [? fields] | ? ]; cbn.
- apply eq_dec.
- apply eq_dec.
- revert fields; fix eq_dec_struct 1.
destruct fields as [ | (nm, tau) fields ]; cbn.
+ apply eq_dec.
+ destruct t1 as [t1 tt1], t2 as [t2 tt2].
destruct (eq_dec_td _ t1 t2); subst; try simple_eq.
destruct (eq_dec_struct _ tt1 tt2); subst; try simple_eq.
- pose {| eq_dec := eq_dec_td (sig.(array_type)) |}.
apply eq_dec.
Defined.