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_reducible]

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_reducible]

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_reducible]

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_reducible]

instance Lean.Parser.instCoeParserParserAliasValue : Coe Parser ParserAliasValue

@[instance_reducible]

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

@[instance_reducible]

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

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.getParserCategory? (env : Environment) (catName : Name) : Option ParserCategory

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) (evalFallback? : Option ParserFn := none) : ParserFn

@[implemented_by Lean.Parser.evalParserConstUnsafe]

opaque Lean.Parser.evalParserConst (declName : Name) (evalFallback? : Option ParserFn := none) : ParserFn

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

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

Interpret declName if possible and inside a quotation, or else run 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) (endPos : String.Pos.Raw := input.rawEndPos) (endPos_valid : endPos ≤ input.rawEndPos := by simp) : 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

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

If the parsing stack's last element is a set_option command, then its value is set in the context while parsing p.

@[inline]

def Lean.Parser.withSetOption : Parser → Parser

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

If the parsing stack ends with an the option name and value, then the option is set in the context while parsing p. The value is the top of the stack and the name is the identifier two entries below it.

@[inline]

def Lean.Parser.withSetOptionValue : 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.ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) (unsetExporting : Bool := false) : 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