From a8da14a23cd8dfdd5fcc527b930ed553d376d18f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 1 Mar 2019 15:45:46 +0000
Subject: Make Sail more flexible with existentials in union types

Issues came up with Christophers translation of hand-written ARM into
Sail2 where we were being overly pedantic about the exact position of
existential quantifiers in constructors with multiple arguments. This
commit generalises unify_typ and type_coercion_unify to be more
flexible and support this. Should think at some point if unify_typ can
be generalised further.

This fix should fix the decode side of things, but may be some issues
with the executes that still need looking into when existentials and
multiple argument constructors are mixed.
---
 test/typecheck/pass/existential_ast.sail      | 54 +++++++++++++++++++++++++++
 test/typecheck/pass/existential_ast/v1.expect |  6 +++
 test/typecheck/pass/existential_ast/v1.sail   | 47 +++++++++++++++++++++++
 test/typecheck/pass/existential_ast/v2.expect |  6 +++
 test/typecheck/pass/existential_ast/v2.sail   | 54 +++++++++++++++++++++++++++
 test/typecheck/pass/existential_ast/v3.expect |  7 ++++
 test/typecheck/pass/existential_ast/v3.sail   | 54 +++++++++++++++++++++++++++
 7 files changed, 228 insertions(+)
 create mode 100644 test/typecheck/pass/existential_ast.sail
 create mode 100644 test/typecheck/pass/existential_ast/v1.expect
 create mode 100644 test/typecheck/pass/existential_ast/v1.sail
 create mode 100644 test/typecheck/pass/existential_ast/v2.expect
 create mode 100644 test/typecheck/pass/existential_ast/v2.sail
 create mode 100644 test/typecheck/pass/existential_ast/v3.expect
 create mode 100644 test/typecheck/pass/existential_ast/v3.sail

(limited to 'test')

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
-- 
cgit v1.2.3