Use Maybe IO.Handle in simplified config

Author: geo2a

kore/src/Kore/Equation/Application.hs

@@ -261,10 +261,12 @@ applyEquation _ term equation result = do
     let results = OrPattern.fromPattern result
     debugApplyEquation equation result
     doTracing <- liftSimplifier $ asks Simplifier.tracingEnabled
-    when doTracing $
+    when (isJust doTracing) emitEquationTrace
+    pure results
+  where
+    emitEquationTrace =
         modify $
             second (|> SimplifierTrace term (Attribute.uniqueId $ attributes equation) result)
-    pure results
 
 {- | Use a 'MatchResult' to instantiate an 'Equation'.
 

kore/src/Kore/Exec.hs

@@ -495,7 +495,8 @@ rpcExec
       where
         simplifierRun
             | tracingEnabled =
-                fmap snd . evalSimplifierLogged verifiedModule' sortGraph overloadGraph metadataTools equations
+                -- FIXME: we need to pass the log stream handle to evalSimplifierLogged here
+                evalSimplifierLogged Nothing verifiedModule' sortGraph overloadGraph metadataTools equations
             | otherwise =
                 evalSimplifier verifiedModule' sortGraph overloadGraph metadataTools equations
 

kore/src/Kore/JsonRpc.hs

@@ -752,12 +752,15 @@ respond serverState moduleName runSMT =
             , equations
             }
             | doTracing =
-                evalSimplifierLogged
-                    verifiedModule
-                    sortGraph
-                    overloadGraph
-                    metadataTools
-                    equations
+                -- FIXME: we need to pass the log stream handle to evalSimplifierLogged here
+                fmap (Seq.empty,)
+                    . evalSimplifierLogged
+                        Nothing
+                        verifiedModule
+                        sortGraph
+                        overloadGraph
+                        metadataTools
+                        equations
             | otherwise =
                 fmap (Seq.empty,)
                     . evalSimplifier

kore/src/Kore/Simplify/API.hs

@@ -19,7 +19,6 @@ import Data.Map.Strict (
     Map,
  )
 import Data.Map.Strict qualified as Map
-import Data.Sequence (Seq)
 import Kore.Attribute.Symbol qualified as Attribute (
     Symbol,
  )
@@ -69,6 +68,7 @@ import Prof
 import SMT (
     SMT,
  )
+import System.IO qualified as IO
 
 traceProfSimplify ::
     MonadProf prof =>
@@ -85,7 +85,7 @@ traceProfSimplify =
         . Pattern.toTermLike
 
 mkSimplifierEnv ::
-    Bool ->
+    Maybe IO.Handle ->
     VerifiedModuleSyntax Attribute.Symbol ->
     SortGraph ->
     OverloadGraph ->
@@ -172,21 +172,28 @@ evalSimplifier ::
     Map AxiomIdentifier [Equation VariableName] ->
     Simplifier a ->
     SMT a
-evalSimplifier verifiedModule sortGraph overloadGraph metadataTools rawEquations simplifier = do
-    env <- mkSimplifierEnv False verifiedModule sortGraph overloadGraph metadataTools rawEquations
-    runSimplifier env simplifier
+evalSimplifier = evalSimplifierLogged Nothing
 
+-- | Evaluate a simplifier computation, logging the simplification into the provided 'Handle'
 evalSimplifierLogged ::
+    Maybe IO.Handle ->
     VerifiedModuleSyntax Attribute.Symbol ->
     SortGraph ->
     OverloadGraph ->
     SmtMetadataTools Attribute.Symbol ->
     Map AxiomIdentifier [Equation VariableName] ->
     Simplifier a ->
-    SMT (Seq SimplifierTrace, a)
-evalSimplifierLogged verifiedModule sortGraph overloadGraph metadataTools rawEquations simplifier = do
-    env <- mkSimplifierEnv True verifiedModule sortGraph overloadGraph metadataTools rawEquations
-    runSimplifierLogged env simplifier
+    SMT a
+evalSimplifierLogged simlifierTraceHandle verifiedModule sortGraph overloadGraph metadataTools rawEquations simplifier = do
+    env <-
+        mkSimplifierEnv
+            simlifierTraceHandle
+            verifiedModule
+            sortGraph
+            overloadGraph
+            metadataTools
+            rawEquations
+    runSimplifier env simplifier
 
 evalSimplifierProofs ::
     VerifiedModule Attribute.Symbol ->

kore/src/Kore/Simplify/Simplify.hs

@@ -57,7 +57,6 @@ module Kore.Simplify.Simplify (
     -- * Re-exports
     MonadSMT,
     MonadLog,
-    runSimplifierLogged,
     SimplifierTrace (..),
 ) where
 
@@ -132,6 +131,7 @@ import SMT (
     MonadSMT (..),
     SMT,
  )
+import System.IO qualified as IO
 
 -- * Simplifier
 
@@ -151,7 +151,7 @@ data Env = Env
     , injSimplifier :: !InjSimplifier
     , overloadSimplifier :: !OverloadSimplifier
     , hookedSymbols :: !(Map Id Text)
-    , tracingEnabled :: Bool
+    , tracingEnabled :: Maybe IO.Handle
     }
 
 data SimplifierTrace = SimplifierTrace
@@ -186,14 +186,6 @@ runSimplifier :: Env -> Simplifier a -> SMT a
 runSimplifier env (Simplifier simplifier) =
     runReaderT (evalStateT simplifier (initCache, mempty)) env
 
-runSimplifierLogged :: Env -> Simplifier a -> SMT (Seq SimplifierTrace, a)
-runSimplifierLogged env (Simplifier simplifier) =
-    runReaderT
-        ( runStateT simplifier (initCache, mempty) >>= \(res, (_, logs)) ->
-            pure (logs, res)
-        )
-        env
-
 -- | Run a simplification, returning the results along all branches.
 runSimplifierBranch ::
     Env ->