From 8335a82aedc280c0396d14192b607b8f6770fc9f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Jul 2022 21:33:29 -0700 Subject: [PATCH] refactor: improve `MVarId` method discoverability See issue #1346 --- RELEASES.md | 4 + src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/BuiltinTerm.lean | 6 +- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/MutualDef.lean | 2 +- src/Lean/Elab/PreDefinition/Eqns.lean | 46 +++--- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 26 ++-- src/Lean/Elab/PreDefinition/WF/Fix.lean | 2 +- .../Elab/PreDefinition/WF/PackDomain.lean | 2 +- .../Elab/PreDefinition/WF/PackMutual.lean | 4 +- src/Lean/Elab/PreDefinition/WF/Rel.lean | 16 +- src/Lean/Elab/StructInst.lean | 6 +- src/Lean/Elab/SyntheticMVars.lean | 24 +-- src/Lean/Elab/Tactic/Basic.lean | 18 +-- src/Lean/Elab/Tactic/BuiltinTactic.lean | 36 ++--- src/Lean/Elab/Tactic/Cache.lean | 2 +- src/Lean/Elab/Tactic/Calc.lean | 2 +- src/Lean/Elab/Tactic/Conv/Basic.lean | 24 +-- src/Lean/Elab/Tactic/Conv/Congr.lean | 18 +-- src/Lean/Elab/Tactic/Conv/Rewrite.lean | 2 +- src/Lean/Elab/Tactic/Delta.lean | 4 +- src/Lean/Elab/Tactic/ElabTerm.lean | 20 +-- src/Lean/Elab/Tactic/Induction.lean | 54 +++---- src/Lean/Elab/Tactic/Rewrite.lean | 8 +- src/Lean/Elab/Tactic/Simp.lean | 4 +- src/Lean/Elab/Tactic/Split.lean | 2 +- src/Lean/Elab/Term.lean | 8 +- src/Lean/Meta/AppBuilder.lean | 4 +- src/Lean/Meta/Basic.lean | 64 ++++++-- src/Lean/Meta/Closure.lean | 2 +- src/Lean/Meta/CollectMVars.lean | 2 +- src/Lean/Meta/DiscrTree.lean | 4 +- src/Lean/Meta/ExprDefEq.lean | 28 ++-- src/Lean/Meta/ForEachExpr.lean | 4 +- src/Lean/Meta/IndPredBelow.lean | 34 ++-- src/Lean/Meta/InferType.lean | 4 +- src/Lean/Meta/Injective.lean | 10 +- src/Lean/Meta/Match/Basic.lean | 2 +- src/Lean/Meta/Match/CaseArraySizes.lean | 26 ++-- src/Lean/Meta/Match/CaseValues.lean | 18 +-- src/Lean/Meta/Match/Match.lean | 6 +- src/Lean/Meta/Match/MatchEqs.lean | 24 +-- src/Lean/Meta/SynthInstance.lean | 10 +- src/Lean/Meta/Tactic/AC/Main.lean | 2 +- src/Lean/Meta/Tactic/Acyclic.lean | 4 +- src/Lean/Meta/Tactic/Apply.lean | 69 +++++---- src/Lean/Meta/Tactic/Assert.lean | 94 ++++++----- src/Lean/Meta/Tactic/Assumption.lean | 24 ++- src/Lean/Meta/Tactic/Cases.lean | 45 +++--- src/Lean/Meta/Tactic/Cleanup.lean | 33 ++-- src/Lean/Meta/Tactic/Clear.lean | 41 +++-- src/Lean/Meta/Tactic/Constructor.lean | 30 ++-- src/Lean/Meta/Tactic/Contradiction.lean | 26 ++-- src/Lean/Meta/Tactic/Delta.lean | 28 +++- src/Lean/Meta/Tactic/Generalize.lean | 16 +- src/Lean/Meta/Tactic/Induction.lean | 34 ++-- src/Lean/Meta/Tactic/Injection.lean | 22 +-- src/Lean/Meta/Tactic/Intro.lean | 85 +++++++--- src/Lean/Meta/Tactic/Refl.lean | 29 ++-- src/Lean/Meta/Tactic/Rename.lean | 17 +- src/Lean/Meta/Tactic/Replace.lean | 146 ++++++++++++------ src/Lean/Meta/Tactic/Revert.lean | 23 ++- src/Lean/Meta/Tactic/Rewrite.lean | 16 +- src/Lean/Meta/Tactic/Simp/Main.lean | 68 ++++---- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 10 +- src/Lean/Meta/Tactic/Split.lean | 48 +++--- src/Lean/Meta/Tactic/SplitIf.lean | 4 +- src/Lean/Meta/Tactic/Subst.lean | 50 +++--- src/Lean/Meta/Tactic/Unfold.lean | 6 +- src/Lean/Meta/Tactic/UnifyEq.lean | 14 +- src/Lean/Meta/Tactic/Util.lean | 90 +++++++---- src/Lean/MetavarContext.lean | 34 ++-- .../PrettyPrinter/Delaborator/Builtins.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 2 +- tests/lean/1163.lean | 2 +- tests/lean/474.lean | 6 +- tests/lean/byCasesMetaM.lean | 2 +- 78 files changed, 1015 insertions(+), 695 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index c8fb03e5de..efaf5453b4 100644 --- a/RELEASES.md +++ b/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 diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 38ca824bcb..a2f87d081c 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 794ca75886..bd759892c1 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index dff9a659b3..293b1eaf8c 100644 --- a/src/Lean/Elab/Match.lean +++ b/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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index b3671dd93e..e0db7b875c 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 5df7dee2d7..9b5ccb1c48 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/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) diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index a6b8f9af72..707814cbe8 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 4c0758bd4a..bc34de8a7a 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/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}" diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index f879f6c7c1..a808a1f960 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/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 => diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index 0a6d1dbe19..389c4ca591 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index d66ccb8e9e..723b885e89 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index fcde49b8f3..efbb5df66c 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -42,7 +42,7 @@ 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}" @@ -50,7 +50,7 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva 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 diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 7747b9498f..72c0fa11ef 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/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 } diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index bd8adccaa3..064f015390 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -22,7 +22,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo It returns `true` if it succeeded, and `false` otherwise. It is used to implement `synthesizeSyntheticMVars`. -/ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool := - withRef stx <| withMVarContext mvarId do + withRef stx <| mvarId.withContext do let s ← saveState try withSavedContext savedContext do @@ -35,7 +35,7 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId let result ← withRef stx <| ensureHasType expectedType result /- We must perform `occursCheck` here since `result` may contain `mvarId` when it has synthetic `sorry`s. -/ if (← occursCheck mvarId result) then - assignExprMVar mvarId result + mvarId.assign result return true else return false @@ -58,7 +58,7 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances are used. It also logs any error message produced. -/ private def synthesizePendingInstMVar (instMVar : MVarId) : TermElabM Bool := - withMVarContext instMVar do + instMVar.withContext do try synthesizeInstMVarCore instMVar catch @@ -73,7 +73,7 @@ private def synthesizePendingInstMVar (instMVar : MVarId) : TermElabM Bool := private def synthesizePendingCoeInstMVar (auxMVarId : MVarId) (errorMsgHeader? : Option String) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool := do let instMVarId := eNew.appArg!.mvarId! - withMVarContext instMVarId do + instMVarId.withContext do let eType ← instantiateMVars eType if (← isSyntheticMVar eType) then return false @@ -83,7 +83,7 @@ private def synthesizePendingCoeInstMVar However, it may succeed here because we have more information, for example, metavariables occurring at `expectedType` and `eType` may have been assigned. -/ if (← occursCheck auxMVarId e) then - assignExprMVar auxMVarId e + auxMVarId.assign e return true else return false @@ -91,7 +91,7 @@ private def synthesizePendingCoeInstMVar if (← synthesizeCoeInstMVarCore instMVarId) then let eNew ← expandCoe eNew if (← occursCheck auxMVarId eNew) then - assignExprMVar auxMVarId eNew + auxMVarId.assign eNew return true return false catch @@ -125,8 +125,8 @@ private def synthesizePendingCoeInstMVar Instead of performing a backtracking search that considers all pending metavariables, we improved the `binrel%` elaborator. -/ private partial def synthesizeUsingDefaultPrio (mvarId : MVarId) (prio : Nat) : TermElabM Bool := - withMVarContext mvarId do - let mvarType := (← Meta.getMVarDecl mvarId).type + mvarId.withContext do + let mvarType ← mvarId.getType match (← isClass? mvarType) with | none => return false | some className => @@ -146,7 +146,7 @@ where return false synthesizePendingInstMVar' (mvarId : MVarId) : TermElabM Bool := - commitWhen <| withMVarContext mvarId do + commitWhen <| mvarId.withContext do try synthesizeInstMVarCore mvarId catch _ => @@ -240,13 +240,13 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl match mvarSyntheticDecl.kind with | .typeClass => unless ignoreStuckTC do - withMVarContext mvarId do + mvarId.withContext do let mvarDecl ← getMVarDecl mvarId unless (← MonadLog.hasErrors) do throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}" | .coe header eNew expectedType eType e f? => let mvarId := eNew.appArg!.mvarId! - withMVarContext mvarId do + mvarId.withContext do let mvarDecl ← getMVarDecl mvarId throwTypeMismatchError header expectedType eType e f? (some ("failed to create type class instance for " ++ indentExpr mvarDecl.type)) | _ => unreachable! -- TODO handle other cases. @@ -360,7 +360,7 @@ mutual -- It would not be incorrect to use `filterM`. let remainingPendingMVars ← pendingMVars.filterRevM fun mvarId => do -- We use `traceM` because we want to make sure the metavar local context is used to trace the message - traceM `Elab.postpone (withMVarContext mvarId do addMessageContext m!"resuming {mkMVar mvarId}") + traceM `Elab.postpone (mvarId.withContext do addMessageContext m!"resuming {mkMVar mvarId}") let succeeded ← synthesizeSyntheticMVar mvarId postponeOnError runTactics if succeeded then markAsResolved mvarId trace[Elab.postpone] if succeeded then format "succeeded" else format "not ready yet" diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 6415fdb772..d7f6416a32 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -21,9 +21,9 @@ open Meta /-- Assign `mvarId := sorry` -/ def admitGoal (mvarId : MVarId) : MetaM Unit := - withMVarContext mvarId do + mvarId.withContext do let mvarType ← inferType (mkMVar mvarId) - assignExprMVar mvarId (← mkSorry mvarType (synthetic := true)) + mvarId.assign (← mkSorry mvarType (synthetic := true)) def goalsToMessageData (goals : List MVarId) : MessageData := MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n" @@ -48,7 +48,7 @@ structure Context where structure SavedState where term : Term.SavedState tactic : State - + abbrev TacticM := ReaderT Context $ StateRefT State TermElabM abbrev Tactic := Syntax → TacticM Unit @@ -64,7 +64,7 @@ def setGoals (mvarIds : List MVarId) : TacticM Unit := def pruneSolvedGoals : TacticM Unit := do let gs ← getGoals - let gs ← gs.filterM fun g => not <$> isExprMVarAssigned g + let gs ← gs.filterM fun g => not <$> g.isAssigned setGoals gs def getUnsolvedGoals : TacticM (List MVarId) := do @@ -78,7 +78,7 @@ def getUnsolvedGoals : TacticM (List MVarId) := do Prod.fst <$> x.runCore ctx s def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) := - withMVarContext mvarId do + mvarId.withContext do let pendingMVarsSaved := (← get).pendingMVars modify fun s => { s with pendingMVars := [] } let aux : TacticM (List MVarId) := @@ -304,7 +304,7 @@ where loop : List MVarId → TacticM MVarId | [] => throwNoGoalsToBeSolved | mvarId :: mvarIds => do - if (← isExprMVarAssigned mvarId) then + if (← mvarId.isAssigned) then loop mvarIds else setGoals (mvarId :: mvarIds) @@ -312,7 +312,7 @@ where /-- Return the main goal metavariable declaration. -/ def getMainDecl : TacticM MetavarDecl := do - getMVarDecl (← getMainGoal) + (← getMainGoal).getDecl /-- Return the main goal tag. -/ def getMainTag : TacticM Name := @@ -324,7 +324,7 @@ def getMainTarget : TacticM Expr := do /-- Execute `x` using the main goal local context and instances -/ def withMainContext (x : TacticM α) : TacticM α := do - withMVarContext (← getMainGoal) x + (← getMainGoal).withContext x /-- Evaluate `tac` at `mvarId`, and return the list of resulting subgoals. -/ def evalTacticAt (tac : Syntax) (mvarId : MVarId) : TacticM (List MVarId) := do @@ -348,7 +348,7 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do if checkUnassigned then ensureHasNoMVars val - assignExprMVar (← getMainGoal) val + (← getMainGoal).assign val replaceMainGoal [] @[inline] def liftMetaMAtMain (x : MVarId → MetaM α) : TacticM α := do diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index 78de6362e1..7ac4a1e833 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -116,7 +116,7 @@ private def getOptRotation (stx : Syntax) : Nat := let mvarIds ← getGoals let mut mvarIdsNew := #[] for mvarId in mvarIds do - unless (← isExprMVarAssigned mvarId) do + unless (← mvarId.isAssigned) do setGoals [mvarId] try evalTactic stx[1] @@ -134,7 +134,7 @@ private def getOptRotation (stx : Syntax) : Nat := let mut mvarIdsNew := #[] let mut succeeded := false for mvarId in mvarIds do - unless (← isExprMVarAssigned mvarId) do + unless (← mvarId.isAssigned) do setGoals [mvarId] try evalTactic stx[1] @@ -181,13 +181,13 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := | some msg => withRef stx[0] <| addRawTrace msg @[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun _ => - liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure [] + liftMetaTactic fun mvarId => do mvarId.assumption; pure [] @[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun _ => liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure [] @[builtinTactic Lean.Parser.Tactic.refl] def evalRefl : Tactic := fun _ => - liftMetaTactic fun mvarId => do Meta.refl mvarId; pure [] + liftMetaTactic fun mvarId => do mvarId.refl; pure [] @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do match stx with @@ -200,7 +200,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := where introStep (ref : Option Syntax) (n : Name) : TacticM Unit := do let fvar ← liftMetaTacticAux fun mvarId => do - let (fvar, mvarId) ← Meta.intro mvarId n + let (fvar, mvarId) ← mvarId.intro n pure (fvar, [mvarId]) if let some stx := ref then withMainContext do @@ -214,11 +214,11 @@ where @[builtinTactic «intros»] def evalIntros : Tactic := fun stx => match stx with | `(tactic| intros) => liftMetaTactic fun mvarId => do - let (_, mvarId) ← Meta.intros mvarId + let (_, mvarId) ← mvarId.intros return [mvarId] | `(tactic| intros $ids*) => do let fvars ← liftMetaTacticAux fun mvarId => do - let (fvars, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList + let (fvars, mvarId) ← mvarId.introN ids.size (ids.map getNameOfIdent').toList return (fvars, [mvarId]) withMainContext do for stx in ids, fvar in fvars do @@ -228,7 +228,7 @@ where @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx => match stx with | `(tactic| revert $hs*) => do - let (_, mvarId) ← Meta.revert (← getMainGoal) (← getFVarIds hs) + let (_, mvarId) ← (← getMainGoal).revert (← getFVarIds hs) replaceMainGoal [mvarId] | _ => throwUnsupportedSyntax @@ -239,7 +239,7 @@ where let fvarIds ← withMainContext <| sortFVarIds fvarIds for fvarId in fvarIds.reverse do withMainContext do - let mvarId ← clear (← getMainGoal) fvarId + let mvarId ← (← getMainGoal).clear fvarId replaceMainGoal [mvarId] | _ => throwUnsupportedSyntax @@ -263,18 +263,18 @@ def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : If none then searches for a metavariable `g` s.t. `tag` is a suffix of its name. If none, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do - match (← mvarIds.findM? fun mvarId => return tag == (← getMVarDecl mvarId).userName) with + match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName) with | some mvarId => return mvarId | none => - match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName) with + match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName) with | some mvarId => return mvarId - | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName + | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : TacticM MVarId := do if hs.isEmpty then return mvarId else - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let mut lctx := mvarDecl.lctx let mut hs := hs let mut info := #[] @@ -297,10 +297,10 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta unless hs.isEmpty do logError m!"too many variable names provided" let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName - withSaveInfoContext <| withMVarContext mvarNew.mvarId! do + withSaveInfoContext <| mvarNew.mvarId!.withContext do for (fvarId, stx) in info do Term.addLocalVarInfo stx (mkFVar fvarId) - assignExprMVar mvarId mvarNew + mvarId.assign mvarNew return mvarNew.mvarId! private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List MVarId) := do @@ -318,7 +318,7 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List let (g, gs) ← getCaseGoals tag let g ← renameInaccessibles g hs setGoals [g] - setMVarTag g Name.anonymous + g.setTag Name.anonymous withCaseRef arr tac do closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac)) setGoals gs @@ -328,12 +328,12 @@ private def getCaseGoals (tag : TSyntax ``binderIdent) : TacticM (MVarId × List | `(tactic| case' $tag $hs* =>%$arr $tac:tacticSeq) => do let (g, gs) ← getCaseGoals tag let g ← renameInaccessibles g hs - let mvarTag ← getMVarTag g + let mvarTag ← g.getTag setGoals [g] withCaseRef arr tac (evalTactic tac) let gs' ← getUnsolvedGoals if let [g'] := gs' then - setMVarTag g' mvarTag + g'.setTag mvarTag setGoals (gs' ++ gs) | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Cache.lean b/src/Lean/Elab/Tactic/Cache.lean index b0bf868de6..9555ca5ea0 100644 --- a/src/Lean/Elab/Tactic/Cache.lean +++ b/src/Lean/Elab/Tactic/Cache.lean @@ -40,7 +40,7 @@ private def dbg_cache' (cacheRef : IO.Ref Cache) (pos : String.Pos) (mvarId : MV private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax) (pos : String.Pos) : TacticM (Option Snapshot) := do let some s := (← cacheRef.get).pre.find? { mvarId, pos } | do dbg_cache "cache key not found"; return none - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let some mvarDeclOld := s.meta.mctx.findDecl? mvarId | return none if equivMVarDecl mvarDecl mvarDeclOld then if stx == s.stx then diff --git a/src/Lean/Elab/Tactic/Calc.lean b/src/Lean/Elab/Tactic/Calc.lean index bfedc8d818..65f24ff9c5 100644 --- a/src/Lean/Elab/Tactic/Calc.lean +++ b/src/Lean/Elab/Tactic/Calc.lean @@ -43,5 +43,5 @@ def evalCalc : Tactic := fun stx => do return val let val ← instantiateMVars val let mvarId ← getMainGoal - assignExprMVar mvarId val + mvarId.assign val replaceMainGoal mvarIds diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean index 2e8783220c..5f5eacf5eb 100644 --- a/src/Lean/Elab/Tactic/Conv/Basic.lean +++ b/src/Lean/Elab/Tactic/Conv/Basic.lean @@ -22,10 +22,10 @@ def mkConvGoalFor (lhs : Expr) : MetaM (Expr × Expr) := do return (rhs, newGoal) def markAsConvGoal (mvarId : MVarId) : MetaM MVarId := do - let target ← getMVarType mvarId + let target ← mvarId.getType if isLHSGoal? target |>.isSome then return mvarId -- it is already tagged as LHS goal - replaceTargetDefEq mvarId (mkLHSGoal (← getMVarType mvarId)) + mvarId.replaceTargetDefEq (mkLHSGoal (← mvarId.getType)) /-- Given `lhs`, runs the `conv` tactic with the goal `⊢ lhs = ?rhs`. `conv` should produce no remaining goals that are not solvable with refl. @@ -50,8 +50,8 @@ def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do return (← instantiateMVars rhs, ← instantiateMVars newGoal) def getLhsRhsCore (mvarId : MVarId) : MetaM (Expr × Expr) := - withMVarContext mvarId do - let some (_, lhs, rhs) ← matchEq? (← getMVarType mvarId) | throwError "invalid 'conv' goal" + mvarId.withContext do + let some (_, lhs, rhs) ← matchEq? (← mvarId.getType) | throwError "invalid 'conv' goal" return (lhs, rhs) def getLhsRhs : TacticM (Expr × Expr) := do @@ -67,14 +67,14 @@ def getRhs : TacticM Expr := def updateLhs (lhs' : Expr) (h : Expr) : TacticM Unit := do let rhs ← getRhs let newGoal ← mkFreshExprSyntheticOpaqueMVar (mkLHSGoal (← mkEq lhs' rhs)) - assignExprMVar (← getMainGoal) (← mkEqTrans h newGoal) + (← getMainGoal).assign (← mkEqTrans h newGoal) replaceMainGoal [newGoal.mvarId!] /-- Replace `lhs` with the definitionally equal `lhs'`. -/ def changeLhs (lhs' : Expr) : TacticM Unit := do let rhs ← getRhs liftMetaTactic1 fun mvarId => do - replaceTargetDefEq mvarId (mkLHSGoal (← mkEq lhs' rhs)) + mvarId.replaceTargetDefEq (mkLHSGoal (← mkEq lhs' rhs)) @[builtinTactic Lean.Parser.Tactic.Conv.whnf] def evalWhnf : Tactic := fun _ => withMainContext do @@ -115,11 +115,11 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do /-- Mark goals of the form `⊢ a = ?m ..` with the conv goal annotation -/ def remarkAsConvGoal : TacticM Unit := do - let newGoals ← (← getUnsolvedGoals).mapM fun mvarId => withMVarContext mvarId do - let target ← getMVarType mvarId + let newGoals ← (← getUnsolvedGoals).mapM fun mvarId => mvarId.withContext do + let target ← mvarId.getType if let some (_, _, rhs) ← matchEq? target then if rhs.getAppFn.isMVar then - replaceTargetDefEq mvarId (mkLHSGoal target) + mvarId.replaceTargetDefEq (mkLHSGoal target) else return mvarId else @@ -135,20 +135,20 @@ def remarkAsConvGoal : TacticM Unit := do let target ← getMainTarget if let some _ := isLHSGoal? target then liftMetaTactic1 fun mvarId => - replaceTargetDefEq mvarId target.mdataExpr! + mvarId.replaceTargetDefEq target.mdataExpr! focus do evalTactic seq; remarkAsConvGoal private def convTarget (conv : Syntax) : TacticM Unit := withMainContext do let target ← getMainTarget let (targetNew, proof) ← convert target (withTacticInfoContext (← getRef) (evalTactic conv)) - liftMetaTactic1 fun mvarId => replaceTargetEq mvarId targetNew proof + liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof evalTactic (← `(tactic| try rfl)) private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := withMainContext do let localDecl ← getLocalDeclFromUserName hUserName let (typeNew, proof) ← convert localDecl.type (withTacticInfoContext (← getRef) (evalTactic conv)) liftMetaTactic1 fun mvarId => - return some (← replaceLocalDecl mvarId localDecl.fvarId typeNew proof).mvarId + return some (← mvarId.replaceLocalDecl localDecl.fvarId typeNew proof).mvarId @[builtinTactic Lean.Parser.Tactic.Conv.conv] def evalConv : Tactic := fun stx => do match stx with diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 78e6b4d12b..a716224bb7 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -40,11 +40,11 @@ private def congrApp (mvarId : MVarId) (lhs rhs : Expr) (addImplicitArgs := fals let proof ← r.getProof unless (← isDefEqGuarded rhs r.expr) do throwError "invalid 'congr' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr r.expr}" - assignExprMVar mvarId proof + mvarId.assign proof return newGoals.toList private def congrImplies (mvarId : MVarId) : MetaM (List MVarId) := do - let [mvarId₁, mvarId₂, _, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``implies_congr) | throwError "'apply implies_congr' unexpected result" + let [mvarId₁, mvarId₂, _, _] ← mvarId.apply (← mkConstWithFreshMVarLevels ``implies_congr) | throwError "'apply implies_congr' unexpected result" let mvarId₁ ← markAsConvGoal mvarId₁ let mvarId₂ ← markAsConvGoal mvarId₂ return [mvarId₁, mvarId₂] @@ -57,7 +57,7 @@ def isImplies (e : Expr) : MetaM Bool := return false def congr (mvarId : MVarId) (addImplicitArgs := false) : MetaM (List (Option MVarId)) := - withMVarContext mvarId do + mvarId.withContext do let (lhs, rhs) ← getLhsRhsCore mvarId let lhs := (← instantiateMVars lhs).consumeMData if (← isImplies lhs) then @@ -131,18 +131,18 @@ def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) let arg ← mkLambdaFVars #[x] mvarNew return (arg, mvarNew.mvarId!) let val := mkApp6 (mkConst ``let_body_congr [u₁, u₂]) t β f f' v arg - assignExprMVar mvarId val + mvarId.assign val return some (← markAsConvGoal mvarId') | _ => return none private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId := - withMVarContext mvarId do + mvarId.withContext do let userNames := if let some userName := userName? then [userName] else [] let (lhs, rhs) ← getLhsRhsCore mvarId let lhs ← instantiateMVars lhs if lhs.isForall then - let [mvarId, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result" - let (_, mvarId) ← introN mvarId 1 userNames + let [mvarId, _] ← mvarId.apply (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result" + let (_, mvarId) ← mvarId.introN 1 userNames markAsConvGoal mvarId else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then return mvarId @@ -150,8 +150,8 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : let lhsType ← whnfD (← inferType lhs) unless lhsType.isForall do throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}" - let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result" - let (_, mvarId) ← introN mvarId 1 userNames + let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result" + let (_, mvarId) ← mvarId.introN 1 userNames markAsConvGoal mvarId private def ext (userName? : Option Name) : TacticM Unit := do diff --git a/src/Lean/Elab/Tactic/Conv/Rewrite.lean b/src/Lean/Elab/Tactic/Conv/Rewrite.lean index 3b904db60f..39861871c2 100644 --- a/src/Lean/Elab/Tactic/Conv/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Conv/Rewrite.lean @@ -15,7 +15,7 @@ open Meta withRWRulesSeq stx[0] stx[2] fun symm term => do Term.withSynthesize <| withMainContext do let e ← elabTerm term none true - let r ← rewrite (← getMainGoal) (← getLhs) e symm (config := config) + let r ← (← getMainGoal).rewrite (← getLhs) e symm (config := config) updateLhs r.eNew r.eqProof replaceMainGoal ((← getMainGoal) :: r.mvarIds) diff --git a/src/Lean/Elab/Tactic/Delta.lean b/src/Lean/Elab/Tactic/Delta.lean index 1efc3a5776..67b0c3a5dd 100644 --- a/src/Lean/Elab/Tactic/Delta.lean +++ b/src/Lean/Elab/Tactic/Delta.lean @@ -16,7 +16,7 @@ def deltaLocalDecl (declName : Name) (fvarId : FVarId) : TacticM Unit := do let typeNew ← deltaExpand localDecl.type (· == declName) if typeNew == localDecl.type then throwTacticEx `delta mvarId m!"did not delta reduce '{declName}' at '{localDecl.userName}'" - replaceMainGoal [← replaceLocalDeclDefEq mvarId fvarId typeNew] + replaceMainGoal [← mvarId.replaceLocalDeclDefEq fvarId typeNew] def deltaTarget (declName : Name) : TacticM Unit := do let mvarId ← getMainGoal @@ -24,7 +24,7 @@ def deltaTarget (declName : Name) : TacticM Unit := do let targetNew ← deltaExpand target (· == declName) if targetNew == target then throwTacticEx `delta mvarId m!"did not delta reduce '{declName}'" - replaceMainGoal [← replaceTargetDefEq mvarId targetNew] + replaceMainGoal [← mvarId.replaceTargetDefEq targetNew] /-- "delta " ident (location)? diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 663f45f190..2f1d304179 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -76,8 +76,8 @@ def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNatur let newMVarIds ← if allowNaturalHoles then pure newMVarIds.toList else - let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural - let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural + let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural + let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← mvarId.getKind).isNatural let naturalMVarIds ← filterOldMVars naturalMVarIds mvarCounterSaved logUnassignedAndAbort naturalMVarIds pure syntheticMVarIds.toList @@ -99,7 +99,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta unless val == mkMVar mvarId do if val.findMVar? (· == mvarId) matches some _ then throwError "'refine' tactic failed, value{indentExpr val}\ndepends on the main goal metavariable '{mkMVar mvarId}'" - assignExprMVar mvarId val + mvarId.assign val replaceMainGoal mvarIds' @[builtinTactic «refine»] def evalRefine : Tactic := fun stx => @@ -119,9 +119,9 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta let h := e.getAppFn if h.isFVar then let localDecl ← getLocalDecl h.fvarId! - let mvarId ← assert (← getMainGoal) localDecl.userName (← inferType e).headBeta e - let (_, mvarId) ← intro1P mvarId - let mvarId ← tryClear mvarId h.fvarId! + let mvarId ← (← getMainGoal).assert localDecl.userName (← inferType e).headBeta e + let (_, mvarId) ← mvarId.intro1P + let mvarId ← mvarId.tryClear h.fvarId! replaceMainGoal (mvarId :: mvarIds') else throwError "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context" @@ -205,12 +205,12 @@ def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do @[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic := fun stx => match stx with - | `(tactic| apply $e) => evalApplyLikeTactic Meta.apply e + | `(tactic| apply $e) => evalApplyLikeTactic (·.apply) e | _ => throwUnsupportedSyntax @[builtinTactic Lean.Parser.Tactic.constructor] def evalConstructor : Tactic := fun _ => withMainContext do - let mvarIds' ← Meta.constructor (← getMainGoal) + let mvarIds' ← (← getMainGoal).constructor Term.synthesizeSyntheticMVarsNoPostponing replaceMainGoal mvarIds' @@ -236,7 +236,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do let mvarId ← getMainGoal let (fvarId, mvarId) ← liftMetaM do - let mvarId ← Meta.assert mvarId userName type e + let mvarId ← mvarId.assert userName type e Meta.intro1Core mvarId preserveBinderNames replaceMainGoal [mvarId] return fvarId @@ -258,7 +258,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId match fvarId? with | none => throwError "failed to find a hypothesis with type{indentExpr type}" | some fvarId => return fvarId - replaceMainGoal [← rename (← getMainGoal) fvarId h.getId] + replaceMainGoal [← (← getMainGoal).rename fvarId h.getId] | _ => throwUnsupportedSyntax /-- diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 1acf41703a..a9f9d88332 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -55,10 +55,10 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (remainingGoals : Array MVarId) : T let rhs := getAltRHS alt withCaseRef (getAltDArrow alt) rhs do if isHoleRHS rhs then - let gs' ← withMVarContext mvarId $ withRef rhs do - let mvarDecl ← getMVarDecl mvarId + let gs' ← mvarId.withContext <| withRef rhs do + let mvarDecl ← mvarId.getDecl let val ← elabTermEnsuringType rhs mvarDecl.type - assignExprMVar mvarId val + mvarId.assign val let gs' ← getMVarsNoDelayed val tagUntaggedGoals mvarDecl.userName `induction gs'.toList pure gs' @@ -156,12 +156,12 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) for mvarId in s.insts do try unless (← Term.synthesizeInstMVarCore mvarId) do - setMVarKind mvarId MetavarKind.syntheticOpaque + mvarId.setKind .syntheticOpaque others := others.push mvarId catch _ => - setMVarKind mvarId MetavarKind.syntheticOpaque + mvarId.setKind .syntheticOpaque others := others.push mvarId - let alts ← s.alts.filterM fun alt => return !(← isExprMVarAssigned alt.2) + let alts ← s.alts.filterM fun alt => return !(← alt.2.isAssigned) return { elimApp := (← instantiateMVars s.f), alts, others := others } /-- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign @@ -173,7 +173,7 @@ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) let motiveType ← inferType (mkMVar motiveArg) unless (← isDefEqGuarded motiverInferredType motiveType) do throwError "type mismatch when assigning motive{indentExpr motive}\n{← mkHasTypeButIsExpectedMsg motiverInferredType motiveType}" - assignExprMVar motiveArg motive + motiveArg.assign motive private def getAltNumFields (elimInfo : ElimInfo) (altName : Name) : TermElabM Nat := do for altInfo in elimInfo.altsInfo do @@ -194,14 +194,14 @@ private def checkAltNames (alts : Array (Name × MVarId)) (altsSyntax : Array Sy /-- Given the goal `altMVarId` for a given alternative that introduces `numFields` new variables, return the number of explicit variables. Recall that when the `@` is not used, only the explicit variables can be named by the user. -/ -private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := withMVarContext altMVarId do - let target ← getMVarType altMVarId +private def getNumExplicitFields (altMVarId : MVarId) (numFields : Nat) : MetaM Nat := altMVarId.withContext do + let target ← altMVarId.getType withoutModifyingState do let (_, bis, _) ← forallMetaBoundedTelescope target numFields return bis.foldl (init := 0) fun r bi => if bi.isExplicit then r + 1 else r private def saveAltVarsInfo (altMVarId : MVarId) (altStx : Syntax) (fvarIds : Array FVarId) : TacticM Unit := - withSaveInfoContext <| withMVarContext altMVarId do + withSaveInfoContext <| altMVarId.withContext do let useNamesForExplicitOnly := !altHasExplicitModifier altStx let mut i := 0 let altVars := getAltVars altStx @@ -277,13 +277,13 @@ where pure none match altStx? with | none => - let mut (_, altMVarId) ← introN altMVarId numFields + let mut (_, altMVarId) ← altMVarId.introN numFields match (← Cases.unifyEqs? numEqs altMVarId {}) with | none => pure () -- alternative is not reachable | some (altMVarId', _) => - (_, altMVarId) ← introNP altMVarId' numGeneralized + (_, altMVarId) ← altMVarId'.introNP numGeneralized for fvarId in toClear do - altMVarId ← tryClear altMVarId fvarId + altMVarId ← altMVarId.tryClear fvarId let altMVarIds ← applyPreTac altMVarId if !hasAlts then -- User did not provide alternatives using `|` @@ -304,14 +304,14 @@ where let numFieldsToName ← if altHasExplicitModifier altStx then pure numFields else getNumExplicitFields altMVarId numFields if altVarNames.size > numFieldsToName then logError m!"too many variable names provided at alternative '{altName}', #{altVarNames.size} provided, but #{numFieldsToName} expected" - let mut (fvarIds, altMVarId) ← introN altMVarId numFields altVarNames.toList (useNamesForExplicitOnly := !altHasExplicitModifier altStx) + let mut (fvarIds, altMVarId) ← altMVarId.introN numFields altVarNames.toList (useNamesForExplicitOnly := !altHasExplicitModifier altStx) saveAltVarsInfo altMVarId altStx fvarIds match (← Cases.unifyEqs? numEqs altMVarId {}) with | none => unusedAlt | some (altMVarId', _) => - (_, altMVarId) ← introNP altMVarId' numGeneralized + (_, altMVarId) ← altMVarId'.introNP numGeneralized for fvarId in toClear do - altMVarId ← tryClear altMVarId fvarId + altMVarId ← altMVarId.tryClear fvarId let altMVarIds ← applyPreTac altMVarId if altMVarIds.isEmpty then unusedAlt @@ -352,7 +352,7 @@ private def getUserGeneralizingFVarIds (stx : Syntax) : TacticM (Array FVarId) : -- process `generalizingVars` subterm of induction Syntax `stx`. private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Expr) : TacticM (Nat × MVarId) := - withMVarContext mvarId do + mvarId.withContext do let userFVarIds ← getUserGeneralizingFVarIds stx let forbidden ← mkGeneralizationForbiddenSet targets let mut s ← getFVarSetToGeneralize targets forbidden @@ -363,7 +363,7 @@ private def generalizeVars (mvarId : MVarId) (stx : Syntax) (targets : Array Exp throwError "unnecessary 'generalizing' argument, variable '{mkFVar userFVarId}' is generalized automatically" s := s.insert userFVarId let fvarIds ← sortFVarIds s.toArray - let (fvarIds, mvarId') ← Meta.revert mvarId fvarIds + let (fvarIds, mvarId') ← mvarId.revert fvarIds return (fvarIds.size, mvarId') /-- @@ -509,20 +509,20 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do let mvarId ← getMainGoal -- save initial info before main goal is reassigned let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef) - let tag ← getMVarTag mvarId - withMVarContext mvarId do + let tag ← mvarId.getTag + mvarId.withContext do let targets ← addImplicitTargets elimInfo targets checkTargets targets let targetFVarIds := targets.map (·.fvarId!) let (n, mvarId) ← generalizeVars mvarId stx targets - withMVarContext mvarId do + mvarId.withContext do let result ← withRef stx[1] do -- use target position as reference ElimApp.mkElimApp elimInfo targets tag trace[Elab.induction] "elimApp: {result.elimApp}" let elimArgs := result.elimApp.getAppArgs ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts - assignExprMVar mvarId result.elimApp + mvarId.assign result.elimApp ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numGeneralized := n) (toClear := targetFVarIds) appendGoals result.others.toList where @@ -570,18 +570,18 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) := let mvarId ← getMainGoal -- save initial info before main goal is reassigned let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef) - let tag ← getMVarTag mvarId - withMVarContext mvarId do + let tag ← mvarId.getTag + mvarId.withContext do let targets ← addImplicitTargets elimInfo targets let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag let elimArgs := result.elimApp.getAppArgs let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]! let motiveType ← inferType elimArgs[elimInfo.motivePos]! let mvarId ← generalizeTargetsEq mvarId motiveType targets - let (targetsNew, mvarId) ← introN mvarId targets.size - withMVarContext mvarId do + let (targetsNew, mvarId) ← mvarId.introN targets.size + mvarId.withContext do ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew - assignExprMVar mvarId result.elimApp + mvarId.assign result.elimApp ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew) builtin_initialize diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index d8339fc9d5..78f1ec5536 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -15,16 +15,16 @@ open Meta def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do Term.withSynthesize <| withMainContext do let e ← elabTerm stx none true - let r ← rewrite (← getMainGoal) (← getMainTarget) e symm (config := config) - let mvarId' ← replaceTargetEq (← getMainGoal) r.eNew r.eqProof + let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config) + let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof replaceMainGoal (mvarId' :: r.mvarIds) def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do Term.withSynthesize <| withMainContext do let e ← elabTerm stx none true let localDecl ← getLocalDecl fvarId - let rwResult ← rewrite (← getMainGoal) localDecl.type e symm (config := config) - let replaceResult ← replaceLocalDecl (← getMainGoal) fvarId rwResult.eNew rwResult.eqProof + let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config) + let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds) def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index d4f0e8efbb..0dc075d41a 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -266,7 +266,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non go fvarIds simplifyTarget fvarIdToLemmaId | Location.wildcard => withMainContext do - go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToLemmaId + go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) fvarIdToLemmaId where go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToLemmaId : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do let mvarId ← getMainGoal @@ -297,7 +297,7 @@ def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do go fvarIds simplifyTarget | Location.wildcard => withMainContext do - go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) + go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) where go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do let mvarId ← getMainGoal diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean index a4a905f393..5615c48a0a 100644 --- a/src/Lean/Elab/Tactic/Split.lean +++ b/src/Lean/Elab/Tactic/Split.lean @@ -29,7 +29,7 @@ open Meta return mvarIds | Location.wildcard => liftMetaTactic fun mvarId => do - let fvarIds ← getNondepPropHyps mvarId + let fvarIds ← mvarId.getNondepPropHyps for fvarId in fvarIds do if let some mvarIds ← splitLocalDecl? mvarId fvarId then return mvarIds diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f520e36195..e6470116be 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -562,7 +562,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op -- To sort the errors by position use -- let sortedErrors := errors.qsort fun e₁ e₂ => e₁.ref.getPos?.getD 0 < e₂.ref.getPos?.getD 0 for error in errors do - withMVarContext error.mvarId do + error.mvarId.withContext do error.logError extraMsg? return hasNewErrors @@ -717,7 +717,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n let result ← trySynthInstance type maxResultSize? match result with | LOption.some val => - if (← isExprMVarAssigned instMVar) then + if (← instMVar.isAssigned) then let oldVal ← instantiateMVars (mkMVar instMVar) unless (← isDefEq oldVal val) do if (← containsPendingMVar oldVal <||> containsPendingMVar val) then @@ -1485,7 +1485,7 @@ where match mvarIds with | [] => return result | mvarId :: mvarIds => do - if (← isExprMVarAssigned mvarId) then + if (← mvarId.isAssigned) then go mvarIds result else if result.contains (mkMVar mvarId) || except mvarId then go mvarIds result @@ -1778,7 +1778,7 @@ def exprToSyntax (e : Expr) : TermElabM Term := withFreshMacroScope do let result ← `(?m) let eType ← inferType e let mvar ← elabTerm result eType - assignExprMVar mvar.mvarId! e + mvar.mvarId!.assign e return result end Term diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 450108cab7..fee4999d59 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -207,9 +207,9 @@ def mkCongr (h₁ h₂ : Expr) : MetaM Expr := do private def mkAppMFinal (methodName : Name) (f : Expr) (args : Array Expr) (instMVars : Array MVarId) : MetaM Expr := do instMVars.forM fun mvarId => do - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let mvarVal ← synthInstance mvarDecl.type - assignExprMVar mvarId mvarVal + mvarId.assign mvarVal let result ← instantiateMVars (mkAppN f args) if (← hasAssignableMVar result) then throwAppBuilderException methodName ("result contains metavariables" ++ indentExpr result) return result diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 63e08c81b3..ec8dce9609 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -516,41 +516,69 @@ def shouldReduceAll : MetaM Bool := def shouldReduceReducibleOnly : MetaM Bool := return (← getTransparency) == TransparencyMode.reducible -def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) := +def _root_.Lean.MVarId.findDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) := return (← getMCtx).findDecl? mvarId -def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do - match (← findMVarDecl? mvarId) with +@[deprecated MVarId.findDecl?] +def findMVarDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl) := + mvarId.findDecl? + +def _root_.Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl := do + match (← mvarId.findDecl?) with | some d => pure d | none => throwError "unknown metavariable '?{mvarId.name}'" +@[deprecated MVarId.getDecl] +def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do + mvarId.getDecl + +def _root_.Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind := + return (← mvarId.getDecl).kind + +@[deprecated MVarId.getKind] def getMVarDeclKind (mvarId : MVarId) : MetaM MetavarKind := - return (← getMVarDecl mvarId).kind + mvarId.getKind /-- Reture `true` if `e` is a synthetic (or synthetic opaque) metavariable -/ def isSyntheticMVar (e : Expr) : MetaM Bool := do if e.isMVar then - return (← getMVarDeclKind e.mvarId!) matches .synthetic | .syntheticOpaque + return (← e.mvarId!.getKind) matches .synthetic | .syntheticOpaque else return false -def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := +def _root_.Lean.MVarId.setKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := modifyMCtx fun mctx => mctx.setMVarKind mvarId kind +@[deprecated MVarId.setKind] +def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := + mvarId.setKind kind + /-- Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one -/ -def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do +def _root_.Lean.MVarId.setType (mvarId : MVarId) (type : Expr) : MetaM Unit := do modifyMCtx fun mctx => mctx.setMVarType mvarId type -def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do - return (← getMVarDecl mvarId).depth != (← getMCtx).depth +@[deprecated MVarId.setType] +def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do + mvarId.setType type -def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do - let mvarDecl ← getMVarDecl mvarId +def _root_.Lean.MVarId.isReadOnly (mvarId : MVarId) : MetaM Bool := do + return (← mvarId.getDecl).depth != (← getMCtx).depth + +@[deprecated MVarId.isReadOnly] +def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do + mvarId.isReadOnly + +def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Bool := do + let mvarDecl ← mvarId.getDecl match mvarDecl.kind with | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque | _ => return mvarDecl.depth != (← getMCtx).depth +@[deprecated MVarId.isReadOnlyOrSyntheticOpaque] +def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do + mvarId.isReadOnlyOrSyntheticOpaque + def getLevelMVarDepth (mvarId : LMVarId) : MetaM Nat := do match (← getMCtx).findLevelDepth? mvarId with | some depth => return depth @@ -562,9 +590,13 @@ def isReadOnlyLevelMVar (mvarId : LMVarId) : MetaM Bool := do else return (← getLevelMVarDepth mvarId) != (← getMCtx).depth -def setMVarUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit := +def _root_.Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit := modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName +@[deprecated MVarId.setUserName] +def setMVarUserName (mvarId : MVarId) (userNameNew : Name) : MetaM Unit := + mvarId.setUserName userNameNew + def throwUnknownFVar (fvarId : FVarId) : MetaM α := throwError "unknown free variable '{mkFVar fvarId}'" @@ -1184,16 +1216,20 @@ def withLCtx (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α mapMetaM <| withLocalContextImp lctx localInsts private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl withLocalContextImp mvarDecl.lctx mvarDecl.localInstances 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) : n α → n α := +def _root_.Lean.MVarId.withContext (mvarId : MVarId) : n α → n α := mapMetaM <| withMVarContextImp mvarId +@[deprecated MVarId.withContext] +def withMVarContext (mvarId : MVarId) : n α → n α := + mvarId.withContext + private def withMCtxImp (mctx : MetavarContext) (x : MetaM α) : MetaM α := do let mctx' ← getMCtx setMCtx mctx diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index 3a9a52a716..cc5e7007f8 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -197,7 +197,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do | Expr.sort u => return e.updateSort! (← collectLevel u) | Expr.const _ us => return e.updateConst! (← us.mapM collectLevel) | Expr.mvar mvarId => - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let type ← preprocess mvarDecl.type let type ← collect type let newFVarId ← mkFreshFVarId diff --git a/src/Lean/Meta/CollectMVars.lean b/src/Lean/Meta/CollectMVars.lean index aebdddb8f8..adc6c5c7c5 100644 --- a/src/Lean/Meta/CollectMVars.lean +++ b/src/Lean/Meta/CollectMVars.lean @@ -36,7 +36,7 @@ def getMVars (e : Expr) : MetaM (Array MVarId) := do /-- Similar to getMVars, but removes delayed assignments. -/ def getMVarsNoDelayed (e : Expr) : MetaM (Array MVarId) := do let mvarIds ← getMVars e - mvarIds.filterM fun mvarId => not <$> isMVarDelayedAssigned mvarId + mvarIds.filterM fun mvarId => not <$> mvarId.isDelayedAssigned def collectMVarsAtDecl (d : Declaration) : StateRefT CollectMVars.State MetaM Unit := d.forExprM collectMVars diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index b068fe00a6..2d12df47e1 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -296,7 +296,7 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key if mvarId == tmpMVarId then -- We use `tmp to mark implicit arguments and proofs return (Key.star, todo) - else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + else if (← mvarId.isReadOnlyOrSyntheticOpaque) then return (Key.other, todo) else return (Key.star, todo) @@ -424,7 +424,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex This is incorrect because it is equivalent to saying that there is no solution even if the caller assigns `?m` and try again. -/ return (Key.star, #[]) - else if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + else if (← mvarId.isReadOnlyOrSyntheticOpaque) then return (Key.other, #[]) else return (Key.star, #[]) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 154cf2ff2e..88f2c831ac 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -125,9 +125,9 @@ def isDefEqStringLit (s t : Expr) : MetaM LBool := do def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do match e.etaExpanded? with | some (Expr.mvar mvarId) => - if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + if (← mvarId.isReadOnlyOrSyntheticOpaque) then pure false - else if (← isExprMVarAssigned mvarId) then + else if (← mvarId.isAssigned) then pure false else pure true @@ -324,7 +324,7 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool := let vType ← inferType v if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then trace[Meta.isDefEq.assign.final] "{mvar} := {v}" - assignExprMVar mvar.mvarId! v + mvar.mvarId!.assign v pure true else trace[Meta.isDefEq.assign.typeMismatch] "{mvar} : {mvarType} := {v} : {vType}" @@ -655,7 +655,7 @@ private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData return m!"{msg} @ {mkMVar ctx.mvarId} {ctx.fvars} := {ctx.rhs}" @[inline] def run (x : CheckAssignmentM Expr) (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : MetaM (Option Expr) := do - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let ctx := { mvarId := mvarId, mvarDecl := mvarDecl, fvars := fvars, hasCtxLocals := hasCtxLocals, rhs := v : Context } let x : CheckAssignmentM (Option Expr) := catchInternalIds [outOfScopeExceptionId, checkAssignmentExceptionId] @@ -689,7 +689,7 @@ mutual else match (← getExprMVarAssignment? mvarId) with | some v => check v | none => - match (← findMVarDecl? mvarId) with + match (← mvarId.findDecl?) with | none => throwUnknownMVar mvarId | some mvarDecl => if ctx.hasCtxLocals then @@ -733,7 +733,7 @@ mutual let localInsts := mvarDecl.localInstances.filter fun localInst => toErase.contains localInst.fvar.fvarId! let mvarType ← check mvarDecl.type let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs - assignExprMVar mvarId newMVar + mvarId.assign newMVar pure newMVar else traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId) @@ -771,7 +771,7 @@ mutual (fun ex => do if !f.isMVar then throw ex - else if (← isMVarDelayedAssigned f.mvarId!) then + else if (← f.mvarId!.isDelayedAssigned) then throw ex else let eType ← inferType e @@ -878,7 +878,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O if !v.hasExprMVar && !v.hasFVar then pure (some v) else - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let hasCtxLocals := fvars.any fun fvar => mvarDecl.lctx.containsFVar fvar let ctx ← read let mctx ← getMCtx @@ -949,7 +949,7 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do /-- Assign `mvar := fun a_1 ... a_{numArgs} => v`. We use it at `processConstApprox` and `isDefEqMVarSelf` -/ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do - let mvarDecl ← getMVarDecl mvar.mvarId! + let mvarDecl ← mvar.mvarId!.getDecl forallBoundedTelescope mvarDecl.type numArgs fun xs _ => do if xs.size != numArgs then pure false @@ -981,7 +981,7 @@ private partial def processConstApprox (mvar : Expr) (args : Array Expr) (patter let rec defaultCase : MetaM Bool := assignConst mvar args.size v let cfg ← getConfig let mvarId := mvar.mvarId! - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl let numArgs := args.size if mvarDecl.numScopeArgs != numArgs && !cfg.constApprox then return false @@ -1022,7 +1022,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool : traceCtx `Meta.isDefEq.assign do trace[Meta.isDefEq.assign] "{mvarApp} := {v}" let mvar := mvarApp.getAppFn - let mvarDecl ← getMVarDecl mvar.mvarId! + let mvarDecl ← mvar.mvarId!.getDecl let rec process (i : Nat) (args : Array Expr) (v : Expr) := do let cfg ← getConfig let useFOApprox (args : Array Expr) : MetaM Bool := @@ -1302,7 +1302,7 @@ private def isDefEqDelta (t s : Expr) : MetaM LBool := do unfoldNonProjFnDefEq tInfo sInfo t s private def isAssigned : Expr → MetaM Bool - | Expr.mvar mvarId => isExprMVarAssigned mvarId + | Expr.mvar mvarId => mvarId.isAssigned | _ => pure false private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do @@ -1335,7 +1335,7 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs) private def isAssignable : Expr → MetaM Bool - | Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b) + | Expr.mvar mvarId => do let b ← mvarId.isReadOnlyOrSyntheticOpaque; pure (!b) | _ => pure false private def etaEq (t s : Expr) : Bool := @@ -1403,7 +1403,7 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM else let cfg ← getConfig let mvarId := mvar.mvarId! - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl if mvarDecl.numScopeArgs == args₁.size || cfg.constApprox then let type ← inferType (mkAppN mvar args₁) let auxMVar ← mkAuxMVar mvarDecl.lctx mvarDecl.localInstances type diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index c3121483f2..dd9997f40f 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -63,7 +63,7 @@ def forEachExpr (e : Expr) (f : Expr → MetaM Unit) : MetaM Unit := /-- Return true iff `x` is a metavariable with an anonymous user facing name. -/ private def shouldInferBinderName (x : Expr) : MetaM Bool := do match x with - | .mvar mvarId => return (← Meta.getMVarDecl mvarId).userName.isAnonymous + | .mvar mvarId => return (← mvarId.getDecl).userName.isAnonymous | _ => return false /-- @@ -82,7 +82,7 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId) let arg := args[i]! if arg.isMVar && isTarget.contains arg then let mvarId := arg.mvarId! - if (← Meta.getMVarDecl mvarId).userName.isAnonymous then + if (← mvarId.getDecl).userName.isAnonymous then forallBoundedTelescope (← inferType e.getAppFn) (some (i+1)) fun xs _ => do if i < xs.size then let mvarId := arg.mvarId! diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index b8306d2c7a..24df5402bd 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -233,9 +233,9 @@ def mkBelowDecl (ctx : Context) : MetaM Declaration := do partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do if depth = 0 then return false else - withMVarContext m do + m.withContext do let lctx ← getLCtx - let mTy ← getMVarType m + let mTy ← m.getType lctx.anyM fun localDecl => if localDecl.isAuxDecl then return false @@ -243,9 +243,9 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do commitWhen do let (mvars, _, t) ← forallMetaTelescope localDecl.type if ←isDefEq mTy t then - assignExprMVar m (mkAppN localDecl.toExpr mvars) + m.assign (mkAppN localDecl.toExpr mvars) mvars.allM fun v => - isExprMVarAssigned v.mvarId! <||> backwardsChaining v.mvarId! (depth - 1) + v.mvarId!.isAssigned <||> backwardsChaining v.mvarId! (depth - 1) else return false partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do @@ -260,16 +260,16 @@ partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : instantiateMVars main where intros (m : MVarId) : MetaM (MVarId × BrecOnVariables) := do - let (params, m) ← introNP m indVal.numParams - let (motives, m) ← introNP m ctx.motives.size - let (indices, m) ← introNP m indVal.numIndices - let (witness, m) ← intro1P m - let (indHyps, m) ← introNP m ctx.motives.size + let (params, m) ← m.introNP indVal.numParams + let (motives, m) ← m.introNP ctx.motives.size + let (indices, m) ← m.introNP indVal.numIndices + let (witness, m) ← m.intro1P + let (indHyps, m) ← m.introNP ctx.motives.size return (m, ⟨params, motives, indices, witness, indHyps⟩) applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do match (← vars.indHyps.findSomeM? - fun ih => do try pure <| some <| (←apply m $ mkFVar ih) catch _ => pure none) with + fun ih => do try pure <| some <| (← m.apply <| mkFVar ih) catch _ => pure none) with | some goals => pure goals | none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}" @@ -287,30 +287,30 @@ where then levelZero::levelParams else levelParams let recursor := mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives - apply m recursor + m.apply recursor applyCtors (ms : List MVarId) : MetaM $ List MVarId := do let mss ← ms.toArray.mapIdxM fun _ m => do let m ← introNPRec m - (← getMVarType m).withApp fun below args => - withMVarContext m do + (← m.getType).withApp fun below args => + m.withContext do args.back.withApp fun ctor _ => do let ctorName := ctor.constName!.updatePrefix below.constName! let ctor := mkConst ctorName below.constLevels! let ctorInfo ← getConstInfoCtor ctorName let (mvars, _, _) ← forallMetaTelescope ctorInfo.type let ctor := mkAppN ctor mvars - apply m ctor + m.apply ctor return mss.foldr List.append [] introNPRec (m : MVarId) : MetaM MVarId := do - if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else return m + if (← m.getType).isForall then introNPRec (← m.intro1P).2 else return m closeGoal (maxDepth : Nat) (m : MVarId) : MetaM Unit := do - unless (← isExprMVarAssigned m) do + unless (← m.isAssigned) do let m ← introNPRec m unless (← backwardsChaining m maxDepth) do - withMVarContext m do + m.withContext do throwError "couldn't solve by backwards chaining ({``maxBackwardChainingDepth} = {maxDepth}): {MessageData.ofGoal m}" def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index d4336e7648..32fc68229c 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -128,11 +128,11 @@ def getLevel (type : Expr) : MetaM Level := do match typeType with | Expr.sort lvl => return lvl | Expr.mvar mvarId => - if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then + if (← mvarId.isReadOnlyOrSyntheticOpaque) then throwTypeExcepted type else let lvl ← mkFreshLevelMVar - assignExprMVar mvarId (mkSort lvl) + mvarId.assign (mkSort lvl) return lvl | _ => throwTypeExcepted type diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean index 65ea5e2fdb..23a77e096c 100644 --- a/src/Lean/Meta/Injective.lean +++ b/src/Lean/Meta/Injective.lean @@ -84,8 +84,8 @@ private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : M match (← injection mvarId h) with | InjectionResult.solved => unreachable! | InjectionResult.subgoal mvarId .. => - (← splitAnd mvarId).forM fun mvarId => - unless (← assumptionCore mvarId) do + (← mvarId.splitAnd).forM fun mvarId => + unless (← mvarId.assumptionCore) do throwInjectiveTheoremFailure ctorName mvarId private def mkInjectiveTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := @@ -118,10 +118,10 @@ private def mkInjectiveEqTheoremType? (ctorVal : ConstructorVal) : MetaM (Option private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do forallTelescopeReducing targetType fun xs type => do let mvar ← mkFreshExprSyntheticOpaqueMVar type - let [mvarId₁, mvarId₂] ← apply mvar.mvarId! (mkConst ``Eq.propIntro) + let [mvarId₁, mvarId₂] ← mvar.mvarId!.apply (mkConst ``Eq.propIntro) | throwError "unexpected number of subgoals when proving injective theorem for constructor '{ctorName}'" - let (h, mvarId₁) ← intro1 mvarId₁ - let (_, mvarId₂) ← intro1 mvarId₂ + let (h, mvarId₁) ← mvarId₁.intro1 + let (_, mvarId₂) ← mvarId₂.intro1 solveEqOfCtorEq ctorName mvarId₁ h let mvarId₂ ← casesAnd mvarId₂ if let some mvarId₂ ← substEqs mvarId₂ then diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index c507a34813..2cb8bd70c9 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/src/Lean/Meta/Match/Basic.lean @@ -263,7 +263,7 @@ structure Problem where deriving Inhabited def withGoalOf {α} (p : Problem) (x : MetaM α) : MetaM α := - withMVarContext p.mvarId x + p.mvarId.withContext x def Problem.toMessageData (p : Problem) : MetaM MessageData := withGoalOf p do diff --git a/src/Lean/Meta/Match/CaseArraySizes.lean b/src/Lean/Meta/Match/CaseArraySizes.lean index 6ab1e34720..3d9832d7f4 100644 --- a/src/Lean/Meta/Match/CaseArraySizes.lean +++ b/src/Lean/Meta/Match/CaseArraySizes.lean @@ -41,13 +41,13 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP let aEqXsLit ← mkEq a xsLit let aEqLitPrf ← mkAppM ``Array.toArrayLit_eq #[a, mkRawNatLit n, aSizeEqN] withLocalDeclD `hEqALit aEqXsLit fun heq => do - let target ← getMVarType mvarId + let target ← mvarId.getType let newTarget ← mkForallFVars (xs.push heq) target pure (newTarget, args.push aEqLitPrf) let (newTarget, args) ← loop 0 #[] #[] - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag - assignExprMVar mvarId (mkAppN newMVar args) + mvarId.assign (mkAppN newMVar args) pure newMVar.mvarId! /-- @@ -58,12 +58,12 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP n+1) `..., (h_1 : a.size != sizes[0]), ..., (h_n : a.size != sizes[n-1]) |- C a` where `n = sizes.size` -/ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNamePrefix := `x) (hNamePrefix := `h) : MetaM (Array CaseArraySizesSubgoal) := - withMVarContext mvarId do + mvarId.withContext do let a := mkFVar fvarId let aSize ← mkAppM `Array.size #[a] - let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize - let (aSizeFVarId, mvarId) ← intro1 mvarId - let (hEq, mvarId) ← intro1 mvarId + let mvarId ← mvarId.assertExt `aSize (mkConst `Nat) aSize + let (aSizeFVarId, mvarId) ← mvarId.intro1 + let (hEq, mvarId) ← mvarId.intro1 let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix subgoals.mapIdxM fun i subgoal => do let subst := subgoal.subst @@ -71,14 +71,14 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam let hEqSz := (subst.get hEq).fvarId! if h : i.val < sizes.size then let n := sizes.get ⟨i, h⟩ - let mvarId ← clear mvarId subgoal.newHs[0]! - let mvarId ← clear mvarId (subst.get aSizeFVarId).fvarId! - withMVarContext mvarId do + let mvarId ← mvarId.clear subgoal.newHs[0]! + let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId! + mvarId.withContext do let hEqSzSymm ← mkEqSymm (mkFVar hEqSz) let mvarId ← introArrayLit mvarId a n xNamePrefix hEqSzSymm - let (xs, mvarId) ← introN mvarId n - let (hEqLit, mvarId) ← intro1 mvarId - let mvarId ← clear mvarId hEqSz + let (xs, mvarId) ← mvarId.introN n + let (hEqLit, mvarId) ← mvarId.intro1 + let mvarId ← mvarId.clear hEqSz let (subst, mvarId) ← substCore mvarId hEqLit false subst pure { mvarId := mvarId, elems := xs, subst := subst } else diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean index 24e70524dc..7a77bd95aa 100644 --- a/src/Lean/Meta/Match/CaseValues.lean +++ b/src/Lean/Meta/Match/CaseValues.lean @@ -25,10 +25,10 @@ structure CaseValueSubgoal where Remark: `subst` field of the second subgoal is equal to the input `subst`. -/ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Name := `h) (subst : FVarSubst := {}) : MetaM (CaseValueSubgoal × CaseValueSubgoal) := - withMVarContext mvarId do - let tag ← getMVarTag mvarId - checkNotAssigned mvarId `caseValue - let target ← getMVarType mvarId + mvarId.withContext do + let tag ← mvarId.getTag + mvarId.checkNotAssigned `caseValue + let target ← mvarId.getType let xEqValue ← mkEq (mkFVar fvarId) (foldPatValue value) let xNeqValue := mkApp (mkConst `Not) xEqValue let thenTarget := Lean.mkForall hName BinderInfo.default xEqValue target @@ -36,14 +36,14 @@ private def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hNa let thenMVar ← mkFreshExprSyntheticOpaqueMVar thenTarget tag let elseMVar ← mkFreshExprSyntheticOpaqueMVar elseTarget tag let val ← mkAppOptM `dite #[none, xEqValue, none, thenMVar, elseMVar] - assignExprMVar mvarId val - let (elseH, elseMVarId) ← intro1P elseMVar.mvarId! + mvarId.assign val + let (elseH, elseMVarId) ← elseMVar.mvarId!.intro1P let elseSubgoal := { mvarId := elseMVarId, newH := elseH, subst := subst : CaseValueSubgoal } - let (thenH, thenMVarId) ← intro1P thenMVar.mvarId! + let (thenH, thenMVarId) ← thenMVar.mvarId!.intro1P let symm := false let clearH := false let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH - withMVarContext thenMVarId do + thenMVarId.withContext do trace[Meta] "subst domain: {thenSubst.domain.map (·.name)}" let thenH := (thenSubst.get thenH).fvarId! trace[Meta] "searching for decl" @@ -87,7 +87,7 @@ def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNameP appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i) let thenMVarId ← hs.foldlM (fun thenMVarId h => match thenSubgoal.subst.get h with - | Expr.fvar fvarId => tryClear thenMVarId fvarId + | Expr.fvar fvarId => thenMVarId.tryClear fvarId | _ => pure thenMVarId) thenSubgoal.mvarId let subgoals ← if substNewEqs then diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 02bdc4c5d1..8588d8c997 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -76,7 +76,7 @@ def assignGoalOf (p : Problem) (e : Expr) : MetaM Unit := let eType ← inferType e unless (← isDefEq mvarType eType) do throwError "dependent elimination failed, type mismatch when solving alternative with type{indentExpr eType}\nbut expected{indentExpr mvarType}" - assignExprMVar p.mvarId e + p.mvarId.assign e structure State where used : Std.HashSet Nat := {} -- used alternatives @@ -173,7 +173,7 @@ private def processLeaf (p : Problem) : StateRefT State MetaM Unit := do /- TODO: allow users to configure which tactic is used to close leaves. -/ unless (← contradictionCore p.mvarId {}) do trace[Meta.Match.match] "missing alternative" - admit p.mvarId + p.mvarId.admit modify fun s => { s with counterExamples := p.examples :: s.counterExamples } | alt :: _ => -- TODO: check whether we have unassigned metavars in rhs @@ -465,7 +465,7 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do match subgoals? with | none => return #[{ p with vars := xs }] | some subgoals => - subgoals.mapM fun subgoal => withMVarContext subgoal.mvarId do + subgoals.mapM fun subgoal => subgoal.mvarId.withContext do let subst := subgoal.subst let fields := subgoal.fields.toList let newVars := fields ++ xs diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 698d52c8a4..f3d12e9734 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -17,7 +17,7 @@ namespace Lean.Meta Helper method for `proveCondEqThm`. Given a goal of the form `C.rec ... xMajor = rhs`, apply `cases xMajor`. -/ partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do - let target ← getMVarType mvarId + let target ← mvarId.getType if let some (_, lhs, _) ← matchEq? target then if let some fvarId ← findFVar? lhs then return (← cases mvarId fvarId).map fun s => s.mvarId @@ -196,7 +196,7 @@ partial def trySubstVarsAndContradiction (mvarId : MVarId) : MetaM Bool := private def processNextEq : M Bool := do let s ← get - withMVarContext s.mvarId do + s.mvarId.withContext do -- If the goal is contradictory, the hypothesis is redundant. if (← contradiction s.mvarId) then return false @@ -256,11 +256,11 @@ end SimpH private partial def simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr) := withDefault do let numVars ← forallTelescope h fun ys _ => pure (ys.size - numEqs) let mvarId := (← mkFreshExprSyntheticOpaqueMVar h).mvarId! - let (xs, mvarId) ← introN mvarId numVars - let (eqs, mvarId) ← introN mvarId numEqs + let (xs, mvarId) ← mvarId.introN numVars + let (eqs, mvarId) ← mvarId.introN numEqs let (r, s) ← SimpH.go |>.run { mvarId, xs := xs.toList, eqs := eqs.toList } if r then - withMVarContext s.mvarId do + s.mvarId.withContext do let eqs := s.eqsNew.reverse.toArray.map mkFVar let mut r ← mkForallFVars eqs (mkConst ``False) /- We only include variables in `xs` if there is a dependency. -/ @@ -273,7 +273,7 @@ private partial def simpH? (h : Expr) (numEqs : Nat) : MetaM (Option Expr) := wi else return none -private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := withMVarContext mvarId do +private def substSomeVar (mvarId : MVarId) : MetaM (Array MVarId) := mvarId.withContext do for localDecl in (← getLCtx) do if let some (_, lhs, rhs) ← matchEq? localDecl.type then if lhs.isFVar then @@ -291,13 +291,13 @@ partial def proveCondEqThm (matchDeclName : Name) (type : Expr) : MetaM Expr := forallTelescope type fun ys target => do let mvar0 ← mkFreshExprSyntheticOpaqueMVar target trace[Meta.Match.matchEqs] "proveCondEqThm {mvar0.mvarId!}" - let mvarId ← deltaTarget mvar0.mvarId! (· == matchDeclName) + let mvarId ← mvar0.mvarId!.deltaTarget (· == matchDeclName) withDefault <| go mvarId 0 mkLambdaFVars ys (← instantiateMVars mvar0) where go (mvarId : MVarId) (depth : Nat) : MetaM Unit := withIncRecDepth do trace[Meta.Match.matchEqs] "proveCondEqThm.go {mvarId}" - let mvarId' ← modifyTargetEqLHS mvarId whnfCore + let mvarId' ← mvarId.modifyTargetEqLHS whnfCore let mvarId := mvarId' let subgoals ← (do applyRefl mvarId; return #[]) @@ -347,7 +347,7 @@ private def injectionAnyCandidate? (type : Expr) : MetaM (Option (Expr × Expr)) return none private def injectionAny (mvarId : MVarId) : MetaM InjectionAnyResult := - withMVarContext mvarId do + mvarId.withContext do for localDecl in (← getLCtx) do if let some (lhs, rhs) ← injectionAnyCandidate? localDecl.type then unless (← isDefEq lhs rhs) do @@ -580,9 +580,9 @@ where | InjectionAnyResult.subgoal mvarId => proveSubgoalLoop mvarId proveSubgoal (mvarId : MVarId) : MetaM Unit := do - trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← getMVarDecl mvarId).kind}, {← isExprMVarAssigned mvarId}\n{MessageData.ofGoal mvarId}" - let (_, mvarId) ← intros mvarId - let mvarId ← tryClearMany mvarId (alts.map (·.fvarId!)) + trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← mvarId.getDecl).kind}, {← mvarId.isAssigned}\n{MessageData.ofGoal mvarId}" + let (_, mvarId) ← mvarId.intros + let mvarId ← mvarId.tryClearMany (alts.map (·.fvarId!)) proveSubgoalLoop mvarId /-- diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 0424e9748a..cac95fde45 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -127,7 +127,7 @@ partial def normExpr (e : Expr) : M Expr := do | Expr.mdata _ b => return e.updateMData! (← normExpr b) | Expr.proj _ _ b => return e.updateProj! (← normExpr b) | Expr.mvar mvarId => - if !(← isExprMVarAssignable mvarId) then + if !(← mvarId.isAssignable) then return e else let s ← get @@ -749,8 +749,8 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex (fun _ => throwError "failed to synthesize{indentExpr type}") @[export lean_synth_pending] -private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| withMVarContext mvarId do - let mvarDecl ← getMVarDecl mvarId +private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do + let mvarDecl ← mvarId.getDecl match mvarDecl.kind with | MetavarKind.syntheticOpaque => return false @@ -773,10 +773,10 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| | none => return false | some val => - if (← isExprMVarAssigned mvarId) then + if (← mvarId.isAssigned) then return false else - assignExprMVar mvarId val + mvarId.assign val return true builtin_initialize diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index 447a7ecab5..1cf47cea12 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -144,7 +144,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do congrTheorems := (← getSimpCongrTheorems) config := Simp.neutralConfig } - let tgt ← getMVarType mvarId + let tgt ← mvarId.getType let res ← Simp.main tgt simpCtx (methods := { post }) let newGoal ← applySimpResultToTarget mvarId tgt res applyRefl newGoal diff --git a/src/Lean/Meta/Tactic/Acyclic.lean b/src/Lean/Meta/Tactic/Acyclic.lean index 57145ea564..b3ea587042 100644 --- a/src/Lean/Meta/Tactic/Acyclic.lean +++ b/src/Lean/Meta/Tactic/Acyclic.lean @@ -18,7 +18,7 @@ private def isTarget (lhs rhs : Expr) : MetaM Bool := do Close the given goal if `h` is a proof for an equality such as `as = a :: as`. Inductive datatypes in Lean are acyclic. -/ -def acyclic (mvarId : MVarId) (h : Expr) : MetaM Bool := withMVarContext mvarId do +def acyclic (mvarId : MVarId) (h : Expr) : MetaM Bool := mvarId.withContext do let type ← whnfD (← inferType h) trace[Meta.Tactic.acyclic] "type: {type}" let some (_, lhs, rhs) := type.eq? | return false @@ -42,7 +42,7 @@ where let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h) let hlt_self ← mkAppM ``Nat.lt_of_lt_of_eq #[hlt, heq] let hlt_irrelf ← mkAppM ``Nat.lt_irrefl #[sizeOf_lhs] - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkApp hlt_irrelf hlt_self)) + mvarId.assign (← mkFalseElim (← mvarId.getType) (mkApp hlt_irrelf hlt_self)) trace[Meta.Tactic.acyclic] "succeeded" return true catch ex => diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index 32d8dc69fd..96560c788d 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -35,18 +35,18 @@ def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Ex throwTacticEx tacticName mvarId "failed to assign synthesized instance" def appendParentTag (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do - let parentTag ← getMVarTag mvarId + let parentTag ← mvarId.getTag if newMVars.size == 1 then -- if there is only one subgoal, we inherit the parent tag - setMVarTag newMVars[0]!.mvarId! parentTag + newMVars[0]!.mvarId!.setTag parentTag else unless parentTag.isAnonymous do newMVars.size.forM fun i => do - let newMVarId := newMVars[i]!.mvarId! - unless (← isExprMVarAssigned newMVarId) do + let mvarIdNew := newMVars[i]!.mvarId! + unless (← mvarIdNew.isAssigned) do unless binderInfos[i]!.isInstImplicit do - let currTag ← getMVarTag newMVarId - setMVarTag newMVarId (appendTag parentTag currTag) + let currTag ← mvarIdNew.getTag + mvarIdNew.setTag (appendTag parentTag currTag) def postprocessAppMVars (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) : MetaM Unit := do synthAppInstances tacticName mvarId newMVars binderInfos @@ -92,10 +92,13 @@ private def reorderGoals (mvars : Array Expr) : ApplyNewGoals → MetaM (List MV structure ApplyConfig where newGoals := ApplyNewGoals.nonDependentFirst -def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := - withMVarContext mvarId do - checkNotAssigned mvarId `apply - let targetType ← getMVarType mvarId +/-- +Close the give goal using `apply e`. +-/ +def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := + mvarId.withContext do + mvarId.checkNotAssigned `apply + let targetType ← mvarId.getType let eType ← inferType e let mut (numArgs, hasMVarHead) ← getExpectedNumArgsAux eType unless hasMVarHead do @@ -105,23 +108,27 @@ def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List M unless (← isDefEq eType targetType) do throwApplyError mvarId eType targetType postprocessAppMVars `apply mvarId newMVars binderInfos let e ← instantiateMVars e - assignExprMVar mvarId (mkAppN e newMVars) - let newMVars ← newMVars.filterM fun mvar => not <$> isExprMVarAssigned mvar.mvarId! + mvarId.assign (mkAppN e newMVars) + let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned let otherMVarIds ← getMVarsNoDelayed e let newMVarIds ← reorderGoals newMVars cfg.newGoals let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId let result := newMVarIds ++ otherMVarIds.toList - result.forM headBetaMVarType + result.forM (·.headBetaType) return result -partial def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := - withMVarContext mvarId do - checkNotAssigned mvarId `splitAnd - let type ← getMVarType' mvarId +@[deprecated MVarId.apply] +def apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := + mvarId.apply e cfg + +partial def splitAndCore (mvarId : MVarId) : MetaM (List MVarId) := + mvarId.withContext do + mvarId.checkNotAssigned `splitAnd + let type ← mvarId.getType' if !type.isAppOfArity ``And 2 then return [mvarId] else - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag let rec go (type : Expr) : StateRefT (Array MVarId) MetaM Expr := do let type ← whnf type if type.isAppOfArity ``And 2 then @@ -134,21 +141,31 @@ partial def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := modify fun s => s.push mvar.mvarId! return mvar let (val, s) ← go type |>.run #[] - assignExprMVar mvarId val + mvarId.assign val return s.toList +/-- +Apply `And.intro` as much as possible to goal `mvarId`. +-/ +abbrev _root_.Lean.MVarId.splitAnd (mvarId : MVarId) : MetaM (List MVarId) := + splitAndCore mvarId + +@[deprecated MVarId.splitAnd] +def splitAnd (mvarId : MVarId) : MetaM (List MVarId) := + mvarId.splitAnd + def applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Unit := - withMVarContext mvarId do - let some [] ← observing? do apply mvarId (mkConst ``Eq.refl [← mkFreshLevelMVar]) + mvarId.withContext do + let some [] ← observing? do mvarId.apply (mkConst ``Eq.refl [← mkFreshLevelMVar]) | throwTacticEx `refl mvarId msg def exfalso (mvarId : MVarId) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `exfalso - let target ← instantiateMVars (← getMVarType mvarId) + mvarId.withContext do + mvarId.checkNotAssigned `exfalso + let target ← instantiateMVars (← mvarId.getType) let u ← getLevel target - let mvarIdNew ← mkFreshExprSyntheticOpaqueMVar (mkConst ``False) (tag := (← getMVarTag mvarId)) - assignExprMVar mvarId (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew) + let mvarIdNew ← mkFreshExprSyntheticOpaqueMVar (mkConst ``False) (tag := (← mvarId.getTag)) + mvarId.assign (mkApp2 (mkConst ``False.elim [u]) target mvarIdNew) return mvarIdNew.mvarId! end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean index 9ad05eef4a..a60746c2eb 100644 --- a/src/Lean/Meta/Tactic/Assert.lean +++ b/src/Lean/Meta/Tactic/Assert.lean @@ -13,44 +13,56 @@ namespace Lean.Meta /-- Convert the given goal `Ctx |- target` into `Ctx |- type -> target`. It assumes `val` has type `type` -/ -def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `assert - let tag ← getMVarTag mvarId - let target ← getMVarType mvarId +def _root_.Lean.MVarId.assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `assert + let tag ← mvarId.getTag + let target ← mvarId.getType let newType := Lean.mkForall name BinderInfo.default type target let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag - assignExprMVar mvarId (mkApp newMVar val) - pure newMVar.mvarId! + mvarId.assign (mkApp newMVar val) + return newMVar.mvarId! + +@[deprecated MVarId.assert] +def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := + mvarId.assert name type val /-- Convert the given goal `Ctx |- target` into `Ctx |- let name : type := val; target`. It assumes `val` has type `type` -/ -def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do - withMVarContext mvarId do - checkNotAssigned mvarId `define - let tag ← getMVarTag mvarId - let target ← getMVarType mvarId +def _root_.Lean.MVarId.define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `define + let tag ← mvarId.getTag + let target ← mvarId.getType let newType := Lean.mkLet name type val target let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag - assignExprMVar mvarId newMVar - pure newMVar.mvarId! + mvarId.assign newMVar + return newMVar.mvarId! + +@[deprecated MVarId.define] +def define (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId := do + mvarId.define name type val /-- Convert the given goal `Ctx |- target` into `Ctx |- (hName : type) -> hName = val -> target`. It assumes `val` has type `type` -/ -def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do - withMVarContext mvarId do - checkNotAssigned mvarId `assert - let tag ← getMVarTag mvarId - let target ← getMVarType mvarId +def _root_.Lean.MVarId.assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `assert + let tag ← mvarId.getTag + let target ← mvarId.getType let u ← getLevel type let hType := mkApp3 (mkConst `Eq [u]) type (mkBVar 0) val let newType := Lean.mkForall name BinderInfo.default type $ Lean.mkForall hName BinderInfo.default hType target let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag let rflPrf ← mkEqRefl val - assignExprMVar mvarId (mkApp2 newMVar val rflPrf) - pure newMVar.mvarId! + mvarId.assign (mkApp2 newMVar val rflPrf) + return newMVar.mvarId! + +@[deprecated MVarId.assertExt] +def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do + mvarId.assertExt name type val hName structure AssertAfterResult where fvarId : FVarId @@ -61,11 +73,11 @@ structure AssertAfterResult where Convert the given goal `Ctx |- target` into a goal containing `(userName : type)` after the local declaration with if `fvarId`. It assumes `val` has type `type`, and that `type` is well-formed after `fvarId`. Note that `val` does not need to be well-formed after `fvarId`. That is, it may contain variables that are defined after `fvarId`. -/ -def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do - withMVarContext mvarId do - checkNotAssigned mvarId `assertAfter - let tag ← getMVarTag mvarId - let target ← getMVarType mvarId +def _root_.Lean.MVarId.assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do + mvarId.withContext do + mvarId.checkNotAssigned `assertAfter + let tag ← mvarId.getTag + let target ← mvarId.getType let localDecl ← getLocalDecl fvarId let lctx ← getLCtx let localInsts ← getLocalInstances @@ -78,11 +90,15 @@ def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Ex let mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar let args := #[val] ++ args - assignExprMVar mvarId (mkAppN mvarNew args) - let (fvarIdNew, mvarIdNew) ← intro1P mvarNew.mvarId! - let (fvarIdsNew, mvarIdNew) ← introNP mvarIdNew fvarIds.size + mvarId.assign (mkAppN mvarNew args) + let (fvarIdNew, mvarIdNew) ← mvarNew.mvarId!.intro1P + let (fvarIdsNew, mvarIdNew) ← mvarIdNew.introNP fvarIds.size let subst := fvarIds.size.fold (init := {}) fun i subst => subst.insert fvarIds[i]! (mkFVar fvarIdsNew[i]!) - pure { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst } + return { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst } + +@[deprecated MVarId.assertAfter] +def assertAfter (mvarId : MVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (val : Expr) : MetaM AssertAfterResult := do + mvarId.assertAfter fvarId userName type val structure Hypothesis where userName : Name @@ -92,18 +108,22 @@ structure Hypothesis where /-- Convert the given goal `Ctx |- target` into `Ctx, (hs[0].userName : hs[0].type) ... |-target`. It assumes `hs[i].val` has type `hs[i].type`. -/ -def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do +def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do if hs.isEmpty then return (#[], mvarId) - else withMVarContext mvarId do - checkNotAssigned mvarId `assertHypotheses - let tag ← getMVarTag mvarId - let target ← getMVarType mvarId + else mvarId.withContext do + mvarId.checkNotAssigned `assertHypotheses + let tag ← mvarId.getTag + let target ← mvarId.getType let targetNew := hs.foldr (init := target) fun h targetNew => mkForall h.userName BinderInfo.default h.type targetNew let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag let val := hs.foldl (init := mvarNew) fun val h => mkApp val h.value - assignExprMVar mvarId val - introNP mvarNew.mvarId! hs.size + mvarId.assign val + mvarNew.mvarId!.introNP hs.size + +@[deprecated MVarId.assertHypotheses] +def assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis) : MetaM (Array FVarId × MVarId) := do + mvarId.assertHypotheses hs end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Assumption.lean b/src/Lean/Meta/Tactic/Assumption.lean index 746f2762d2..27ccfa3e0b 100644 --- a/src/Lean/Meta/Tactic/Assumption.lean +++ b/src/Lean/Meta/Tactic/Assumption.lean @@ -17,15 +17,25 @@ def findLocalDeclWithType? (type : Expr) : MetaM (Option FVarId) := do else return none -def assumptionCore (mvarId : MVarId) : MetaM Bool := - withMVarContext mvarId do - checkNotAssigned mvarId `assumption - match (← findLocalDeclWithType? (← getMVarType mvarId)) with +/-- Return `true` if managed to close goal `mvarId` using an assumption. -/ +def _root_.Lean.MVarId.assumptionCore (mvarId : MVarId) : MetaM Bool := + mvarId.withContext do + mvarId.checkNotAssigned `assumption + match (← findLocalDeclWithType? (← mvarId.getType)) with | none => return false - | some fvarId => assignExprMVar mvarId (mkFVar fvarId); return true + | some fvarId => mvarId.assign (mkFVar fvarId); return true -def assumption (mvarId : MVarId) : MetaM Unit := - unless (← assumptionCore mvarId) do +@[deprecated MVarId.assumptionCore] +def assumptionCore (mvarId : MVarId) : MetaM Bool := + mvarId.assumptionCore + +/-- Close goal `mvarId` using an assumption. Throw error message if failed. -/ +def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit := + unless (← mvarId.assumptionCore) do throwTacticEx `assumption mvarId "" +@[deprecated MVarId.assumption] +def assumption (mvarId : MVarId) : MetaM Unit := + mvarId.assumption + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index d87d57864a..f99e66c669 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -43,19 +43,19 @@ private partial def withNewEqs (targets targetsNew : Array Expr) (k : Array Expr loop 0 #[] #[] def generalizeTargetsEq (mvarId : MVarId) (motiveType : Expr) (targets : Array Expr) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `generalizeTargets + mvarId.withContext do + mvarId.checkNotAssigned `generalizeTargets let (typeNew, eqRefls) ← forallTelescopeReducing motiveType fun targetsNew _ => do unless targetsNew.size == targets.size do throwError "invalid number of targets #{targets.size}, motive expects #{targetsNew.size}" withNewEqs targets targetsNew fun eqs eqRefls => do - let type ← getMVarType mvarId + let type ← mvarId.getType let typeNew ← mkForallFVars eqs type let typeNew ← mkForallFVars targetsNew typeNew pure (typeNew, eqRefls) - let mvarNew ← mkFreshExprSyntheticOpaqueMVar typeNew (← getMVarTag mvarId) - assignExprMVar mvarId (mkAppN (mkAppN mvarNew targets) eqRefls) + let mvarNew ← mkFreshExprSyntheticOpaqueMVar typeNew (← mvarId.getTag) + mvarId.assign (mkAppN (mkAppN mvarNew targets) eqRefls) pure mvarNew.mvarId! structure GeneralizeIndicesSubgoal where @@ -83,10 +83,10 @@ structure GeneralizeIndicesSubgoal where - `fvarId`: `h'` id - `numEqs`: number of equations in the target -/ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndicesSubgoal := - withMVarContext mvarId do + mvarId.withContext do let lctx ← getLCtx let localInsts ← getLocalInstances - checkNotAssigned mvarId `generalizeIndices + mvarId.checkNotAssigned `generalizeIndices let fvarDecl ← getLocalDecl fvarId let type ← whnf fvarDecl.type type.withApp fun f args => matchConstInduct f (fun _ => throwTacticEx `generalizeIndices mvarId "inductive type expected") fun val _ => do @@ -104,17 +104,17 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi withLocalDeclD `h newEqType fun newEq => do let newEqs := newEqs.push newEq /- auxType `forall (j' : J) (h' : I A j'), j == j' -> h == h' -> target -/ - let target ← getMVarType mvarId - let tag ← getMVarTag mvarId + let target ← mvarId.getType + let tag ← mvarId.getTag let auxType ← mkForallFVars newEqs target let auxType ← mkForallFVars #[h'] auxType let auxType ← mkForallFVars newIndices auxType let newMVar ← mkFreshExprMVarAt lctx localInsts auxType MetavarKind.syntheticOpaque tag /- assign mvarId := newMVar indices h refls -/ - assignExprMVar mvarId (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls) - let (indicesFVarIds, newMVarId) ← introNP newMVar.mvarId! newIndices.size - let (fvarId, newMVarId) ← intro1P newMVarId - pure { + mvarId.assign (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls) + let (indicesFVarIds, newMVarId) ← newMVar.mvarId!.introNP newIndices.size + let (fvarId, newMVarId) ← newMVarId.intro1P + return { mvarId := newMVarId, indicesFVarIds := indicesFVarIds, fvarId := fvarId, @@ -182,7 +182,7 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases indicesFVarIds.foldlM (init := s) fun s indexFVarId => match s.subst.get indexFVarId with | Expr.fvar indexFVarId' => - (do let mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId }) + (do let mvarId ← s.mvarId.clear indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId }) <|> (pure s) | _ => pure s @@ -203,7 +203,7 @@ partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (case if numEqs == 0 then return some (mvarId, subst) else - let (eqFVarId, mvarId) ← intro1 mvarId + let (eqFVarId, mvarId) ← mvarId.intro1 if let some { mvarId, subst, numNewEqs } ← unifyEq? mvarId eqFVarId subst acyclic caseName? then unifyEqs? (numEqs - 1 + numNewEqs) mvarId subst caseName? else @@ -221,19 +221,18 @@ private def unifyCasesEqs (numEqs : Nat) (subgoals : Array CasesSubgoal) : MetaM } private def inductionCasesOn (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames) (ctx : Context) - : MetaM (Array CasesSubgoal) := do - withMVarContext mvarId do + : MetaM (Array CasesSubgoal) := mvarId.withContext do let majorType ← inferType (mkFVar majorFVarId) let (us, params) ← getInductiveUniverseAndParams majorType let casesOn := mkCasesOnName ctx.inductiveVal.name let ctors := ctx.inductiveVal.ctors.toArray - let s ← induction mvarId majorFVarId casesOn givenNames + let s ← mvarId.induction majorFVarId casesOn givenNames return toCasesSubgoals s ctors majorFVarId us params def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) := do try - withMVarContext mvarId do - checkNotAssigned mvarId `cases + mvarId.withContext do + mvarId.checkNotAssigned `cases let context? ← mkCasesContext? majorFVarId match context? with | none => throwTacticEx `cases mvarId "not applicable to the given hypothesis" @@ -260,7 +259,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNam def casesRec (mvarId : MVarId) (p : LocalDecl → MetaM Bool) : MetaM (List MVarId) := saturate mvarId fun mvarId => - withMVarContext mvarId do + mvarId.withContext do for localDecl in (← getLCtx) do if (← p localDecl) then let r? ← observing? do @@ -285,8 +284,8 @@ structure ByCasesSubgoal where fvarId : FVarId def byCases (mvarId : MVarId) (p : Expr) (hName : Name := `h) : MetaM (ByCasesSubgoal × ByCasesSubgoal) := do - let mvarId ← assert mvarId `hByCases (mkOr p (mkNot p)) (mkEM p) - let (fvarId, mvarId) ← intro1 mvarId + let mvarId ← mvarId.assert `hByCases (mkOr p (mkNot p)) (mkEM p) + let (fvarId, mvarId) ← mvarId.intro1 let #[s₁, s₂] ← cases mvarId fvarId #[{ varNames := [hName] }, { varNames := [hName] }] | throwError "'byCases' tactic failed, unexpected number of subgoals" return ((← toByCasesSubgoal s₁), (← toByCasesSubgoal s₂)) diff --git a/src/Lean/Meta/Tactic/Cleanup.lean b/src/Lean/Meta/Tactic/Cleanup.lean index 4c7dc621ed..506d0bf160 100644 --- a/src/Lean/Meta/Tactic/Cleanup.lean +++ b/src/Lean/Meta/Tactic/Cleanup.lean @@ -8,24 +8,17 @@ import Lean.Meta.Tactic.Clear namespace Lean.Meta -/-- - Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are *not* relevant. - We say a variable `x` is "relevant" if - - It occurs in the target type, or - - There is a relevant variable `y` that depends on `x`, or - - The type of `x` is a proposition and it depends on a relevant variable `y`. --/ -partial def cleanup (mvarId : MVarId) : MetaM MVarId := do - withMVarContext mvarId do - checkNotAssigned mvarId `cleanup +private partial def cleanupCore (mvarId : MVarId) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `cleanup let used ← collectUsed |>.run' (false, {}) let mut lctx ← getLCtx for localDecl in lctx do unless used.contains localDecl.fvarId do lctx := lctx.erase localDecl.fvarId let localInsts := (← getLocalInstances).filter fun inst => used.contains inst.fvar.fvarId! - let mvarNew ← mkFreshExprMVarAt lctx localInsts (← instantiateMVars (← getMVarType mvarId)) MetavarKind.syntheticOpaque (← getMVarTag mvarId) - assignExprMVar mvarId mvarNew + let mvarNew ← mkFreshExprMVarAt lctx localInsts (← instantiateMVars (← mvarId.getType)) .syntheticOpaque (← mvarId.getTag) + mvarId.assign mvarNew return mvarNew.mvarId! where addUsedFVars (e : Expr) : StateRefT (Bool × FVarIdSet) MetaM Unit := do @@ -59,8 +52,22 @@ where collectProps collectUsed : StateRefT (Bool × FVarIdSet) MetaM FVarIdSet := do - addUsedFVars (← instantiateMVars (← getMVarType mvarId)) + addUsedFVars (← instantiateMVars (← mvarId.getType)) collectProps return (← get).2 +/-- + Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are *not* relevant. + We say a variable `x` is "relevant" if + - It occurs in the target type, or + - There is a relevant variable `y` that depends on `x`, or + - The type of `x` is a proposition and it depends on a relevant variable `y`. +-/ +abbrev _root_.Lean.MVarId.cleanup (mvarId : MVarId) : MetaM MVarId := do + cleanupCore mvarId + +@[deprecated MVarId.cleanup] +abbrev cleanup (mvarId : MVarId) : MetaM MVarId := do + mvarId.cleanup + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Clear.lean b/src/Lean/Meta/Tactic/Clear.lean index 6ef0ae3931..c996fe8839 100644 --- a/src/Lean/Meta/Tactic/Clear.lean +++ b/src/Lean/Meta/Tactic/Clear.lean @@ -7,18 +7,21 @@ import Lean.Meta.Tactic.Util namespace Lean.Meta -def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `clear +/-- +Erase the given free variable from the goal `mvarId`. +-/ +def _root_.Lean.MVarId.clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `clear let lctx ← getLCtx unless lctx.contains fvarId do throwTacticEx `clear mvarId m!"unknown variable '{mkFVar fvarId}'" - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag lctx.forM fun localDecl => do unless localDecl.fvarId == fvarId do if (← localDeclDependsOn localDecl fvarId) then throwTacticEx `clear mvarId m!"variable '{localDecl.toExpr}' depends on '{mkFVar fvarId}'" - let mvarDecl ← getMVarDecl mvarId + let mvarDecl ← mvarId.getDecl if (← exprDependsOn mvarDecl.type fvarId) then throwTacticEx `clear mvarId m!"target depends on '{mkFVar fvarId}'" let lctx := lctx.erase fvarId @@ -27,13 +30,33 @@ def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := | none => localInsts | some idx => localInsts.eraseIdx idx let newMVar ← mkFreshExprMVarAt lctx localInsts mvarDecl.type MetavarKind.syntheticOpaque tag - assignExprMVar mvarId newMVar + mvarId.assign newMVar pure newMVar.mvarId! -def tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := - clear mvarId fvarId <|> pure mvarId +@[deprecated MVarId.clear] +def clear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := + mvarId.clear fvarId + +/-- +Try to erase the given free variable from the goal `mvarId`. It is no-op if the free variable +cannot be erased due to forward dependencies. +-/ +def _root_.Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := + mvarId.clear fvarId <|> pure mvarId + +@[deprecated MVarId.tryClear] +def tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := + mvarId.tryClear fvarId + +/-- +Try to erase the given free variables from the goal `mvarId`. +-/ +def _root_.Lean.MVarId.tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do + fvarIds.foldrM (init := mvarId) fun fvarId mvarId => mvarId.tryClear fvarId + +@[deprecated MVarId.tryClearMany] def tryClearMany (mvarId : MVarId) (fvarIds : Array FVarId) : MetaM MVarId := do - fvarIds.foldrM (init := mvarId) fun fvarId mvarId => tryClear mvarId fvarId + mvarId.tryClearMany fvarIds end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Constructor.lean b/src/Lean/Meta/Tactic/Constructor.lean index 93ab123660..ff6ed55692 100644 --- a/src/Lean/Meta/Tactic/Constructor.lean +++ b/src/Lean/Meta/Tactic/Constructor.lean @@ -10,27 +10,31 @@ import Lean.Meta.Tactic.Apply namespace Lean.Meta /-- -When the goal `mvarId` is an inductive datatype, +When the goal `mvarId` type is an inductive datatype, `constructor` calls `apply` with the first matching constructor. -/ -def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do - withMVarContext mvarId do - checkNotAssigned mvarId `constructor - let target ← getMVarType' mvarId +def _root_.Lean.MVarId.constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do + mvarId.withContext do + mvarId.checkNotAssigned `constructor + let target ← mvarId.getType' matchConstInduct target.getAppFn (fun _ => throwTacticEx `constructor mvarId "target is not an inductive datatype") fun ival us => do for ctor in ival.ctors do try - return ← apply mvarId (Lean.mkConst ctor us) cfg + return ← mvarId.apply (Lean.mkConst ctor us) cfg catch _ => pure () throwTacticEx `constructor mvarId "no applicable constructor found" -def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do - withMVarContext mvarId do - checkNotAssigned mvarId `exists - let target ← getMVarType' mvarId +@[deprecated MVarId.constructor] +def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do + mvarId.constructor cfg + +def _root_.Lean.MVarId.existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `exists + let target ← mvarId.getType' matchConstStruct target.getAppFn (fun _ => throwTacticEx `exists mvarId "target is not an inductive datatype with one constructor") fun _ us cval => do @@ -41,8 +45,12 @@ def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.numFields-2)) let f := mkAppN ctor mvars checkApp f w - let [mvarId] ← apply mvarId <| mkApp f w + let [mvarId] ← mvarId.apply <| mkApp f w | throwTacticEx `exists mvarId "unexpected number of subgoals" pure mvarId +@[deprecated MVarId.existsIntro] +def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do + mvarId.existsIntro w + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean index ab3b1ca54d..bdf79fb332 100644 --- a/src/Lean/Meta/Tactic/Contradiction.lean +++ b/src/Lean/Meta/Tactic/Contradiction.lean @@ -28,10 +28,10 @@ structure Contradiction.Config where Return `true` iff the goal has been closed. -/ private def nestedFalseElim (mvarId : MVarId) : MetaM Bool := do - let target ← getMVarType mvarId + let target ← mvarId.getType if let some falseElim := target.find? fun e => e.isAppOfArity ``False.elim 2 && !e.appArg!.hasLooseBVars then let falseProof := falseElim.appArg! - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) falseProof) + mvarId.assign (← mkFalseElim (← mvarId.getType) falseProof) return true else return false @@ -62,7 +62,7 @@ partial def elim (mvarId : MVarId) (fvarId : FVarId) : M Bool := do trace[Meta.Tactic.contradiction] "elimEmptyInductive, number subgoals: {subgoals.size}" for subgoal in subgoals do -- If one of the fields is uninhabited, then we are done - let found ← withMVarContext subgoal.mvarId do + let found ← subgoal.mvarId.withContext do for field in subgoal.fields do let field := subgoal.subst.apply field if field.isFVar then @@ -77,7 +77,7 @@ partial def elim (mvarId : MVarId) (fvarId : FVarId) : M Bool := do end ElimEmptyInductive private def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (fuel : Nat) : MetaM Bool := do - withMVarContext mvarId do + mvarId.withContext do if (← isElimEmptyInductiveCandidate fvarId) then commitWhen do ElimEmptyInductive.elim (← exfalso mvarId) fvarId |>.run' fuel @@ -139,16 +139,16 @@ private def processGenDiseq (mvarId : MVarId) (localDecl : LocalDecl) : MetaM Bo let falseProof ← instantiateMVars (mkAppN localDecl.toExpr args) if (← hasAssignableMVar falseProof) then return none - return some (← mkFalseElim (← getMVarType mvarId) falseProof) + return some (← mkFalseElim (← mvarId.getType) falseProof) if let some val := val? then - assignExprMVar mvarId val + mvarId.assign val return true else return false def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM Bool := do - withMVarContext mvarId do - checkNotAssigned mvarId `contradiction + mvarId.withContext do + mvarId.checkNotAssigned `contradiction if (← nestedFalseElim mvarId) then return true for localDecl in (← getLCtx) do @@ -156,12 +156,12 @@ def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM -- (h : ¬ p) (h' : p) if let some p ← matchNot? localDecl.type then if let some pFVarId ← findLocalDeclWithType? p then - assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) (mkFVar pFVarId) localDecl.toExpr) + mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr) return true -- (h : x ≠ x) if let some (_, lhs, rhs) ← matchNe? localDecl.type then if (← isDefEq lhs rhs) then - assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) (← mkEqRefl lhs) localDecl.toExpr) + mvarId.assign (← mkAbsurd (← mvarId.getType) (← mkEqRefl lhs) localDecl.toExpr) return true let mut isEq := false -- (h : ctor₁ ... = ctor₂ ...) @@ -170,7 +170,7 @@ def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM if let some lhsCtor ← matchConstructorApp? lhs then if let some rhsCtor ← matchConstructorApp? rhs then if lhsCtor.name != rhsCtor.name then - assignExprMVar mvarId (← mkNoConfusion (← getMVarType mvarId) localDecl.toExpr) + mvarId.assign (← mkNoConfusion (← mvarId.getType) localDecl.toExpr) return true let mut isHEq := false -- (h : HEq (ctor₁ ...) (ctor₂ ...)) @@ -180,7 +180,7 @@ def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM if let some rhsCtor ← matchConstructorApp? rhs then if lhsCtor.name != rhsCtor.name then if (← isDefEq α β) then - assignExprMVar mvarId (← mkNoConfusion (← getMVarType mvarId) (← mkEqOfHEq localDecl.toExpr)) + mvarId.assign (← mkNoConfusion (← mvarId.getType) (← mkEqOfHEq localDecl.toExpr)) return true -- (h : p) s.t. `decide p` evaluates to `false` if config.useDecide && !localDecl.type.hasFVar then @@ -191,7 +191,7 @@ def contradictionCore (mvarId : MVarId) (config : Contradiction.Config) : MetaM let r ← withDefault <| whnf d if r.isConstOf ``false then let hn := mkAppN (mkConst ``of_decide_eq_false) <| d.getAppArgs.push (← mkEqRefl d) - assignExprMVar mvarId (← mkAbsurd (← getMVarType mvarId) localDecl.toExpr hn) + mvarId.assign (← mkAbsurd (← mvarId.getType) localDecl.toExpr hn) return true catch _ => pure () diff --git a/src/Lean/Meta/Tactic/Delta.lean b/src/Lean/Meta/Tactic/Delta.lean index afd7ba8216..b310159cb4 100644 --- a/src/Lean/Meta/Tactic/Delta.lean +++ b/src/Lean/Meta/Tactic/Delta.lean @@ -23,14 +23,28 @@ def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr := | some e' => return TransformStep.visit e' | none => return TransformStep.visit e -def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `delta - change mvarId (← deltaExpand (← getMVarType mvarId) p) (checkDefEq := false) +/-- +Delta expand declarations that satisfy `p` at `mvarId` type. +-/ +def _root_.Lean.MVarId.deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `delta + mvarId.change (← deltaExpand (← mvarId.getType) p) (checkDefEq := false) +@[deprecated MVarId.deltaTarget] +def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId := + mvarId.deltaTarget p + +/-- +Delta expand declarations that satisfy `p` at `fvarId` type. +-/ +def _root_.Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `delta + mvarId.changeLocalDecl fvarId (← deltaExpand (← mvarId.getType) p) (checkDefEq := false) + +@[deprecated MVarId.deltaLocalDecl] def deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `delta - changeLocalDecl mvarId fvarId (← deltaExpand (← getMVarType mvarId) p) (checkDefEq := false) + mvarId.deltaLocalDecl fvarId p end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Generalize.lean b/src/Lean/Meta/Tactic/Generalize.lean index 502cb94e3f..f293f3be63 100644 --- a/src/Lean/Meta/Tactic/Generalize.lean +++ b/src/Lean/Meta/Tactic/Generalize.lean @@ -20,10 +20,10 @@ partial def generalize (mvarId : MVarId) (args : Array GeneralizeArg) -- (pred : (parent? : Option Expr) → (e : Expr) → MetaM Bool := fun _ _ => return true) : MetaM (Array FVarId × MVarId) := - withMVarContext mvarId do - checkNotAssigned mvarId `generalize - let tag ← getMVarTag mvarId - let target ← instantiateMVars (← getMVarType mvarId) + mvarId.withContext do + mvarId.checkNotAssigned `generalize + let tag ← mvarId.getTag + let target ← instantiateMVars (← mvarId.getType) let rec go (i : Nat) : MetaM Expr := do if i < args.size then let arg := args[i]! @@ -40,8 +40,8 @@ partial def generalize let es := args.map (·.expr) if !args.any fun arg => arg.hName?.isSome then let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag - assignExprMVar mvarId (mkAppN mvarNew es) - introNP mvarNew.mvarId! args.size + mvarId.assign (mkAppN mvarNew es) + mvarNew.mvarId!.introNP args.size else let (rfls, targetNew) ← forallBoundedTelescope targetNew args.size fun xs type => do let rec go' (i : Nat) : MetaM (List Expr × Expr) := do @@ -64,7 +64,7 @@ partial def generalize let (rfls, type) ← go' 0 return (rfls, ← mkForallFVars xs type) let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag - assignExprMVar mvarId (mkAppN (mkAppN mvarNew es) rfls.toArray) - introNP mvarNew.mvarId! (args.size + rfls.length) + mvarId.assign (mkAppN (mkAppN mvarNew es) rfls.toArray) + mvarNew.mvarId!.introNP (args.size + rfls.length) end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean index ff31f58cf7..1d911f6ffc 100644 --- a/src/Lean/Meta/Tactic/Induction.lean +++ b/src/Lean/Meta/Tactic/Induction.lean @@ -56,7 +56,7 @@ private partial def finalize (mvarId : MVarId) (givenNames : Array AltVarNames) (recursorInfo : RecursorInfo) (reverted : Array FVarId) (major : Expr) (indices : Array Expr) (baseSubst : FVarSubst) (recursor : Expr) : MetaM (Array InductionSubgoal) := do - let target ← getMVarType mvarId + let target ← mvarId.getType let initialArity := getTargetArity target let recursorType ← inferType recursor let numMinors := recursorInfo.produceMotive.length @@ -73,7 +73,7 @@ private partial def finalize loop (pos+1+indices.size) minorIdx recursor recursorType true subgoals else -- consume motive - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag if minorIdx ≥ numMinors then throwTacticEx `induction mvarId "ill-formed recursor" match recursorType with | Expr.forallE n d _ c => @@ -101,9 +101,9 @@ private partial def finalize let recursor := mkApp recursor mvar let recursorType ← getTypeBody mvarId recursorType mvar -- Try to clear major premise from new goal - let mvarId' ← tryClear mvar.mvarId! major.fvarId! - let (fields, mvarId') ← introN mvarId' nparams minorGivenNames.varNames (useNamesForExplicitOnly := !minorGivenNames.explicit) - let (extra, mvarId') ← introNP mvarId' nextra + let mvarId' ← mvar.mvarId!.tryClear major.fvarId! + let (fields, mvarId') ← mvarId'.introN nparams minorGivenNames.varNames (useNamesForExplicitOnly := !minorGivenNames.explicit) + let (extra, mvarId') ← mvarId'.introNP nextra let subst := reverted.size.fold (init := baseSubst) fun i (subst : FVarSubst) => if i < indices.size + 1 then subst else @@ -115,17 +115,17 @@ private partial def finalize | _ => unreachable! else unless consumedMajor do throwTacticEx `induction mvarId "ill-formed recursor" - assignExprMVar mvarId recursor + mvarId.assign recursor pure subgoals loop (recursorInfo.paramsPos.length + 1) 0 recursor recursorType false #[] private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) : MetaM α := throwTacticEx `induction mvarId m!"unexpected major premise type{indentExpr majorType}" -def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) := - withMVarContext mvarId do +def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) := + mvarId.withContext do trace[Meta.Tactic.induction] "initial\n{MessageData.ofGoal mvarId}" - checkNotAssigned mvarId `induction + mvarId.checkNotAssigned `induction let majorLocalDecl ← getLocalDecl majorFVarId let recursorInfo ← mkRecursorInfo recursorName let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type @@ -152,14 +152,14 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi if (← localDeclDependsOn idxDecl arg.fvarId!) then throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}" pure idx - let target ← getMVarType mvarId + let target ← mvarId.getType if (← pure !recursorInfo.depElim <&&> exprDependsOn target majorFVarId) then throwTacticEx `induction mvarId m!"recursor '{recursorName}' does not support dependent elimination, but conclusion depends on major premise" -- Revert indices and major premise preserving variable order - let (reverted, mvarId) ← revert mvarId ((indices.map Expr.fvarId!).push majorFVarId) true + let (reverted, mvarId) ← mvarId.revert ((indices.map Expr.fvarId!).push majorFVarId) true -- Re-introduce indices and major - let (indices', mvarId) ← introNP mvarId indices.size - let (majorFVarId', mvarId) ← intro1P mvarId + let (indices', mvarId) ← mvarId.introNP indices.size + let (majorFVarId', mvarId) ← mvarId.intro1P -- Create FVarSubst with indices let baseSubst := Id.run do let mut subst : FVarSubst := {} @@ -173,8 +173,8 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi let indices := indices'.map mkFVar let majorFVarId := majorFVarId' let major := mkFVar majorFVarId - withMVarContext mvarId do - let target ← getMVarType mvarId + mvarId.withContext do + let target ← mvarId.getType let targetLevel ← getLevel target let targetLevel ← normalizeLevel targetLevel let majorLocalDecl ← getLocalDecl majorFVarId @@ -206,6 +206,10 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi | _ => throwTacticEx `induction mvarId "major premise is not of the form (C ...)" +@[deprecated MVarId.induction] +def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) := + mvarId.induction majorFVarId recursorName givenNames + builtin_initialize registerTraceClass `Meta.Tactic.induction end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index 2185c1081c..ef026a53b6 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -25,8 +25,8 @@ inductive InjectionResultCore where | subgoal (mvarId : MVarId) (numNewEqs : Nat) def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCore := - withMVarContext mvarId do - checkNotAssigned mvarId `injection + mvarId.withContext do + mvarId.checkNotAssigned `injection let decl ← getLocalDecl fvarId let type ← whnf decl.type let go (type prf : Expr) : MetaM InjectionResultCore := do @@ -35,13 +35,13 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor | some (_, a, b) => let a ← whnf a let b ← whnf b - let target ← getMVarType mvarId + let target ← mvarId.getType let env ← getEnv match a.isConstructorApp? env, b.isConstructorApp? env with | some aCtor, some bCtor => let val ← mkNoConfusion target prf if aCtor.name != bCtor.name then - assignExprMVar mvarId val + mvarId.assign val return InjectionResultCore.solved else let valType ← inferType val @@ -49,10 +49,10 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor match valType with | Expr.forallE _ newTarget _ _ => let newTarget := newTarget.headBeta - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag - assignExprMVar mvarId (mkApp val newMVar) - let mvarId ← tryClear newMVar.mvarId! fvarId + mvarId.assign (mkApp val newMVar) + let mvarId ← newMVar.mvarId!.tryClear fvarId /- Recall that `noConfusion` does not include equalities for propositions since they are trivial due to proof irrelevance. -/ let numPropFields ← getCtorNumPropFields aCtor @@ -78,11 +78,11 @@ def injectionIntro (mvarId : MVarId) (numEqs : Nat) (newNames : List Name) (tryT | 0, mvarId, fvarIds, remainingNames => return InjectionResult.subgoal mvarId fvarIds remainingNames | n+1, mvarId, fvarIds, name::remainingNames => do - let (fvarId, mvarId) ← intro mvarId name + let (fvarId, mvarId) ← mvarId.intro name let (fvarId, mvarId) ← heqToEq mvarId fvarId tryToClear go n mvarId (fvarIds.push fvarId) remainingNames | n+1, mvarId, fvarIds, [] => do - let (fvarId, mvarId) ← intro1 mvarId + let (fvarId, mvarId) ← mvarId.intro1 let (fvarId, mvarId) ← heqToEq mvarId fvarId tryToClear go n mvarId (fvarIds.push fvarId) [] go numEqs mvarId #[] newNames @@ -93,7 +93,7 @@ def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) : | InjectionResultCore.subgoal mvarId numEqs => injectionIntro mvarId numEqs newNames partial def injections (mvarId : MVarId) (maxDepth : Nat := 5) : MetaM (Option MVarId) := - withMVarContext mvarId do + mvarId.withContext do let fvarIds := (← getLCtx).getFVarIds go maxDepth fvarIds.toList mvarId where @@ -112,7 +112,7 @@ where match (← injection mvarId fvarId) with | InjectionResult.solved => return none | InjectionResult.subgoal mvarId newEqs _ => - withMVarContext mvarId <| go d (newEqs.toList ++ fvarIds) mvarId + mvarId.withContext <| go d (newEqs.toList ++ fvarIds) mvarId catch _ => cont else cont diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 43c9e1cd4f..058fd3f392 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -8,9 +8,9 @@ import Lean.Meta.Tactic.Util namespace Lean.Meta @[inline] private partial def introNImp {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → Bool → σ → MetaM (Name × σ)) (s : σ) - : MetaM (Array FVarId × MVarId) := withMVarContext mvarId do - checkNotAssigned mvarId `introN - let mvarType ← getMVarType mvarId + : MetaM (Array FVarId × MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `introN + let mvarType ← mvarId.getType let lctx ← getLCtx let rec @[specialize] loop (i : Nat) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (s : σ) (type : Expr) : MetaM (Array Expr × MVarId) := do match i, type with @@ -18,13 +18,13 @@ namespace Lean.Meta let type := type.instantiateRevRange j fvars.size fvars withReader (fun ctx => { ctx with lctx := lctx }) do withNewLocalInstances fvars j do - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag let type := type.headBeta let newMVar ← mkFreshExprSyntheticOpaqueMVar type tag let newVal ← mkLambdaFVars fvars newMVar - assignExprMVar mvarId newVal + mvarId.assign newVal return (fvars, newMVar.mvarId!) - | i+1, Expr.letE n type val body _ => + | i+1, .letE n type val body _ => let type := type.instantiateRevRange j fvars.size fvars let type := type.headBeta let val := val.instantiateRevRange j fvars.size fvars @@ -34,7 +34,7 @@ namespace Lean.Meta let fvar := mkFVar fvarId let fvars := fvars.push fvar loop i lctx fvars j s body - | i+1, Expr.forallE n type body c => + | i+1, .forallE n type body c => let type := type.instantiateRevRange j fvars.size fvars let type := type.headBeta let fvarId ← mkFreshFVarId @@ -100,39 +100,82 @@ def introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (useNamesFor else introNImp mvarId n (mkAuxNameImp preserveBinderNames hygienic useNamesForExplicitOnly) givenNames -abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) := +/-- +Introduce `n` binders in the goal `mvarId`. +-/ +abbrev _root_.Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) := introNCore mvarId n givenNames (useNamesForExplicitOnly := useNamesForExplicitOnly) (preserveBinderNames := false) -abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) := +@[deprecated MVarId.introN] +abbrev introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly := false) : MetaM (Array FVarId × MVarId) := + mvarId.introN n givenNames useNamesForExplicitOnly + +/-- +Introduce `n` binders in the goal `mvarId`. The new hypotheses are named using the binder names. +The suffix `P` stands for "preserving`. +-/ +abbrev _root_.Lean.MVarId.introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) := introNCore mvarId n [] (useNamesForExplicitOnly := false) (preserveBinderNames := true) -def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do - let (fvarIds, mvarId) ← introN mvarId 1 [name] +@[deprecated MVarId.introNP] +abbrev introNP (mvarId : MVarId) (n : Nat) : MetaM (Array FVarId × MVarId) := + mvarId.introNP n + +/-- +Introduce one binder using `name` as the the new hypothesis name. +-/ +def _root_.Lean.MVarId.intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do + let (fvarIds, mvarId) ← mvarId.introN 1 [name] return (fvarIds[0]!, mvarId) +@[deprecated MVarId.intro] +def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do + mvarId.intro name + def intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) : MetaM (FVarId × MVarId) := do let (fvarIds, mvarId) ← introNCore mvarId 1 [] (useNamesForExplicitOnly := false) preserveBinderNames return (fvarIds[0]!, mvarId) -abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := +/-- +Introduce one binder. +-/ +abbrev _root_.Lean.MVarId.intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := intro1Core mvarId false -abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) := +@[deprecated MVarId.intro1] +abbrev intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := + mvarId.intro1 + +/-- +Introduce one binder. The new hypothesis is named using the binder name. +-/ +abbrev _root_.Lean.MVarId.intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) := intro1Core mvarId true -private def getIntrosSize : Expr → Nat - | Expr.forallE _ _ b _ => getIntrosSize b + 1 - | Expr.letE _ _ _ b _ => getIntrosSize b + 1 - | Expr.mdata _ b => getIntrosSize b - | _ => 0 +@[deprecated MVarId.intro1P] +abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) := + mvarId.intro1P -def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do - let type ← Meta.getMVarType mvarId +private def getIntrosSize : Expr → Nat + | .forallE _ _ b _ => getIntrosSize b + 1 + | .letE _ _ _ b _ => getIntrosSize b + 1 + | .mdata _ b => getIntrosSize b + | _ => 0 + +/-- +Introduce as many binders as possible without unfolding definitions. +-/ +def _root_.Lean.MVarId.intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do + let type ← mvarId.getType let type ← instantiateMVars type let n := getIntrosSize type if n == 0 then return (#[], mvarId) else - Meta.introN mvarId n + mvarId.introN n + +@[deprecated MVarId.intros] +def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do + mvarId.intros end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean index 8d32e4842f..4a98ed3cee 100644 --- a/src/Lean/Meta/Tactic/Refl.lean +++ b/src/Lean/Meta/Tactic/Refl.lean @@ -8,10 +8,19 @@ import Lean.Meta.Tactic.Util namespace Lean.Meta -def refl (mvarId : MVarId) : MetaM Unit := do - withMVarContext mvarId do - checkNotAssigned mvarId `apply - let targetType ← getMVarType' mvarId +private def useKernel (lhs rhs : Expr) : MetaM Bool := do + if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then + return false + else + return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all + +/-- +Close given goal using `Eq.refl`. +-/ +def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do + mvarId.withContext do + mvarId.checkNotAssigned `refl + let targetType ← mvarId.getType' unless targetType.isAppOfArity ``Eq 3 do throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}" let lhs ← instantiateMVars targetType.appFn!.appArg! @@ -24,12 +33,10 @@ def refl (mvarId : MVarId) : MetaM Unit := do throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}" let us := targetType.getAppFn.constLevels! let α := targetType.appFn!.appFn!.appArg! - assignExprMVar mvarId (mkApp2 (mkConst ``Eq.refl us) α lhs) -where - useKernel (lhs rhs : Expr) : MetaM Bool := do - if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then - return false - else - return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all + mvarId.assign (mkApp2 (mkConst ``Eq.refl us) α lhs) + +@[deprecated MVarId.refl] +def refl (mvarId : MVarId) : MetaM Unit := do + mvarId.refl end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Rename.lean b/src/Lean/Meta/Tactic/Rename.lean index eef0142de5..ce92193ab3 100644 --- a/src/Lean/Meta/Tactic/Rename.lean +++ b/src/Lean/Meta/Tactic/Rename.lean @@ -7,11 +7,18 @@ import Lean.Meta.Tactic.Util namespace Lean.Meta -def rename (mvarId : MVarId) (fvarId : FVarId) (newUserName : Name) : MetaM MVarId := withMVarContext mvarId do - checkNotAssigned mvarId `rename - let lctxNew := (← getLCtx).setUserName fvarId newUserName - let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) (← getMVarType mvarId) MetavarKind.syntheticOpaque (← getMVarTag mvarId) - assignExprMVar mvarId mvarNew +/-- +Rename the user-face naming for the free variable `fvarId` at `mvarId`. +-/ +def _root_.Lean.MVarId.rename (mvarId : MVarId) (fvarId : FVarId) (userNameNew : Name) : MetaM MVarId := mvarId.withContext do + mvarId.checkNotAssigned `rename + let lctxNew := (← getLCtx).setUserName fvarId userNameNew + let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) (← mvarId.getType) MetavarKind.syntheticOpaque (← mvarId.getTag) + mvarId.assign mvarNew return mvarNew.mvarId! +@[deprecated MVarId.rename] +def rename (mvarId : MVarId) (fvarId : FVarId) (newUserName : Name) : MetaM MVarId := + mvarId.rename fvarId newUserName + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index fef76e7e60..d9ffb56fdf 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -17,19 +17,23 @@ namespace Lean.Meta /-- Convert the given goal `Ctx |- target` into `Ctx |- targetNew` using an equality proof `eqProof : target = targetNew`. It assumes `eqProof` has type `target = targetNew` -/ -def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `replaceTarget - let tag ← getMVarTag mvarId +def _root_.Lean.MVarId.replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `replaceTarget + let tag ← mvarId.getTag let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag - let target ← getMVarType mvarId + let target ← mvarId.getType let u ← getLevel target let eq ← mkEq target targetNew let newProof ← mkExpectedTypeHint eqProof eq let val := mkAppN (Lean.mkConst `Eq.mpr [u]) #[target, targetNew, newProof, mvarNew] - assignExprMVar mvarId val + mvarId.assign val return mvarNew.mvarId! +@[deprecated MVarId.replaceTargetEq] +def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : MetaM MVarId := + mvarId.replaceTargetEq targetNew eqProof + /-- Convert the given goal `Ctx | target` into `Ctx |- targetNew`. It assumes the goals are definitionally equal. We use the proof term @@ -37,35 +41,32 @@ def replaceTargetEq (mvarId : MVarId) (targetNew : Expr) (eqProof : Expr) : Meta @id target mvarNew ``` to create a checkpoint. -/ -def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := - withMVarContext mvarId do - checkNotAssigned mvarId `change - let target ← getMVarType mvarId +def _root_.Lean.MVarId.replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := + mvarId.withContext do + mvarId.checkNotAssigned `change + let target ← mvarId.getType if target == targetNew then return mvarId else - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag let newVal ← mkExpectedTypeHint mvarNew target - assignExprMVar mvarId newVal + mvarId.assign newVal return mvarNew.mvarId! -/-- - Replace type of the local declaration with id `fvarId` with one with the same user-facing name, but with type `typeNew`. - This method assumes `eqProof` is a proof that type of `fvarId` is equal to `typeNew`. - This tactic actually adds a new declaration and (try to) clear the old one. - If the old one cannot be cleared, then at least its user-facing name becomes inaccessible. - Remark: the new declaration is added immediately after `fvarId`. - `typeNew` must be well-formed at `fvarId`, but `eqProof` may contain variables declared after `fvarId`. -/ -def replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult := - withMVarContext mvarId do +@[deprecated MVarId.replaceTargetDefEq] +def replaceTargetDefEq (mvarId : MVarId) (targetNew : Expr) : MetaM MVarId := + mvarId.replaceTargetDefEq targetNew + +private def replaceLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult := + mvarId.withContext do let localDecl ← getLocalDecl fvarId let typeNewPr ← mkEqMP eqProof (mkFVar fvarId) -- `typeNew` may contain variables that occur after `fvarId`. -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed at the position we are inserting it. let (_, localDecl') ← findMaxFVar typeNew |>.run localDecl - let result ← assertAfter mvarId localDecl'.fvarId localDecl.userName typeNew typeNewPr - (do let mvarIdNew ← clear result.mvarId fvarId + let result ← mvarId.assertAfter localDecl'.fvarId localDecl.userName typeNew typeNewPr + (do let mvarIdNew ← result.mvarId.clear fvarId pure { result with mvarId := mvarIdNew }) <|> pure result where @@ -78,53 +79,108 @@ where else return e.hasFVar -def replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do - withMVarContext mvarId do - let mvarDecl ← getMVarDecl mvarId +/-- + Replace type of the local declaration with id `fvarId` with one with the same user-facing name, but with type `typeNew`. + This method assumes `eqProof` is a proof that type of `fvarId` is equal to `typeNew`. + This tactic actually adds a new declaration and (try to) clear the old one. + If the old one cannot be cleared, then at least its user-facing name becomes inaccessible. + Remark: the new declaration is added immediately after `fvarId`. + `typeNew` must be well-formed at `fvarId`, but `eqProof` may contain variables declared after `fvarId`. -/ +abbrev _root_.Lean.MVarId.replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult := + replaceLocalDeclCore mvarId fvarId typeNew eqProof + +@[deprecated MVarId.replaceLocalDecl] +abbrev replaceLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (eqProof : Expr) : MetaM AssertAfterResult := + mvarId.replaceLocalDecl fvarId typeNew eqProof + +/-- +Replace the type of `fvarId` at `mvarId` with `typeNew`. +Remark: this method assumes that `typeNew` is definitionally equal to the current type of `fvarId`. +-/ +def _root_.Lean.MVarId.replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do + mvarId.withContext do + let mvarDecl ← mvarId.getDecl if typeNew == mvarDecl.type then return mvarId else let lctxNew := (← getLCtx).modifyLocalDecl fvarId (·.setType typeNew) let mvarNew ← mkFreshExprMVarAt lctxNew (← getLocalInstances) mvarDecl.type mvarDecl.kind mvarDecl.userName - assignExprMVar mvarId mvarNew + mvarId.assign mvarNew return mvarNew.mvarId! -def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := withMVarContext mvarId do - let target ← getMVarType mvarId +@[deprecated MVarId.replaceLocalDeclDefEq] +def replaceLocalDeclDefEq (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) : MetaM MVarId := do + mvarId.replaceLocalDeclDefEq fvarId typeNew + +/-- +Replace the target type of `mvarId` with `typeNew`. +If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to the current target type. +If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to the current target type. +-/ +def _root_.Lean.MVarId.change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do + let target ← mvarId.getType if checkDefEq then unless (← isDefEq target targetNew) do throwTacticEx `change mvarId m!"given type{indentExpr targetNew}\nis not definitionally equal to{indentExpr target}" - replaceTargetDefEq mvarId targetNew + mvarId.replaceTargetDefEq targetNew -def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do - checkNotAssigned mvarId `changeLocalDecl - let (xs, mvarId) ← revert mvarId #[fvarId] true - withMVarContext mvarId do +@[deprecated MVarId.change] +def change (mvarId : MVarId) (targetNew : Expr) (checkDefEq := true) : MetaM MVarId := mvarId.withContext do + mvarId.change targetNew checkDefEq + +/-- +Replace the type of the free variable `fvarId` with `typeNew`. +If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to `fvarId` type. +If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to `fvarId` type. +-/ +def _root_.Lean.MVarId.changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do + mvarId.checkNotAssigned `changeLocalDecl + let (xs, mvarId) ← mvarId.revert #[fvarId] true + mvarId.withContext do let numReverted := xs.size - let target ← getMVarType mvarId + let target ← mvarId.getType let check (typeOld : Expr) : MetaM Unit := do if checkDefEq then unless (← isDefEq typeNew typeOld) do throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}" let finalize (targetNew : Expr) : MetaM MVarId := do - let mvarId ← replaceTargetDefEq mvarId targetNew - let (_, mvarId) ← introNP mvarId numReverted + let mvarId ← mvarId.replaceTargetDefEq targetNew + let (_, mvarId) ← mvarId.introNP numReverted pure mvarId match target with - | Expr.forallE n d b c => do check d; finalize (mkForall n c typeNew b) - | Expr.letE n t v b _ => do check t; finalize (mkLet n typeNew v b) + | .forallE n d b c => do check d; finalize (mkForall n c typeNew b) + | .letE n t v b _ => do check t; finalize (mkLet n typeNew v b) | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target" -def modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do - withMVarContext mvarId do - checkNotAssigned mvarId `modifyTarget - change mvarId (← f (← getMVarType mvarId)) (checkDefEq := false) +@[deprecated MVarId.changeLocalDecl] +def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkDefEq := true) : MetaM MVarId := do + mvarId.changeLocalDecl fvarId typeNew checkDefEq -def modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do - modifyTarget mvarId fun target => do +/-- +Modify `mvarId` target type using `f`. +-/ +def _root_.Lean.MVarId.modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + mvarId.withContext do + mvarId.checkNotAssigned `modifyTarget + mvarId.change (← f (← mvarId.getType)) (checkDefEq := false) + +@[deprecated modifyTarget] +def modifyTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + mvarId.modifyTarget f + +/-- +Modify `mvarId` target type left-hand-side using `f`. +Throw an error if target type is not an equality. +-/ +def _root_.Lean.MVarId.modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + mvarId.modifyTarget fun target => do if let some (_, lhs, rhs) ← matchEq? target then mkEq (← f lhs) rhs else throwTacticEx `modifyTargetEqLHS mvarId m!"equality expected{indentExpr target}" +@[deprecated MVarId.modifyTargetEqLHS] +def modifyTargetEqLHS (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := do + mvarId.modifyTargetEqLHS f + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean index 7dacfea3d7..6c56cc5d2b 100644 --- a/src/Lean/Meta/Tactic/Revert.lean +++ b/src/Lean/Meta/Tactic/Revert.lean @@ -7,11 +7,14 @@ import Lean.Meta.Tactic.Clear namespace Lean.Meta -def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do +/-- +Revert free variables `fvarIds` at goal `mvarId`. +-/ +def _root_.Lean.MVarId.revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do if fvarIds.isEmpty then pure (#[], mvarId) - else withMVarContext mvarId do - checkNotAssigned mvarId `revert + else mvarId.withContext do + mvarId.checkNotAssigned `revert for fvarId in fvarIds do if (← getLocalDecl fvarId) |>.isAuxDecl then throwError "failed to revert {mkFVar fvarId}, it is an auxiliary declaration created to represent recursive definitions" @@ -22,22 +25,26 @@ def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := f let mut toRevertNew := #[] for x in toRevert do if (← getLocalDecl x.fvarId!) |>.isAuxDecl then - mvarId ← clear mvarId x.fvarId! + mvarId ← mvarId.clear x.fvarId! else toRevertNew := toRevertNew.push x - let tag ← getMVarTag mvarId + let tag ← mvarId.getTag -- TODO: the following code can be optimized because `MetavarContext.revert` will compute `collectDeps` again. -- We should factor out the relevat part -- Set metavariable kind to natural to make sure `revert` will assign it. - setMVarKind mvarId MetavarKind.natural + mvarId.setKind .natural let (e, toRevert) ← try liftMkBindingM <| MetavarContext.revert toRevertNew mvarId preserveOrder finally - setMVarKind mvarId MetavarKind.syntheticOpaque + mvarId.setKind .syntheticOpaque let mvar := e.getAppFn - setMVarTag mvar.mvarId! tag + mvar.mvarId!.setTag tag return (toRevert.map Expr.fvarId!, mvar.mvarId!) +@[deprecated MVarId.revert] +def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := false) : MetaM (Array FVarId × MVarId) := do + mvarId.revert fvarIds preserveOrder + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean index d04d2e6c7e..449430f4f3 100644 --- a/src/Lean/Meta/Tactic/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Rewrite.lean @@ -16,10 +16,13 @@ structure RewriteResult where eqProof : Expr mvarIds : List MVarId -- new goals -def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) +/-- +Rewrite goal `mvarId` +-/ +def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult := - withMVarContext mvarId do - checkNotAssigned mvarId `rewrite + mvarId.withContext do + mvarId.checkNotAssigned `rewrite let heqType ← instantiateMVars (← inferType heq) let (newMVars, binderInfos, heqType) ← forallMetaTelescopeReducing heqType let heq := mkAppN heq newMVars @@ -45,7 +48,7 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) let eqRefl ← mkEqRefl e let eqPrf ← mkEqNDRec motive eqRefl heq postprocessAppMVars `rewrite mvarId newMVars binderInfos - let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM (not <$> isExprMVarAssigned ·) + let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned let otherMVarIds ← getMVarsNoDelayed eqPrf let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·) let newMVarIds := newMVarIds ++ otherMVarIds @@ -64,4 +67,9 @@ def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) | none => cont heq heqType +@[deprecated MVarId.rewrite] +def rewrite (mvarId : MVarId) (e : Expr) (heq : Expr) + (symm : Bool := false) (occs : Occurrences := Occurrences.all) (config := { : Rewrite.Config }) : MetaM RewriteResult := + mvarId.rewrite e heq symm occs config + end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index ae1be6a3f7..5c43556230 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -759,8 +759,8 @@ partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do where go? (mvarId : MVarId) : MetaM (Option MVarId) := try - let (fvarId, mvarId) ← intro1 mvarId - withMVarContext mvarId do + let (fvarId, mvarId) ← mvarId.intro1 + mvarId.withContext do let localDecl ← getLocalDecl fvarId if localDecl.type.isEq || localDecl.type.isHEq then if let some { mvarId, .. } ← unifyEq? mvarId fvarId {} then @@ -824,21 +824,21 @@ def dsimp (e : Expr) (ctx : Simp.Context) : MetaM Expr := do profileitM Exceptio -/ def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId := do match r.proof? with - | some proof => replaceTargetEq mvarId r.expr proof + | some proof => mvarId.replaceTargetEq r.expr proof | none => if target != r.expr then - replaceTargetDefEq mvarId r.expr + mvarId.replaceTargetDefEq r.expr else return mvarId /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) := do - let target ← instantiateMVars (← getMVarType mvarId) + let target ← instantiateMVars (← mvarId.getType) let r ← simp target ctx discharge? if mayCloseGoal && r.expr.isConstOf ``True then match r.proof? with - | some proof => assignExprMVar mvarId (← mkOfEqTrue proof) - | none => assignExprMVar mvarId (mkConst ``True.intro) + | some proof => mvarId.assign (← mkOfEqTrue proof) + | none => mvarId.assign (mkConst ``True.intro) return none else applySimpResultToTarget mvarId target r @@ -847,8 +847,8 @@ def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise, where `mvarId'` is the simplified new goal. -/ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option MVarId) := - withMVarContext mvarId do - checkNotAssigned mvarId `simp + mvarId.withContext do + mvarId.checkNotAssigned `simp simpTargetCore mvarId ctx discharge? mayCloseGoal /-- @@ -859,8 +859,8 @@ def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp. def applySimpResultToProp (mvarId : MVarId) (proof : Expr) (prop : Expr) (r : Simp.Result) (mayCloseGoal := true) : MetaM (Option (Expr × Expr)) := do if mayCloseGoal && r.expr.isConstOf ``False then match r.proof? with - | some eqProof => assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (← mkEqMP eqProof proof)) - | none => assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) proof) + | some eqProof => mvarId.assign (← mkFalseElim (← mvarId.getType) (← mkEqMP eqProof proof)) + | none => mvarId.assign (← mkFalseElim (← mvarId.getType) proof) return none else match r.proof? with @@ -890,9 +890,9 @@ def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Opti | some (value, type') => let localDecl ← getLocalDecl fvarId if localDecl.type != type' then - let mvarId ← assert mvarId localDecl.userName type' value - let mvarId ← tryClear mvarId localDecl.fvarId - let (fvarId, mvarId) ← intro1P mvarId + let mvarId ← mvarId.assert localDecl.userName type' value + let mvarId ← mvarId.tryClear localDecl.fvarId + let (fvarId, mvarId) ← mvarId.intro1P return some (fvarId, mvarId) else return some (fvarId, mvarId) @@ -903,9 +903,9 @@ def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Opti def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId)) := do if r.proof?.isNone then -- New result is definitionally equal to input. Thus, we can avoid creating a new variable if there are dependencies - let mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr + let mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr if mayCloseGoal && r.expr.isConstOf ``False then - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId)) + mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) return none else return some (fvarId, mvarId) @@ -913,8 +913,8 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal) def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (mayCloseGoal := true) : MetaM (Option (FVarId × MVarId)) := do - withMVarContext mvarId do - checkNotAssigned mvarId `simp + mvarId.withContext do + mvarId.checkNotAssigned `simp let localDecl ← getLocalDecl fvarId let type ← instantiateMVars localDecl.type applySimpResultToLocalDeclCore mvarId fvarId (← simpStep mvarId (mkFVar fvarId) type ctx discharge? mayCloseGoal) @@ -922,8 +922,8 @@ def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (disc abbrev FVarIdToLemmaId := FVarIdMap Name def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (fvarIdToLemmaId : FVarIdToLemmaId := {}) : MetaM (Option (Array FVarId × MVarId)) := do - withMVarContext mvarId do - checkNotAssigned mvarId `simp + mvarId.withContext do + mvarId.checkNotAssigned `simp let mut mvarId := mvarId let mut toAssert := #[] let mut replaced := #[] @@ -940,22 +940,22 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value } | none => if r.expr.isConstOf ``False then - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId)) + mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) return none -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...` -- Reason: it introduces a `mkExpectedTypeHint` - mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr + mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr replaced := replaced.push fvarId if simplifyTarget then match (← simpTarget mvarId ctx discharge?) with | none => return none | some mvarIdNew => mvarId := mvarIdNew - let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert + let (fvarIdsNew, mvarIdNew) ← mvarId.assertHypotheses toAssert let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId - let mvarIdNew ← tryClearMany mvarIdNew toClear + let mvarIdNew ← mvarIdNew.tryClearMany toClear return (fvarIdsNew, mvarIdNew) -def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := withMVarContext mvarId do +def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := mvarId.withContext do let mut ctx := ctx for h in (← getPropHyps) do let localDecl ← getLocalDecl h @@ -965,36 +965,36 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option S match (← simpTarget mvarId ctx discharge?) with | none => return TacticResultCNM.closed | some mvarId' => - if (← getMVarType mvarId) == (← getMVarType mvarId') then + if (← mvarId.getType) == (← mvarId'.getType) then return TacticResultCNM.noChange else return TacticResultCNM.modified mvarId' def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) : MetaM (Option MVarId) := do - withMVarContext mvarId do - checkNotAssigned mvarId `simp + mvarId.withContext do + mvarId.checkNotAssigned `simp let mut mvarId := mvarId for fvarId in fvarIdsToSimp do let localDecl ← getLocalDecl fvarId let type ← instantiateMVars localDecl.type let typeNew ← dsimp type ctx if typeNew.isConstOf ``False then - assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId)) + mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId)) return none if typeNew != type then - mvarId ← replaceLocalDeclDefEq mvarId fvarId typeNew + mvarId ← mvarId.replaceLocalDeclDefEq fvarId typeNew if simplifyTarget then - let target ← getMVarType mvarId + let target ← mvarId.getType let targetNew ← dsimp target ctx if targetNew.isConstOf ``True then - assignExprMVar mvarId (mkConst ``True.intro) + mvarId.assign (mkConst ``True.intro) return none if let some (_, lhs, rhs) := targetNew.eq? then if (← withReducible <| isDefEq lhs rhs) then - assignExprMVar mvarId (← mkEqRefl lhs) + mvarId.assign (← mkEqRefl lhs) return none if target != targetNew then - mvarId ← replaceTargetDefEq mvarId targetNew + mvarId ← mvarId.replaceTargetDefEq targetNew return some mvarId end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index 01d7c944d7..f70529fefd 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -28,8 +28,8 @@ structure State where abbrev M := StateRefT State MetaM private def initEntries : M Unit := do - let hs ← withMVarContext (← get).mvarId do getPropHyps - let hsNonDeps ← getNondepPropHyps (← get).mvarId + let hs ← (← get).mvarId.withContext do getPropHyps + let hsNonDeps ← (← get).mvarId.getNondepPropHyps let mut simpThms := (← get).ctx.simpTheorems for h in hs do let localDecl ← getLocalDecl h @@ -114,15 +114,15 @@ def main : M (Option MVarId) := do else let mvarId := (← get).mvarId let entries := (← get).entries - let (_, mvarId) ← assertHypotheses mvarId <| entries.filterMap fun e => + let (_, mvarId) ← mvarId.assertHypotheses <| entries.filterMap fun e => -- Do not assert `True` hypotheses if e.type.isConstOf ``True then none else some { userName := e.userName, type := e.type, value := e.proof } - tryClearMany mvarId (entries.map fun e => e.fvarId) + mvarId.tryClearMany (entries.map fun e => e.fvarId) end SimpAll def simpAll (mvarId : MVarId) (ctx : Simp.Context) : MetaM (Option MVarId) := do - withMVarContext mvarId do + mvarId.withContext do SimpAll.main.run' { mvarId := mvarId, ctx := ctx } end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 3fd3ca6a9c..271f2d3ef1 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -29,8 +29,8 @@ where | some r => return r | none => return Simp.Step.visit { expr := e } -def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do - let target ← instantiateMVars (← getMVarType mvarId) +def simpMatchTarget (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do + let target ← instantiateMVars (← mvarId.getType) let r ← simpMatch target applySimpResultToTarget mvarId target r @@ -51,12 +51,12 @@ where return Simp.Step.visit { expr := e } private def simpMatchTargetCore (mvarId : MVarId) (matchDeclName : Name) (matchEqDeclName : Name) : MetaM MVarId := do - withMVarContext mvarId do - let target ← instantiateMVars (← getMVarType mvarId) + mvarId.withContext do + let target ← instantiateMVars (← mvarId.getType) let r ← simpMatchCore matchDeclName matchEqDeclName target match r.proof? with - | some proof => replaceTargetEq mvarId r.expr proof - | none => replaceTargetDefEq mvarId r.expr + | some proof => mvarId.replaceTargetEq r.expr proof + | none => mvarId.replaceTargetDefEq r.expr private partial def withEqs (lhs rhs : Array Expr) (k : Array Expr → Array Expr → MetaM α) : MetaM α := do go 0 #[] #[] @@ -99,7 +99,7 @@ where ⊢ g x = 2 * x + 1 ``` -/ -private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : Name) (motiveType : Expr) (discrs : Array Expr) : MetaM (Array FVarId × Array FVarId × MVarId) := withMVarContext mvarId do +private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : Name) (motiveType : Expr) (discrs : Array Expr) : MetaM (Array FVarId × Array FVarId × MVarId) := mvarId.withContext do if discrs.all (·.isFVar) then return (discrs.map (·.fvarId!), #[], mvarId) let some matcherInfo ← getMatcherInfo? matcherDeclName | unreachable! @@ -138,18 +138,18 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N altsNew := altsNew.push altNew return .done { matcherApp with alts := altsNew }.toExpr transform (← instantiateMVars e) pre - let targetNew ← mkNewTarget (← getMVarType mvarId) + let targetNew ← mkNewTarget (← mvarId.getType) unless (← foundRef.get) do throwError "'applyMatchSplitter' failed, did not find discriminants" let targetNew ← mkForallFVars (discrVars ++ eqs) targetNew unless (← isTypeCorrect targetNew) do throwError "'applyMatchSplitter' failed, failed to generalize target" return (targetNew, rfls) - let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew (← getMVarTag mvarId) + let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew (← mvarId.getTag) trace[Meta.Tactic.split] "targetNew:\n{mvarNew.mvarId!}" - assignExprMVar mvarId (mkAppN (mkAppN mvarNew discrs) rfls) - let (discrs', mvarId') ← introNP mvarNew.mvarId! discrs.size - let (discrEqs, mvarId') ← introNP mvarId' discrs.size + mvarId.assign (mkAppN (mkAppN mvarNew discrs) rfls) + let (discrs', mvarId') ← mvarNew.mvarId!.introNP discrs.size + let (discrEqs, mvarId') ← mvarId'.introNP discrs.size return (discrs', discrEqs, mvarId') where /-- @@ -183,7 +183,7 @@ where k altEqsNew subst go 0 #[] #[] -private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs : Array FVarId) : MetaM MVarId := withMVarContext mvarId do +private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs : Array FVarId) : MetaM MVarId := mvarId.withContext do let mut mvarId := mvarId let mut fvarSubst := fvarSubst for fvarId in discrEqs do @@ -208,14 +208,14 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le let (discrFVarIds, discrEqs, mvarId) ← generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs trace[Meta.Tactic.split] "after generalizeMatchDiscrs\n{mvarId}" let mvarId ← generalizeTargetsEq mvarId motiveType (discrFVarIds.map mkFVar) - withMVarContext mvarId do trace[Meta.Tactic.split] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}" + mvarId.withContext do trace[Meta.Tactic.split] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}" trace[Meta.Tactic.split] "after generalize\n{mvarId}" let numEqs := discrs.size - let (discrFVarIdsNew, mvarId) ← introN mvarId discrs.size + let (discrFVarIdsNew, mvarId) ← mvarId.introN discrs.size trace[Meta.Tactic.split] "after introN\n{mvarId}" let discrsNew := discrFVarIdsNew.map mkFVar - let mvarType ← getMVarType mvarId - let elimUniv ← withMVarContext mvarId <| getLevel mvarType + let mvarType ← mvarId.getType + let elimUniv ← mvarId.withContext <| getLevel mvarType let us ← if let some uElimPos := info.uElimPos? then pure <| us.set! uElimPos elimUniv else @@ -223,17 +223,17 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le throwError "match-splitter can only eliminate into `Prop`" pure us let splitter := mkAppN (mkConst matchEqns.splitterName us.toList) params - withMVarContext mvarId do + mvarId.withContext do let motive ← mkLambdaFVars discrsNew mvarType let splitter := mkAppN (mkApp splitter motive) discrsNew check splitter trace[Meta.Tactic.split] "after check splitter" - let mvarIds ← apply mvarId splitter + let mvarIds ← mvarId.apply splitter unless mvarIds.length == matchEqns.size do throwError "'applyMatchSplitter' failed, unexpected number of goals created after applying splitter for '{matcherDeclName}'." let (_, mvarIds) ← mvarIds.foldlM (init := (0, [])) fun (i, mvarIds) mvarId => do let numParams := matchEqns.splitterAltNumParams[i]! - let (_, mvarId) ← introN mvarId numParams + let (_, mvarId) ← mvarId.introN numParams trace[Meta.Tactic.split] "before unifyEqs\n{mvarId}" match (← Cases.unifyEqs? (numEqs + info.getNumDiscrEqs) mvarId {}) with | none => return (i+1, mvarIds) -- case was solved @@ -289,7 +289,7 @@ end Split open Split partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do - let target ← instantiateMVars (← getMVarType mvarId) + let target ← instantiateMVars (← mvarId.getType) let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do if let some e := findSplit? (← getEnv) target splitIte badCases then if e.isIte || e.isDIte then @@ -305,15 +305,15 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L go {} def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do - withMVarContext mvarId do + mvarId.withContext do if let some e := findSplit? (← getEnv) (← instantiateMVars (← inferType (mkFVar fvarId))) then if e.isIte || e.isDIte then return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂] else - let (fvarIds, mvarId) ← revert mvarId #[fvarId] + let (fvarIds, mvarId) ← mvarId.revert #[fvarId] let num := fvarIds.size let mvarIds ← splitMatch mvarId e - let mvarIds ← mvarIds.mapM fun mvarId => return (← introNP mvarId num).2 + let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.introNP num).2 return some mvarIds else return none diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index 76a58e32e8..d7dda76ed1 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/src/Lean/Meta/Tactic/SplitIf.lean @@ -95,7 +95,7 @@ def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do unreachable! def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := commitWhenSome? do - if let some (s₁, s₂) ← splitIfAt? mvarId (← getMVarType mvarId) hName? then + if let some (s₁, s₂) ← splitIfAt? mvarId (← mvarId.getType) hName? then let mvarId₁ ← simpIfTarget s₁.mvarId let mvarId₂ ← simpIfTarget s₂.mvarId if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then @@ -106,7 +106,7 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt return none def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name := none) : MetaM (Option (MVarId × MVarId)) := commitWhenSome? do - withMVarContext mvarId do + mvarId.withContext do if let some (s₁, s₂) ← splitIfAt? mvarId (← inferType (mkFVar fvarId)) hName? then let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index 11835b7b47..9015c3a5e0 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -15,9 +15,9 @@ import Lean.Meta.Tactic.FVarSubst namespace Lean.Meta def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : FVarSubst := {}) (clearH := true) (tryToSkip := false) : MetaM (FVarSubst × MVarId) := - withMVarContext mvarId do - let tag ← getMVarTag mvarId - checkNotAssigned mvarId `subst + mvarId.withContext do + let tag ← mvarId.getTag + mvarId.checkNotAssigned `subst let hFVarIdOriginal := hFVarId let hLocalDecl ← getLocalDecl hFVarId match (← matchEq? hLocalDecl.type) with @@ -31,9 +31,9 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId.name}) with {b}" if (← exprDependsOn b aFVarId) then throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}" - let (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true + let (vars, mvarId) ← mvarId.revert #[aFVarId, hFVarId] true trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}" - let (twoVars, mvarId) ← introNP mvarId 2 + let (twoVars, mvarId) ← mvarId.introNP 2 trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}" trace[Meta.Tactic.subst] "reverted variables {vars.map (·.name)}" let aFVarId := twoVars[0]! @@ -44,20 +44,20 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let skip ← if !tryToSkip || vars.size != 2 then pure false else - let mvarType ← getMVarType mvarId + let mvarType ← mvarId.getType if (← exprDependsOn mvarType aFVarId) then pure false else if (← exprDependsOn mvarType hFVarId) then pure false else pure true if skip then if clearH then - let mvarId ← clear mvarId hFVarId - let mvarId ← clear mvarId aFVarId + let mvarId ← mvarId.clear hFVarId + let mvarId ← mvarId.clear aFVarId pure ({}, mvarId) else pure ({}, mvarId) else - withMVarContext mvarId do - let mvarDecl ← getMVarDecl mvarId + mvarId.withContext do + let mvarDecl ← mvarId.getDecl let type := mvarDecl.type let hLocalDecl ← getLocalDecl hFVarId match (← matchEq? hLocalDecl.type) with @@ -70,14 +70,14 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag let minor := newMVar let newVal ← if depElim then mkEqRec motive minor major else mkEqNDRec motive minor major - assignExprMVar mvarId newVal + mvarId.assign newVal let mvarId := newMVar.mvarId! let mvarId ← if clearH then - let mvarId ← clear mvarId hFVarId - clear mvarId aFVarId + let mvarId ← mvarId.clear hFVarId + mvarId.clear aFVarId else pure mvarId - let (newFVars, mvarId) ← introNP mvarId (vars.size - 2) + let (newFVars, mvarId) ← mvarId.introNP (vars.size - 2) trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}" let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) => let var := vars[i+2]! @@ -120,7 +120,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : If `h` is not of the give form, then just return `(h, mvarId)` -/ def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool := true) : MetaM (FVarId × MVarId) := - withMVarContext mvarId do + mvarId.withContext do let decl ← getLocalDecl fvarId let type ← whnf decl.type match type.heq? with @@ -129,16 +129,16 @@ def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool := true) : Me if (← isDefEq α β) then let pr ← mkEqOfHEq (mkFVar fvarId) let eq ← mkEq a b - let mut mvarId ← assert mvarId decl.userName eq pr + let mut mvarId ← mvarId.assert decl.userName eq pr if tryToClear then - mvarId ← tryClear mvarId fvarId - let (fvarId, mvarId') ← intro1P mvarId + mvarId ← mvarId.tryClear fvarId + let (fvarId, mvarId') ← mvarId.intro1P return (fvarId, mvarId') else return (fvarId, mvarId) partial def subst (mvarId : MVarId) (h : FVarId) : MetaM MVarId := - withMVarContext mvarId do + mvarId.withContext do let localDecl ← getLocalDecl h match (← matchEq? localDecl.type) with | some _ => substEq mvarId h @@ -152,13 +152,13 @@ partial def subst (mvarId : MVarId) (h : FVarId) : MetaM MVarId := | none => findEq mvarId h where /-- Give `h : Eq α a b`, try to apply `substCore` -/ - substEq (mvarId : MVarId) (h : FVarId) : MetaM MVarId := withMVarContext mvarId do + substEq (mvarId : MVarId) (h : FVarId) : MetaM MVarId := mvarId.withContext do let localDecl ← getLocalDecl h let some (_, lhs, rhs) ← matchEq? localDecl.type | unreachable! let substReduced (newType : Expr) (symm : Bool) : MetaM MVarId := do - let mvarId ← assert mvarId localDecl.userName newType (mkFVar h) - let (hFVarId', mvarId) ← intro1P mvarId - let mvarId ← clear mvarId h + let mvarId ← mvarId.assert localDecl.userName newType (mkFVar h) + let (hFVarId', mvarId) ← mvarId.intro1P + let mvarId ← mvarId.clear h return (← substCore mvarId hFVarId' (symm := symm) (tryToSkip := true)).2 let rhs' ← whnf rhs if rhs'.isFVar then @@ -177,7 +177,7 @@ where throwTacticEx `subst mvarId m!"invalid equality proof, it is not of the form (x = t) or (t = x){indentExpr localDecl.type}" /-- Try to find an equation of the form `heq : h = rhs` or `heq : lhs = h` -/ - findEq (mvarId : MVarId) (h : FVarId) : MetaM MVarId := withMVarContext mvarId do + findEq (mvarId : MVarId) (h : FVarId) : MetaM MVarId := mvarId.withContext do let localDecl ← getLocalDecl h if localDecl.isLet then throwTacticEx `subst mvarId m!"variable '{mkFVar h}' is a let-declaration" @@ -212,7 +212,7 @@ def trySubst (mvarId : MVarId) (hFVarId : FVarId) : MetaM MVarId := do | some mvarId => return mvarId | none => return mvarId -def substSomeVar? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do +def substSomeVar? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do for localDecl in (← getLCtx) do if let some mvarId ← subst? mvarId localDecl.fvarId then return some mvarId diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean index d84c8873e4..7c8c7cfb6e 100644 --- a/src/Lean/Meta/Tactic/Unfold.lean +++ b/src/Lean/Meta/Tactic/Unfold.lean @@ -30,13 +30,13 @@ where | _ => return Simp.Step.done r return Simp.Step.visit { expr := e } -def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do - let target ← instantiateMVars (← getMVarType mvarId) +def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do + let target ← instantiateMVars (← mvarId.getType) let r ← unfold target declName if r.expr == target then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr target}" applySimpResultToTarget mvarId target r -def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do +def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do let localDecl ← getLocalDecl fvarId let r ← unfold (← instantiateMVars localDecl.type) declName if r.expr == localDecl.type then throwError "tactic 'unfold' failed to unfold '{declName}' at{indentExpr localDecl.type}" diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean index 0dad193463..55b64fa414 100644 --- a/src/Lean/Meta/Tactic/UnifyEq.lean +++ b/src/Lean/Meta/Tactic/UnifyEq.lean @@ -12,8 +12,8 @@ private def heqToEq' (mvarId : MVarId) (eqDecl : LocalDecl) : MetaM MVarId := do /- Convert heterogeneous equality into a homegeneous one -/ let prf ← mkEqOfHEq (mkFVar eqDecl.fvarId) let aEqb ← whnf (← inferType prf) - let mvarId ← assert mvarId eqDecl.userName aEqb prf - clear mvarId eqDecl.fvarId + let mvarId ← mvarId.assert eqDecl.userName aEqb prf + mvarId.clear eqDecl.fvarId structure UnifyEqResult where mvarId : MVarId @@ -38,7 +38,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) (acyclic : MVarId → Expr → MetaM Bool := fun _ _ => return false) (caseName? : Option Name := none) : MetaM (Option UnifyEqResult) := do - withMVarContext mvarId do + mvarId.withContext do let eqDecl ← getLocalDecl eqFVarId if eqDecl.type.isHEq then let mvarId ← heqToEq' mvarId eqDecl @@ -58,7 +58,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) return some { mvarId, subst } else if (← isDefEq a b) then /- Skip equality -/ - return some { mvarId := (← clear mvarId eqFVarId), subst } + return some { mvarId := (← mvarId.clear eqFVarId), subst } else if (← acyclic mvarId (mkFVar eqFVarId)) then return none -- this alternative has been solved else @@ -77,8 +77,8 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) /- Reduced lhs/rhs of current equality -/ let prf := mkFVar eqFVarId let aEqb' ← mkEq a' b' - let mvarId ← assert mvarId eqDecl.userName aEqb' prf - let mvarId ← clear mvarId eqFVarId + let mvarId ← mvarId.assert eqDecl.userName aEqb' prf + let mvarId ← mvarId.clear eqFVarId return some { mvarId, subst, numNewEqs := 1 } else match caseName? with @@ -97,7 +97,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) | a, b => if (← isDefEq a b) then /- Skip equality -/ - return some { mvarId := (← clear mvarId eqFVarId), subst } + return some { mvarId := (← mvarId.clear eqFVarId), subst } else injection a b diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index b916c67978..9586e4b864 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -11,18 +11,26 @@ import Lean.Meta.PPGoal namespace Lean.Meta /-- Aka user name -/ -def getMVarTag (mvarId : MVarId) : MetaM Name := - return (← getMVarDecl mvarId).userName +def _root_.Lean.MVarId.getTag (mvarId : MVarId) : MetaM Name := + return (← mvarId.getDecl).userName -def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do +@[deprecated MVarId.getTag] +def getMVarTag (mvarId : MVarId) : MetaM Name := + mvarId.getTag + +def _root_.Lean.MVarId.setTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do modify fun s => { s with mctx := s.mctx.setMVarUserName mvarId tag } +@[deprecated MVarId.setTag] +def setMVarTag (mvarId : MVarId) (tag : Name) : MetaM Unit := do + mvarId.setTag tag + def appendTag (tag : Name) (suffix : Name) : Name := tag.modifyBase (· ++ suffix.eraseMacroScopes) def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do - let tag ← getMVarTag mvarId - setMVarTag mvarId (appendTag tag suffix) + let tag ← mvarId.getTag + mvarId.setTag (appendTag tag suffix) def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr := mkFreshExprMVar type MetavarKind.syntheticOpaque tag @@ -36,33 +44,64 @@ def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : Me def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}" -def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do - if (← isExprMVarAssigned mvarId) then +/-- +Throw error message if `mvarId` is already assigned. +-/ +def _root_.Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do + if (← mvarId.isAssigned) then throwTacticEx tacticName mvarId "metavariable has already been assigned" -def getMVarType (mvarId : MVarId) : MetaM Expr := - return (← getMVarDecl mvarId).type +@[deprecated MVarId.checkNotAssigned] +def checkNotAssigned (mvarId : MVarId) (tacticName : Name) : MetaM Unit := do + mvarId.checkNotAssigned tacticName +def _root_.Lean.MVarId.getType (mvarId : MVarId) : MetaM Expr := + return (← mvarId.getDecl).type + +@[deprecated MVarId.getType] +def getMVarType (mvarId : MVarId) : MetaM Expr := + mvarId.getType + +def _root_.Lean.MVarId.getType' (mvarId : MVarId) : MetaM Expr := do + whnf (← instantiateMVars (← mvarId.getType)) + +@[deprecated MVarId.getType'] def getMVarType' (mvarId : MVarId) : MetaM Expr := do - whnf (← instantiateMVars (← getMVarDecl mvarId).type) + mvarId.getType' builtin_initialize registerTraceClass `Meta.Tactic /-- Assign `mvarId` to `sorryAx` -/ -def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit := - withMVarContext mvarId do - checkNotAssigned mvarId `admit - let mvarType ← getMVarType mvarId +def _root_.Lean.MVarId.admit (mvarId : MVarId) (synthetic := true) : MetaM Unit := + mvarId.withContext do + mvarId.checkNotAssigned `admit + let mvarType ← mvarId.getType let val ← mkSorry mvarType synthetic - assignExprMVar mvarId val + mvarId.assign val + +@[deprecated MVarId.admit] +def admit (mvarId : MVarId) (synthetic := true) : MetaM Unit := + mvarId.admit synthetic /-- Beta reduce the metavariable type head -/ +def _root_.Lean.MVarId.headBetaType (mvarId : MVarId) : MetaM Unit := do + mvarId.setType (← mvarId.getType).headBeta + +@[deprecated MVarId.headBetaType] def headBetaMVarType (mvarId : MVarId) : MetaM Unit := do - setMVarType mvarId (← getMVarType mvarId).headBeta + mvarId.headBetaType /-- Collect nondependent hypotheses that are propositions. -/ -def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := - withMVarContext mvarId do +def _root_.Lean.MVarId.getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := + let removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do + let e ← instantiateMVars e + let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do + e.forEach fun + | Expr.fvar fvarId => modify fun s => s.erase fvarId + | _ => pure () + get + visit |>.run' candidates + mvarId.withContext do let mut candidates : FVarIdHashSet := {} for localDecl in (← getLCtx) do unless localDecl.isAuxDecl do @@ -72,7 +111,7 @@ def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := | some value => candidates ← removeDeps value candidates if (← isProp localDecl.type) && !localDecl.hasValue then candidates := candidates.insert localDecl.fvarId - candidates ← removeDeps (← getMVarType mvarId) candidates + candidates ← removeDeps (← mvarId.getType) candidates if candidates.isEmpty then return #[] else @@ -81,15 +120,10 @@ def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := if candidates.contains localDecl.fvarId then result := result.push localDecl.fvarId return result -where - removeDeps (e : Expr) (candidates : FVarIdHashSet) : MetaM FVarIdHashSet := do - let e ← instantiateMVars e - let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do - e.forEach fun - | Expr.fvar fvarId => modify fun s => s.erase fvarId - | _ => pure () - get - visit |>.run' candidates + +@[deprecated MVarId.getNondepPropHyps] +def getNondepPropHyps (mvarId : MVarId) : MetaM (Array FVarId) := + mvarId.getNondepPropHyps partial def saturate (mvarId : MVarId) (x : MVarId → MetaM (Option (List MVarId))) : MetaM (List MVarId) := do let (_, r) ← go mvarId |>.run #[] diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index f034607f8b..d0688ef4c3 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -337,14 +337,22 @@ def isLevelMVarAssigned [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := d return (← getMCtx).lAssignment.contains mvarId /-- Return `true` if the give metavariable is already assigned. -/ -def isExprMVarAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do +def _root_.Lean.MVarId.isAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do markUsedAssignment return (← getMCtx).eAssignment.contains mvarId -def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do +@[deprecated MVarId.isAssigned] +def isExprMVarAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do + mvarId.isAssigned + +def _root_.Lean.MVarId.isDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do markUsedAssignment return (← getMCtx).dAssignment.contains mvarId +@[deprecated MVarId.isDelayedAssigned] +def isMVarDelayedAssigned [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do + mvarId.isDelayedAssigned + def isLevelMVarAssignable [Monad m] [MonadMCtx m] (mvarId : LMVarId) : m Bool := do markUsedAssignment let mctx ← getMCtx @@ -357,12 +365,16 @@ def MetavarContext.getDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarDe | some decl => decl | none => panic! "unknown metavariable" -def isExprMVarAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do +def _root_.Lean.MVarId.isAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do markUsedAssignment let mctx ← getMCtx let decl := mctx.getDecl mvarId return decl.depth == mctx.depth +@[deprecated MVarId.isAssignable] +def isExprMVarAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := do + mvarId.isAssignable + /-- Return true iff the given level contains an assigned metavariable. -/ def hasAssignedLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool | Level.succ lvl => pure lvl.hasMVar <&&> hasAssignedLevelMVar lvl @@ -385,7 +397,7 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool | Expr.lit _ => return false | Expr.mdata _ e => pure e.hasMVar <&&> hasAssignedMVar e | Expr.proj _ _ e => pure e.hasMVar <&&> hasAssignedMVar e - | Expr.mvar mvarId => isExprMVarAssigned mvarId <||> isMVarDelayedAssigned mvarId + | Expr.mvar mvarId => mvarId.isAssigned <||> mvarId.isDelayedAssigned /-- Return true iff the given level contains a metavariable that can be assigned. -/ def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool @@ -409,7 +421,7 @@ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool | Expr.lit _ => return false | Expr.mdata _ e => pure e.hasMVar <&&> hasAssignableMVar e | Expr.proj _ _ e => pure e.hasMVar <&&> hasAssignableMVar e - | Expr.mvar mvarId => isExprMVarAssignable mvarId + | Expr.mvar mvarId => mvarId.isAssignable /-- Add `mvarId := u` to the universe metavariable assignment. @@ -426,9 +438,13 @@ This method does not check whether `mvarId` is already assigned, nor it checks w a cycle is being introduced, or whether the expression has the right type. This is a low-level API, and it is safer to use `isDefEq (mkMVar mvarId) x`. -/ -def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit := +def _root_.Lean.MVarId.assign [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit := modifyMCtx fun m => { m with eAssignment := m.eAssignment.insert mvarId val, usedAssignment := true } +@[deprecated MVarId.assign] +def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit := + mvarId.assign val + def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvarIdPending : MVarId) : m Unit := modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending }, usedAssignment := true } @@ -531,7 +547,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi match (← getExprMVarAssignment? mvarId) with | some newE => do let newE' ← instantiateExprMVars newE - assignExprMVar mvarId newE' + mvarId.assign newE' pure newE' | none => pure e | e => pure e @@ -1024,7 +1040,7 @@ mutual A potential disadvantage is that `isDefEq` will not eagerly use `synthPending` for natural metavariables. That being said, we should try this approach as soon as we have an extensive test suite. -/ - let newMVarKind := if !(← isExprMVarAssignable mvarId) then MetavarKind.syntheticOpaque else mvarDecl.kind + let newMVarKind := if !(← mvarId.isAssignable) then MetavarKind.syntheticOpaque else mvarDecl.kind let args ← args.mapM (visit xs) let toRevert ← collectForwardDeps mvarLCtx toRevert let newMVarLCtx := reduceLocalContext mvarLCtx toRevert @@ -1041,7 +1057,7 @@ mutual ngen := s.ngen.next } if !mvarDecl.kind.isSyntheticOpaque then - assignExprMVar mvarId result + mvarId.assign result else /- If `mvarId` is the lhs of a delayed assignment `?m #[x_1, ... x_n] := ?mvarPending`, then `nestedFVars` is `#[x_1, ..., x_n]`. diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 58052a6f6a..6a3dbcc4b2 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -41,7 +41,7 @@ def delabBVar : Delab := do @[builtinDelab mvar] def delabMVar : Delab := do let Expr.mvar n ← getExpr | unreachable! - let mvarDecl ← getMVarDecl n + let mvarDecl ← n.getDecl let n := match mvarDecl.userName with | Name.anonymous => n.name.replacePrefix `_uniq `m diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 0dadefb0bf..8f1b41081a 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -243,7 +243,7 @@ where | Name.anonymous => false def mvarName (mvar : Expr) : MetaM Name := - return (← getMVarDecl mvar.mvarId!).userName + return (← mvar.mvarId!.getDecl).userName def containsBadMax : Level → Bool | Level.succ u .. => containsBadMax u diff --git a/tests/lean/1163.lean b/tests/lean/1163.lean index 6b0d134f99..e9279e1b2c 100644 --- a/tests/lean/1163.lean +++ b/tests/lean/1163.lean @@ -6,7 +6,7 @@ macro "obviously1" : tactic => `(exact sorryAx _) theorem result1 : False := by obviously1 elab "obviously2" : tactic => - liftMetaTactic1 (Meta.admit · *> pure none) + liftMetaTactic1 fun mvarId => mvarId.admit *> pure none theorem result2 : False := by obviously2 diff --git a/tests/lean/474.lean b/tests/lean/474.lean index d4d5713c63..763d47d866 100644 --- a/tests/lean/474.lean +++ b/tests/lean/474.lean @@ -4,7 +4,7 @@ open Lean Meta #eval do let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do let m ← mkFreshExprMVar (mkConst ``Nat) - assignExprMVar m.mvarId! y + m.mvarId!.assign y let e := mkApp2 (mkConst ``Nat.add) m y -- goal: construct λ y, e dbg_trace (← ppExpr (← mkLambdaFVars #[y] e)) -- doesn't work: creates let @@ -17,7 +17,7 @@ open Lean Meta #eval withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do let m ← mkFreshExprMVar (mkConst ``Nat) - assignExprMVar m.mvarId! y + m.mvarId!.assign y let e := mkApp2 (mkConst ``Nat.add) m y -- goal: construct λ y, e dbg_trace (← instantiateMVars <| -- doesn't work: contains free variable @@ -31,6 +31,6 @@ open Lean Meta dbg_trace (← ppExpr (← abstract e #[y])) let e ← instantiateMVars <| -- doesn't work: contains free variable mkLambda `y BinderInfo.default (mkConst ``Nat) (← abstract e #[y]) - assignExprMVar m.mvarId! (mkApp2 (mkConst ``Nat.add) y y) + m.mvarId!.assign (mkApp2 (mkConst ``Nat.add) y y) return (e, m) dbg_trace (← ppExpr (← instantiateMVars e)) diff --git a/tests/lean/byCasesMetaM.lean b/tests/lean/byCasesMetaM.lean index b28e8dd5f3..c00ca08bf2 100644 --- a/tests/lean/byCasesMetaM.lean +++ b/tests/lean/byCasesMetaM.lean @@ -7,7 +7,7 @@ open Lean.Meta in def test : MetaM Unit := do let type := (← getConstInfo ``ex).type let mvar ← mkFreshExprMVar type - let (#[p, q, h], mvarId) ← introNP mvar.mvarId! 3 | throwError "unexpected" + let (#[p, q, h], mvarId) ← mvar.mvarId!.introNP 3 | throwError "unexpected" trace[Meta.debug] "{MessageData.ofGoal mvarId}" let (s₁, s₂) ← byCases mvarId (mkFVar p) `hAux trace[Meta.debug] "{MessageData.ofGoal s₁.mvarId}\n------\n{MessageData.ofGoal s₂.mvarId}"