feat: add synthInstance cache

src/Init/Lean/Meta/AbstractMVars.lean

@@ -9,11 +9,6 @@ import Init.Lean.Meta.Basic
 namespace Lean
 namespace Meta
 
-structure AbstractMVarsResult :=
-(levels   : Array Level)
-(numMVars : Nat)
-(expr     : Expr)
-
 namespace AbstractMVars
 
 structure State :=

src/Init/Lean/Meta/Basic.lean

@@ -12,6 +12,7 @@ import Init.Lean.Trace
 import Init.Lean.Class
 import Init.Lean.ReducibilityAttrs
 import Init.Lean.Meta.Exception
+import Init.Lean.Meta.DiscrTreeTypes
 
 /-
 This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks.
@@ -98,9 +99,17 @@ instance : HasBeq InfoCacheKey :=
 ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩
 end InfoCacheKey
 
+structure AbstractMVarsResult :=
+(levels   : Array Level)
+(numMVars : Nat)
+(expr     : Expr)
+
+abbrev SynthInstanceAnswer := AbstractMVarsResult
+
 structure Cache :=
-(inferType : PersistentExprStructMap Expr := {})
-(funInfo   : PersistentHashMap InfoCacheKey FunInfo := {})
+(inferType     : PersistentExprStructMap Expr := {})
+(funInfo       : PersistentHashMap InfoCacheKey FunInfo := {})
+(synthInstance : DiscrTree (List SynthInstanceAnswer) := {})
 
 structure Context :=
 (config         : Config         := {})
@@ -411,15 +420,18 @@ partial def isClassQuick : Expr → MetaM (LOption Name)
   | _                 => pure LOption.none
 | Expr.localE _ _ _ _ => unreachable!
 
-/-- Reset type class cache, execute `x`, and restore cache -/
-@[inline] def resettingTypeClassCache {α} (x : MetaM α) : MetaM α :=
-x -- TODO
+/-- 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 })
 
 /-- Add entry `{ className := className, fvar := fvar }` to localInstances,
     and then execute continuation `k`.
-    It resets the type class cache using `resettingTypeClassCache`. -/
+    It resets the type class cache using `resettingSynthInstanceCache`. -/
 @[inline] def withNewLocalInstance {α} (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α :=
-resettingTypeClassCache $
+resettingSynthInstanceCache $
   adaptReader
     (fun (ctx : Context) => {
       localInstances := ctx.localInstances.push { className := className, fvar := fvar },
@@ -433,7 +445,7 @@ resettingTypeClassCache $
   - `isClassExpensive` is defined later.
   - The type class chache is reset whenever a new local instance is found.
   - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.
-    Thus, each new local instance requires a new `resettingTypeClassCache`. -/
+    Thus, each new local instance requires a new `resettingSynthInstanceCache`. -/
 @[specialize] partial def withNewLocalInstances {α}
     (isClassExpensive : Expr → MetaM (Option Name))
     (fvars : Array Expr) : Nat → MetaM α → MetaM α

src/Init/Lean/Meta/DiscrTree.lean

@@ -51,34 +51,6 @@ namespace DiscrTree
   2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
 -/
 
-inductive Key
-| const : Name → Nat → Key
-| fvar  : FVarId → Nat → Key
-| lit   : Literal → Key
-| star  : Key
-| other : Key
-
-instance Key.inhabited : Inhabited Key := ⟨Key.star⟩
-
-def Key.hash : Key → USize
-| Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
-| Key.fvar n a  => mixHash 3541 $ mixHash (hash n) (hash a)
-| Key.lit v     => mixHash 1879 $ hash v
-| Key.star      => 7883
-| Key.other     => 2411
-
-instance Key.hashable : Hashable Key := ⟨Key.hash⟩
-
-def Key.beq : Key → Key → Bool
-| Key.const c₁ a₁, Key.const c₂ a₂ => c₁ == c₂ && a₁ == a₂
-| Key.fvar c₁ a₁,  Key.fvar c₂ a₂  => c₁ == c₂ && a₁ == a₂
-| Key.lit v₁,      Key.lit v₂      => v₁ == v₂
-| Key.star,        Key.star        => true
-| Key.other,       Key.other       => true
-| _,                _              => false
-
-instance Key.hasBeq : HasBeq Key := ⟨Key.beq⟩
-
 def Key.ctorIdx : Key → Nat
 | Key.star      => 0
 | Key.other     => 1
@@ -109,20 +81,8 @@ def Key.arity : Key → Nat
 | Key.fvar _ a  => a
 | _             => 0
 
-inductive Trie (α : Type)
-| node (vs : Array α) (children : Array (Key × Trie)) : Trie
-
 instance Trie.inhabited {α} : Inhabited (Trie α) := ⟨Trie.node #[] #[]⟩
 
-end DiscrTree
-
-open DiscrTree
-
-structure DiscrTree (α : Type) :=
-(root : PersistentHashMap Key (Trie α) := {})
-
-namespace DiscrTree
-
 def empty {α} : DiscrTree α := { root := {} }
 
 /- The discrimination tree ignores implicit arguments and proofs.

src/Init/Lean/Meta/DiscrTreeTypes.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Expr
+
+namespace Lean
+namespace Meta
+
+/- See file `DiscrTree.lean` for the actual implementation and documentation. -/
+
+namespace DiscrTree
+
+inductive Key
+| const : Name → Nat → Key
+| fvar  : FVarId → Nat → Key
+| lit   : Literal → Key
+| star  : Key
+| other : Key
+
+instance Key.inhabited : Inhabited Key := ⟨Key.star⟩
+
+def Key.hash : Key → USize
+| Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
+| Key.fvar n a  => mixHash 3541 $ mixHash (hash n) (hash a)
+| Key.lit v     => mixHash 1879 $ hash v
+| Key.star      => 7883
+| Key.other     => 2411
+
+instance Key.hashable : Hashable Key := ⟨Key.hash⟩
+
+def Key.beq : Key → Key → Bool
+| Key.const c₁ a₁, Key.const c₂ a₂ => c₁ == c₂ && a₁ == a₂
+| Key.fvar c₁ a₁,  Key.fvar c₂ a₂  => c₁ == c₂ && a₁ == a₂
+| Key.lit v₁,      Key.lit v₂      => v₁ == v₂
+| Key.star,        Key.star        => true
+| Key.other,       Key.other       => true
+| _,                _              => false
+
+instance Key.hasBeq : HasBeq Key := ⟨Key.beq⟩
+
+inductive Trie (α : Type)
+| node (vs : Array α) (children : Array (Key × Trie)) : Trie
+
+end DiscrTree
+
+open DiscrTree
+
+structure DiscrTree (α : Type) :=
+(root : PersistentHashMap Key (Trie α) := {})
+
+end Meta
+end Lean