Use source location in rewrite trace (#3382)

* replace TermLike with SourceLocation in DebugInitialClaim

* use instance Pretty SourceLocation

Co-authored-by: Ana Pantilie <[email protected]>

Author: alexd1971

kore/src/Kore/Log/DebugRewriteTrace.hs

@@ -35,6 +35,7 @@ import Data.Yaml (
     toJSON,
     (.=),
  )
+import Kore.Attribute.SourceLocation (SourceLocation (..))
 import Kore.Attribute.UniqueId (
     UniqueId (..),
  )
@@ -83,7 +84,7 @@ import Pretty (
     renderText,
  )
 
-data DebugInitialClaim = DebugInitialClaim UniqueId (TermLike VariableName)
+data DebugInitialClaim = DebugInitialClaim UniqueId SourceLocation
     deriving stock (Show)
 
 newtype DebugInitialPattern = DebugInitialPattern (TermLike VariableName)
@@ -131,7 +132,7 @@ instance ToJSON DebugInitialClaim where
     toJSON (DebugInitialClaim uniqueId claim) =
         object
             [ "task" .= ("reachability" :: Text)
-            , "claim" .= unparseOneLine claim
+            , "claim" .= show (pretty claim)
             , "claim-id" .= maybe Null toJSON (getUniqueId uniqueId)
             ]
 
@@ -202,7 +203,7 @@ unparseOneLine = renderText . layoutOneLine . unparse
 debugInitialClaim ::
     MonadLog log =>
     UniqueId ->
-    TermLike VariableName ->
+    SourceLocation ->
     log ()
 debugInitialClaim uniqueId claimPattern = logEntry $ DebugInitialClaim uniqueId claimPattern
 

kore/src/Kore/Reachability/Prove.hs

@@ -87,9 +87,6 @@ import Kore.Log.DebugTransition (
 import Kore.Log.InfoProofDepth
 import Kore.Log.WarnStuckClaimState
 import Kore.Log.WarnTrivialClaim
-import Kore.Reachability.AllPathClaim (
-    allPathRuleToTerm,
- )
 import Kore.Reachability.Claim
 import Kore.Reachability.ClaimState (
     ClaimState,
@@ -98,9 +95,6 @@ import Kore.Reachability.ClaimState (
     extractUnproven,
  )
 import Kore.Reachability.ClaimState qualified as ClaimState
-import Kore.Reachability.OnePathClaim (
-    onePathRuleToTerm,
- )
 import Kore.Reachability.Prim as Prim (
     Prim (..),
  )
@@ -291,8 +285,8 @@ proveClaimsWorker
             traceExceptT D_OnePath_verifyClaim [debugArg "rule" claim] $ do
                 debugBeginClaim claim
                 debugInitialClaim (from claim) $ case claim of
-                    OnePath term -> onePathRuleToTerm term
-                    AllPath term -> allPathRuleToTerm term
+                    OnePath onePathClaim -> from $ getOnePathClaim onePathClaim
+                    AllPath allPathClaim -> from $ getAllPathClaim allPathClaim
                 result <-
                     lift . lift $
                         proveClaim