src/test/test5.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

register (bit) SAT

val forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm.
  (nat, [|'n|], [|'m|]) -> [|'n:'m|] effect { wreg } Clamp

function
  forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm. ([|'n:'m|])
  Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = {
    ([|'n:'m|]) result := 0;
    if (x<y) then {
      result := y;
      SAT := bitone;
    } else if (x > z) then {
      result := z;
      SAT := bitone;
    } else {
      result := x;
    };
    result;
  }