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
|
default Order dec
$include <prelude.sail>
$[no_enum_number_conversions]
enum E = A | B | C
register r_A : E
register r_B : E
register r_C : E
function match_enum(x : E) -> bit = {
match x {
A => bitone,
B => bitone,
C => bitzero,
}
}
function match_option(x : option(bit)) -> bit = {
match x {
Some(x) => x,
None() => bitzero,
}
}
function match_pair_pat((x, y) : (int, int)) -> int = {
match (x, y) {
(a, b) => a + b,
}
}
function match_pair(x : (int, int)) -> int = {
match x {
(a, b) => a + b,
}
}
function match_reg(x : E) -> E = {
match x {
A => r_A,
B => r_B,
C => r_C,
}
}
function match_let (x : E, y : int) -> int = {
match x {
A =>
let x = y + y in
let z = y + y + undefined_int() in
z + x,
B => 42,
C => 23
}
}
function match_read(x : E) -> unit = {
r_A = match x {
A => r_A,
B => r_B,
C => r_C,
}
}
function const16() -> (bitvector(16), bool) = {
(0xFFFF, true)
}
function const32() -> (bitvector(32), bool) = {
(0xEEEE_EEEE, false)
}
val match_width : forall 'n, 'n >= 0. bitvector('n) -> bitvector(2 * 'n)
function match_width x = {
let (foo, _) : (bitvector('n), bool) = match 'n {
16 => const16(),
32 => const32(),
n => (sail_zeros(n), false)
} in
bitvector_concat(foo, foo)
}
val match_option_bitvec : (option(bitvector(16))) -> int
function match_option_bitvec (x : option(bitvector(16))) = {
match x {
Some(0xFFFF) => 1,
_ => 0
}
}
|
