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

fix: pp.analyze also bottom-up the trivials

Browse source
This commit is contained in:
Daniel Selsam 2021-08-04 20:17:06 -07:00 • committed by Sebastian Ullrich
parent 1a815a4339
commit 4cdfbde93b
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -277,6 +277,9 @@ where
inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars
| _, _ => return ()
partial def trivialBottomUp (e : Expr) : AnalyzeM Bool := do
e.isFVar || e.isMVar || e.isConst
partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := 10) : AnalyzeM Bool := do
-- Here we check if `e` can be safely elaborated without its expected type.
-- These are incomplete (and possibly unsound) heuristics.
@ -296,15 +299,12 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
for i in [:mvars.size] do
if bInfos[i] == BinderInfo.instImplicit then
inspectOutParams args[i] mvars[i]
else if ← bInfos[i] == BinderInfo.default <&&> typeUnknown mvars[i] then
else if ← bInfos[i] == BinderInfo.default <&&> (typeUnknown mvars[i] <||> trivialBottomUp args[i]) then
if ← canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i]
if ← (isHBinOp e <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
return !(← valUnknown resultType)
partial def trivialBottomUp (e : Expr) : AnalyzeM Bool := do
e.isFVar || e.isMVar || e.isConst
def withKnowing (knowsType knowsLevel : Bool) (x : AnalyzeM α) : AnalyzeM α := do
withReader (fun ctx => { ctx with knowsType := knowsType, knowsLevel := knowsLevel }) x