From 3bef119136128640e797cfaa8580a80315780bd6 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 30 Jul 2021 10:48:50 -0700 Subject: [PATCH] fix: pp.analyze missing inBottomUp --- .../PrettyPrinter/Delaborator/TopDownAnalyze.lean | 13 +++++++++---- tests/lean/run/PPTopDownAnalyze.lean | 2 +- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 437320ee8a..f8f22f5b24 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -445,6 +445,7 @@ where -- TODO: this is a very crude heuristic, motivated by https://github.com/leanprover/lean4/issues/590 unless getPPAnalyzeOmitMax (← getOptions) && ls.any containsBadMax do annotateBool `pp.universes + maybeAddExplicit analyzePi : AnalyzeM Unit := do annotateBool `pp.binderTypes @@ -458,10 +459,14 @@ where analyzeLet : AnalyzeM Unit := do let Expr.letE n t v body .. ← getExpr | unreachable! - let needsType := (← okBottomUp? v).needsType - if needsType then annotateBool `pp.analysis.letVarType - withLetValue $ withKnowing true true analyze - withLetVarType $ withKnowing true false analyze + if (← okBottomUp? v).needsType then + annotateBool `pp.analysis.letVarType + withLetVarType $ withKnowing true false analyze + withLetValue $ withKnowing true true analyze + else + withReader (fun ctx => { ctx with inBottomUp := true }) do + withLetValue $ withKnowing true true analyze + withLetBody analyze analyzeSort : AnalyzeM Unit := pure () diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index d11b5c447c..c3b9d2c195 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -51,7 +51,7 @@ syntax (name := testDelabTDN) "#testDelabN " ident : command @[commandElab testDelabTDN] def elabTestDelabTDN : CommandElab | `(#testDelabN $name:ident) => liftTermElabM `delabTD do let name := name.getId - let [name] ← resolveGlobalConst name | throwError "cannot resolve name" + let [name] ← resolveGlobalConst (mkIdent name) | throwError "cannot resolve name" let some cInfo ← (← getEnv).find? name | throwError "no decl for name" let some value ← pure cInfo.value? | throwError "decl has no value" modify fun s => { s with levelNames := cInfo.levelParams }