From b3ba78aade428d5e8e9f5fa69882486774edcf60 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 23 Oct 2022 02:07:40 -0400 Subject: [PATCH] feat: hovers & name resolution in registerCombinatorAttribute (part 2) --- src/Lean/Parser/Term.lean | 4 +- src/Lean/PrettyPrinter/Formatter.lean | 132 +++++++++++----------- src/Lean/PrettyPrinter/Parenthesizer.lean | 132 +++++++++++----------- 3 files changed, 134 insertions(+), 134 deletions(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index a097c0d6e3..f30fa31faf 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -13,8 +13,8 @@ namespace Command def commentBody : Parser := { fn := rawFn (finishCommentBlock 1) (trailingWs := true) } -@[combinator_parenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken -@[combinator_formatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous +@[combinator_parenthesizer commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken +@[combinator_formatter commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine end Command diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 59b08cd723..4774077246 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -173,7 +173,7 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter := else x -@[combinator_formatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := +@[combinator_formatter orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try -- them in turn. Uses the syntax traverser non-linearly! p1 <|> p2 @@ -211,20 +211,20 @@ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do @[implemented_by formatterForKindUnsafe] opaque formatterForKind (k : SyntaxNodeKind) : Formatter -@[combinator_formatter Lean.Parser.withAntiquot] +@[combinator_formatter withAntiquot] def withAntiquot.formatter (antiP p : Formatter) : Formatter := -- TODO: could be optimized using `isAntiquot` (which would have to be moved), but I'd rather -- fix the backtracking hack outright. orelse.formatter antiP p -@[combinator_formatter Lean.Parser.withAntiquotSuffixSplice] +@[combinator_formatter withAntiquotSuffixSplice] def withAntiquotSuffixSplice.formatter (_ : SyntaxNodeKind) (p suffix : Formatter) : Formatter := do if (← getCur).isAntiquotSuffixSplice then visitArgs <| suffix *> p else p -@[combinator_formatter Lean.Parser.tokenWithAntiquot] +@[combinator_formatter tokenWithAntiquot] def tokenWithAntiquot.formatter (p : Formatter) : Formatter := do if (← getCur).isTokenAntiquot then visitArgs p @@ -246,7 +246,7 @@ def categoryFormatterCore (cat : Name) : Formatter := do withAntiquot.formatter (mkAntiquot.formatter' cat.toString cat (isPseudoKind := true)) (formatterForKind stx.getKind) modify fun st => { st with mustBeGrouped := true, isUngrouped := !st.mustBeGrouped } -@[combinator_formatter Lean.Parser.categoryParser] +@[combinator_formatter categoryParser] def categoryParser.formatter (cat : Name) : Formatter := do concat <| categoryFormatterCore cat unless (← get).isUngrouped do @@ -259,31 +259,31 @@ def categoryParser.formatter (cat : Name) : Formatter := do def categoryFormatter (cat : Name) : Formatter := fill <| indent <| categoryFormatterCore cat -@[combinator_formatter Lean.Parser.categoryParserOfStack] +@[combinator_formatter categoryParserOfStack] def categoryParserOfStack.formatter (offset : Nat) : Formatter := do let st ← get let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset) categoryParser.formatter stx.getId -@[combinator_formatter Lean.Parser.parserOfStack] +@[combinator_formatter parserOfStack] def parserOfStack.formatter (offset : Nat) (_prec : Nat := 0) : Formatter := do let st ← get let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset) formatterForKind stx.getKind -@[combinator_formatter Lean.Parser.error] +@[combinator_formatter error] def error.formatter (_msg : String) : Formatter := pure () -@[combinator_formatter Lean.Parser.errorAtSavedPos] +@[combinator_formatter errorAtSavedPos] def errorAtSavedPos.formatter (_msg : String) (_delta : Bool) : Formatter := pure () -@[combinator_formatter Lean.Parser.atomic] +@[combinator_formatter atomic] def atomic.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.lookahead] +@[combinator_formatter lookahead] def lookahead.formatter (_ : Formatter) : Formatter := pure () -@[combinator_formatter Lean.Parser.notFollowedBy] +@[combinator_formatter notFollowedBy] def notFollowedBy.formatter (_ : Formatter) : Formatter := pure () -@[combinator_formatter Lean.Parser.andthen] +@[combinator_formatter andthen] def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1 def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do @@ -292,12 +292,12 @@ def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do trace[PrettyPrinter.format.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'" throwBacktrack -@[combinator_formatter Lean.Parser.node] +@[combinator_formatter node] def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do checkKind k; visitArgs p -@[combinator_formatter Lean.Parser.trailingNode] +@[combinator_formatter trailingNode] def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Formatter := do checkKind k visitArgs do @@ -370,7 +370,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do modify fun st => { st with leadWord := "" } | _ => pure () -@[combinator_formatter Lean.Parser.symbolNoAntiquot] +@[combinator_formatter symbolNoAntiquot] def symbolNoAntiquot.formatter (sym : String) : Formatter := do let stx ← getCur if stx.isToken sym then do @@ -381,11 +381,11 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'" throwBacktrack -@[combinator_formatter Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter +@[combinator_formatter nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter -@[combinator_formatter Lean.Parser.rawCh] def rawCh.formatter (ch : Char) := symbolNoAntiquot.formatter ch.toString +@[combinator_formatter rawCh] def rawCh.formatter (ch : Char) := symbolNoAntiquot.formatter ch.toString -@[combinator_formatter Lean.Parser.unicodeSymbolNoAntiquot] +@[combinator_formatter unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do let Syntax.atom info val ← getCur | throwError m!"not an atom: {← getCur}" @@ -395,7 +395,7 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do pushToken info asciiSym; goLeft -@[combinator_formatter Lean.Parser.identNoAntiquot] +@[combinator_formatter identNoAntiquot] def identNoAntiquot.formatter : Formatter := do checkKind identKind let stx@(Syntax.ident info _ id _) ← getCur @@ -404,14 +404,14 @@ def identNoAntiquot.formatter : Formatter := do withMaybeTag (getExprPos? stx) (pushToken info id.toString) goLeft -@[combinator_formatter Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do +@[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do checkKind identKind let Syntax.ident info _ id _ ← getCur | throwError m!"not an ident: {← getCur}" pushToken info id.toString goLeft -@[combinator_formatter Lean.Parser.identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter +@[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter def visitAtom (k : SyntaxNodeKind) : Formatter := do let stx ← getCur @@ -422,24 +422,24 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do pushToken info val goLeft -@[combinator_formatter Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind -@[combinator_formatter Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind -@[combinator_formatter Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind -@[combinator_formatter Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind -@[combinator_formatter Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind -@[combinator_formatter Lean.Parser.fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind +@[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind +@[combinator_formatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind +@[combinator_formatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind +@[combinator_formatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind +@[combinator_formatter scientificLitNoAntiquot] def scientificLitNoAntiquot.formatter := visitAtom scientificLitKind +@[combinator_formatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind -@[combinator_formatter Lean.Parser.manyNoAntiquot] +@[combinator_formatter manyNoAntiquot] def manyNoAntiquot.formatter (p : Formatter) : Formatter := do let stx ← getCur visitArgs $ stx.getArgs.size.forM fun _ => p -@[combinator_formatter Lean.Parser.many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p +@[combinator_formatter many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p -@[combinator_formatter Lean.Parser.optionalNoAntiquot] +@[combinator_formatter optionalNoAntiquot] def optionalNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p -@[combinator_formatter Lean.Parser.many1Unbox] +@[combinator_formatter many1Unbox] def many1Unbox.formatter (p : Formatter) : Formatter := do let stx ← getCur if stx.getKind == nullKind then do @@ -447,65 +447,65 @@ def many1Unbox.formatter (p : Formatter) : Formatter := do else p -@[combinator_formatter Lean.Parser.sepByNoAntiquot] +@[combinator_formatter sepByNoAntiquot] def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do let stx ← getCur visitArgs <| (List.range stx.getArgs.size).reverse.forM fun i => if i % 2 == 0 then p else pSep -@[combinator_formatter Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter +@[combinator_formatter sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter -@[combinator_formatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withoutInfo] def withoutInfo.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.setExpected] +@[combinator_formatter withPosition] def withPosition.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withPositionAfterLinebreak] def withPositionAfterLinebreak.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withForbidden] def withForbidden.formatter (_tk : Token) (p : Formatter) : Formatter := p +@[combinator_formatter withoutForbidden] def withoutForbidden.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withoutInfo] def withoutInfo.formatter (p : Formatter) : Formatter := p +@[combinator_formatter setExpected] def setExpected.formatter (_expected : List String) (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.evalInsideQuot] def evalInsideQuot.formatter (_declName : Name) (p : Formatter) : Formatter := p +@[combinator_formatter incQuotDepth] def incQuotDepth.formatter (p : Formatter) : Formatter := p +@[combinator_formatter decQuotDepth] def decQuotDepth.formatter (p : Formatter) : Formatter := p +@[combinator_formatter suppressInsideQuot] def suppressInsideQuot.formatter (p : Formatter) : Formatter := p +@[combinator_formatter evalInsideQuot] def evalInsideQuot.formatter (_declName : Name) (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.checkWsBefore] def checkWsBefore.formatter : Formatter := do +@[combinator_formatter checkWsBefore] def checkWsBefore.formatter : Formatter := do let st ← get if st.leadWord != "" then pushLine -@[combinator_formatter Lean.Parser.checkPrec] def checkPrec.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkLhsPrec] def checkLhsPrec.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.setLhsPrec] def setLhsPrec.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkStackTop] def checkStackTop.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := +@[combinator_formatter checkPrec] def checkPrec.formatter : Formatter := pure () +@[combinator_formatter checkLhsPrec] def checkLhsPrec.formatter : Formatter := pure () +@[combinator_formatter setLhsPrec] def setLhsPrec.formatter : Formatter := pure () +@[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure () +@[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := -- prevent automatic whitespace insertion modify fun st => { st with leadWord := "" } -@[combinator_formatter Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkTailWs] def checkTailWs.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkColEq] def checkColEq.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkColGe] def checkColGe.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkColGt] def checkColGt.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkLineEq] def checkLineEq.formatter : Formatter := pure () +@[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure () +@[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure () +@[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure () +@[combinator_formatter checkColGe] def checkColGe.formatter : Formatter := pure () +@[combinator_formatter checkColGt] def checkColGt.formatter : Formatter := pure () +@[combinator_formatter checkLineEq] def checkLineEq.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.eoi] def eoi.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.skip] def skip.formatter : Formatter := pure () +@[combinator_formatter eoi] def eoi.formatter : Formatter := pure () +@[combinator_formatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure () +@[combinator_formatter skip] def skip.formatter : Formatter := pure () -@[combinator_formatter Lean.Parser.pushNone] def pushNone.formatter : Formatter := goLeft +@[combinator_formatter pushNone] def pushNone.formatter : Formatter := goLeft -@[combinator_formatter Lean.Parser.withOpenDecl] def withOpenDecl.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.withOpen] def withOpen.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withOpenDecl] def withOpenDecl.formatter (p : Formatter) : Formatter := p +@[combinator_formatter withOpen] def withOpen.formatter (p : Formatter) : Formatter := p -@[combinator_formatter Lean.Parser.interpolatedStr] +@[combinator_formatter interpolatedStr] def interpolatedStr.formatter (p : Formatter) : Formatter := do visitArgs $ (← getCur).getArgs.reverse.forM fun chunk => match chunk.isLit? interpolatedStrLitKind with | some str => push str *> goLeft | none => p -@[combinator_formatter Lean.Parser.dbgTraceState] def dbgTraceState.formatter (_label : String) (p : Formatter) : Formatter := p +@[combinator_formatter dbgTraceState] def dbgTraceState.formatter (_label : String) (p : Formatter) : Formatter := p -@[combinator_formatter ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Formatter) : Formatter := +@[combinator_formatter _root_.ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Formatter) : Formatter := if c then t else e abbrev FormatterAliasValue := AliasValue Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 1b388ab8f3..fd7646c5d2 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -162,7 +162,7 @@ unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttr namespace Parenthesizer -open Lean.Core +open Lean.Core Parser open Std.Format def throwBacktrack {α} : ParenthesizerM α := @@ -247,7 +247,7 @@ def visitToken : Parenthesizer := do modify fun st => { st with contPrec := none, contCat := Name.anonymous, visitedToken := true } goLeft -@[combinator_parenthesizer Lean.Parser.orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do +@[combinator_parenthesizer orelse] def orelse.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := do -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try -- them in turn. Uses the syntax traverser non-linearly! p1 <|> p2 @@ -276,7 +276,7 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do @[implemented_by parenthesizerForKindUnsafe] opaque parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer -@[combinator_parenthesizer Lean.Parser.withAntiquot] +@[combinator_parenthesizer withAntiquot] def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do let stx ← getCur -- early check as minor optimization that also cleans up the backtrack traces @@ -285,14 +285,14 @@ def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do else p -@[combinator_parenthesizer Lean.Parser.withAntiquotSuffixSplice] +@[combinator_parenthesizer withAntiquotSuffixSplice] def withAntiquotSuffixSplice.parenthesizer (_ : SyntaxNodeKind) (p suffix : Parenthesizer) : Parenthesizer := do if (← getCur).isAntiquotSuffixSplice then visitArgs <| suffix *> p else p -@[combinator_parenthesizer Lean.Parser.tokenWithAntiquot] +@[combinator_parenthesizer tokenWithAntiquot] def tokenWithAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do if (← getCur).isTokenAntiquot then visitArgs p @@ -310,7 +310,7 @@ def parenthesizeCategoryCore (cat : Name) (_prec : Nat) : Parenthesizer := withAntiquot.parenthesizer (mkAntiquot.parenthesizer' cat.toString cat (isPseudoKind := true)) (parenthesizerForKind stx.getKind) modify fun st => { st with contCat := cat } -@[combinator_parenthesizer Lean.Parser.categoryParser] +@[combinator_parenthesizer categoryParser] def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do let env ← getEnv match categoryParenthesizerAttribute.getValues env cat with @@ -319,13 +319,13 @@ def categoryParser.parenthesizer (cat : Name) (prec : Nat) : Parenthesizer := do -- In this case this node will never be parenthesized since we don't know which parentheses to use. | _ => parenthesizeCategoryCore cat prec -@[combinator_parenthesizer Lean.Parser.categoryParserOfStack] +@[combinator_parenthesizer categoryParserOfStack] def categoryParserOfStack.parenthesizer (offset : Nat) (prec : Nat) : Parenthesizer := do let st ← get let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset) categoryParser.parenthesizer stx.getId prec -@[combinator_parenthesizer Lean.Parser.parserOfStack] +@[combinator_parenthesizer parserOfStack] def parserOfStack.parenthesizer (offset : Nat) (_prec : Nat := 0) : Parenthesizer := do let st ← get let stx := st.stxTrav.parents.back.getArg (st.stxTrav.idxs.back - offset) @@ -350,27 +350,27 @@ def level.parenthesizer : CategoryParenthesizer | prec => do def rawStx.parenthesizer : CategoryParenthesizer | _ => do goLeft -@[combinator_parenthesizer Lean.Parser.error] +@[combinator_parenthesizer error] def error.parenthesizer (_msg : String) : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.errorAtSavedPos] +@[combinator_parenthesizer errorAtSavedPos] def errorAtSavedPos.parenthesizer (_msg : String) (_delta : Bool) : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.atomic] +@[combinator_parenthesizer atomic] def atomic.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.lookahead] +@[combinator_parenthesizer lookahead] def lookahead.parenthesizer (_ : Parenthesizer) : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.notFollowedBy] +@[combinator_parenthesizer notFollowedBy] def notFollowedBy.parenthesizer (_ : Parenthesizer) : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.andthen] +@[combinator_parenthesizer andthen] def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p2 *> p1 @@ -381,16 +381,16 @@ def checkKind (k : SyntaxNodeKind) : Parenthesizer := do -- HACK; see `orelse.parenthesizer` throwBacktrack -@[combinator_parenthesizer Lean.Parser.node] +@[combinator_parenthesizer node] def node.parenthesizer (k : SyntaxNodeKind) (p : Parenthesizer) : Parenthesizer := do checkKind k visitArgs p -@[combinator_parenthesizer Lean.Parser.checkPrec] +@[combinator_parenthesizer checkPrec] def checkPrec.parenthesizer (prec : Nat) : Parenthesizer := addPrecCheck prec -@[combinator_parenthesizer Lean.Parser.leadingNode] +@[combinator_parenthesizer leadingNode] def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do node.parenthesizer k p addPrecCheck prec @@ -399,7 +399,7 @@ def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesiz -- into a trailing one. modify fun st => { st with contPrec := Nat.min (Parser.maxPrec-1) prec } -@[combinator_parenthesizer Lean.Parser.trailingNode] +@[combinator_parenthesizer trailingNode] def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Parenthesizer) : Parenthesizer := do checkKind k visitArgs do @@ -413,33 +413,33 @@ def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec lhsPrec : Nat) (p : Pa -- parser is calling us. categoryParser.parenthesizer ctx.cat lhsPrec -@[combinator_parenthesizer Lean.Parser.rawCh] def rawCh.parenthesizer (_ch : Char) := visitToken +@[combinator_parenthesizer rawCh] def rawCh.parenthesizer (_ch : Char) := visitToken -@[combinator_parenthesizer Lean.Parser.symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (_sym : String) := visitToken -@[combinator_parenthesizer Lean.Parser.unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken +@[combinator_parenthesizer symbolNoAntiquot] def symbolNoAntiquot.parenthesizer (_sym : String) := visitToken +@[combinator_parenthesizer unicodeSymbolNoAntiquot] def unicodeSymbolNoAntiquot.parenthesizer (_sym _asciiSym : String) := visitToken -@[combinator_parenthesizer Lean.Parser.identNoAntiquot] def identNoAntiquot.parenthesizer := do checkKind identKind; visitToken -@[combinator_parenthesizer Lean.Parser.rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.identEq] def identEq.parenthesizer (_id : Name) := visitToken -@[combinator_parenthesizer Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken +@[combinator_parenthesizer identNoAntiquot] def identNoAntiquot.parenthesizer := do checkKind identKind; visitToken +@[combinator_parenthesizer rawIdentNoAntiquot] def rawIdentNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer identEq] def identEq.parenthesizer (_id : Name) := visitToken +@[combinator_parenthesizer nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.parenthesizer (_sym : String) (_includeIdent : Bool) := visitToken -@[combinator_parenthesizer Lean.Parser.charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.nameLitNoAntiquot] def nameLitNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.numLitNoAntiquot] def numLitNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.fieldIdx] def fieldIdx.parenthesizer := visitToken +@[combinator_parenthesizer charLitNoAntiquot] def charLitNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer strLitNoAntiquot] def strLitNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer nameLitNoAntiquot] def nameLitNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer numLitNoAntiquot] def numLitNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer scientificLitNoAntiquot] def scientificLitNoAntiquot.parenthesizer := visitToken +@[combinator_parenthesizer fieldIdx] def fieldIdx.parenthesizer := visitToken -@[combinator_parenthesizer Lean.Parser.manyNoAntiquot] +@[combinator_parenthesizer manyNoAntiquot] def manyNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do let stx ← getCur visitArgs $ stx.getArgs.size.forM fun _ => p -@[combinator_parenthesizer Lean.Parser.many1NoAntiquot] +@[combinator_parenthesizer many1NoAntiquot] def many1NoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do manyNoAntiquot.parenthesizer p -@[combinator_parenthesizer Lean.Parser.many1Unbox] +@[combinator_parenthesizer many1Unbox] def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do let stx ← getCur if stx.getKind == nullKind then @@ -447,55 +447,55 @@ def many1Unbox.parenthesizer (p : Parenthesizer) : Parenthesizer := do else p -@[combinator_parenthesizer Lean.Parser.optionalNoAntiquot] +@[combinator_parenthesizer optionalNoAntiquot] def optionalNoAntiquot.parenthesizer (p : Parenthesizer) : Parenthesizer := do visitArgs p -@[combinator_parenthesizer Lean.Parser.sepByNoAntiquot] +@[combinator_parenthesizer sepByNoAntiquot] def sepByNoAntiquot.parenthesizer (p pSep : Parenthesizer) : Parenthesizer := do let stx ← getCur visitArgs <| (List.range stx.getArgs.size).reverse.forM fun i => if i % 2 == 0 then p else pSep -@[combinator_parenthesizer Lean.Parser.sepBy1NoAntiquot] def sepBy1NoAntiquot.parenthesizer := sepByNoAntiquot.parenthesizer +@[combinator_parenthesizer sepBy1NoAntiquot] def sepBy1NoAntiquot.parenthesizer := sepByNoAntiquot.parenthesizer -@[combinator_parenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do +@[combinator_parenthesizer withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do -- We assume the formatter will indent syntax sufficiently such that parenthesizing a `withPosition` node is never necessary modify fun st => { st with contPrec := none } p -@[combinator_parenthesizer Lean.Parser.withPositionAfterLinebreak] def withPositionAfterLinebreak.parenthesizer (p : Parenthesizer) : Parenthesizer := +@[combinator_parenthesizer withPositionAfterLinebreak] def withPositionAfterLinebreak.parenthesizer (p : Parenthesizer) : Parenthesizer := -- TODO: improve? withPosition.parenthesizer p -@[combinator_parenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.withoutInfo] def withoutInfo.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.setExpected] +@[combinator_parenthesizer withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withForbidden] def withForbidden.parenthesizer (_tk : Parser.Token) (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withoutForbidden] def withoutForbidden.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withoutInfo] def withoutInfo.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer setExpected] def setExpected.parenthesizer (_expected : List String) (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.evalInsideQuot] def evalInsideQuot.parenthesizer (_declName : Name) (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer incQuotDepth] def incQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer decQuotDepth] def decQuotDepth.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer suppressInsideQuot] def suppressInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer evalInsideQuot] def evalInsideQuot.parenthesizer (_declName : Name) (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkLinebreakBefore] def checkLinebreakBefore.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkColEq] def checkColEq.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkLineEq] def checkLineEq.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.eoi] def eoi.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.skip] def skip.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkLinebreakBefore] def checkLinebreakBefore.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkColEq] def checkColEq.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkLineEq] def checkLineEq.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer eoi] def eoi.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure () +@[combinator_parenthesizer skip] def skip.parenthesizer : Parenthesizer := pure () -@[combinator_parenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft +@[combinator_parenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft -@[combinator_parenthesizer Lean.Parser.withOpenDecl] def withOpenDecl.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.withOpen] def withOpen.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withOpenDecl] def withOpenDecl.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer withOpen] def withOpen.parenthesizer (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer Lean.Parser.interpolatedStr] +@[combinator_parenthesizer interpolatedStr] def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do visitArgs $ (← getCur).getArgs.reverse.forM fun chunk => if chunk.isOfKind interpolatedStrLitKind then @@ -503,9 +503,9 @@ def interpolatedStr.parenthesizer (p : Parenthesizer) : Parenthesizer := do else p -@[combinator_parenthesizer Lean.Parser.dbgTraceState] def dbgTraceState.parenthesizer (_label : String) (p : Parenthesizer) : Parenthesizer := p +@[combinator_parenthesizer dbgTraceState] def dbgTraceState.parenthesizer (_label : String) (p : Parenthesizer) : Parenthesizer := p -@[combinator_parenthesizer ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Parenthesizer) : Parenthesizer := +@[combinator_parenthesizer _root_.ite, macro_inline] def ite {_ : Type} (c : Prop) [Decidable c] (t e : Parenthesizer) : Parenthesizer := if c then t else e open Parser