Documentation

Lean.ParserCompiler.Attribute

structure Lean.ParserCompiler.CombinatorAttribute :

Type

impl : Lean.AttributeImpl
ext : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)

instance Lean.ParserCompiler.instInhabitedCombinatorAttribute :

Inhabited Lean.ParserCompiler.CombinatorAttribute

Equations

Lean.ParserCompiler.instInhabitedCombinatorAttribute = { default := { impl := default, ext := default } }

def Lean.ParserCompiler.registerCombinatorAttribute (name : Lean.Name) (descr : String) :

IO Lean.ParserCompiler.CombinatorAttribute

Equations

Lean.ParserCompiler.registerCombinatorAttribute name descr = do let ext ← Lean.registerSimplePersistentEnvExtension { name := name, addEntryFn := fun s p => Lean.NameMap.insert s p.fst p.snd, addImportedFn := Lean.mkStateFromImportedEntries (fun s p => Lean.NameMap.insert s p.fst p.snd) ∅, toArrayFn := fun es => List.toArray es } let attrImpl : Lean.AttributeImpl := { toAttributeImplCore := { name := name, descr := descr, applicationTime := Lean.AttributeApplicationTime.afterTypeChecking }, add := fun decl stx x => do let env ← Lean.getEnv let parserDeclName ← Lean.Attribute.Builtin.getId stx discard (Lean.getConstInfo parserDeclName) Lean.setEnv (Lean.PersistentEnvExtension.addEntry ext env (parserDeclName, decl)), erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") } Lean.registerBuiltinAttribute attrImpl pure { impl := attrImpl, ext := ext }

def Lean.ParserCompiler.CombinatorAttribute.getDeclFor? (attr : Lean.ParserCompiler.CombinatorAttribute) (env : Lean.Environment) (parserDecl : Lean.Name) :

Option Lean.Name

Equations

Lean.ParserCompiler.CombinatorAttribute.getDeclFor? attr env parserDecl = Lean.NameMap.find? (Lean.SimplePersistentEnvExtension.getState attr.ext env) parserDecl

def Lean.ParserCompiler.CombinatorAttribute.setDeclFor (attr : Lean.ParserCompiler.CombinatorAttribute) (env : Lean.Environment) (parserDecl : Lean.Name) (decl : Lean.Name) :

Lean.Environment

Equations

Lean.ParserCompiler.CombinatorAttribute.setDeclFor attr env parserDecl decl = Lean.PersistentEnvExtension.addEntry attr.ext env (parserDecl, decl)

unsafe def Lean.ParserCompiler.CombinatorAttribute.runDeclFor {α : Type} (attr : Lean.ParserCompiler.CombinatorAttribute) (parserDecl : Lean.Name) :

Equations

Lean.ParserCompiler.CombinatorAttribute.runDeclFor attr parserDecl = do let a ← Lean.getEnv match Lean.ParserCompiler.CombinatorAttribute.getDeclFor? attr a parserDecl with | some d => Lean.evalConst α d | x => Lean.throwError (Lean.toMessageData "no declaration of attribute [" ++ Lean.toMessageData attr.impl.toAttributeImplCore.name ++ Lean.toMessageData "] found for '" ++ Lean.toMessageData parserDecl ++ Lean.toMessageData "'")