bookshelf-doc/DocGen4/Process/DefinitionInfo.lean

73 lines
2.0 KiB
Plaintext
Raw Normal View History

/-
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) (k : Expr → MetaM α) : MetaM α :=
match e.consumeMData with
| Expr.forallE name type body bi =>
let name := name.eraseMacroScopes
Meta.withLocalDecl name bi type fun fvar => do
stripArgs (Expr.instantiate1 body fvar) k
| _ => k e
def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
withOptions (tactic.hygienic.set . false) do
lambdaTelescope v.value fun xs body => do
let us := v.levelParams.map mkLevelParam
let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
let type ← mkForallFVars xs type
return type
def processEq (eq : Name) : MetaM CodeWithInfos := do
let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
stripArgs type prettyPrintTerm
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
match eqs? with
| some eqs =>
let equations ← eqs.mapM processEq
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
| none =>
let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
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 {
2022-07-23 11:37:17 +00:00
toInfo := info,
isUnsafe,
hints := v.hints,
equations := none,
isNonComputable
}
end DocGen4.Process