summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/mono/assign_range.sail32
-rw-r--r--test/mono/pass/assign_range1
2 files changed, 33 insertions, 0 deletions
diff --git a/test/mono/assign_range.sail b/test/mono/assign_range.sail
new file mode 100644
index 00000000..baf3ed43
--- /dev/null
+++ b/test/mono/assign_range.sail
@@ -0,0 +1,32 @@
+default Order dec
+$include <prelude.sail>
+
+val use : forall 'n, 'n >= 8. int('n) -> int
+
+function use(n) = {
+ let x : bits('n) = sail_sign_extend(0x12, n);
+ unsigned(x)
+}
+
+val test1 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test1(n) = {
+ size : {'m, 'm >= 8. int('m)} = n * 8;
+ use(size)
+}
+
+val test2 : forall 'n, 'n in {2,4}. int('n) -> int
+
+function test2(n) = {
+ size : range(8,32) = n * 8;
+ use(size)
+}
+
+val run : unit -> unit effect {escape}
+
+function run () = {
+ assert(test1(2) == 18);
+ assert(test1(4) == 18);
+ assert(test2(2) == 18);
+ assert(test2(4) == 18);
+}
diff --git a/test/mono/pass/assign_range b/test/mono/pass/assign_range
new file mode 100644
index 00000000..13642ef2
--- /dev/null
+++ b/test/mono/pass/assign_range
@@ -0,0 +1 @@
+assign_range.sail -auto_mono