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
|
2021-11-28 20:31:22 +00:00
|
|
|
|
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
|
|
|
|
|
|
2021-12-25 13:08:09 +00:00
|
|
|
|
open Lean Meta PrettyPrinter Std Widget
|
2021-12-17 14:59:43 +00:00
|
|
|
|
|
2021-12-05 01:54:38 +00:00
|
|
|
|
structure NameInfo where
|
|
|
|
|
name : Name
|
2021-12-25 13:08:09 +00:00
|
|
|
|
type : CodeWithInfos
|
|
|
|
|
deriving Inhabited
|
2021-12-05 01:54:38 +00:00
|
|
|
|
|
2021-12-25 15:55:30 +00:00
|
|
|
|
structure Arg where
|
|
|
|
|
name : Name
|
|
|
|
|
type : CodeWithInfos
|
|
|
|
|
binderInfo : BinderInfo
|
|
|
|
|
|
2021-12-05 01:54:38 +00:00
|
|
|
|
structure Info extends NameInfo where
|
2021-12-25 15:55:30 +00:00
|
|
|
|
args : Array Arg
|
2021-11-27 15:19:56 +00:00
|
|
|
|
doc : Option String
|
2021-12-05 14:45:19 +00:00
|
|
|
|
declarationRange : DeclarationRange
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
|
|
|
|
structure AxiomInfo extends Info where
|
|
|
|
|
isUnsafe : Bool
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
2021-12-17 14:59:43 +00:00
|
|
|
|
structure TheoremInfo extends Info
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
|
|
|
|
structure OpaqueInfo extends Info where
|
2021-12-25 13:08:09 +00:00
|
|
|
|
value : CodeWithInfos
|
2021-11-27 15:19:56 +00:00
|
|
|
|
isUnsafe : Bool
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
2021-12-01 17:25:22 +00:00
|
|
|
|
structure DefinitionInfo extends Info where
|
2021-12-25 13:08:09 +00:00
|
|
|
|
--value : CodeWithInfos
|
2021-12-01 17:25:22 +00:00
|
|
|
|
unsafeInformation : DefinitionSafety
|
|
|
|
|
hints : ReducibilityHints
|
2021-12-25 13:08:09 +00:00
|
|
|
|
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
|
2021-12-05 01:54:38 +00:00
|
|
|
|
ctors : List NameInfo -- List of all constructors and their type for this inductive datatype
|
2021-12-01 17:25:22 +00:00
|
|
|
|
isUnsafe : Bool
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-12-01 17:25:22 +00:00
|
|
|
|
|
2021-12-02 09:34:20 +00:00
|
|
|
|
structure StructureInfo extends Info where
|
2022-01-04 07:23:39 +00:00
|
|
|
|
fieldInfo : Array NameInfo
|
2021-12-02 09:34:20 +00:00
|
|
|
|
parents : Array Name
|
2021-12-05 01:54:38 +00:00
|
|
|
|
ctor : NameInfo
|
2021-12-25 13:08:09 +00:00
|
|
|
|
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
|
2021-12-25 13:08:09 +00:00
|
|
|
|
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
|
2021-12-25 13:08:09 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
2022-01-07 17:25:26 +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
|
|
|
|
|
|
2021-11-28 20:31:22 +00:00
|
|
|
|
structure Module where
|
|
|
|
|
name : Name
|
|
|
|
|
doc : Option String
|
2022-01-07 17:25:26 +00:00
|
|
|
|
-- Sorted according to their line numbers
|
2021-11-28 20:31:22 +00:00
|
|
|
|
members : Array DocInfo
|
2021-12-01 17:25:22 +00:00
|
|
|
|
deriving Inhabited
|
2021-11-28 20:31:22 +00:00
|
|
|
|
|
2021-12-25 15:55:30 +00:00
|
|
|
|
partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
|
|
|
|
|
match e.consumeMData with
|
|
|
|
|
| Expr.lam name type body data =>
|
|
|
|
|
let name := name.eraseMacroScopes
|
|
|
|
|
let arg := (name, type, data.binderInfo)
|
|
|
|
|
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
|
|
|
|
|
(#[arg] ++ args, final)
|
|
|
|
|
| Expr.forallE name type body data =>
|
|
|
|
|
let name := name.eraseMacroScopes
|
|
|
|
|
let arg := (name, type, data.binderInfo)
|
|
|
|
|
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
|
|
|
|
|
(#[arg] ++ args, final)
|
|
|
|
|
| _ => (#[], e)
|
|
|
|
|
|
2021-12-25 13:08:09 +00:00
|
|
|
|
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
|
|
|
|
|
fileMap := arbitrary
|
|
|
|
|
}
|
|
|
|
|
tagExprInfos ctx infos tt
|
2021-11-28 20:31:22 +00:00
|
|
|
|
|
|
|
|
|
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
|
|
|
|
|
let env ← getEnv
|
2021-12-25 15:55:30 +00:00
|
|
|
|
let (args, type) := typeToArgsType v.type
|
|
|
|
|
let type ← prettyPrintTerm type
|
|
|
|
|
let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b)
|
2021-12-11 13:26:32 +00:00
|
|
|
|
let doc ← findDocString? env v.name
|
2021-12-05 14:45:19 +00:00
|
|
|
|
match ←findDeclarationRanges? v.name with
|
|
|
|
|
-- TODO: Maybe selection range is more relevant? Figure this out in the future
|
2021-12-25 15:55:30 +00:00
|
|
|
|
| some range => return Info.mk ⟨v.name, type⟩ args doc range.range
|
2021-12-05 14:45:19 +00:00
|
|
|
|
| none => panic! s!"{v.name} is a declaration without position"
|
2021-11-28 20:31:22 +00:00
|
|
|
|
|
|
|
|
|
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
|
2021-12-17 14:59:43 +00:00
|
|
|
|
let t ← prettyPrintTerm v.value
|
|
|
|
|
return OpaqueInfo.mk info t v.isUnsafe
|
2021-11-28 20:31:22 +00:00
|
|
|
|
|
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
|
|
|
|
|
|
2021-12-25 13:08:09 +00:00
|
|
|
|
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
|
2021-12-05 01:54:38 +00:00
|
|
|
|
let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
|
2022-01-03 17:22:12 +00:00
|
|
|
|
return InductiveInfo.mk info ctors v.isUnsafe
|
2021-12-01 17:25:22 +00:00
|
|
|
|
|
2022-01-04 07:23:39 +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"
|
|
|
|
|
|
2022-01-09 13:07:50 +00:00
|
|
|
|
def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
|
2022-01-04 07:23:39 +00:00
|
|
|
|
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
|
2022-01-09 13:07:50 +00:00
|
|
|
|
field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
|
2022-01-04 07:23:39 +00:00
|
|
|
|
field_infos
|
2021-12-05 01:54:38 +00:00
|
|
|
|
|
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
|
2022-01-04 07:23:39 +00:00
|
|
|
|
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
|
2021-12-04 21:33:00 +00:00
|
|
|
|
| some i =>
|
2022-01-04 07:23:39 +00:00
|
|
|
|
if i.fieldNames.size - parents.size > 0 then
|
2022-01-09 13:07:50 +00:00
|
|
|
|
return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
|
2022-01-04 07:23:39 +00:00
|
|
|
|
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
|
2021-12-05 14:45:19 +00:00
|
|
|
|
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
|
|
|
|
|
2021-12-02 10:09:54 +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
|
2021-12-02 10:09:54 +00:00
|
|
|
|
| ConstantInfo.defnInfo i =>
|
2021-12-03 19:37:25 +00:00
|
|
|
|
if ← (isProjFn i.name) then
|
2021-12-02 10:09:54 +00:00
|
|
|
|
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
|
|
|
|
|
|
2021-12-15 10:59:36 +00:00
|
|
|
|
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
|
|
|
|
|
|
2021-12-25 13:08:09 +00:00
|
|
|
|
def getType : DocInfo → CodeWithInfos
|
2021-12-17 14:59:43 +00:00
|
|
|
|
| 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
|
|
|
|
|
|
2021-12-25 15:55:30 +00:00
|
|
|
|
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
|
|
|
|
|
deriving Inhabited
|
|
|
|
|
|
|
|
|
|
def process : MetaM AnalyzerResult := do
|
2021-11-28 20:31:22 +00:00
|
|
|
|
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
|
2021-11-28 20:31:22 +00:00
|
|
|
|
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 => ()
|
2022-01-07 17:25:26 +00:00
|
|
|
|
|
|
|
|
|
-- 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}
|
|
|
|
|
|
2021-12-17 16:20:44 +00:00
|
|
|
|
return {
|
|
|
|
|
name2ModIdx := env.const2ModIdx,
|
|
|
|
|
moduleNames := env.header.moduleNames,
|
|
|
|
|
moduleInfo := res,
|
|
|
|
|
hierarchy := Hierarchy.fromArray env.header.moduleNames
|
|
|
|
|
}
|
2021-11-27 15:19:56 +00:00
|
|
|
|
|
|
|
|
|
end DocGen4
|