From 02ac3c9945d6e26348c178c76c1e244d219d8521 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 21 May 2020 17:22:30 +0100
Subject: [PATCH] Forgot to add some test files!

---
 tests/idris2/total007/expected    |  5 +++++
 tests/idris2/total007/partial.idr | 29 +++++++++++++++++++++++++++++
 tests/idris2/total007/run         |  3 +++
 3 files changed, 37 insertions(+)
 create mode 100644 tests/idris2/total007/expected
 create mode 100644 tests/idris2/total007/partial.idr
 create mode 100755 tests/idris2/total007/run

diff --git a/tests/idris2/total007/expected b/tests/idris2/total007/expected
new file mode 100644
index 000000000..9decfe9d3
--- /dev/null
+++ b/tests/idris2/total007/expected
@@ -0,0 +1,5 @@
+1/1: Building partial (partial.idr)
+partial.idr:5:1--7:1:foo is not covering. Missing cases:
+	foo Nothing
+partial.idr:13:1--15:1:qsortBad is not total:
+	possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad
diff --git a/tests/idris2/total007/partial.idr b/tests/idris2/total007/partial.idr
new file mode 100644
index 000000000..88ec048fc
--- /dev/null
+++ b/tests/idris2/total007/partial.idr
@@ -0,0 +1,29 @@
+import Data.List
+
+-- %default total
+
+total
+foo : Maybe a -> a
+foo (Just x) = x
+
+total
+bar : %World -> ()
+bar %MkWorld = ()
+
+total
+qsortBad : Ord a => List a -> List a
+qsortBad [] = []
+qsortBad (x :: xs)
+   = qsortBad (filter (< x) xs) ++ x :: qsortBad (filter (> x) xs)
+
+total
+qsort : Ord a => List a -> List a
+qsort [] = []
+qsort (x :: xs)
+   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
+         x :: qsort (assert_smaller (x :: xs) (filter (> x) xs))
+
+partial
+main : IO ()
+main = do let x = foo Nothing
+          printLn (the Int x)
diff --git a/tests/idris2/total007/run b/tests/idris2/total007/run
new file mode 100755
index 000000000..0c4efcfe7
--- /dev/null
+++ b/tests/idris2/total007/run
@@ -0,0 +1,3 @@
+$1 --no-banner partial.idr --check
+
+rm -rf build