Fix typo a mono_rewrites definition

- add tests for a couple of related rewrites
- accept same range of constants for sign extension in the rewrite as for
  the zero extension version (to make the test simpler)

2 files changed, 27 insertions, 0 deletions

diff --git a/test/mono/pass/rewrites b/test/mono/pass/rewrites
new file mode 100644
index 00000000..10272fed
--- /dev/null
+++ b/test/mono/pass/rewrites
@@ -0,0 +1 @@
+rewrites.sail -mono_rewrites
diff --git a/test/mono/rewrites.sail b/test/mono/rewrites.sail
new file mode 100644
index 00000000..b08af90f
--- /dev/null
+++ b/test/mono/rewrites.sail
@@ -0,0 +1,26 @@
+// Tests for -mono_rewrites
+
+default Order dec
+$include <prelude.sail>
+$include <mono_rewrites.sail>
+
+// The preconditions for this rewrite require a non-constant size somewhere, so
+// pull the example out into a separate function.
+val sign_ext_fun : forall 'z 'n, 'z >= 0 & 'n >= 4 + 'z. (bits(12), int('z), int('n)) -> bits('n)
+function sign_ext_fun(y, z, n) = {
+  sail_sign_extend(y[7..4] @ sail_zeros(z), n)
+}
+
+val run : unit -> unit effect {escape}
+
+function run() = {
+    let x : bits(12) = 0x123;
+    let y : bits(12) = 0x987;
+    let 'i = 7;
+    let 'j = 4;
+    let 'z = 8;
+    assert(sail_zero_extend(x[7..4] @ sail_zeros(8), 32) == 0x00000200);
+    assert(sign_ext_fun(x, z, 32) == 0x00000200);
+    assert(sail_zero_extend(y[7..4] @ sail_zeros(8), 32) == 0x00000800);
+    assert(sign_ext_fun(y, z, 32) == 0xfffff800);
+}