From 1c770ac8d7c6f501cfc39101d111eb4e1c53c671 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Jul 2022 13:40:08 -0700 Subject: [PATCH] feat: doc strings for `declare_syntax_cat` see #1374 --- src/Init/Notation.lean | 26 +++++++++++- src/Lean/Elab/Syntax.lean | 22 +++++++--- src/Lean/Parser/Syntax.lean | 2 +- tests/lean/interactive/catHover.lean | 19 +++++++++ .../interactive/catHover.lean.expected.out | 40 +++++++++++++++++++ 5 files changed, 101 insertions(+), 8 deletions(-) create mode 100644 tests/lean/interactive/catHover.lean create mode 100644 tests/lean/interactive/catHover.lean.expected.out diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 8b2e7ae892..b09c848c2b 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -9,10 +9,34 @@ prelude import Init.Prelude import Init.Coe --- DSL for specifying parser precedences and priorities +/-- Auxiliary type used to represent syntax categories. We mainly use them to attach doc strings to syntax categories. -/ +structure Lean.Parser.Category + +namespace Lean.Parser.Category + +/-- The command syntax category. -/ +def command : Category := {} +/-- The term syntax category. -/ +def term : Category := {} +/-- The tactic syntax category. -/ +def tactic : Category := {} +/-- The syntax category for elements that can appear in the `do` notation. -/ +def doElem : 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. -/ +def stx : Category := {} +/-- The priority syntax category. Priorities are used in many different attributes. -/ +def prio : Category := {} +/-- The precedence syntax category. Parsers have precedence in Lean. -/ +def prec : Category := {} + +end Lean.Parser.Category namespace Lean.Parser.Syntax +/-! DSL for specifying parser precedences and priorities -/ + syntax:65 (name := addPrec) prec " + " prec:66 : prec syntax:65 (name := subPrec) prec " - " prec:66 : prec diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index b2d4349b27..bf5c64a6e8 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -87,6 +87,12 @@ def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv | _ => none catch _ => return [] +/-- (Try to) a term info for the category `catName` at `ref`. -/ +def addCategoryInfo (ref : Syntax) (catName : Name) : TermElabM Unit := do + let declName := ``Lean.Parser.Category ++ catName + if (← getEnv).contains declName then + addTermInfo' ref (Lean.mkConst declName) + open TSyntax.Compat in /-- Given a `stx` of category `syntax`, return a `(newStx, lhsPrec?)`, @@ -148,6 +154,7 @@ where throwErrorAt stx "invalid atomic left recursive syntax" let prec? ← liftMacroM <| expandOptPrecedence stx[1] let prec := prec?.getD 0 + addCategoryInfo stx catName return (← `(ParserDescr.cat $(quote catName) $(quote prec)), 1) processAlias (id : Syntax) (args : Array Syntax) := do @@ -254,19 +261,21 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d elabCommand cmd @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do - let catName := stx[1].getId + let docString? := stx[0].getOptional?.map fun stx => ⟨stx⟩ + let catName := stx[2].getId let catBehavior := - if stx[2].isNone then + if stx[3].isNone then Parser.LeadingIdentBehavior.default - else if stx[2][3].getKind == ``Parser.Command.catBehaviorBoth then + else if stx[3][3].getKind == ``Parser.Command.catBehaviorBoth then Parser.LeadingIdentBehavior.both else Parser.LeadingIdentBehavior.symbol let attrName := catName.appendAfter "Parser" - let env ← getEnv - let env ← Parser.registerParserCategory env attrName catName catBehavior - setEnv env + setEnv (← Parser.registerParserCategory (← getEnv) attrName catName catBehavior) + let catDeclName := `_root_ ++ ``Lean.Parser.Category ++ catName + let cmd ← `($[$docString?]? def $(mkIdentFrom stx[2] catDeclName) : Lean.Parser.Category := {}) declareSyntaxCatQuotParser catName + elabCommand cmd /-- Auxiliary function for creating declaration names from parser descriptions. @@ -330,6 +339,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do let cat := catStx.getId.eraseMacroScopes unless (Parser.isParserCategory (← getEnv) cat) do throwErrorAt catStx "unknown category '{cat}'" + liftTermElabM none <| Term.addCategoryInfo catStx cat let syntaxParser := mkNullNode ps -- If the user did not provide an explicit precedence, we assign `maxPrec` to atom-like syntax and `leadPrec` otherwise. let precDefault := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 9eaddf7db8..470fb3e220 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -74,7 +74,7 @@ def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Par def catBehaviorBoth := leading_parser nonReservedSymbol "both" def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol" def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")") -@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident >> catBehavior +@[builtinCommandParser] def syntaxCat := leading_parser optional docComment >> "declare_syntax_cat " >> ident >> catBehavior def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> withPosition termParser def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1 diff --git a/tests/lean/interactive/catHover.lean b/tests/lean/interactive/catHover.lean new file mode 100644 index 0000000000..4a5b3632b4 --- /dev/null +++ b/tests/lean/interactive/catHover.lean @@ -0,0 +1,19 @@ +/-- Index syntax categoy -/ +declare_syntax_cat index + + --v textDocument/hover +syntax "foo " term prio index : term + --^ textDocument/hover + --^ textDocument/hover +namespace Foo + +/-- Value syntax category -/ +declare_syntax_cat value + +syntax "bla " value : term + --^ textDocument/hover + +end Foo + +macro "boo " : term => `(0) + --^ textDocument/hover diff --git a/tests/lean/interactive/catHover.lean.expected.out b/tests/lean/interactive/catHover.lean.expected.out new file mode 100644 index 0000000000..9eafda9050 --- /dev/null +++ b/tests/lean/interactive/catHover.lean.expected.out @@ -0,0 +1,40 @@ +{"textDocument": {"uri": "file://catHover.lean"}, + "position": {"line": 4, "character": 33}} +{"range": + {"start": {"line": 4, "character": 32}, "end": {"line": 4, "character": 36}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\nThe term syntax category. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://catHover.lean"}, + "position": {"line": 4, "character": 14}} +{"range": + {"start": {"line": 4, "character": 14}, "end": {"line": 4, "character": 18}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\nThe term syntax category. ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://catHover.lean"}, + "position": {"line": 4, "character": 25}} +{"range": + {"start": {"line": 4, "character": 24}, "end": {"line": 4, "character": 29}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.index : Lean.Parser.Category\n```\n***\nIndex syntax categoy ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://catHover.lean"}, + "position": {"line": 12, "character": 16}} +{"range": + {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 19}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.value : Lean.Parser.Category\n```\n***\nValue syntax category ", + "kind": "markdown"}} +{"textDocument": {"uri": "file://catHover.lean"}, + "position": {"line": 17, "character": 15}} +{"range": + {"start": {"line": 17, "character": 15}, "end": {"line": 17, "character": 19}}, + "contents": + {"value": + "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\nThe term syntax category. ", + "kind": "markdown"}}