From ec2561f34bdec6341d2a25774a30e43f768b3ae8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 5 Nov 2023 09:38:22 +0100 Subject: [PATCH] feat: use Kyle Miller's instance analysis algorithm --- DocGen4/Process/InstanceInfo.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index e25cec6..df37004 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -16,14 +16,18 @@ open Lean Meta def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do let (_, _, tail) ← forallMetaTelescopeReducing typ let args := tail.getAppArgs - let (_, names) ← args.mapM (Expr.forEach · findName) |>.run .empty + let (_, bis, _) ← forallMetaTelescopeReducing (← inferType tail.getAppFn) + let (_, names) ← (bis.zip args).mapM findName |>.run .empty return names where - findName : Expr → StateRefT (Array Name) MetaM Unit - | .const name _ => modify (·.push name) - | .sort .zero => modify (·.push "_builtin_prop") - | .sort (.succ _) => modify (·.push "_builtin_typeu") - | .sort _ => modify (·.push "_builtin_sortu") + findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit + | (.default, .sort .zero) => modify (·.push "_builtin_prop") + | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu") + | (.default, .sort _) => modify (·.push "_builtin_sortu") + | (.default, e) => + match e.getAppFn with + | .const name .. => modify (·.push name) + | _ => return () | _ => return () def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do