refactor: improve MVarId method discoverability

See issue #1346

RELEASES.md

@@ -1,6 +1,10 @@
 Unreleased
 ---------
 
+* Improve `MVarId` methods discoverability. See [issue #1346](https://github.com/leanprover/lean4/issues/1346).
+  We still have to add similar methods for `FVarId`, `LVarId`, `Expr`, and other objects.
+  Many existing methods have been marked as deprecated.
+
 * Add attribute `[deprecated]` for marking deprecated declarations. Examples:
   ```lean
   def g (x : Nat) := x + 1

src/Lean/Elab/App.lean

@@ -386,7 +386,7 @@ private def finalize : M Expr := do
     synthesizeAppInstMVars
     /- If `eType != mkMVar outParamMVarId`, then the
        function is partially applied, and we do not apply default instances. -/
-    if !(← isExprMVarAssigned outParamMVarId) && eType.isMVar && eType.mvarId! == outParamMVarId then
+    if !(← outParamMVarId.isAssigned) && eType.isMVar && eType.mvarId! == outParamMVarId then
       synthesizeSyntheticMVarsUsingDefault
       return e
     else

src/Lean/Elab/BuiltinTerm.lean

@@ -89,12 +89,12 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
           withLCtx mvarDecl.lctx mvarDecl.localInstances do
             throwError "synthetic hole has already been defined and assigned to value incompatible with the current context{indentExpr val}"
       | none =>
-        if (← isMVarDelayedAssigned mvarId) then
+        if (← mvarId.isDelayedAssigned) then
           -- We can try to improve this case if needed.
           throwError "synthetic hole has already beend defined and delayed assigned with an incompatible local context"
         else if lctx.isSubPrefixOf mvarDecl.lctx then
           let mvarNew ← mkNewHole ()
-          assignExprMVar mvarId mvarNew
+          mvarId.assign mvarNew
           return mvarNew
         else
           throwError "synthetic hole has already been defined with an incompatible local context"
@@ -107,7 +107,7 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
      | none =>
        let e ← elabTerm e none
        let mvar ← mkFreshExprMVar (← inferType e) MetavarKind.syntheticOpaque n.getId
-       assignExprMVar mvar.mvarId! e
+       mvar.mvarId!.assign e
        -- We use `mkSaveInfoAnnotation` to make sure the info trees for `e` are saved even if `b` is a metavariable.
        return mkSaveInfoAnnotation (← elabTerm b expectedType?)
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Match.lean

@@ -529,7 +529,7 @@ where
       return mkInaccessible (← eraseInaccessibleAnnotations e)
     else
       if e'.isMVar then
-        setMVarTag e'.mvarId! (← read).userName
+        e'.mvarId!.setTag (← read).userName
       modify fun s => { s with patternVars := s.patternVars.push e' }
       return e
 

src/Lean/Elab/MutualDef.lean

@@ -525,7 +525,7 @@ private def mkLetRecClosureFor (toLift : LetRecToLift) (freeVars : Array FVarId)
     let type := Closure.mkForall s.localDecls <| Closure.mkForall s.newLetDecls type
     let val  := Closure.mkLambda s.localDecls <| Closure.mkLambda s.newLetDecls val
     let c    := mkAppN (Lean.mkConst toLift.declName) s.exprArgs
-    assignExprMVar toLift.mvarId c
+    toLift.mvarId.assign c
     return {
       ref        := toLift.ref
       localDecls := s.newLocalDecls

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -24,18 +24,18 @@ partial def expand : Expr → Expr
   | e => e
 
 def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
-  let target ← getMVarType' mvarId
+  let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
   unless rhs.isLet || rhs.isMData do return none
-  return some (← replaceTargetDefEq mvarId (← mkEq lhs (expand rhs)))
+  return some (← mvarId.replaceTargetDefEq (← mkEq lhs (expand rhs)))
 
 def funext? (mvarId : MVarId) : MetaM (Option MVarId) := do
-  let target ← getMVarType' mvarId
+  let target ← mvarId.getType'
   let some (_, _, rhs) := target.eq? | return none
   unless rhs.isLambda do return none
   commitWhenSome? do
-    let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | return none
-    let (_, mvarId) ← intro1 mvarId
+    let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | return none
+    let (_, mvarId) ← mvarId.intro1
     return some mvarId
 
 def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
@@ -76,7 +76,7 @@ private def findMatchToSplit? (env : Environment) (e : Expr) (declNames : Array
         return Expr.FindStep.visit
 
 partial def splitMatch? (mvarId : MVarId) (declNames : Array Name) : MetaM (Option (List MVarId)) := commitWhenSome? do
-  let target ← getMVarType' mvarId
+  let target ← mvarId.getType'
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
     if let some e := findMatchToSplit? (← getEnv) target declNames badCases then
       try
@@ -145,8 +145,8 @@ where
       ST.Prim.Ref.get ref
     runST (go e)
 
-private partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+private partial def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := mvarId.withContext do
+  let target ← mvarId.getType'
   let fvarState := collectFVars {} target
   let fvarState ← (← getLCtx).foldrM (init := fvarState) fun decl fvarState => do
     if fvarState.fvarSet.contains decl.fvarId then
@@ -229,7 +229,7 @@ where
 /-    if let some mvarId ← funext? mvarId then
         return (← go mvarId) -/
 
-    if (← shouldUseSimpMatch (← getMVarType' mvarId)) then
+    if (← shouldUseSimpMatch (← mvarId.getType')) then
       if let some mvarId ← simpMatch? mvarId then
         return (← go mvarId)
 
@@ -270,32 +270,32 @@ where
         return (lctx.mkForall xsNew type, lctx.mkLambda xsNew value)
 
 /-- Delta reduce the equation left-hand-side -/
-def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+def deltaLHS (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
   let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
-  replaceTargetDefEq mvarId (← mkEq lhs rhs)
+  mvarId.replaceTargetDefEq (← mkEq lhs rhs)
 
-def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
   let some rhs ← delta? rhs.consumeMData (· == declName) | return none
-  replaceTargetDefEq mvarId (← mkEq lhs rhs)
+  mvarId.replaceTargetDefEq (← mkEq lhs rhs)
 
 private partial def whnfAux (e : Expr) : MetaM Expr := do
   let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
   let f := e.getAppFn
   match f with
-  | Expr.proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
+  | .proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
   | _ => return e
 
 /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
-def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
   let lhs' ← whnfAux lhs
   if lhs' != lhs then
-    return some (← replaceTargetDefEq mvarId (← mkEq lhs' rhs))
+    return some (← mvarId.replaceTargetDefEq (← mkEq lhs' rhs))
   else
     return none
 
@@ -325,12 +325,12 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
   let tryEqns (mvarId : MVarId) : MetaM Bool :=
     eqs.anyM fun eq => commitWhen do
       try
-        let subgoals ← apply mvarId (← mkConstWithFreshMVarLevels eq)
+        let subgoals ← mvarId.apply (← mkConstWithFreshMVarLevels eq)
         subgoals.allM fun subgoal => do
-          if (← isExprMVarAssigned subgoal) then
+          if (← subgoal.isAssigned) then
             return true -- Subgoal was already solved. This can happen when there are dependencies between the subgoals
           else
-            assumptionCore subgoal
+            subgoal.assumptionCore
       catch _ =>
         return false
   let rec go (mvarId : MVarId) : MetaM Unit := do
@@ -340,7 +340,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
     -- else if let some mvarId ← funext? mvarId then
     --  go mvarId
 
-    if (← shouldUseSimpMatch (← getMVarType' mvarId)) then
+    if (← shouldUseSimpMatch (← mvarId.getType')) then
       if let some mvarId ← simpMatch? mvarId then
         return (← go mvarId)
 

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -25,7 +25,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
   trace[Elab.definition.structural.eqns] "proving: {type}"
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
-    let (_, mvarId) ← intros main.mvarId!
+    let (_, mvarId) ← main.mvarId!.intros
     unless (← tryURefl mvarId) do -- catch easy cases
       go (← deltaLHS mvarId)
     instantiateMVars main

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -18,22 +18,22 @@ structure EqnInfo extends EqnInfoCore where
   fixedPrefixSize : Nat
   deriving Inhabited
 
-private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, _) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
   if lhs.isAppOf ``WellFounded.fix then
     return mvarId
   else
     deltaLHSUntilFix (← deltaLHS mvarId)
 
-private def rwFixEq (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | unreachable!
   let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
   let some (_, _, lhsNew) := (← inferType h).eq? | unreachable!
   let targetNew ← mkEq lhsNew rhs
   let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
-  assignExprMVar mvarId (← mkEqTrans h mvarNew)
+  mvarId.assign (← mkEqTrans h mvarNew)
   return mvarNew.mvarId!
 
 private def hasWellFoundedFix (e : Expr) : Bool :=
@@ -103,8 +103,8 @@ where
   See comment at `tryToFoldWellFoundedFix`.
 -/
 def simpMatchWF? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
-  withMVarContext mvarId do
-    let target ← instantiateMVars (← getMVarType mvarId)
+  mvarId.withContext do
+    let target ← instantiateMVars (← mvarId.getType)
     let targetNew ← Simp.main target (← Split.getSimpMatchContext) (methods := { pre })
     let mvarIdNew ← applySimpResultToTarget mvarId target targetNew
     if mvarId != mvarIdNew then return some mvarIdNew else return none
@@ -127,22 +127,22 @@ where
       | none => return Simp.Step.visit { expr := e }
 
 private def tryToFoldLHS? (info : EqnInfo) (us : List Level) (fixedPrefix : Array Expr) (mvarId : MVarId) : MetaM (Option MVarId) :=
-  withMVarContext mvarId do
-    let target ← getMVarType' mvarId
+  mvarId.withContext do
+    let target ← mvarId.getType'
     let some (_, lhs, rhs) := target.eq? | unreachable!
     let lhsNew ← tryToFoldWellFoundedFix info us fixedPrefix lhs
     if lhs == lhsNew then return none
     let targetNew ← mkEq lhsNew rhs
     let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
-    assignExprMVar mvarId mvarNew
+    mvarId.assign mvarNew
     return mvarNew.mvarId!
 
 /--
   Given a goal of the form `|- f.{us} a_1 ... a_n b_1 ... b_m = ...`, return `(us, #[a_1, ..., a_n])`
   where `f` is a constant named `declName`, and `n = info.fixedPrefixSize`.
 -/
-private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId) : MetaM (List Level × Array Expr) := withMVarContext mvarId do
-  let target ← getMVarType' mvarId
+private def getFixedPrefix (declName : Name) (info : EqnInfo) (mvarId : MVarId) : MetaM (List Level × Array Expr) := mvarId.withContext do
+  let target ← mvarId.getType'
   let some (_, lhs, _) := target.eq? | unreachable!
   let lhsArgs := lhs.getAppArgs
   if lhsArgs.size < info.fixedPrefixSize || !lhs.getAppFn matches .const .. then
@@ -155,7 +155,7 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
   trace[Elab.definition.wf.eqns] "proving: {type}"
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
-    let (_, mvarId) ← intros main.mvarId!
+    let (_, mvarId) ← main.mvarId!.intros
     let (us, fixedPrefix) ← getFixedPrefix declName info mvarId
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -25,7 +25,7 @@ private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
 private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
   let mvar ← mkFreshExprSyntheticOpaqueMVar decreasingProp
   let mvarId := mvar.mvarId!
-  let mvarId ← cleanup mvarId
+  let mvarId ← mvarId.cleanup
   match decrTactic? with
   | none => applyDefaultDecrTactic mvarId
   | some decrTactic =>

src/Lean/Elab/PreDefinition/WF/PackDomain.lean

@@ -49,7 +49,7 @@ private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Exp
       go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!)
     else
       let ys := ys.push (mkFVar y)
-      assignExprMVar mvarId (value.replaceFVars xs ys)
+      mvarId.assign (value.replaceFVars xs ys)
   go mvar.mvarId! y.fvarId! #[]
   instantiateMVars mvar
 

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -82,10 +82,10 @@ private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Arra
          else
            #[{ varNames := [varNames[i]!] }]
        let #[s₁, s₂] ← cases mvarId x (givenNames := givenNames) | unreachable!
-      assignExprMVar s₁.mvarId (mkApp preDefValues[i]! s₁.fields[0]!).headBeta
+      s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta
       go s₂.mvarId s₂.fields[0]!.fvarId! (i+1)
     else
-      assignExprMVar mvarId (mkApp preDefValues[i]! (mkFVar x)).headBeta
+      mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta
   go mvar.mvarId! x.fvarId! 0
   instantiateMVars mvar
 

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -42,15 +42,15 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
   let mut mvarId := mvarId
   for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
     unless localDecl.userName == varName do
-      mvarId ← rename mvarId localDecl.fvarId varName
+      mvarId ← mvarId.rename localDecl.fvarId varName
   let numPackedArgs := varNames.size - prefixSize
   let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) : TermElabM MVarId := do
     trace[Elab.definition.wf] "i: {i}, varNames: {varNames}, goal: {mvarId}"
     if i < numPackedArgs - 1 then
       let #[s] ← cases mvarId fvarId #[{ varNames := [varNames[prefixSize + i]!] }] | unreachable!
       go (i+1) s.mvarId s.fields[1]!.fvarId!
     else
-      rename mvarId fvarId varNames.back
+      mvarId.rename fvarId varNames.back
   go 0 mvarId fvarId
 
 def getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : Array PreDefinition) : MetaM (Array Nat) := do
@@ -115,16 +115,16 @@ where
   go (expectedType : Expr) (elements : Array TerminationByElement) : TermElabM α :=
     withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do
       let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
-      let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
-      let (d, fMVarId) ← intro1 fMVarId
+      let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
+      let (d, fMVarId) ← fMVarId.intro1
       let subgoals ← unpackMutual preDefs fMVarId d
       for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
         let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
-        withMVarContext mvarId do
-          let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← getMVarType mvarId)
-          assignExprMVar mvarId value
+        mvarId.withContext do
+          let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+          mvarId.assign value
       let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
-      assignExprMVar wfRelMVarId wfRelVal
+      wfRelMVarId.assign wfRelVal
       k (← instantiateMVars (mkMVar mainMVarId))
 
   generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do

src/Lean/Elab/StructInst.lean

@@ -705,7 +705,7 @@ partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (O
    | _ => match field.expr? with
      | none      => unreachable!
      | some expr => match defaultMissing? expr with
-       | some (.mvar mvarId) => return if (← isExprMVarAssigned mvarId) then none else some field
+       | some (.mvar mvarId) => return if (← mvarId.isAssigned) then none else some field
        | _                   => return none
 
 def getFieldName (field : Field Struct) : Name :=
@@ -811,7 +811,7 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar
           | none   =>
             let mvarDecl ← getMVarDecl mvarId
             let val ← ensureHasType mvarDecl.type val
-            assignExprMVar mvarId val
+            mvarId.assign val
             return true
       | _ => loop (i+1) dist
     else
@@ -829,7 +829,7 @@ partial def step (struct : Struct) : M Unit :=
           | some expr =>
             match defaultMissing? expr with
             | some (.mvar mvarId) =>
-              unless (← isExprMVarAssigned mvarId) do
+              unless (← mvarId.isAssigned) do
                 let ctx ← read
                 if (← withRef field.ref <| tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then
                   modify fun _ => { progress := true }