From bc2fd5f80e235a1bd00c58e29554aea91afcf4d8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 12 May 2020 13:16:15 +0100
Subject: Add debug to reduction

---
 src/Verismith/Fuzz.hs   |  4 ++--
 src/Verismith/Reduce.hs | 14 ++++++++++++--
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/Verismith/Fuzz.hs b/src/Verismith/Fuzz.hs
index 2fb9f00..278879d 100644
--- a/src/Verismith/Fuzz.hs
+++ b/src/Verismith/Fuzz.hs
@@ -397,7 +397,7 @@ reduction rsrc = do
   simFails <- failedSimulations
   _ <- liftSh $ mapM (red checker datadir) fails
   _ <- liftSh $ mapM redSynth synthFails
-  _ <- liftSh $ mapM (redSim datadir) simFails
+  -- _ <- liftSh $ mapM (redSim datadir) simFails
   return ()
   where
     red checker datadir (SynthResult a b _ _) = do
@@ -490,7 +490,7 @@ fuzz gen = do
     $ conf
       & configProperty
       . propSeed
-      ?~ seed'
+        ?~ seed'
   (tsynth, _) <- titleRun "Synthesis" $ synthesis src
   (tequiv, _) <-
     if (_fuzzOptsNoEquiv opts)
diff --git a/src/Verismith/Reduce.hs b/src/Verismith/Reduce.hs
index 8a5bbbd..956722e 100644
--- a/src/Verismith/Reduce.hs
+++ b/src/Verismith/Reduce.hs
@@ -44,6 +44,7 @@ import Control.Monad (void)
 import Control.Monad.IO.Class (MonadIO, liftIO)
 import Data.ByteString (ByteString)
 import Data.Foldable (foldrM)
+import Data.IORef (newIORef, readIORef, writeIORef)
 import Data.List (nub)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NonEmpty
@@ -681,16 +682,25 @@ reduceSynth ::
   b ->
   (SourceInfo ()) ->
   m (SourceInfo ())
-reduceSynth mt datadir a b = reduce (fromText $ "reduce_" <> toText a <> "_" <> toText b <> ".v") synth
+reduceSynth mt datadir a b src = do
+  counter <- liftSh . liftIO $ newIORef (0 :: Int)
+  reduce (fromText $ prefix <> ".v") (synth counter) src
   where
-    synth src' = liftSh $ do
+    synth counter src' = liftSh $ do
+      count <- liftIO $ readIORef counter
+      liftIO $ writeIORef counter (count + 1)
+      Shelly.mkdir (fromText $ prefix <> "_" <> showT count)
+      current_dir <- Shelly.pwd
+      Shelly.cd (fromText $ prefix <> "_" <> showT count)
       r <- runResultT $ do
         runSynth a src'
         runSynth b src'
         runEquiv mt datadir a b src'
+      Shelly.cd current_dir
       return $ case r of
         Fail (EquivFail _) -> True
         _ -> False
+    prefix = "reduce_" <> toText a <> "_" <> toText b
 
 reduceSynthesis :: (Synthesiser a, MonadSh m) => a -> SourceInfo () -> m (SourceInfo ())
 reduceSynthesis a = reduce (fromText $ "reduce_" <> toText a <> ".v") synth
-- 
cgit