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
|
/* Not really *all* of the patterns, but enough to exercise the exhaustiveness
checker for Coq output */
default Order dec
$include <prelude.sail>
enum anenum = {Athing, Bthing, Cthing}
union aunion = {Dthing: unit, Ething: anenum, Fthing: (anenum,int)}
struct arecord = {elone: anenum, eltwo: aunion}
val f : (anenum, aunion, arecord, vector(5,dec,int), bits(4),list(anenum)) -> unit
function f(a,b,c,d,e,g) = {
match a {
Athing => (),
Bthing => (),
Cthing => ()
};
match a {
Athing => (),
_ => ()
};
match a {
Athing => (),
Bthing => ()
};
match b {
Dthing(()) => (),
Ething(Athing) => (),
Ething(Bthing) => (),
Ething(Cthing) => (),
Fthing(Athing,_) => (),
Fthing(Bthing,_) => (),
Fthing(Cthing,_) => ()
};
match b {
Dthing(()) => (),
Ething(Athing) => (),
Ething(Bthing) => (),
Ething(Cthing) => (),
Fthing(Athing,_) => (),
Fthing(Cthing,_) => ()
};
match b {
Dthing(()) => (),
Ething(Athing) => (),
Ething(Bthing) => (),
Ething(Cthing) => (),
Fthing(Athing,_) => (),
Fthing(_ as x,_) => ()
};
/* Um, no syntax for record patterns? */
/* Vector patterns must be bits? */
match e {
[_,_,_,bitzero] => (),
[_,_,_,_] => ()
};
match e {
[_,_,_,bitzero] => ()
};
match e {
[_,bitzero] @ (_ : bits(2)) => (),
_ => ()
};
match e {
[_,bitzero] @ (_ : bits(2)) => ()
};
match (a,b) {
(Athing,Ething(Bthing)) => (),
(_,Fthing(_,_)) => (),
(_,Dthing(())) => (),
(Bthing,_) => (),
(Cthing,_) => ()
};
match (a,b) {
(Athing,Ething(Bthing)) => (),
(Athing,Ething(_)) => (),
(_,Fthing(_,_)) => (),
(_,Dthing(())) => (),
(Bthing,_) => (),
(Cthing,_) => ()
};
match g {
[| |] => (),
[| Athing, Bthing |] => (),
_::_::_ => ()
};
match g {
[| |] => (),
[| Athing, _, Bthing |] => (),
_::_::_::_ => ()
};
match g {
[| |] => (),
[| Athing, _, Bthing |] => (),
_::_ => ()
}
}
|
