From 4581de785b6a3830f361f3c16e1d2ff18a0f20ea Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 29 Jun 2017 15:59:46 +0100
Subject: Additional tests for overloading and vector patterns

---
 test/typecheck/fail/vec_pat1.sail     | 17 +++++++++++++++++
 test/typecheck/pass/deinfix_plus.sail | 12 ++++++++++++
 test/typecheck/pass/vec_pat1.sail     | 17 +++++++++++++++++
 3 files changed, 46 insertions(+)
 create mode 100644 test/typecheck/fail/vec_pat1.sail
 create mode 100644 test/typecheck/pass/deinfix_plus.sail
 create mode 100644 test/typecheck/pass/vec_pat1.sail

diff --git a/test/typecheck/fail/vec_pat1.sail b/test/typecheck/fail/vec_pat1.sail
new file mode 100644
index 00000000..e10838f6
--- /dev/null
+++ b/test/typecheck/fail/vec_pat1.sail
@@ -0,0 +1,17 @@
+default Order inc
+
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a.
+  (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a>
+  effect pure vector_append_inc
+
+overload (deinfix +) [bv_add]
+overload vector_append [vector_append_inc]
+
+val (bit[3], bit[3]) -> bit[3] effect pure test
+
+function bit[3] test (((bit[0]) x : 0b11 : 0b0), z) =
+{
+  (x : 0b11) + z
+}
diff --git a/test/typecheck/pass/deinfix_plus.sail b/test/typecheck/pass/deinfix_plus.sail
new file mode 100644
index 00000000..c5a0f1ee
--- /dev/null
+++ b/test/typecheck/pass/deinfix_plus.sail
@@ -0,0 +1,12 @@
+default Order inc
+
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+  
+overload (deinfix +) [bv_add]
+
+val (bit[3], bit[3]) -> bit[3] effect pure test
+
+function bit[3] test (x, y) =
+{
+  x + y
+}
diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail
new file mode 100644
index 00000000..0a79d701
--- /dev/null
+++ b/test/typecheck/pass/vec_pat1.sail
@@ -0,0 +1,17 @@
+default Order inc
+
+val extern forall Num 'n. (bit['n], bit['n]) -> bit['n] effect pure bv_add = "bv_add_inc"
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Type 'a.
+  (vector<'n,'m,inc,'a>, vector<'o,'p,inc,'a>) -> vector<'n,'m + 'p,inc,'a>
+  effect pure vector_append_inc
+
+overload (deinfix +) [bv_add]
+overload vector_append [vector_append_inc]
+
+val (bit[3], bit[3]) -> bit[3] effect pure test
+
+function bit[3] test (((bit[1]) x : 0b1 : 0b0), z) =
+{
+  (x : 0b11) + z
+}
-- 
cgit v1.2.3