From a55841aa68c7319ab1dea4e775fddffb1356f728 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Dec 2019 18:05:46 -0800
Subject: [PATCH] chore: simplify `synthInstance` cache

Make sure it handle the common cases efficiently.
---
 src/Init/Lean/Meta/AbstractMVars.lean |  5 +++++
 src/Init/Lean/Meta/Basic.lean         | 20 +++++---------------
 2 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/src/Init/Lean/Meta/AbstractMVars.lean b/src/Init/Lean/Meta/AbstractMVars.lean
index a126acf532..ca6ac27e36 100644
--- a/src/Init/Lean/Meta/AbstractMVars.lean
+++ b/src/Init/Lean/Meta/AbstractMVars.lean
@@ -9,6 +9,11 @@ import Init.Lean.Meta.Basic
 namespace Lean
 namespace Meta
 
+structure AbstractMVarsResult :=
+(paramNames : Array Name)
+(numMVars   : Nat)
+(expr       : Expr)
+
 namespace AbstractMVars
 
 structure State :=
diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index c22b117ad0..4fe98a452b 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -99,19 +99,10 @@ instance : HasBeq InfoCacheKey :=
 ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩
 end InfoCacheKey
 
-structure AbstractMVarsResult :=
-(paramNames : Array Name)
-(numMVars   : Nat)
-(expr       : Expr)
-
-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  := {})
-(synthInstanceFailure : DiscrTree SynthInstance.Failure := {})
+(inferType     : PersistentExprStructMap Expr := {})
+(funInfo       : PersistentHashMap InfoCacheKey FunInfo := {})
+(synthInstance : PersistentHashMap Expr (Option Expr) := {})
 
 structure Context :=
 (config         : Config         := {})
@@ -426,9 +417,8 @@ partial def isClassQuick : Expr → MetaM (LOption Name)
 @[inline] def resettingSynthInstanceCache {α} (x : MetaM α) : MetaM α :=
 do s ← get;
    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 })
+   modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s };
+   finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s })
 
 /-- Add entry `{ className := className, fvar := fvar }` to localInstances,
     and then execute continuation `k`.