From c0ef2c3ea1ce7fc2c0b2ba970de27c3a1a5f6591 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 27 Jul 2017 17:41:37 +0100
Subject: Some more test cases

---
 test/typecheck/pass/add_real.sail                     |  5 +++++
 test/typecheck/pass/add_vec_exts_no_annot.sail        | 19 +++++++++++++++++++
 .../pass/add_vec_exts_no_annot_overload.sail          | 19 +++++++++++++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 test/typecheck/pass/add_real.sail
 create mode 100644 test/typecheck/pass/add_vec_exts_no_annot.sail
 create mode 100644 test/typecheck/pass/add_vec_exts_no_annot_overload.sail

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
+  ()
+}
-- 
cgit v1.2.3