Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

14 files changed, 461 insertions, 0 deletions

diff --git a/test/typecheck/pass/existential_ast2.sail b/test/typecheck/pass/existential_ast2.sail
new file mode 100644
index 00000000..f15d1f57
--- /dev/null
+++ b/test/typecheck/pass/existential_ast2.sail
@@ -0,0 +1,28 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (nat, int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (int, int('d), bits(4))},
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  let a = unsigned(a);
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  let a = unsigned(a);
+
+  Some(Ctor2(a, x, c))
+}
diff --git a/test/typecheck/pass/existential_ast3.sail b/test/typecheck/pass/existential_ast3.sail
new file mode 100644
index 00000000..971b919c
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
new file mode 100644
index 00000000..a1975425
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -0,0 +1,20 @@
+Type error:
+[existential_ast3/v1.sail]:17:48-65
+17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |                                                ^---------------^
+   | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
+   | Coercion failed because:
+   | (int(33), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex57# bound here
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex58# bound here
+   | [existential_ast3/v1.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex62# bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v1.sail b/test/typecheck/pass/existential_ast3/v1.sail
new file mode 100644
index 00000000..05e13181
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v1.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
new file mode 100644
index 00000000..1ac6c87c
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -0,0 +1,20 @@
+Type error:
+[existential_ast3/v2.sail]:17:48-65
+17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |                                                ^---------------^
+   | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
+   | Coercion failed because:
+   | (int(31), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex57# bound here
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex58# bound here
+   | [existential_ast3/v2.sail]:17:48-65
+   | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+   |    |                                                ^---------------^
+   |    | 'ex62# bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v2.sail b/test/typecheck/pass/existential_ast3/v2.sail
new file mode 100644
index 00000000..77fc14c6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v2.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
new file mode 100644
index 00000000..05dcd0a1
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast3/v3.sail]:25:9-40
+25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
+   |         ^-----------------------------^
+   | Could not resolve quantifiers for Ctor
+   | * (datasize(64) & (0 <= 'ex78# & ('ex78# + 1) <= 64))
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v3.sail b/test/typecheck/pass/existential_ast3/v3.sail
new file mode 100644
index 00000000..53a55109
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v3.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(0b0 @ b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v4.expect b/test/typecheck/pass/existential_ast3/v4.expect
new file mode 100644
index 00000000..3de8b154
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v4.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v4.sail]:36:18-20
+36 |    if is_64 then 64 else 32;
+   |                  ^^
+   | Tried performing type coercion from int(64) to {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)} on 64
+   | Coercion failed because:
+   | int(64) is not a subtype of {('d : Int), (('is_64 & 'd == 63) | (not('is_64) & 'd == 32)). int('d)}
+   | [existential_ast3/v4.sail]:34:6-12
+   | 34 |  let 'is_64 = b == 0b0;
+   |    |      ^----^
+   |    | 'is_64 bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v4.sail b/test/typecheck/pass/existential_ast3/v4.sail
new file mode 100644
index 00000000..c2f03a86
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v4.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 63) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v5.expect b/test/typecheck/pass/existential_ast3/v5.expect
new file mode 100644
index 00000000..da686f6a
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v5.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v5.sail]:37:50-65
+37 |  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
+   |                                                  ^-------------^
+   | Tried performing type coercion from range(0, (2 ^ (1 + 5) - 1)) to range(0, ('datasize - 2)) on unsigned(bitvector_concat(b, a))
+   | Coercion failed because:
+   | range(0, (2 ^ (1 + 5) - 1)) is not a subtype of range(0, ('datasize - 2))
+   | [existential_ast3/v5.sail]:35:6-15
+   | 35 |  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+   |    |      ^-------^
+   |    | 'datasize bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v5.sail b/test/typecheck/pass/existential_ast3/v5.sail
new file mode 100644
index 00000000..5a34dd32
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v5.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize - 2) = if is_64 then unsigned(b @ a) else unsigned(a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast3/v6.expect b/test/typecheck/pass/existential_ast3/v6.expect
new file mode 100644
index 00000000..696f634a
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v6.expect
@@ -0,0 +1,12 @@
+Type error:
+[existential_ast3/v6.sail]:37:71-86
+37 |  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
+   |                                                                       ^-------------^
+   | Tried performing type coercion from range(0, (2 ^ (1 + 5) - 1)) to range(0, ('datasize - 1)) on unsigned(bitvector_concat(b, a))
+   | Coercion failed because:
+   | range(0, (2 ^ (1 + 5) - 1)) is not a subtype of range(0, ('datasize - 1))
+   | [existential_ast3/v6.sail]:35:6-15
+   | 35 |  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+   |    |      ^-------^
+   |    | 'datasize bound here
+   | 
diff --git a/test/typecheck/pass/existential_ast3/v6.sail b/test/typecheck/pass/existential_ast3/v6.sail
new file mode 100644
index 00000000..87496c3d
--- /dev/null
+++ b/test/typecheck/pass/existential_ast3/v6.sail
@@ -0,0 +1,50 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+union ast = {
+  Ctor : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))}
+}
+
+val decode : bits(16) -> option(ast)
+
+// Can have a constrained pair
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then (64, unsigned(b @ a)) else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
+
+// Or just lift the function body into the body if the if for flow typing
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  if b == 0b0 then {
+    Some(Ctor(64, unsigned(b @ a)))
+  } else {
+    Some(Ctor(32, unsigned(a)))
+  }
+}
+
+// Or use boolean constraint
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let 'is_64 = b == 0b0;
+  let 'datasize : {'d, ('is_64 & 'd == 64) | (not('is_64) & 'd == 32). int('d)} =
+    if is_64 then 64 else 32;
+  let n : range(0, 'datasize - 1) = if is_64 then unsigned(b @ a) else unsigned(b @ a);
+  None()
+}
+
+// Other variants
+
+function clause decode(a : bits(5) @ b : bits(1) @ 0b0000011111) = {
+  let (datasize, n) : {'d 'n, datasize('d) & 0 <= 'n < 'd. (int('d), int('n))} =
+    if b == 0b0 then {
+      let c = unsigned(b @ a);
+      (64, c)
+    } else (32, unsigned(a));
+  Some(Ctor(datasize, n))
+}
\ No newline at end of file