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
|
default Order dec
$include <prelude.sail>
val ex_int : int -> {'n, true. int('n)}
function ex_int 'n = n
/* Decode -> int -> existential test */
val needssize : forall 'n, 'n >= 0. int('n) -> unit
function needssize(n) = {
let x : bits('n) = replicate_bits(0b0,n) in
()
}
val test : bits(2) -> unit
function test(x) = {
n : int = undefined;
match x {
0b00 => n = 1,
0b01 => n = 2,
0b10 => n = 4,
0b11 => n = 8
};
let 'n2 = ex_int(n) in {
assert(constraint('n2 >= 0));
needssize(n2)
}
}
val run : unit -> unit
function run () = {
test(0b00);
test(0b01);
test(0b10);
test(0b11);
}
|
