feat: Attributes

main
Henrik Böving 2022-02-13 03:32:53 +01:00
parent 59e50943d6
commit d700da7284
4 changed files with 147 additions and 8 deletions

View File

@ -9,3 +9,4 @@ import DocGen4.Load
import DocGen4.ToHtmlFormat
import DocGen4.IncludeStr
import DocGen4.Output
import DocGen4.Attributes

110
DocGen4/Attributes.lean Normal file
View File

@ -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

View File

@ -72,7 +72,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
pure <div «class»="decl_header"> [nodes] </div>
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
<div «class»="decl" id={doc.getName.toString}>
<div «class»={doc.getKind}>
<div «class»="gh_link">
<a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
</div>
-- TODO: Attributes
[attrsHtml]
{←docInfoHeader doc}
[doc_html]
[docHtml]
</div>
</div>

View File

@ -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