@[inline]
@[inline]
@[inline]
def
Lean.PrettyPrinter.ParenthesizerM.orElse
{α : Type}
(p₁ : Lean.PrettyPrinter.ParenthesizerM α)
(p₂ : Unit → Lean.PrettyPrinter.ParenthesizerM α)
:
Equations
- Lean.PrettyPrinter.ParenthesizerM.orElse p₁ p₂ = do let s ← get Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId p₁ fun x => do set s p₂ ()
Equations
- Lean.PrettyPrinter.instOrElseParenthesizerM = { orElse := Lean.PrettyPrinter.ParenthesizerM.orElse }
Equations
- Lean.PrettyPrinter.mkParenthesizerAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinParenthesizer, name := `parenthesizer, descr := "Register a parenthesizer for a parser.\n\n [parenthesizer k] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `SyntaxNodeKind` `k`.", valueTypeName := `Lean.PrettyPrinter.Parenthesizer, evalKey := fun builtin stx => do let env ← Lean.getEnv let id ← Lean.Attribute.Builtin.getId stx if (builtin && Option.isSome (Lean.Environment.find? env id) || Lean.Parser.isValidSyntaxNodeKind env id) = true then pure id else Lean.throwError (Lean.toMessageData "invalid [parenthesizer] argument, unknown syntax kind '" ++ Lean.toMessageData id ++ Lean.toMessageData "'"), onAdded := fun builtin declName => pure () } `Lean.PrettyPrinter.parenthesizerAttribute
@[inline]
Equations
- Lean.PrettyPrinter.mkCategoryParenthesizerAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinCategoryParenthesizer, name := `categoryParenthesizer, descr := "Register a parenthesizer for a syntax category.\n\n [categoryParenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`,\n which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize`\n with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized,\n but still be traversed for parenthesizing nested categories.", valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer, evalKey := fun x stx => do let env ← Lean.getEnv let id ← Lean.Attribute.Builtin.getId stx if Lean.Parser.isParserCategory env id = true then pure id else Lean.throwError (Lean.toMessageData "invalid [categoryParenthesizer] argument, unknown parser category '" ++ Lean.toMessageData (toString id) ++ Lean.toMessageData "'"), onAdded := fun builtin declName => pure () } `Lean.PrettyPrinter.categoryParenthesizerAttribute
Equations
- Lean.PrettyPrinter.mkCombinatorParenthesizerAttribute = Lean.ParserCompiler.registerCombinatorAttribute `combinatorParenthesizer "Register a parenthesizer for a parser combinator.\n\n [combinatorParenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`.\n Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds.\n The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced\n with `Parenthesizer` in the parameter types."
Equations
- Lean.PrettyPrinter.Parenthesizer.throwBacktrack = throw (Lean.Exception.internal Lean.PrettyPrinter.backtrackExceptionId)
Equations
- Lean.PrettyPrinter.Parenthesizer.instMonadTraverserParenthesizerM = { st := { get := Lean.PrettyPrinter.Parenthesizer.State.stxTrav <$> get, set := fun t => modify fun st => { stxTrav := t, contPrec := st.contPrec, contCat := st.contCat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken }, modifyGet := fun {α} f => modifyGet fun st => let x := f st.stxTrav; match x with | (a, t) => (a, { stxTrav := t, contPrec := st.contPrec, contCat := st.contCat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken }) } }
Equations
- Lean.PrettyPrinter.Parenthesizer.addPrecCheck prec = modify fun st => { stxTrav := st.stxTrav, contPrec := some (Nat.min (Option.getD st.contPrec prec) prec), contCat := st.contCat, minPrec := some (Nat.min (Option.getD st.minPrec prec) prec), trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken }
Equations
- Lean.PrettyPrinter.Parenthesizer.visitArgs x = do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => Lean.Syntax.MonadTraverser.goLeft if Array.size (Lean.Syntax.getArgs stx) > 0 then do let y ← SeqLeft.seqLeft (SeqRight.seqRight (Lean.Syntax.MonadTraverser.goDown (Array.size (Lean.Syntax.getArgs stx) - 1)) fun x => x) fun x => Lean.Syntax.MonadTraverser.goUp _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.PrettyPrinter.Parenthesizer.instMonadQuotationParenthesizerM = Lean.MonadQuotation.mk (pure default) (pure default) fun {α} x => x
def
Lean.PrettyPrinter.Parenthesizer.maybeParenthesize
(cat : Lean.Name)
(canJuxtapose : Bool)
(mkParen : Lean.Syntax → Lean.Syntax)
(prec : Nat)
(x : Lean.PrettyPrinter.ParenthesizerM Unit)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.maybeParenthesize cat canJuxtapose mkParen prec x = do let stx ← Lean.Syntax.MonadTraverser.getCur let idx ← Lean.Syntax.MonadTraverser.getIdx let st ← get set { stxTrav := st.stxTrav, contPrec := none, contCat := Lean.Name.anonymous, minPrec := none, trailPrec := none, trailCat := Lean.Name.anonymous, visitedToken := false } let cls : Lean.Name := `PrettyPrinter.parenthesize let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => do x let discr ← get match discr with | { stxTrav := x, contPrec := x_1, contCat := x_2, minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, visitedToken := x_3 } => let cls := `PrettyPrinter.parenthesize; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => let _do_jp := fun y => do let discr ← get let x : Lean.PrettyPrinter.Parenthesizer.State := discr match x with | { stxTrav := x, contPrec := x_4, contCat := x_5, minPrec := x_6, trailPrec := trailPrec, trailCat := x_7, visitedToken := x_8 } => let _do_jp := fun y => modify fun stP => { stxTrav := stP.stxTrav, contPrec := stP.contPrec, contCat := stP.contCat, minPrec := st.minPrec, trailPrec := stP.trailPrec, trailCat := stP.trailCat, visitedToken := stP.visitedToken }; if st.visitedToken = true then do let y ← modify fun stP => { stxTrav := stP.stxTrav, contPrec := stP.contPrec, contCat := stP.contCat, minPrec := stP.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := stP.visitedToken } _do_jp y else let trailPrec := match trailPrec with | some trailPrec => some (Nat.min trailPrec prec) | x => some prec; do let y ← modify fun stP => { stxTrav := stP.stxTrav, contPrec := stP.contPrec, contCat := stP.contCat, minPrec := stP.minPrec, trailPrec := trailPrec, trailCat := cat, visitedToken := stP.visitedToken } _do_jp y; if (decide (prec > minPrec) || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && decide (trailPrec ≤ contPrec) | x, x_4 => false) = true then let _do_jp := fun y => do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : Lean.Syntax → PUnit → Lean.PrettyPrinter.ParenthesizerM Unit := fun stx y => let _do_jp := fun stx y => let stx' := mkParen stx; let _do_jp := fun stx' y => let _do_jp := fun stx' y => let cls := `PrettyPrinter.parenthesize; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => do Lean.Syntax.MonadTraverser.setCur stx' Lean.Syntax.MonadTraverser.goLeft let y ← modify fun st => { stxTrav := st.stxTrav, contPrec := some Lean.Parser.maxPrec, contCat := cat, minPrec := st.minPrec, trailPrec := none, trailCat := st.trailCat, visitedToken := st.visitedToken } _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "parenthesized: " ++ Lean.toMessageData (Lean.Syntax.formatStx stx' none) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; match Lean.Syntax.getTailInfo stx with | Lean.SourceInfo.original x pos trail endPos => let stx' := Lean.Syntax.setTailInfo stx' (Lean.SourceInfo.original (String.toSubstring "") pos trail endPos); do let y ← pure PUnit.unit _do_jp stx' y | x => do let y ← pure PUnit.unit _do_jp stx' y; match Lean.Syntax.getHeadInfo stx with | Lean.SourceInfo.original lead pos x endPos => let stx' := Lean.Syntax.setHeadInfo stx' (Lean.SourceInfo.original lead pos (String.toSubstring "") endPos); do let y ← pure PUnit.unit _do_jp stx' y | x => do let y ← pure PUnit.unit _do_jp stx' y; match Lean.Syntax.getTailInfo stx with | Lean.SourceInfo.original lead pos x endPos => let stx := Lean.Syntax.setTailInfo stx (Lean.SourceInfo.original lead pos (String.toSubstring "") endPos); do let y ← pure PUnit.unit _do_jp stx y | x => do let y ← pure PUnit.unit _do_jp stx y match Lean.Syntax.getHeadInfo stx with | Lean.SourceInfo.original x pos trail endPos => let stx := Lean.Syntax.setHeadInfo stx (Lean.SourceInfo.original (String.toSubstring "") pos trail endPos); do let y ← pure PUnit.unit _do_jp stx y | x => do let y ← pure PUnit.unit _do_jp stx y; if idx > 0 then do let y ← Lean.Syntax.MonadTraverser.goRight _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "...precedences are " ++ Lean.toMessageData prec ++ Lean.toMessageData " >? " ++ Lean.toMessageData minPrec ++ Lean.toMessageData "" ++ if canJuxtapose = true then Lean.toMessageData ", " ++ Lean.toMessageData (trailPrec, trailCat) ++ Lean.toMessageData " <=? " ++ Lean.toMessageData (st.contPrec, st.contCat) ++ Lean.toMessageData "" else Function.comp Lean.MessageData.ofFormat Lean.format "") _do_jp y else do let y ← pure PUnit.unit _do_jp y | x => let cls := `PrettyPrinter.parenthesize; do let a ← Lean.isTracingEnabledFor cls if a = true then Lean.addTrace cls (Lean.toMessageData "visited a syntax tree without precedences?!" ++ Lean.toMessageData (Lean.Format.line ++ Lean.format stx) ++ Lean.toMessageData "") else pure PUnit.unit if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "parenthesizing (cont := " ++ Lean.toMessageData (st.contPrec, st.contCat) ++ Lean.toMessageData ")" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofFormat (Lean.format stx))) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.PrettyPrinter.Parenthesizer.visitToken = do modify fun st => { stxTrav := st.stxTrav, contPrec := none, contCat := Lean.Name.anonymous, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := true } Lean.Syntax.MonadTraverser.goLeft
def
Lean.PrettyPrinter.Parenthesizer.orelse.parenthesizer
(p1 : Lean.PrettyPrinter.Parenthesizer)
(p2 : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.orelse.parenthesizer p1 p2 = do let _ ← get HOrElse.hOrElse p1 fun x => p2
@[extern 8lean_mk_antiquot_parenthesizer]
constant
Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer'
(name : String)
(kind : Option Lean.SyntaxNodeKind)
(anonymous : optParam Bool true)
:
@[extern lean_pretty_printer_parenthesizer_interpret_parser_descr]
Equations
- Lean.PrettyPrinter.Parenthesizer.parenthesizerForKindUnsafe k = if (k == `missing) = true then pure () else do let p ← liftM (Lean.PrettyPrinter.runForNodeKind Lean.PrettyPrinter.parenthesizerAttribute k Lean.PrettyPrinter.Parenthesizer.interpretParserDescr') p
@[implementedBy Lean.PrettyPrinter.Parenthesizer.parenthesizerForKindUnsafe]
def
Lean.PrettyPrinter.Parenthesizer.withAntiquotSuffixSplice.parenthesizer
(k : Lean.SyntaxNodeKind)
(p : Lean.PrettyPrinter.Parenthesizer)
(suffix : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.withAntiquotSuffixSplice.parenthesizer k p suffix = do let a ← Lean.Syntax.MonadTraverser.getCur if Lean.Syntax.isAntiquotSuffixSplice a = true then Lean.PrettyPrinter.Parenthesizer.visitArgs (SeqRight.seqRight suffix fun x => p) else p
def
Lean.PrettyPrinter.Parenthesizer.tokenWithAntiquot.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.tokenWithAntiquot.parenthesizer p = do let a ← Lean.Syntax.MonadTraverser.getCur if Lean.Syntax.isTokenAntiquot a = true then Lean.PrettyPrinter.Parenthesizer.visitArgs p else p
Equations
- Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore cat prec = withReader (fun ctx => { cat := cat }) do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => modify fun st => { stxTrav := st.stxTrav, contPrec := st.contPrec, contCat := cat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken } if (Lean.Syntax.getKind stx == `choice) = true then do let y ← Lean.PrettyPrinter.Parenthesizer.visitArgs (Nat.forM (Array.size (Lean.Syntax.getArgs stx)) fun x => do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind (Lean.Syntax.getKind stx)) _do_jp y else do let y ← Lean.PrettyPrinter.Parenthesizer.withAntiquot.parenthesizer (Lean.PrettyPrinter.Parenthesizer.mkAntiquot.parenthesizer' (Lean.Name.toString cat) none true) (Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind (Lean.Syntax.getKind stx)) _do_jp y
Equations
- Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer cat prec = do let env ← Lean.getEnv match Lean.KeyedDeclsAttribute.getValues Lean.PrettyPrinter.categoryParenthesizerAttribute env cat with | p :: x => p prec | x => Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore cat prec
def
Lean.PrettyPrinter.Parenthesizer.categoryParserOfStack.parenthesizer
(offset : Nat)
(prec : Nat)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.categoryParserOfStack.parenthesizer offset prec = do let st ← get let stx : Lean.Syntax := Lean.Syntax.getArg (Array.back st.stxTrav.parents) (Array.back st.stxTrav.idxs - offset) Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer (Lean.Syntax.getId stx) prec
def
Lean.PrettyPrinter.Parenthesizer.parserOfStack.parenthesizer
(offset : Nat)
(prec : optParam Nat 0)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.parserOfStack.parenthesizer offset prec = do let st ← get let stx : Lean.Syntax := Lean.Syntax.getArg (Array.back st.stxTrav.parents) (Array.back st.stxTrav.idxs - offset) Lean.PrettyPrinter.Parenthesizer.parenthesizerForKind (Lean.Syntax.getKind stx)
Equations
- Lean.PrettyPrinter.Parenthesizer.term.parenthesizer x = let prec := x; do let stx ← Lean.Syntax.MonadTraverser.getCur if (Lean.Syntax.getKind stx == Lean.nullKind) = true then Lean.PrettyPrinter.Parenthesizer.throwBacktrack else Lean.PrettyPrinter.Parenthesizer.maybeParenthesize `term true (fun stx => Lean.Unhygienic.run do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `null #[stx, Lean.Syntax.node Lean.SourceInfo.none `null #[]], Lean.Syntax.atom info ")"])) prec (Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore `term prec)
Equations
- Lean.PrettyPrinter.Parenthesizer.tactic.parenthesizer x = let prec := x; Lean.PrettyPrinter.Parenthesizer.maybeParenthesize `tactic false (fun stx => Lean.Unhygienic.run do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.paren #[Lean.Syntax.atom info "(", Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Tactic.tacticSeq #[stx], Lean.Syntax.atom info ")"])) prec (Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore `tactic prec)
Equations
- Lean.PrettyPrinter.Parenthesizer.level.parenthesizer x = let prec := x; Lean.PrettyPrinter.Parenthesizer.maybeParenthesize `level false (fun stx => Lean.Unhygienic.run do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure (Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Level.paren #[Lean.Syntax.atom info "(", stx, Lean.Syntax.atom info ")"])) prec (Lean.PrettyPrinter.Parenthesizer.parenthesizeCategoryCore `level prec)
Equations
def
Lean.PrettyPrinter.Parenthesizer.andthen.parenthesizer
(p1 : Lean.PrettyPrinter.Parenthesizer)
(p2 : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.andthen.parenthesizer p1 p2 = SeqRight.seqRight p2 fun x => p1
def
Lean.PrettyPrinter.Parenthesizer.node.parenthesizer
(k : Lean.SyntaxNodeKind)
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.node.parenthesizer k p = do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : PUnit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => Lean.PrettyPrinter.Parenthesizer.visitArgs p if (k != Lean.Syntax.getKind stx) = true then let cls := `PrettyPrinter.parenthesize.backtrack; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => do let y ← Lean.PrettyPrinter.Parenthesizer.throwBacktrack _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "unexpected node kind '" ++ Lean.toMessageData (Lean.Syntax.getKind stx) ++ Lean.toMessageData "', expected '" ++ Lean.toMessageData k ++ Lean.toMessageData "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.PrettyPrinter.Parenthesizer.leadingNode.parenthesizer
(k : Lean.SyntaxNodeKind)
(prec : Nat)
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.leadingNode.parenthesizer k prec p = do Lean.PrettyPrinter.Parenthesizer.node.parenthesizer k p Lean.PrettyPrinter.Parenthesizer.addPrecCheck prec modify fun st => { stxTrav := st.stxTrav, contPrec := some (Nat.min (Lean.Parser.maxPrec - 1) prec), contCat := st.contCat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken }
def
Lean.PrettyPrinter.Parenthesizer.trailingNode.parenthesizer
(k : Lean.SyntaxNodeKind)
(prec : Nat)
(lhsPrec : Nat)
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.trailingNode.parenthesizer k prec lhsPrec p = do let stx ← Lean.Syntax.MonadTraverser.getCur let _do_jp : PUnit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => Lean.PrettyPrinter.Parenthesizer.visitArgs do p Lean.PrettyPrinter.Parenthesizer.addPrecCheck prec let ctx ← read modify fun st => { stxTrav := st.stxTrav, contPrec := st.contPrec, contCat := ctx.cat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken } Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer ctx.cat lhsPrec if (k != Lean.Syntax.getKind stx) = true then let cls := `PrettyPrinter.parenthesize.backtrack; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.PrettyPrinter.ParenthesizerM Unit := fun y => do let y ← Lean.PrettyPrinter.Parenthesizer.throwBacktrack _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "unexpected node kind '" ++ Lean.toMessageData (Lean.Syntax.getKind stx) ++ Lean.toMessageData "', expected '" ++ Lean.toMessageData k ++ Lean.toMessageData "'") _do_jp y else do let y ← pure PUnit.unit _do_jp y else do let y ← pure PUnit.unit _do_jp y
def
Lean.PrettyPrinter.Parenthesizer.nonReservedSymbolNoAntiquot.parenthesizer
(sym : String)
(includeIdent : Bool)
:
def
Lean.PrettyPrinter.Parenthesizer.manyNoAntiquot.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.manyNoAntiquot.parenthesizer p = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.visitArgs (Nat.forM (Array.size (Lean.Syntax.getArgs stx)) fun x => p)
def
Lean.PrettyPrinter.Parenthesizer.many1Unbox.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.many1Unbox.parenthesizer p = do let stx ← Lean.Syntax.MonadTraverser.getCur if (Lean.Syntax.getKind stx == Lean.nullKind) = true then Lean.PrettyPrinter.Parenthesizer.manyNoAntiquot.parenthesizer p else p
def
Lean.PrettyPrinter.Parenthesizer.sepByNoAntiquot.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
(pSep : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.sepByNoAntiquot.parenthesizer p pSep = do let stx ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.visitArgs (List.forM (List.reverse (List.range (Array.size (Lean.Syntax.getArgs stx)))) fun i => if (i % 2 == 0) = true then p else pSep)
def
Lean.PrettyPrinter.Parenthesizer.withPosition.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.withPosition.parenthesizer p = do modify fun st => { stxTrav := st.stxTrav, contPrec := none, contCat := st.contCat, minPrec := st.minPrec, trailPrec := st.trailPrec, trailCat := st.trailCat, visitedToken := st.visitedToken } p
def
Lean.PrettyPrinter.Parenthesizer.setExpected.parenthesizer
(expected : List String)
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
def
Lean.PrettyPrinter.Parenthesizer.evalInsideQuot.parenthesizer
(declName : Lean.Name)
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
Equations
- Lean.PrettyPrinter.Parenthesizer.pushNone.parenthesizer = Lean.Syntax.MonadTraverser.goLeft
def
Lean.PrettyPrinter.Parenthesizer.interpolatedStr.parenthesizer
(p : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.interpolatedStr.parenthesizer p = do let a ← Lean.Syntax.MonadTraverser.getCur Lean.PrettyPrinter.Parenthesizer.visitArgs (Array.forM (fun chunk => if Lean.Syntax.isOfKind chunk Lean.interpolatedStrLitKind = true then Lean.Syntax.MonadTraverser.goLeft else p) (Array.reverse (Lean.Syntax.getArgs a)) 0 (Array.size (Array.reverse (Lean.Syntax.getArgs a))))
@[macroInline]
def
Lean.PrettyPrinter.Parenthesizer.ite
{α : Type}
(c : Prop)
[h : Decidable c]
(t : Lean.PrettyPrinter.Parenthesizer)
(e : Lean.PrettyPrinter.Parenthesizer)
:
Equations
- Lean.PrettyPrinter.Parenthesizer.ite c t e = if c then t else e
def
Lean.PrettyPrinter.Parenthesizer.registerAlias
(aliasName : Lean.Name)
(v : Lean.PrettyPrinter.Parenthesizer.ParenthesizerAliasValue)
:
Equations
Equations
- Lean.PrettyPrinter.Parenthesizer.instCoeParenthesizerParenthesizerAliasValue = { coe := Lean.Parser.AliasValue.const }
Equations
- Lean.PrettyPrinter.Parenthesizer.instCoeForAllParenthesizerParenthesizerAliasValue = { coe := Lean.Parser.AliasValue.unary }
Equations
- Lean.PrettyPrinter.Parenthesizer.instCoeForAllParenthesizerParenthesizerAliasValue_1 = { coe := Lean.Parser.AliasValue.binary }
def
Lean.PrettyPrinter.parenthesize
(parenthesizer : Lean.PrettyPrinter.Parenthesizer)
(stx : Lean.Syntax)
:
Equations
- Lean.PrettyPrinter.parenthesize parenthesizer stx = let cls := `PrettyPrinter.parenthesize.input; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.CoreM Lean.Syntax := fun y => Lean.catchInternalId Lean.PrettyPrinter.backtrackExceptionId (do let discr ← StateRefT'.run (parenthesizer { cat := Lean.Name.anonymous }) { stxTrav := Lean.Syntax.Traverser.fromSyntax stx, contPrec := none, contCat := Lean.Name.anonymous, minPrec := none, trailPrec := none, trailCat := Lean.Name.anonymous, visitedToken := false } let x : Unit × Lean.PrettyPrinter.Parenthesizer.State := discr match x with | (x, st) => pure st.stxTrav.cur) fun x => Lean.throwError (Lean.toMessageData "parenthesize: uncaught backtrack exception") if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Lean.format stx) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y