diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean index 6ff84fc4da..f1e49c6829 100644 --- a/src/Lean/Elab/Exception.lean +++ b/src/Lean/Elab/Exception.lean @@ -12,6 +12,7 @@ builtin_initialize postponeExceptionId : InternalExceptionId ← registerInterna builtin_initialize unsupportedSyntaxExceptionId : InternalExceptionId ← registerInternalExceptionId `unsupportedSyntax builtin_initialize abortCommandExceptionId : InternalExceptionId ← registerInternalExceptionId `abortCommandElab builtin_initialize abortTermExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTermElab +builtin_initialize abortTacticExceptionId : InternalExceptionId ← registerInternalExceptionId `abortTactic builtin_initialize autoBoundImplicitExceptionId : InternalExceptionId ← registerInternalExceptionId `autoBoundImplicit def throwPostpone [MonadExceptOf Exception m] : m α := @@ -46,8 +47,17 @@ def throwAbortCommand {α m} [MonadExcept Exception m] : m α := def throwAbortTerm {α m} [MonadExcept Exception m] : m α := throw <| Exception.internal abortTermExceptionId +-- Throw exception to abort evaluation of the current tactic without producing any error message +def throwAbortTactic {α m} [MonadExcept Exception m] : m α := + throw <| Exception.internal abortTacticExceptionId + +def isAbortTacticException (ex : Exception) : Bool := + match ex with + | Exception.internal id .. => id == abortTacticExceptionId + | _ => false + def isAbortExceptionId (id : InternalExceptionId) : Bool := - id == abortCommandExceptionId || id == abortTermExceptionId + id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message := let pos := fileMap.toPosition pos diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 7c07cff814..d52ce05fd9 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -193,26 +193,14 @@ private def getSomeSynthethicMVarsRef : TermElabM Syntax := do mutual - partial def liftTacticElabM {α} (mvarId : MVarId) (x : TacticM α) : TermElabM α := - withMVarContext mvarId do - let savedSyntheticMVars := (← get).syntheticMVars - modify fun s => { s with syntheticMVars := [] } - try - let a ← x.run' { main := mvarId } { goals := [mvarId] } - synthesizeSyntheticMVars (mayPostpone := false) - pure a - finally - modify fun s => { s with syntheticMVars := savedSyntheticMVars } - partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do /- Recall, `tacticCode` is the whole `by ...` expression. -/ let byTk := tacticCode[0] let code := tacticCode[1] modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId } - let remainingGoals ← withInfoHole mvarId <| - liftTacticElabM mvarId do - withTacticInfoContext tacticCode (evalTactic code) - getUnsolvedGoals + let remainingGoals ← withInfoHole mvarId <| Tactic.run mvarId do + withTacticInfoContext tacticCode (evalTactic code) + synthesizeSyntheticMVars (mayPostpone := false) unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals /-- Try to synthesize the given pending synthetic metavariable. -/ diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index a5fa4501af..f4ad78301c 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -41,6 +41,47 @@ structure SavedState where abbrev TacticM := ReaderT Context $ StateRefT State TermElabM abbrev Tactic := Syntax → TacticM Unit +def getGoals : TacticM (List MVarId) := + return (← get).goals + +def setGoals (mvarIds : List MVarId) : TacticM Unit := + modify fun s => { s with goals := mvarIds } + +def pruneSolvedGoals : TacticM Unit := do + let gs ← getGoals + let gs ← gs.filterM fun g => not <$> isExprMVarAssigned g + setGoals gs + +def getUnsolvedGoals : TacticM (List MVarId) := do + pruneSolvedGoals + getGoals + +@[inline] private def TacticM.runCore (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) := + x ctx |>.run s + +@[inline] private def TacticM.runCore' (x : TacticM α) (ctx : Context) (s : State) : TermElabM α := + Prod.fst <$> x.runCore ctx s + +def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) := + withMVarContext mvarId do + let savedSyntheticMVars := (← get).syntheticMVars + modify fun s => { s with syntheticMVars := [] } + let aux : TacticM (List MVarId) := + /- Important: the following `try` does not backtrack the state. + This is intentional because we don't want to backtrack the error messages when we catch the "abort internal exception" + We must define `run` here because we define `MonadExcept` instance for `TacticM` -/ + try + x; getUnsolvedGoals + catch ex => + if isAbortTacticException ex then + getUnsolvedGoals + else + throw ex + try + aux.runCore' { main := mvarId } { goals := [mvarId] } + finally + modify fun s => { s with syntheticMVars := savedSyntheticMVars } + protected def saveState : TacticM SavedState := return { term := (← Term.saveState), tactic := (← get) } @@ -48,24 +89,6 @@ def SavedState.restore (b : SavedState) : TacticM Unit := do b.term.restore set b.tactic -instance : MonadBacktrack SavedState TacticM where - saveState := Tactic.saveState - restoreState b := b.restore - -@[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do - let b ← saveState - try x catch ex => b.restore; h ex - -instance : MonadExcept Exception TacticM where - throw := throw - tryCatch := Tactic.tryCatch - -@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do - try x catch _ => y - -instance {α} : OrElse (TacticM α) where - orElse := Tactic.orElse - protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Term.Context).currMacroScope protected def getMainModule : TacticM Name := do pure (← getEnv).mainModule @@ -74,6 +97,13 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) := @[builtinInit mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic +/- +Important: we must define `evalTacticUsing` and `expandTacticMacroFns` 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 Tactic) : TacticM Unit := do let rec loop : List Tactic → TacticM Unit | [] => throwErrorAt stx "unexpected syntax {indentD stx}" @@ -83,7 +113,7 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact catch | ex@(Exception.error _ _) => match evalFns with - | [] => throw ex + | [] => throw ex -- (*) | evalFns => s.restore; loop evalFns | ex@(Exception.internal id _) => if id == unsupportedSyntaxExceptionId then @@ -92,9 +122,6 @@ private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tact throw ex loop tactics -def getGoals : TacticM (List MVarId) := - return (← get).goals - def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info := return Info.ofTacticInfo { mctxBefore := mctxBefore @@ -120,7 +147,7 @@ mutual let stx' ← adaptMacro m stx evalTactic stx' catch ex => - if ms.isEmpty then throw ex + if ms.isEmpty then throw ex -- (*) loop ms loop macros @@ -138,7 +165,7 @@ mutual stx.getArgs.forM evalTactic else do trace[Elab.step] "{stx}" - let s ← saveState + let s ← Tactic.saveState let table := (tacticElabAttribute.ext.getState (← getEnv)).table let k := stx.getKind match table.find? k with @@ -151,6 +178,24 @@ mutual end +instance : MonadBacktrack SavedState TacticM where + saveState := Tactic.saveState + restoreState b := b.restore + +@[inline] protected def tryCatch {α} (x : TacticM α) (h : Exception → TacticM α) : TacticM α := do + let b ← saveState + try x catch ex => b.restore; h ex + +instance : MonadExcept Exception TacticM where + throw := throw + tryCatch := Tactic.tryCatch + +@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do + try x catch _ => y + +instance {α} : OrElse (TacticM α) where + orElse := Tactic.orElse + /- Save the current tactic state for a token `stx`. This method is a no-op if `stx` has no position information. @@ -171,9 +216,6 @@ def adaptExpander (exp : Syntax → TacticM Syntax) : Tactic := fun stx => do let stx' ← exp stx withMacroExpansion stx stx' $ evalTactic stx' -def setGoals (mvarIds : List MVarId) : TacticM Unit := - modify fun s => { s with goals := mvarIds } - def appendGoals (mvarIds : List MVarId) : TacticM Unit := modify fun s => { s with goals := s.goals ++ mvarIds } @@ -184,15 +226,6 @@ def replaceMainGoal (mvarIds : List MVarId) : TacticM Unit := do let (mvarId :: mvarIds') ← getGoals | throwNoGoalsToBeSolved modify fun s => { s with goals := mvarIds ++ mvarIds' } -def pruneSolvedGoals : TacticM Unit := do - let gs ← getGoals - let gs ← gs.filterM fun g => not <$> isExprMVarAssigned g - setGoals gs - -def getUnsolvedGoals : TacticM (List MVarId) := do - pruneSolvedGoals - getGoals - /-- Return the first goal. -/ def getMainGoal : TacticM MVarId := do loop (← getGoals) @@ -601,10 +634,4 @@ where builtin_initialize registerTraceClass `Elab.tactic -@[inline] def TacticM.run (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) := - x ctx |>.run s - -@[inline] def TacticM.run' (x : TacticM α) (ctx : Context) (s : State) : TermElabM α := - Prod.fst <$> x.run ctx s - end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 7368b0cddc..4739aa2d8c 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -33,14 +33,21 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo return e /- Try to close main goal using `x target`, where `target` is the type of the main goal. -/ -def closeMainGoalUsing (x : Expr → TacticM Expr) : TacticM Unit := +def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit := withMainContext do - closeMainGoal (← x (← getMainTarget)) + closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget)) + +private def logUnassignedAndAbort (mvarIds : Array MVarId) : TacticM Unit := do + if (← Term.logUnassignedUsingErrorInfos mvarIds) then + throwAbortTactic @[builtinTactic «exact»] def evalExact : Tactic := fun stx => match stx with - | `(tactic| exact $e) => closeMainGoalUsing (fun type => elabTermEnsuringType e type) - | _ => throwUnsupportedSyntax + | `(tactic| exact $e) => closeMainGoalUsing (checkUnassigned := false) fun type => do + let r ← elabTermEnsuringType e type + logUnassignedAndAbort (← getMVars r) + return r + | _ => throwUnsupportedSyntax def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do let val ← elabTermEnsuringType stx expectedType? @@ -53,7 +60,7 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : else let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural - discard <| Term.logUnassignedUsingErrorInfos naturalMVarIds + logUnassignedAndAbort naturalMVarIds pure syntheticMVarIds.toList tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds pure (val, newMVarIds) diff --git a/tests/lean/exactErrorPos.lean b/tests/lean/exactErrorPos.lean new file mode 100644 index 0000000000..0a6da62fb9 --- /dev/null +++ b/tests/lean/exactErrorPos.lean @@ -0,0 +1,19 @@ +set_option pp.rawOnError true + +theorem ex1 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by + exact h1 _ _ + +theorem ex2 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by + refine h1 _ _ + +theorem ex3 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by + first | exact h1 _ _ | apply h1 + assumption + +theorem ex4 (f : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) : f x = x := by + first | refine h1 _ _ | apply h1 + assumption + +theorem ex5 (f g : Nat → Nat) (x : Nat) (h1 : (x : Nat) → x > 0 → f x = x) (h2 : x > 0) (h3 : g x = x) : f x = x := by + first | apply h3 | apply h1 + assumption diff --git a/tests/lean/exactErrorPos.lean.expected.out b/tests/lean/exactErrorPos.lean.expected.out new file mode 100644 index 0000000000..29be7d9834 --- /dev/null +++ b/tests/lean/exactErrorPos.lean.expected.out @@ -0,0 +1,26 @@ +exactErrorPos.lean:4:13-4:14: error: don't know how to synthesize placeholder +context: +f : Nat → Nat +x : Nat +h1 : ∀ (x : Nat), x > 0 → f x = x +h2 : x > 0 +⊢ x > 0 +exactErrorPos.lean:3:99-4:14: error: unsolved goals +f : Nat → Nat +x : Nat +h1 : ∀ (x : Nat), x > 0 → f x = x +h2 : x > 0 +⊢ f x = x +exactErrorPos.lean:7:14-7:15: error: don't know how to synthesize placeholder +context: +f : Nat → Nat +x : Nat +h1 : ∀ (x : Nat), x > 0 → f x = x +h2 : x > 0 +⊢ x > 0 +exactErrorPos.lean:6:99-7:15: error: unsolved goals +f : Nat → Nat +x : Nat +h1 : ∀ (x : Nat), x > 0 → f x = x +h2 : x > 0 +⊢ f x = x