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

instance Lean.Parser.ParserExtension.instInhabitedOLeanEntry : Inhabited OLeanEntry

Equations

• Lean.Parser.ParserExtension.instInhabitedOLeanEntry = { default := Lean.Parser.ParserExtension.instInhabitedOLeanEntry.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_reducible]

instance Lean.Parser.ParserExtension.instInhabitedEntry : Inhabited Entry

Equations

• Lean.Parser.ParserExtension.instInhabitedEntry = { default := Lean.Parser.ParserExtension.instInhabitedEntry.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_reducible]

instance Lean.Parser.ParserExtension.instInhabitedState : Inhabited State

Equations

• Lean.Parser.ParserExtension.instInhabitedState = { default := Lean.Parser.ParserExtension.instInhabitedState.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 (Std.TreeMap.getD __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_reducible]

instance Lean.Parser.instCoeParserParserAliasValue : Coe Parser ParserAliasValue

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

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

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

Equations

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

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

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) (endPos : String.Pos.Raw := input.rawEndPos) (endPos_valid : endPos ≤ input.rawEndPos := by simp) : 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 have 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

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.

Equations

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

@[inline]

def Lean.Parser.withSetOption : Parser → Parser

Equations

• Lean.Parser.withSetOption = Lean.Parser.withFn Lean.Parser.withSetOptionFn

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.

Equations

• Lean.Parser.withSetOptionValueFn p c s = if s.stxStack.size ≥ 3 then Lean.Parser.withSetOptionValueFnCore✝ (s.stxStack.get! (s.stxStack.size - 3)) s.stxStack.back p c s else p c s

@[inline]

def Lean.Parser.withSetOptionValue : Parser → Parser

Equations

• Lean.Parser.withSetOptionValue = Lean.Parser.withFn Lean.Parser.withSetOptionValueFn

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.

Equations

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

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.