From f65e3ae9859a4288b94b4a9fda93f406244d8dbc Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 3 Jun 2024 16:21:31 +0200 Subject: [PATCH] feat: simp to still work even if one simp arg does not work (#4177) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit this fixes a usability paper cut that just annoyed me. When editing a larger simp proof, I usually want to see the goal state after the simp, and this is what I see while the `simp` command is complete. But then, when I start typing, and necessarily type incomplete lemma names, that error makes `simp` do nothing again and I see the original goal state. In fact, if a prefix of the simp theorem name I am typing is a valid identifier, it jumps even more around. With this PR, using `logException`, I still get the red squiggly lines for the unknown identifer, but `simp` just ignores that argument and still shows me the final goal. Much nicer. I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a warning and gave it the correct `ref`. See it in action here: (in the middle, when you suddenly see the terminal, I am switching lean versions.) https://github.com/leanprover/lean4/assets/148037/8cb3c563-1354-4c2d-bcee-26dfa1005ae0 --- src/Lean/Elab/Tactic/Simp.lean | 101 +++++++++--------- src/Lean/Elab/Util.lean | 3 + src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 5 +- tests/lean/eraseSimp.lean.expected.out | 2 +- .../interactive/plainGoal.lean.expected.out | 10 +- tests/lean/run/simproc1.lean | 2 +- 6 files changed, 62 insertions(+), 61 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index d5e773f0b2..380e084444 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -153,6 +153,7 @@ inductive ResolveSimpIdResult where Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"` If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`), this option only makes sense for `simp_all` or `*` is used. + Try to recover from errors as much as possible so that users keep seeing the current goal. -/ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do if stx.isNone then @@ -171,56 +172,58 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr let mut simprocs := simprocs let mut starArg := false for arg in stx[1].getSepArgs do - if arg.getKind == ``Lean.Parser.Tactic.simpErase then - let fvar ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none - if let some fvar := fvar then - -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet - thms := thms.eraseCore (.fvar fvar.fvarId!) + try -- like withLogging, but compatible with do-notation + if arg.getKind == ``Lean.Parser.Tactic.simpErase then + let fvar? ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none + if let some fvar := fvar? then + -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet + thms := thms.eraseCore (.fvar fvar.fvarId!) + else + let id := arg[1] + if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then + if (← Simp.isSimproc declName) then + simprocs := simprocs.erase declName + else if ctx.config.autoUnfold then + thms := thms.eraseCore (.decl declName) + else + thms ← withRef id <| thms.erase (.decl declName) + else + -- If `id` could not be resolved, we should check whether it is a builtin simproc. + -- before returning error. + let name := id.getId.eraseMacroScopes + if (← Simp.isBuiltinSimproc name) then + simprocs := simprocs.erase name + else + withRef id <| throwUnknownConstant name + else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then + let post := + if arg[0].isNone then + true + else + arg[0][0].getKind == ``Parser.Tactic.simpPost + let inv := !arg[1].isNone + let term := arg[2] + match (← resolveSimpIdTheorem? term) with + | .expr e => + let name ← mkFreshId + thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind + | .simproc declName => + simprocs ← simprocs.add declName post + | .ext (some ext₁) (some ext₂) _ => + thmsArray := thmsArray.push (← ext₁.getTheorems) + simprocs := simprocs.push (← ext₂.getSimprocs) + | .ext (some ext₁) none _ => + thmsArray := thmsArray.push (← ext₁.getTheorems) + | .ext none (some ext₂) _ => + simprocs := simprocs.push (← ext₂.getSimprocs) + | .none => + let name ← mkFreshId + thms ← addSimpTheorem thms (.stx name arg) term post inv + else if arg.getKind == ``Lean.Parser.Tactic.simpStar then + starArg := true else - let id := arg[1] - if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then - if (← Simp.isSimproc declName) then - simprocs := simprocs.erase declName - else if ctx.config.autoUnfold then - thms := thms.eraseCore (.decl declName) - else - thms ← thms.erase (.decl declName) - else - -- If `id` could not be resolved, we should check whether it is a builtin simproc. - -- before returning error. - let name := id.getId.eraseMacroScopes - if (← Simp.isBuiltinSimproc name) then - simprocs := simprocs.erase name - else - throwUnknownConstant name - else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then - let post := - if arg[0].isNone then - true - else - arg[0][0].getKind == ``Parser.Tactic.simpPost - let inv := !arg[1].isNone - let term := arg[2] - match (← resolveSimpIdTheorem? term) with - | .expr e => - let name ← mkFreshId - thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind - | .simproc declName => - simprocs ← simprocs.add declName post - | .ext (some ext₁) (some ext₂) _ => - thmsArray := thmsArray.push (← ext₁.getTheorems) - simprocs := simprocs.push (← ext₂.getSimprocs) - | .ext (some ext₁) none _ => - thmsArray := thmsArray.push (← ext₁.getTheorems) - | .ext none (some ext₂) _ => - simprocs := simprocs.push (← ext₂.getSimprocs) - | .none => - let name ← mkFreshId - thms ← addSimpTheorem thms (.stx name arg) term post inv - else if arg.getKind == ``Lean.Parser.Tactic.simpStar then - starArg := true - else - throwUnsupportedSyntax + throwUnsupportedSyntax + catch ex => logException ex return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg } where isSimproc? (e : Expr) : MetaM (Option Name) := do diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 8cd4b1995c..1314531f7d 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -209,6 +209,9 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [ let name ← id.getName logError m!"internal exception: {name}" +/-- +If `x` throws an exception, catch it and turn it into a log message (using `logException`). +-/ def withLogging [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m] (x : m Unit) : m Unit := do try x catch ex => logException ex diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 91c316e3e2..1acb7354a6 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -221,13 +221,14 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe else d -def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do +def SimpTheorems.erase [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] + (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do unless d.isLemma thmId || match thmId with | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName | _ => false do - throwError "'{thmId.key}' does not have [simp] attribute" + logWarning m!"'{thmId.key}' does not have [simp] attribute" return d.eraseCore thmId private partial def isPerm : Expr → Expr → MetaM Bool diff --git a/tests/lean/eraseSimp.lean.expected.out b/tests/lean/eraseSimp.lean.expected.out index 131ece2459..4d6239f2d4 100644 --- a/tests/lean/eraseSimp.lean.expected.out +++ b/tests/lean/eraseSimp.lean.expected.out @@ -1 +1 @@ -eraseSimp.lean:4:18-4:21: error: 'foo' does not have [simp] attribute +eraseSimp.lean:4:18-4:21: warning: 'foo' does not have [simp] attribute diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out index 91a2fdd633..ee7eee80fc 100644 --- a/tests/lean/interactive/plainGoal.lean.expected.out +++ b/tests/lean/interactive/plainGoal.lean.expected.out @@ -109,16 +109,10 @@ "t a n✝ : Nat\na✝ : t * (a + n✝) = t * a + t * n✝\n⊢ t * (a + n✝) + t = t * a + (t * n✝ + t)"]} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 82, "character": 53}} -{"rendered": - "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```", - "goals": - ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]} +{"rendered": "no goals", "goals": []} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 82, "character": 54}} -{"rendered": - "```lean\ncase nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)\n```", - "goals": - ["case nil\nα : Type ?u\nbs cs : List α\n⊢ [] ++ bs ++ cs = [] ++ (bs ++ cs)"]} +{"rendered": "no goals", "goals": []} {"textDocument": {"uri": "file:///plainGoal.lean"}, "position": {"line": 86, "character": 38}} {"rendered": "no goals", "goals": []} diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean index 90e4a3deb8..653605daa2 100644 --- a/tests/lean/run/simproc1.lean +++ b/tests/lean/run/simproc1.lean @@ -31,7 +31,7 @@ example : x + foo 2 = 12 + x := by example : x + foo 2 = 12 + x := by -- We can use `-` to disable `simproc`s - fail_if_success simp [-reduce_foo] + fail_if_success simp [-reduceFoo] simp_arith example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h