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

chore: refine synthInstance cache

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-01 11:43:05 -08:00
parent 11d829eccd
commit 27bf6c8229
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -104,12 +104,14 @@ structure AbstractMVarsResult :=
(numMVars : Nat)
(expr : Expr)
abbrev SynthInstance.Answer := AbstractMVarsResult
abbrev SynthInstance.Answer := AbstractMVarsResult -- The `expr` field is the synthesized instance value
abbrev SynthInstance.Failure := AbstractMVarsResult -- The `expr` field is the type (i.e, instance) we failed to synthesize
structure Cache :=
(inferType : PersistentExprStructMap Expr := {})
(funInfo : PersistentHashMap InfoCacheKey FunInfo := {})
(synthInstance : DiscrTree SynthInstance.Answer := {})
(inferType : PersistentExprStructMap Expr := {})
(funInfo : PersistentHashMap InfoCacheKey FunInfo := {})
(synthInstance : DiscrTree SynthInstance.Answer := {})
(synthInstanceFailure : DiscrTree SynthInstance.Failure := {})
structure Context :=
(config : Config := {})
@ -423,9 +425,10 @@ partial def isClassQuick : Expr → MetaM (LOption Name)
/-- Reset `synthInstance` cache, execute `x`, and restore cache -/
@[inline] def resettingSynthInstanceCache {α} (x : MetaM α) : MetaM α :=
do s ← get;
let savedCached := s.cache.synthInstance;
modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s };
finally x (modify $ fun s => { cache := { synthInstance := savedCached, .. s.cache }, .. s })
let savedSythInstance := s.cache.synthInstance;
let savedSythInstanceFailure := s.cache.synthInstanceFailure;
modify $ fun s => { cache := { synthInstance := {}, synthInstanceFailure := {}, .. s.cache }, .. s };
finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, synthInstanceFailure := savedSythInstanceFailure, .. s.cache }, .. s })
/-- Add entry `{ className := className, fvar := fvar }` to localInstances,
and then execute continuation `k`.