bookshelf-doc/DocGen4/Process.lean

295 lines
10 KiB
Plaintext
Raw 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) 2021 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 Lean.PrettyPrinter
import Std.Data.HashMap
import Lean.Meta.SynthInstance
namespace DocGen4
open Lean Meta PrettyPrinter Std
structure NameInfo where
name : Name
type : Syntax
deriving Repr
def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do
s!"{i.name} : {←PrettyPrinter.formatTerm i.type}"
structure Info extends NameInfo where
doc : Option String
declarationRange : DeclarationRange
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
structure DefinitionInfo extends Info where
--value : Syntax
unsafeInformation : DefinitionSafety
hints : ReducibilityHints
abbrev InstanceInfo := DefinitionInfo
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
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
structure StructureInfo extends Info where
fieldInfo : Array FieldInfo
parents : Array Name
ctor : NameInfo
deriving Repr
structure ClassInfo extends StructureInfo where
hasOutParam : Bool
instances : Array Syntax
deriving Repr
inductive DocInfo where
| axiomInfo (info : AxiomInfo) : DocInfo
| theoremInfo (info : TheoremInfo) : DocInfo
| opaqueInfo (info : OpaqueInfo) : DocInfo
| definitionInfo (info : DefinitionInfo) : DocInfo
| instanceInfo (info : InstanceInfo) : DocInfo
| inductiveInfo (info : InductiveInfo) : DocInfo
| structureInfo (info : StructureInfo) : DocInfo
| classInfo (info : ClassInfo) : DocInfo
structure Module where
name : Name
doc : Option String
members : Array DocInfo
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
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
def isInstance (declName : Name) : MetaM Bool := do
(instanceExtension.getState (←getEnv)).instanceNames.contains declName
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
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))
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?
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⟩
| none => panic! s!"{v.name} is not a structure"
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
let sinfo ← StructureInfo.ofInductiveVal v
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
namespace DocInfo
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
-- 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
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 =>
if ← (isProjFn i.name) then
none
else
let info ← DefinitionInfo.ofDefinitionVal i
if (←isInstance i.name) then
some $ instanceInfo info
else
some $ definitionInfo info
-- TODO: Differentiate between all the different types of inductives (structures, classes etc.)
| ConstantInfo.inductInfo i =>
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)
else
some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
-- 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}"
| inductiveInfo i =>
let ctorString ← i.ctors.mapM NameInfo.prettyPrint
s!"inductive {←i.toNameInfo.prettyPrint}, ctors: {ctorString}, doc string: {i.doc}"
| 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}"
| 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}"
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 #[])
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"
| none => ()
return res
end DocGen4