Extensible parsing via attributes

opaque Lean.Parser.builtinTokenTable : IO.Ref TokenTable

opaque Lean.Parser.builtinSyntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet

def Lean.Parser.registerBuiltinNodeKind (k : SyntaxNodeKind) : IO Unit

opaque Lean.Parser.builtinParserCategoriesRef : IO.Ref ParserCategories

inductive Lean.Parser.ParserExtension.OLeanEntry : Type

• token (val : Token) : OLeanEntry
• kind (val : SyntaxNodeKind) : OLeanEntry
• category (catName declName : Name) (behavior : LeadingIdentBehavior) : OLeanEntry
• parser (catName declName : Name) (prio : Nat) : OLeanEntry

instance Lean.Parser.ParserExtension.instInhabitedOLeanEntry : Inhabited OLeanEntry

inductive Lean.Parser.ParserExtension.Entry : Type

• token (val : Token) : Entry
• kind (val : SyntaxNodeKind) : Entry
• category (catName declName : Name) (behavior : LeadingIdentBehavior) : Entry
• parser (catName declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Entry

instance Lean.Parser.ParserExtension.instInhabitedEntry : Inhabited Entry

def Lean.Parser.ParserExtension.Entry.toOLeanEntry : Entry → OLeanEntry

structure Lean.Parser.ParserExtension.State : Type

• tokens : TokenTable
• kinds : SyntaxNodeKindSet
• categories : ParserCategories

instance Lean.Parser.ParserExtension.instInhabitedState : Inhabited State

@[reducible, inline]

abbrev Lean.Parser.ParserExtension : Type

def Lean.Parser.throwUnknownParserCategory {α : Type} (catName : Name) : ExceptT String Id α

@[reducible, inline]

abbrev Lean.Parser.getCategory (categories : ParserCategories) (catName : Name) : Option ParserCategory

def Lean.Parser.addLeadingParser (categories : ParserCategories) (catName declName : Name) (p : Parser) (prio : Nat) : Except String ParserCategories

def Lean.Parser.addTrailingParser (categories : ParserCategories) (catName declName : Name) (p : TrailingParser) (prio : Nat) : Except String ParserCategories

def Lean.Parser.addParser (categories : ParserCategories) (catName declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : Except String ParserCategories

def Lean.Parser.addParserTokens (tokenTable : TokenTable) (info : ParserInfo) : Except String TokenTable

def Lean.Parser.ParserExtension.addEntryImpl (s : State) (e : Entry) : State

inductive Lean.Parser.AliasValue (α : Type) : Type

Parser aliases for making ParserDescr extensible

• const {α : Type} (p : α) : AliasValue α
• unary {α : Type} (p : α → α) : AliasValue α
• binary {α : Type} (p : α → α → α) : AliasValue α

@[reducible, inline]

abbrev Lean.Parser.AliasTable (α : Type) : Type

def Lean.Parser.registerAliasCore {α : Type} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit

def Lean.Parser.getAlias {α : Type} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : IO (Option (AliasValue α))

def Lean.Parser.getConstAlias {α : Type} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : IO α

def Lean.Parser.getUnaryAlias {α : Type} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : IO (α → α)

def Lean.Parser.getBinaryAlias {α : Type} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : IO (α → α → α)

@[reducible, inline]

abbrev Lean.Parser.ParserAliasValue : Type

structure Lean.Parser.ParserAliasInfo : Type

• declName : Name
• stackSz? : Option Nat

  Number of syntax nodes produced by this parser. none means "sum of input sizes".

• autoGroupArgs : Bool

  Whether arguments should be wrapped in group(·) if they do not produce exactly one syntax node.

opaque Lean.Parser.parserAliasesRef : IO.Ref (NameMap ParserAliasValue)

opaque Lean.Parser.parserAlias2kindRef : IO.Ref (NameMap SyntaxNodeKind)

opaque Lean.Parser.parserAliases2infoRef : IO.Ref (NameMap ParserAliasInfo)

def Lean.Parser.getParserAliasInfo (aliasName : Name) : IO ParserAliasInfo

def Lean.Parser.registerAlias (aliasName declName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := { }) : IO Unit

instance Lean.Parser.instCoeParserParserAliasValue : Coe Parser ParserAliasValue

instance Lean.Parser.instCoeForallParserParserAliasValue : Coe (Parser → Parser) ParserAliasValue

instance Lean.Parser.instCoeForallParserForallParserAliasValue : Coe (Parser → Parser → Parser) ParserAliasValue

def Lean.Parser.isParserAlias (aliasName : Name) : IO Bool

def Lean.Parser.getSyntaxKindOfParserAlias? (aliasName : Name) : IO (Option SyntaxNodeKind)

def Lean.Parser.ensureUnaryParserAlias (aliasName : Name) : IO Unit

def Lean.Parser.ensureBinaryParserAlias (aliasName : Name) : IO Unit

def Lean.Parser.ensureConstantParserAlias (aliasName : Name) : IO Unit

unsafe def Lean.Parser.mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)

@[implemented_by Lean.Parser.mkParserOfConstantUnsafe]

opaque Lean.Parser.mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)

def Lean.Parser.compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser

partial def Lean.Parser.compileParserDescr.visit (categories : ParserCategories) : ParserDescr → ImportM Parser

def Lean.Parser.mkParserOfConstant (categories : ParserCategories) (constName : Name) : ImportM (Bool × Parser)

structure Lean.Parser.ParserAttributeHook : Type

• postAdd (catName declName : Name) (builtin : Bool) : AttrM Unit

  Called after a parser attribute is applied to a declaration.

opaque Lean.Parser.parserAttributeHooks : IO.Ref (List ParserAttributeHook)

def Lean.Parser.registerParserAttributeHook (hook : ParserAttributeHook) : IO Unit

def Lean.Parser.runParserAttributeHooks (catName declName : Name) (builtin : Bool) : AttrM Unit

opaque Lean.Parser.parserExtension : ParserExtension

def Lean.Parser.isParserCategory (env : Environment) (catName : Name) : Bool

def Lean.Parser.addParserCategory (env : Environment) (catName declName : Name) (behavior : LeadingIdentBehavior) : Except String Environment

def Lean.Parser.leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBehavior

unsafe def Lean.Parser.evalParserConstUnsafe (declName : Name) : ParserFn

@[implemented_by Lean.Parser.evalParserConstUnsafe]

opaque Lean.Parser.evalParserConst (declName : Name) : ParserFn

opaque Lean.Parser.internal.parseQuotWithCurrentStage : Lean.Option Bool

def Lean.Parser.evalInsideQuot (declName : Name) : Parser → Parser

Run declName if possible and inside a quotation, or else p. The ParserInfo will always be taken from p.

def Lean.Parser.addBuiltinParser (catName declName : Name) (leading : Bool) (p : Parser) (prio : Nat) : IO Unit

def Lean.Parser.addBuiltinLeadingParser (catName declName : Name) (p : Parser) (prio : Nat) : IO Unit

def Lean.Parser.addBuiltinTrailingParser (catName declName : Name) (p : TrailingParser) (prio : Nat) : IO Unit

def Lean.Parser.mkCategoryAntiquotParser (kind : Name) : Parser

def Lean.Parser.categoryParserFnImpl (catName : Name) : ParserFn

def Lean.Parser.addToken (tk : Token) (kind : AttributeKind) : AttrM Unit

def Lean.Parser.addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment

def Lean.Parser.isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool

def Lean.Parser.getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind

def Lean.Parser.getTokenTable (env : Environment) : TokenTable

def Lean.Parser.mkInputContext (input fileName : String) (normalizeLineEndings : Bool := true) : InputContext

def Lean.Parser.mkParserState (input : String) : ParserState

def Lean.Parser.runParserCategory (env : Environment) (catName : Name) (input : String) (fileName : String := "<input>") : Except String Syntax

convenience function for testing

def Lean.Parser.declareBuiltinParser (addFnName catName declName : Name) (prio : Nat) : CoreM Unit

def Lean.Parser.declareLeadingBuiltinParser (catName declName : Name) (prio : Nat) : CoreM Unit

def Lean.Parser.declareTrailingBuiltinParser (catName declName : Name) (prio : Nat) : CoreM Unit

def Lean.Parser.getParserPriority (args : Syntax) : Except String Nat

def Lean.Parser.registerBuiltinParserAttribute (attrName declName : Name) (behavior : LeadingIdentBehavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Unit

The parsing tables for builtin parsers are "stored" in the extracted source code.

def Lean.Parser.mkParserAttributeImpl (attrName catName : Name) (ref : Name := by exact decl_name%) : AttributeImpl

def Lean.Parser.registerBuiltinDynamicParserAttribute (attrName catName : Name) (ref : Name := by exact decl_name%) : IO Unit

A builtin parser attribute that can be extended by users.

def Lean.Parser.registerParserCategory (env : Environment) (attrName catName : Name) (behavior : LeadingIdentBehavior := LeadingIdentBehavior.default) (ref : Name := by exact decl_name%) : IO Environment

@[inline]

def Lean.Parser.commandParser (rbp : Nat := 0) : Parser

def Lean.Parser.withOpenDeclFnCore (openDeclStx : Syntax) (p : ParserFn) : ParserFn

def Lean.Parser.withOpenFn (p : ParserFn) : ParserFn

If the parsing stack is of the form #[.., openCommand], we process the open command, and execute p

@[inline]

def Lean.Parser.withOpen : Parser → Parser

def Lean.Parser.withOpenDeclFn (p : ParserFn) : ParserFn

If the parsing stack is of the form #[.., openDecl], we process the open declaration, and execute p

@[inline]

def Lean.Parser.withOpenDecl : Parser → Parser

opaque Lean.Parser.aliasExtension : EnvExtension (NameMap ParserAliasValue)

Helper environment extension that gives us access to built-in aliases in pure parser functions.

inductive Lean.Parser.ParserResolution : Type

Result of resolving a parser name.

• category (cat : Name) : ParserResolution

  Reference to a category.

• parser (decl : Name) (isDescr : Bool) : ParserResolution

  Reference to a parser declaration in the environment. A (Trailing)ParserDescr if isDescr is true.

• alias (p : ParserAliasValue) : ParserResolution

  Reference to a parser alias. Note that as aliases are built-in, a corresponding declaration may not be in the environment (yet).

def Lean.Parser.resolveParserNameCore (env : Environment) (currNamespace : Name) (openDecls : List OpenDecl) (ident : Ident) : List ParserResolution

Resolve the given parser name and return a list of candidates.

def Lean.Parser.resolveParserNameCore.isParser (env : Environment) (name : Name) : Option Bool

def Lean.Parser.ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserResolution

Resolve the given parser name and return a list of candidates.

def Lean.Parser.resolveParserName (id : Ident) : CoreM (List ParserResolution)

Resolve the given parser name and return a list of candidates.

def Lean.Parser.parserOfStackFn (offset : Nat) : ParserFn

def Lean.Parser.parserOfStack (offset : Nat) (prec : Nat := 0) : Parser