2022-05-19 22:36:21 +00:00
|
|
|
|
/-
|
|
|
|
|
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
|
|
|
|
|
|
2023-10-17 19:32:48 +00:00
|
|
|
|
partial def stripArgs (e : Expr) (k : Expr → MetaM α) : MetaM α :=
|
2022-05-19 22:36:21 +00:00
|
|
|
|
match e.consumeMData with
|
2023-10-17 19:32:48 +00:00
|
|
|
|
| Expr.forallE name type body bi =>
|
2022-05-19 22:36:21 +00:00
|
|
|
|
let name := name.eraseMacroScopes
|
2023-10-17 19:32:48 +00:00
|
|
|
|
Meta.withLocalDecl name bi type fun fvar => do
|
|
|
|
|
stripArgs (Expr.instantiate1 body fvar) k
|
|
|
|
|
| _ => k e
|
2022-05-19 22:36:21 +00:00
|
|
|
|
|
2023-10-08 09:33:27 +00:00
|
|
|
|
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
|
|
|
|
|
|
2022-05-19 22:36:21 +00:00
|
|
|
|
def processEq (eq : Name) : MetaM CodeWithInfos := do
|
|
|
|
|
let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
|
2023-10-17 19:32:48 +00:00
|
|
|
|
stripArgs type prettyPrintTerm
|
2022-05-19 22:36:21 +00:00
|
|
|
|
|
|
|
|
|
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
|
|
|
|
|
let info ← Info.ofConstantVal v.toConstantVal
|
|
|
|
|
let isUnsafe := v.safety == DefinitionSafety.unsafe
|
2023-01-01 18:30:28 +00:00
|
|
|
|
let isNonComputable := isNoncomputable (← getEnv) v.name
|
2023-11-18 22:06:55 +00:00
|
|
|
|
|
2022-05-19 22:36:21 +00:00
|
|
|
|
try
|
2023-11-18 22:49:28 +00:00
|
|
|
|
let eqs? ← getEqnsFor? v.name
|
2023-11-18 22:06:55 +00:00
|
|
|
|
|
2023-10-08 09:33:27 +00:00
|
|
|
|
match eqs? with
|
|
|
|
|
| some eqs =>
|
|
|
|
|
let equations ← eqs.mapM processEq
|
|
|
|
|
return {
|
|
|
|
|
toInfo := info,
|
|
|
|
|
isUnsafe,
|
|
|
|
|
hints := v.hints,
|
|
|
|
|
equations,
|
|
|
|
|
isNonComputable
|
|
|
|
|
}
|
|
|
|
|
| none =>
|
2023-10-17 19:32:48 +00:00
|
|
|
|
let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
|
2023-10-08 09:33:27 +00:00
|
|
|
|
return {
|
|
|
|
|
toInfo := info,
|
|
|
|
|
isUnsafe,
|
|
|
|
|
hints := v.hints,
|
|
|
|
|
equations,
|
|
|
|
|
isNonComputable
|
|
|
|
|
}
|
2022-05-19 22:36:21 +00:00
|
|
|
|
catch err =>
|
2023-01-01 18:30:28 +00:00
|
|
|
|
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
|
|
|
|
|
}
|
|
|
|
|
|
2022-05-19 22:36:21 +00:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
end DocGen4.Process
|