Merge branch 'mono-tweaks' into sail2

5 files changed, 45 insertions, 6 deletions

diff --git a/test/typecheck/pass/floor_pow2.sail b/test/typecheck/pass/floor_pow2.sail
new file mode 100644
index 00000000..fa8680cf
--- /dev/null
+++ b/test/typecheck/pass/floor_pow2.sail
@@ -0,0 +1,17 @@
+$include <arith.sail>
+
+val "pow2" : forall 'n, 'n >= 0. int('n) -> int(2 ^ 'n)
+
+val floor_pow2 : forall ('x : Int), 'x >= 0. int('x) -> int
+
+function floor_pow2 x = {
+    if x == 0 then {
+        return(0);
+    } else {
+        n : {'n, 'n >= 1. int('n)} = 1;
+        while x >= pow2(n) do {
+            n = n + 1
+        };
+        return(pow2(n - 1))
+    }
+}
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index 90166904..8854282d 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -1,13 +1,11 @@
 Type error:
-[reg_32_64/v2.sail]:21:18-22
+[reg_32_64/v2.sail]:21:2-15
 21 |  (*R)['d .. 0] = data
-   |                  ^--^
-   | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
-   | Coercion failed because:
-   | Mismatched argument types in subtype check
+   |  ^-----------^
+   | Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64)
    | This error was caused by:
    | [reg_32_64/v2.sail]:21:2-15
    | 21 |  (*R)['d .. 0] = data
    |    |  ^-----------^
-   |    | Mismatched argument types in subtype check
+   |    | Bounds check failed for l-expression: ((0 <= 0 & 0 <= 'd) & 'd < 64)
    | 
diff --git a/test/typecheck/pass/repeat_constraint.sail b/test/typecheck/pass/repeat_constraint.sail
new file mode 100644
index 00000000..6d63f2e8
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _not_prove(constraint(false));
+  } until (false);
+}
diff --git a/test/typecheck/pass/repeat_constraint/v1.expect b/test/typecheck/pass/repeat_constraint/v1.expect
new file mode 100644
index 00000000..9d561e11
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[repeat_constraint/v1.sail]:7:4-29
+7 |    _prove(constraint(false));
+  |    ^-----------------------^
+  | Cannot prove false
+  | 
diff --git a/test/typecheck/pass/repeat_constraint/v1.sail b/test/typecheck/pass/repeat_constraint/v1.sail
new file mode 100644
index 00000000..5dd2f513
--- /dev/null
+++ b/test/typecheck/pass/repeat_constraint/v1.sail
@@ -0,0 +1,9 @@
+$include <flow.sail>
+
+val main : unit -> unit
+
+function main() = {
+  repeat {
+    _prove(constraint(false));
+  } until (false);
+}