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
|
val forall Num 'n, 'n >= 0. [:'n:] -> bit['n] effect pure zeros
function zeros n = replicate_bits(0b0, sizeof 'n)
val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> (bit['n], bit) effect pure lslc
function lslc (vec, shift) = {
assert(constraint('shift >= 1), "shift must be positive");
(bit['shift + 'n]) extended := vec : zeros(shift);
(bit['n]) result := extended[sizeof 'n - 1 .. 0];
(bit) c := extended[sizeof 'n];
return (result, c)
}
val forall Num 'n, Num 'shift, 'n >= 0. (bit['n], [:'shift:]) -> bit['n] effect pure lsl
function lsl (vec, shift) =
if shift == 0
then vec
else let (result, _) = lslc(vec, shift) in result
val unit -> unit effect pure main
function main () = {
print(if lsl(0b0110,1) == 0b1100 then "pass" else "fail");
print(if lsl(0b1111,2) == 0b1100 then "pass" else "fail");
print(if lsl(0x0F,4) == 0xF0 then "pass" else "fail");
let (result, c) = lslc(0xF000,2) in
print(if result == 0xC000 & c == bitone then "pass" else "fail")
}
|
