refactor: Predefinition.Structural code cleanup

useful bits from the shelved #5849

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -30,11 +30,11 @@ partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) :
   | .const `True _ => throwToBelowFailed
   | _ => k e F
 
-/-- See `toBelow` -/
-private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : Expr) : MetaM Expr := do
-  trace[Elab.definition.structural] "belowDict start:{indentExpr belowDict}\narg:{indentExpr arg}"
+private partial def searchThroughBelow (belowDictType : Expr) (belowVal : Expr) (arg : Expr)
+    (pred : Expr → MetaM Bool) := do
+  trace[Elab.definition.structural] "belowDict start:{indentExpr belowDictType}\narg:{indentExpr arg}"
   -- First search through the PProd packing of the different `brecOn` motives
-  searchPProd belowDict F fun belowDict F => do
+  searchPProd belowDictType belowVal fun belowDict F => do
     trace[Elab.definition.structural] "belowDict step 1:{indentExpr belowDict}"
     -- Then instantiate parameters of a reflexive type, if needed
     forallTelescopeReducing belowDict fun xs belowDict => do
@@ -50,14 +50,15 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E
       -- targeted indexing.)
       searchPProd belowDict (mkAppN F argTailArgs) fun belowDict F => do
         trace[Elab.definition.structural] "belowDict step 2:{indentExpr belowDict}"
-        match belowDict with
-        | .app belowDictFun belowDictArg =>
-          unless belowDictFun.getAppFn == C do throwToBelowFailed
-          unless ← isDefEq belowDictArg arg do throwToBelowFailed
-          pure F
-        | _ =>
+        unless belowDict.isApp do
           trace[Elab.definition.structural] "belowDict not an app:{indentExpr belowDict}"
           throwToBelowFailed
+        if (← pred belowDict) then pure F else throwToBelowFailed
+
+/-- See `toBelow` -/
+private def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : Expr) : MetaM Expr := do
+  searchThroughBelow belowDict F arg fun belowDict' =>
+    isDefEq belowDict' (.app C arg)
 
 /-- See `toBelow` -/
 private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
@@ -114,8 +115,9 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
   The dictionary is built using the `PProd` (`And` for inductive predicates).
   We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
 private partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
-  withBelowDict below numIndParams positions fun Cs belowDict =>
-    toBelowAux Cs[fnIndex]! belowDict recArg below
+  withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
+    withBelowDict below numIndParams positions fun Cs belowDict =>
+      toBelowAux Cs[fnIndex]! belowDict recArg below
 
 private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
     (below : Expr) (e : Expr) : M Expr :=

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -4,18 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Util.HasConstCache
-import Lean.Meta.Match.Match
-import Lean.Meta.Tactic.Simp.Main
-import Lean.Meta.Tactic.Cleanup
-import Lean.Meta.ArgsPacker
-import Lean.Elab.Tactic.Basic
-import Lean.Elab.RecAppSyntax
+import Lean.Data.Array
 import Lean.Elab.PreDefinition.Basic
-import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.Structural.BRecOn
 import Lean.Elab.PreDefinition.WF.Basic
-import Lean.Data.Array
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.ArgsPacker
+import Lean.Meta.ForEachExpr
+import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Tactic.Cleanup
+import Lean.Util.HasConstCache
 
 namespace Lean.Elab.WF
 open Meta

tests/lean/run/issue5836.lean

@@ -0,0 +1,85 @@
+inductive Foo where
+  | foo : (String → Option Foo) → Foo
+
+-- Would be great if this worked, but it doesn't yet:
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  failed to eliminate recursive application
+    map m x
+-/
+#guard_msgs in
+def Foo.map (m : Foo → Foo) : Foo → Foo
+  | .foo f => .foo fun s => match f s with
+    | none => none
+    | some x => map m x
+termination_by structural x => x
+
+-- workaround:
+
+mutual
+def Foo.bar (m : Foo → Foo) : Foo → Foo
+  | .foo f => .foo fun s => Foo.bar_aux m (f s)
+termination_by structural x => x
+
+def Foo.bar_aux (m : Foo → Foo) : Option Foo → Option Foo
+    | none => none
+    | some x => bar m x
+termination_by structural x => x
+end
+
+-- similar
+
+-- set_option trace.Elab.definition.structural true in
+-- set_option pp.match false in
+/--
+error: failed to infer structural recursion:
+Cannot use parameter xs:
+  failed to eliminate recursive application
+    g zs
+-/
+#guard_msgs in
+def g (xs : List Nat) : Nat :=
+  match xs with
+  | [] => 0
+  | _::ys =>
+    match ys with
+    | []       => 1
+    | _::_::zs => g zs + 1
+    | _zs       => g ys + 2
+termination_by structural xs
+
+
+inductive Foo2 where
+  | none
+  | foo : (String → Foo2) → Foo2
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  failed to eliminate recursive application
+    map m (f₂ s)
+-/
+#guard_msgs in
+def Foo2.map (m : Foo2 → Foo2) : Foo2 → Foo2
+  | none => none
+  | .foo f => .foo fun s => match f s with
+    | none => none
+    | foo f₂ => .foo fun s => map m (f₂ s)
+termination_by structural x => x
+
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  failed to eliminate recursive application
+    map_tricky m (f₂ s)
+-/
+#guard_msgs in
+def Foo2.map_tricky (m : Foo2 → Foo2) : Foo2 → Foo2
+  | none => none
+  | .foo f => .foo fun s => match f s, f (s ++ s) with
+    | foo f₂, foo f₃ => .foo fun s => if s = "test" then map_tricky m (f₂ s) else map_tricky m (f₃ s)
+    | _, _ => none
+termination_by structural x => x