max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: pp.analyze no explicit holes by default

Browse source
This commit is contained in:
Daniel Selsam 2021-09-14 12:23:33 -07:00 • committed by Sebastian Ullrich
parent cbe5241663
commit 4646b36459
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
View file

@ -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 }

1
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -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)