- afterTypeChecking: Lean.AttributeApplicationTime
- afterCompilation: Lean.AttributeApplicationTime
- beforeElaboration: Lean.AttributeApplicationTime
Equations
- Lean.instBEqAttributeApplicationTime = { beq := [anonymous] }
Equations
- Lean.instMonadLiftImportMAttrM = { monadLift := fun {α} x => do let a ← Lean.getEnv let a_1 ← Lean.getOptions liftM (x { env := a, opts := a_1 }) }
- name : Lean.Name
- descr : String
- applicationTime : Lean.AttributeApplicationTime
Equations
- Lean.instInhabitedAttributeImplCore = { default := { name := default, descr := default, applicationTime := default } }
- global: Lean.AttributeKind
- local: Lean.AttributeKind
- scoped: Lean.AttributeKind
Equations
- Lean.instBEqAttributeKind = { beq := [anonymous] }
Equations
- Lean.instInhabitedAttributeKind = { default := Lean.AttributeKind.global }
Equations
- Lean.instToStringAttributeKind = { toString := fun x => match x with | Lean.AttributeKind.global => "global" | Lean.AttributeKind.local => "local" | Lean.AttributeKind.scoped => "scoped" }
- add : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Unit
- erase : Lean.Name → Lean.AttrM Unit
Equations
- Lean.instInhabitedAttributeImpl = { default := { toAttributeImplCore := default, add := default, erase := default } }
Equations
- Lean.registerBuiltinAttribute attr = do let m ← ST.Ref.get Lean.attributeMapRef let _do_jp : PUnit → IO Unit := fun y => do let a ← Lean.initializing let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify Lean.attributeMapRef fun m => Std.PersistentHashMap.insert m attr.toAttributeImplCore.name attr if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register attribute, attributes can only be registered during initialization") _do_jp y if Std.PersistentHashMap.contains m attr.toAttributeImplCore.name = true then do let y ← throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attr.toAttributeImplCore.name ++ "' has already been used")) _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.Attribute.Builtin.ensureNoArgs stx = if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.simple && Lean.Syntax.isNone (Lean.Syntax.getOp stx 1) && Lean.Syntax.isNone (Lean.Syntax.getOp stx 2)) = true then pure () else if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.class) = true then pure () else match stx with | Lean.Syntax.missing => pure () | x => Lean.throwErrorAt stx (Lean.toMessageData "unexpected attribute argument")
Equations
- Lean.Attribute.Builtin.getIdent? stx = if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.simple) = true then if (!Lean.Syntax.isNone (Lean.Syntax.getOp stx 1) && Lean.Syntax.isIdent (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0)) = true then pure (some (Lean.Syntax.getOp (Lean.Syntax.getOp stx 1) 0)) else pure none else if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.macro || Lean.Syntax.getKind stx == `Lean.Parser.Attr.export) = true then pure (some (Lean.Syntax.getOp stx 1)) else Lean.throwErrorAt stx (Lean.toMessageData "unexpected attribute argument")
Equations
- Lean.Attribute.Builtin.getIdent stx = do let a ← Lean.Attribute.Builtin.getIdent? stx match a with | some id => pure id | none => Lean.throwErrorAt stx (Lean.toMessageData "unexpected attribute argument, identifier expected")
Equations
- Lean.Attribute.Builtin.getId? stx = do let ident? ← Lean.Attribute.Builtin.getIdent? stx pure (Lean.Syntax.getId <$> ident?)
Equations
- Lean.Attribute.Builtin.getId stx = do let a ← Lean.Attribute.Builtin.getIdent stx pure (Lean.Syntax.getId a)
Equations
- Lean.getAttrParamOptPrio optPrioStx = if Lean.Syntax.isNone optPrioStx = true then pure 1000 else match Lean.Syntax.isNatLit? (Lean.Syntax.getOp optPrioStx 0) with | some prio => pure prio | none => Lean.throwErrorAt optPrioStx (Lean.toMessageData "priority expected")
Equations
- Lean.Attribute.Builtin.getPrio stx = if (Lean.Syntax.getKind stx == `Lean.Parser.Attr.simple) = true then Lean.getAttrParamOptPrio (Lean.Syntax.getOp stx 1) else Lean.throwErrorAt stx (Lean.toMessageData "unexpected attribute argument, optional priority expected")
Equations
- Lean.instInhabitedTagAttribute = { default := { attr := default, ext := default } }
def
Lean.registerTagAttribute
(name : Lean.Name)
(descr : String)
(validate : optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ())
:
Equations
- Lean.registerTagAttribute name descr validate = do let ext ← Lean.registerPersistentEnvExtension { name := name, mkInitial := pure ∅, addImportedFn := fun x x => pure ∅, addEntryFn := fun s n => Lean.NameSet.insert s n, exportEntriesFn := fun es => let r := Std.RBTree.fold (fun a e => Array.push a e) #[] es; Array.qsort r Lean.Name.quickLt 0 (Array.size r - 1), statsFn := fun s => Std.Format.text "tag attribute" ++ Lean.Format.line ++ Std.Format.text "number of local entries: " ++ Lean.format (Std.RBMap.size s) } let attrImpl : Lean.AttributeImpl := { toAttributeImplCore := { name := name, descr := descr, applicationTime := Lean.AttributeApplicationTime.afterTypeChecking }, add := fun decl stx kind => do Lean.Attribute.Builtin.ensureNoArgs stx let _do_jp : PUnit → Lean.AttrM Unit := fun y => do let env ← Lean.getEnv let _do_jp : PUnit → Lean.AttrM Unit := fun y => do validate decl let env ← Lean.getEnv Lean.setEnv (Lean.PersistentEnvExtension.addEntry ext env decl) if Option.isNone (Lean.Environment.getModuleIdxFor? env decl) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid attribute '" ++ Lean.toMessageData name ++ Lean.toMessageData "', declaration is in an imported module") _do_jp y 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 name ++ Lean.toMessageData "', must be global") _do_jp y, erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") } Lean.registerBuiltinAttribute attrImpl pure { attr := attrImpl, ext := ext }
def
Lean.TagAttribute.hasTag
(attr : Lean.TagAttribute)
(env : Lean.Environment)
(decl : Lean.Name)
:
Equations
- Lean.TagAttribute.hasTag attr env decl = match Lean.Environment.getModuleIdxFor? env decl with | some modIdx => Array.binSearchContains (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) decl Lean.Name.quickLt 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) - 1) | none => Lean.NameSet.contains (Lean.PersistentEnvExtension.getState attr.ext env) decl
- attr : Lean.AttributeImpl
- ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)
instance
Lean.instInhabitedParametricAttribute
:
{a : Type} → Inhabited (Lean.ParametricAttribute a)
Equations
- Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
- getParam : Lean.Name → Lean.Syntax → Lean.AttrM α
- afterSet : Lean.Name → α → Lean.AttrM Unit
- afterImport : Array (Array (Lean.Name × α)) → Lean.ImportM Unit
def
Lean.registerParametricAttribute
{α : Type}
[inst : Inhabited α]
(impl : Lean.ParametricAttributeImpl α)
:
Equations
- Lean.registerParametricAttribute impl = do let ext ← Lean.registerPersistentEnvExtension { name := impl.toAttributeImplCore.name, mkInitial := pure ∅, addImportedFn := fun s => SeqRight.seqRight (Lean.ParametricAttributeImpl.afterImport impl s) fun x => pure ∅, addEntryFn := fun s p => Lean.NameMap.insert s p.fst p.snd, exportEntriesFn := fun m => let r := Std.RBMap.fold (fun a n p => Array.push a (n, p)) #[] m; Array.qsort r (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size r - 1), statsFn := fun s => Std.Format.text "parametric attribute" ++ Lean.Format.line ++ Std.Format.text "number of local entries: " ++ Lean.format (Std.RBMap.size s) } let attrImpl : Lean.AttributeImpl := { toAttributeImplCore := { name := impl.toAttributeImplCore.name, descr := impl.toAttributeImplCore.descr, applicationTime := Lean.AttributeApplicationTime.afterTypeChecking }, add := fun decl stx kind => let _do_jp := fun y => do let env ← Lean.getEnv let _do_jp : PUnit → Lean.AttrM Unit := fun y => do let val ← Lean.ParametricAttributeImpl.getParam impl decl stx let env' : Lean.Environment := Lean.PersistentEnvExtension.addEntry ext env (decl, val) Lean.setEnv env' tryCatch (Lean.ParametricAttributeImpl.afterSet impl decl val) fun x => Lean.setEnv env if Option.isNone (Lean.Environment.getModuleIdxFor? env decl) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid attribute '" ++ Lean.toMessageData impl.toAttributeImplCore.name ++ Lean.toMessageData "', declaration is in an imported module") _do_jp y; 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 impl.toAttributeImplCore.name ++ Lean.toMessageData "', must be global") _do_jp y, erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") } Lean.registerBuiltinAttribute attrImpl pure { attr := attrImpl, ext := ext }
def
Lean.ParametricAttribute.getParam
{α : Type}
[inst : Inhabited α]
(attr : Lean.ParametricAttribute α)
(env : Lean.Environment)
(decl : Lean.Name)
:
Option α
Equations
- Lean.ParametricAttribute.getParam attr env decl = match Lean.Environment.getModuleIdxFor? env decl with | some modIdx => match Array.binSearch (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) (decl, default) (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) - 1) with | some (x, val) => some val | none => none | none => Lean.NameMap.find? (Lean.PersistentEnvExtension.getState attr.ext env) decl
def
Lean.ParametricAttribute.setParam
{α : Type}
(attr : Lean.ParametricAttribute α)
(env : Lean.Environment)
(decl : Lean.Name)
(param : α)
:
Equations
- Lean.ParametricAttribute.setParam attr env decl param = if Option.isSome (Lean.Environment.getModuleIdxFor? env decl) = true then Except.error ("invalid '" ++ toString attr.attr.toAttributeImplCore.name ++ "'.setParam, declaration is in an imported module") else if Option.isSome (Lean.NameMap.find? (Lean.PersistentEnvExtension.getState attr.ext env) decl) = true then Except.error ("invalid '" ++ toString attr.attr.toAttributeImplCore.name ++ "'.setParam, attribute has already been set") else Except.ok (Lean.PersistentEnvExtension.addEntry attr.ext env (decl, param))
- attrs : List Lean.AttributeImpl
- ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)
Equations
- Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
def
Lean.registerEnumAttributes
{α : Type}
[inst : Inhabited α]
(extName : Lean.Name)
(attrDescrs : List (Lean.Name × String × α))
(validate : optParam (Lean.Name → α → Lean.AttrM Unit) fun x x => pure ())
(applicationTime : optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking)
:
Equations
- Lean.registerEnumAttributes extName attrDescrs validate applicationTime = do let ext ← Lean.registerPersistentEnvExtension { name := extName, mkInitial := pure ∅, addImportedFn := fun x x => pure ∅, addEntryFn := fun s p => Lean.NameMap.insert s p.fst p.snd, exportEntriesFn := fun m => let r := Std.RBMap.fold (fun a n p => Array.push a (n, p)) #[] m; Array.qsort r (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size r - 1), statsFn := fun s => Std.Format.text "enumeration attribute extension" ++ Lean.Format.line ++ Std.Format.text "number of local entries: " ++ Lean.format (Std.RBMap.size s) } let attrs : List Lean.AttributeImpl := List.map (fun x => match x with | (name, descr, val) => { toAttributeImplCore := { name := name, descr := descr, applicationTime := applicationTime }, add := fun decl stx kind => do Lean.Attribute.Builtin.ensureNoArgs stx let _do_jp : PUnit → Lean.AttrM Unit := fun y => do let env ← Lean.getEnv let _do_jp : PUnit → Lean.AttrM Unit := fun y => do validate decl val Lean.setEnv (Lean.PersistentEnvExtension.addEntry ext env (decl, val)) if Option.isNone (Lean.Environment.getModuleIdxFor? env decl) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid attribute '" ++ Lean.toMessageData name ++ Lean.toMessageData "', declaration is in an imported module") _do_jp y 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 name ++ Lean.toMessageData "', must be global") _do_jp y, erase := fun decl => Lean.throwError (Lean.toMessageData "attribute cannot be erased") }) attrDescrs List.forM attrs Lean.registerBuiltinAttribute pure { attrs := attrs, ext := ext }
def
Lean.EnumAttributes.getValue
{α : Type}
[inst : Inhabited α]
(attr : Lean.EnumAttributes α)
(env : Lean.Environment)
(decl : Lean.Name)
:
Option α
Equations
- Lean.EnumAttributes.getValue attr env decl = match Lean.Environment.getModuleIdxFor? env decl with | some modIdx => match Array.binSearch (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) (decl, default) (fun a b => Lean.Name.quickLt a.fst b.fst) 0 (Array.size (Lean.PersistentEnvExtension.getModuleEntries attr.ext env modIdx) - 1) with | some (x, val) => some val | none => none | none => Lean.NameMap.find? (Lean.PersistentEnvExtension.getState attr.ext env) decl
def
Lean.EnumAttributes.setValue
{α : Type}
(attrs : Lean.EnumAttributes α)
(env : Lean.Environment)
(decl : Lean.Name)
(val : α)
:
Equations
- Lean.EnumAttributes.setValue attrs env decl val = if Option.isSome (Lean.Environment.getModuleIdxFor? env decl) = true then Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module") else if Option.isSome (Lean.NameMap.find? (Lean.PersistentEnvExtension.getState attrs.ext env) decl) = true then Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, attribute has already been set") else Except.ok (Lean.PersistentEnvExtension.addEntry attrs.ext env (decl, val))
@[inline]
Equations
@[inline]
def
Lean.registerAttributeImplBuilder
(builderId : Lean.Name)
(builder : Lean.AttributeImplBuilder)
:
Equations
- Lean.registerAttributeImplBuilder builderId builder = do let table ← ST.Ref.get Lean.attributeImplBuilderTableRef let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify Lean.attributeImplBuilderTableRef fun table => Std.HashMap.insert table builderId builder if Std.HashMap.contains table builderId = true then do let y ← throw (IO.userError ("attribute implementation builder '" ++ toString builderId ++ "' has already been declared")) _do_jp y else do let y ← pure PUnit.unit _do_jp y
Equations
- Lean.mkAttributeImplOfBuilder builderId args = do let table ← ST.Ref.get Lean.attributeImplBuilderTableRef match Std.HashMap.find? table builderId with | none => throw (IO.userError ("unknown attribute implementation builder '" ++ toString builderId ++ "'")) | some builder => IO.ofExcept (builder args)
- decl: Lean.Name → Lean.AttributeExtensionOLeanEntry
- builder: Lean.Name → List Lean.DataValue → Lean.AttributeExtensionOLeanEntry
- newEntries : List Lean.AttributeExtensionOLeanEntry
- map : Std.PersistentHashMap Lean.Name Lean.AttributeImpl
Equations
- Lean.instInhabitedAttributeExtensionState = { default := { newEntries := default, map := default } }
unsafe def
Lean.mkAttributeImplOfConstantUnsafe
(env : Lean.Environment)
(opts : Lean.Options)
(declName : Lean.Name)
:
Equations
- Lean.mkAttributeImplOfConstantUnsafe env opts declName = match Lean.Environment.find? env declName with | none => throw ("unknow constant '" ++ toString declName ++ "'") | some info => match Lean.ConstantInfo.type info with | Lean.Expr.const (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "Lean" x_2) "AttributeImpl" x_3) x x_1 => Lean.Environment.evalConst Lean.AttributeImpl env opts declName | x => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected")
@[implementedBy Lean.mkAttributeImplOfConstantUnsafe]
constant
Lean.mkAttributeImplOfConstant
(env : Lean.Environment)
(opts : Lean.Options)
(declName : Lean.Name)
:
def
Lean.mkAttributeImplOfEntry
(env : Lean.Environment)
(opts : Lean.Options)
(e : Lean.AttributeExtensionOLeanEntry)
:
Equations
- Lean.mkAttributeImplOfEntry env opts e = match e with | Lean.AttributeExtensionOLeanEntry.decl declName => IO.ofExcept (Lean.mkAttributeImplOfConstant env opts declName) | Lean.AttributeExtensionOLeanEntry.builder builderId args => Lean.mkAttributeImplOfBuilder builderId args
Equations
- Lean.isBuiltinAttribute n = do let m ← ST.Ref.get Lean.attributeMapRef pure (Std.PersistentHashMap.contains m n)
Equations
- Lean.getBuiltinAttributeNames = do let a ← ST.Ref.get Lean.attributeMapRef pure (Std.PersistentHashMap.foldl a (fun r n x => n :: r) [])
Equations
- Lean.getBuiltinAttributeImpl attrName = do let m ← ST.Ref.get Lean.attributeMapRef match Std.PersistentHashMap.find? m attrName with | some attr => pure attr | none => throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'"))
Equations
- Lean.getBuiltinAttributeApplicationTime n = do let attr ← Lean.getBuiltinAttributeImpl n pure attr.toAttributeImplCore.applicationTime
Equations
- Lean.isAttribute env attrName = Std.PersistentHashMap.contains (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map attrName
Equations
- Lean.getAttributeNames env = let m := (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map; Std.PersistentHashMap.foldl m (fun r n x => n :: r) []
Equations
- Lean.getAttributeImpl env attrName = let m := (Lean.PersistentEnvExtension.getState Lean.attributeExtension env).map; match Std.PersistentHashMap.find? m attrName with | some attr => pure attr | none => throw ("unknown attribute '" ++ toString attrName ++ "'")
def
Lean.registerAttributeOfDecl
(env : Lean.Environment)
(opts : Lean.Options)
(attrDeclName : Lean.Name)
:
Equations
- Lean.registerAttributeOfDecl env opts attrDeclName = do let attrImpl ← Lean.mkAttributeImplOfConstant env opts attrDeclName if Lean.isAttribute env attrImpl.toAttributeImplCore.name = true then throw ("invalid builtin attribute declaration, '" ++ toString attrImpl.toAttributeImplCore.name ++ "' has already been used") else pure (Lean.PersistentEnvExtension.addEntry Lean.attributeExtension env (Lean.AttributeExtensionOLeanEntry.decl attrDeclName, attrImpl))
def
Lean.registerAttributeOfBuilder
(env : Lean.Environment)
(builderId : Lean.Name)
(args : List Lean.DataValue)
:
Equations
- Lean.registerAttributeOfBuilder env builderId args = do let attrImpl ← Lean.mkAttributeImplOfBuilder builderId args if Lean.isAttribute env attrImpl.toAttributeImplCore.name = true then throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attrImpl.toAttributeImplCore.name ++ "' has already been used")) else pure (Lean.PersistentEnvExtension.addEntry Lean.attributeExtension env (Lean.AttributeExtensionOLeanEntry.builder builderId args, attrImpl))
def
Lean.Attribute.add
(declName : Lean.Name)
(attrName : Lean.Name)
(stx : Lean.Syntax)
(kind : optParam Lean.AttributeKind Lean.AttributeKind.global)
:
Equations
- Lean.Attribute.add declName attrName stx kind = do let a ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl a attrName) Lean.AttributeImpl.add attr declName stx kind
Equations
- Lean.Attribute.erase declName attrName = do let a ← Lean.getEnv let attr ← Lean.ofExcept (Lean.getAttributeImpl a attrName) Lean.AttributeImpl.erase attr declName
Equations
- Lean.updateEnvAttributesImpl env = do let map ← ST.Ref.get Lean.attributeMapRef let s ← pure (Lean.PersistentEnvExtension.getState Lean.attributeExtension env) let s : Lean.AttributeExtensionState := Std.PersistentHashMap.foldl map (fun s attrName attrImpl => if Std.PersistentHashMap.contains s.map attrName = true then s else { newEntries := s.newEntries, map := Std.PersistentHashMap.insert s.map attrName attrImpl }) s pure (Lean.PersistentEnvExtension.setState Lean.attributeExtension env s)
Equations
- Lean.getNumBuiltiAttributesImpl = do let a ← ST.Ref.get Lean.attributeMapRef pure a.size