Extensible parsing via attributes

opaque Lean.Parser.builtinTokenTable : IO.Ref Lean.Parser.TokenTable

opaque Lean.Parser.builtinSyntaxNodeKindSetRef : IO.Ref Lean.Parser.SyntaxNodeKindSet

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

opaque Lean.Parser.builtinParserCategoriesRef : IO.Ref Lean.Parser.ParserCategories

inductive Lean.Parser.ParserExtension.OLeanEntry : Type

• token: Lean.Parser.Token → Lean.Parser.ParserExtension.OLeanEntry
• kind: Lean.SyntaxNodeKind → Lean.Parser.ParserExtension.OLeanEntry
• category: Lake.Name → Lake.Name → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserExtension.OLeanEntry
• parser: Lake.Name → Lake.Name → Nat → Lean.Parser.ParserExtension.OLeanEntry

instance Lean.Parser.ParserExtension.instInhabitedOLeanEntry : Inhabited Lean.Parser.ParserExtension.OLeanEntry

inductive Lean.Parser.ParserExtension.Entry : Type

• token: Lean.Parser.Token → Lean.Parser.ParserExtension.Entry
• kind: Lean.SyntaxNodeKind → Lean.Parser.ParserExtension.Entry
• category: Lake.Name → Lake.Name → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserExtension.Entry
• parser: Lake.Name → Lake.Name → Bool → Lean.Parser.Parser → Nat → Lean.Parser.ParserExtension.Entry

instance Lean.Parser.ParserExtension.instInhabitedEntry : Inhabited Lean.Parser.ParserExtension.Entry

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

structure Lean.Parser.ParserExtension.State : Type

• tokens : Lean.Parser.TokenTable
• kinds : Lean.Parser.SyntaxNodeKindSet
• categories : Lean.Parser.ParserCategories

instance Lean.Parser.ParserExtension.instInhabitedState : Inhabited Lean.Parser.ParserExtension.State

@[inline, reducible]

abbrev Lean.Parser.ParserExtension : Type

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

@[inline, reducible]

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

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

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

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

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

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

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

• const: {α : Type} → α → Lean.Parser.AliasValue α
• unary: {α : Type} → (α → α) → Lean.Parser.AliasValue α
• binary: {α : Type} → (α → α → α) → Lean.Parser.AliasValue α

Parser aliases for making ParserDescr extensible

@[inline, reducible]

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

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

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

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

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

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

@[inline, reducible]

abbrev Lean.Parser.ParserAliasValue : Type

structure Lean.Parser.ParserAliasInfo : Type

• declName : Lake.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 (Lake.NameMap Lean.Parser.ParserAliasValue)

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

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

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

def Lean.Parser.registerAlias (aliasName : Lake.Name) (declName : Lake.Name) (p : Lean.Parser.ParserAliasValue) (kind? : optParam (Option Lean.SyntaxNodeKind) none) (info : optParam Lean.Parser.ParserAliasInfo { declName := Lean.Name.anonymous, stackSz? := some 1, autoGroupArgs := Option.isSome (some 1) }) : IO Unit

instance Lean.Parser.instCoeParserParserAliasValue : Coe Lean.Parser.Parser Lean.Parser.ParserAliasValue

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

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

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

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

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

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

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

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

@[implemented_by Lean.Parser.mkParserOfConstantUnsafe]

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

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

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

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

structure Lean.Parser.ParserAttributeHook : Type

• postAdd : Lake.Name → Lake.Name → Bool → Lean.AttrM Unit

  Called after a parser attribute is applied to a declaration.

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

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

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

opaque Lean.Parser.parserExtension : Lean.Parser.ParserExtension

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

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

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

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

@[implemented_by Lean.Parser.evalParserConstUnsafe]

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

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

def Lean.Parser.evalInsideQuot (declName : Lake.Name) : Lean.Parser.Parser → Lean.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 : Lake.Name) (declName : Lake.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : Nat) : IO Unit

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

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

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

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

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

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

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

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

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

def Lean.Parser.mkInputContext (input : String) (fileName : String) : Lean.Parser.InputContext

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

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

convenience function for testing

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

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

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

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

def Lean.Parser.registerBuiltinParserAttribute (attrName : Lake.Name) (declName : Lake.Name) (behavior : optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default) : IO Unit

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

def Lean.Parser.mkParserAttributeImpl (attrName : Lake.Name) (catName : Lake.Name) (ref : autoParam Lake.Name _auto✝) : Lean.AttributeImpl

def Lean.Parser.registerBuiltinDynamicParserAttribute (attrName : Lake.Name) (catName : Lake.Name) (ref : autoParam Lake.Name _auto✝) : IO Unit

A builtin parser attribute that can be extended by users.

def Lean.Parser.registerParserCategory (env : Lean.Environment) (attrName : Lake.Name) (catName : Lake.Name) (behavior : optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default) (ref : autoParam Lake.Name _auto✝) : IO Lean.Environment

@[inline]

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

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

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

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

@[inline]

def Lean.Parser.withOpen : Lean.Parser.Parser → Lean.Parser.Parser

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

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

@[inline]

def Lean.Parser.withOpenDecl : Lean.Parser.Parser → Lean.Parser.Parser

inductive Lean.Parser.ParserName : Type

• category: Lake.Name → Lean.Parser.ParserName
• parser: Lake.Name → Bool → Lean.Parser.ParserName

instance Lean.Parser.instReprParserName : Repr Lean.Parser.ParserName

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

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

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

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

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

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

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

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

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