bookshelf-doc/DocGen4/Process/DefinitionInfo.lean

73 lines
2.0 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-
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 {
toInfo := info,
isUnsafe,
hints := v.hints,
equations := none,
isNonComputable
}
end DocGen4.Process