bookshelf-doc/DocGen4/Process.lean

295 lines
10 KiB
Plaintext
Raw Normal View History

2021-12-10 12:29:04 +00:00
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
2021-11-27 15:19:56 +00:00
import Lean
import Lean.PrettyPrinter
import Std.Data.HashMap
2021-12-03 19:37:25 +00:00
import Lean.Meta.SynthInstance
2021-11-27 15:19:56 +00:00
namespace DocGen4
open Lean Meta PrettyPrinter Std
2021-11-27 15:19:56 +00:00
structure NameInfo where
name : Name
2021-11-27 15:19:56 +00:00
type : Syntax
deriving Repr
def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do
s!"{i.name} : {←PrettyPrinter.formatTerm i.type}"
structure Info extends NameInfo where
2021-11-27 15:19:56 +00:00
doc : Option String
declarationRange : DeclarationRange
2021-11-27 15:19:56 +00:00
deriving Repr
structure AxiomInfo extends Info where
isUnsafe : Bool
deriving Repr
structure TheoremInfo extends Info where
deriving Repr
structure OpaqueInfo extends Info where
value : Syntax
isUnsafe : Bool
deriving Repr
2021-12-01 17:25:22 +00:00
structure DefinitionInfo extends Info where
--value : Syntax
unsafeInformation : DefinitionSafety
hints : ReducibilityHints
2021-12-03 19:37:25 +00:00
abbrev InstanceInfo := DefinitionInfo
2021-12-01 17:25:22 +00:00
structure InductiveInfo extends Info where
numParams : Nat -- Number of parameters
numIndices : Nat -- Number of indices
all : List Name -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
ctors : List NameInfo -- List of all constructors and their type for this inductive datatype
2021-12-01 17:25:22 +00:00
isRec : Bool -- `true` Iff it is recursive
isUnsafe : Bool
isReflexive : Bool
isNested : Bool
deriving Repr
structure FieldInfo extends NameInfo where
projFn : Name
subobject? : Option Name
deriving Repr
2021-12-02 09:34:20 +00:00
structure StructureInfo extends Info where
fieldInfo : Array FieldInfo
2021-12-02 09:34:20 +00:00
parents : Array Name
ctor : NameInfo
2021-12-02 09:34:20 +00:00
deriving Repr
2021-12-02 10:17:46 +00:00
structure ClassInfo extends StructureInfo where
hasOutParam : Bool
2021-12-03 19:37:25 +00:00
instances : Array Syntax
deriving Repr
2021-12-02 10:17:46 +00:00
2021-11-27 15:19:56 +00:00
inductive DocInfo where
| axiomInfo (info : AxiomInfo) : DocInfo
| theoremInfo (info : TheoremInfo) : DocInfo
| opaqueInfo (info : OpaqueInfo) : DocInfo
2021-12-01 17:25:22 +00:00
| definitionInfo (info : DefinitionInfo) : DocInfo
2021-12-03 19:37:25 +00:00
| instanceInfo (info : InstanceInfo) : DocInfo
2021-12-01 17:25:22 +00:00
| inductiveInfo (info : InductiveInfo) : DocInfo
2021-12-02 09:34:20 +00:00
| structureInfo (info : StructureInfo) : DocInfo
2021-12-02 10:17:46 +00:00
| classInfo (info : ClassInfo) : DocInfo
2021-11-27 15:19:56 +00:00
structure Module where
name : Name
doc : Option String
members : Array DocInfo
2021-12-01 17:25:22 +00:00
deriving Inhabited
def prettyPrintTerm (expr : Expr) : MetaM Syntax := do
let ((expr, _), _) ← Elab.Term.TermElabM.run $ Elab.Term.levelMVarToParam (←instantiateMVars expr)
let term ← delab Name.anonymous [] expr
parenthesizeTerm term
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let env ← getEnv
2021-12-03 19:37:25 +00:00
let type ← prettyPrintTerm v.type
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 => return Info.mk ⟨v.name, type⟩ doc range.range
| none => panic! s!"{v.name} is a declaration without position"
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
let info ← Info.ofConstantVal v.toConstantVal
return AxiomInfo.mk info v.isUnsafe
def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
let info ← Info.ofConstantVal v.toConstantVal
return TheoremInfo.mk info
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let value ← prettyPrintTerm v.value
return OpaqueInfo.mk info value v.isUnsafe
2021-12-03 19:37:25 +00:00
def isInstance (declName : Name) : MetaM Bool := do
(instanceExtension.getState (←getEnv)).instanceNames.contains declName
2021-12-01 17:25:22 +00:00
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal
-- Elaborating the value yields weird exceptions
--let value ← prettyPrintTerm v.value
return DefinitionInfo.mk info v.safety v.hints
def getConstructorType (ctor : Name) : MetaM Syntax := do
let env ← getEnv
match env.find? ctor with
| some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type
| _ => panic! s!"Constructor {ctor} was requested but does not exist"
-- TODO: Obtain parameters that come after the inductive Name
2021-12-01 17:25:22 +00:00
def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
2021-12-01 17:25:22 +00:00
return InductiveInfo.mk info v.numParams v.numIndices v.all ctors v.isRec v.isUnsafe v.isReflexive v.isNested
def getFieldTypeAux (type : Expr) (vars : List Name) : (Expr × List Name) :=
match type with
| Expr.forallE `self _ b .. => (b, (`self :: vars))
| Expr.forallE n _ b .. => getFieldTypeAux b (n :: vars)
| _ => (type, vars)
def getFieldType (projFn : Name) : MetaM Expr := do
let fn ← mkConstWithFreshMVarLevels projFn
let type ← inferType fn
let (type, vars) := getFieldTypeAux type []
type.instantiate $ vars.toArray.map mkConst
def FieldInfo.ofStructureFieldInfo (i : StructureFieldInfo) : MetaM FieldInfo := do
let type ← getFieldType i.projFn
let ni := NameInfo.mk i.fieldName (←prettyPrintTerm type)
FieldInfo.mk ni i.projFn i.subobject?
2021-12-02 09:34:20 +00:00
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let parents := getParentStructures env v.name
let ctor := getStructureCtor env v.name |>.name
let ctorType ← getConstructorType ctor
match getStructureInfo? env v.name with
| some i =>
let fieldInfos ← i.fieldInfo.mapM FieldInfo.ofStructureFieldInfo
return StructureInfo.mk info fieldInfos parents ⟨ctor, ctorType⟩
2021-12-02 09:34:20 +00:00
| none => panic! s!"{v.name} is not a structure"
2021-12-02 10:17:46 +00:00
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
let sinfo ← StructureInfo.ofInductiveVal v
2021-12-03 19:37:25 +00:00
let fn ← mkConstWithFreshMVarLevels v.name
let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
let insts ← SynthInstance.getInstances (mkAppN fn xs)
let insts_stx ← insts.mapM prettyPrintTerm
return ClassInfo.mk sinfo (hasOutParams (←getEnv) v.name) insts_stx
2021-12-02 10:17:46 +00:00
2021-11-27 15:19:56 +00:00
namespace DocInfo
2021-12-02 09:34:20 +00:00
def isBlackListed (declName : Name) : MetaM Bool := do
match ←findDeclarationRanges? declName with
| some _ =>
let env ← getEnv
declName.isInternal
<||> isAuxRecursor env declName
<||> isNoConfusion env declName
<||> isRec declName
<||> isMatcher declName
-- TODO: Evaluate whether filtering out declarations without range is sensible
| none => true
2021-11-27 15:19:56 +00:00
-- 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 _ => true
| none => false
| none => panic! s!"{parent} is not a structure"
else
false
| _ => false
2021-12-01 17:25:22 +00:00
2021-11-27 15:19:56 +00:00
def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
if (←isBlackListed name) then
return none
match info with
| ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i)
| ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i)
| ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
-- TODO: Find a way to extract equations nicely
| ConstantInfo.defnInfo i =>
2021-12-03 19:37:25 +00:00
if ← (isProjFn i.name) then
none
else
2021-12-03 19:37:25 +00:00
let info ← DefinitionInfo.ofDefinitionVal i
if (←isInstance i.name) then
some $ instanceInfo info
else
some $ definitionInfo info
2021-11-27 15:19:56 +00:00
-- TODO: Differentiate between all the different types of inductives (structures, classes etc.)
2021-12-02 09:34:20 +00:00
| ConstantInfo.inductInfo i =>
2021-12-02 10:17:46 +00:00
let env ← getEnv
if isStructure env i.name then
if isClass env i.name then
some $ classInfo (←ClassInfo.ofInductiveVal i)
else
some $ structureInfo (←StructureInfo.ofInductiveVal i)
2021-12-02 09:34:20 +00:00
else
some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
2021-11-27 15:19:56 +00:00
-- we ignore these for now
| ConstantInfo.ctorInfo i => none
| ConstantInfo.recInfo i => none
| ConstantInfo.quotInfo i => none
def prettyPrint (i : DocInfo) : CoreM String := do
match i with
| axiomInfo i => s!"axiom {←i.toNameInfo.prettyPrint}, doc string: {i.doc}"
| theoremInfo i => s!"theorem {←i.toNameInfo.prettyPrint}, doc string: {i.doc}"
| opaqueInfo i => s!"constant {←i.toNameInfo.prettyPrint}, doc string: {i.doc}"
| definitionInfo i => s!"def {←i.toNameInfo.prettyPrint}, doc string: {i.doc}"
| instanceInfo i => s!"instance {←i.toNameInfo.prettyPrint}, doc string: {i.doc}"
2021-12-01 17:25:22 +00:00
| inductiveInfo i =>
let ctorString ← i.ctors.mapM NameInfo.prettyPrint
s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}"
2021-12-02 09:34:20 +00:00
| structureInfo i =>
let ctorString ← i.ctor.prettyPrint
let fieldString ← i.fieldInfo.mapM (λ f => do s!"{f.name} : {←PrettyPrinter.formatTerm f.type}")
s!"structure {←i.toNameInfo.prettyPrint} extends {i.parents}, ctor: {ctorString}, fields : {fieldString}, doc string: {i.doc}"
2021-12-02 10:17:46 +00:00
| classInfo i =>
let instanceString ← i.instances.mapM PrettyPrinter.formatTerm
let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo)
s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}"
2021-11-27 15:19:56 +00:00
end DocInfo
namespace Module
def prettyPrint (m : Module) : CoreM String := do
let pretty := s!"Module {m.name}, doc string: {m.doc} with members:\n"
Array.foldlM (λ p mem => return p ++ " " ++ (←mem.prettyPrint) ++ "\n") pretty m.members
end Module
def process : MetaM (HashMap Name Module) := do
let env ← getEnv
let mut res := mkHashMap env.header.moduleNames.size
for module in env.header.moduleNames do
-- TODO: Check why modules can have multiple doc strings and add that later on
let moduleDoc := match getModuleDoc? env module with
| none => none
| some #[] => none
| some doc => doc.get! 0
res := res.insert module (Module.mk module moduleDoc #[])
2021-11-27 15:19:56 +00:00
for cinfo in env.constants.toList do
let d := ←DocInfo.ofConstant cinfo
match d with
| some dinfo =>
match (env.getModuleIdxFor? cinfo.fst) with
| some modidx =>
-- TODO: Check whether this is still efficient
let moduleName := env.allImportedModuleNames.get! modidx
let module := res.find! moduleName
res := res.insert moduleName {module with members := module.members.push dinfo}
| none => panic! "impossible"
2021-11-27 15:19:56 +00:00
| none => ()
return res
end DocGen4