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

Equations

• Lean.Parser.registerBuiltinNodeKind k = ST.Ref.modify Lean.Parser.builtinSyntaxNodeKindSetRef fun (s : Lean.Parser.SyntaxNodeKindSet) => s.insert k

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

Equations

• Lean.Parser.ParserExtension.instInhabitedOLeanEntry = { default := Lean.Parser.ParserExtension.OLeanEntry.token default }

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

Equations

• Lean.Parser.ParserExtension.instInhabitedEntry = { default := Lean.Parser.ParserExtension.Entry.token default }

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

Equations

• (Lean.Parser.ParserExtension.Entry.token v).toOLeanEntry = Lean.Parser.ParserExtension.OLeanEntry.token v
• (Lean.Parser.ParserExtension.Entry.kind v).toOLeanEntry = Lean.Parser.ParserExtension.OLeanEntry.kind v
• (Lean.Parser.ParserExtension.Entry.category c d b).toOLeanEntry = Lean.Parser.ParserExtension.OLeanEntry.category c d b
• (Lean.Parser.ParserExtension.Entry.parser c d leading p prio).toOLeanEntry = Lean.Parser.ParserExtension.OLeanEntry.parser c d prio

structure Lean.Parser.ParserExtension.State : Type

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

instance Lean.Parser.ParserExtension.instInhabitedState : Inhabited State

Equations

• Lean.Parser.ParserExtension.instInhabitedState = { default := { tokens := default, kinds := default, categories := default } }

@[reducible, inline]

abbrev Lean.Parser.ParserExtension : Type

Equations

• Lean.Parser.ParserExtension = Lean.ScopedEnvExtension Lean.Parser.ParserExtension.OLeanEntry Lean.Parser.ParserExtension.Entry Lean.Parser.ParserExtension.State

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

Equations

• Lean.Parser.throwUnknownParserCategory catName = throw (toString "unknown parser category '" ++ toString catName ++ toString "'")

@[reducible, inline]

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

Equations

• Lean.Parser.getCategory categories catName = Lean.PersistentHashMap.find? categories catName

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.addParser categories catName declName true p prio = Lean.Parser.addLeadingParser categories catName declName p prio
• Lean.Parser.addParser categories catName declName false p prio = Lean.Parser.addTrailingParser categories catName declName p prio

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

Equations

• Lean.Parser.addParserTokens tokenTable info = List.foldlM Lean.Parser.addTokenConfig✝ tokenTable (info.collectTokens [])

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.ParserExtension.addEntryImpl s (Lean.Parser.ParserExtension.Entry.kind v) = { tokens := s.tokens, kinds := s.kinds.insert v, categories := s.categories }

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

Equations

• Lean.Parser.AliasTable α = Lean.NameMap (Lean.Parser.AliasValue α)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.getAlias mapRef aliasName = do let __do_lift ← ST.Ref.get mapRef pure (Lean.NameMap.find? __do_lift aliasName)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Parser.ParserAliasValue : Type

Equations

• Lean.Parser.ParserAliasValue = Lean.Parser.AliasValue Lean.Parser.Parser

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

Equations

• Lean.Parser.getParserAliasInfo aliasName = do let __do_lift ← ST.Ref.get Lean.Parser.parserAliases2infoRef pure (Lean.RBMap.findD __do_lift aliasName { })

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

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Parser.instCoeParserParserAliasValue : Coe Parser ParserAliasValue

Equations

• Lean.Parser.instCoeParserParserAliasValue = { coe := Lean.Parser.AliasValue.const }

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

Equations

• Lean.Parser.instCoeForallParserParserAliasValue = { coe := Lean.Parser.AliasValue.unary }

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

Equations

• Lean.Parser.instCoeForallParserForallParserAliasValue = { coe := Lean.Parser.AliasValue.binary }

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

Equations

• Lean.Parser.isParserAlias aliasName = do let __do_lift ← Lean.Parser.getAlias Lean.Parser.parserAliasesRef aliasName match __do_lift with | some val => pure true | x => pure false

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

Equations

• Lean.Parser.getSyntaxKindOfParserAlias? aliasName = do let __do_lift ← ST.Ref.get Lean.Parser.parserAlias2kindRef pure (__do_lift.find? aliasName)

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

Equations

• Lean.Parser.ensureUnaryParserAlias aliasName = discard (Lean.Parser.getUnaryAlias Lean.Parser.parserAliasesRef aliasName)

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

Equations

• Lean.Parser.ensureBinaryParserAlias aliasName = discard (Lean.Parser.getBinaryAlias Lean.Parser.parserAliasesRef aliasName)

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

Equations

• Lean.Parser.ensureConstantParserAlias aliasName = discard (Lean.Parser.getConstAlias Lean.Parser.parserAliasesRef aliasName)

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

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• Lean.Parser.compileParserDescr categories d = Lean.Parser.compileParserDescr.visit categories d

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

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

Equations

• Lean.Parser.mkParserOfConstant categories constName = Lean.Parser.mkParserOfConstantAux constName (Lean.Parser.compileParserDescr categories)

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

Equations

• Lean.Parser.registerParserAttributeHook hook = ST.Ref.modify Lean.Parser.parserAttributeHooks fun (hooks : List Lean.Parser.ParserAttributeHook) => hook :: hooks

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

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Parser.parserExtension : ParserExtension

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

Equations

• Lean.Parser.isParserCategory env catName = Lean.PersistentHashMap.contains (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).categories catName

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.addBuiltinLeadingParser catName declName p prio = Lean.Parser.addBuiltinParser catName declName true p prio

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

Equations

• Lean.Parser.addBuiltinTrailingParser catName declName p prio = Lean.Parser.addBuiltinParser catName declName false p prio

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

Equations

• Lean.Parser.mkCategoryAntiquotParser kind = Lean.Parser.mkAntiquot kind.toString kind true true

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.addSyntaxNodeKind env k = Lean.ScopedEnvExtension.addEntry Lean.Parser.parserExtension env (Lean.Parser.ParserExtension.Entry.kind k)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.getTokenTable env = (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).tokens

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.mkParserState input = { cache := Lean.Parser.initCacheForInput input }

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

convenience function for testing

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.declareLeadingBuiltinParser catName declName prio = Lean.Parser.declareBuiltinParser `Lean.Parser.addBuiltinLeadingParser catName declName prio

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

Equations

• Lean.Parser.declareTrailingBuiltinParser catName declName prio = Lean.Parser.declareBuiltinParser `Lean.Parser.addBuiltinTrailingParser catName declName prio

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.registerBuiltinParserAttribute attrName declName behavior ref = throw (IO.userError "`declName` should be in Lean.Parser.Category")

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Parser.registerBuiltinDynamicParserAttribute attrName catName ref = Lean.registerBuiltinAttribute (Lean.Parser.mkParserAttributeImpl attrName catName ref)

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

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

Equations

• Lean.Parser.commandParser rbp = Lean.Parser.categoryParser `command rbp

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lean.Parser.withOpen : Parser → Parser

Equations

• Lean.Parser.withOpen = Lean.Parser.withFn Lean.Parser.withOpenFn

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

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

Equations

• Lean.Parser.withOpenDeclFn p c s = if s.stxStack.size > 0 then let stx := s.stxStack.back; Lean.Parser.withOpenDeclFnCore stx p c s else p c s

@[inline]

def Lean.Parser.withOpenDecl : Parser → Parser

Equations

• Lean.Parser.withOpenDecl = Lean.Parser.withFn Lean.Parser.withOpenDeclFn

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.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.resolveParserNameCore env currNamespace openDecls ident = (pure []).run

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• ctx.resolveParserName id = Lean.Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.