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

refactor: do not save/restore cache at "telescope" methods

Browse source 
@kha @dselsam FYI

The original motivation for saving/restoring the cache was not
correctness, but cache size management. When we go inside a binder
using the telescope methods, we extend the local context with new fresh
free variables, execute the action `k` using the new extended local
context, and then restore it. Any cached result containing these
fresh variables is dead after executing `k`. So, `savingCache` here
could be viewed as a "checkpoint". However, it also removes any
cached entry that does not contain the new fresh variables.
I found this inconvenient in practice, and it is the wrong choice
in a few cases. Example: we have a `forall` expr (aka arrow), and use a
telescope to go inside, and then invoke TC. If the telescope uses
`savingCache`, we lose the cached TC instance witness. This is
wasteful since the witness often doesn't even depend on the new fresh
free variables created by the telescope.
Thus, this commit removes the `savingCache` occurrences from
the "telescope" methods. Users may still manually use it if
they think it is appropriate. That is, they can write
```lean
savingCache $ forallTelescope e $ fun xs body => <code>
```
if they really want to discard any new cache entry created while
executing `<code>`.
This commit is contained in:
Leonardo de Moura 2019-12-02 10:57:19 -08:00
parent 00a5860ce6
commit 770649ce1d
1 changed files with 7 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Init/Lean/Meta/Basic.lean
View file

@ -527,10 +527,9 @@ resettingSynthInstanceCache $
(isClassExpensive : Expr → MetaM (Option Name))
(type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
do newType ← whnf type;
if newType.isForall then
savingCache $ do
lctx ← getLCtx;
forallTelescopeReducingAuxAux isClassExpensive true maxFVars? k lctx #[] 0 newType
if newType.isForall then do
lctx ← getLCtx;
forallTelescopeReducingAuxAux isClassExpensive true maxFVars? k lctx #[] 0 newType
else
k #[] type
@ -548,9 +547,8 @@ partial def isClassExpensive : Expr → MetaM (Option Name)
This combinator will declare local declarations, create free variables for them,
execute `k` with updated local context, and make sure the cache is restored after executing `k`. -/
@[inline] def forallTelescope {α} (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
savingCache $ do
lctx ← getLCtx;
forallTelescopeReducingAuxAux isClassExpensive false none k lctx #[] 0 type
do lctx ← getLCtx;
forallTelescopeReducingAuxAux isClassExpensive false none k lctx #[] 0 type
/--
Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
@ -597,9 +595,8 @@ do c? ← isClassQuick type;
/-- Similar to `forallTelescope` but for lambda and let expressions. -/
@[specialize] def lambdaTelescope {α}
(e : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
savingCache $ do
lctx ← getLCtx;
lambdaTelescopeAux k lctx #[] 0 e
do lctx ← getLCtx;
lambdaTelescopeAux k lctx #[] 0 e
private partial def forallMetaTelescopeReducingAux
(reducing? : Bool) (maxMVars? : Option Nat)