From 4660485ac8c8d0448f345e6f16e265bf9ca067ae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Mar 2022 07:37:45 -0800 Subject: [PATCH] refactor: `collectDeps` => `collectForwardDeps` --- src/Lean/Meta/Tactic/Revert.lean | 2 +- src/Lean/MetavarContext.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Tactic/Revert.lean b/src/Lean/Meta/Tactic/Revert.lean index 4d1cc137e9..944a070f32 100644 --- a/src/Lean/Meta/Tactic/Revert.lean +++ b/src/Lean/Meta/Tactic/Revert.lean @@ -16,7 +16,7 @@ def revert (mvarId : MVarId) (fvarIds : Array FVarId) (preserveOrder : Bool := f if (← getLocalDecl fvarId) |>.isAuxDecl then throwError "failed to revert {mkFVar fvarId}, it is an auxiliary declaration created to represent recursive definitions" let fvars := fvarIds.map mkFVar - match MetavarContext.MkBinding.collectDeps (← getMCtx) (← getLCtx) fvars preserveOrder with + match MetavarContext.MkBinding.collectForwardDeps (← getMCtx) (← getLCtx) fvars preserveOrder with | Except.error _ => throwError "failed to revert variables {fvars}" | Except.ok toRevert => /- We should clear any `auxDecl` in `toRevert` -/ diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index bbba6df822..8b8aa89390 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -791,7 +791,7 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) Note that https://github.com/leanprover/lean/issues/1258 is not an issue in Lean4 because we have changed how we compile recursive definitions. -/ -def collectDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) (preserveOrder : Bool) : Except Exception (Array Expr) := do +def collectForwardDeps (mctx : MetavarContext) (lctx : LocalContext) (toRevert : Array Expr) (preserveOrder : Bool) : Except Exception (Array Expr) := do if toRevert.size == 0 then pure toRevert else @@ -923,14 +923,14 @@ mutual ``` ?n #[y_1, ..., y_m, x_1, ... x_n] := ?m x_1 ... x_n ``` - where `#[y_1, ..., y_m]` is `toRevert` after `collectDeps`. + where `#[y_1, ..., y_m]` is `toRevert` after `collectForwardDeps`. Remark: `newMVarKind != MetavarKind.syntheticOpaque ==> nestedFVars == #[]` -/ let rec cont (nestedFVars : Array Expr) (nestedLCtx : LocalContext) : M (Expr × Array Expr) := do let args ← args.mapM (visit xs) let preserve ← preserveOrder - match collectDeps mctx mvarLCtx toRevert preserve with + match collectForwardDeps mctx mvarLCtx toRevert preserve with | Except.error ex => throw ex | Except.ok toRevert => let newMVarLCtx := reduceLocalContext mvarLCtx toRevert