From dd4fac2a7b337d75ddfcd42cc1bf02d2b3219a1d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Feb 2020 21:02:59 -0800
Subject: [PATCH] chore: helper functions

---
 src/Init/Lean/LocalContext.lean |  5 +++++
 src/Init/Lean/Meta/Basic.lean   | 17 ++++++++++-------
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean
index e65338fb61..4b907ba0fc 100644
--- a/src/Init/Lean/LocalContext.lean
+++ b/src/Init/Lean/LocalContext.lean
@@ -94,6 +94,11 @@ match lctx with
   let decl := LocalDecl.ldecl idx fvarId userName type value;
   { fvarIdToDecl := map.insert fvarId decl, decls := decls.push decl }
 
+/- Low level API -/
+def addDecl (lctx : LocalContext) (newDecl : LocalDecl) : LocalContext :=
+match lctx with
+| { fvarIdToDecl := map, decls := decls } => { fvarIdToDecl := map.insert newDecl.fvarId newDecl, decls := decls.set newDecl.index newDecl }
+
 @[export lean_local_ctx_find]
 def find? (lctx : LocalContext) (fvarId : FVarId) : Option LocalDecl :=
 lctx.fvarIdToDecl.find? fvarId
diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 3276bfae04..54e7df5be1 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -781,18 +781,21 @@ let savedMCtx  := s.mctx;
 modify $ fun s => { mctx := s.mctx.incDepth, .. s };
 finally x (modify $ fun s => { mctx := savedMCtx, .. s })
 
+def withLocalContext {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
+localInstsCurr ← getLocalInstances;
+adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) $
+  if localInsts == localInstsCurr then
+    x
+  else
+    resettingSynthInstanceCache x
+
 /--
   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. -/
-def withMVarContext {α} (mvarId : MVarId) (x : MetaM α) : MetaM α := do
+@[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
+withLocalContext mvarDecl.lctx mvarDecl.localInstances x
 
 @[inline] def withMCtx {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α := do
 mctx' ← getMCtx;