Desugar pattern matching lambdas

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)

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",

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)

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!

tests/idris2/basic024/input

@@ -0,0 +1,3 @@
+addToNums nums
+lengths vects
+:q

tests/idris2/basic024/run

@@ -0,0 +1,3 @@
+$1 PatLam.idr < input
+
+rm -rf build