1 files changed, 31 insertions, 0 deletions
diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail
new file mode 100644
index 00000000..fdb9dc43
--- /dev/null
+++ b/test/ocaml/lsl/lsl.sail
@@ -0,0 +1,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")
+}