feat: use Kyle Miller's instance analysis algorithm

leanprover · Nov 5, 2023 · ec2561f · ec2561f
1 parent 8bccb92
commit ec2561f
Showing 1 changed file with 10 additions and 6 deletions.
diff --git 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