From 4646b36459f2b080843873abfd90a422f6abc6fe Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Tue, 14 Sep 2021 12:23:33 -0700
Subject: [PATCH] feat: pp.analyze no explicit holes by default

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 9 ++++++++-
 tests/lean/run/PPTopDownAnalyze.lean                   | 1 +
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index ea40ee274b..80e1a04fb9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -96,6 +96,12 @@ register_builtin_option pp.analyze.knowsType : Bool := {
   descr    := "(pretty printer analyzer) assume the type of the original expression is known"
 }
 
+register_builtin_option pp.analyze.explicitHoles : Bool := {
+  defValue := false
+  group    := "pp.analyze"
+  descr    := "(pretty printer analyzer) use `_` for explicit arguments that can be inferred"
+}
+
 def getPPAnalyze                            (o : Options) : Bool := o.get pp.analyze.name pp.analyze.defValue
 def getPPAnalyzeCheckInstances              (o : Options) : Bool := o.get pp.analyze.checkInstances.name pp.analyze.checkInstances.defValue
 def getPPAnalyzeTypeAscriptions             (o : Options) : Bool := o.get pp.analyze.typeAscriptions.name pp.analyze.typeAscriptions.defValue
@@ -107,6 +113,7 @@ def getPPAnalyzeTrustCoe                    (o : Options) : Bool := o.get pp.ana
 def getPPAnalyzeTrustKnownFOType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownFOType2TypeHOFuns.name pp.analyze.trustKnownFOType2TypeHOFuns.defValue
 def getPPAnalyzeOmitMax                     (o : Options) : Bool := o.get pp.analyze.omitMax.name pp.analyze.omitMax.defValue
 def getPPAnalyzeKnowsType                   (o : Options) : Bool := o.get pp.analyze.knowsType.name pp.analyze.knowsType.defValue
+def getPPAnalyzeExplicitHoles               (o : Options) : Bool := o.get pp.analyze.explicitHoles.name pp.analyze.explicitHoles.defValue
 
 def getPPAnalysisSkip            (o : Options) : Bool := o.get `pp.analysis.skip false
 def getPPAnalysisHole            (o : Options) : Bool := o.get `pp.analysis.hole false
@@ -562,7 +569,7 @@ mutual
 
           match bInfos[i] with
           | BinderInfo.default =>
-            if ← !(← valUnknown mvars[i]) <&&> !(← readThe Context).inBottomUp <&&> !(← isFunLike arg) <&&> !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
+            if ← getPPAnalyzeExplicitHoles (← getOptions) <&&> !(← valUnknown mvars[i]) <&&> !(← readThe Context).inBottomUp <&&> !(← isFunLike arg) <&&> !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
               annotateBool `pp.analysis.hole
             else
               modify fun s => { s with provideds := s.provideds.set! i true }
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 99a7eea13b..29199366e8 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -68,6 +68,7 @@ universe u v
 
 set_option pp.analyze true
 set_option pp.analyze.checkInstances true
+set_option pp.analyze.explicitHoles true
 set_option pp.proofs true
 
 #testDelab @Nat.brecOn (fun x => Nat) 0 (fun x ih => x)