Always accept antiquotations

RELEASES.md

@@ -105,6 +105,9 @@ ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
 * (Experimental) New `checkpoint <tactic-seq>` tactic for big interactive proofs.
 
 * Rename tactic `nativeDecide` => `native_decide`.
+* Antiquotations are now accepted in any syntax. The `incQuotDepth` `syntax` parser is therefore obsolete and has been removed.
+
+* Renamed tactic `nativeDecide` => `native_decide`.
 
 * "Cleanup" local context before elaborating a `match` alternative right-hand-side. Examples:
 ```lean

doc/macro_overview.md

@@ -158,7 +158,7 @@ Output:
 [Elab.definition.body] binderterm.quot : Lean.ParserDescr :=
 Lean.ParserDescr.node `Lean.Parser.Term.quot 1024
   (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "`(binderterm|")
-    (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `incQuotDepth (Lean.ParserDescr.cat `binderterm 0))
+    (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `binderterm 0)
       (Lean.ParserDescr.symbol ")")))
 -/
 ```

src/Lean/Elab/Syntax.lean

@@ -226,7 +226,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
         Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec)
           (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
             (Lean.ParserDescr.binary `andthen
-              (Lean.ParserDescr.unary `incQuotDepth (Lean.ParserDescr.cat $(quote catName) 0))
+              (Lean.ParserDescr.cat $(quote catName) 0)
               (Lean.ParserDescr.symbol ")"))))
     elabCommand cmd
 

src/Lean/Parser.lean

@@ -41,7 +41,6 @@ builtin_initialize
   register_parser_alias interpolatedStr
   register_parser_alias orelse
   register_parser_alias andthen
-  register_parser_alias incQuotDepth
 
   registerAlias "notFollowedBy" (notFollowedBy · "element")
   Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer

src/Lean/Parser/Basic.lean

@@ -129,6 +129,7 @@ structure ParserModuleContext where
 structure ParserContext extends InputContext, ParserModuleContext where
   prec               : Nat
   tokens             : TokenTable
+  -- used for bootstrapping only
   quotDepth          : Nat := 0
   suppressInsideQuot : Bool := false
   savedPos?          : Option String.Pos := none
@@ -444,25 +445,7 @@ def setLhsPrecFn (prec : Nat) : ParserFn := fun c s =>
   fn   := setLhsPrecFn prec
 }
 
-def checkInsideQuotFn : ParserFn := fun c s =>
-  if c.quotDepth > 0 && !c.suppressInsideQuot then s
-  else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
-
-@[inline] def checkInsideQuot : Parser := {
-  info := epsilonInfo,
-  fn   := checkInsideQuotFn
-}
-
-def checkOutsideQuotFn : ParserFn := fun c s =>
-  if !c.quotDepth == 0 || c.suppressInsideQuot then s
-  else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
-
-@[inline] def checkOutsideQuot : Parser := {
-  info := epsilonInfo,
-  fn   := checkOutsideQuotFn
-}
-
-def addQuotDepthFn (i : Int) (p : ParserFn) : ParserFn := fun c s =>
+private def addQuotDepthFn (i : Int) (p : ParserFn) : ParserFn := fun c s =>
   p { c with quotDepth := c.quotDepth + i |>.toNat } s
 
 @[inline] def incQuotDepth (p : Parser) : Parser := {
@@ -1691,9 +1674,8 @@ def pushNone : Parser :=
 def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
 def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
-@[inline] def tokenWithAntiquotFn (p : ParserFn) : ParserFn := fun c s => Id.run <| do
-  let s := p c s
-  if s.hasError || c.quotDepth == 0 then
+def tokenAntiquotFn : ParserFn := fun c s => Id.run do
+  if s.hasError then
     return s
   let iniSz  := s.stackSize
   let iniPos := s.pos
@@ -1703,7 +1685,13 @@ def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
   s.mkNode (`token_antiquot) (iniSz - 1)
 
 @[inline] def tokenWithAntiquot (p : Parser) : Parser where
-  fn   := tokenWithAntiquotFn p.fn
+  fn c s :=
+    let s := p.fn c s
+    -- fast check that is false in most cases
+    if c.input.get s.pos == '%' then
+      tokenAntiquotFn c s
+    else
+      s
   info := p.info
 
 @[inline] def symbol (sym : String) : Parser :=
@@ -1736,16 +1724,12 @@ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true
     checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
     nameP
 
-def tryAnti (c : ParserContext) (s : ParserState) : Bool := Id.run <| do
-  if c.quotDepth == 0 then
-    return false
-  let (s, stx) := peekToken c s
-  match stx with
-  | Except.ok stx@(Syntax.atom _ sym) => sym == "$"
-  | _                                 => false
-
 @[inline] def withAntiquotFn (antiquotP p : ParserFn) : ParserFn := fun c s =>
-  if tryAnti c s then orelseFn antiquotP p c s else p c s
+  -- fast check that is false in most cases
+  if c.input.get s.pos == '$' then
+    orelseFn antiquotP p c s
+  else
+    p c s
 
 /-- Optimized version of `mkAntiquot ... <|> p`. -/
 @[inline] def withAntiquot (antiquotP p : Parser) : Parser := {
@@ -1765,10 +1749,7 @@ def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
     checkNoWsBefore "no space before spliced term" >> symbol "[" >> node nullKind p >> symbol "]" >>
     suffix
 
-@[inline] def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (p suffix : ParserFn) : ParserFn := fun c s => Id.run <| do
-  let s := p c s
-  if s.hasError || c.quotDepth == 0 || !s.stxStack.back.isAntiquot then
-    return s
+private def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (suffix : ParserFn) : ParserFn := fun c s => Id.run do
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let s      := suffix c s
@@ -1777,10 +1758,15 @@ def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
   s.mkNode (kind ++ `antiquot_suffix_splice) (s.stxStack.size - 2)
 
 /-- Parse `suffix` after an antiquotation, e.g. `$x,*`, and put both into a new node. -/
-@[inline] def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser := {
-  info := andthenInfo p.info suffix.info,
-  fn   := withAntiquotSuffixSpliceFn kind p.fn suffix.fn
-}
+@[inline] def withAntiquotSuffixSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser where
+  info := andthenInfo p.info suffix.info
+  fn c s :=
+    let s := p.fn c s
+    -- fast check that is false in most cases
+    if !s.hasError && s.stxStack.back.isAntiquot then
+      withAntiquotSuffixSpliceFn kind suffix.fn c s
+    else
+      s
 
 def withAntiquotSpliceAndSuffix (kind : SyntaxNodeKind) (p suffix : Parser) :=
   -- prevent `p`'s info from being collected twice

src/Lean/Parser/Extension.lean

@@ -547,31 +547,6 @@ builtin_initialize registerBuiltinDynamicParserAttribute `commandParser `command
 @[inline] def commandParser (rbp : Nat := 0) : Parser :=
   categoryParser `command rbp
 
-def notFollowedByCategoryTokenFn (catName : Name) : ParserFn := fun ctx s =>
-  let categories := (parserExtension.getState ctx.env).categories
-  match getCategory categories catName with
-  | none => s.mkUnexpectedError s!"unknown parser category '{catName}'"
-  | some cat =>
-    let (s, stx) := peekToken ctx s
-    match stx with
-    | Except.ok (Syntax.atom _ sym) =>
-      if ctx.quotDepth > 0 && sym == "$" then s
-      else match cat.tables.leadingTable.find? (Name.mkSimple sym) with
-      | some _ => s.mkUnexpectedError (toString catName)
-      | _      => s
-    | Except.ok _    => s
-    | Except.error _ => s
-
-@[inline] def notFollowedByCategoryToken (catName : Name) : Parser := {
-  fn := notFollowedByCategoryTokenFn catName
-}
-
-abbrev notFollowedByCommandToken : Parser :=
-  notFollowedByCategoryToken `command
-
-abbrev notFollowedByTermToken : Parser :=
-  notFollowedByCategoryToken `term
-
 private def withNamespaces (ids : Array Name) (p : ParserFn) (addOpenSimple : Bool) : ParserFn := fun c s =>
   let c := ids.foldl (init := c) fun c id =>
     match ResolveName.resolveNamespace? c.env c.currNamespace c.openDecls id with

src/Lean/PrettyPrinter/Formatter.lean

@@ -478,10 +478,7 @@ def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :
 @[combinatorFormatter Lean.Parser.checkLineEq] def checkLineEq.formatter : Formatter := pure ()
 
 @[combinatorFormatter Lean.Parser.eoi] def eoi.formatter : Formatter := pure ()
-@[combinatorFormatter Lean.Parser.notFollowedByCategoryToken] def notFollowedByCategoryToken.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
-@[combinatorFormatter Lean.Parser.checkInsideQuot] def checkInsideQuot.formatter : Formatter := pure ()
-@[combinatorFormatter Lean.Parser.checkOutsideQuot] def checkOutsideQuot.formatter : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.skip] def skip.formatter : Formatter := pure ()
 
 @[combinatorFormatter Lean.Parser.pushNone] def pushNone.formatter : Formatter := goLeft

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -484,10 +484,7 @@ def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Par
 @[combinatorParenthesizer Lean.Parser.checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkLineEq] def checkLineEq.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.eoi] def eoi.parenthesizer : Parenthesizer := pure ()
-@[combinatorParenthesizer Lean.Parser.notFollowedByCategoryToken] def notFollowedByCategoryToken.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
-@[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure ()
-@[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.skip] def skip.parenthesizer : Parenthesizer := pure ()
 
 @[combinatorParenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft