From d256dbf5ec913615627b4d8cf6ff544759262cb4 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 19 May 2019 20:30:27 +0100
Subject: [PATCH] Add a test for non linear LHS

---
 tests/Main.idr                | 2 +-
 tests/ttimp/qtt003/QTTEq.yaff | 8 ++++++++
 tests/ttimp/qtt003/expected   | 3 +++
 tests/ttimp/qtt003/input      | 5 +++++
 tests/ttimp/qtt003/run        | 3 +++
 5 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/ttimp/qtt003/QTTEq.yaff
 create mode 100644 tests/ttimp/qtt003/expected
 create mode 100644 tests/ttimp/qtt003/input
 create mode 100755 tests/ttimp/qtt003/run

diff --git a/tests/Main.idr b/tests/Main.idr
index 5ca2c90..c910b1f 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -11,7 +11,7 @@ ttimpTests
        "eta001", "eta002",
        "nest001", "nest002",
        "perf001", "perf002", "perf003",
-       "qtt001", "qtt002"]
+       "qtt001", "qtt002", "qtt003"]
 
 chdir : String -> IO Bool
 chdir dir 
diff --git a/tests/ttimp/qtt003/QTTEq.yaff b/tests/ttimp/qtt003/QTTEq.yaff
new file mode 100644
index 0000000..ce32966
--- /dev/null
+++ b/tests/ttimp/qtt003/QTTEq.yaff
@@ -0,0 +1,8 @@
+data Eq : $a -> $b -> Type where
+     Refl : Eq $x $x
+
+okay : {p : $a -> $b} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) -> 
+       p x -> p y
+-- Should fail on the LHS, before even getting to the RHS, because
+-- after elaboration 'x' appears twice even though it is linearly bound.
+okay _ $x Refl $q = q
diff --git a/tests/ttimp/qtt003/expected b/tests/ttimp/qtt003/expected
new file mode 100644
index 0000000..31ffa52
--- /dev/null
+++ b/tests/ttimp/qtt003/expected
@@ -0,0 +1,3 @@
+Processing as TTImp
+QTTEq.yaff:8:1--9:1:There are 2 uses of linear name x
+Yaffle> Yaffle> Yaffle> Yaffle> Yaffle> Bye for now!
diff --git a/tests/ttimp/qtt003/input b/tests/ttimp/qtt003/input
new file mode 100644
index 0000000..2d115ca
--- /dev/null
+++ b/tests/ttimp/qtt003/input
@@ -0,0 +1,5 @@
+:t foo
+:t bar
+:t baz1
+:t baz2
+:q
diff --git a/tests/ttimp/qtt003/run b/tests/ttimp/qtt003/run
new file mode 100755
index 0000000..29975de
--- /dev/null
+++ b/tests/ttimp/qtt003/run
@@ -0,0 +1,3 @@
+$1 QTTEq.yaff < input
+
+rm -rf build