bookshelf/DocGen4/Process/DocInfo.lean

224 lines
6.7 KiB
Plaintext
Raw Permalink Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.AxiomInfo
import DocGen4.Process.TheoremInfo
import DocGen4.Process.OpaqueInfo
import DocGen4.Process.InstanceInfo
import DocGen4.Process.DefinitionInfo
import DocGen4.Process.ClassInfo
import DocGen4.Process.StructureInfo
import DocGen4.Process.InductiveInfo
namespace DocGen4.Process
namespace DocInfo
open Lean Meta Widget
def getDeclarationRange : DocInfo → DeclarationRange
| axiomInfo i => i.declarationRange
| theoremInfo i => i.declarationRange
| opaqueInfo i => i.declarationRange
| definitionInfo i => i.declarationRange
| instanceInfo i => i.declarationRange
| inductiveInfo i => i.declarationRange
| structureInfo i => i.declarationRange
| classInfo i => i.declarationRange
| classInductiveInfo i => i.declarationRange
| ctorInfo i => i.declarationRange
def getName : DocInfo → Name
| axiomInfo i => i.name
| theoremInfo i => i.name
| opaqueInfo i => i.name
| definitionInfo i => i.name
| instanceInfo i => i.name
| inductiveInfo i => i.name
| structureInfo i => i.name
| classInfo i => i.name
| classInductiveInfo i => i.name
| ctorInfo i => i.name
def getKind : DocInfo → String
| axiomInfo _ => "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo _ => "opaque"
| definitionInfo _ => "def"
| instanceInfo _ => "instance"
| inductiveInfo _ => "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class"
| classInductiveInfo _ => "class"
| ctorInfo _ => "ctor" -- TODO: kind ctor support in js
def getType : DocInfo → CodeWithInfos
| axiomInfo i => i.type
| theoremInfo i => i.type
| opaqueInfo i => i.type
| definitionInfo i => i.type
| instanceInfo i => i.type
| inductiveInfo i => i.type
| structureInfo i => i.type
| classInfo i => i.type
| classInductiveInfo i => i.type
| ctorInfo i => i.type
def getArgs : DocInfo → Array Arg
| axiomInfo i => i.args
| theoremInfo i => i.args
| opaqueInfo i => i.args
| definitionInfo i => i.args
| instanceInfo i => i.args
| inductiveInfo i => i.args
| structureInfo i => i.args
| classInfo i => i.args
| classInductiveInfo i => i.args
| ctorInfo 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
| ctorInfo i => i.attrs
def getDocString : DocInfo → Option String
| axiomInfo i => i.doc
| theoremInfo i => i.doc
| opaqueInfo i => i.doc
| definitionInfo i => i.doc
| instanceInfo i => i.doc
| inductiveInfo i => i.doc
| structureInfo i => i.doc
| classInfo i => i.doc
| classInductiveInfo i => i.doc
| ctorInfo i => i.doc
def shouldRender : DocInfo → Bool
| axiomInfo i => i.render
| theoremInfo i => i.render
| opaqueInfo i => i.render
| definitionInfo i => i.render
| instanceInfo i => i.render
| inductiveInfo i => i.render
| structureInfo i => i.render
| classInfo i => i.render
| classInductiveInfo i => i.render
| ctorInfo i => i.render
def isBlackListed (declName : Name) : MetaM Bool := do
match ← findDeclarationRanges? declName with
| some _ =>
let env ← getEnv
pure (declName.isInternal)
<||> (pure <| isAuxRecursor env declName)
<||> (pure <| isNoConfusion env declName)
<||> isRec declName
<||> isMatcher declName
-- TODO: Evaluate whether filtering out declarations without range is sensible
| none => return true
-- TODO: Is this actually the best way?
def isProjFn (declName : Name) : MetaM Bool := do
let env ← getEnv
match declName with
| Name.str parent name =>
if isStructure env parent then
match getStructureInfo? env parent with
| some i =>
match i.fieldNames.find? (· == name) with
| some _ => return true
| none => return false
| none => panic! s!"{parent} is not a structure"
else
return false
| _ => return false
def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do
if ← isBlackListed name then
return none
match info with
| ConstantInfo.axiomInfo i => return some <| axiomInfo (← AxiomInfo.ofAxiomVal i)
| ConstantInfo.thmInfo i => return some <| theoremInfo (← TheoremInfo.ofTheoremVal i)
| ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
| ConstantInfo.defnInfo i =>
if ← isProjFn i.name then
let info ← DefinitionInfo.ofDefinitionVal i
return some <| definitionInfo { info with render := false }
else
if ← isInstance i.name then
let info ← InstanceInfo.ofDefinitionVal i
return some <| instanceInfo info
else
let info ← DefinitionInfo.ofDefinitionVal i
return some <| definitionInfo info
| ConstantInfo.inductInfo i =>
let env ← getEnv
if isStructure env i.name then
if isClass env i.name then
return some <| classInfo (← ClassInfo.ofInductiveVal i)
else
return some <| structureInfo (← StructureInfo.ofInductiveVal i)
else
if isClass env i.name then
return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i)
else
return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i)
| ConstantInfo.ctorInfo i =>
let info ← Info.ofConstantVal i.toConstantVal
return some <| ctorInfo { info with render := false }
-- we ignore these for now
| ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
def getKindDescription : DocInfo → String
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo i =>
match i.definitionSafety with
| DefinitionSafety.safe => "opaque"
| DefinitionSafety.unsafe => "unsafe opaque"
| DefinitionSafety.partial => "partial def"
| definitionInfo i => Id.run do
let mut modifiers := #[]
if i.isUnsafe then
modifiers := modifiers.push "unsafe"
if i.isNonComputable then
modifiers := modifiers.push "noncomputable"
let defKind :=
if i.hints.isAbbrev then
"abbrev"
else
"def"
modifiers := modifiers.push defKind
return String.intercalate " " modifiers.toList
| instanceInfo i => Id.run do
let mut modifiers := #[]
if i.isUnsafe then
modifiers := modifiers.push "unsafe"
if i.isNonComputable then
modifiers := modifiers.push "noncomputable"
modifiers := modifiers.push "instance"
return String.intercalate " " modifiers.toList
| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class"
| classInductiveInfo _ => "class inductive"
| ctorInfo _ => "constructor"
end DocInfo
end DocGen4.Process