r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

refactor: Remove unnecessary cases in type analysis

main
Henrik 2023-09-10 11:07:22 +02:00
parent 7dc8018130
commit a090875215
2 changed files with 8 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
DocGen4/Process/DefinitionInfo.lean
View File

@ -14,9 +14,6 @@ open Lean Meta Widget
partial def stripArgs (e : Expr) : Expr := partial def stripArgs (e : Expr) : Expr :=
match e.consumeMData with match e.consumeMData with
| Expr.lam name _ body _ =>
let name := name.eraseMacroScopes
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
| Expr.forallE name _ body _ => | Expr.forallE name _ body _ =>
let name := name.eraseMacroScopes let name := name.eraseMacroScopes
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩)) stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
@ -27,39 +24,20 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do
let final := stripArgs type let final := stripArgs type
prettyPrintTerm final prettyPrintTerm final
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 DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
let isUnsafe := v.safety == DefinitionSafety.unsafe let isUnsafe := v.safety == DefinitionSafety.unsafe
let isNonComputable := isNoncomputable (← getEnv) v.name let isNonComputable := isNoncomputable (← getEnv) v.name
try try
let eqs? ← getEqnsFor? v.name let eqs? ← getEqnsFor? v.name
match eqs? with let equations ← eqs?.mapM (·.mapM processEq)
| some eqs => return {
let equations ← eqs.mapM processEq toInfo := info,
return { isUnsafe,
toInfo := info, hints := v.hints,
isUnsafe, equations,
hints := v.hints, isNonComputable
equations, }
isNonComputable
}
| none =>
let equations := #[← prettyPrintTerm <| stripArgs (← valueToEq v)]
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
catch err => catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}" IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
return { return {

1
DocGen4/Process/NameInfo.lean
View File

@ -32,7 +32,6 @@ partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderI
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
(#[arg] ++ args, final) (#[arg] ++ args, final)
match e.consumeMData with match e.consumeMData with
| Expr.lam name type body binderInfo => helper name type body binderInfo
| Expr.forallE name type body binderInfo => helper name type body binderInfo | Expr.forallE name type body binderInfo => helper name type body binderInfo
| _ => (#[], e) | _ => (#[], e)