Merge branch 'sail2' into rmem_interpreter

10 files changed, 55 insertions, 1 deletions

diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail
new file mode 100644
index 00000000..6d212e40
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect
new file mode 100644
index 00000000..71fd6f30
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24
+
+constraint Size('n) = 'm in {32, 64}
+
+No type variable 'm
diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail
new file mode 100644
index 00000000..4421ee77
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'm in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect
new file mode 100644
index 00000000..58a0f416
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
+
+Constraint synonym Siz is not defined
diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail
new file mode 100644
index 00000000..1d98e3e4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect
new file mode 100644
index 00000000..ab4526dc
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
+
+Constraint is badly formed, 'n has kind Type but should have kind Int
diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail
new file mode 100644
index 00000000..886acbe4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect
new file mode 100644
index 00000000..c8374baf
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15
+
+constraint Size('n) = 'n in {32, 64}
+
+Use -Xconstraint_synonyms to enable constraint synonyms
diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail
new file mode 100644
index 00000000..96bf5e82
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.sail
@@ -0,0 +1,6 @@
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8014f88a..c7e06dc7 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-Kind identifier 'size is already bound
+type variable 'size is already bound