Lean.KeyedDeclsAttribute

source

@[inline]

abbrev Lean.KeyedDeclsAttribute.Key :

Type

Equations

Lean.KeyedDeclsAttribute.Key = Lean.Name

source

structure Lean.KeyedDeclsAttribute.Def (γ : Type) :

Type

builtinName : Lean.Name
name : Lean.Name
descr : String
valueTypeName : Lean.Name
evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key
onAdded : Bool → Lean.Name → Lean.AttrM Unit

source

instance Lean.KeyedDeclsAttribute.instInhabitedDef :

{a : Type} → Inhabited (Lean.KeyedDeclsAttribute.Def a)

Equations

Lean.KeyedDeclsAttribute.instInhabitedDef = { default := { builtinName := default, name := default, descr := default, valueTypeName := default, evalKey := default, onAdded := default } }

source

structure Lean.KeyedDeclsAttribute.OLeanEntry :

Type

key : Lean.KeyedDeclsAttribute.Key
declName : Lean.Name

source

instance Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry :

Inhabited Lean.KeyedDeclsAttribute.OLeanEntry

Equations

Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry = { default := { key := default, declName := default } }

source

structure Lean.KeyedDeclsAttribute.AttributeEntry (γ : Type) extends Lean.KeyedDeclsAttribute.OLeanEntry :

Type

value : γ

source

@[inline]

abbrev Lean.KeyedDeclsAttribute.Table (γ : Type) :

Type

Equations

Lean.KeyedDeclsAttribute.Table γ = Lean.SMap Lean.KeyedDeclsAttribute.Key (List (Lean.KeyedDeclsAttribute.AttributeEntry γ))

source

structure Lean.KeyedDeclsAttribute.ExtensionState (γ : Type) :

Type

newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry
table : Lean.KeyedDeclsAttribute.Table γ
declNames : Std.PHashSet Lean.Name
erased : Std.PHashSet Lean.Name

source

instance Lean.KeyedDeclsAttribute.instInhabitedExtensionState :

{a : Type} → Inhabited (Lean.KeyedDeclsAttribute.ExtensionState a)

Equations

Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := { newEntries := default, table := default, declNames := default, erased := default } }

source

@[inline]

abbrev Lean.KeyedDeclsAttribute.Extension (γ : Type) :

Type

Equations

Lean.KeyedDeclsAttribute.Extension γ = Lean.ScopedEnvExtension Lean.KeyedDeclsAttribute.OLeanEntry (Lean.KeyedDeclsAttribute.AttributeEntry γ) (Lean.KeyedDeclsAttribute.ExtensionState γ)

source

structure Lean.KeyedDeclsAttribute (γ : Type) :

Type

defn : Lean.KeyedDeclsAttribute.Def γ
tableRef : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)
ext : Lean.KeyedDeclsAttribute.Extension γ

source

noncomputable instance Lean.instNonemptyKeyedDeclsAttribute {γ : Type} :

Nonempty (Lean.KeyedDeclsAttribute γ)

Equations

@Lean.instNonemptyKeyedDeclsAttribute = @Lean.instNonemptyKeyedDeclsAttribute.proof_1

source

def Lean.KeyedDeclsAttribute.ExtensionState.insert {γ : Type} (s : Lean.KeyedDeclsAttribute.ExtensionState γ) (v : Lean.KeyedDeclsAttribute.AttributeEntry γ) :

Lean.KeyedDeclsAttribute.ExtensionState γ

Equations

Lean.KeyedDeclsAttribute.ExtensionState.insert s v = { newEntries := v.toOLeanEntry :: s.newEntries, table := Lean.KeyedDeclsAttribute.Table.insert s.table v, declNames := Std.PersistentHashSet.insert s.declNames v.toOLeanEntry.declName, erased := Std.PersistentHashSet.erase s.erased v.toOLeanEntry.declName }

source

def Lean.KeyedDeclsAttribute.addBuiltin {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (key : Lean.KeyedDeclsAttribute.Key) (declName : Lean.Name) (value : γ) :

IO Unit

Equations

Lean.KeyedDeclsAttribute.addBuiltin attr key declName value = ST.Ref.modify attr.tableRef fun m => Lean.KeyedDeclsAttribute.Table.insert m { toOLeanEntry := { key := key, declName := declName }, value := value }

source

def Lean.KeyedDeclsAttribute.mkStateOfTable {γ : Type} (table : Lean.KeyedDeclsAttribute.Table γ) :

Lean.KeyedDeclsAttribute.ExtensionState γ

Equations

Lean.KeyedDeclsAttribute.mkStateOfTable table = { newEntries := [], table := table, declNames := Lean.SMap.fold (fun s x es => List.foldl (fun s e => Std.PersistentHashSet.insert s e.toOLeanEntry.declName) s es) ∅ table, erased := ∅ }

source

def Lean.KeyedDeclsAttribute.ExtensionState.erase {γ : Type} (s : Lean.KeyedDeclsAttribute.ExtensionState γ) (attrName : Lean.Name) (declName : Lean.Name) :

Lean.CoreM (Lean.KeyedDeclsAttribute.ExtensionState γ)

Equations

Lean.KeyedDeclsAttribute.ExtensionState.erase s attrName declName = let _do_jp := fun y => pure { newEntries := s.newEntries, table := s.table, declNames := Std.PersistentHashSet.erase s.declNames declName, erased := Std.PersistentHashSet.insert s.erased declName }; if Std.PersistentHashSet.contains s.declNames declName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData declName ++ Lean.toMessageData "' does not have [" ++ Lean.toMessageData attrName ++ Lean.toMessageData "] attribute") _do_jp y

source

unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Lean.KeyedDeclsAttribute.Def γ) (attrDeclName : Lean.Name) :

IO (Lean.KeyedDeclsAttribute γ)

Equations

Lean.KeyedDeclsAttribute.init df attrDeclName = do let tableRef ← liftM (IO.mkRef { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }) let ext ← Lean.registerScopedEnvExtension { name := df.name, mkInitial := do let a ← ST.Ref.get tableRef pure (Lean.KeyedDeclsAttribute.mkStateOfTable a), ofOLeanEntry := fun s entry => do let ctx ← read match Lean.Environment.evalConstCheck γ ctx.env ctx.opts df.valueTypeName entry.declName with | Except.ok f => pure { toOLeanEntry := entry, value := f } | Except.error ex => throw (IO.userError ex), toOLeanEntry := fun a => a.toOLeanEntry, addEntry := fun s e => Lean.KeyedDeclsAttribute.ExtensionState.insert s e, finalizeImport := id } let _do_jp : PUnit → IO (Lean.KeyedDeclsAttribute γ) := fun y => do Lean.registerBuiltinAttribute { toAttributeImplCore := { name := df.name, descr := df.descr, applicationTime := Lean.AttributeApplicationTime.afterCompilation }, add := fun declName stx attrKind => do let key ← Lean.KeyedDeclsAttribute.Def.evalKey df false stx let a ← Lean.getEnv match Lean.IR.getSorryDep a declName with | none => do let val ← Lean.evalConstCheck γ df.valueTypeName declName Lean.ScopedEnvExtension.add ext { toOLeanEntry := { key := key, declName := declName }, value := val } attrKind Lean.KeyedDeclsAttribute.Def.onAdded df false declName | x => pure (), erase := fun declName => do let a ← Lean.getEnv let s ← pure (Lean.ScopedEnvExtension.getState ext a) let s ← Lean.KeyedDeclsAttribute.ExtensionState.erase s df.name declName Lean.modifyEnv fun env => Lean.ScopedEnvExtension.modifyState ext env fun x => s } pure { defn := df, tableRef := tableRef, ext := ext } if Lean.Name.isAnonymous df.builtinName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.registerBuiltinAttribute { toAttributeImplCore := { name := df.builtinName, descr := "(builtin) " ++ df.descr, applicationTime := Lean.AttributeApplicationTime.afterCompilation }, add := fun declName stx kind => let _do_jp := fun y => do let key ← Lean.KeyedDeclsAttribute.Def.evalKey df true stx let decl ← Lean.getConstInfo declName match Lean.ConstantInfo.type decl with | Lean.Expr.const c x x_1 => if (c != df.valueTypeName) = true then Lean.throwError (Lean.toMessageData "unexpected type at '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', '" ++ Lean.toMessageData df.valueTypeName ++ Lean.toMessageData "' expected") else do let _ ← Lean.getEnv let val : Lean.Expr := Lean.mkAppN (Lean.mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[Lean.mkConst df.valueTypeName, Lean.mkConst attrDeclName, Lean.toExpr key, Lean.toExpr declName, Lean.mkConst declName] Lean.declareBuiltin declName val Lean.KeyedDeclsAttribute.Def.onAdded df true declName | x => Lean.throwError (Lean.toMessageData "unexpected type at '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', '" ++ Lean.toMessageData df.valueTypeName ++ Lean.toMessageData "' expected"); if (kind == Lean.AttributeKind.global) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid attribute '" ++ Lean.toMessageData df.builtinName ++ Lean.toMessageData "', must be global") _do_jp y, erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") } _do_jp y

source

def Lean.KeyedDeclsAttribute.getEntries {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (env : Lean.Environment) (key : Lean.Name) :

List (Lean.KeyedDeclsAttribute.AttributeEntry γ)

Equations

Lean.KeyedDeclsAttribute.getEntries attr env key = let s := Lean.ScopedEnvExtension.getState attr.ext env; let attrs := Lean.SMap.findD s.table key []; if Std.PersistentHashSet.isEmpty s.erased = true then attrs else List.filter (fun attr => !Std.PersistentHashSet.contains s.erased attr.toOLeanEntry.declName) attrs

source

def Lean.KeyedDeclsAttribute.getValues {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (env : Lean.Environment) (key : Lean.Name) :

List γ

Equations

Lean.KeyedDeclsAttribute.getValues attr env key = List.map Lean.KeyedDeclsAttribute.AttributeEntry.value (Lean.KeyedDeclsAttribute.getEntries attr env key)