From 7030eaad3d53f10f286c19bc794dac7cf4742681 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 29 Jul 2021 12:18:21 -0700 Subject: [PATCH] feat: one more pp.analyze pass --- .../Delaborator/TopDownAnalyze.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index ecc59911b7..3cfc7d8d70 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -303,14 +303,27 @@ where -- Unify with the expected type tryUnify (← inferType (mkAppN f args)) resultType - -- Collect explicit arguments that can be elaborated without expected type let mut bottomUps := mkArray args.size false + + -- Collect explicit arguments that can be elaborated without expected type, with *no* top-down info + -- Note: we perform this before the next pass because we prefer simple bottom-ups to unify first before + -- more complex ones. for i in [:args.size] do if bInfos[i] == BinderInfo.default then + if (← valUnknown mvars[i]) && (← okBottomUp? args[i]).isSafe then + tryUnify args[i] mvars[i] + bottomUps := bottomUps.set! i true + + -- Now, collect explicit arguments that can be elaborated with *incomplete* top-down info + for i in [:args.size] do + if !bottomUps[i] && bInfos[i] == BinderInfo.default then if (← valUnknown mvars[i]) && (← okBottomUp? args[i] mvars[i]).isSafe then tryUnify args[i] mvars[i] bottomUps := bottomUps.set! i true - else if bInfos[i] == BinderInfo.instImplicit then + + -- Next, look at out params + for i in [:args.size] do + if bInfos[i] == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i] -- Collect implicit higher-order arguments