From 57533726f628efbfd9be1240ffd4c32bca8e45a5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Aug 2020 10:35:38 -0700
Subject: [PATCH] feat: add `mkFreshExprMVarWithId`

---
 src/Lean/Elab/Term.lean  |  5 +++++
 src/Lean/Meta/Basic.lean | 15 +++++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 04f24996c9..e34a378799 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -272,11 +272,16 @@ def unfoldDefinition? (ref : Syntax) (e : Expr) : TermElabM (Option Expr) := lif
 def instantiateMVars (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.instantiateMVars e
 def instantiateLevelMVars (ref : Syntax) (u : Level) : TermElabM Level := liftMetaM ref $ Meta.instantiateLevelMVars u
 def isClass (ref : Syntax) (t : Expr) : TermElabM (Option Name) := liftMetaM ref $ Meta.isClass t
+def mkFreshId : TermElabM Name := liftMetaM Syntax.missing Meta.mkFreshId
 def mkFreshLevelMVar (ref : Syntax) : TermElabM Level := liftMetaM ref $ Meta.mkFreshLevelMVar
 def mkFreshExprMVar (ref : Syntax) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
 match type? with
 | some type => liftMetaM ref $ Meta.mkFreshExprMVar type userName? kind
 | none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
+def mkFreshExprMVarWithId (ref : Syntax) (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
+match type? with
+| some type => liftMetaM ref $ Meta.mkFreshExprMVarWithId mvarId type userName? kind
+| none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVarWithId mvarId type userName? kind
 def mkFreshTypeMVar (ref : Syntax) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
 liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
 def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index dd65be1e99..383aa5994d 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -233,18 +233,29 @@ let id := s.ngen.curr;
 modify $ fun s => { s with ngen := s.ngen.next };
 pure id
 
+private def mkFreshExprMVarAtCore
+    (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : MetaM Expr := do
+modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
+pure $ mkMVar mvarId
+
 def mkFreshExprMVarAt
     (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
     : MetaM Expr := do
 mvarId ← mkFreshId;
-modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
-pure $ mkMVar mvarId
+mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
 
 def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
 lctx ← getLCtx;
 localInsts ← getLocalInstances;
 mkFreshExprMVarAt lctx localInsts type userName kind
 
+/- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
+   the metavar using this method. -/
+def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
+lctx ← getLCtx;
+localInsts ← getLocalInstances;
+mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
+
 def mkFreshLevelMVar : MetaM Level := do
 mvarId ← mkFreshId;
 modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };