Additional tests for overloading and vector patterns

3 files changed, 46 insertions, 0 deletions

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
+}