Some more test cases

3 files changed, 43 insertions, 0 deletions

diff --git a/test/typecheck/pass/add_real.sail b/test/typecheck/pass/add_real.sail
new file mode 100644
index 00000000..38a9cff3
--- /dev/null
+++ b/test/typecheck/pass/add_real.sail
@@ -0,0 +1,5 @@
+val (real, real) -> real effect pure add_real
+
+overload (deinfix +) [add_real]
+
+let (real) r = 2.2 + 0.2
diff --git a/test/typecheck/pass/add_vec_exts_no_annot.sail b/test/typecheck/pass/add_vec_exts_no_annot.sail
new file mode 100644
index 00000000..54aa2d40
--- /dev/null
+++ b/test/typecheck/pass/add_vec_exts_no_annot.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTS [exts]
+
+val forall Nat 'n, Nat 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val (bit[32], bit[32]) -> unit effect pure test
+
+function test (x, y) =
+{
+  let (bit[64]) z = add_vec(exts(x), exts(y)) in
+  ()
+}
diff --git a/test/typecheck/pass/add_vec_exts_no_annot_overload.sail b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail
new file mode 100644
index 00000000..01e3bf7c
--- /dev/null
+++ b/test/typecheck/pass/add_vec_exts_no_annot_overload.sail
@@ -0,0 +1,19 @@
+default Order dec
+
+val forall Nat 'n, Nat 'm, Nat 'o, Nat 'p, Order 'ord.
+    vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTS [exts]
+
+val forall Nat 'n, Nat 'o, Order 'ord.
+    (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val (bit[32], bit[32]) -> unit effect pure test
+
+function test (x, y) =
+{
+  let (bit[64]) z = EXTS(x) + EXTS(y) in
+  ()
+}