Support multiple let bindings

This sort of thing now works:

  test : Nat -> Nat
  test n = let foo = n
               S k = plus foo foo
              in k

The bindings must be aligned, and the keyword 'in' (indented however you
like within the 'test' block) terminates the list.

Pattern match alternatives are also supported, for quickly catching
failures:

  test2 : Nat -> Nat
  test2 n = let foo = n
                S k = plus foo foo
                    | Z => 42
              in k

Fixes #1362

src/Idris/ParseExpr.hs

@@ -780,23 +780,32 @@ TypeSig' ::=
 @
  -}
 let_ :: SyntaxInfo -> IdrisParser PTerm
-let_ syn = try (do reserved "let"; fc <- getFC; n <- name;
-                   ty <- option Placeholder (do lchar ':'; expr' syn)
-                   lchar '='
-                   v <- expr syn
-                   ts <- option [] (do lchar '|'
-                                       sepBy1 (do_alt syn) (lchar '|'))
+let_ syn = try (do reserved "let"
+                   ls <- indentedBlock (let_binding syn)
                    reserved "in";  sc <- expr syn
-                   case ts of
-                        [] -> return (PLet n ty v sc)
-                        alts -> return (PCase fc v ((PRef fc n, sc) : ts)))
-           <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
-                   symbol "="; v <- expr syn
-                   ts <- option [] (do lchar '|'
-                                       sepBy1 (do_alt syn) (lchar '|'))
-                   reserved "in"; sc <- expr syn
-                   return (PCase fc v ((pat, sc) : ts)))
+                   return (buildLets ls sc))
+--            <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
+--                    symbol "="; v <- expr syn
+--                    ts <- option [] (do lchar '|'
+--                                        sepBy1 (do_alt syn) (lchar '|'))
+--                    reserved "in"; sc <- expr syn
+--                    return (PCase fc v ((pat, sc) : ts)))
            <?> "let binding"
+  where buildLets [] sc = sc
+        buildLets ((fc,PRef _ n,ty,v,[]):ls) sc
+          = PLet n ty v (buildLets ls sc)
+        buildLets ((fc,pat,ty,v,alts):ls) sc
+          = PCase fc v ((pat, buildLets ls sc) : alts)
+
+let_binding syn = do fc <- getFC; 
+                     pat <- expr' (syn { inPattern = True })
+                     ty <- option Placeholder (do lchar ':'; expr' syn)
+                     lchar '='
+                     v <- expr syn
+                     ts <- option [] (do lchar '|'
+                                         sepBy1 (do_alt syn) (lchar '|'))
+                     return (fc,pat,ty,v,ts)
+                  
 
 {- | Parses a quote goal
 

src/Idris/ParseHelpers.hs

@@ -439,7 +439,8 @@ closeBlock = do ist <- get
                         Nothing : xs -> lchar '}' >> return xs <?> "end of block"
                         Just lvl : xs -> (do i   <- indent
                                              isParen <- lookAheadMatches (char ')')
-                                             if i >= lvl && not isParen
+                                             isIn <- lookAheadMatches (reserved "in")
+                                             if i >= lvl && not (isParen || isIn)
                                                 then fail "not end of block"
                                                 else return xs)
                                           <|> (do notOpenBraces
@@ -462,7 +463,8 @@ keepTerminator =  do lchar ';'; return ()
               <|> do c <- indent; l <- lastIndent
                      unless (c <= l) $ fail "not a terminator"
               <|> do isParen <- lookAheadMatches (oneOf ")}|")
-                     unless isParen $ fail "not a terminator"
+                     isIn <- lookAheadMatches (reserved "in")
+                     unless (isIn || isParen) $ fail "not a terminator"
               <|> lookAhead eof
 
 -- | Checks if application expression does not end