54 lines
1.4 KiB
Plaintext
54 lines
1.4 KiB
Plaintext
/-
|
|
Copyright (c) 2022 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 DocGen4.Process.Base
|
|
import DocGen4.Process.NameInfo
|
|
|
|
namespace DocGen4.Process
|
|
|
|
open Lean Meta Widget
|
|
|
|
partial def stripArgs (e : Expr) : Expr :=
|
|
match e.consumeMData with
|
|
| Expr.forallE name _ body _ =>
|
|
let name := name.eraseMacroScopes
|
|
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
|
|
| _ => e
|
|
|
|
def processEq (eq : Name) : MetaM CodeWithInfos := do
|
|
let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
|
|
let final := stripArgs type
|
|
prettyPrintTerm final
|
|
|
|
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
|
|
let info ← Info.ofConstantVal v.toConstantVal
|
|
let isUnsafe := v.safety == DefinitionSafety.unsafe
|
|
let isNonComputable := isNoncomputable (← getEnv) v.name
|
|
try
|
|
let eqs? ← getEqnsFor? v.name
|
|
let equations ← eqs?.mapM (·.mapM processEq)
|
|
return {
|
|
toInfo := info,
|
|
isUnsafe,
|
|
hints := v.hints,
|
|
equations,
|
|
isNonComputable
|
|
}
|
|
catch err =>
|
|
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
|
|
return {
|
|
toInfo := info,
|
|
isUnsafe,
|
|
hints := v.hints,
|
|
equations := none,
|
|
isNonComputable
|
|
}
|
|
|
|
|
|
|
|
end DocGen4.Process
|