From 47c85cc3517bf5c7bbf3b29a718d3c2e4075fcfa Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jan 2020 21:55:16 -0800
Subject: [PATCH] fix: bug at `ParserDescr.ident`

---
 src/Init/Lean/Parser/Parser.lean | 119 +++++++++++++++++--------------
 tests/lean/run/macro.lean        |   8 +--
 2 files changed, 66 insertions(+), 61 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 5dc3cfccc1..5eda2377d4 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1398,6 +1398,69 @@ fun rbp ctx s => categoryParserFnExtension.getState ctx.env catName rbp ctx s
 def categoryParser {k} (catName : Name) (rbp : Nat) : Parser k :=
 { fn := fun _ => categoryParserFn catName rbp }
 
+-- Define `termParser` here because we need it for antiquotations
+@[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
+categoryParser `term rbp
+
+/- ============== -/
+/- Antiquotations -/
+/- ============== -/
+
+def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1
+
+/-- Fail if previous token is immediately followed by ':'. -/
+private def noImmediateColon {k : ParserKind} : Parser k :=
+{ fn := fun _ c s =>
+  let prev := s.stxStack.back;
+  if checkTailNoWs prev then
+    let input := c.input;
+    let i     := s.pos;
+    if input.atEnd i then s
+    else
+      let curr := input.get i;
+      if curr == ':' then
+        s.mkUnexpectedError "unexpected ':'"
+      else s
+  else s
+}
+
+private def pushNone {k : ParserKind} : Parser k :=
+{ fn := fun a c s => s.pushSyntax mkNullNode }
+
+/-
+  We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
+
+  TODO: we are making both cases look like syntax terms. Reason: the current expander expects a term.
+  We should remove this hack and modify the expander. This hack is bad since it relies on how we define `id` and `paren` in
+  the term parser at `Term.lean`. -/
+private def antiquotId {k} : Parser k         := node `Lean.Parser.Term.id (identNoAntiquot >> pushNone)
+private def antiquotNestedExpr {k} : Parser k := node `Lean.Parser.Term.paren ("(" >> node nullKind (termParser >> pushNone) >> ")")
+private def antiquotExpr {k} : Parser k       := antiquotId <|> antiquotNestedExpr
+
+/--
+  Define parser for `$e` (if anonymous == true) and `$e:name`. Both
+  forms can also be used with an appended `*` to turn them into an
+  antiquotation "splice". If `kind` is given, it will additionally be checked
+  when evaluating `match_syntax`. -/
+def mkAntiquot {k : ParserKind} (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser k :=
+let kind := (kind.getD Name.anonymous) ++ `antiquot;
+let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux ":" >> nonReservedSymbol name;
+-- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
+-- antiquotation kind via `noImmediateColon`
+let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
+node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*")
+
+/- ===================== -/
+/- End of Antiquotations -/
+/- ===================== -/
+
+def ident {k : ParserKind} : Parser k :=
+mkAntiquot "ident" `ident <|> identNoAntiquot
+
+-- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
+def rawIdent {k : ParserKind} : Parser k :=
+mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
+
 def categoryParserOfStackFn (offset : Nat) : ParserFn leading :=
 fun rbp ctx s =>
   let stack := s.stxStack;
@@ -1582,7 +1645,7 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
 | _, ParserDescr.num                                 => pure $ numLit
 | _, ParserDescr.str                                 => pure $ strLit
 | _, ParserDescr.char                                => pure $ charLit
-| _, ParserDescr.ident                               => pure $ identNoAntiquot -- Kha, do we need `ident` here?
+| _, ParserDescr.ident                               => pure $ ident
 | ParserKind.leading,
   ParserDescr.nonReservedSymbol tk includeIdent      => pure $ nonReservedSymbol tk includeIdent
 | _, ParserDescr.parser catName rbp =>
@@ -1851,60 +1914,6 @@ registerBuiltinParserAttribute `builtinTermParser `term
 @[init] def regTermParserAttribute : IO Unit :=
 registerBuiltinDynamicParserAttribute `termParser `term
 
-@[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
-categoryParser `term rbp
-
-def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1
-
-/-- Fail if previous token is immediately followed by ':'. -/
-private def noImmediateColon {k : ParserKind} : Parser k :=
-{ fn := fun _ c s =>
-  let prev := s.stxStack.back;
-  if checkTailNoWs prev then
-    let input := c.input;
-    let i     := s.pos;
-    if input.atEnd i then s
-    else
-      let curr := input.get i;
-      if curr == ':' then
-        s.mkUnexpectedError "unexpected ':'"
-      else s
-  else s
-}
-
-private def pushNone {k : ParserKind} : Parser k :=
-{ fn := fun a c s => s.pushSyntax mkNullNode }
-
-/-
-  We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
-
-  TODO: we are making both cases look like syntax terms. Reason: the current expander expects a term.
-  We should remove this hack and modify the expander. This hack is bad since it relies on how we define `id` and `paren` in
-  the term parser at `Term.lean`. -/
-private def antiquotId {k} : Parser k         := node `Lean.Parser.Term.id (identNoAntiquot >> pushNone)
-private def antiquotNestedExpr {k} : Parser k := node `Lean.Parser.Term.paren ("(" >> node nullKind (termParser >> pushNone) >> ")")
-private def antiquotExpr {k} : Parser k       := antiquotId <|> antiquotNestedExpr
-
-/--
-  Define parser for `$e` (if anonymous == true) and `$e:name`. Both
-  forms can also be used with an appended `*` to turn them into an
-  antiquotation "splice". If `kind` is given, it will additionally be checked
-  when evaluating `match_syntax`. -/
-def mkAntiquot {k : ParserKind} (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser k :=
-let kind := (kind.getD Name.anonymous) ++ `antiquot;
-let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux ":" >> nonReservedSymbol name;
--- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
--- antiquotation kind via `noImmediateColon`
-let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
-node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*")
-
-def ident {k : ParserKind} : Parser k :=
-mkAntiquot "ident" `ident <|> identNoAntiquot
-
--- `ident` and `rawIdent` produce the same syntax tree, so we reuse the antiquotation kind name
-def rawIdent {k : ParserKind} : Parser k :=
-mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
-
 def fieldIdxFn : BasicParserFn :=
 fun c s =>
   let iniPos := s.pos;
diff --git a/tests/lean/run/macro.lean b/tests/lean/run/macro.lean
index fc6cbe90d5..c6745d8402 100644
--- a/tests/lean/run/macro.lean
+++ b/tests/lean/run/macro.lean
@@ -19,19 +19,15 @@ syntax ident ":" term : index
 
 syntax "{" index " | " term "}" : term
 
--- #check { x : Nat → Nat | x > 0 }
-
--- set_option trace.Elab true
--- set_option syntaxMaxDepth 6
-
 macro_rules
 | `({$l ≤ $x:ident < $u | $p}) => `(setOf (fun $x:ident => $l ≤ $x:ident ∧ $x:ident < $u ∧ $p))
--- | `({$x:ident : $t | $p}) => `(setOf (fun ($x:ident : $t) => $p))
+| `({$x:ident : $t | $p}) => `(setOf (fun ($x:ident : $t) => $p))
 | `({$x ∈ $s | $p}) => `(setOf (fun $x => $x ∈ $s ∧ $p))
 | `({$x ≤ $e | $p}) => `(setOf (fun $x => $x ≤ $e ∧ $p))
 | `({$b      | $r}) => `(setOf (fun $b => $r))
 
 #check { 1 ≤ x < 10 | x ≠ 5 }
+#check { f : Nat → Nat | f 1  > 0 }
 
 syntax "⋃ " term ", " term : term