From 325bb6b5b59d2d12b9e39e3483ae30875ca7cc8e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 23 Feb 2020 10:34:49 -0800
Subject: [PATCH] feat: helper function for user-defined recursors

---
 src/Init/Lean/Elab/Tactic/Basic.lean     |  2 ++
 src/Init/Lean/Elab/Tactic/Induction.lean | 30 +++++++++++++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean
index 6d35d9560b..894ec7ad57 100644
--- a/src/Init/Lean/Elab/Tactic/Basic.lean
+++ b/src/Init/Lean/Elab/Tactic/Basic.lean
@@ -78,6 +78,8 @@ def ensureHasType (ref : Syntax) (expectedType? : Option Expr) (e : Expr) : Tact
 def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals ref goals
 def inferType (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.inferType ref e
 def whnf (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnf ref e
+def whnfCore (ref : Syntax) (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnfCore ref e
+def unfoldDefinition? (ref : Syntax) (e : Expr) : TacticM (Option Expr) := liftTermElabM $ Term.unfoldDefinition? ref e
 
 /-- Collect unassigned metavariables -/
 def collectMVars (ref : Syntax) (e : Expr) : TacticM (List MVarId) := do
diff --git a/src/Init/Lean/Elab/Tactic/Induction.lean b/src/Init/Lean/Elab/Tactic/Induction.lean
index e59ac6eed3..befdac37aa 100644
--- a/src/Init/Lean/Elab/Tactic/Induction.lean
+++ b/src/Init/Lean/Elab/Tactic/Induction.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
+import Init.Lean.Meta.RecursorInfo
 import Init.Lean.Elab.Tactic.ElabTerm
 import Init.Lean.Elab.Tactic.Generalize
 
@@ -111,6 +112,31 @@ liftMetaMAtMain ref $ fun mvarId => do
     | _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType)
   | _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType)
 
+private partial def getRecFromUsingLoop (ref : Syntax) (baseRecName : Name) : Expr → TacticM (Option Meta.RecursorInfo)
+| majorType => do
+  let continue (majorType : Expr) : TacticM (Option Meta.RecursorInfo) := do {
+    majorType? ← unfoldDefinition? ref majorType;
+    match majorType? with
+    | some majorType => withIncRecDepth ref $ getRecFromUsingLoop majorType
+    | none           => pure none
+  };
+  majorType ← whnfCore ref majorType;
+  match majorType.getAppFn with
+  | Expr.const name _ _ => do
+    let candidate := name ++ baseRecName;
+    env ← getEnv;
+    match env.find? candidate with
+    | some _ =>
+      catch
+        (liftMetaMAtMain ref $ fun _ => do info ← Meta.mkRecursorInfo candidate; pure (some info))
+        (fun _ => continue majorType)
+    | none   => continue majorType
+  | _ => continue majorType
+
+
+def getRecFromUsing (ref : Syntax) (major : Expr) (baseRecName : Name) : TacticM Name := do
+throw $ arbitrary _
+
 /-
   Recall that
   ```
@@ -150,7 +176,9 @@ if usingRecStx.isNone then do
     unless remainingAlts.isEmpty $
       throwError (remainingAlts.get! 0) "unused alternative";
     pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
-else
+else do
+  let baseRecName := (usingRecStx.getIdAt 1).eraseMacroScopes;
+  let recName := getRecFromUsing ref major baseRecName;
   -- TODO
   throw $ arbitrary _