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

feat: one more pp.analyze pass

Browse source
This commit is contained in:
Daniel Selsam 2021-07-29 12:18:21 -07:00 • committed by Sebastian Ullrich
parent d6412b3a98
commit 7030eaad3d
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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