From c5111de0f0646e4e1031180ad50320cd07b16798 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Jan 2020 08:04:25 -0800
Subject: [PATCH] feat: add option `set_option synthInstance.maxSteps <num>`

cc @dselsam @kha
---
 src/Init/Lean/Meta/Basic.lean         |  2 +-
 src/Init/Lean/Meta/SynthInstance.lean | 26 ++++++++++++++++++--------
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index ef4f33ffad..6ec524f3ee 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -251,7 +251,7 @@ ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
 @[inline] def getTransparency : MetaM TransparencyMode := do
 ctx ← read; pure $ ctx.config.transparency
 
-@[inline] private def getOptions : MetaM Options := do
+@[inline] def getOptions : MetaM Options := do
 ctx ← read; pure ctx.config.opts
 
 -- Remark: wanted to use `private`, but in C++ parser, `private` declarations do not shadow outer public ones.
diff --git a/src/Init/Lean/Meta/SynthInstance.lean b/src/Init/Lean/Meta/SynthInstance.lean
index 1a45d9750f..29920bc05e 100644
--- a/src/Init/Lean/Meta/SynthInstance.lean
+++ b/src/Init/Lean/Meta/SynthInstance.lean
@@ -421,15 +421,16 @@ else pure false
 def getResult : SynthM (Option Expr) := do
 s ← get; pure s.result
 
-partial def synth : Nat → SynthM (Option Expr)
+def synth : Nat → SynthM (Option Expr)
 | 0   => do
   trace! `Meta.synthInstance "synthInstance is out of fuel";
   pure none
-| n+1 => do
+| fuel+1 => do
+  trace! `Meta.synthInstance ("remaining fuel " ++ toString fuel);
   condM step
     (do result? ← getResult;
         match result? with
-        | none        => synth n
+        | none        => synth fuel
         | some result => pure result)
     (do trace! `Meta.synthInstance "failed";
         pure none)
@@ -511,7 +512,16 @@ forallTelescope type $ fun xs typeBody =>
         pure type
   | _ => pure type
 
-def synthInstance? (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) := do
+
+@[init] def maxStepsOption : IO Unit :=
+registerOption `synthInstance.maxSteps { defValue := (10000 : Nat), group := "", descr := "maximum steps for the type class instance synthesis procedure" }
+
+private def getMaxSteps (opts : Options) : Nat :=
+opts.getNat `synthInstance.maxSteps 10000
+
+def synthInstance? (type : Expr) : MetaM (Option Expr) := do
+opts ← getOptions;
+let fuel := getMaxSteps opts;
 inputConfig ← getConfig;
 withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox := true, ctxApprox := true, .. config }) $ do
   type ← instantiateMVars type;
@@ -543,17 +553,17 @@ withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
   instance cannot be synthesized right now because `type` contains metavariables. -/
-def trySynthInstance (type : Expr) (fuel : Nat := 10000) : MetaM (LOption Expr) :=
+def trySynthInstance (type : Expr) : MetaM (LOption Expr) :=
 adaptReader (fun (ctx : Context) => { config := { isDefEqStuckEx := true, .. ctx.config }, .. ctx }) $
   catch
-    (toLOptionM $ synthInstance? type fuel)
+    (toLOptionM $ synthInstance? type)
     (fun ex => match ex with
       | Exception.isExprDefEqStuck _ _ _  => pure LOption.undef
       | Exception.isLevelDefEqStuck _ _ _ => pure LOption.undef
       | _                                 => throw ex)
 
-def synthInstance (type : Expr) (fuel : Nat := 10000) : MetaM Expr := do
-result? ← synthInstance? type fuel;
+def synthInstance (type : Expr) : MetaM Expr := do
+result? ← synthInstance? type;
 match result? with
 | some result => pure result
 | none        => throwEx $ Exception.synthInstance type