Lean.Parser.Extension

Number of syntax nodes produced by this parser. none means "sum of input sizes".
stackSz? : Option Nat
Whether arguments should be wrapped in group(·) if they do not produce exactly one syntax node.
autoGroupArgs : Bool

source

opaque Lean.Parser.parserAliasesRef:

IO.Ref (Lean.NameMap Lean.Parser.ParserAliasValue)

source

opaque Lean.Parser.parserAlias2kindRef:

IO.Ref (Lean.NameMap Lean.SyntaxNodeKind)

source

opaque Lean.Parser.parserAliases2infoRef:

IO.Ref (Lean.NameMap Lean.Parser.ParserAliasInfo)

source

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

IO Lean.Parser.ParserAliasInfo

Equations

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

source

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

IO Unit

Equations

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

source

instance Lean.Parser.instCoeParserParserAliasValue:

Coe Lean.Parser.Parser Lean.Parser.ParserAliasValue

Equations

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

source

instance Lean.Parser.instCoeForAllParserParserAliasValue:

Coe (Lean.Parser.Parser → Lean.Parser.Parser) Lean.Parser.ParserAliasValue

Equations

Lean.Parser.instCoeForAllParserParserAliasValue = { coe := Lean.Parser.AliasValue.unary }

source

instance Lean.Parser.instCoeForAllParserParserAliasValue_1:

Coe (Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser) Lean.Parser.ParserAliasValue

Equations

Lean.Parser.instCoeForAllParserParserAliasValue_1 = { coe := Lean.Parser.AliasValue.binary }

source

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

IO Bool

Equations

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

source

def Lean.Parser.getSyntaxKindOfParserAlias? (aliasName : Lean.Name) :

IO (Option Lean.SyntaxNodeKind)

Equations

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

source

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

IO Unit

Equations

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

source

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

IO Unit

Equations

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

source

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

IO Unit

Equations

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

source

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

source

@[implementedBy Lean.Parser.mkParserOfConstantUnsafe]

opaque Lean.Parser.mkParserOfConstantAux (constName : Lean.Name) (compileParserDescr : Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser) :

Lean.ImportM (Bool × Lean.Parser.Parser)

source

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

source

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

Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser

source

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

Lean.ImportM (Bool × Lean.Parser.Parser)

Equations

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

source

structure Lean.Parser.ParserAttributeHook:

Type

postAdd : Lean.Name → Lean.Name → Bool → Lean.AttrM Unit

source

opaque Lean.Parser.parserAttributeHooks:

IO.Ref (List Lean.Parser.ParserAttributeHook)

source

def Lean.Parser.registerParserAttributeHook (hook : Lean.Parser.ParserAttributeHook) :

IO Unit

Equations

Lean.Parser.registerParserAttributeHook hook = ST.Ref.modify Lean.Parser.parserAttributeHooks fun hooks => hook :: hooks

source

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

Lean.AttrM Unit

Equations

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

source

opaque Lean.Parser.parserExtension:

Lean.Parser.ParserExtension

source

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

Bool

Equations

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

source

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

Except String Lean.Environment

Equations

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

source

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.

source

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

Lean.Parser.ParserFn

Equations

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

source

@[implementedBy Lean.Parser.evalParserConstUnsafe]

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

Lean.Parser.ParserFn

source

opaque Lean.Parser.internal.parseQuotWithCurrentStage:

Lean.Option Bool

source

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

source

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

IO Unit

Equations

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

source

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

source

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

source

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

Lean.Parser.Parser

Equations

Lean.Parser.mkCategoryAntiquotParser kind = Lean.Parser.mkAntiquot (Lean.Name.toString kind) kind true true

source

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

Lean.Parser.ParserFn

Equations

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

source

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.

source

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)

source

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

Bool

Equations

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

source

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

List Lean.SyntaxNodeKind

Equations

Lean.Parser.getSyntaxNodeKinds env = let kinds := (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).kinds; Std.PersistentHashMap.foldl kinds (fun ks k x => k :: ks) []

source

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

Lean.Parser.TokenTable

Equations

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

source

def Lean.Parser.mkInputContext (input : String) (fileName : String) :

Lean.Parser.InputContext

Equations

Lean.Parser.mkInputContext input fileName = { input := input, fileName := fileName, fileMap := String.toFileMap input }

source

def Lean.Parser.mkParserContext (ictx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) :

Lean.Parser.ParserContext

Equations

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

source

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

Lean.Parser.ParserState

Equations

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

source

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

Except String Lean.Syntax

Equations

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

source

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

Lean.CoreM Unit

Equations

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

source

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

Lean.CoreM Unit

Equations

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

source

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

Lean.CoreM Unit

Equations

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

source

def Lean.Parser.getParserPriority (args : Lean.Syntax) :

Except String Nat

Equations

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

source

def Lean.Parser.registerBuiltinParserAttribute (attrName : Lean.Name) (catName : Lean.Name) (behavior : optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default) :

IO Unit

Equations

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

source

def Lean.Parser.mkParserAttributeImpl (attrName : Lean.Name) (catName : Lean.Name) :

Lean.AttributeImpl

Equations

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

source

def Lean.Parser.registerBuiltinDynamicParserAttribute (attrName : Lean.Name) (catName : Lean.Name) :

IO Unit

Equations

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

source

def Lean.Parser.registerParserCategory (env : Lean.Environment) (attrName : Lean.Name) (catName : Lean.Name) (behavior : optParam Lean.Parser.LeadingIdentBehavior Lean.Parser.LeadingIdentBehavior.default) :

IO Lean.Environment

Equations

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

source

@[inline]

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

Lean.Parser.Parser

Equations

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

source

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.

source

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.

source

@[inline]

def Lean.Parser.withOpen (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withOpen p = { info := p.info, fn := Lean.Parser.withOpenFn p.fn }

source

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 Array.size s.stxStack > 0 then let stx := Array.back s.stxStack; Lean.Parser.withOpenDeclFnCore stx p c s else p c s

source

@[inline]

def Lean.Parser.withOpenDecl (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.withOpenDecl p = { info := p.info, fn := Lean.Parser.withOpenDeclFn p.fn }

source

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

Lean.Parser.ParserFn

Equations

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

source

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.