Lean.Parser.Extension

Lean.Parser.addLeadingParser categories catName parserName p prio = match Lean.Parser.getCategory categories catName with | none => Lean.Parser.throwUnknownParserCategory catName | some cat => let addTokens := fun tks => let tks := List.map (fun tk => Lean.Name.mkSimple tk) tks; let tables := List.foldl (fun tables tk => { leadingTable := Lean.Parser.TokenMap.insert tables.leadingTable tk (p, prio), leadingParsers := tables.leadingParsers, trailingTable := tables.trailingTable, trailingParsers := tables.trailingParsers }) cat.tables (List.eraseDups tks); pure (Std.PersistentHashMap.insert categories catName { tables := tables, behavior := cat.behavior }); match p.info.firstTokens with | Lean.Parser.FirstTokens.tokens tks => addTokens tks | Lean.Parser.FirstTokens.optTokens tks => addTokens tks | x => let tables := let src := cat.tables; { leadingTable := src.leadingTable, leadingParsers := (p, prio) :: cat.tables.leadingParsers, trailingTable := src.trailingTable, trailingParsers := src.trailingParsers }; pure (Std.PersistentHashMap.insert categories catName { tables := tables, behavior := cat.behavior })

source

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

Except String Lean.Parser.ParserCategories

Equations

Lean.Parser.addTrailingParser categories catName p prio = match Lean.Parser.getCategory categories catName with | none => Lean.Parser.throwUnknownParserCategory catName | some cat => pure (Std.PersistentHashMap.insert categories catName { tables := Lean.Parser.addTrailingParserAux cat.tables p prio, behavior := cat.behavior })

source

def Lean.Parser.addParser (categories : Lean.Parser.ParserCategories) (catName : Lean.Name) (declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : Nat) :

Except String Lean.Parser.ParserCategories

Equations

Lean.Parser.addParser categories catName declName leading p prio = match leading, p with | true, p => Lean.Parser.addLeadingParser categories catName declName p prio | false, p => Lean.Parser.addTrailingParser categories catName p prio

source

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 := Lean.Parser.ParserInfo.collectTokens info []; List.foldlM Lean.Parser.addTokenConfig tokenTable newTokens

source

def Lean.Parser.ParserExtension.addEntryImpl (s : Lean.Parser.ParserExtension.State) (e : Lean.Parser.ParserExtension.Entry) :

Lean.Parser.ParserExtension.State

Equations

Lean.Parser.ParserExtension.addEntryImpl s e = match e with | Lean.Parser.ParserExtension.Entry.token tk => match Lean.Parser.addTokenConfig s.tokens tk with | Except.ok tokens => { tokens := tokens, kinds := s.kinds, categories := s.categories } | x => panicWithPosWithDecl "Lean.Parser.Extension" "Lean.Parser.ParserExtension.addEntryImpl" 155 26 "unreachable code has been reached" | Lean.Parser.ParserExtension.Entry.kind k => { tokens := s.tokens, kinds := Lean.Parser.SyntaxNodeKindSet.insert s.kinds k, categories := s.categories } | Lean.Parser.ParserExtension.Entry.category catName behavior => if Std.PersistentHashMap.contains s.categories catName = true then s else { tokens := s.tokens, kinds := s.kinds, categories := Std.PersistentHashMap.insert s.categories catName { tables := { leadingTable := ∅, leadingParsers := [], trailingTable := ∅, trailingParsers := [] }, behavior := behavior } } | Lean.Parser.ParserExtension.Entry.parser catName declName leading parser prio => match Lean.Parser.addParser s.categories catName declName leading parser prio with | Except.ok categories => { tokens := s.tokens, kinds := s.kinds, categories := categories } | x => panicWithPosWithDecl "Lean.Parser.Extension" "Lean.Parser.ParserExtension.addEntryImpl" 165 11 "unreachable code has been reached"

source

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

Type

const: {α : Type} → α → Lean.Parser.AliasValue α
unary: {α : Type} → (α → α) → Lean.Parser.AliasValue α
binary: {α : Type} → (α → α → α) → Lean.Parser.AliasValue α

source

@[inline]

abbrev Lean.Parser.AliasTable (α : Type) :

Type

Equations

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

source

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

IO Unit

Equations

Lean.Parser.registerAliasCore mapRef aliasName value = do let a ← liftM IO.initializing let _do_jp : PUnit → IO Unit := fun y => do let a ← ST.Ref.get mapRef let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify mapRef fun a => Lean.NameMap.insert a aliasName value if Lean.NameMap.contains a aliasName = true then do let y ← throw (IO.userError (toString "alias '" ++ toString aliasName ++ toString "' has already been declared")) _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "aliases can only be registered during initialization") _do_jp y

source

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 a ← ST.Ref.get mapRef pure (Lean.NameMap.find? a aliasName)

source

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

IO α

Equations

Lean.Parser.getConstAlias mapRef aliasName = do let a ← Lean.Parser.getAlias mapRef aliasName match a with | some (Lean.Parser.AliasValue.const v) => pure v | some (Lean.Parser.AliasValue.unary x) => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' is not a constant, it takes one argument")) | some (Lean.Parser.AliasValue.binary x) => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' is not a constant, it takes two arguments")) | none => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' was not found"))

source

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

IO (α → α)

Equations

Lean.Parser.getUnaryAlias mapRef aliasName = do let a ← Lean.Parser.getAlias mapRef aliasName match a with | some (Lean.Parser.AliasValue.unary v) => pure v | some x => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' does not take one argument")) | none => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' was not found"))

source

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

IO (α → α → α)

Equations

Lean.Parser.getBinaryAlias mapRef aliasName = do let a ← Lean.Parser.getAlias mapRef aliasName match a with | some (Lean.Parser.AliasValue.binary v) => pure v | some x => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' does not take two arguments")) | none => throw (IO.userError (toString "parser '" ++ toString aliasName ++ toString "' was not found"))

source

@[inline]

abbrev Lean.Parser.ParserAliasValue :

Type

Equations

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

source

constant Lean.Parser.parserAliasesRef :

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

source

def Lean.Parser.registerAlias (aliasName : Lean.Name) (p : Lean.Parser.ParserAliasValue) :

IO Unit

Equations

Lean.Parser.registerAlias aliasName p = Lean.Parser.registerAliasCore Lean.Parser.parserAliasesRef aliasName p

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 x => pure true | x => pure false

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

Lean.Parser.mkParserOfConstantUnsafe constName compileParserDescr = do let a ← read let env : Lean.Environment := a.env let a ← read let opts : Lean.Options := a.opts match Lean.Environment.find? env constName with | none => throw (IO.userError (toString "unknow constant '" ++ toString constName ++ toString "'")) | some info => match Lean.ConstantInfo.type info with | Lean.Expr.const (Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "Parser" x_3) "TrailingParser" x_4) x x_1 => do let p ← liftM (IO.ofExcept (Lean.Environment.evalConst Lean.Parser.Parser env opts constName)) pure (false, p) | Lean.Expr.const (Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "Parser" x_3) "Parser" x_4) x x_1 => do let p ← liftM (IO.ofExcept (Lean.Environment.evalConst Lean.Parser.Parser env opts constName)) pure (true, p) | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "ParserDescr" x_3) x x_1 => do let d ← liftM (IO.ofExcept (Lean.Environment.evalConst Lean.ParserDescr env opts constName)) let p ← compileParserDescr d pure (true, p) | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "TrailingParserDescr" x_3) x x_1 => do let d ← liftM (IO.ofExcept (Lean.Environment.evalConst Lean.TrailingParserDescr env opts constName)) let p ← compileParserDescr d pure (false, p) | x => throw (IO.userError (toString "unexpected parser type at '" ++ toString constName ++ toString "' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected"))

source

@[implementedBy Lean.Parser.mkParserOfConstantUnsafe]

constant 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 = (fun visit => visit d) (Lean.Parser.compileParserDescr.visit categories)

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

constant 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

Lean.Parser.runParserAttributeHooks catName declName builtin = do let hooks ← ST.Ref.get Lean.Parser.parserAttributeHooks List.forM hooks fun hook => Lean.Parser.ParserAttributeHook.postAdd hook catName declName builtin

source

constant 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

Lean.Parser.addParserCategory env catName behavior = if Lean.Parser.isParserCategory env catName = true then Lean.Parser.throwParserCategoryAlreadyDefined catName else pure (Lean.ScopedEnvExtension.addEntry Lean.Parser.parserExtension env (Lean.Parser.ParserExtension.Entry.category catName behavior))

source

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

Lean.Parser.LeadingIdentBehavior

Equations

Lean.Parser.leadingIdentBehavior env catName = match Lean.Parser.getCategory (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).categories catName with | none => Lean.Parser.LeadingIdentBehavior.default | some cat => cat.behavior

source

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

Lean.Parser.ParserFn

Equations

Lean.Parser.evalParserConstUnsafe declName ctx s = unsafeBaseIO (let categories := (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension ctx.toParserModuleContext.env).categories; do let a ← EIO.toBaseIO (Lean.Parser.mkParserOfConstant categories declName { env := ctx.toParserModuleContext.env, opts := ctx.toParserModuleContext.options }) match a with | Except.ok (bool, p) => pure (Lean.Parser.Parser.fn p ctx s) | Except.error e => pure (Lean.Parser.ParserState.mkUnexpectedError s (IO.Error.toString e)))

source

@[implementedBy Lean.Parser.evalParserConstUnsafe]

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

Lean.Parser.ParserFn

source

constant Lean.Parser.internal.parseQuotWithCurrentStage :

Lean.Option Bool

source

def Lean.Parser.evalInsideQuot (declName : Lean.Name) (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.evalInsideQuot declName p = { info := p.info, fn := fun c s => if (decide (c.quotDepth > 0) && !c.suppressInsideQuot && Lean.Option.get c.toParserModuleContext.options Lean.Parser.internal.parseQuotWithCurrentStage && Lean.Environment.contains c.toParserModuleContext.env declName) = true then Lean.Parser.evalParserConst declName c s else Lean.Parser.Parser.fn p c s }

source

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

IO Unit

Equations

Lean.Parser.addBuiltinParser catName declName leading p prio = let p := Lean.Parser.evalInsideQuot declName p; do let categories ← ST.Ref.get Lean.Parser.builtinParserCategoriesRef let categories ← IO.ofExcept (Lean.Parser.addParser categories catName declName leading p prio) ST.Ref.set Lean.Parser.builtinParserCategoriesRef categories ST.Ref.modify Lean.Parser.builtinSyntaxNodeKindSetRef p.info.collectKinds Lean.Parser.updateBuiltinTokens p.info declName

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

source

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

Lean.Parser.ParserFn

Equations

Lean.Parser.categoryParserFnImpl catName ctx s = let catName := if (catName == `syntax) = true then `stx else catName; let categories := (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension ctx.toParserModuleContext.env).categories; match Lean.Parser.getCategory categories catName with | some cat => Lean.Parser.prattParser catName cat.tables cat.behavior (Lean.Parser.mkCategoryAntiquotParserFn catName) ctx s | none => Lean.Parser.ParserState.mkUnexpectedError s ("unknown parser category '" ++ toString catName ++ "'")

source

def Lean.Parser.addToken (tk : Lean.Parser.Token) (kind : Lean.AttributeKind) :

Lean.AttrM Unit

Equations

Lean.Parser.addToken tk kind = do let a ← Lean.getEnv discard (Lean.ofExcept (Lean.Parser.addTokenConfig (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension a).tokens tk)) Lean.ScopedEnvExtension.add Lean.Parser.parserExtension (Lean.Parser.ParserExtension.Entry.token tk) kind

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

Lean.Parser.isValidSyntaxNodeKind env k = let kinds := (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension env).kinds; Std.PersistentHashMap.contains kinds k

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

Lean.Parser.mkParserContext ictx pmctx = { toInputContext := ictx, toParserModuleContext := pmctx, prec := 0, tokens := Lean.Parser.getTokenTable pmctx.env, quotDepth := 0, suppressInsideQuot := false, savedPos? := none, forbiddenTk? := none }

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

Except String Lean.Syntax

Equations

Lean.Parser.runParserCategory env catName input fileName = let c := Lean.Parser.mkParserContext (Lean.Parser.mkInputContext input fileName) { env := env, options := { entries := [] }, currNamespace := Lean.Name.anonymous, openDecls := [] }; let s := Lean.Parser.mkParserState input; let s := Lean.Parser.whitespace c s; let s := Lean.Parser.categoryParserFnImpl catName c s; if Lean.Parser.ParserState.hasError s = true then Except.error (Lean.Parser.ParserState.toErrorMsg c s) else if String.atEnd input s.pos = true then Except.ok (Array.back s.stxStack) else Except.error (Lean.Parser.ParserState.toErrorMsg c (Lean.Parser.ParserState.mkError s "end of input"))

source

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

Lean.CoreM Unit

Equations

Lean.Parser.declareBuiltinParser addFnName catName declName prio = let val := Lean.mkAppN (Lean.mkConst addFnName) #[Lean.toExpr catName, Lean.toExpr declName, Lean.mkConst declName, Lean.mkRawNatLit prio]; Lean.declareBuiltin declName val

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

Lean.Parser.getParserPriority args = match Lean.Syntax.getNumArgs args with | 0 => pure 0 | 1 => match Lean.Syntax.isNatLit? (Lean.Syntax.getArg args 0) with | some prio => pure prio | none => throw "invalid parser attribute, numeral expected" | x => throw "invalid parser attribute, no argument or numeral expected"

source

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

IO Unit

Equations

Lean.Parser.registerBuiltinParserAttribute attrName catName behavior = do Lean.Parser.addBuiltinParserCategory catName behavior Lean.registerBuiltinAttribute { toAttributeImplCore := { name := attrName, descr := "Builtin parser", applicationTime := Lean.AttributeApplicationTime.afterCompilation }, add := fun declName stx kind => liftM (Lean.Parser.BuiltinParserAttribute.add attrName catName declName stx kind), erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") }

source

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

Lean.AttributeImpl

Equations

Lean.Parser.mkParserAttributeImpl attrName catName = { toAttributeImplCore := { name := attrName, descr := "parser", applicationTime := Lean.AttributeApplicationTime.afterCompilation }, add := fun declName stx attrKind => Lean.Parser.ParserAttribute.add attrName catName declName stx attrKind, erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") }

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

Lean.Parser.registerParserCategory env attrName catName behavior = do let env ← IO.ofExcept (Lean.Parser.addParserCategory env catName behavior) Lean.registerAttributeOfBuilder env `parserAttr [Lean.DataValue.ofName attrName, Lean.DataValue.ofName catName]

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.notFollowedByCategoryTokenFn (catName : Lean.Name) :

Lean.Parser.ParserFn

Equations

Lean.Parser.notFollowedByCategoryTokenFn catName ctx s = let categories := (Lean.ScopedEnvExtension.getState Lean.Parser.parserExtension ctx.toParserModuleContext.env).categories; match Lean.Parser.getCategory categories catName with | none => Lean.Parser.ParserState.mkUnexpectedError s (toString "unknown parser category '" ++ toString catName ++ toString "'") | some cat => let x := Lean.Parser.peekToken ctx s; match x with | (s, stx) => match stx with | Except.ok (Lean.Syntax.atom x sym) => if (decide (ctx.quotDepth > 0) && sym == "$") = true then s else match Std.RBMap.find? cat.tables.leadingTable (Lean.Name.mkSimple sym) with | some x => Lean.Parser.ParserState.mkUnexpectedError s (toString catName) | x => s | Except.ok x => s | Except.error x => s

source

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.notFollowedByCategoryToken catName = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.notFollowedByCategoryTokenFn catName }

source

@[inline]

abbrev Lean.Parser.notFollowedByCommandToken :

Lean.Parser.Parser

Equations

Lean.Parser.notFollowedByCommandToken = Lean.Parser.notFollowedByCategoryToken `command

source

@[inline]

abbrev Lean.Parser.notFollowedByTermToken :

Lean.Parser.Parser

Equations

Lean.Parser.notFollowedByTermToken = Lean.Parser.notFollowedByCategoryToken `term

source

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

Lean.Parser.ParserFn

Equations

Lean.Parser.withOpenDeclFnCore openDeclStx p c s = if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openSimple) = true then Lean.Parser.withNamespaces (Array.map (fun stx => Lean.Syntax.getId stx) (Lean.Syntax.getArgs (Lean.Syntax.getOp openDeclStx 0))) p true c s else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openScoped) = true then Lean.Parser.withNamespaces (Array.map (fun stx => Lean.Syntax.getId stx) (Lean.Syntax.getArgs (Lean.Syntax.getOp openDeclStx 1))) p false c s else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openOnly) = true then p c s else if (Lean.Syntax.getKind openDeclStx == `Lean.Parser.Command.openHiding) = true then p c s else p c s

source

def Lean.Parser.withOpenFn (p : Lean.Parser.ParserFn) :

Lean.Parser.ParserFn

Equations

Lean.Parser.withOpenFn p c s = if Array.size s.stxStack > 0 then let stx := Array.back s.stxStack; if (Lean.Syntax.getKind stx == `Lean.Parser.Command.open) = true then Lean.Parser.withOpenDeclFnCore (Lean.Syntax.getOp stx 1) p c s else p c s else p c s

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

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

Lean.Parser.parserOfStackFn offset ctx s = let stack := s.stxStack; if Array.size stack < offset + 1 then Lean.Parser.ParserState.mkUnexpectedError s "failed to determine parser using syntax stack, stack is too small" else match Array.get! stack (Array.size stack - offset - 1) with | Lean.Syntax.ident x x_1 parserName x_2 => match Lean.Parser.ParserContext.resolveName ctx parserName with | [(parserName, [])] => let iniSz := Lean.Parser.ParserState.stackSize s; let s := Lean.Parser.evalParserConst parserName ctx s; if (!Lean.Parser.ParserState.hasError s && Lean.Parser.ParserState.stackSize s != iniSz + 1) = true then Lean.Parser.ParserState.mkUnexpectedError s "expected parser to return exactly one syntax object" else s | x :: x_3 :: x_4 => Lean.Parser.ParserState.mkUnexpectedError s (toString "ambiguous parser name " ++ toString parserName ++ toString "") | x => Lean.Parser.ParserState.mkUnexpectedError s (toString "unknown parser " ++ toString parserName ++ toString "") | x => Lean.Parser.ParserState.mkUnexpectedError s "failed to determine parser using syntax stack, the specified element on the stack is not an identifier"

source

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

Lean.Parser.Parser

Equations

Lean.Parser.parserOfStack offset prec = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := fun c s => Lean.Parser.parserOfStackFn offset { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := prec, tokens := c.tokens, quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? } s }