bookshelf-doc/DocGen4/Process/Attributes.lean

183 lines
6.3 KiB
Plaintext
Raw Normal View History

2022-02-13 02:32:53 +00:00
import Lean
namespace DocGen4
open Lean Meta
-- The following is probably completely overengineered but I love it
2022-05-20 07:41:52 +00:00
/--
Captures the notion of a value based attributes, `attrKind` is things like
`EnumAttributes`.
-/
2022-02-13 02:32:53 +00:00
class ValueAttr (attrKind : Type → Type) where
2022-05-20 07:41:52 +00:00
/--
Given a certain value based attribute, an `Environment` and the `Name` of
a declaration returns the value of the attribute on this declaration if present.
-/
2022-02-13 02:32:53 +00:00
getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
2022-05-20 07:41:52 +00:00
/--
Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).
-/
2022-02-13 02:32:53 +00:00
structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
{α : Type}
attr : attrKind α
[str : ToString α]
[inhab : Inhabited α]
2022-05-20 07:41:52 +00:00
/--
Obtain the value of an enum attribute for a certain name.
-/
2022-05-21 10:50:55 +00:00
def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := do
2022-02-13 02:32:53 +00:00
let val ← EnumAttributes.getValue attr env decl
some (toString val)
instance : ValueAttr EnumAttributes where
getValue := enumGetValue
2022-05-20 07:41:52 +00:00
/--
Obtain the value of a parametric attribute for a certain name.
-/
2022-05-21 10:50:55 +00:00
def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
let val ← ParametricAttribute.getParam? attr env decl
2022-02-13 02:32:53 +00:00
some (attr.attr.name.toString ++ " " ++ toString val)
instance : ValueAttr ParametricAttribute where
getValue := parametricGetValue
abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
2022-05-20 07:41:52 +00:00
/--
The list of all tag based attributes doc-gen knows about and can recover.
-/
2022-04-19 18:28:30 +00:00
def tagAttributes : Array TagAttribute :=
2023-04-16 07:54:48 +00:00
#[IR.UnboxResult.unboxAttr, neverExtractAttr,
Elab.Term.elabWithoutExpectedTypeAttr, matchPatternAttr]
2022-02-13 02:32:53 +00:00
deriving instance Repr for Compiler.InlineAttributeKind
deriving instance Repr for Compiler.SpecializeAttributeKind
open Compiler in
instance : ToString InlineAttributeKind where
toString kind :=
match kind with
| .inline => "inline"
| .noinline => "noinline"
| .macroInline => "macro_inline"
| .inlineIfReduce => "inline_if_reduce"
| .alwaysInline => "always_inline"
2022-02-13 02:32:53 +00:00
open Compiler in
instance : ToString SpecializeAttributeKind where
toString kind :=
match kind with
| .specialize => "specialize"
| .nospecialize => "nospecialize"
instance : ToString ReducibilityStatus where
toString kind :=
match kind with
| .reducible => "reducible"
| .semireducible => "semireducible"
| .irreducible => "irreducible"
2022-02-13 02:32:53 +00:00
2022-05-20 07:41:52 +00:00
/--
The list of all enum based attributes doc-gen knows about and can recover.
-/
@[reducible]
def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
2022-02-13 02:32:53 +00:00
instance : ToString ExternEntry where
toString entry :=
match entry with
| .adhoc `all => ""
| .adhoc backend => s!"{backend} adhoc"
| .standard `all fn => fn
| .standard backend fn => s!"{backend} {fn}"
| .inline backend pattern => s!"{backend} inline {String.quote pattern}"
2022-02-13 02:32:53 +00:00
-- TODO: The docs in the module dont specific how to render this
| .foreign backend fn => s!"{backend} foreign {fn}"
2022-02-13 02:32:53 +00:00
instance : ToString ExternAttrData where
2022-02-16 20:24:42 +00:00
toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
2022-02-13 02:32:53 +00:00
2022-05-20 07:41:52 +00:00
/--
The list of all parametric attributes (that is, attributes with any kind of information attached)
doc-gen knows about and can recover.
-/
def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩, ⟨Compiler.specializeAttr⟩]
2022-02-13 02:32:53 +00:00
def getTags (decl : Name) : MetaM (Array String) := do
let env ← getEnv
return tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (·.attr.name.toString)
2022-02-13 02:32:53 +00:00
def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
let env ← getEnv
return va.getValue attr env decl
2022-02-13 02:32:53 +00:00
def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
let mut res := #[]
for attr in attrs do
if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
res := res.push val
return res
2022-02-13 02:32:53 +00:00
def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
2023-09-08 21:06:56 +00:00
def getParametricValues (decl : Name) : MetaM (Array String) := do
let mut uniform ← getValues decl parametricAttributes
-- This attribute contains an `Option Name` but we would like to pretty print it better
if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
let str := match depTag with
| some alt => s!"deprecated {alt.toString}"
| none => "deprecated"
uniform := uniform.push str
return uniform
2022-02-13 02:32:53 +00:00
def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
let insts ← getDefaultInstances className
for (inst, prio) in insts do
if inst == decl then
2022-07-23 11:01:25 +00:00
return some s!"defaultInstance {prio}"
return none
2022-02-13 02:32:53 +00:00
2022-04-19 18:28:30 +00:00
def hasSimp (decl : Name) : MetaM (Option String) := do
2022-02-13 02:32:53 +00:00
let thms ← simpExtension.getTheorems
if thms.isLemma (.decl decl) then
return "simp"
else
return none
2022-04-19 18:28:30 +00:00
def hasCsimp (decl : Name) : MetaM (Option String) := do
let env ← getEnv
if Compiler.hasCSimpAttribute env decl then
return some "csimp"
else
return none
2022-04-19 18:28:30 +00:00
2022-05-20 07:41:52 +00:00
/--
The list of custom attributes, that don't fit in the parametric or enum
attribute kinds, doc-gen konws about and can recover.
-/
2022-04-19 18:28:30 +00:00
def customAttrs := #[hasSimp, hasCsimp]
def getCustomAttrs (decl : Name) : MetaM (Array String) := do
let mut values := #[]
for attr in customAttrs do
if let some value ← attr decl then
values := values.push value
return values
2022-02-13 02:32:53 +00:00
2022-05-20 07:41:52 +00:00
/--
The main entry point for recovering all attribute values for a given
declaration.
-/
2022-02-13 02:32:53 +00:00
def getAllAttributes (decl : Name) : MetaM (Array String) := do
let tags ← getTags decl
let enums ← getEnumValues decl
let parametric ← getParametricValues decl
2022-04-19 18:28:30 +00:00
let customs ← getCustomAttrs decl
return customs ++ tags ++ enums ++ parametric
2022-02-13 02:32:53 +00:00
end DocGen4