max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: simplify processing of antiquotations in pretty-printer

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-05 16:05:38 +02:00 • committed by Leonardo de Moura
parent eded953022
commit 3f6de2af06
4 changed files with 54 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/Elab/Quotation.lean
View file

@ -49,14 +49,15 @@ else
def antiquotKind? : Syntax → Option SyntaxNodeKind
| Syntax.node (Name.str k "antiquot" _) args =>
-- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
if (args.get! 3).isNone then some Name.anonymous
else some k
if (args.get! 3).isOfKind `antiquotName then some k
else
-- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
some Name.anonymous
| _ => none
-- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
def isAntiquotSplice (stx : Syntax) : Bool :=
isAntiquot stx && (stx.getArg 5).getOptional?.isSome
isAntiquot stx && (stx.getArg 4).getOptional?.isSome
-- If any item of a `many` node is an antiquotation splice, its result should
-- be substituted into the `many` node's children

12
src/Lean/Parser/Parser.lean
View file

@ -1428,7 +1428,7 @@ categoryParser `term prec
def dollarSymbol : Parser := symbol "$"
/-- Fail if previous token is immediately followed by ':'. -/
private def noImmediateColon : Parser :=
def checkNoImmediateColon : Parser :=
{ fn := fun c s =>
let prev := s.stxStack.back;
if checkTailNoWs prev then
@ -1466,10 +1466,10 @@ def antiquotExpr : Parser := identNoAntiquot <|> antiquotNestedExpr
produces the syntax tree for `$e`. -/
def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser :=
let kind := (kind.getD Name.anonymous) ++ `antiquot;
let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name;
let nameP := node `antiquotName $ checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbol ":" >> nonReservedSymbol name;
-- if parsing the kind fails and `anonymous` is true, check that we're not ignoring a different
-- antiquotation kind via `noImmediateColon`
let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP;
let nameP := if anonymous then nameP <|> checkNoImmediateColon >> pushNone else nameP;
-- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error
node kind $ try $
setExpected [] dollarSymbol >>
@ -1866,15 +1866,15 @@ private def catNameToString : Name → String
| Name.str Name.anonymous s _ => s
| n => n.toString
@[inline] def mkCategoryAntiquotParser (kind : Name) : ParserFn :=
(mkAntiquot (catNameToString kind) none).fn
@[inline] def mkCategoryAntiquotParser (kind : Name) : Parser :=
mkAntiquot (catNameToString kind) none
def categoryParserFnImpl (catName : Name) : ParserFn :=
fun ctx s =>
let categories := (parserExtension.getState ctx.env).categories;
match categories.find? catName with
| some cat =>
prattParser catName cat.tables cat.leadingIdentAsSymbol (mkCategoryAntiquotParser catName) ctx s
prattParser catName cat.tables cat.leadingIdentAsSymbol (mkCategoryAntiquotParser catName).fn ctx s
| none => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
@[init] def setCategoryParserFnRef : IO Unit :=

20
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -142,17 +142,13 @@ trace! `PrettyPrinter.format (" => " ++ (stack.extract sp stack.size).foldl (fun
open Lean.Parser
def visitAntiquot : Formatter | _ => do
stx ← getCur;
if Elab.Term.Quotation.isAntiquot stx then
visit (mkAppN (mkConst `Lean.Parser.mkAntiquot) #[mkNatLit 0, mkNatLit 0])
else
throw $ Exception.other $ "not an antiquotation"
@[builtinFormatter categoryParser]
def categoryParser.formatter : Formatter | p => visitAntiquot p <|> do
def categoryParser.formatter : Formatter | p => do
stx ← getCur;
visit (mkConst stx.getKind)
-- visit `(mkCategoryAntiquotParser $(p.getArg! 0) <|> $(mkConst stx.getKind))
visit (mkAppN (mkConst `Lean.Parser.orelse) #[
mkApp (mkConst `Lean.Parser.mkCategoryAntiquotParser) (p.getArg! 0),
mkConst stx.getKind])
@[builtinFormatter termParser]
def termParser.formatter : Formatter | p => do
@ -165,7 +161,8 @@ else
@[builtinFormatter withAntiquot]
def withAntiquot.formatter : Formatter | p =>
visitAntiquot p <|> visit (p.getArg! 1)
-- deoptimize
visit (mkAppN (mkConst `Lean.Parser.orelse) #[p.getArg! 0, p.getArg! 1])
@[builtinFormatter try]
def try.formatter : Formatter | p =>
@ -304,6 +301,8 @@ catch (visit (p.getArg! 0)) $ fun e => match e with
-- call closure with dummy position
visit $ mkApp (p.getArg! 0) (mkConst `sorryAx [levelZero])
@[builtinFormatter setExpected] def setExpected.formatter : Formatter | p => visit (p.getArg! 1)
@[builtinFormatter checkWsBefore] def checkWsBefore.formatter : Formatter | p => do
modify fun st => { st with leadWord := "" };
push " "
@ -313,6 +312,7 @@ push " "
@[builtinFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter | p => pure ()
@[builtinFormatter checkTailWs] def checkTailWs.formatter : Formatter | p => pure ()
@[builtinFormatter checkColGe] def checkColGe.formatter : Formatter | p => pure ()
@[builtinFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter | p => pure ()
@[builtinFormatter pushNone] def pushNone.formatter : Formatter | p => goLeft

66
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -63,7 +63,7 @@ practice since if there is another parser to the left that produced zero nodes i
there is no danger of the left-most child being processed multiple times.
Ultimately, most parenthesizers are implemented via three primitives that do all the actual syntax traversal:
`visitParenthesizable mkParen prec` recurses on the current node and afterwards transforms it with `mkParen` if the above
`maybeParenthesize mkParen prec x` runs `x` and afterwards transforms it with `mkParen` if the above
condition for `p prec` is fulfilled. `visitToken` advances to the preceding sibling and is used on atoms. `visitArgs x`
executes `x` on the last child of the current node and then advances to the preceding sibling (of the original current
node).
@ -165,6 +165,12 @@ match c >>= (parenthesizerAttribute.ext.getState env).table.find? with
| throw $ Exception.other $ "no known parenthesizer for '" ++ toString p ++ "'";
visit p'
/-- Continue evaluation of `p` by further reducing it. -/
def resume : Parenthesizer | p => do
some p' ← liftM $ unfoldDefinition? p
| throw $ Exception.other $ "no known parenthesizer for '" ++ toString p ++ "'";
visit p'
open Lean.Parser
-- Macro scopes in the parenthesizer output are ultimately ignored by the pretty printer,
@ -175,26 +181,14 @@ 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, `syntax:maxPrec "$" "$"* antiquotExpr ":" (nonReservedSymbol name) "*"?`
goLeft; goLeft; goLeft; -- now on `antiquotExpr`
visit (mkConst `Lean.Parser.antiquotExpr);
addPrecCheck maxPrec
else
throw $ Exception.other $ "not an antiquotation"
/-- Recurse using `visit`, and parenthesize the result using `mkParen` if necessary. -/
def visitParenthesizable (mkParen : Syntax → Syntax) (prec : Nat) : ParenthesizerM Unit := do
/-- Run `x` and parenthesize the result using `mkParen` if necessary. -/
def maybeParenthesize (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
stx ← getCur;
idx ← getIdx;
st ← get;
-- reset prec/prec and store `mkParen` for the recursive call
set { stxTrav := st.stxTrav };
adaptReader (fun (ctx : Context) => { ctx with mkParen := some mkParen }) $
-- we assume that each node kind is produced by a 0-ary parser of the same name
visit (mkConst stx.getKind);
adaptReader (fun (ctx : Context) => { ctx with mkParen := some mkParen }) x;
{ minPrec := some minPrec, trailPrec := trailPrec, .. } ← get
| panic! "visitParenthesizable: visited a term without tokens?!";
trace! `PrettyPrinter.parenthesize ("...precedences are " ++ fmt prec ++ " >? " ++ fmt minPrec ++ ", " ++ fmt trailPrec ++ " <=? " ++ fmt st.contPrec);
@ -231,34 +225,38 @@ def visitToken : Parenthesizer | p => do
modify (fun st => { st with contPrec := none, visitedToken := true });
goLeft
@[builtinParenthesizer categoryParser]
def categoryParser.parenthesizer : Parenthesizer | p => do
stx ← getCur;
-- visit `(mkCategoryAntiquotParser $(p.getArg! 0) <|> $(mkConst stx.getKind))
visit (mkAppN (mkConst `Lean.Parser.orelse) #[
mkApp (mkConst `Lean.Parser.mkCategoryAntiquotParser) (p.getArg! 0),
mkConst stx.getKind])
@[builtinParenthesizer termParser]
def termParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
def termParser.parenthesizer : Parenthesizer | p => do
stx ← getCur;
-- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
if stx.getKind == nullKind then
throw $ Exception.other "BACKTRACK"
else do
prec ← liftM $ reduceEval p.appArg!;
visitParenthesizable (fun stx => Unhygienic.run `(($stx))) prec
maybeParenthesize (fun stx => Unhygienic.run `(($stx))) prec (resume p)
@[builtinParenthesizer tacticParser]
def tacticParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
def tacticParser.parenthesizer : Parenthesizer | p => do
prec ← liftM $ reduceEval p.appArg!;
visitParenthesizable (fun stx => Unhygienic.run `(tactic|($stx))) prec
maybeParenthesize (fun stx => Unhygienic.run `(tactic|($stx))) prec (resume p)
@[builtinParenthesizer levelParser]
def levelParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
def levelParser.parenthesizer : Parenthesizer | p => do
prec ← liftM $ reduceEval p.appArg!;
visitParenthesizable (fun stx => Unhygienic.run `(level|($stx))) prec
@[builtinParenthesizer categoryParser]
def categoryParser.parenthesizer : Parenthesizer | p => visitAntiquot <|> do
stx ← getCur;
visit (mkConst stx.getKind)
maybeParenthesize (fun stx => Unhygienic.run `(level|($stx))) prec (resume p)
@[builtinParenthesizer withAntiquot]
def withAntiquot.parenthesizer : Parenthesizer | p =>
visitAntiquot <|> visit (p.getArg! 1)
-- deoptimize
visit (mkAppN (mkConst `Lean.Parser.orelse) #[p.getArg! 0, p.getArg! 1])
@[builtinParenthesizer try]
def try.parenthesizer : Parenthesizer | p =>
@ -289,9 +287,7 @@ def leadingNode.parenthesizer : Parenthesizer | p => do
-- Unfold `leadingNode` as usual, but limit `contPrec` to `maxPrec-1` afterwards.
-- This is because `maxPrec-1` is the precedence of function application, which is the only way to turn a leading parser
-- into a trailing one.
some p ← liftM $ unfoldDefinition? p
| unreachable!;
visit p;
resume p;
modify $ fun st => { st with contPrec := (fun p => Nat.min (maxPrec-1) p) <$> st.contPrec }
@[builtinParenthesizer trailingNode]
@ -313,7 +309,8 @@ visitArgs $ do {
-- parser is calling us; we only need to know its `mkParen`, which we retrieve from the context.
{ mkParen := some mkParen, .. } ← read
| panic! "trailingNode.parenthesizer called outside of visitParenthesizable call";
visitAntiquot <|> visitParenthesizable mkParen 0
maybeParenthesize mkParen 0 $
visit (mkAppN (mkConst `Lean.Parser.categoryParser) #[toExpr `someCategory, mkNatLit 0])
}
@[builtinParenthesizer symbol] def symbol.parenthesizer := visitToken
@ -366,13 +363,16 @@ catch (visit (p.getArg! 0)) $ fun e => match e with
-- call closure with dummy position
visit $ mkApp (p.getArg! 0) (mkConst `sorryAx [levelZero])
@[builtinParenthesizer setExpected] def setExpected.parenthesizer : Parenthesizer | p => visit (p.getArg! 1)
@[builtinParenthesizer checkStackTop] def checkStackTop.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer checkTailWs] def checkTailWs.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer checkColGe] def checkColGe.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer | p => pure ()
@[builtinParenthesizer pushNone] def pushNone.formatter : Parenthesizer | p => goLeft
@[builtinParenthesizer pushNone] def pushNone.parenthesizer : Parenthesizer | p => goLeft
open Lean.Parser.Command
@[builtinParenthesizer commentBody] def commentBody.parenthesizer := visitToken