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
|
default Order dec
$include <prelude.sail>
$include <generic_equality.sail>
union ast = {
Foo : {'n, 'n in {16,32}. (int, int, int('n), bits('n))},
Bar : (int, int, {'n, 'n in {16,32}. (int('n), bits('n))}),
}
function test1(x : ast) -> int = {
match x {
Foo(a,b,_,d) => a+b+unsigned(d),
Bar(a,b,(_,d)) => a+b+unsigned(d),
}
}
function test2(x : ast) -> int = {
match x {
Foo(a,b,_,d) => a+b+unsigned(d),
Bar(a,b,y) => match y { (_, d) => a+b+unsigned(d) },
}
}
function test3(x : ast) -> int = {
match x {
Foo(a) => match a { (a,b,_,d) => a+b+unsigned(d) },
Bar(_) => 1,
}
}
function test4(i : int, v : bits(16)) -> ast =
let x : {'n, 'n in {16, 32}. (int, int, int('n), bits('n))} = (i,i,16,v) in
Foo(x)
union ast' = {
Foo' : {'n, 'n in {16,32}. (int, int, bits('n), int('n))},
}
function test4b(i : int, v : bits(16)) -> ast' =
let x : {'n, 'n in {16, 32}. (int, int, bits('n), int('n))} = (i,i,v,16) in
Foo'(x)
function test5() -> unit = {
let x = Foo(3,3,16,0x1234);
let y = test4(3,0x1234);
assert(x == y);
assert(test1(x) == test2(x));
}
val test6 : (int, {'n, 'n in {16, 32}. (int('n), bits('n))}) -> int
function test6(x, t) = {
let i : int = match t { (n,v) => unsigned(v) };
i + x
}
val test7 : (int, (int, {'n, 'n in {16, 32}. (int('n), bits('n))})) -> int
function test7(x, (_, t)) = {
let i : int = match t { (n,v) => unsigned(v) };
i + x
}
val test8 : (int, (int, {'n, 'n in {16, 32}. (int('n), bits('n))})) -> int
function test8(x, t) = {
let i : int = match t { (_, (n,v)) => unsigned(v) };
i + x
}
val test9 : (int, int) -> {'n, 'n > 0. (int('n), bits('n))}
function test9(n,v) = {
let n' = if n <= 0 then 1 else n;
(n', add_bits_int(sail_zeros(n'), v))
}
val test10 : (int, int) -> (int, {'n, 'n > 0. (int('n), bits('n))})
function test10(n,v) = {
let n' = if n <= 0 then 1 else n;
(v, (n', add_bits_int(sail_zeros(n'), v)))
}
|
