diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 76dab4f54d..d4ecccfa35 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -131,68 +131,85 @@ def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do withInfoContext x (← mkInitialTacticInfo stx) /- -Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define +Important: we must define `evalTactic` before we define the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages, and this is bad when rethrowing the exception at the `catch` block in these methods. We marked these places with a `(*)` in these methods. -/ -private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List (KeyedDeclsAttribute.AttributeEntry Tactic)) : TacticM Unit := do - let rec loop - | [] => throwErrorAt stx "unexpected syntax {indentD stx}" - | evalFn::evalFns => do - try - withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx - catch - | ex@(.error ..) => - match evalFns with - | [] => throw ex -- (*) - | evalFns => s.restore; loop evalFns - | ex@(.internal id _) => +/-- + Auxiliary datastructure for capturing exceptions at `evalTactic`. +-/ +inductive EvalTacticFailure where + | /-- Exceptions ≠ AbortException -/ + exception (ex : Exception) + | /-- + `abort` exceptions are used when exceptions have already been logged at the message Log. + Thus, we save the whole state here to make sure we don't lose them. + -/ + abort (s : SavedState) + +partial def evalTactic (stx : Syntax) : TacticM Unit := + withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with + | .node _ k _ => + if k == nullKind then + -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` + stx.getArgs.forM evalTactic + else do + trace[Elab.step] "{stx}" + let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind + let macros := macroAttribute.getEntries (← getEnv) stx.getKind + if evalFns.isEmpty && macros.isEmpty then + throwErrorAt stx "tactic '{stx.getKind}' has not been implemented" + let s ← Tactic.saveState + expandEval s macros evalFns #[] + | .missing => pure () + | _ => throwError m!"unexpected tactic{indentD stx}" +where + throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do + let exs := failures.filterMap fun | .abort _ => none | .exception ex => some ex + if exs.isEmpty then + if let some (.abort s) := failures.find? fun | .abort _ => true | _ => false then + s.restore + throwAbortTactic + else + throwErrorAt stx "unexpected syntax {indentD stx}" + else if h : 0 < exs.size then + throw exs[0] -- (*) + else + withRef stx do throwErrorWithNestedErrors "tactic failed" exs -- (*) + + @[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → TacticM Unit) := do + match ex with + | .error .. => s.restore; k (failures.push (.exception ex)) + | .internal id _ => if id == unsupportedSyntaxExceptionId then - s.restore; loop evalFns + -- We do not store `unsupportedSyntaxExceptionId`, see throwExs + s.restore; k failures + else if id == abortTacticExceptionId then + let failures := failures.push (.abort (← Tactic.saveState)) + s.restore; k failures else - throw ex - loop tactics + throw ex -- (*) -mutual - - partial def expandTacticMacroFns (s : SavedState) (stx : Syntax) (macros : List (KeyedDeclsAttribute.AttributeEntry Macro)) : TacticM Unit := - let rec loop - | [] => throwErrorAt stx "tactic '{stx.getKind}' has not been implemented" - | m::ms => do + expandEval (s : SavedState) (macros : List _) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit := + match macros with + | [] => eval s evalFns failures + | m :: ms => try withReader ({ · with elaborator := m.declName }) do withTacticInfoContext stx do let stx' ← adaptMacro m.value stx evalTactic stx' - catch ex => - if ms.isEmpty then throw ex -- (*) - s.restore; loop ms - loop macros + catch ex => handleEx s failures ex (expandEval s ms evalFns) - partial def expandTacticMacro (s : SavedState) (stx : Syntax) : TacticM Unit := do - expandTacticMacroFns s stx (macroAttribute.getEntries (← getEnv) stx.getKind) - - partial def evalTacticAux (stx : Syntax) : TacticM Unit := - withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with - | .node _ k _ => - if k == nullKind then - -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]` - stx.getArgs.forM evalTactic - else do - trace[Elab.step] "{stx}" - let s ← Tactic.saveState - match tacticElabAttribute.getEntries (← getEnv) stx.getKind with - | [] => expandTacticMacro s stx - | evalFns => evalTacticUsing s stx evalFns - | .missing => pure () - | _ => throwError m!"unexpected tactic{indentD stx}" - - partial def evalTactic (stx : Syntax) : TacticM Unit := - evalTacticAux stx - -end + eval (s : SavedState) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit := do + match evalFns with + | [] => throwExs failures + | evalFn::evalFns => do + try + withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx + catch ex => handleEx s failures ex (eval s evalFns) def throwNoGoalsToBeSolved : TacticM α := throwError "no goals to be solved" diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index 2d57d64fb0..0a9bd24741 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -37,7 +37,7 @@ "position": {"line": 39, "character": 2}} {"range": {"start": {"line": 39, "character": 2}, "end": {"line": 39, "character": 23}}, - "contents": {"value": "My ultimate tactic ", "kind": "markdown"}} + "contents": {"value": "My way better tactic ", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 46, "character": 7}} {"range": diff --git a/tests/lean/macroElabRulesIssue1.lean b/tests/lean/macroElabRulesIssue1.lean new file mode 100644 index 0000000000..f511da52e6 --- /dev/null +++ b/tests/lean/macroElabRulesIssue1.lean @@ -0,0 +1,16 @@ +import Lean + +open Lean Elab Tactic + +syntax "Foo" (ident <|> num) : tactic + +elab_rules : tactic + | `(tactic| Foo $x:num) => + logInfo "num" + +macro_rules + | `(tactic| Foo $x:ident) => `(tactic| trace "ident") + +example : True := by + Foo x -- should not fail + trivial diff --git a/tests/lean/macroElabRulesIssue1.lean.expected.out b/tests/lean/macroElabRulesIssue1.lean.expected.out new file mode 100644 index 0000000000..08a89d1260 --- /dev/null +++ b/tests/lean/macroElabRulesIssue1.lean.expected.out @@ -0,0 +1 @@ +ident diff --git a/tests/lean/macroElabRulesIssue2.lean b/tests/lean/macroElabRulesIssue2.lean new file mode 100644 index 0000000000..640f98cda8 --- /dev/null +++ b/tests/lean/macroElabRulesIssue2.lean @@ -0,0 +1,22 @@ +import Lean +open Lean Elab + +declare_syntax_cat fixDecl +syntax ident : fixDecl +syntax ident "<" term : fixDecl + +syntax "Fix₁ " fixDecl : tactic + +elab_rules : tactic + | `(tactic| Fix₁ $x:ident) => logInfo "simple" + +elab_rules : tactic + | `(tactic| Fix₁ $x:ident < $bound:term) => + throwError "Failed at elab_rules" + +macro_rules +| `(ℕ) => `(Nat) + +example : ∀ b : ℕ, ∀ a : Nat, a ≥ 2 → a / a = 1 := by + Fix₁ b + Fix₁ a < 2 -- should produce `Failed at elab_rules` diff --git a/tests/lean/macroElabRulesIssue2.lean.expected.out b/tests/lean/macroElabRulesIssue2.lean.expected.out new file mode 100644 index 0000000000..fd21d5fc3c --- /dev/null +++ b/tests/lean/macroElabRulesIssue2.lean.expected.out @@ -0,0 +1 @@ +macroElabRulesIssue2.lean:22:2-22:12: error: Failed at elab_rules