Revert "Add oneLineJson to all log entries"

This reverts commit 339ec7a.

Author: geo2a

kore/src/Kore/Equation/DebugEquation.hs

@@ -28,7 +28,6 @@ import Control.Error (
     ExceptT,
     withExceptT,
  )
-import Data.Aeson qualified as JSON
 import Data.Text (
     Text,
  )
@@ -60,7 +59,13 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import Kore.Unparser (Unparse (..))
-import Log
+import Log (
+    Entry (..),
+    MonadLog,
+    Severity (..),
+    logEntry,
+    logWhile,
+ )
 import Prelude.Kore
 import Pretty (Pretty (..))
 import Pretty qualified
@@ -271,7 +276,6 @@ instance Entry DebugAttemptEquation where
             (srcLoc equation)
     oneLineDoc (DebugAttemptEquationResult _ (Left _)) = "equation is not applicable"
     oneLineDoc (DebugAttemptEquationResult _ (Right _)) = "equation is applicable"
-
     oneLineJson = \case
         entry@DebugAttemptEquation{} -> JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
         DebugAttemptEquationResult equation (Right _) ->
@@ -363,8 +367,6 @@ instance Entry DebugApplyEquation where
                 _
             ) =
             pretty sourceLocation
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log equation application successes"
 
 {- | Log when an 'Equation' is actually applied.

kore/src/Kore/Log/DebugAppliedRewriteRules.hs

@@ -13,7 +13,6 @@ module Kore.Log.DebugAppliedRewriteRules (
     debugAppliedLabeledRewriteRule,
 ) where
 
-import Data.Aeson qualified as JSON
 import Data.Text (Text)
 import Kore.Attribute.Axiom (
     SourceLocation,
@@ -61,11 +60,8 @@ instance Pretty DebugAppliedRewriteRules where
 instance Entry DebugAppliedRewriteRules where
     entrySeverity _ = Debug
     helpDoc _ = "log applied rewrite rules"
-
     oneLineDoc DebugAppliedRewriteRules{appliedRewriteRules} =
         Pretty.hsep $ pretty <$> appliedRewriteRules
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
 
 debugAppliedRewriteRules ::
     MonadLog log =>
@@ -110,8 +106,6 @@ instance Entry DebugAppliedLabeledRewriteRule where
     entrySeverity _ = Debug
     helpDoc _ = "log applied rewrite rule with label"
     oneLineDoc DebugAppliedLabeledRewriteRule{sourceLocation} = pretty sourceLocation
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
 
 debugAppliedLabeledRewriteRule ::
     MonadLog log =>

kore/src/Kore/Log/DebugAttemptUnification.hs

@@ -10,7 +10,6 @@ module Kore.Log.DebugAttemptUnification (
     debugAttemptUnification,
 ) where
 
-import Data.Aeson qualified as JSON
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
 import Kore.Internal.TermLike (
@@ -39,8 +38,6 @@ instance Entry DebugAttemptUnification where
     entrySeverity _ = Debug
     contextDoc _ = Just "while attempting unification"
     oneLineDoc _ = "DebugAttemptUnification"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log unification attempts"
 
 instance Pretty DebugAttemptUnification where

kore/src/Kore/Log/DebugAttemptedRewriteRules.hs

@@ -11,7 +11,6 @@ module Kore.Log.DebugAttemptedRewriteRules (
     debugAttemptedRewriteRule,
 ) where
 
-import Data.Aeson qualified as JSON
 import Data.Text (Text)
 import Kore.Attribute.Axiom (
     SourceLocation,
@@ -57,8 +56,6 @@ instance Pretty DebugAttemptedRewriteRules where
 instance Entry DebugAttemptedRewriteRules where
     entrySeverity _ = Debug
     helpDoc _ = "log attempted rewrite rules"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     oneLineDoc DebugAttemptedRewriteRules{attemptedRewriteRule} =
         pretty attemptedRewriteRule
 

kore/src/Kore/Log/DebugBeginClaim.hs

@@ -10,7 +10,6 @@ module Kore.Log.DebugBeginClaim (
     debugBeginClaim,
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Attribute.SourceLocation (
     SourceLocation,
  )
@@ -36,8 +35,6 @@ instance Entry DebugBeginClaim where
     helpDoc _ = "log starting claims"
     oneLineDoc DebugBeginClaim{claim} =
         pretty @SourceLocation $ from claim
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
 
 debugBeginClaim ::
     MonadLog log =>

kore/src/Kore/Log/DebugCreatedSubstitution.hs

@@ -10,7 +10,6 @@ module Kore.Log.DebugCreatedSubstitution (
     debugCreatedSubstitution,
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Internal.Predicate qualified as Predicate
 import Kore.Internal.Substitution (Substitution)
 import Kore.Internal.Substitution qualified as Substitution
@@ -48,8 +47,6 @@ instance Entry DebugCreatedSubstitution where
             . layoutPrettyUnbounded
             . Pretty.group
             . pretty
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log every substitution created when applying semantic rules"
 
 debugCreatedSubstitution ::

kore/src/Kore/Log/DebugEvaluateCondition.hs

@@ -11,7 +11,6 @@ module Kore.Log.DebugEvaluateCondition (
     debugEvaluateConditionResult,
 ) where
 
-import Data.Aeson qualified as JSON
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
 import Kore.Internal.Predicate (
@@ -62,8 +61,6 @@ instance Entry DebugEvaluateCondition where
     contextDoc _ = Just "while evaluating predicate"
     oneLineDoc (DebugEvaluateCondition _) = "DebugEvaluateCondition _"
     oneLineDoc result = pretty (show result)
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log every predicate evaluated by the SMT solver"
 
 instance SQL.Table DebugEvaluateCondition

kore/src/Kore/Log/DebugProven.hs

@@ -9,7 +9,6 @@ module Kore.Log.DebugProven (
     DebugProven (..),
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Attribute.SourceLocation (SourceLocation)
 import Kore.Reachability.SomeClaim (
     SomeClaim (..),
@@ -31,6 +30,4 @@ instance Pretty DebugProven where
 instance Entry DebugProven where
     entrySeverity _ = Debug
     oneLineDoc DebugProven{claim} = pretty @SourceLocation $ from claim
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log proven claims"

kore/src/Kore/Log/DebugRetrySolverQuery.hs

@@ -10,7 +10,6 @@ module Kore.Log.DebugRetrySolverQuery (
     debugRetrySolverQuery,
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Internal.Predicate (
     Predicate,
  )
@@ -49,8 +48,6 @@ instance Pretty DebugRetrySolverQuery where
 instance Entry DebugRetrySolverQuery where
     entrySeverity _ = Debug
     oneLineDoc _ = "DebugRetrySolverQuery"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ =
         "warning raised when the solver failed to decide\
         \ the satisfiability of a formula, indicating that\

kore/src/Kore/Log/DebugRewriteTrace.hs

@@ -17,7 +17,6 @@ module Kore.Log.DebugRewriteTrace (
     rewriteTraceLogger,
 ) where
 
-import Data.Aeson qualified as JSON
 import Data.ByteString (
     ByteString,
  )
@@ -181,33 +180,21 @@ instance Pretty DebugRewriteTrace where
 instance Entry DebugInitialClaim where
     entrySeverity _ = Debug
     oneLineDoc (DebugInitialClaim uniqueId _) = "Initial claim " <> maybe mempty pretty (getUniqueId uniqueId)
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
-
     helpDoc _ = "log every claim before proving it"
 
 instance Entry DebugInitialPattern where
     entrySeverity _ = Debug
     oneLineDoc (DebugInitialPattern _) = "Initial pattern"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
-
     helpDoc _ = "log initial pattern before rewriting"
 
 instance Entry DebugFinalPatterns where
     entrySeverity _ = Debug
     oneLineDoc (DebugFinalPatterns _) = "Final patterns"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
-
     helpDoc _ = "log final patterns after rewriting"
 
 instance Entry DebugRewriteTrace where
     entrySeverity _ = Debug
     oneLineDoc DebugRewriteTrace{} = "Rewrite trace"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
-
     helpDoc _ = "log rewrite substitutions"
 
 unparseOneLine :: Unparse p => p -> Text

kore/src/Kore/Log/DebugSolver.hs

@@ -16,7 +16,6 @@ module Kore.Log.DebugSolver (
     solverTranscriptLogger,
 ) where
 
-import Data.Aeson qualified as JSON
 import Data.Default
 import Data.Text (
     Text,
@@ -28,9 +27,7 @@ import Log (
     LogAction (..),
     Severity (Debug),
     SomeEntry (..),
-    entryTypeText,
     logWith,
-    toEntry,
  )
 import Options.Applicative (
     Parser,
@@ -68,15 +65,11 @@ instance Pretty DebugSolverRecv where
 instance Entry DebugSolverSend where
     entrySeverity _ = Debug
     oneLineDoc _ = "DebugSolverSend"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log commands sent to SMT solver"
 
 instance Entry DebugSolverRecv where
     entrySeverity _ = Debug
     oneLineDoc _ = "DebugSolverRecv"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log responses received from SMT solver"
 
 logDebugSolverSendWith ::

kore/src/Kore/Log/DebugSubstitutionSimplifier.hs

@@ -11,7 +11,6 @@ module Kore.Log.DebugSubstitutionSimplifier (
     debugSubstitutionSimplifierResult,
 ) where
 
-import Data.Aeson qualified as JSON
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
 import Log
@@ -39,8 +38,6 @@ instance Entry DebugSubstitutionSimplifier where
     entrySeverity _ = Debug
     contextDoc _ = Just "while simplifying substitution"
     oneLineDoc = pretty . show
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "log non-\\bottom results when normalizing unification solutions"
 
 instance SQL.Table DebugSubstitutionSimplifier

kore/src/Kore/Log/DebugTransition.hs

@@ -12,7 +12,6 @@ module Kore.Log.DebugTransition (
     debugFinalTransition,
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Attribute.SourceLocation (
     SourceLocation,
  )
@@ -110,8 +109,6 @@ instance Entry DebugTransition where
     oneLineDoc
         (DebugBeforeTransition BeforeTransition{transition}) =
             "before " <> pretty transition
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
 
 debugBeforeTransition ::
     MonadLog log =>

kore/src/Kore/Log/DebugUnification.hs

@@ -15,7 +15,6 @@ module Kore.Log.DebugUnification (
     whileDebugUnification,
 ) where
 
-import Data.Aeson qualified as JSON
 import Kore.Internal.Pattern as Pattern
 import Kore.Internal.TermLike as TermLike
 import Kore.Unparser
@@ -42,8 +41,6 @@ instance Entry DebugUnification where
     oneLineDoc (DebugUnificationWhile _) = "DebugUnificationWhile"
     oneLineDoc (DebugUnificationSolved _) = "DebugUnificationSolved"
     oneLineDoc (DebugUnificationUnsolved _) = "DebugUnificationUnsolved"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
 
 -- | @WhileDebugUnification@ encloses the context of unification log entries.
 data WhileDebugUnification = WhileDebugUnification {term1, term2 :: TermLike VariableName}

kore/src/Kore/Log/DebugUnifyBottom.hs

@@ -12,7 +12,6 @@ module Kore.Log.DebugUnifyBottom (
     debugUnifyBottomAndReturnBottom,
 ) where
 
-import Data.Aeson qualified as JSON
 import Data.Text (
     Text,
  )
@@ -27,9 +26,7 @@ import Log (
     Entry (..),
     MonadLog (..),
     Severity (..),
-    entryTypeText,
     logEntry,
-    toEntry,
  )
 import Logic (
     MonadLogic,
@@ -62,8 +59,6 @@ instance Pretty DebugUnifyBottom where
 instance Entry DebugUnifyBottom where
     entrySeverity _ = Debug
     oneLineDoc _ = "DebugUnifyBottom"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= entryTypeText (toEntry entry)]
     helpDoc _ = "log failed unification"
 
 mkDebugUnifyBottom ::

kore/src/Kore/Log/DecidePredicateUnknown.hs

@@ -20,7 +20,6 @@ import Control.Exception (
     Exception (..),
     throw,
  )
-import Data.Aeson qualified as JSON
 import Data.Text (Text)
 import Debug
 import Kore.Attribute.SourceLocation (
@@ -103,8 +102,6 @@ instance Entry DecidePredicateUnknown where
         prettyHsLoc Loc{loc_module, loc_start = (row, col)} =
             Pretty.pretty loc_module <> ":" <> Pretty.pretty row <> ":" <> Pretty.pretty col
     oneLineDoc _ = "DecidePredicateUnknown"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ =
         "error or a warning when the solver cannot decide the satisfiability of a formula"
 

kore/src/Kore/Log/ErrorBottomTotalFunction.hs

@@ -28,7 +28,6 @@ import Pretty (
  )
 import Pretty qualified
 import SQL qualified
-import Data.Aeson qualified as JSON
 
 newtype ErrorBottomTotalFunction = ErrorBottomTotalFunction
     { term :: TermLike VariableName
@@ -56,8 +55,6 @@ instance Exception ErrorBottomTotalFunction where
 instance Entry ErrorBottomTotalFunction where
     entrySeverity _ = Error
     oneLineDoc _ = "ErrorBottomTotalFunction"
-    oneLineJson entry =
-        JSON.object ["entry" JSON..= Log.entryTypeText (Log.toEntry entry)]
     helpDoc _ = "errors raised when a total function is undefined"
 
 instance SQL.Table ErrorBottomTotalFunction