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

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 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: Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → Lean.Parser.ParserExtension.OLeanEntry
• parser: Lean.Name → Lean.Name → Nat → Lean.Parser.ParserExtension.OLeanEntry

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

Equations

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

inductive Lean.Parser.ParserExtension.Entry : Type

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

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

Equations

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

def Lean.Parser.ParserExtension.Entry.toOLeanEntry : Lean.Parser.ParserExtension.Entry → Lean.Parser.ParserExtension.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 : Lean.Parser.TokenTable
• kinds : Lean.Parser.SyntaxNodeKindSet
• categories : Lean.Parser.ParserCategories

instance Lean.Parser.ParserExtension.instInhabitedState : Inhabited Lean.Parser.ParserExtension.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 : Lean.Name) : ExceptT String Id α

@[reducible, inline]

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

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

Equations

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

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

Equations

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

def Lean.Parser.addParser (categories : Lean.Parser.ParserCategories) (catName declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : Nat) : Except String Lean.Parser.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 : 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

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} → α → Lean.Parser.AliasValue α
• unary: {α : Type} → (α → α) → Lean.Parser.AliasValue α
• binary: {α : Type} → (α → α → α) → Lean.Parser.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 (Lean.Parser.AliasTable α)) (aliasName : Lean.Name) (value : Lean.Parser.AliasValue α) : IO Unit

def Lean.Parser.getAlias {α : Type} (mapRef : IO.Ref (Lean.Parser.AliasTable α)) (aliasName : Lean.Name) : IO (Option (Lean.Parser.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 (Lean.Parser.AliasTable α)) (aliasName : Lean.Name) : IO α

Equations

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

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

Equations

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

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

@[reducible, inline]

abbrev Lean.Parser.ParserAliasValue : Type

structure Lean.Parser.ParserAliasInfo : Type

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.isParserAlias (aliasName : Lean.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 : Lean.Name) : IO (Option Lean.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 : Lean.Name) : IO Unit

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

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

unsafe def Lean.Parser.mkParserOfConstantUnsafe (constName : Lean.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 : Lean.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

Equations

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

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 : Lean.Name) : Lean.ImportM (Bool × Lean.Parser.Parser)

structure Lean.Parser.ParserAttributeHook : Type

• postAdd : Lean.Name → Lean.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

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 : Lean.Name) (builtin : Bool) : Lean.AttrM Unit

Equations

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

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

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

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

Equations

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

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

Equations

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

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

@[implemented_by Lean.Parser.evalParserConstUnsafe]

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

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

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

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

def Lean.Parser.addBuiltinTrailingParser (catName declName : Lean.Name) (p : Lean.Parser.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 : Lean.Name) : Lean.Parser.Parser

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

def Lean.Parser.runParserCategory (env : Lean.Environment) (catName : Lean.Name) (input : String) (fileName : String := "<input>") : Except String Lean.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 : Lean.Name) (prio : Nat) : Lean.CoreM Unit

Equations

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

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

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

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

Equations

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

def Lean.Parser.registerBuiltinParserAttribute (attrName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior := Lean.Parser.LeadingIdentBehavior.default) (ref : Lean.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 : Lean.Name) (ref : Lean.Name := by exact decl_name%) : Lean.AttributeImpl

def Lean.Parser.registerBuiltinDynamicParserAttribute (attrName catName : Lean.Name) (ref : Lean.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 : Lean.Environment) (attrName catName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior := Lean.Parser.LeadingIdentBehavior.default) (ref : Lean.Name := by exact decl_name%) : IO Lean.Environment

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

opaque Lean.Parser.aliasExtension : Lean.EnvExtension (Lean.NameMap Lean.Parser.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: Lean.Name → Lean.Parser.ParserResolution

  Reference to a category.

• parser: Lean.Name → Bool → Lean.Parser.ParserResolution

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

• alias: Lean.Parser.ParserAliasValue → Lean.Parser.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 : Lean.Environment) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (ident : Lean.Ident) : List Lean.Parser.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 : Lean.Environment) (name : Lean.Name) : Option Bool

Equations

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

def Lean.Parser.ParserContext.resolveParserName (ctx : Lean.Parser.ParserContext) (id : Lean.Ident) : List Lean.Parser.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 : Lean.Ident) : Lean.CoreM (List Lean.Parser.ParserResolution)

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

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

Equations

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

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

Equations

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