diff --git a/DocGen4.lean b/DocGen4.lean
index bc6d9b6..e91e7c7 100644
--- a/DocGen4.lean
+++ b/DocGen4.lean
@@ -9,3 +9,4 @@ import DocGen4.Load
import DocGen4.ToHtmlFormat
import DocGen4.IncludeStr
import DocGen4.Output
+import DocGen4.Attributes
diff --git a/DocGen4/Attributes.lean b/DocGen4/Attributes.lean
new file mode 100644
index 0000000..474e175
--- /dev/null
+++ b/DocGen4/Attributes.lean
@@ -0,0 +1,110 @@
+import Lean
+
+namespace DocGen4
+
+open Lean Meta
+
+-- The following is probably completely overengineered but I love it
+class ValueAttr (attrKind : Type → Type) where
+ getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
+
+structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
+ {α : Type}
+ attr : attrKind α
+ [str : ToString α]
+ [inhab : Inhabited α]
+
+def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+ let val ← EnumAttributes.getValue attr env decl
+ some (toString val)
+
+instance : ValueAttr EnumAttributes where
+ getValue := enumGetValue
+
+def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+ let val ← ParametricAttribute.getParam attr env decl
+ some (attr.attr.name.toString ++ " " ++ toString val)
+
+instance : ValueAttr ParametricAttribute where
+ getValue := parametricGetValue
+
+abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
+abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
+
+def tagAttributes : Array TagAttribute := #[IR.UnboxResult.unboxAttr, neverExtractAttr, Elab.Term.elabWithoutExpectedTypeAttr, SynthInstance.inferTCGoalsRLAttr, matchPatternAttr]
+
+deriving instance Repr for Compiler.InlineAttributeKind
+deriving instance Repr for Compiler.SpecializeAttributeKind
+
+open Compiler in
+instance : ToString InlineAttributeKind where
+ toString kind :=
+ match kind with
+ | InlineAttributeKind.inline => "inline"
+ | InlineAttributeKind.noinline => "noinline"
+ | InlineAttributeKind.macroInline => "macroInline"
+ | InlineAttributeKind.inlineIfReduce => "inlineIfReduce"
+
+open Compiler in
+instance : ToString SpecializeAttributeKind where
+ toString kind :=
+ match kind with
+ | SpecializeAttributeKind.specialize => "specialize"
+ | SpecializeAttributeKind.nospecialize => "nospecialize"
+
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨Compiler.specializeAttrs⟩]
+
+instance : ToString ExternEntry where
+ toString entry :=
+ match entry with
+ | ExternEntry.adhoc `all => ""
+ | ExternEntry.adhoc backend => s!"{backend} adhoc"
+ | ExternEntry.standard `all fn => fn
+ | ExternEntry.standard backend fn => s!"{backend} {fn}"
+ | ExternEntry.inline backend pattern => s!"{backend} inline {String.quote pattern}"
+ -- TODO: The docs in the module dont specific how to render this
+ | ExternEntry.foreign backend fn => s!"{backend} foreign {fn}"
+
+instance : ToString ExternAttrData where
+ toString data := (data.arity?.map toString |>.getD "") ++ String.intercalate " " (data.entries.map toString)
+
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩]
+
+def getTags (decl : Name) : MetaM (Array String) := do
+ let env ← getEnv
+ pure $ tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (λ t => t.attr.name.toString)
+
+def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
+ let env ← getEnv
+ pure $ va.getValue attr env decl
+
+def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
+ let env ← getEnv
+ 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
+ pure res
+
+def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
+def getParametricValues (decl : Name) : MetaM (Array String) := getValues decl parametricAttributes
+
+def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
+ let insts ← getDefaultInstances className
+ for (inst, prio) in insts do
+ if inst == decl then
+ return some $ s!"defaultInstance {prio}"
+ pure none
+
+def hasSimp (decl : Name) : MetaM (Bool) := do
+ let thms ← simpExtension.getTheorems
+ pure $ thms.isLemma decl
+
+def getAllAttributes (decl : Name) : MetaM (Array String) := do
+ let tags ← getTags decl
+ let enums ← getEnumValues decl
+ let parametric ← getParametricValues decl
+ let simp := if ←hasSimp decl then #["simp"] else #[]
+ pure $ simp ++ tags ++ enums ++ parametric
+
+end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 94d7827..eef3186 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -72,7 +72,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
pure
[nodes]
def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
- let doc_html ← match doc with
+ let docHtml ← match doc with
| DocInfo.inductiveInfo i => inductiveToHtml i
| DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i
@@ -81,15 +81,23 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.classInductiveInfo i => classInductiveToHtml i
| _ => pure #[]
+ let attrs := doc.getAttrs
+ let attrsHtml :=
+ if attrs.size > 0 then
+ let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
+ #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+ else
+ #[]
+
pure
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index cb3df71..8435845 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -10,6 +10,7 @@ import Std.Data.HashMap
import Lean.Meta.SynthInstance
import DocGen4.Hierarchy
+import DocGen4.Attributes
namespace DocGen4
@@ -29,6 +30,7 @@ structure Info extends NameInfo where
args : Array Arg
doc : Option String
declarationRange : DeclarationRange
+ attrs : Array String
deriving Inhabited
structure AxiomInfo extends Info where
@@ -151,7 +153,7 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let doc ← findDocString? env v.name
match ←findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future
- | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range
+ | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range (←getAllAttributes v.name)
| none => panic! s!"{v.name} is a declaration without position"
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
@@ -223,6 +225,14 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+ let info ← DefinitionInfo.ofDefinitionVal v
+ let some className := getClassName (←getEnv) v.type | unreachable!
+ if let some instAttr ← getDefaultInstance v.name className then
+ pure { info with attrs := info.attrs.push instAttr }
+ else
+ pure info
+
def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
let env ← getEnv
match env.find? ctor with
@@ -322,11 +332,12 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name,
if ← (isProjFn i.name) then
pure none
else
- let info ← DefinitionInfo.ofDefinitionVal i
if (←isInstance i.name) then
+ let info ← InstanceInfo.ofDefinitionVal i
pure <| some <| instanceInfo info
else
- pure <| some <| definitionInfo info
+ let info ← DefinitionInfo.ofDefinitionVal i
+ pure <| some <| definitionInfo info
| ConstantInfo.inductInfo i =>
let env ← getEnv
if isStructure env i.name then
@@ -422,6 +433,17 @@ def getArgs : DocInfo → Array Arg
| classInfo i => i.args
| classInductiveInfo i => i.args
+def getAttrs : DocInfo → Array String
+| axiomInfo i => i.attrs
+| theoremInfo i => i.attrs
+| opaqueInfo i => i.attrs
+| definitionInfo i => i.attrs
+| instanceInfo i => i.attrs
+| inductiveInfo i => i.attrs
+| structureInfo i => i.attrs
+| classInfo i => i.attrs
+| classInductiveInfo i => i.attrs
+
end DocInfo
structure AnalyzerResult where
@@ -475,6 +497,4 @@ def process : MetaM AnalyzerResult := do
importAdj := adj
}
-
-
end DocGen4