Extensible parsing via attributes

source
opaque Lean.Parser.builtinTokenTable :
IO.Ref TokenTable
source
opaque Lean.Parser.builtinSyntaxNodeKindSetRef :
IO.Ref SyntaxNodeKindSet
source
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

Instances For

source
opaque Lean.Parser.builtinParserCategoriesRef :
IO.Ref ParserCategories
source
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

Instances For

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

- Lean.Parser.ParserExtension.instInhabitedOLeanEntry = { default := Lean.Parser.ParserExtension.instInhabitedOLeanEntry.default }

source
def Lean.Parser.ParserExtension.instInhabitedOLeanEntry.default :
OLeanEntry
Equations

- Lean.Parser.ParserExtension.instInhabitedOLeanEntry.default = Lean.Parser.ParserExtension.OLeanEntry.token default

Instances For

source
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

Instances For

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

- Lean.Parser.ParserExtension.instInhabitedEntry = { default := Lean.Parser.ParserExtension.instInhabitedEntry.default }

source
def Lean.Parser.ParserExtension.instInhabitedEntry.default :
Entry
Equations

- Lean.Parser.ParserExtension.instInhabitedEntry.default = Lean.Parser.ParserExtension.Entry.token default

Instances For

source
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

Instances For

source
structure Lean.Parser.ParserExtension.State :
Type

- tokens : TokenTable
- kinds : SyntaxNodeKindSet
- categories : ParserCategories

Instances For

source
def Lean.Parser.ParserExtension.instInhabitedState.default :
State
Equations

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

Instances For

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

- Lean.Parser.ParserExtension.instInhabitedState = { default := Lean.Parser.ParserExtension.instInhabitedState.default }

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

Instances For

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

- Lean.Parser.throwUnknownParserCategory catName = throw (toString "unknown parser category `" ++ toString catName ++ toString "`")

Instances For

source
@[reducible, inline]
abbrev Lean.Parser.getCategory (categories : ParserCategories) (catName : Name) :
Option ParserCategory
Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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 [])

Instances For

source
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 }

Instances For

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

Parser aliases for making `ParserDescr` extensible

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

Instances For

source
@[reducible, inline]
abbrev Lean.Parser.AliasTable (α : Type) :
Type
Equations

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

Instances For

source
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.

Instances For

source
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)

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[reducible, inline]
abbrev Lean.Parser.ParserAliasValue :
Type
Equations

- Lean.Parser.ParserAliasValue = Lean.Parser.AliasValue Lean.Parser.Parser

Instances For

source
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.

Instances For

source
opaque Lean.Parser.parserAliasesRef :
IO.Ref (NameMap ParserAliasValue)
source
opaque Lean.Parser.parserAlias2kindRef :
IO.Ref (NameMap SyntaxNodeKind)
source
opaque Lean.Parser.parserAliases2infoRef :
IO.Ref (NameMap ParserAliasInfo)
source
def Lean.Parser.getParserAliasInfo (aliasName : Name) :
IO ParserAliasInfo
Equations

- Lean.Parser.getParserAliasInfo aliasName = do let __do_lift ← ST.Ref.get Lean.Parser.parserAliases2infoRef pure (Std.TreeMap.getD __do_lift aliasName { })

Instances For

source
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.

Instances For

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

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

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

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

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

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

source
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

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

source
@[implemented_by Lean.Parser.mkParserOfConstantUnsafe]
opaque Lean.Parser.mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) :
ImportM (Bool × Parser)
source
def Lean.Parser.compileParserDescr (categories : ParserCategories) (d : ParserDescr) :
ImportM Parser
Equations

- Lean.Parser.compileParserDescr categories d = Lean.Parser.compileParserDescr.visit✝ categories d

Instances For

source
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)

Instances For

source
structure Lean.Parser.ParserAttributeHook :
Type

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

  Called after a parser attribute is applied to a declaration.

Instances For

source
opaque Lean.Parser.parserAttributeHooks :
IO.Ref (List ParserAttributeHook)
source
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

Instances For

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

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

Instances For

source
opaque Lean.Parser.parserExtension :
ParserExtension
source
def Lean.Parser.getParserCategory? (env : Environment) (catName : Name) :
Option ParserCategory
Equations

- Lean.Parser.getParserCategory? env catName = Lean.PersistentHashMap.find? (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).categories catName

Instances For

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

- Lean.Parser.isParserCategory env catName = (Lean.Parser.getParserCategory? env catName).isSome

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

source
@[implemented_by Lean.Parser.evalParserConstUnsafe]
opaque Lean.Parser.evalParserConst (declName : Name) :
ParserFn
source
opaque Lean.Parser.internal.parseQuotWithCurrentStage :
Lean.Option Bool
source
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`.

Equations

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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Parser.mkInputContext (input fileName : String) (normalizeLineEndings : Bool := true) (endPos : String.Pos.Raw := input.endPos) (endPos_valid : endPos ≤ input.endPos := by simp) :
InputContext
Equations

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

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

source
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")

Instances For

source
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.

Instances For

source
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)

Instances For

source
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.

Instances For

source
@[inline]
def Lean.Parser.commandParser (rbp : Nat := 0) :
Parser
Equations

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

Instances For

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

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

Instances For

source
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.

Instances For

source
@[inline]
def Lean.Parser.withOpen :
Parser → Parser
Equations

- Lean.Parser.withOpen = Lean.Parser.withFn Lean.Parser.withOpenFn

Instances For

source
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 have stx := s.stxStack.back; Lean.Parser.withOpenDeclFnCore stx p c s else p c s

Instances For

source
@[inline]
def Lean.Parser.withOpenDecl :
Parser → Parser
Equations

- Lean.Parser.withOpenDecl = Lean.Parser.withFn Lean.Parser.withOpenDeclFn

Instances For

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

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

source
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).

Instances For

source
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.options ctx.currNamespace ctx.openDecls id

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For