De-duplicate showHashHex

Author: geo2a

booster/library/Booster/Log.hs

@@ -14,6 +14,7 @@ import Booster.Pattern.Base (
     TermAttributes (hash),
     pattern AndTerm,
  )
+import Kore.Util (showHashHex)
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KorePattern, prettyPattern)
 import Control.Monad.IO.Class
@@ -39,12 +40,9 @@ import Data.List.Extra (splitOn, takeEnd)
 import Data.Set qualified as Set
 import Data.String (IsString)
 import Data.Text (Text, pack)
-import Data.Text qualified as Text
 import Data.Text.Lazy qualified as LazyText
-import Data.Word (Word64)
 import GHC.Exts (IsString (..))
 import GHC.TypeLits (KnownSymbol, symbolVal)
-import Numeric (showHex)
 import Prettyprinter (Pretty, pretty)
 
 newtype Logger a = Logger (a -> IO ())
@@ -97,9 +95,6 @@ withContext c = withLogger (\(Logger l) -> Logger $ l . (\(LogMessage ctxt m) ->
 
 newtype TermCtxt = TermCtxt Int
 
-showHashHex :: Int -> Text
-showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ pack $ showHex w64 ""
-
 instance ToLogFormat TermCtxt where
     toTextualLog (TermCtxt hsh) = "term " <> (showHashHex hsh)
 

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -84,6 +84,7 @@ import Booster.Prettyprinter (renderDefault, renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Util (Bound (..), Flag (..))
 import Kore.JsonRpc.Types.Log qualified as KoreRpcLog
+import Kore.Util (showHashHex)
 
 newtype EquationT io a
     = EquationT (ReaderT EquationConfig (ExceptT EquationFailure (StateT EquationState io)) a)

kore-rpc-types/kore-rpc-types.cabal

@@ -37,6 +37,7 @@ common haskell
     OverloadedStrings
     StandaloneDeriving
     ScopedTypeVariables
+    TypeApplications
     TypeFamilies
   default-language: Haskell2010
   build-depends: base >=4.7
@@ -82,6 +83,7 @@ library
   import: haskell
   import: library
   exposed-modules:
+    Kore.Util
     Kore.JsonRpc.Error
     Kore.JsonRpc.Types
     Kore.JsonRpc.Types.Log

kore-rpc-types/src/Kore/Util.hs

@@ -0,0 +1,30 @@
+{- |
+Copyright   : (c) Runtime Verification, 2019-2024
+License     : BSD-3-Clause
+-}
+module Kore.Util (
+    showHashHex,
+    extractLogMessageContext,
+) where
+
+import Data.Char
+import Data.Text (Text)
+import Data.Text qualified as Text
+import Data.Word (Word64)
+import Numeric (showHex)
+
+-- | Represent aa 'Int' as a short hexadecimal string
+showHashHex :: Int -> Text
+showHashHex h = let cutoff = 7 in Text.take cutoff . Text.pack $ showHex (fromIntegral @Int @Word64 h) ""
+
+-- | From a Kore/Booster contextual one-line log message, extract the context prefix
+extractLogMessageContext :: Text -> Text
+extractLogMessageContext = Text.takeWhile isContextCharacter
+  where
+    isContextCharacter :: Char -> Bool
+    isContextCharacter c = isHexDigit c || isLower c || isSpace c || isBracket c
+
+    isBracket = \case
+        '[' -> True
+        ']' -> True
+        _ -> False

kore/src/Kore/Equation/DebugEquation.hs

@@ -33,7 +33,6 @@ import Data.Text (
     Text,
  )
 import Data.Text qualified as Text
-import Data.Word (Word64)
 import Debug
 import GHC.Generics qualified as GHC
 import Generics.SOP qualified as SOP
@@ -61,8 +60,8 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import Kore.Unparser (Unparse (..))
+import Kore.Util (showHashHex)
 import Log
-import Numeric (showHex)
 import Prelude.Kore
 import Pretty (Pretty (..))
 import Pretty qualified
@@ -268,10 +267,7 @@ failureDescription err = shorten . Pretty.renderText . Pretty.layoutOneLine . Pr
     shorten :: Text -> Text
     shorten msg =
         let cutoff = 500
-         in if Text.length msg > cutoff then Text.take 500 msg <> ("...truncated" :: Text) else msg
-
-showHashHex :: Int -> Text
-showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ Text.pack $ showHex w64 ""
+         in if Text.length msg > cutoff then Text.take cutoff msg <> ("...truncated" :: Text) else msg
 
 ruleIdText :: Equation a -> Text
 ruleIdText equation = fromMaybe "UNKNOWN" (Attribute.getUniqueId . Attribute.uniqueId . attributes $ equation)

kore/src/Kore/Log/DebugAttemptedRewriteRules.hs

@@ -14,7 +14,6 @@ module Kore.Log.DebugAttemptedRewriteRules (
 
 import Data.Text (Text)
 import Data.Text qualified as Text
-import Data.Word (Word64)
 import Kore.Attribute.Axiom (
     SourceLocation,
     UniqueId (..),
@@ -31,7 +30,7 @@ import Kore.Internal.Variable (
 import Kore.Rewrite.RewritingVariable
 import Kore.Unparser
 import Log
-import Numeric (showHex)
+import Kore.Util (showHashHex)
 import Prelude.Kore
 import Pretty (
     Pretty (..),
@@ -59,9 +58,6 @@ instance Pretty DebugAttemptedRewriteRules where
             , Pretty.indent 2 . unparse $ configuration
             ]
 
-showHashHex :: Int -> Text
-showHashHex h = let w64 :: Word64 = fromIntegral h in Text.take 7 $ Text.pack $ showHex w64 ""
-
 shortenRuleId :: Text -> Text
 shortenRuleId msg = Text.take 8 msg