r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring

main
Xubai Wang 2022-02-18 04:01:34 +08:00
parent cce4285c96 5ce1ce9fe7
commit 0724806fe6
1 changed files with 9 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
DocGen4/Process.lean
View File

@ -52,7 +52,7 @@ structure DefinitionInfo extends Info where
isUnsafe : Bool isUnsafe : Bool
hints : ReducibilityHints hints : ReducibilityHints
equations : Option (Array CodeWithInfos) equations : Option (Array CodeWithInfos)
isComputable : Bool isNonComputable : Bool
deriving Inhabited deriving Inhabited
abbrev InstanceInfo := DefinitionInfo abbrev InstanceInfo := DefinitionInfo
@ -203,30 +203,22 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
let type ← mkForallFVars xs type let type ← mkForallFVars xs type
pure type pure type
-- The following code is translated from ll_infer_type.cpp
def computable? (defn : Name) : MetaM Bool := do
let cstage2Name := defn.append `_cstage2
let env ← getEnv
let extern? := externAttr.getParam env defn |>.isSome
let cstage2? := env.find? cstage2Name |>.isSome
pure $ extern? ∨ cstage2?
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
let isUnsafe := v.safety == DefinitionSafety.unsafe let isUnsafe := v.safety == DefinitionSafety.unsafe
let isComputable ← computable? v.name let isNonComput := isNoncomputable (←getEnv) v.name
try try
let eqs? ← getEqnsFor? v.name let eqs? ← getEqnsFor? v.name
match eqs? with match eqs? with
| some eqs => | some eqs =>
let prettyEqs ← eqs.mapM processEq let prettyEqs ← eqs.mapM processEq
pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isComputable pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput
| none => | none =>
let eq ← prettyPrintTerm $ stripArgs (←valueToEq v) let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isComputable pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput
catch err => catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}" IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable pure $ DefinitionInfo.mk info isUnsafe v.hints none isNonComput
def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let info ← DefinitionInfo.ofDefinitionVal v let info ← DefinitionInfo.ofDefinitionVal v
@ -395,7 +387,7 @@ def getKindDescription : DocInfo → String
let mut modifiers := #[] let mut modifiers := #[]
if i.isUnsafe then if i.isUnsafe then
modifiers := modifiers.push "unsafe" modifiers := modifiers.push "unsafe"
if ¬i.isComputable then if i.isNonComputable then
modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "noncomputable"
modifiers := modifiers.push "def" modifiers := modifiers.push "def"
@ -404,7 +396,7 @@ def getKindDescription : DocInfo → String
let mut modifiers := #[] let mut modifiers := #[]
if i.isUnsafe then if i.isUnsafe then
modifiers := modifiers.push "unsafe" modifiers := modifiers.push "unsafe"
if ¬i.isComputable then if i.isNonComputable then
modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "noncomputable"
modifiers := modifiers.push "instance" modifiers := modifiers.push "instance"
@ -492,6 +484,8 @@ structure AnalyzerResult where
importAdj : Array (Array Bool) importAdj : Array (Array Bool)
deriving Inhabited deriving Inhabited
deriving instance Inhabited for ModuleDoc
def process : MetaM AnalyzerResult := do def process : MetaM AnalyzerResult := do
let env ← getEnv let env ← getEnv
let mut res := mkHashMap env.header.moduleNames.size let mut res := mkHashMap env.header.moduleNames.size
@ -500,7 +494,6 @@ def process : MetaM AnalyzerResult := do
| none => #[] | none => #[]
| some ds => ds | some ds => ds
|>.map (λ doc => ModuleMember.modDoc doc) |>.map (λ doc => ModuleMember.modDoc doc)
res := res.insert module (Module.mk module modDocs) res := res.insert module (Module.mk module modDocs)
for cinfo in env.constants.toList do for cinfo in env.constants.toList do