From bdfcb327ccf23982ae74549fc56ec3451c493ed5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 5 Feb 2018 17:49:11 +0000
Subject: Allow type variables to be introduced by global let bindings.

This was technically allowed previously but the rules for type
variable names in function types were too strict so it didn't work.

Also fixed a bug where Nexp_app constructors were never considered identical

and fixed a bug where top-level let bindings got annotated with the
wrong environment
---
 test/typecheck/pass/global_type_var.sail      | 21 +++++++++++++++++++++
 test/typecheck/pass/global_type_var/v1.expect |  6 ++++++
 test/typecheck/pass/global_type_var/v1.sail   | 23 +++++++++++++++++++++++
 test/typecheck/pass/global_type_var/v2.expect |  6 ++++++
 test/typecheck/pass/global_type_var/v2.sail   | 23 +++++++++++++++++++++++
 test/typecheck/pass/global_type_var/v3.expect |  5 +++++
 test/typecheck/pass/global_type_var/v3.sail   | 21 +++++++++++++++++++++
 7 files changed, 105 insertions(+)
 create mode 100644 test/typecheck/pass/global_type_var.sail
 create mode 100644 test/typecheck/pass/global_type_var/v1.expect
 create mode 100644 test/typecheck/pass/global_type_var/v1.sail
 create mode 100644 test/typecheck/pass/global_type_var/v2.expect
 create mode 100644 test/typecheck/pass/global_type_var/v2.sail
 create mode 100644 test/typecheck/pass/global_type_var/v3.expect
 create mode 100644 test/typecheck/pass/global_type_var/v3.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/global_type_var.sail b/test/typecheck/pass/global_type_var.sail
new file mode 100644
index 00000000..215907b4
--- /dev/null
+++ b/test/typecheck/pass/global_type_var.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
new file mode 100644
index 00000000..67355f59
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(32)
+
+Tried performing type coercion on 32
+Failed because atom<32> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v1.sail b/test/typecheck/pass/global_type_var/v1.sail
new file mode 100644
index 00000000..f2b2f89a
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(32)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
new file mode 100644
index 00000000..fb31fbed
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(64)
+
+Tried performing type coercion on 64
+Failed because atom<64> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.sail b/test/typecheck/pass/global_type_var/v2.sail
new file mode 100644
index 00000000..e8340978
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(64)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
new file mode 100644
index 00000000..a01f3eec
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23
+
+val test : forall 'size. atom('size) -> unit
+
+Kind identifier 'size is already bound
diff --git a/test/typecheck/pass/global_type_var/v3.sail b/test/typecheck/pass/global_type_var/v3.sail
new file mode 100644
index 00000000..274490ff
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : forall 'size. atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
-- 
cgit v1.2.3