From 89c8314a0f00d15efd306ced64f7afba4afaacc5 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Wed, 3 Jul 2019 15:11:57 +0100
Subject: [PATCH] Desugar pattern matching lambdas

---
 src/Idris/Desugar.idr            |  6 ++++--
 tests/Main.idr                   |  2 +-
 tests/idris2/basic024/PatLam.idr | 15 +++++++++++++++
 tests/idris2/basic024/expected   |  5 +++++
 tests/idris2/basic024/input      |  3 +++
 tests/idris2/basic024/run        |  3 +++
 6 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/basic024/PatLam.idr
 create mode 100644 tests/idris2/basic024/expected
 create mode 100644 tests/idris2/basic024/input
 create mode 100755 tests/idris2/basic024/run

diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 68fd4b0..6f975d2 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -119,9 +119,11 @@ mutual
                                       !(desugar side (n :: ps) scope)
   desugar side ps (PLam fc rig p (PImplicit _) argTy scope) 
       = pure $ ILam fc rig p Nothing !(desugar side ps argTy) 
-                                      !(desugar side ps scope)
+                                     !(desugar side ps scope)
   desugar side ps (PLam fc rig p pat argTy scope)
-      = throw (GenericMsg fc "Pattern matching lambda not implemented")
+      = pure $ ILam fc rig p (Just (MN "lamc" 0)) !(desugar side ps argTy) $
+                 ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False)
+                     [!(desugarClause ps True (MkPatClause fc pat scope []))]
   desugar side ps (PLet fc rig (PRef _ n) nTy nVal scope [])
       = pure $ ILet fc rig n !(desugar side ps nTy) !(desugar side ps nVal) 
                              !(desugar side (n :: ps) scope)
diff --git a/tests/Main.idr b/tests/Main.idr
index 966040a..e085377 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -27,7 +27,7 @@ idrisTests
        "basic006", "basic007", "basic008", "basic009", "basic010",
        "basic011", "basic012", "basic013", "basic014", "basic015",
        "basic016", "basic017", "basic018", "basic019", "basic020",
-       "basic021", "basic022", "basic023",
+       "basic021", "basic022", "basic023", "basic024",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006",
diff --git a/tests/idris2/basic024/PatLam.idr b/tests/idris2/basic024/PatLam.idr
new file mode 100644
index 0000000..c3791d5
--- /dev/null
+++ b/tests/idris2/basic024/PatLam.idr
@@ -0,0 +1,15 @@
+import Data.Vect
+
+nums : List (Int, Int)
+nums = [(1, 2), (3, 4), (5, 6)]
+
+addToNums : List (Int, Int) -> List (Int, Int)
+addToNums = map (\ (x, y) => (x + 1, y + 1))
+
+vects : List (n ** Vect n Int)
+vects = [(_ ** [1,2,3]),
+         (_ ** [1,2,3,4]),
+         (_ ** [1,2,3,4,5])]
+
+lengths : List (n ** Vect n a) -> List Nat
+lengths = map (\ (len ** xs) => length xs)
diff --git a/tests/idris2/basic024/expected b/tests/idris2/basic024/expected
new file mode 100644
index 0000000..afa5977
--- /dev/null
+++ b/tests/idris2/basic024/expected
@@ -0,0 +1,5 @@
+1/1: Building PatLam (PatLam.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> [(2, 3), (4, 5), (6, 7)]
+Main> [S (S (S Z)), S (S (S (S Z))), S (S (S (S (S Z))))]
+Main> Bye for now!
diff --git a/tests/idris2/basic024/input b/tests/idris2/basic024/input
new file mode 100644
index 0000000..c3058cd
--- /dev/null
+++ b/tests/idris2/basic024/input
@@ -0,0 +1,3 @@
+addToNums nums
+lengths vects
+:q
diff --git a/tests/idris2/basic024/run b/tests/idris2/basic024/run
new file mode 100755
index 0000000..6c8639b
--- /dev/null
+++ b/tests/idris2/basic024/run
@@ -0,0 +1,3 @@
+$1 PatLam.idr < input
+
+rm -rf build