From 4cd5b67271b090ab5af80e93d21dc876ea95da26 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 14 Nov 2022 12:53:18 +0100
Subject: [PATCH] chore: generalize parser kind detection

---
 src/Lean/ParserCompiler.lean | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index ba73523eb6..492bd24bc4 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -37,12 +37,17 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   let e ← whnfCore e
   if e matches Expr.lam .. then
     lambdaLetTelescope e fun _ e => parserNodeKind? e
-  else if e.isAppOfArity ``nodeWithAntiquot 4 || e.isAppOfArity ``withAntiquot 2 || e.isAppOfArity ``withCache 2 then
-    parserNodeKind? (e.getArg! 1)
   else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then
     reduceEval? (e.getArg! 0)
-  else
-    return none
+  else if e.isAppOfArity ``withAntiquot 2 then
+    parserNodeKind? (e.getArg! 1)
+  else forallTelescope (← inferType e.getAppFn) fun params _ => do
+    let lctx ← getLCtx
+    -- if there is exactly one parameter of type `Parser`, search there
+    if let [(i, _)] := params.toList.enum.filter (lctx.getFVar! ·.2 |>.type.isConstOf ``Parser) then
+      parserNodeKind? (e.getArg! i)
+    else
+      return none
 
 section
 open Meta