@@ -234,6 +234,14 @@ internalExpr syn =
234234 <|> app syn
235235 <?> "expression"
236236
237+{- | Parses the "impossible" keyword
238+@
239+Impossible ::= 'impossible'
240+@
241+-}
242+impossible :: IdrisParser PTerm
243+impossible = PImpossible <$ reserved "impossible"
244+
237245{- | Parses a case expression
238246@
239247CaseExpr ::=
@@ -250,13 +258,13 @@ caseExpr syn = do reserved "case"; fc <- getFC
250258{- | Parses a case in a case expression
251259@
252260CaseOption ::=
253− Expr '=>' Expr Terminator
261+ Expr (Impossible | '=>' Expr) Terminator
254262 ;
255263@
256264-}
257265caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
258266caseOption syn = do lhs <- expr (syn { inPattern = True })
259− r <- PImpossible <$ reserved "impossible" <|> do symbol "=>"; expr syn
267+ r <- impossible <|> symbol "=>" *> expr syn
260268 return (lhs, r)
261269 <?> "case option"
262270
@@ -732,8 +740,8 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu
732740{- | Parses a lambda expression
733741@
734742Lambda ::=
735− '\\' TypeOptDeclList '=>' Expr
736− | '\\' SimpleExprList '=>' Expr
743+ '\\' TypeOptDeclList LambdaTail
744+ | '\\' SimpleExprList LambdaTail
737745 ;
738746@
739747@
@@ -742,21 +750,22 @@ SimpleExprList ::=
742750 | SimpleExpr ',' SimpleExprList
743751 ;
744752@
753+@
754+LambdaTail ::=
755+ Impossible
756+ | '=>' Expr
757+@
745758-}
746759lambda :: SyntaxInfo -> IdrisParser PTerm
747760lambda syn = do lchar '\\' <?> "lambda expression"
748761 (do xt <- try $ tyOptDeclList syn
749762 fc <- getFC
750− sc <- PImpossible <$ reserved "impossible" <|> do
751− symbol "=>"
752− expr syn
763+ sc <- lambdaTail
753764 return (bindList (PLam fc) xt sc)) <|> do
754765 ps <- sepBy (do fc <- getFC
755766 e <- simpleExpr (syn { inPattern = True })
756767 return (fc, e)) (lchar ',')
757− sc <- PImpossible <$ reserved "impossible" <|> do
758− symbol "=>"
759− expr syn
768+ sc <- lambdaTail
760769 return (pmList (zip [0..] ps) sc)
761770 <?> "lambda expression"
762771 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
@@ -765,6 +774,8 @@ lambda syn = do lchar '\\' <?> "lambda expression"
765774 = PLam fc (sMN i "lamp") Placeholder
766775 (PCase fc (PRef fc (sMN i "lamp"))
767776 [(x, pmList xs sc)])
777+ lambdaTail :: IdrisParser PTerm
778+ lambdaTail = impossible <|> symbol "=>" *> expr syn
768779
769780{- | Parses a term rewrite expression
770781@