From 86d2b82c29497767b4b5377567ea2341faf2bd70 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 18 Feb 2020 15:32:44 +0100
Subject: [PATCH] refactor: get rid of antiquotExpr hack

---
 src/Init/Lean/Elab/Quotation.lean | 13 ++++++-------
 src/Init/Lean/Elab/Syntax.lean    |  6 +++---
 src/Init/Lean/Parser/Parser.lean  | 12 +++---------
 3 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 926d47e8a2..26d0d9491d 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -79,7 +79,11 @@ if isAntiquot stx then
 else stx
 
 def getAntiquotTerm (stx : Syntax) : Syntax :=
-stx.getArg 2
+let e := stx.getArg 2;
+if e.isIdent then mkTermIdFromIdent e
+else
+  -- `e` is from `"(" >> termParser >> ")"`
+  e.getArg 1
 
 def antiquotKind? : Syntax → Option SyntaxNodeKind
 | Syntax.node (Name.str k "antiquot" _) args =>
@@ -226,9 +230,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
     -- else
     --   let e := stx; ...
     let kind := if k == Name.anonymous then none else k;
-    let anti := match_syntax getAntiquotTerm quoted with
-    | `(($e)) => e
-    | anti    => anti;
+    let anti := getAntiquotTerm quoted;
     -- Splices should only appear inside a nullKind node, see next case
     if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice"
     else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn :=  fun rhs => `(let $anti := discr; $rhs) }
@@ -292,9 +294,6 @@ private partial def getPatternVarsAux : Syntax → List Syntax
 | stx@(Syntax.node k args) =>
   if isAntiquot stx && !isEscapedAntiquot stx then
     let anti := getAntiquotTerm stx;
-    let anti := match_syntax anti with
-    | `(($e)) => e
-    | _       => anti;
     if anti.isOfKind `Lean.Parser.Term.id then [anti]
     else []
   else
diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index c27f826301..026b8f2b5b 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -259,7 +259,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
 | stx => match_syntax stx with
 | `($id:ident) =>
   if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
-    Syntax.node `antiquot #[mkAtom "$", mkNullNode, Unhygienic.run `($id:ident), mkNullNode, mkNullNode]
+    Syntax.node `antiquot #[mkAtom "$", mkNullNode, id, mkNullNode, mkNullNode]
   else
     stx
 | _ => match stx with
@@ -290,7 +290,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.identPrec then
   let item := stx.getArg 0;
-  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode]
+  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
 else if k == `Lean.Parser.Command.quotedSymbolPrec then
   pure $ (stx.getArg 0).getArg 1
 else if k == `Lean.Parser.Command.strLitPrec then
@@ -346,7 +346,7 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
 let k := stx.getKind;
 if k == `Lean.Parser.Command.macroArgSimple then
   let item := stx.getArg 0;
-  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode]
+  pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
 else if k == `Lean.Parser.Command.strLitPrec then
   strLitPrecToPattern stx
 else
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 238239345f..b16b4ecb6c 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1418,15 +1418,9 @@ def setExpected (expected : List String) (p : Parser) : Parser :=
 def pushNone : Parser :=
 { fn := fun 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 : Parser         := node `Lean.Parser.Term.id (identNoAntiquot >> pushNone)
-private def antiquotNestedExpr : Parser := node `Lean.Parser.Term.paren ("(" >> node nullKind (termParser >> pushNone) >> ")")
-private def antiquotExpr : Parser       := antiquotId <|> antiquotNestedExpr
+-- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
+private def antiquotNestedExpr : Parser := node `antiquotNestedExpr ("(" >> termParser >> ")")
+private def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
 /--
   Define parser for `$e` (if anonymous == true) and `$e:name`. Both