From e7409dc55eb5ee8834aa4541cceaa8dff5d786f4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 2 Jul 2024 10:32:00 +1000 Subject: [PATCH] Use typed log context in kore, add optional timestamp (with flexible parsing) (#3967) --- .../simplify-log.txt.golden | 4 +- booster/tools/booster/Server.hs | 5 +- dev-tools/kore-rpc-dev/Server.hs | 3 +- .../src/Kore/JsonRpc/Types/ContextLog.hs | 52 +++++++++++++- kore/src/Kore/Equation/Application.hs | 4 +- kore/src/Kore/Equation/DebugEquation.hs | 69 +++++++------------ kore/src/Kore/JsonRpc.hs | 56 +++++++-------- kore/src/Kore/Log/BoosterAdaptor.hs | 11 +-- kore/src/Kore/Log/DebugAppliedRewriteRules.hs | 7 +- kore/src/Kore/Log/DebugAttemptUnification.hs | 2 +- .../Kore/Log/DebugAttemptedRewriteRules.hs | 29 +++----- kore/src/Kore/Log/DebugBeginClaim.hs | 1 + kore/src/Kore/Log/DebugContext.hs | 17 +++-- kore/src/Kore/Log/DebugCreatedSubstitution.hs | 1 + kore/src/Kore/Log/DebugEvaluateCondition.hs | 4 ++ kore/src/Kore/Log/DebugProven.hs | 1 + kore/src/Kore/Log/DebugRetrySolverQuery.hs | 1 + .../Kore/Log/DebugRewriteRulesRemainder.hs | 36 +++------- kore/src/Kore/Log/DebugRewriteTrace.hs | 7 +- kore/src/Kore/Log/DebugSolver.hs | 4 ++ .../Kore/Log/DebugSubstitutionSimplifier.hs | 1 + kore/src/Kore/Log/DebugTransition.hs | 1 + kore/src/Kore/Log/DebugUnification.hs | 1 + kore/src/Kore/Log/DebugUnifyBottom.hs | 3 + kore/src/Kore/Log/DecidePredicateUnknown.hs | 8 ++- kore/src/Kore/Log/ErrorBottomTotalFunction.hs | 1 + .../Kore/Log/ErrorEquationRightFunction.hs | 3 + kore/src/Kore/Log/ErrorEquationsSameMatch.hs | 3 + kore/src/Kore/Log/ErrorException.hs | 1 + kore/src/Kore/Log/ErrorOutOfDate.hs | 1 + kore/src/Kore/Log/ErrorParse.hs | 1 + kore/src/Kore/Log/ErrorRewriteLoop.hs | 1 + .../Kore/Log/ErrorRewritesInstantiation.hs | 1 + kore/src/Kore/Log/ErrorVerify.hs | 1 + kore/src/Kore/Log/InfoExecBreadth.hs | 1 + kore/src/Kore/Log/InfoExecDepth.hs | 1 + kore/src/Kore/Log/InfoJsonRpcCancelRequest.hs | 1 + .../src/Kore/Log/InfoJsonRpcProcessRequest.hs | 1 + kore/src/Kore/Log/InfoProofDepth.hs | 1 + kore/src/Kore/Log/InfoReachability.hs | 1 + kore/src/Kore/Log/InfoUserLog.hs | 1 + kore/src/Kore/Log/JsonRpc.hs | 2 +- kore/src/Kore/Log/WarnBottom.hs | 2 + kore/src/Kore/Log/WarnDepthLimitExceeded.hs | 1 + .../Kore/Log/WarnFunctionWithoutEvaluators.hs | 3 + kore/src/Kore/Log/WarnIfLowProductivity.hs | 1 + kore/src/Kore/Log/WarnNotAPredicate.hs | 1 + kore/src/Kore/Log/WarnNotImplemented.hs | 1 + kore/src/Kore/Log/WarnRestartSolver.hs | 1 + kore/src/Kore/Log/WarnStepTimeout.hs | 2 + kore/src/Kore/Log/WarnStuckClaimState.hs | 1 + .../Kore/Log/WarnSymbolSMTRepresentation.hs | 1 + kore/src/Kore/Log/WarnTrivialClaim.hs | 1 + kore/src/Kore/Log/WarnUnexploredBranches.hs | 1 + kore/src/Kore/Log/WarnUnsimplified.hs | 2 + kore/src/Kore/Rewrite/Step.hs | 8 +-- kore/src/Kore/Simplify/Simplify.hs | 2 +- kore/src/Kore/Unification/Procedure.hs | 4 +- kore/src/Log.hs | 40 +++-------- kore/src/Log/Entry.hs | 38 ++++++++-- 60 files changed, 262 insertions(+), 198 deletions(-) diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index 5ce3270771..e7d03842a4 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -57,8 +57,8 @@ {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} -{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} -{"context":["request 4","kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768c"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} +{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"...resources/log-simplify-json.kore:3913:7"} +{"context":[{"request":"4"},"kore","execute",{"term":"8aaaa91"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"c107051"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"b378f16"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"dfe34e0"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","simplify",{"term":"ee3511f"},{"term":"4a36bb8"},{"hook":"INT.le"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","simplify",{"term":"66aa67b"},{"term":"8f1e2b8"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 8f1cdadbe7..8d90fb504b 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -22,6 +22,7 @@ import Control.Monad.Logger ( import Control.Monad.Trans.Reader (runReaderT) import Data.Aeson qualified as JSON import Data.Bifunctor (bimap) +import Data.ByteString.Char8 qualified as BS import Data.Coerce (coerce) import Data.Conduit.Network (serverSettings) import Data.IORef (writeIORef) @@ -176,7 +177,7 @@ main = do not contextLoggingEnabled || ( let contextStrs = concatMap - ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c + ( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c ) ctxt in any (flip Ctxt.mustMatch contextStrs) logContextsWithcustomLevelContexts @@ -508,7 +509,7 @@ translateSMTOpts = \case mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions = - flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext "kore") $ do + flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext $ Log.CLNullary CtxKore) $ do sd@GlobalMain.SerializedDefinition{internedTextCache} <- GlobalMain.deserializeDefinition koreSolverOptions diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs index 768d3d2788..ed64ff6e14 100644 --- a/dev-tools/kore-rpc-dev/Server.hs +++ b/dev-tools/kore-rpc-dev/Server.hs @@ -19,6 +19,7 @@ import Control.Monad.Logger ( ) import Control.Monad.Trans.Reader (runReaderT) import Data.Aeson.Types (Value (..)) +import Data.ByteString.Char8 qualified as BS import Data.Conduit.Network (serverSettings) import Data.IORef (writeIORef) import Data.InternedText (globalInternedTextCache) @@ -187,7 +188,7 @@ main = do null logContextsWithcustomLevelContexts || ( let contextStrs = concatMap - ( \(Log.SomeEntry _ c) -> Text.encodeUtf8 <$> Log.oneLineContextDoc c + ( \(Log.SomeEntry _ c) -> BS.pack . show <$> Log.oneLineContextDoc c ) ctxt in any (flip Booster.Log.Context.mustMatch contextStrs) logContextsWithcustomLevelContexts diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs index 86a76839f5..bd5ae93b74 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs @@ -8,6 +8,8 @@ module Kore.JsonRpc.Types.ContextLog ( module Kore.JsonRpc.Types.ContextLog, ) where +import Control.Applicative ((<|>)) +import Data.Aeson ((.:), (.:?), (.=)) import Data.Aeson.TH (deriveJSON) import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions) import Data.Aeson.Types qualified as JSON @@ -15,6 +17,9 @@ import Data.Data (Data, toConstr) import Data.Sequence (Seq) import Data.Text (Text, unpack) import Data.Text qualified as Text +import Data.Time.Clock.System (SystemTime (..), systemToUTCTime, utcToSystemTime) +import Data.Time.Format (defaultTimeLocale, formatTime, parseTimeM) +import Text.Read (readMaybe) data SimpleContext = -- component @@ -30,6 +35,7 @@ data SimpleContext | -- mode/phase CtxInternalise | CtxMatch + | CtxUnify | CtxDefinedness | CtxConstraint | CtxSMT @@ -45,6 +51,7 @@ data SimpleContext CtxKoreTerm | CtxDetail | CtxSubstitution + | CtxRemainder | CtxDepth | CtxTiming | -- standard log levels @@ -183,9 +190,50 @@ instance ToJSON CLMessage where toJSON (CLValue value) = value data LogLine = LogLine - { context :: Seq CLContext + { timestamp :: Maybe SystemTime + , context :: Seq CLContext , message :: CLMessage } deriving stock (Show, Eq) -$(deriveJSON defaultOptions ''LogLine) +instance FromJSON LogLine where + parseJSON = JSON.withObject "LogLine" $ \l -> + LogLine + <$> (l .:? "timestamp" >>= parseTimestamp) + <*> l .: "context" + <*> l .: "message" + +parseTimestamp :: Maybe JSON.Value -> JSON.Parser (Maybe SystemTime) +parseTimestamp Nothing = pure Nothing +parseTimestamp (Just x) = + JSON.withScientific "numeric timestamp" (pure . Just . fromNumeric) x + <|> JSON.withText "human-readable timestamp" fromString x + <|> JSON.withText "nanosecond timestamp" fromNanos x + where + -- fromNumeric :: Scientific -> SystemTime + fromNumeric n = + let seconds = truncate n + nanos = truncate $ 1e9 * (n - fromIntegral seconds) -- no leap seconds + in MkSystemTime seconds nanos + fromString s = do + utc <- parseTimeM False defaultTimeLocale timestampFormat (Text.unpack s) + pure . Just $ utcToSystemTime utc + fromNanos s = + case readMaybe (Text.unpack s) of + Nothing -> fail $ "bad number " <> show s + Just (n :: Integer) -> pure . Just $ fromNumeric (fromIntegral n :: Double) + +instance ToJSON LogLine where + toJSON LogLine{timestamp, context, message} = + JSON.object $ + maybe + [] + (\t -> ["timestamp" .= formatted t]) + timestamp + <> ["context" .= context, "message" .= message] + where + formatted = formatTime defaultTimeLocale timestampFormat . systemToUTCTime + +-- same format as the one used in Booster.Util +timestampFormat :: String +timestampFormat = "%Y-%m-%dT%H:%M:%S%6Q" diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs index 936f9c8c3e..c5285c9de6 100644 --- a/kore/src/Kore/Equation/Application.hs +++ b/kore/src/Kore/Equation/Application.hs @@ -89,7 +89,7 @@ import Kore.Internal.TermLike ( TermLike, ) import Kore.Internal.TermLike qualified as TermLike -import Kore.Log.DebugContext (inContext) +import Kore.Log.DebugContext (SimpleContext (CtxConstraint), inContext) import Kore.Log.DecidePredicateUnknown ( OnDecidePredicateUnknown (..), srcLoc, @@ -362,7 +362,7 @@ checkRequires :: Predicate RewritingVariableName -> ExceptT (CheckRequiresError RewritingVariableName) Simplifier () checkRequires onUnknown sideCondition predicate requires = - inContext "constraint" $ + inContext CtxConstraint $ do let requires' = makeAndPredicate predicate requires -- The condition to refute: diff --git a/kore/src/Kore/Equation/DebugEquation.hs b/kore/src/Kore/Equation/DebugEquation.hs index 300b11a76e..5652a8151e 100644 --- a/kore/src/Kore/Equation/DebugEquation.hs +++ b/kore/src/Kore/Equation/DebugEquation.hs @@ -36,7 +36,6 @@ import Data.Text ( Text, ) import Data.Text qualified as Text -import Data.Vector qualified as Vec import Debug import GHC.Generics qualified as GHC import Generics.SOP qualified as SOP @@ -48,7 +47,7 @@ import Kore.Attribute.SourceLocation ( ) import Kore.Equation.Equation (Equation (..)) import Kore.Internal.OrCondition (OrCondition) -import Kore.Internal.Pattern (Conditional (..), Pattern) +import Kore.Internal.Pattern (Conditional (..), Pattern, toTermLike) import Kore.Internal.Predicate (Predicate) import Kore.Internal.SideCondition (SideCondition) import Kore.Internal.TermLike ( @@ -294,10 +293,14 @@ instance Entry DebugAttemptEquation where helpDoc _ = "log equation application attempts" oneLineContextDoc = \case - _entry@DebugAttemptEquation{} -> ["detail"] + _entry@DebugAttemptEquation{} -> single CtxDetail (DebugAttemptEquationResult _ result) -> case result of - Right Conditional{term} -> ["success", "term " <> (showHashHex $ hash term), "kore-term"] - Left{} -> ["failure"] + Right Conditional{term} -> + [ CLNullary CtxSuccess + , CtxTerm `withShortId` showHashHex (hash term) + , CLNullary CtxKoreTerm + ] + Left{} -> single CtxFailure oneLineDoc (DebugAttemptEquation equation _term) = maybe @@ -310,21 +313,6 @@ instance Entry DebugAttemptEquation where Right Conditional{term} -> " " <> unparse term Left failure -> " " <> Pretty.pretty (failureDescription failure) - oneLineContextJson = \case - _entry@DebugAttemptEquation{} -> JSON.String "detail" - _entry@(DebugAttemptEquationResult _equation result) -> - case result of - Right Conditional{term} -> - JSON.Array $ - Vec.fromList - [ JSON.String "success" - , JSON.object - [ "term" JSON..= showHashHex (hash term) - ] - , JSON.String "kore-term" - ] - Left _failure -> JSON.String "failure" - oneLineJson = \case _entry@(DebugAttemptEquation equation _term) -> JSON.toJSON $ renderDefault (maybe "UNKNOWN" pretty (srcLoc equation)) @@ -350,12 +338,7 @@ instance Entry DebugTermContext where oneLineDoc DebugTermContext{} = mempty oneLineContextDoc (DebugTermContext term) = - ["term " <> (showHashHex $ hash term)] - - oneLineContextJson (DebugTermContext term) = - JSON.object - [ "term" JSON..= showHashHex (hash term) - ] + [CtxTerm `withShortId` showHashHex (hash term)] oneLineJson :: DebugTermContext -> JSON.Value oneLineJson DebugTermContext{} = @@ -366,13 +349,7 @@ instance Entry DebugTerm where oneLineDoc (DebugTerm term) = unparse term - oneLineContextDoc DebugTerm{} = - ["kore-term"] - - oneLineContextJson DebugTerm{} = - JSON.toJSON - [ "kore-term" :: Text - ] + oneLineContextDoc DebugTerm{} = single CtxKoreTerm oneLineJson (DebugTerm term) = JSON.toJSON $ Kore.Syntax.Json.fromTermLike (getRewritingTerm term) @@ -383,18 +360,9 @@ instance Entry DebugEquation where oneLineDoc _ = mempty oneLineContextDoc (DebugEquation equation) = - let equationKindTxt = if isSimplification equation then "simplification" else "function" - in [ equationKindTxt <> " " <> shortRuleIdText equation - ] - oneLineContextJson (DebugEquation equation) = - let equationKindTxt = if isSimplification equation then "simplification" else "function" - in JSON.Array $ - Vec.fromList - [ JSON.object - [ equationKindTxt - JSON..= ruleIdText equation - ] - ] + let equationKind = if isSimplification equation then CtxSimplification else CtxFunction + in [equationKind `withId` ruleIdText equation] + oneLineJson _ = JSON.Null whileDebugTerm :: @@ -485,7 +453,16 @@ instance Entry DebugApplyEquation where ] helpDoc _ = "log equation application successes" - oneLineJson _ = JSON.Null + oneLineContextDoc (DebugApplyEquation equation result) = + let equationKind = if isSimplification equation then CtxSimplification else CtxFunction + in [ equationKind `withId` ruleIdText equation + , CLNullary CtxSuccess + , CtxTerm `withShortId` showHashHex (hash result) + , CLNullary CtxKoreTerm + ] + + oneLineJson (DebugApplyEquation _ result) = + JSON.toJSON $ Kore.Syntax.Json.fromTermLike . getRewritingTerm $ toTermLike result {- | Log when an 'Equation' is actually applied. diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 9397a4e2f2..1f54c929db 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -162,24 +162,22 @@ respond reqId serverState moduleName runSMT = traversalResult <- liftIO ( runSMT (Exec.metadataTools serializedModule) lemmas $ - Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) $ - Log.logWhile (Log.DebugContext "kore") $ - Log.logWhile (Log.DebugContext "execute") $ - Exec.rpcExec - (maybe Unlimited (\(Depth n) -> Limit n) maxDepth) - (coerce stepTimeout) - ( if fromMaybe False movingAverageStepTimeout - then EnableMovingAverage - else DisableMovingAverage - ) - ( if fromMaybe False assumeStateDefined - then EnableAssumeInitialDefined - else DisableAssumeInitialDefined - ) - tracingEnabled - serializedModule - (toStopLabels cutPointRules terminalRules) - verifiedPattern + withContextLog Log.CtxExecute $ + Exec.rpcExec + (maybe Unlimited (\(Depth n) -> Limit n) maxDepth) + (coerce stepTimeout) + ( if fromMaybe False movingAverageStepTimeout + then EnableMovingAverage + else DisableMovingAverage + ) + ( if fromMaybe False assumeStateDefined + then EnableAssumeInitialDefined + else DisableAssumeInitialDefined + ) + tracingEnabled + serializedModule + (toStopLabels cutPointRules terminalRules) + verifiedPattern ) stop <- liftIO $ getTime Monotonic @@ -433,9 +431,7 @@ respond reqId serverState moduleName runSMT = result <- liftIO . runSMT (Exec.metadataTools serializedModule) lemmas - . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) - . Log.logWhile (Log.DebugContext "kore") - . Log.logWhile (Log.DebugContext "implies") + . withContextLog Log.CtxImplies . evalInSimplifierContext serializedModule . runExceptT $ Claim.checkSimpleImplication @@ -518,9 +514,7 @@ respond reqId serverState moduleName runSMT = result <- liftIO . runSMT (Exec.metadataTools serializedModule) lemmas - . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) - . Log.logWhile (Log.DebugContext "kore") - . Log.logWhile (Log.DebugContext "simplify") + . withContextLog Log.CtxSimplify . evalInSimplifierContext serializedModule $ SMT.Evaluator.filterMultiOr $srcLoc =<< Pattern.simplify patt @@ -616,9 +610,7 @@ respond reqId serverState moduleName runSMT = serializedModule <- liftIO . runSMT metadataTools lemmas - . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) - . Log.logWhile (Log.DebugContext "kore") - . Log.logWhile (Log.DebugContext "add-module") + . withContextLog Log.CtxAddModule $ Exec.makeSerializedModule newModule internedTextCacheHash <- liftIO $ readIORef globalInternedTextCache @@ -677,9 +669,7 @@ respond reqId serverState moduleName runSMT = else liftIO . runSMT tools lemmas - . Log.logWhile (Log.DebugContext $ Text.pack $ "request " <> reqId) - . Log.logWhile (Log.DebugContext "kore") - . Log.logWhile (Log.DebugContext "get-model") + . withContextLog Log.CtxGetModel . SMT.Evaluator.getModelFor tools $ NonEmpty.fromList preds @@ -706,6 +696,12 @@ respond reqId serverState moduleName runSMT = -- this case is only reachable if the cancel appeared as part of a batch request Cancel -> pure $ Left cancelUnsupportedInBatchMode where + withContextLog :: Log.SimpleContext -> SMT.SMT a -> SMT.SMT a + withContextLog method = + Log.logWhile (Log.DebugContext $ Log.CLWithId $ Log.CtxRequest $ Text.pack reqId) + . Log.inContext Log.CtxKore + . Log.inContext method + withMainModule module' act = do let mainModule = fromMaybe moduleName module' ServerState{serializedModules} <- liftIO $ MVar.readMVar serverState diff --git a/kore/src/Kore/Log/BoosterAdaptor.hs b/kore/src/Kore/Log/BoosterAdaptor.hs index 6f844a1701..0c6019a730 100644 --- a/kore/src/Kore/Log/BoosterAdaptor.hs +++ b/kore/src/Kore/Log/BoosterAdaptor.hs @@ -82,13 +82,8 @@ renderJson mTime e@(SomeEntry context actualEntry) = json where jsonContext = - foldr - ( \(SomeEntry _ c) cs -> case oneLineContextJson c of - JSON.Array cs' -> cs' <> cs - j -> Vec.cons j cs - ) - mempty - (context <> [e]) + Vec.fromList $ + concatMap (\(SomeEntry _ c) -> map JSON.toJSON (oneLineContextDoc c)) (context <> [e]) json = case oneLineJson actualEntry of JSON.Object o @@ -112,7 +107,7 @@ renderOnelinePretty :: Maybe ByteString -> SomeEntry -> LogStr renderOnelinePretty mTime entry@(SomeEntry entryContext _actualEntry) = let cs = (entryContext <> [entry]) - & concatMap (map Pretty.brackets . (\(SomeEntry _ e) -> Pretty.pretty <$> oneLineContextDoc e)) + & concatMap (map Pretty.brackets . (\(SomeEntry _ e) -> Pretty.pretty . show <$> oneLineContextDoc e)) leaf = oneLineDoc entry in maybe mempty ((<> " ") . toLogStr) mTime <> ( mconcat cs Pretty.<+> leaf diff --git a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs index 8aa8dc28f2..eba576062d 100644 --- a/kore/src/Kore/Log/DebugAppliedRewriteRules.hs +++ b/kore/src/Kore/Log/DebugAppliedRewriteRules.hs @@ -78,9 +78,9 @@ instance Entry DebugAppliedRewriteRules where "applied " <> show (length appliedRewriteRules) <> " rewrite rules" oneLineContextDoc DebugAppliedRewriteRules{appliedRewriteRules} | null appliedRewriteRules = - ["failure"] + single CtxFailure | otherwise = - ["success"] + single CtxSuccess debugAppliedRewriteRules :: MonadLog log => @@ -127,8 +127,7 @@ instance Entry DebugAppliedLabeledRewriteRule where oneLineDoc DebugAppliedLabeledRewriteRule{label, sourceLocation} = maybe (pretty sourceLocation) pretty label oneLineJson = toJSON . renderDefault . oneLineDoc - oneLineContextDoc DebugAppliedLabeledRewriteRule{} = ["success"] - oneLineContextJson DebugAppliedLabeledRewriteRule{} = toJSON ("success" :: Text) + oneLineContextDoc DebugAppliedLabeledRewriteRule{} = single CtxSuccess debugAppliedLabeledRewriteRule :: MonadLog log => diff --git a/kore/src/Kore/Log/DebugAttemptUnification.hs b/kore/src/Kore/Log/DebugAttemptUnification.hs index 3a64c201e4..026d130c56 100644 --- a/kore/src/Kore/Log/DebugAttemptUnification.hs +++ b/kore/src/Kore/Log/DebugAttemptUnification.hs @@ -38,7 +38,7 @@ instance Entry DebugAttemptUnification where entrySeverity _ = Debug contextDoc _ = Just "while attempting unification" oneLineDoc _ = "DebugAttemptUnification" - oneLineContextDoc _ = ["unify"] + oneLineContextDoc _ = single CtxUnify helpDoc _ = "log unification attempts" instance Pretty DebugAttemptUnification where diff --git a/kore/src/Kore/Log/DebugAttemptedRewriteRules.hs b/kore/src/Kore/Log/DebugAttemptedRewriteRules.hs index 29d782da7a..41dc1cd232 100644 --- a/kore/src/Kore/Log/DebugAttemptedRewriteRules.hs +++ b/kore/src/Kore/Log/DebugAttemptedRewriteRules.hs @@ -12,10 +12,9 @@ module Kore.Log.DebugAttemptedRewriteRules ( whileDebugAttemptRewriteRule, ) where -import Data.Aeson (Value (Array), object, toJSON, (.=)) +import Data.Aeson (object, (.=)) import Data.Text (Text) import Data.Text qualified as Text -import Data.Vector (fromList) import Kore.Attribute.Axiom ( SourceLocation, UniqueId (..), @@ -32,7 +31,7 @@ import Kore.Internal.Variable ( import Kore.Rewrite.RewritingVariable import Kore.Unparser import Kore.Util (showHashHex) -import Log +import Log hiding (UniqueId) import Prelude.Kore import Pretty ( Pretty (..), @@ -72,23 +71,12 @@ instance Entry DebugAttemptedRewriteRules where oneLineContextDoc = \case DebugAttemptedRewriteRules{configuration, ruleId} -> - [ "term " <> (showHashHex $ hash configuration) - , "rewrite " <> shortRuleIdTxt ruleId + [ CtxTerm `withShortId` showHashHex (hash configuration) + , CtxRewrite `withId` fromMaybe "UNKNOWN" (getUniqueId ruleId) ] - oneLineContextJson - DebugAttemptedRewriteRules{configuration, ruleId} = - Array $ - fromList - [ object - [ "term" .= showHashHex (hash configuration) - ] - , object - [ "rewrite" .= shortRuleIdTxt ruleId - ] - ] oneLineDoc entry@(DebugAttemptedRewriteRules{configuration, label, ruleId, attemptedRewriteRule}) = - let context = map Pretty.brackets (pretty <$> oneLineContextDoc entry <> ["detail"]) + let context = map Pretty.brackets (pretty . show <$> oneLineContextDoc entry <> single CtxDetail) logMsg = ( Pretty.hsep . concat $ [ ["attempting to apply rewrite rule", Pretty.pretty (shortRuleIdTxt ruleId), Pretty.pretty label] @@ -99,7 +87,12 @@ instance Entry DebugAttemptedRewriteRules where in mconcat context <> logMsg oneLineJson DebugAttemptedRewriteRules{label, attemptedRewriteRule} = - toJSON $ renderDefault $ maybe (Pretty.pretty attemptedRewriteRule) Pretty.pretty label + -- add the "detail" context here (floated out in BoosterAdaptor) + object + [ "context" .= CtxDetail + , "message" + .= renderDefault (maybe (Pretty.pretty attemptedRewriteRule) Pretty.pretty label) + ] whileDebugAttemptRewriteRule :: MonadLog log => diff --git a/kore/src/Kore/Log/DebugBeginClaim.hs b/kore/src/Kore/Log/DebugBeginClaim.hs index 2017621b2e..ea0cbf7f11 100644 --- a/kore/src/Kore/Log/DebugBeginClaim.hs +++ b/kore/src/Kore/Log/DebugBeginClaim.hs @@ -35,6 +35,7 @@ instance Entry DebugBeginClaim where helpDoc _ = "log starting claims" oneLineDoc DebugBeginClaim{claim} = pretty @SourceLocation $ from claim + oneLineContextDoc _ = single CtxDetail debugBeginClaim :: MonadLog log => diff --git a/kore/src/Kore/Log/DebugContext.hs b/kore/src/Kore/Log/DebugContext.hs index 9a052ec073..c50ddb301a 100644 --- a/kore/src/Kore/Log/DebugContext.hs +++ b/kore/src/Kore/Log/DebugContext.hs @@ -4,30 +4,29 @@ License : BSD-3-Clause -} module Kore.Log.DebugContext ( DebugContext (..), + SimpleContext (..), -- re-export for inContext inContext, ) where import Data.Aeson qualified as JSON -import Data.Text qualified as Text import Log import Prelude.Kore import Pretty ( Pretty (..), ) -newtype DebugContext = DebugContext {msg :: Text.Text} +newtype DebugContext = DebugContext {ctx :: CLContext} deriving stock (Show) instance Pretty DebugContext where - pretty DebugContext{msg} = pretty msg + pretty DebugContext{ctx} = pretty $ show ctx instance Entry DebugContext where entrySeverity DebugContext{} = Debug - helpDoc _ = "Plain text debug message to signify an action's context" - oneLineDoc DebugContext{msg} = pretty msg - oneLineContextDoc DebugContext{msg} = [msg] + helpDoc _ = "Debug message to signify an action's context" + oneLineDoc DebugContext{ctx} = pretty $ show ctx + oneLineContextDoc DebugContext{ctx} = [ctx] oneLineJson DebugContext{} = JSON.Null - oneLineContextJson DebugContext{msg} = JSON.String msg -inContext :: MonadLog log => Text.Text -> log a -> log a -inContext = logWhile . DebugContext +inContext :: MonadLog log => SimpleContext -> log a -> log a +inContext = logWhile . DebugContext . CLNullary diff --git a/kore/src/Kore/Log/DebugCreatedSubstitution.hs b/kore/src/Kore/Log/DebugCreatedSubstitution.hs index e35335ae96..a6dc9d7125 100644 --- a/kore/src/Kore/Log/DebugCreatedSubstitution.hs +++ b/kore/src/Kore/Log/DebugCreatedSubstitution.hs @@ -47,6 +47,7 @@ instance Entry DebugCreatedSubstitution where . layoutPrettyUnbounded . Pretty.group . pretty + oneLineContextDoc _ = single CtxSubstitution helpDoc _ = "log every substitution created when applying semantic rules" debugCreatedSubstitution :: diff --git a/kore/src/Kore/Log/DebugEvaluateCondition.hs b/kore/src/Kore/Log/DebugEvaluateCondition.hs index 5514ce72b2..bf5df66e21 100644 --- a/kore/src/Kore/Log/DebugEvaluateCondition.hs +++ b/kore/src/Kore/Log/DebugEvaluateCondition.hs @@ -61,6 +61,10 @@ instance Entry DebugEvaluateCondition where contextDoc _ = Just "while evaluating predicate" oneLineDoc (DebugEvaluateCondition _) = "DebugEvaluateCondition _" oneLineDoc result = pretty (show result) + oneLineContextDoc DebugEvaluateCondition{} = + map CLNullary [CtxConstraint, CtxSMT] + oneLineContextDoc DebugEvaluateConditionResult{} = + map CLNullary [CtxConstraint, CtxSMT] helpDoc _ = "log every predicate evaluated by the SMT solver" instance SQL.Table DebugEvaluateCondition diff --git a/kore/src/Kore/Log/DebugProven.hs b/kore/src/Kore/Log/DebugProven.hs index b6562eb872..1195dcab37 100644 --- a/kore/src/Kore/Log/DebugProven.hs +++ b/kore/src/Kore/Log/DebugProven.hs @@ -30,4 +30,5 @@ instance Pretty DebugProven where instance Entry DebugProven where entrySeverity _ = Debug oneLineDoc DebugProven{claim} = pretty @SourceLocation $ from claim + oneLineContextDoc _ = single CtxDetail helpDoc _ = "log proven claims" diff --git a/kore/src/Kore/Log/DebugRetrySolverQuery.hs b/kore/src/Kore/Log/DebugRetrySolverQuery.hs index ad10093a8b..32d1839b4b 100644 --- a/kore/src/Kore/Log/DebugRetrySolverQuery.hs +++ b/kore/src/Kore/Log/DebugRetrySolverQuery.hs @@ -48,6 +48,7 @@ instance Pretty DebugRetrySolverQuery where instance Entry DebugRetrySolverQuery where entrySeverity _ = Debug oneLineDoc _ = "DebugRetrySolverQuery" + oneLineContextDoc _ = single CtxSMT helpDoc _ = "warning raised when the solver failed to decide\ \ the satisfiability of a formula, indicating that\ diff --git a/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs b/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs index 187b7bdfd9..5ec9a59576 100644 --- a/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs +++ b/kore/src/Kore/Log/DebugRewriteRulesRemainder.hs @@ -11,9 +11,7 @@ module Kore.Log.DebugRewriteRulesRemainder ( debugRewriteRulesRemainder, ) where -import Data.Aeson (Value (Array), object, toJSON, (.=)) -import Data.Text qualified as Text -import Data.Vector (fromList) +import Data.Aeson (object, (.=)) import Kore.Internal.Conditional qualified as Conditional import Kore.Internal.Pattern ( Pattern, @@ -67,20 +65,8 @@ instance Entry DebugRewriteRulesRemainder where helpDoc _ = "log rewrite rules remainder" oneLineContextDoc - DebugRewriteRulesRemainder{} = [remainderContextName] - - oneLineContextJson - DebugRewriteRulesRemainder{configuration, rulesCount} = - Array $ - fromList - [ toJSON remainderContextName - , object - [ "term" .= showHashHex (hash configuration) - ] - , object - [ "rules-count" .= Text.pack (show rulesCount) - ] - ] + DebugRewriteRulesRemainder{configuration} = + [CLNullary CtxRemainder, CtxTerm `withShortId` showHashHex (hash configuration)] oneLineDoc (DebugRewriteRulesRemainder{rulesCount, remainder}) = let context = [Pretty.brackets "detail"] @@ -95,14 +81,14 @@ instance Entry DebugRewriteRulesRemainder where ) in mconcat context <> logMsg - oneLineJson DebugRewriteRulesRemainder{remainder} = - toJSON - . PatternJson.fromPredicate sortBool - . Predicate.mapVariables (pure toVariableName) - $ remainder - -remainderContextName :: Text.Text -remainderContextName = "remainder" + oneLineJson DebugRewriteRulesRemainder{remainder, rulesCount} = + object + [ "remainder" + .= PatternJson.fromPredicate + sortBool + (Predicate.mapVariables (pure toVariableName) remainder) + , "rules-count" .= rulesCount + ] sortBool :: TermLike.Sort sortBool = diff --git a/kore/src/Kore/Log/DebugRewriteTrace.hs b/kore/src/Kore/Log/DebugRewriteTrace.hs index 2257157dc4..1c904f2f66 100644 --- a/kore/src/Kore/Log/DebugRewriteTrace.hs +++ b/kore/src/Kore/Log/DebugRewriteTrace.hs @@ -76,7 +76,8 @@ import Kore.Unparser ( Unparse, unparse, ) -import Log +import Kore.Util (showHashHex) +import Log hiding (UniqueId) import Prelude.Kore import Pretty ( Pretty (..), @@ -180,21 +181,25 @@ instance Pretty DebugRewriteTrace where instance Entry DebugInitialClaim where entrySeverity _ = Debug oneLineDoc (DebugInitialClaim uniqueId _) = "Initial claim " <> maybe mempty pretty (getUniqueId uniqueId) + oneLineContextDoc _ = single CtxDetail helpDoc _ = "log every claim before proving it" instance Entry DebugInitialPattern where entrySeverity _ = Debug oneLineDoc (DebugInitialPattern _) = "Initial pattern" + oneLineContextDoc (DebugInitialPattern p) = [CtxTerm `withShortId` showHashHex (hash p)] helpDoc _ = "log initial pattern before rewriting" instance Entry DebugFinalPatterns where entrySeverity _ = Debug oneLineDoc (DebugFinalPatterns _) = "Final patterns" + oneLineContextDoc _ = single CtxDetail helpDoc _ = "log final patterns after rewriting" instance Entry DebugRewriteTrace where entrySeverity _ = Debug oneLineDoc DebugRewriteTrace{} = "Rewrite trace" + oneLineContextDoc _ = single CtxDetail helpDoc _ = "log rewrite substitutions" unparseOneLine :: Unparse p => p -> Text diff --git a/kore/src/Kore/Log/DebugSolver.hs b/kore/src/Kore/Log/DebugSolver.hs index 9de6bffbdc..6e7428c80a 100644 --- a/kore/src/Kore/Log/DebugSolver.hs +++ b/kore/src/Kore/Log/DebugSolver.hs @@ -26,8 +26,10 @@ import Log ( Entry (..), LogAction (..), Severity (Debug), + SimpleContext (CtxSMT), SomeEntry (..), logWith, + single, ) import Options.Applicative ( Parser, @@ -66,11 +68,13 @@ instance Entry DebugSolverSend where entrySeverity _ = Debug oneLineDoc _ = "DebugSolverSend" helpDoc _ = "log commands sent to SMT solver" + oneLineContextDoc _ = single CtxSMT instance Entry DebugSolverRecv where entrySeverity _ = Debug oneLineDoc _ = "DebugSolverRecv" helpDoc _ = "log responses received from SMT solver" + oneLineContextDoc _ = single CtxSMT logDebugSolverSendWith :: LogAction m SomeEntry -> diff --git a/kore/src/Kore/Log/DebugSubstitutionSimplifier.hs b/kore/src/Kore/Log/DebugSubstitutionSimplifier.hs index f69daf2fc0..6c0442654e 100644 --- a/kore/src/Kore/Log/DebugSubstitutionSimplifier.hs +++ b/kore/src/Kore/Log/DebugSubstitutionSimplifier.hs @@ -38,6 +38,7 @@ instance Entry DebugSubstitutionSimplifier where entrySeverity _ = Debug contextDoc _ = Just "while simplifying substitution" oneLineDoc = pretty . show + oneLineContextDoc _ = single CtxSubstitution helpDoc _ = "log non-\\bottom results when normalizing unification solutions" instance SQL.Table DebugSubstitutionSimplifier diff --git a/kore/src/Kore/Log/DebugTransition.hs b/kore/src/Kore/Log/DebugTransition.hs index 6071212aae..591c55ce25 100644 --- a/kore/src/Kore/Log/DebugTransition.hs +++ b/kore/src/Kore/Log/DebugTransition.hs @@ -109,6 +109,7 @@ instance Entry DebugTransition where oneLineDoc (DebugBeforeTransition BeforeTransition{transition}) = "before " <> pretty transition + oneLineContextDoc _ = single CtxDetail debugBeforeTransition :: MonadLog log => diff --git a/kore/src/Kore/Log/DebugUnification.hs b/kore/src/Kore/Log/DebugUnification.hs index 9ad88108ea..a9ce3eb49c 100644 --- a/kore/src/Kore/Log/DebugUnification.hs +++ b/kore/src/Kore/Log/DebugUnification.hs @@ -41,6 +41,7 @@ instance Entry DebugUnification where oneLineDoc (DebugUnificationWhile _) = "DebugUnificationWhile" oneLineDoc (DebugUnificationSolved _) = "DebugUnificationSolved" oneLineDoc (DebugUnificationUnsolved _) = "DebugUnificationUnsolved" + oneLineContextDoc _ = single CtxUnify -- | @WhileDebugUnification@ encloses the context of unification log entries. data WhileDebugUnification = WhileDebugUnification {term1, term2 :: TermLike VariableName} diff --git a/kore/src/Kore/Log/DebugUnifyBottom.hs b/kore/src/Kore/Log/DebugUnifyBottom.hs index e22531acc3..7603befc71 100644 --- a/kore/src/Kore/Log/DebugUnifyBottom.hs +++ b/kore/src/Kore/Log/DebugUnifyBottom.hs @@ -23,9 +23,11 @@ import Kore.Internal.TermLike ( import Kore.Internal.TermLike qualified as TermLike import Kore.Unparser (unparse) import Log ( + CLContext (CLNullary), Entry (..), MonadLog (..), Severity (..), + SimpleContext (CtxFailure, CtxUnify), logEntry, ) import Logic ( @@ -59,6 +61,7 @@ instance Pretty DebugUnifyBottom where instance Entry DebugUnifyBottom where entrySeverity _ = Debug oneLineDoc _ = "DebugUnifyBottom" + oneLineContextDoc _ = map CLNullary [CtxUnify, CtxFailure] helpDoc _ = "log failed unification" mkDebugUnifyBottom :: diff --git a/kore/src/Kore/Log/DecidePredicateUnknown.hs b/kore/src/Kore/Log/DecidePredicateUnknown.hs index 109436a32b..9dd04c0171 100644 --- a/kore/src/Kore/Log/DecidePredicateUnknown.hs +++ b/kore/src/Kore/Log/DecidePredicateUnknown.hs @@ -104,8 +104,7 @@ instance Entry DecidePredicateUnknown where Pretty.pretty loc_module <> ":" <> Pretty.pretty row <> ":" <> Pretty.pretty col oneLineDoc (DecidePredicateUnknown{message, predicates}) = Pretty.hsep - [ Pretty.brackets "smt" - , Pretty.pretty description + [ Pretty.pretty description , unparse ( Predicate.fromPredicate sortBool @@ -119,6 +118,11 @@ instance Entry DecidePredicateUnknown where <> message <> " for predicate " + oneLineContextDoc DecidePredicateUnknown{action} = + let level = case action of + ErrorDecidePredicateUnknown{} -> CtxError + WarnDecidePredicateUnknown{} -> CtxWarn + in map CLNullary [CtxSMT, level] helpDoc _ = "error or a warning when the solver cannot decide the satisfiability of a formula" diff --git a/kore/src/Kore/Log/ErrorBottomTotalFunction.hs b/kore/src/Kore/Log/ErrorBottomTotalFunction.hs index 9d55b08cdc..bccae791e3 100644 --- a/kore/src/Kore/Log/ErrorBottomTotalFunction.hs +++ b/kore/src/Kore/Log/ErrorBottomTotalFunction.hs @@ -55,6 +55,7 @@ instance Exception ErrorBottomTotalFunction where instance Entry ErrorBottomTotalFunction where entrySeverity _ = Error oneLineDoc _ = "ErrorBottomTotalFunction" + oneLineContextDoc _ = single CtxError helpDoc _ = "errors raised when a total function is undefined" instance SQL.Table ErrorBottomTotalFunction diff --git a/kore/src/Kore/Log/ErrorEquationRightFunction.hs b/kore/src/Kore/Log/ErrorEquationRightFunction.hs index cca2cdc1bb..4bde61a51f 100644 --- a/kore/src/Kore/Log/ErrorEquationRightFunction.hs +++ b/kore/src/Kore/Log/ErrorEquationRightFunction.hs @@ -28,7 +28,9 @@ import Kore.Internal.TermLike ( import Log ( Entry (..), Severity (Error), + SimpleContext (CtxError), SomeEntry (SomeEntry), + single, ) import Prelude.Kore import Pretty ( @@ -71,6 +73,7 @@ instance Entry ErrorEquationRightFunction where Equation{attributes = Axiom{sourceLocation}} ) = pretty sourceLocation + oneLineContextDoc _ = single CtxError helpDoc _ = "errors raised when right-hand side of equation is not a function pattern" instance SQL.Table ErrorEquationRightFunction diff --git a/kore/src/Kore/Log/ErrorEquationsSameMatch.hs b/kore/src/Kore/Log/ErrorEquationsSameMatch.hs index 6e670b7a89..52d6eb628a 100644 --- a/kore/src/Kore/Log/ErrorEquationsSameMatch.hs +++ b/kore/src/Kore/Log/ErrorEquationsSameMatch.hs @@ -28,7 +28,9 @@ import Kore.Internal.TermLike ( import Log ( Entry (..), Severity (Error), + SimpleContext (CtxError), SomeEntry (SomeEntry), + single, ) import Prelude.Kore import Pretty ( @@ -83,6 +85,7 @@ instance Entry ErrorEquationsSameMatch where , Pretty.comma , pretty sourceLoc2 ] + oneLineContextDoc _ = single CtxError instance SQL.Table ErrorEquationsSameMatch diff --git a/kore/src/Kore/Log/ErrorException.hs b/kore/src/Kore/Log/ErrorException.hs index 02fe67f3dd..23ffc8bb42 100644 --- a/kore/src/Kore/Log/ErrorException.hs +++ b/kore/src/Kore/Log/ErrorException.hs @@ -49,6 +49,7 @@ instance Pretty ErrorException where instance Entry ErrorException where entrySeverity _ = Error oneLineDoc _ = "ErrorException" + oneLineContextDoc _ = single CtxError helpDoc _ = "log internal errors" errorException :: MonadLog log => SomeException -> log () diff --git a/kore/src/Kore/Log/ErrorOutOfDate.hs b/kore/src/Kore/Log/ErrorOutOfDate.hs index 816c0b13fb..b217ced969 100644 --- a/kore/src/Kore/Log/ErrorOutOfDate.hs +++ b/kore/src/Kore/Log/ErrorOutOfDate.hs @@ -34,6 +34,7 @@ instance Pretty ErrorOutOfDate where instance Entry ErrorOutOfDate where entrySeverity _ = Error oneLineDoc _ = "ErrorOutOfDate" + oneLineContextDoc _ = single CtxError errorOutOfDate :: MonadThrow log => String -> log a errorOutOfDate message = diff --git a/kore/src/Kore/Log/ErrorParse.hs b/kore/src/Kore/Log/ErrorParse.hs index ca73488a12..808293fc92 100644 --- a/kore/src/Kore/Log/ErrorParse.hs +++ b/kore/src/Kore/Log/ErrorParse.hs @@ -34,6 +34,7 @@ instance Pretty ErrorParse where instance Entry ErrorParse where entrySeverity _ = Error oneLineDoc _ = "ErrorParse" + oneLineContextDoc _ = single CtxError errorParse :: MonadThrow log => String -> log a errorParse message = diff --git a/kore/src/Kore/Log/ErrorRewriteLoop.hs b/kore/src/Kore/Log/ErrorRewriteLoop.hs index cac837a61b..92a31679de 100644 --- a/kore/src/Kore/Log/ErrorRewriteLoop.hs +++ b/kore/src/Kore/Log/ErrorRewriteLoop.hs @@ -63,6 +63,7 @@ instance Pretty ErrorRewriteLoop where instance Entry ErrorRewriteLoop where oneLineDoc ErrorRewriteLoop{rule} = pretty @SourceLocation $ from rule + oneLineContextDoc _ = single CtxError entrySeverity _ = Error errorRewriteLoop :: diff --git a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs index efd1bda845..6cea737796 100644 --- a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs +++ b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs @@ -94,6 +94,7 @@ instance Entry ErrorRewritesInstantiation where { problem = SubstitutionCoverageError{location} } = pretty location + oneLineContextDoc _ = single CtxError helpDoc _ = "log rewrite instantiation errors" instance Pretty ErrorRewritesInstantiation where diff --git a/kore/src/Kore/Log/ErrorVerify.hs b/kore/src/Kore/Log/ErrorVerify.hs index bd1234d134..84240ace4b 100644 --- a/kore/src/Kore/Log/ErrorVerify.hs +++ b/kore/src/Kore/Log/ErrorVerify.hs @@ -38,6 +38,7 @@ instance Pretty ErrorVerify where instance Entry ErrorVerify where entrySeverity _ = Error oneLineDoc _ = "ErrorVerify" + oneLineContextDoc _ = single CtxError errorVerify :: MonadThrow log => Kore.Error VerifyError -> log a errorVerify koreError = diff --git a/kore/src/Kore/Log/InfoExecBreadth.hs b/kore/src/Kore/Log/InfoExecBreadth.hs index 37bcbc7808..099fa7d4f5 100644 --- a/kore/src/Kore/Log/InfoExecBreadth.hs +++ b/kore/src/Kore/Log/InfoExecBreadth.hs @@ -39,6 +39,7 @@ instance Entry InfoExecBreadth where entrySeverity _ = Info oneLineDoc (InfoExecBreadth (ExecBreadth execBreadth)) = Pretty.pretty execBreadth + oneLineContextDoc _ = single CtxInfo helpDoc _ = "log number of concurrent branches" infoExecBreadth :: MonadLog log => ExecBreadth -> log () diff --git a/kore/src/Kore/Log/InfoExecDepth.hs b/kore/src/Kore/Log/InfoExecDepth.hs index ea28c1e7cc..f3a8c2c39a 100644 --- a/kore/src/Kore/Log/InfoExecDepth.hs +++ b/kore/src/Kore/Log/InfoExecDepth.hs @@ -48,6 +48,7 @@ instance Pretty InfoExecDepth where instance Entry InfoExecDepth where entrySeverity _ = Info oneLineDoc (InfoExecDepth (ExecDepth execDepth)) = Pretty.pretty execDepth + oneLineContextDoc _ = single CtxInfo helpDoc _ = "log depth of execution graph" infoExecDepth :: MonadLog log => ExecDepth -> log () diff --git a/kore/src/Kore/Log/InfoJsonRpcCancelRequest.hs b/kore/src/Kore/Log/InfoJsonRpcCancelRequest.hs index b6456c4c19..673c3c4eed 100644 --- a/kore/src/Kore/Log/InfoJsonRpcCancelRequest.hs +++ b/kore/src/Kore/Log/InfoJsonRpcCancelRequest.hs @@ -35,4 +35,5 @@ instance Pretty InfoJsonRpcCancelRequest where instance Entry InfoJsonRpcCancelRequest where entrySeverity _ = Info oneLineDoc = Pretty.pretty + oneLineContextDoc _ = single CtxInfo helpDoc _ = "log cancelled request to the JSON RPC server" diff --git a/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs b/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs index e44ecadc1c..c1c66e29cf 100644 --- a/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs +++ b/kore/src/Kore/Log/InfoJsonRpcProcessRequest.hs @@ -43,4 +43,5 @@ instance Pretty InfoJsonRpcProcessRequest where instance Entry InfoJsonRpcProcessRequest where entrySeverity _ = Info oneLineDoc = Pretty.pretty + oneLineContextDoc _ = single CtxInfo helpDoc _ = "log valid requests to the JSON RPC server" diff --git a/kore/src/Kore/Log/InfoProofDepth.hs b/kore/src/Kore/Log/InfoProofDepth.hs index aea19302ab..aadf636a67 100644 --- a/kore/src/Kore/Log/InfoProofDepth.hs +++ b/kore/src/Kore/Log/InfoProofDepth.hs @@ -58,6 +58,7 @@ instance Entry InfoProofDepth where , Pretty.pretty depth ] + oneLineContextDoc _ = single CtxInfo helpDoc _ = "log depth of proof graph" infoUnprovenDepth :: MonadLog log => ProofDepth -> log () diff --git a/kore/src/Kore/Log/InfoReachability.hs b/kore/src/Kore/Log/InfoReachability.hs index fd6606f5af..00bf373ab9 100644 --- a/kore/src/Kore/Log/InfoReachability.hs +++ b/kore/src/Kore/Log/InfoReachability.hs @@ -31,6 +31,7 @@ instance Log.Entry InfoReachability where entrySeverity _ = Log.Info contextDoc InfoReachability{prim} = (<+>) "while" <$> primDoc prim oneLineDoc InfoReachability{prim} = Pretty.pretty . show $ prim + oneLineContextDoc _ = Log.single Log.CtxInfo helpDoc _ = "log reachability proof steps" primDoc :: Prim -> Maybe (Doc ann) diff --git a/kore/src/Kore/Log/InfoUserLog.hs b/kore/src/Kore/Log/InfoUserLog.hs index 89efa02ebb..a32824bf6a 100644 --- a/kore/src/Kore/Log/InfoUserLog.hs +++ b/kore/src/Kore/Log/InfoUserLog.hs @@ -35,6 +35,7 @@ instance Pretty InfoUserLog where instance Entry InfoUserLog where entrySeverity _ = Info oneLineDoc (InfoUserLog userLog) = Pretty.pretty userLog + oneLineContextDoc _ = single CtxInfo helpDoc _ = "user-specified log message" infoUserLog :: MonadLog log => Text -> log () diff --git a/kore/src/Kore/Log/JsonRpc.hs b/kore/src/Kore/Log/JsonRpc.hs index c9f3532ad4..1b4aac1094 100644 --- a/kore/src/Kore/Log/JsonRpc.hs +++ b/kore/src/Kore/Log/JsonRpc.hs @@ -41,7 +41,7 @@ instance Entry LogJsonRpcServer where _ -> Debug helpDoc _ = "log JSON RPC Server messages" oneLineDoc LogJsonRpcServer{msg} = pretty $ Text.replace "\n" " " $ Text.decodeUtf8 $ fromLogStr msg - + oneLineContextDoc l = [severityToContext $ entrySeverity l] contextDoc LogJsonRpcServer{loc} = if isDefaultLoc loc then Nothing diff --git a/kore/src/Kore/Log/WarnBottom.hs b/kore/src/Kore/Log/WarnBottom.hs index baf5363940..44bce92c14 100644 --- a/kore/src/Kore/Log/WarnBottom.hs +++ b/kore/src/Kore/Log/WarnBottom.hs @@ -38,6 +38,7 @@ instance Entry WarnClaimRHSIsBottom where entrySeverity _ = Warning helpDoc _ = "warn when the right-hand side of a claim is bottom" oneLineDoc WarnClaimRHSIsBottom{claim} = prettySourceLocation claim + oneLineContextDoc _ = single CtxWarn prettySourceLocation :: ClaimPattern -> Pretty.Doc ann prettySourceLocation = Pretty.pretty @SourceLocation . from @@ -64,6 +65,7 @@ instance Entry WarnConfigIsBottom where entrySeverity _ = Warning helpDoc _ = "warn when the configuration is bottom" oneLineDoc _ = "A configuration has been simplified to bottom." + oneLineContextDoc _ = single CtxWarn warnConfigIsBottom :: MonadLog log => diff --git a/kore/src/Kore/Log/WarnDepthLimitExceeded.hs b/kore/src/Kore/Log/WarnDepthLimitExceeded.hs index 8b74104c5f..dc5792cd66 100644 --- a/kore/src/Kore/Log/WarnDepthLimitExceeded.hs +++ b/kore/src/Kore/Log/WarnDepthLimitExceeded.hs @@ -39,6 +39,7 @@ instance Entry WarnDepthLimitExceeded where entrySeverity _ = Warning oneLineDoc (WarnDepthLimitExceeded limitExceeded) = Pretty.pretty limitExceeded + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warn when depth limit is exceeded" warnDepthLimitExceeded :: MonadLog log => Natural -> log () diff --git a/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs b/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs index ab96ceb720..7137406da9 100644 --- a/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs +++ b/kore/src/Kore/Log/WarnFunctionWithoutEvaluators.hs @@ -27,7 +27,9 @@ import Log ( Entry (..), MonadLog, Severity (Warning), + SimpleContext (CtxWarn), logEntry, + single, ) import Prelude.Kore import Pretty ( @@ -65,6 +67,7 @@ instance Entry WarnFunctionWithoutEvaluators where entrySeverity _ = Warning oneLineDoc (WarnFunctionWithoutEvaluators Symbol{symbolAttributes}) = Pretty.pretty $ sourceLocation symbolAttributes + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warn when encountering a function with no definition" instance SQL.Table WarnFunctionWithoutEvaluators diff --git a/kore/src/Kore/Log/WarnIfLowProductivity.hs b/kore/src/Kore/Log/WarnIfLowProductivity.hs index 9261726126..c27dbb2b19 100644 --- a/kore/src/Kore/Log/WarnIfLowProductivity.hs +++ b/kore/src/Kore/Log/WarnIfLowProductivity.hs @@ -62,6 +62,7 @@ instance Entry WarnIfLowProductivity where entrySeverity _ = Warning oneLineDoc (WarnIfLowProductivity productivityPercent _) = Pretty.pretty productivityPercent + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warn when productivty (MUT time / Total time) drops below 90%" warnIfLowProductivity :: diff --git a/kore/src/Kore/Log/WarnNotAPredicate.hs b/kore/src/Kore/Log/WarnNotAPredicate.hs index cf8f2ec9eb..a859a7a7fb 100644 --- a/kore/src/Kore/Log/WarnNotAPredicate.hs +++ b/kore/src/Kore/Log/WarnNotAPredicate.hs @@ -47,6 +47,7 @@ instance Entry WarnNotAPredicate where . Pretty.renderString . Pretty.layoutOneLine . Pretty.pretty + oneLineContextDoc WarnNotAPredicate{severity} = [severityToContext severity] helpDoc _ = "warn when a predicate simplification produces a non-predicate" diff --git a/kore/src/Kore/Log/WarnNotImplemented.hs b/kore/src/Kore/Log/WarnNotImplemented.hs index 4699880cb5..95f1dad602 100644 --- a/kore/src/Kore/Log/WarnNotImplemented.hs +++ b/kore/src/Kore/Log/WarnNotImplemented.hs @@ -34,6 +34,7 @@ instance InternalVariable variable => Entry (WarnNotImplemented variable) where entrySeverity _ = Warning oneLineDoc (WarnNotImplemented (Application Symbol{symbolAttributes} _)) = Pretty.pretty $ sourceLocation symbolAttributes + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warn when we try to evaluate a partial builtin function on unimplemented cases" warnNotImplemented :: diff --git a/kore/src/Kore/Log/WarnRestartSolver.hs b/kore/src/Kore/Log/WarnRestartSolver.hs index 7f5e2d9e20..f70dd69815 100644 --- a/kore/src/Kore/Log/WarnRestartSolver.hs +++ b/kore/src/Kore/Log/WarnRestartSolver.hs @@ -35,6 +35,7 @@ instance Pretty WarnRestartSolver where instance Entry WarnRestartSolver where entrySeverity _ = Warning oneLineDoc _ = "WarnRestartSolver" + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warning raised to notify the user that the solver has\ \ crashed and the backend will attempt to restart it,\ diff --git a/kore/src/Kore/Log/WarnStepTimeout.hs b/kore/src/Kore/Log/WarnStepTimeout.hs index c2961b553c..bf28f28baa 100644 --- a/kore/src/Kore/Log/WarnStepTimeout.hs +++ b/kore/src/Kore/Log/WarnStepTimeout.hs @@ -41,6 +41,8 @@ instance Entry WarnStepTimeout where oneLineDoc _ = "WarnStepTimeout" + oneLineContextDoc _ = single CtxWarn + helpDoc _ = "warn when a step has timed out" warnStepManualTimeout :: MonadLog log => Int -> log () diff --git a/kore/src/Kore/Log/WarnStuckClaimState.hs b/kore/src/Kore/Log/WarnStuckClaimState.hs index 99a7cfc869..f7aece7ece 100644 --- a/kore/src/Kore/Log/WarnStuckClaimState.hs +++ b/kore/src/Kore/Log/WarnStuckClaimState.hs @@ -75,6 +75,7 @@ instance Entry WarnStuckClaimState where , Pretty.colon , Pretty.pretty @SourceLocation $ from claim ] + oneLineContextDoc _ = single CtxWarn helpDoc _ = "distinguish the ways a proof can become stuck" diff --git a/kore/src/Kore/Log/WarnSymbolSMTRepresentation.hs b/kore/src/Kore/Log/WarnSymbolSMTRepresentation.hs index f4091fd282..839b373ab3 100644 --- a/kore/src/Kore/Log/WarnSymbolSMTRepresentation.hs +++ b/kore/src/Kore/Log/WarnSymbolSMTRepresentation.hs @@ -46,6 +46,7 @@ instance Entry WarnSymbolSMTRepresentation where entrySeverity _ = Warning oneLineDoc (WarnSymbolSMTRepresentation Symbol{symbolAttributes}) = Pretty.pretty (sourceLocation symbolAttributes) + oneLineContextDoc _ = map CLNullary [CtxSMT, CtxWarn] helpDoc _ = "warn when a symbol cannot be translated for the SMT solver, despite being given an explicit translation" diff --git a/kore/src/Kore/Log/WarnTrivialClaim.hs b/kore/src/Kore/Log/WarnTrivialClaim.hs index bf8cf100ad..c7dad7ca4b 100644 --- a/kore/src/Kore/Log/WarnTrivialClaim.hs +++ b/kore/src/Kore/Log/WarnTrivialClaim.hs @@ -57,6 +57,7 @@ instance Entry WarnTrivialClaim where , Pretty.colon , Pretty.pretty @SourceLocation $ from claim ] + oneLineContextDoc _ = single CtxWarn helpDoc _ = "warn when a claim is proven without taking any steps" warnProvenClaimZeroDepth :: diff --git a/kore/src/Kore/Log/WarnUnexploredBranches.hs b/kore/src/Kore/Log/WarnUnexploredBranches.hs index e0d2138d64..8ecac43db8 100644 --- a/kore/src/Kore/Log/WarnUnexploredBranches.hs +++ b/kore/src/Kore/Log/WarnUnexploredBranches.hs @@ -36,6 +36,7 @@ instance Entry WarnUnexploredBranches where oneLineDoc (WarnUnexploredBranches count) = Pretty.pretty count Pretty.<+> "branches were still unexplored when the action failed." + oneLineContextDoc _ = single CtxWarn helpDoc _ = "indicate whether and how many unexplored branches existed when failing." diff --git a/kore/src/Kore/Log/WarnUnsimplified.hs b/kore/src/Kore/Log/WarnUnsimplified.hs index 933b9a7b75..3d50e68705 100644 --- a/kore/src/Kore/Log/WarnUnsimplified.hs +++ b/kore/src/Kore/Log/WarnUnsimplified.hs @@ -89,11 +89,13 @@ instance Pretty WarnUnsimplifiedCondition where instance Entry WarnUnsimplifiedPredicate where entrySeverity _ = Debug oneLineDoc WarnUnsimplifiedPredicate{limit} = Pretty.pretty limit + oneLineContextDoc _ = single CtxDetail helpDoc _ = "warn when a predicate is not simplified" instance Entry WarnUnsimplifiedCondition where entrySeverity _ = Debug oneLineDoc WarnUnsimplifiedCondition{limit} = Pretty.pretty limit + oneLineContextDoc _ = single CtxDetail helpDoc _ = "warn when a condition is not simplified" warnUnsimplifiedPredicate :: diff --git a/kore/src/Kore/Rewrite/Step.hs b/kore/src/Kore/Rewrite/Step.hs index 14dcb746f1..533debdfc5 100644 --- a/kore/src/Kore/Rewrite/Step.hs +++ b/kore/src/Kore/Rewrite/Step.hs @@ -75,7 +75,7 @@ import Kore.Log.DebugAppliedRewriteRules ( import Kore.Log.DebugAttemptedRewriteRules ( whileDebugAttemptRewriteRule, ) -import Kore.Log.DebugContext (inContext) +import Kore.Log.DebugContext (SimpleContext (CtxConstraint, CtxRemainder), inContext) import Kore.Log.DecidePredicateUnknown (srcLoc) import Kore.Rewrite.Result qualified as Result import Kore.Rewrite.Result qualified as Results @@ -181,7 +181,7 @@ unifyRule sideCondition initial rule = do let ruleRequires = precondition rule requires' = Condition.fromPredicate ruleRequires unification' <- - inContext "constraint" $ + inContext CtxConstraint $ Simplifier.simplifyCondition sideCondition' (unification <> requires') @@ -297,7 +297,7 @@ applyInitialConditions :: -- | Unification conditions Condition RewritingVariableName -> LogicT Simplifier (Condition RewritingVariableName) -applyInitialConditions sideCondition initial unification = inContext "apply-initial-condition" $ do +applyInitialConditions sideCondition initial unification = inContext CtxConstraint $ do -- Combine the initial conditions and the unification conditions. The axiom -- requires clause is already included in the unification conditions, and -- the conjunction has already been simplified with respect to the initial @@ -323,7 +323,7 @@ applyRemainder :: -- | Remainder Condition RewritingVariableName -> LogicT Simplifier (Pattern RewritingVariableName) -applyRemainder sideCondition initial remainder = inContext "apply-remainder" $ do +applyRemainder sideCondition initial remainder = inContext CtxRemainder $ do -- Simplify the remainder predicate under the initial conditions. We must -- ensure that functions in the remainder are evaluated using the top-level -- side conditions because we will not re-evaluate them after they are added diff --git a/kore/src/Kore/Simplify/Simplify.hs b/kore/src/Kore/Simplify/Simplify.hs index 73109680d9..45d7445e92 100644 --- a/kore/src/Kore/Simplify/Simplify.hs +++ b/kore/src/Kore/Simplify/Simplify.hs @@ -121,7 +121,7 @@ import Kore.Simplify.OverloadSimplifier (OverloadSimplifier (..)) import Kore.Syntax (Id) import Kore.Syntax.Application import Kore.Unparser -import Log +import Log hiding (UniqueId) import Logic import Prelude.Kore import Pretty qualified diff --git a/kore/src/Kore/Unification/Procedure.hs b/kore/src/Kore/Unification/Procedure.hs index 7bf60a67a1..02326bdc59 100644 --- a/kore/src/Kore/Unification/Procedure.hs +++ b/kore/src/Kore/Unification/Procedure.hs @@ -27,7 +27,7 @@ import Kore.Internal.TermLike import Kore.Log.DebugAttemptUnification ( debugAttemptUnification, ) -import Kore.Log.DebugContext (inContext) +import Kore.Log.DebugContext (SimpleContext (CtxSimplify), inContext) import Kore.Log.DebugUnifyBottom (debugUnifyBottomAndReturnBottom) import Kore.Rewrite.RewritingVariable ( RewritingVariableName, @@ -72,7 +72,7 @@ unificationProcedure sideCondition p1 p2 orCeil <- liftSimplifier $ makeEvaluateTermCeil sideCondition term marker "unify" "CombineCeil" ceil' <- Monad.Unify.scatter orCeil - inContext "ceil-simplify" . lowerLogicT . simplifyCondition sideCondition $ + inContext CtxSimplify . lowerLogicT . simplifyCondition sideCondition $ Conditional.andCondition ceil' condition where p1Sort = termLikeSort p1 diff --git a/kore/src/Log.hs b/kore/src/Log.hs index 0cf4cbb0ed..d05cee9af3 100644 --- a/kore/src/Log.hs +++ b/kore/src/Log.hs @@ -47,47 +47,28 @@ import Control.Monad.Catch ( MonadMask, MonadThrow (throwM), ) -import Control.Monad.Counter ( - CounterT, - ) -import Control.Monad.Except ( - ExceptT, - ) -import Control.Monad.Morph ( - MFunctor, - ) +import Control.Monad.Counter (CounterT) +import Control.Monad.Except (ExceptT) +import Control.Monad.Morph (MFunctor) import Control.Monad.Morph qualified as Monad.Morph -import Control.Monad.RWS.Strict ( - RWST, - ) +import Control.Monad.RWS.Strict (RWST) import Control.Monad.Trans.Accum ( AccumT, mapAccumT, ) import Control.Monad.Trans.Control (MonadBaseControl (..)) -import Control.Monad.Trans.Identity ( - IdentityT, - ) -import Control.Monad.Trans.Maybe ( - MaybeT, - ) +import Control.Monad.Trans.Identity (IdentityT) +import Control.Monad.Trans.Maybe (MaybeT) import Control.Monad.Trans.Reader -import Control.Monad.Trans.State.Strict qualified as Strict ( - StateT, - ) +import Control.Monad.Trans.State.Strict qualified as Strict (StateT) import Data.Aeson qualified as JSON -import Data.Text ( - Text, - pack, - ) +import Data.Text (Text) import GHC.Generics qualified as GHC import GHC.Stack qualified as GHC import Log.Entry import Logic import Prelude.Kore -import Pretty ( - Pretty, - ) +import Pretty (Pretty) import Pretty qualified import Prof @@ -107,9 +88,8 @@ data LogMessage = LogMessage instance Entry LogMessage where entrySeverity LogMessage{severity} = severity oneLineDoc LogMessage{message} = Pretty.pretty message - oneLineContextDoc LogMessage{severity} = [pack $ show severity] + oneLineContextDoc LogMessage{severity} = [severityToContext severity] oneLineJson LogMessage{message} = JSON.toJSON message - oneLineContextJson LogMessage{severity} = JSON.toJSON $ show severity instance Pretty LogMessage where pretty LogMessage{message, callstack} = diff --git a/kore/src/Log/Entry.hs b/kore/src/Log/Entry.hs index f10ddbe012..9413e143de 100644 --- a/kore/src/Log/Entry.hs +++ b/kore/src/Log/Entry.hs @@ -9,12 +9,22 @@ module Log.Entry ( -- * Severity Severity (..), prettySeverity, + severityToContext, -- * Entry Entry (..), SomeEntry (..), someEntry, entryTypeText, + + -- * re-exported ContextLog + CLContext (..), + IdContext (..), + SimpleContext (..), + UniqueId (UNKNOWN), + withId, + withShortId, + single, ) where import Colog ( @@ -45,6 +55,8 @@ import Pretty ( import Pretty qualified import Type.Reflection qualified as Reflection +import Kore.JsonRpc.Types.ContextLog + class (Show entry, Typeable entry) => Entry entry where toEntry :: entry -> SomeEntry toEntry = SomeEntry [] @@ -64,13 +76,7 @@ class (Show entry, Typeable entry) => Entry entry where default oneLineJson :: entry -> JSON.Value oneLineJson entry = JSON.object ["entry" JSON..= entryTypeText (toEntry entry)] - oneLineContextJson :: entry -> JSON.Value - default oneLineContextJson :: entry -> JSON.Value - oneLineContextJson entry = JSON.object ["entry" JSON..= entryTypeText (toEntry entry)] - - oneLineContextDoc :: entry -> [Text] - default oneLineContextDoc :: entry -> [Text] - oneLineContextDoc = (: []) . entryTypeText . toEntry + oneLineContextDoc :: entry -> [CLContext] contextDoc :: entry -> Maybe (Pretty.Doc ann) contextDoc = const Nothing @@ -98,6 +104,7 @@ instance Entry SomeEntry where longDoc (SomeEntry _ entry) = longDoc entry oneLineDoc (SomeEntry _ entry) = oneLineDoc entry contextDoc (SomeEntry _ entry) = contextDoc entry + oneLineContextDoc (SomeEntry _ entry) = oneLineContextDoc entry someEntry :: (Entry e1, Entry e2) => Prism SomeEntry SomeEntry e1 e2 someEntry = Lens.prism' toEntry fromEntry @@ -108,3 +115,20 @@ entryTypeText (SomeEntry _ entry) = prettySeverity :: Severity -> Pretty.Doc ann prettySeverity = Pretty.pretty . show + +severityToContext :: Severity -> CLContext +severityToContext = + CLNullary . \case + Debug -> CtxDetail + Info -> CtxInfo + Warning -> CtxWarn + Error -> CtxError + +withId :: (UniqueId -> IdContext) -> Text -> CLContext +c `withId` i = CLWithId $ c $ LongId i + +withShortId :: (UniqueId -> IdContext) -> Text -> CLContext +c `withShortId` i = CLWithId $ c $ ShortId i + +single :: SimpleContext -> [CLContext] +single c = [CLNullary c]