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

7 files changed, 228 insertions, 0 deletions

diff --git a/test/typecheck/pass/existential_ast.sail b/test/typecheck/pass/existential_ast.sail
new file mode 100644
index 00000000..37cf2378
--- /dev/null
+++ b/test/typecheck/pass/existential_ast.sail
@@ -0,0 +1,54 @@
+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). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, 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;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect
new file mode 100644
index 00000000..f743abb6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v1.sail]:46:7-21
+46 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v1.sail b/test/typecheck/pass/existential_ast/v1.sail
new file mode 100644
index 00000000..935313f7
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.sail
@@ -0,0 +1,47 @@
+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). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, 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;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b01);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect
new file mode 100644
index 00000000..20738cd8
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v2.sail]:39:7-21
+39 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v2.sail b/test/typecheck/pass/existential_ast/v2.sail
new file mode 100644
index 00000000..fd272dbb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 30)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, 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;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
new file mode 100644
index 00000000..1b6239bb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast/v3.sail]:26:7-21
+26 |  Some(Ctor1(a, x, c))
+   |       ^------------^
+   | Could not resolve quantifiers for Ctor1
+   | * datasize('ex59#)
+   | 
diff --git a/test/typecheck/pass/existential_ast/v3.sail b/test/typecheck/pass/existential_ast/v3.sail
new file mode 100644
index 00000000..1bacbf80
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.sail
@@ -0,0 +1,54 @@
+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). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, 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;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|16, 32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file