From 48246c8e4a49ab7e9109e4eaba1ca567df3ab1f3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 24 May 2020 16:17:15 +0200
Subject: [PATCH] feat: parenthesizer: support antiquotations

---
 src/Init/Lean/Parser/Parser.lean              |  4 +-
 .../Lean/PrettyPrinter/Parenthesizer.lean     | 38 ++++++++++++-------
 2 files changed, 27 insertions(+), 15 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 81099d3c1d..2e7c64e0e1 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1423,8 +1423,8 @@ 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.
-private def antiquotNestedExpr : Parser := node `antiquotNestedExpr ("(" >> termParser >> ")")
-private def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
+def antiquotNestedExpr : Parser := node `antiquotNestedExpr ("(" >> termParser >> ")")
+def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
 /--
   Define parser for `$e` (if anonymous == true) and `$e:name`. Both
diff --git a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
index b92c1859bc..a4c6cc42f6 100644
--- a/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Init/Lean/PrettyPrinter/Parenthesizer.lean
@@ -76,6 +76,7 @@ the left. `visitArgs x` executes `x` on the right-most child of the current node
 prelude
 import Init.Lean.Parser
 import Init.Lean.Elab.Command
+import Init.Lean.Elab.Quotation
 import Init.Lean.Delaborator
 
 namespace Lean
@@ -195,6 +196,13 @@ instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM :=
 
 open Syntax.MonadTraverser
 
+/-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/
+def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
+stx ← getCur;
+when (stx.getArgs.size > 0) $
+  goDown (stx.getArgs.size - 1) *> x <* goUp;
+goLeft
+
 /--
   Call an appropriate `[parenthesizer]` depending on the `Parser` `Expr` `p`. After the call, the traverser position
   should be to the left of all nodes produced by `p`, or at the left-most child if there are no other nodes left. -/
@@ -225,6 +233,17 @@ instance monadQuotation : MonadQuotation ParenthesizerM := {
   withFreshMacroScope := fun α x => x,
 }
 
+def visitAntiquot : ParenthesizerM Unit := do
+stx ← getCur;
+if Elab.Term.Quotation.isAntiquot stx then visitArgs $ do
+  -- antiquot syntax is, simplified, `"$" "$"* antiquotExpr ":" (nonReservedSymbol name) "*"?`
+  goLeft; goLeft; goLeft; -- now on `antiquotExpr`
+  visit (mkConst `Lean.Parser.antiquotExpr);
+  -- set precedence; see special case in `currLbp`
+  modify (fun st => { st with firstLbp := Parser.appPrec, minLbp := Parser.appPrec })
+else
+  throw $ Exception.other $ "not an antiquotation"
+
 /-- Recurse using `visit`, and parenthesize the result using `mkParen` if necessary. -/
 def visitParenthesizable (mkParen : Syntax → Syntax) (rbp : Nat) : ParenthesizerM Unit := do
 stx ← getCur;
@@ -271,13 +290,6 @@ def visitToken (lbp : Nat) : ParenthesizerM Unit := do
 modify (fun st => { st with firstLbp := lbp });
 goLeft
 
-/-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/
-def visitArgs (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
-stx ← getCur;
-when (stx.getArgs.size > 0) $
-  goDown (stx.getArgs.size - 1) *> x <* goUp;
-goLeft
-
 def evalNat (e : Expr) : ParenthesizerM Nat := do
 e ← liftM $ whnf e;
 some n ← pure $ Meta.evalNat e
@@ -317,23 +329,23 @@ lbp ← evalNat p.appArg!;
 visitParenthesizable (fun stx => Unhygienic.run `(($stx))) lbp
 
 @[builtinParenthesizer tacticParser]
-def tacticParser.parenthesizer : Parenthesizer | p => do
+def tacticParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
 lbp ← evalNat p.appArg!;
 visitParenthesizable (fun stx => Unhygienic.run `(tactic|($stx))) lbp
 
 @[builtinParenthesizer levelParser]
-def levelParser.parenthesizer : Parenthesizer | p => do
+def levelParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
 lbp ← evalNat p.appArg!;
 visitParenthesizable (fun stx => Unhygienic.run `(level|($stx))) lbp
 
-@[builtinParenthesizer commandParser]
-def commandParser.parenthesizer : Parenthesizer | p => do
+@[builtinParenthesizer categoryParser]
+def categoryParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
 stx ← getCur;
 visit (mkConst stx.getKind)
 
 @[builtinParenthesizer withAntiquot]
 def withAntiquot.parenthesizer : Parenthesizer | p =>
-visit (p.getArg! 1)
+visitAntiquot <|> visit (p.getArg! 1)
 
 @[builtinParenthesizer try]
 def try.parenthesizer : Parenthesizer | p =>
@@ -374,7 +386,7 @@ visitArgs $ do {
     | panic! "trailingNode.parenthesizer: visited a trailing term without tokens?!";
   { mkParen := some mkParen, .. } ← read
     | panic! "trailingNode.parenthesizer called outside of visitParenthesizable call";
-  visitParenthesizable mkParen 0;
+  visitAntiquot <|> visitParenthesizable mkParen 0;
   modify $ fun st => { st with minLbp := Nat.min (st.minLbp.getD (lbp - 1)) (lbp - 1) }
 }