on master help sign in
Parse lambdas with impossible
58875b2Melvar Chen
src/Idris/ParseExpr.hs+6−4
@@ -747,14 +747,16 @@ lambda :: SyntaxInfo -> IdrisParser PTerm
747lambda syn = do lchar '\\' <?> "lambda expression"
747lambda syn = do lchar '\\' <?> "lambda expression"
748 (do xt <- try $ tyOptDeclList syn
748 (do xt <- try $ tyOptDeclList syn
749 fc <- getFC
749 fc <- getFC
750− symbol "=>"
750+ sc <- PImpossible <$ reserved "impossible" <|> do
751+ symbol "=>"
751− sc <- expr syn
752+ expr syn
752 return (bindList (PLam fc) xt sc)) <|> do
753 return (bindList (PLam fc) xt sc)) <|> do
753 ps <- sepBy (do fc <- getFC
754 ps <- sepBy (do fc <- getFC
754 e <- simpleExpr (syn { inPattern = True })
755 e <- simpleExpr (syn { inPattern = True })
755 return (fc, e)) (lchar ',')
756 return (fc, e)) (lchar ',')
756− symbol "=>"
757+ sc <- PImpossible <$ reserved "impossible" <|> do
758+ symbol "=>"
757− sc <- expr syn
759+ expr syn
758 return (pmList (zip [0..] ps) sc)
760 return (pmList (zip [0..] ps) sc)
759 <?> "lambda expression"
761 <?> "lambda expression"
760 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
762 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm