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: 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

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: 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

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

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

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 : Lake.Name) : ExceptT String Id α

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.addParserTokens tokenTable info = let newTokens := info.collectTokens []; List.foldlM Lean.Parser.addTokenConfig tokenTable newTokens

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.

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 α = Lake.NameMap (Lean.Parser.AliasValue α)

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

Equations

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

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

Equations

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

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 := (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

Equations

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

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 : Lake.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 : Lake.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 : Lake.Name) : IO Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

def Lean.Parser.runParserAttributeHooks (catName : Lake.Name) (declName : Lake.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 : Lake.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 : Lean.Environment) (catName : Lake.Name) (declName : Lake.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 : Lake.Name) : Lean.Parser.LeadingIdentBehavior

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.categoryParserFnImpl (catName : Lake.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

Equations

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

def Lean.Parser.addSyntaxNodeKind (env : Lean.Environment) (k : Lean.SyntaxNodeKind) : Lean.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 : Lean.Environment) (k : Lean.SyntaxNodeKind) : Bool

Equations

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

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 : String) (fileName : String) (normalizeLineEndings : optParam 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

Equations

• Lean.Parser.mkParserState input = { stxStack := Lean.Parser.SyntaxStack.empty, lhsPrec := 0, pos := 0, cache := Lean.Parser.initCacheForInput input, errorMsg := none, recoveredErrors := #[] }

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

Equations

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

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

Equations

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

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

Equations

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

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 : Lake.Name) (declName : Lake.Name) (behavior : optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default) (ref : autoParam Lake.Name _auto✝) : 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.

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

Equations

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

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.

Equations

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

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

Equations

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

@[inline]

def Lean.Parser.commandParser (rbp : optParam 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

Equations

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

@[inline]

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

Equations

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

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

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 : Lean.Parser.Parser → Lean.Parser.Parser

Equations

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

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

  Reference to a category.

• parser: Lake.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 : Lake.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.

def Lean.Parser.resolveParserNameCore.isParser (env : Lean.Environment) (name : Lake.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.

Equations

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

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 : optParam Nat 0) : Lean.Parser.Parser

Equations

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