Emit a different warning type for each case of stuck proof state

kore/src/Kore/Log/Registry.hs

@@ -86,6 +86,9 @@ import Kore.Log.InfoReachability
 import Kore.Log.WarnFunctionWithoutEvaluators
     ( WarnFunctionWithoutEvaluators
     )
+import Kore.Log.WarnStuckProofState
+    ( WarnStuckProofState
+    )
 import Kore.Log.WarnSymbolSMTRepresentation
     ( WarnSymbolSMTRepresentation
     )
@@ -135,6 +138,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @ErrorDecidePredicateUnknown
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation
+    , mk $ Proxy @WarnStuckProofState
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop

kore/src/Kore/Log/WarnStuckProofState.hs

@@ -0,0 +1,49 @@
+{- |
+Copyright   : (c) Runtime Verification, 2019
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnStuckProofState
+    ( WarnStuckProofState (..)
+    , warnStuckProofStateTermsUnifiable
+    , warnStuckProofStateTermsNotUnifiable
+    ) where
+
+import Prelude.Kore
+
+import Log
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+
+{- | @WarnStuckProofState@ is emitted when a proof gets stuck.
+
+The warning message distinguishes for the user the ways that a proof can be stuck.
+
+ -}
+data WarnStuckProofState
+    = TermsUnifiableStuck
+    -- ^ The terms of the left- and right-hand sides do not unify,
+    -- and the left-hand side cannot be rewritten any further.
+    | TermsNotUnifiableStuck
+    -- ^ The left- and right-hand side terms are unifiable, but the left-hand side
+    -- condition does not imply the right-hand side condition.
+    deriving Show
+
+instance Pretty WarnStuckProofState where
+    pretty TermsUnifiableStuck =
+        "The proof has reached the final configuration, but the claimed implication is not valid."
+    pretty TermsNotUnifiableStuck =
+        "The claim cannot be rewritten further, and the claimed implication is not valid."
+
+instance Entry WarnStuckProofState where
+    entrySeverity _ = Warning
+    helpDoc _ = "distinguish the ways a proof can become stuck"
+
+warnStuckProofStateTermsUnifiable :: MonadLog log => log ()
+warnStuckProofStateTermsUnifiable = logEntry TermsUnifiableStuck
+
+warnStuckProofStateTermsNotUnifiable :: MonadLog log => log ()
+warnStuckProofStateTermsNotUnifiable = logEntry TermsNotUnifiableStuck

kore/src/Kore/Strategies/Goal.hs

@@ -98,6 +98,10 @@ import Kore.Internal.TermLike
     , termLikeSort
     )
 import Kore.Log.InfoReachability
+import Kore.Log.WarnStuckProofState
+    ( warnStuckProofStateTermsNotUnifiable
+    , warnStuckProofStateTermsUnifiable
+    )
 import Kore.Rewriting.RewritingVariable
 import Kore.Step.Result
     ( Result (..)
@@ -523,15 +527,21 @@ transitionRule claims axiomGroups = transitionRuleWorker
     transitionRuleWorker CheckImplication (Goal goal) = do
         result <- checkImplication goal
         case result of
-            NotImpliedStuck a -> pure (GoalStuck a)
+            NotImpliedStuck a -> do
+                warnStuckProofStateTermsUnifiable
+                pure (GoalStuck a)
             Implied -> pure Proven
             NotImplied a -> pure (Goal a)
     transitionRuleWorker CheckImplication (GoalRemainder goal) = do
         result <- checkImplication goal
         case result of
-            NotImpliedStuck a -> pure (GoalStuck a)
+            NotImpliedStuck a -> do
+                warnStuckProofStateTermsUnifiable
+                pure (GoalStuck a)
             Implied -> pure Proven
-            NotImplied a -> pure (GoalRemainder a)
+            NotImplied a -> do
+                warnStuckProofStateTermsNotUnifiable
+                pure (GoalRemainder a)
 
     transitionRuleWorker TriviallyValid (Goal goal)
       | isTriviallyValid goal =