73 lines
2.0 KiB
Plaintext
73 lines
2.0 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) (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
|