From ffee6676effe44de95947037a8ed76508ceaedd1 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 31 Mar 2022 11:29:15 +0200 Subject: [PATCH] feat: allow adjusting anonymous antiquot generation at `leading_parser` --- src/Lean/Elab/BuiltinNotation.lean | 10 +++++----- src/Lean/Parser/Term.lean | 3 ++- stage0/src/stdlib_flags.h | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 5d10041a0b..7b4a54ec85 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -96,21 +96,21 @@ are turned into a new anonymous constructor application. For example, | _ => Macro.throwUnsupported open Lean.Parser in -private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do +private def elabParserMacroAux (prec : Syntax) (e : Syntax) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do let (some declName) ← getDeclName? | throwError "invalid `leading_parser` macro, it must be used in definitions" match extractMacroScopes declName with | { name := Name.str _ s _, .. } => let kind := quote declName let s := quote s - ``(withAntiquot (mkAntiquot $s $kind) (leadingNode $kind $prec $e)) + ``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e)) | _ => throwError "invalid `leading_parser` macro, unexpected declaration name" @[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab := adaptExpander fun stx => match stx with - | `(leading_parser $e) => elabParserMacroAux (quote Parser.maxPrec) e - | `(leading_parser : $prec $e) => elabParserMacroAux prec e - | _ => throwUnsupportedSyntax + | `(leading_parser $[: $prec?]? $[(withAnonymousAntiquot := $anon?)]? $e) => + elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.isOfKind ``Parser.Term.trueVal)) + | _ => throwUnsupportedSyntax private def elabTParserMacroAux (prec lhsPrec : Syntax) (e : Syntax) : TermElabM Syntax := do let declName? ← getDeclName? diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index ce2cdead49..04c5a9f71f 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -164,7 +164,8 @@ def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun @[builtinTermParser] def «fun» := leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts) def optExprPrecedence := optional (atomic ":" >> termParser maxPrec) -@[builtinTermParser] def «leading_parser» := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> termParser +def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "withAnonymousAntiquot" >> " := ") >> (trueVal <|> falseVal) >> ")" >> ppSpace +@[builtinTermParser] def «leading_parser» := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> optional withAnonymousAntiquot >> termParser @[builtinTermParser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser @[builtinTermParser] def borrowed := leading_parser "@& " >> termParser leadPrec diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 77aa54db2d..af0dd83b01 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -8,7 +8,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); #endif return opts; }