From 6c007fc046cedebbeb05f6a1720d7756fa552396 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 27 Jun 2020 15:47:38 +0100
Subject: [PATCH] Use full names for constructors in case split

Fixes #184
---
 src/TTImp/Interactive/CaseSplit.idr |  5 ++++-
 tests/Main.idr                      |  2 +-
 tests/idris2/reg024/expected        | 10 ++++++++++
 tests/idris2/reg024/input           |  1 +
 tests/idris2/reg024/run             |  3 +++
 tests/idris2/reg024/split.idr       | 13 +++++++++++++
 6 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/reg024/expected
 create mode 100644 tests/idris2/reg024/input
 create mode 100755 tests/idris2/reg024/run
 create mode 100644 tests/idris2/reg024/split.idr

diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr
index d227667cf..2d55368ff 100644
--- a/src/TTImp/Interactive/CaseSplit.idr
+++ b/src/TTImp/Interactive/CaseSplit.idr
@@ -84,6 +84,8 @@ getDefining tm
            Ref _ _ fn => Just fn
            _ => Nothing
 
+-- For the name on the lhs, return the function name being defined, the
+-- type name, and the possible constructors.
 findCons : {auto c : Ref Ctxt Defs} ->
            Name -> Term [] -> Core (SplitResult (Name, Name, List Name))
 findCons n lhs
@@ -102,7 +104,8 @@ findCons n lhs
                                             (CantSplitThis n
                                                ("Not a type constructor " ++
                                                   show res)))
-                             pure (OK (fn, tyn, cons))
+                             pure (OK (fn, !(toFullNames tyn),
+                                           !(traverse toFullNames cons)))
 
 findAllVars : Term vars -> List Name
 findAllVars (Bind _ x (PVar c p ty) sc)
diff --git a/tests/Main.idr b/tests/Main.idr
index 407993ed1..ac4404725 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -97,7 +97,7 @@ idrisTests
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
-       "reg022", "reg023",
+       "reg022", "reg023", "reg024",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",
diff --git a/tests/idris2/reg024/expected b/tests/idris2/reg024/expected
new file mode 100644
index 000000000..2536fd253
--- /dev/null
+++ b/tests/idris2/reg024/expected
@@ -0,0 +1,10 @@
+1/1: Building split (split.idr)
+Main> notLtz BLT_ZO impossible
+notLtz BLT_ZE impossible
+notLtz (BLT_OO x) impossible
+notLtz (BLT_OE x) impossible
+notLtz BLT_OE_Eq impossible
+notLtz (BLT_EO x) impossible
+notLtz (BLT_EE x) impossible
+Main> 
+Bye for now!
diff --git a/tests/idris2/reg024/input b/tests/idris2/reg024/input
new file mode 100644
index 000000000..01d18ad8e
--- /dev/null
+++ b/tests/idris2/reg024/input
@@ -0,0 +1 @@
+:cs 13 8 x
diff --git a/tests/idris2/reg024/run b/tests/idris2/reg024/run
new file mode 100755
index 000000000..4d9fc04bc
--- /dev/null
+++ b/tests/idris2/reg024/run
@@ -0,0 +1,3 @@
+$1 --no-banner split.idr < input
+
+rm -rf build
diff --git a/tests/idris2/reg024/split.idr b/tests/idris2/reg024/split.idr
new file mode 100644
index 000000000..680070624
--- /dev/null
+++ b/tests/idris2/reg024/split.idr
@@ -0,0 +1,13 @@
+data BNat = BZ | O BNat | E BNat
+
+data BLT : BNat -> BNat -> Type where
+  BLT_ZO : BLT BZ (O bn)
+  BLT_ZE : BLT BZ (E bn)
+  BLT_OO : BLT bn bm -> BLT (O bn) (O bm)
+  BLT_OE : BLT bn bm -> BLT (O bn) (E bm)
+  BLT_OE_Eq : BLT (O bn) (E bn)
+  BLT_EO : BLT bn bm -> BLT (E bn) (O bm)
+  BLT_EE : BLT bn bm -> BLT (E bn) (E bm)
+
+notLtz : BLT bn BZ -> Void
+notLtz x = ?notLtz_rhs