Profiles rewrite (#2690)

* Rewriting some logging-related functions

* Format with fourmolu

* removing comment

Co-authored-by: github-actions <github-actions@github.com>

Author: emarzion

kore/src/Kore/Log/InfoReachability.hs

@@ -8,7 +8,7 @@ module Kore.Log.InfoReachability (
 ) where
 
 import Kore.Reachability.Prim
-import Log
+import qualified Log
 import Prelude.Kore
 import Pretty (
     Doc,
@@ -24,8 +24,8 @@ instance Pretty InfoReachability where
     pretty InfoReachability{prim} =
         (Pretty.hsep . catMaybes) [primDoc prim]
 
-instance Entry InfoReachability where
-    entrySeverity _ = Info
+instance Log.Entry InfoReachability where
+    entrySeverity _ = Log.Info
     contextDoc InfoReachability{prim} = (<+>) "while" <$> primDoc prim
     helpDoc _ = "log reachability proof steps"
 
@@ -37,10 +37,10 @@ primDoc ApplyAxioms = Just "applying axioms"
 primDoc _ = Nothing
 
 whileReachability ::
-    MonadLog log =>
+    Log.MonadLog log =>
     Prim ->
     log a ->
     log a
-whileReachability prim
-    | Just _ <- primDoc prim = logWhile InfoReachability{prim}
-    | otherwise = id
+whileReachability prim log
+    | Just _ <- primDoc prim = Log.logWhile InfoReachability{prim} log
+    | otherwise = log

kore/src/Kore/Reachability/Prove.hs

@@ -575,34 +575,35 @@ withDebugClaimState ::
     MonadLog monad =>
     CommonTransitionRule monad ->
     CommonTransitionRule monad
-withDebugClaimState transitionFunc =
-    \transition state ->
-        Transition.orElse
-            ( debugClaimStateBracket
-                state
-                transition
-                (transitionFunc transition state)
-            )
-            ( debugClaimStateFinal
-                state
-                transition
-            )
+withDebugClaimState transitionFunc transition state =
+    Transition.orElse
+        ( debugClaimStateBracket
+            state
+            transition
+            (transitionFunc transition state)
+        )
+        ( debugClaimStateFinal
+            state
+            transition
+        )
 
 withDebugProven ::
     forall monad.
     MonadLog monad =>
     CommonTransitionRule monad ->
     CommonTransitionRule monad
 withDebugProven rule prim state =
-    rule prim state >>= debugProven
-  where
-    debugProven state'
-        | ClaimState.Proven <- state'
-          , Just claim <- extractUnproven state =
-            do
-                Log.logEntry DebugProven{claim}
-                pure state'
-        | otherwise = pure state'
+    do
+        state' <- rule prim state
+        case state' of
+            ClaimState.Proven ->
+                case extractUnproven state of
+                    Just claim ->
+                        do
+                            Log.logEntry DebugProven{claim}
+                            pure state'
+                    _ -> pure state'
+            _ -> pure state'
 
 withConfiguration ::
     MonadCatch monad =>