From 8a920f7aebe5eba0f61dbea811220eceff5732d4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Sep 2020 16:55:15 -0700
Subject: [PATCH] feat: `replaceRecApps` find matcher

---
 src/Lean/Elab/PreDefinition/Structural.lean | 28 ++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 3071cafd7a..b5d210128b 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExpr
 import Lean.Meta.RecursorInfo
+import Lean.Meta.Match.Match
 import Lean.Elab.PreDefinition.Basic
 
 namespace Lean
@@ -131,9 +132,30 @@ private partial def findRecArgAux {α} (numFixed : Nat) (xs : Array Expr) (k : R
 @[inline] private def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → MetaM α) : MetaM α :=
 findRecArgAux numFixed xs k numFixed
 
-private def replaceRecApps (argInfo : RecArgInfo) (below : Expr) (value : Expr) : MetaM Expr :=
--- TODO
-pure value
+private partial def replaceRecApps (argInfo : RecArgInfo) (below : Expr) : Expr → MetaM Expr
+| e@(Expr.lam _ _ _ _) => lambdaTelescope e fun xs b => do b ← replaceRecApps b; mkLambdaFVars xs b
+| Expr.letE n type val body _ => do
+  val ← replaceRecApps val;
+  withLetDecl n type val fun x => do
+    body ← replaceRecApps body;
+    mkLetFVars #[x] body
+| Expr.mdata d e _   => do e ← replaceRecApps e; pure $ mkMData d e
+| Expr.proj n i e _  => do e ← replaceRecApps e; pure $ mkProj n i e
+| e@(Expr.app _ _ _) => do
+  let processApp (e : Expr) : MetaM Expr :=
+    e.withApp fun f args => do {
+      f ← replaceRecApps f;
+      args ← args.mapM replaceRecApps;
+      pure $ mkAppN f args
+    };
+  matcherApp? ← Match.matchMatcherApp? e;
+  match matcherApp? with
+  | some matcherApp => do
+    trace! `Elab.definition.structural ("found matcher");
+    -- TODO
+    pure e
+  | none => processApp e
+| e => pure e
 
 private def mkBRecOn (argInfo : RecArgInfo) (value : Expr) : MetaM Expr := do
 type ← inferType value;