From 0dcdc2c1987e9f7b9a3abd3ac0749552b1468fcd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Jul 2019 10:06:30 -0700
Subject: [PATCH] feat(library/init/lean/parser/term): add support for "named"
 patterns `n@(x :: s)`

@kha, the implementation is a little bit hackish. It is whitespace
sensitive to avoid `f @g`, an application with argument `@g` to be
parsed as a named pattern.
Here are other approaches I have considered:

1- In the `namedPattern`, we add a guard that ensures the pattern
is *not* an identifier. Thus, `f @g` would not be considered a valid
`namedPattern`. Drawback: we would always try to parse it as a
namedPattern first, fail, and then try as an application.

2- Enforce whitespace before application arguments. Drawback: `f(a+b)`
would not be a valid application anymore.
---
 library/init/lean/parser/parser.lean | 19 ++++++++++++++-----
 library/init/lean/parser/term.lean   |  4 +++-
 2 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 09a5fcbbb3..8266087bda 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -925,6 +925,20 @@ def checkWsBefore {k : ParserKind} (errorMsg : String) : Parser k :=
 { info := epsilonInfo,
   fn   := fun _ => checkWsBeforeFn errorMsg }
 
+def checkTailNoWs (prev : Syntax) : Bool :=
+match prev.getTailInfo with
+| some info => info.trailing.stopPos == info.trailing.startPos
+| none      => false
+
+def checkNoWsBeforeFn (errorMsg : String) : BasicParserFn :=
+fun c s =>
+  let prev := s.stxStack.back;
+  if checkTailNoWs prev then s else s.mkError errorMsg
+
+def checkNoWsBefore {k : ParserKind} (errorMsg : String) : Parser k :=
+{ info := epsilonInfo,
+  fn   := fun _ => checkNoWsBeforeFn errorMsg }
+
 def insertNoWsToken (sym : String) (lbpNoWs : Option Nat) (tks : TokenTable) : ExceptT String Id TokenTable :=
 if sym == "" then throw "invalid empty symbol"
 else match tks.find sym, lbpNoWs with
@@ -939,11 +953,6 @@ def symbolNoWsInfo (sym : String) (lbpNoWs : Option Nat) : ParserInfo :=
 { updateTokens := insertNoWsToken sym lbpNoWs,
   firstTokens  := FirstTokens.tokens [ { val := sym, lbpNoWs := lbpNoWs } ] }
 
-def checkTailNoWs (left : Syntax) : Bool :=
-match left.getTailInfo with
-| some info => info.trailing.stopPos == info.trailing.startPos
-| none      => false
-
 @[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn trailing :=
 fun left c s =>
   if checkTailNoWs left then
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index f74b65279a..843f7e75cd 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -41,7 +41,9 @@ def infixL (sym : String) (lbp : Nat) : TrailingParser :=
 pushLeading >> symbol sym lbp >> termParser lbp
 
 /- Builting parsers -/
-@[builtinTermParser] def id := parser! ident >> optional (".{" >> sepBy1 levelParser ", " >> "}")
+def explicitUniv   := parser! ".{" >> sepBy1 levelParser ", " >> "}"
+def namedPattern := parser! checkNoWsBefore "no space before '@'" >> "@" >> termParser appPrec
+@[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
 @[builtinTermParser] def num : Parser := numLit
 @[builtinTermParser] def str : Parser := strLit
 @[builtinTermParser] def char : Parser := charLit