From 00a5860ce680b99217b55c88518cb0ed21eaf6a2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2019 10:49:34 -0800
Subject: [PATCH] feat: add `withMVarContext`

cc @dselsam @kha
---
 src/Init/Lean/Meta/Basic.lean     | 15 ++++++++++++++-
 src/Init/Lean/MetavarContext.lean |  5 +++++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index b3d272e53e..26c60d931d 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -344,7 +344,7 @@ do lctx ← getLCtx;
 def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
 getLocalDecl fvar.fvarId!
 
-def getMVarDecl (mvarId : Name) : MetaM MetavarDecl :=
+def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with
    | some d => pure d
@@ -717,6 +717,19 @@ do s ← get;
    modify $ fun s => { mctx := s.mctx.incDepth, .. s };
    finally x (modify $ fun s => { cache := savedCache, mctx := savedMCtx, .. s })
 
+/--
+  Execute `x` using the given metavariable `LocalContext` and `LocalInstances`.
+  The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
+  different from the current ones. -/
+@[inline] def withMVarContext {α} (mvarId : MVarId) (x : MetaM α) : MetaM α :=
+do mvarDecl ← getMVarDecl mvarId;
+   localInsts ← getLocalInstances;
+   adaptReader (fun (ctx : Context) => { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances, .. ctx }) $
+     if localInsts == mvarDecl.localInstances then
+       x
+     else
+       resettingSynthInstanceCache x
+
 end Meta
 end Lean
 
diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index 3ffc942dff..23c9deda51 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -199,6 +199,11 @@ structure LocalInstance :=
 
 abbrev LocalInstances := Array LocalInstance
 
+def LocalInstance.beq (i₁ i₂ : LocalInstance) : Bool :=
+i₁.fvar == i₂.fvar
+
+instance LocalInstance.hasBeq : HasBeq LocalInstance := ⟨LocalInstance.beq⟩
+
 structure MetavarDecl :=
 (userName       : Name := Name.anonymous)
 (lctx           : LocalContext)