From e816424466000fcef2a86f2b8a051f27fa285ef6 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 4 Aug 2022 03:10:54 +0200 Subject: [PATCH] chore: use Category declarations for builtin cats too (#1400) --- src/Init/Notation.lean | 2 ++ src/Lean/Parser/Attr.lean | 4 ++-- src/Lean/Parser/Basic.lean | 7 +++---- src/Lean/Parser/Do.lean | 2 +- src/Lean/Parser/Extension.lean | 15 +++++++++------ src/Lean/Parser/Level.lean | 2 +- src/Lean/Parser/Syntax.lean | 4 ++-- src/Lean/Parser/Term.lean | 4 ++-- 8 files changed, 22 insertions(+), 18 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index b09c848c2b..e22d2c6cf5 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -22,6 +22,8 @@ def term : Category := {} def tactic : Category := {} /-- The syntax category for elements that can appear in the `do` notation. -/ def doElem : Category := {} +/-- The level syntax category. -/ +def level : Category := {} /-- The attribute syntax category. Declarations can be annotated with attributes using the `@[...]` notation. -/ def attr : Category := {} /-- The syntax syntax category. This is the syntax category used to define syntax itself. -/ diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean index 7d037d3325..2901522d49 100644 --- a/src/Lean/Parser/Attr.lean +++ b/src/Lean/Parser/Attr.lean @@ -9,11 +9,11 @@ import Lean.Parser.Extra namespace Lean.Parser builtin_initialize - registerBuiltinParserAttribute `builtinPrioParser `prio LeadingIdentBehavior.both + registerBuiltinParserAttribute `builtinPrioParser ``Category.prio .both registerBuiltinDynamicParserAttribute `prioParser `prio builtin_initialize - registerBuiltinParserAttribute `builtinAttrParser `attr LeadingIdentBehavior.symbol + registerBuiltinParserAttribute `builtinAttrParser ``Category.attr .symbol registerBuiltinDynamicParserAttribute `attrParser `attr @[inline] def priorityParser (rbp : Nat := 0) : Parser := diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index e0ae52b477..e648c97cb8 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1614,10 +1614,9 @@ inductive LeadingIdentBehavior where structure ParserCategory where /-- The name of a declaration which will be used as the target of go-to-definition queries and from which doc strings will be extracted. - This is usually a dummy declaration of type `Lean.Parser.Category` - created by `declare_syntax_cat`, but for builtin categories this will - be the `builtin_initialize` command containing the call to - `registerBuiltinParserAttribute`. -/ + This is a dummy declaration of type `Lean.Parser.Category` + created by `declare_syntax_cat`, but for builtin categories the declaration + is made manually and passed to `registerBuiltinParserAttribute`. -/ declName : Name /-- The list of syntax nodes that can parse into this category. This can be used to list all syntaxes in the category. -/ diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index fe662ee6fe..5f744ab2cc 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -8,7 +8,7 @@ import Lean.Parser.Term namespace Lean namespace Parser -builtin_initialize registerBuiltinParserAttribute `builtinDoElemParser `doElem +builtin_initialize registerBuiltinParserAttribute `builtinDoElemParser ``Category.doElem builtin_initialize registerBuiltinDynamicParserAttribute `doElemParser `doElem @[inline] def doElemParser (rbp : Nat := 0) : Parser := diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 5d2555cb5e..7799a4678e 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -509,11 +509,14 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name) /-- The parsing tables for builtin parsers are "stored" in the extracted source code. -/ -def registerBuiltinParserAttribute (attrName : Name) (catName : Name) - (behavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Unit := do - addBuiltinParserCategory catName ref behavior +def registerBuiltinParserAttribute (attrName declName : Name) + (behavior := LeadingIdentBehavior.default) : IO Unit := do + let .str ``Lean.Parser.Category s := declName + | throw (IO.userError "`declName` should be in Lean.Parser.Category") + let catName := Name.mkSimple s + addBuiltinParserCategory catName declName behavior registerBuiltinAttribute { - ref := ref + ref := declName name := attrName descr := "Builtin parser" add := fun declName stx kind => liftM $ BuiltinParserAttribute.add attrName catName declName stx kind @@ -566,12 +569,12 @@ def registerParserCategory (env : Environment) (attrName catName : Name) -- declare `termParser` here since it is used everywhere via antiquotations -builtin_initialize registerBuiltinParserAttribute `builtinTermParser `term +builtin_initialize registerBuiltinParserAttribute `builtinTermParser ``Category.term builtin_initialize registerBuiltinDynamicParserAttribute `termParser `term -- declare `commandParser` to break cyclic dependency -builtin_initialize registerBuiltinParserAttribute `builtinCommandParser `command +builtin_initialize registerBuiltinParserAttribute `builtinCommandParser ``Category.command builtin_initialize registerBuiltinDynamicParserAttribute `commandParser `command diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index c49cb80a69..a23b5de1a2 100644 --- a/src/Lean/Parser/Level.lean +++ b/src/Lean/Parser/Level.lean @@ -9,7 +9,7 @@ namespace Lean namespace Parser builtin_initialize - registerBuiltinParserAttribute `builtinLevelParser `level + registerBuiltinParserAttribute `builtinLevelParser ``Category.level @[inline] def levelParser (rbp : Nat := 0) : Parser := categoryParser `level rbp diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 470fb3e220..89ad653013 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -10,11 +10,11 @@ namespace Lean namespace Parser builtin_initialize - registerBuiltinParserAttribute `builtinSyntaxParser `stx LeadingIdentBehavior.both + registerBuiltinParserAttribute `builtinSyntaxParser ``Category.stx .both registerBuiltinDynamicParserAttribute `stxParser `stx builtin_initialize - registerBuiltinParserAttribute `builtinPrecParser `prec LeadingIdentBehavior.both + registerBuiltinParserAttribute `builtinPrecParser ``Category.prec .both registerBuiltinDynamicParserAttribute `precParser `prec @[inline] def precedenceParser (rbp : Nat := 0) : Parser := diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 95a4f753cf..1a9e1e954d 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -16,11 +16,11 @@ def commentBody : Parser := @[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken @[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine +def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine end Command builtin_initialize - registerBuiltinParserAttribute `builtinTacticParser `tactic LeadingIdentBehavior.both + registerBuiltinParserAttribute `builtinTacticParser ``Category.tactic .both registerBuiltinDynamicParserAttribute `tacticParser `tactic @[inline] def tacticParser (rbp : Nat := 0) : Parser :=