bookshelf-doc/DocGen4/Process.lean

374 lines
12 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-12-12 12:21:53 +00:00
import DocGen4.Hierarchy
2021-11-27 15:19:56 +00:00
namespace DocGen4
open Lean Meta PrettyPrinter Std Widget
structure NameInfo where
name : Name
type : CodeWithInfos
deriving Inhabited
structure Arg where
name : Name
type : CodeWithInfos
binderInfo : BinderInfo
structure Info extends NameInfo where
args : Array Arg
2021-11-27 15:19:56 +00:00
doc : Option String
declarationRange : DeclarationRange
deriving Inhabited
2021-11-27 15:19:56 +00:00
structure AxiomInfo extends Info where
isUnsafe : Bool
deriving Inhabited
2021-11-27 15:19:56 +00:00
structure TheoremInfo extends Info
deriving Inhabited
2021-11-27 15:19:56 +00:00
structure OpaqueInfo extends Info where
value : CodeWithInfos
2021-11-27 15:19:56 +00:00
isUnsafe : Bool
deriving Inhabited
2021-11-27 15:19:56 +00:00
2021-12-01 17:25:22 +00:00
structure DefinitionInfo extends Info where
--value : CodeWithInfos
2021-12-01 17:25:22 +00:00
unsafeInformation : DefinitionSafety
hints : ReducibilityHints
deriving Inhabited
2021-12-01 17:25:22 +00:00
2021-12-03 19:37:25 +00:00
abbrev InstanceInfo := DefinitionInfo
2021-12-01 17:25:22 +00:00
structure InductiveInfo extends Info where
ctors : List NameInfo -- List of all constructors and their type for this inductive datatype
2021-12-01 17:25:22 +00:00
isUnsafe : Bool
deriving Inhabited
2021-12-01 17:25:22 +00:00
2021-12-02 09:34:20 +00:00
structure StructureInfo extends Info where
fieldInfo : Array NameInfo
2021-12-02 09:34:20 +00:00
parents : Array Name
ctor : NameInfo
deriving Inhabited
2021-12-02 09:34:20 +00:00
2021-12-02 10:17:46 +00:00
structure ClassInfo extends StructureInfo where
2022-01-06 13:51:46 +00:00
instances : Array Name
deriving Inhabited
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
deriving Inhabited
2021-11-27 15:19:56 +00:00
namespace DocInfo
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
def lineOrder (l r : DocInfo) : Bool :=
l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
end DocInfo
structure Module where
name : Name
doc : Option String
-- Sorted according to their line numbers
members : Array DocInfo
2021-12-01 17:25:22 +00:00
deriving Inhabited
partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
let helper := λ name type body data =>
-- Once we hit a name with a macro scope we stop traversing the expression
-- and print what is left after the : instead. The only exception
-- to this is instances since these almost never have a name
-- but should still be printed as arguments instead of after the :.
if name.hasMacroScopes ∧ ¬data.binderInfo.isInstImplicit then
(#[], e)
else
let name := name.eraseMacroScopes
let arg := (name, type, data.binderInfo)
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final)
match e.consumeMData with
| Expr.lam name type body data => helper name type body data
| Expr.forallE name type body data => helper name type body data
| _ => (#[], e)
def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
let (fmt, infos) ← formatInfos expr
let tt := TaggedText.prettyTagged fmt
let ctx := {
env := ← getEnv
mctx := ← getMCtx
options := ← getOptions
currNamespace := ← getCurrNamespace
openDecls := ← getOpenDecls
2022-01-16 13:22:53 +00:00
fileMap := default
}
tagExprInfos ctx infos tt
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let env ← getEnv
let (args, type) := typeToArgsType v.type
let type ← prettyPrintTerm type
let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b)
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⟩ args 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 t ← prettyPrintTerm v.value
return OpaqueInfo.mk info t 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 CodeWithInfos := do
2021-12-01 17:25:22 +00:00
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"
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 ctors v.isUnsafe
2021-12-01 17:25:22 +00:00
def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
match type, n with
| e, 0 => (e, [])
| Expr.forallE name type body _, x + 1 =>
let body := body.instantiate1 $ mkFVar ⟨name⟩
let next := dropArgs body x
{ next with snd := (name, type) :: next.snd}
| e, x + 1 => panic! s!"No forallE left"
def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
let type := ctor.type
let (field_function, params) := dropArgs type (ctor.numParams + parents)
let (_, fields) := dropArgs field_function (ctor.numFields - parents)
let mut field_infos := #[]
for (name, type) in fields do
field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
field_infos
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
let ctorType ← prettyPrintTerm ctor.type
2021-12-02 09:34:20 +00:00
match getStructureInfo? env v.name with
| some i =>
if i.fieldNames.size - parents.size > 0 then
return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
else
return StructureInfo.mk info #[] parents ⟨ctor.name, 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)
2022-01-06 13:51:46 +00:00
return ClassInfo.mk sinfo (insts.map Expr.constName!)
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-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 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
def getKind : DocInfo → String
| axiomInfo _ => "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo _ => "constant"
| definitionInfo _ => "def"
| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
| inductiveInfo _ => "inductive"
| structureInfo _ => "structure"
| classInfo _ => "class" -- TODO: This is handled as structure right now
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
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
2021-11-27 15:19:56 +00:00
end DocInfo
2021-12-12 12:21:53 +00:00
structure AnalyzerResult where
2021-12-17 16:20:44 +00:00
name2ModIdx : HashMap Name ModuleIdx
moduleNames : Array Name
moduleInfo : HashMap Name Module
2021-12-12 12:21:53 +00:00
hierarchy : Hierarchy
2022-01-16 13:22:53 +00:00
-- Indexed by ModIdx
importAdj : Array (Array Bool)
2021-12-12 12:21:53 +00:00
deriving Inhabited
def process : MetaM AnalyzerResult := 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 =>
2022-01-16 13:22:53 +00:00
let some modidx ← env.getModuleIdxFor? cinfo.fst | unreachable!
let moduleName := env.allImportedModuleNames.get! modidx
let module := res.find! moduleName
res := res.insert moduleName {module with members := module.members.push dinfo}
2021-11-27 15:19:56 +00:00
| none => ()
2022-01-16 13:22:53 +00:00
-- TODO: This is definitely not the most efficient way to store this data
let mut adj := Array.mkArray res.size (Array.mkArray res.size false)
-- TODO: This could probably be faster if we did an insertion sort above instead
for (moduleName, module) in res.toArray do
res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
2022-01-16 13:22:53 +00:00
let some modIdx ← env.getModuleIdx? moduleName | unreachable!
let moduleData := env.header.moduleData.get! modIdx
for imp in moduleData.imports do
let some importIdx ← env.getModuleIdx? imp.module | unreachable!
adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
2021-12-17 16:20:44 +00:00
return {
name2ModIdx := env.const2ModIdx,
moduleNames := env.header.moduleNames,
moduleInfo := res,
2022-01-16 13:22:53 +00:00
hierarchy := Hierarchy.fromArray env.header.moduleNames,
importAdj := adj
2021-12-17 16:20:44 +00:00
}
2021-11-27 15:19:56 +00:00
end DocGen4