84e46162b5
This is the groundwork for a tactic index in generated documentation, as there was in Lean 3. There are a few challenges to getting this to work well in Lean 4: * There's no natural notion of *tactic identity* - a tactic may be specified by multiple syntax rules (e.g. the pattern-matching version of `intro` is specified apart from the default version, but both are the same from a user perspective) * There's no natural notion of *tactic name* - here, we take the pragmatic choice of using the first keyword atom in the tactic's syntax specification, but this may need to be overridable someday. * Tactics are extensible, but we don't want to allow arbitrary imports to clobber existing tactic docstrings, which could become unpredictable in practice. For tactic identity, this PR introduces the notion of a *tactic alternative*, which is a `syntax` specification that is really "the same as" an existing tactic, but needs to be separate for technical reasons. This provides a notion of tactic identity, which we can use as the basis of a tactic index in generated documentation. Alternative forms of tactics are specified using a new `@[tactic_alt IDENT]` attribute, applied to the new tactic syntax. It is an error to declare a tactic syntax rule to be an alternative of another one that is itself an alternative. Documentation hovers now take alternatives into account, and display the docs for the canonical name. *Tactic tags*, created with the `register_tactic_tag` command, specify tags that may be applied to tactics. This is intended to be used by doc-gen and Verso. Tags may be applied using the `@[tactic_tag TAG1 TAG2 ...]` attribute on a canonical tactic parser, which may be used in any module to facilitate downstream projects introducing tags that apply to pre-existing tactics. Tags may not be removed, but it's fine to redundantly add them. The collection of tags, and the tactics to which they're applied, can be seen using the `#print tactic tags` command. *Extension documentation* provides a structured way to document extensions to tactics. The resulting documentation is gathered into a bulleted list at the bottom of the tactic's docstring. Extensions are added using the `tactic_extension TAC` command. This can be used when adding new interpretations of a tactic via `macro_rules`, when extending some table or search index used by the tactic, or in any other way. It is a command to facilitate its flexible use with various extension mechanisms.
127 lines
7.6 KiB
Text
127 lines
7.6 KiB
Text
/-
|
|
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura, Sebastian Ullrich
|
|
-/
|
|
prelude
|
|
import Lean.Parser.Basic
|
|
import Lean.Parser.Level
|
|
import Lean.Parser.Term
|
|
import Lean.Parser.Tactic
|
|
import Lean.Parser.Command
|
|
import Lean.Parser.Module
|
|
import Lean.Parser.Syntax
|
|
import Lean.Parser.Do
|
|
import Lean.Parser.Tactic.Doc
|
|
|
|
namespace Lean
|
|
namespace Parser
|
|
open Lean.PrettyPrinter
|
|
open Lean.PrettyPrinter.Parenthesizer
|
|
open Lean.PrettyPrinter.Formatter
|
|
|
|
builtin_initialize
|
|
register_parser_alias "ws" checkWsBefore { stackSz? := some 0 }
|
|
register_parser_alias "noWs" checkNoWsBefore { stackSz? := some 0 }
|
|
register_parser_alias "linebreak" checkLinebreakBefore { stackSz? := some 0 }
|
|
register_parser_alias (kind := numLitKind) "num" numLit
|
|
register_parser_alias (kind := strLitKind) "str" strLit
|
|
register_parser_alias (kind := charLitKind) "char" charLit
|
|
register_parser_alias (kind := nameLitKind) "name" nameLit
|
|
register_parser_alias (kind := scientificLitKind) "scientific" scientificLit
|
|
register_parser_alias (kind := identKind) ident
|
|
register_parser_alias (kind := hygieneInfoKind) hygieneInfo
|
|
register_parser_alias "colGt" checkColGt { stackSz? := some 0 }
|
|
register_parser_alias "colGe" checkColGe { stackSz? := some 0 }
|
|
register_parser_alias "colEq" checkColEq { stackSz? := some 0 }
|
|
register_parser_alias "lineEq" checkLineEq { stackSz? := some 0 }
|
|
register_parser_alias lookahead { stackSz? := some 0 }
|
|
register_parser_alias atomic { stackSz? := none }
|
|
register_parser_alias many
|
|
register_parser_alias many1
|
|
register_parser_alias manyIndent
|
|
register_parser_alias many1Indent
|
|
register_parser_alias optional { autoGroupArgs := false }
|
|
register_parser_alias withPosition { stackSz? := none }
|
|
register_parser_alias withoutPosition { stackSz? := none }
|
|
register_parser_alias withoutForbidden { stackSz? := none }
|
|
register_parser_alias (kind := interpolatedStrKind) interpolatedStr
|
|
register_parser_alias orelse
|
|
register_parser_alias andthen { stackSz? := none }
|
|
register_parser_alias recover
|
|
|
|
registerAlias `notFollowedBy ``notFollowedBy (notFollowedBy · "element")
|
|
Parenthesizer.registerAlias `notFollowedBy notFollowedBy.parenthesizer
|
|
Formatter.registerAlias `notFollowedBy notFollowedBy.formatter
|
|
|
|
end Parser
|
|
|
|
namespace PrettyPrinter
|
|
namespace Parenthesizer
|
|
|
|
-- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
|
|
@[export lean_mk_antiquot_parenthesizer]
|
|
def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Parenthesizer :=
|
|
Parser.mkAntiquot.parenthesizer name kind anonymous isPseudoKind
|
|
|
|
-- The parenthesizer auto-generated these instances correctly, but tagged them with the wrong kind, since the actual kind
|
|
-- (e.g. `ident`) is not equal to the parser name `Lean.Parser.Term.ident`.
|
|
@[builtin_parenthesizer ident] def ident.parenthesizer : Parenthesizer := Parser.Term.ident.parenthesizer
|
|
@[builtin_parenthesizer num] def numLit.parenthesizer : Parenthesizer := Parser.Term.num.parenthesizer
|
|
@[builtin_parenthesizer scientific] def scientificLit.parenthesizer : Parenthesizer := Parser.Term.scientific.parenthesizer
|
|
@[builtin_parenthesizer char] def charLit.parenthesizer : Parenthesizer := Parser.Term.char.parenthesizer
|
|
@[builtin_parenthesizer str] def strLit.parenthesizer : Parenthesizer := Parser.Term.str.parenthesizer
|
|
|
|
open Lean.Parser
|
|
|
|
@[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
|
|
unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
|
|
| ParserDescr.const n => getConstAlias parenthesizerAliasesRef n
|
|
| ParserDescr.unary n d => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d)
|
|
| ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
|
|
| ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d)
|
|
| ParserDescr.nodeWithAntiquot n k d => return withAntiquot.parenthesizer (mkAntiquot.parenthesizer' n k (anonymous := true)) <|
|
|
node.parenthesizer k (← interpretParserDescr d)
|
|
| ParserDescr.sepBy p sep psep trail => return sepBy.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
|
|
| ParserDescr.sepBy1 p sep psep trail => return sepBy1.parenthesizer (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
|
|
| ParserDescr.trailingNode k prec lhsPrec d => return trailingNode.parenthesizer k prec lhsPrec (← interpretParserDescr d)
|
|
| ParserDescr.symbol tk => return symbol.parenthesizer tk
|
|
| ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.parenthesizer tk includeIdent
|
|
| ParserDescr.parser constName => combinatorParenthesizerAttribute.runDeclFor constName
|
|
| ParserDescr.cat catName prec => return categoryParser.parenthesizer catName prec
|
|
|
|
end Parenthesizer
|
|
|
|
namespace Formatter
|
|
|
|
@[export lean_mk_antiquot_formatter]
|
|
def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Formatter :=
|
|
Parser.mkAntiquot.formatter name kind anonymous isPseudoKind
|
|
|
|
@[builtin_formatter ident] def ident.formatter : Formatter := Parser.Term.ident.formatter
|
|
@[builtin_formatter num] def numLit.formatter : Formatter := Parser.Term.num.formatter
|
|
@[builtin_formatter scientific] def scientificLit.formatter : Formatter := Parser.Term.scientific.formatter
|
|
@[builtin_formatter char] def charLit.formatter : Formatter := Parser.Term.char.formatter
|
|
@[builtin_formatter str] def strLit.formatter : Formatter := Parser.Term.str.formatter
|
|
|
|
open Lean.Parser
|
|
|
|
@[export lean_pretty_printer_formatter_interpret_parser_descr]
|
|
unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
|
|
| ParserDescr.const n => getConstAlias formatterAliasesRef n
|
|
| ParserDescr.unary n d => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d)
|
|
| ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂)
|
|
| ParserDescr.node k _ d => return node.formatter k (← interpretParserDescr d)
|
|
| ParserDescr.nodeWithAntiquot n k d => return withAntiquot.formatter (mkAntiquot.formatter' n k (anonymous := true)) <|
|
|
node.formatter k (← interpretParserDescr d)
|
|
| ParserDescr.sepBy p sep psep trail => return sepBy.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
|
|
| ParserDescr.sepBy1 p sep psep trail => return sepBy1.formatter (← interpretParserDescr p) sep (← interpretParserDescr psep) trail
|
|
| ParserDescr.trailingNode k prec lhsPrec d => return trailingNode.formatter k prec lhsPrec (← interpretParserDescr d)
|
|
| ParserDescr.symbol tk => return symbol.formatter tk
|
|
| ParserDescr.nonReservedSymbol tk _ => return nonReservedSymbol.formatter tk
|
|
| ParserDescr.parser constName => combinatorFormatterAttribute.runDeclFor constName
|
|
| ParserDescr.cat catName _ => return categoryParser.formatter catName
|
|
|
|
end Formatter
|
|
end PrettyPrinter
|
|
end Lean
|