Fail if nonterminal Aesop made no progress

fixes #85

Aesop/Search/Expansion/Norm.lean

@@ -312,8 +312,9 @@ def normUnfold (goal : MVarId) (goalMVars : HashSet MVarId) :
 
 inductive NormSeqResult where
   | proved (script? : Except DisplayRuleName UnstructuredScript)
-  | unproved (goal : MVarId)
+  | changed (goal : MVarId)
       (script? : Except DisplayRuleName UnstructuredScript)
+  | unchanged (script? : Except DisplayRuleName UnstructuredScript)
 
 abbrev NormStep :=
   MVarId → Array (IndexMatchResult NormRule) →
@@ -329,6 +330,7 @@ def runNormSteps (goal : MVarId) (steps : Array NormStep)
   let mut script? : Except DisplayRuleName UnstructuredScript := .ok #[]
   let mut preSimpRules := ∅
   let mut postSimpRules := ∅
+  let mut anySuccess := false
   while iteration < maxIterations do
     if step.val == 0 then
       let rules ← ProfileT.liftBase (selectNormRules ctx.ruleSet goal)
@@ -338,6 +340,7 @@ def runNormSteps (goal : MVarId) (steps : Array NormStep)
       postSimpRules := postSimpRules'
     match ← steps[step] goal preSimpRules postSimpRules with
     | .succeeded newGoal scriptStep? =>
+      anySuccess := true
       goal := newGoal
       script? := return (← script?).push (← scriptStep?)
       iteration := iteration + 1
@@ -353,7 +356,10 @@ def runNormSteps (goal : MVarId) (steps : Array NormStep)
       if h : step.val + 1 < steps.size then
         step := ⟨step.val + 1, h⟩
       else
-        return .unproved goal script?
+        if anySuccess then
+          return .changed goal script?
+        else
+          return .unchanged script?
   throwError "aesop: exceeded maximum number of normalisation iterations ({maxIterations}). This means normalisation probably got stuck in an infinite loop."
 
 def NormStep.runPreSimpRules (mvars : UnorderedArraySet MVarId) : NormStep
@@ -393,23 +399,27 @@ partial def normalizeGoalMVar (goal : MVarId)
 def normalizeGoalIfNecessary (gref : GoalRef) [Aesop.Queue Q] :
     SearchM Q Bool := do
   let g ← gref.get
+  let preGoal := g.preNormGoal
   if ← g.isRoot then
     -- For the root goal, we skip normalization.
     let rootState ← getRootMetaState
     gref.modify λ g =>
-      g.setNormalizationState (.normal g.preNormGoal rootState (.ok #[]))
+      g.setNormalizationState (.normal preGoal rootState (.ok #[]))
     return false
   match g.normalizationState with
   | .provenByNormalization .. => return true
   | .normal .. => return false
   | .notNormal => pure ()
   let (normResult, postState) ← controlAt MetaM λ runInBase => do
     (← gref.get).runMetaMInParentState do
-      runInBase $ normalizeGoalMVar g.preNormGoal g.mvars
+      runInBase $ normalizeGoalMVar preGoal g.mvars
   match normResult with
-  | .unproved postGoal script? =>
+  | .changed postGoal script? =>
     gref.modify (·.setNormalizationState (.normal postGoal postState script?))
     return false
+  | .unchanged script? =>
+    gref.modify (·.setNormalizationState (.normal preGoal postState script?))
+    return false
   | .proved script? =>
     gref.modify
       (·.setNormalizationState (.provenByNormalization postState script?))

Aesop/Search/Main.lean

@@ -182,6 +182,27 @@ def finishIfProven : SearchM Q Bool := do
   traceTree
   return true
 
+def treeHasNonPreprocessingRapp : TreeM Bool := do
+  let resultRef ← IO.mkRef false
+  preTraverseDown
+    (λ gref => do
+      let g ← gref.get
+      if let some postGoal := g.normalizationState.normalizedGoal? then
+        if postGoal != g.preNormGoal then
+          resultRef.set true
+          return false
+      return true)
+    (λ rref => do
+      if (← rref.get).appliedRule.name != preprocessRule.name then
+        resultRef.set true
+        return false
+      else
+        return true
+      )
+    (λ _ => return true)
+    (.mvarCluster (← get).root)
+  resultRef.get
+
 -- When we hit a non-fatal error (i.e. the search terminates without a proof
 -- because the root goal is unprovable or because we hit a search limit), we
 -- usually:
@@ -198,9 +219,11 @@ def handleNonfatalError (err : MessageData) : SearchM Q (Array MVarId) := do
   let opts := (← read).options
   if opts.terminal then
     throwTacticEx `aesop (← getRootMVarId) err
+  expandSafePrefix
+  if ! (← treeHasNonPreprocessingRapp) then
+    throwTacticEx `aesop (← getRootMVarId) "made no progress"
   if opts.warnOnNonterminal then
     logWarning m!"aesop: {err}"
-  expandSafePrefix
   let goals ← extractSafePrefix
   aesop_trace[proof] do
     match ← getProof? with

Aesop/Tree/Data.lean

@@ -271,6 +271,10 @@ def isProvenByNormalization : NormalizationState → Bool
   | normal .. => false
   | provenByNormalization .. => true
 
+def normalizedGoal? : NormalizationState → Option MVarId
+  | notNormal .. | provenByNormalization .. => none
+  | normal (postGoal := g) .. => g
+
 end NormalizationState
 
 

tests/NoProgress.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2023 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+
+import Aesop
+
+set_option aesop.check.all true
+
+def T := True
+
+example : T := by
+  aesop
+
+@[aesop norm simp]
+def F := False
+
+example : F := by
+  aesop
+
+def F' := False
+
+@[aesop safe apply]
+theorem F'_def : False → F' := id
+
+example : F' := by
+  aesop

tests/NoProgress.lean.expected

@@ -0,0 +1,8 @@
+tests/NoProgress.lean:14:2: error: tactic 'aesop' failed, made no progress
+⊢ T
+tests/NoProgress.lean:20:2: warning: aesop: failed to prove the goal after exhaustive search.
+tests/NoProgress.lean:19:15: error: unsolved goals
+⊢ False
+tests/NoProgress.lean:28:2: warning: aesop: failed to prove the goal after exhaustive search.
+tests/NoProgress.lean:27:16: error: unsolved goals
+⊢ False