{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell #-}

-- |
-- Module      : Verismith.Fuzz
-- Description : Environment to run the simulator and synthesisers in a matrix.
-- Copyright   : (c) 2019, Yann Herklotz
-- License     : GPL-3
-- Maintainer  : yann [at] yannherklotz [dot] com
-- Stability   : experimental
-- Portability : POSIX
--
-- Environment to run the simulator and synthesisers in a matrix.
module Verismith.Fuzz
  ( Fuzz (..),
    FuzzOpts (..),
    fuzz,
    fuzzInDir,
    fuzzMultiple,
    fuzzMultipleEMI,
    runFuzz,
    sampleSeed,

    -- * Helpers
    make,
    pop,
  )
where

import Control.DeepSeq (force)
import Control.Exception.Lifted (finally)
import Control.Lens hiding ((<.>))
import Control.Monad (forM, replicateM)
import Control.Monad.IO.Class
import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Monad.Trans.Control (MonadBaseControl)
import Data.ByteString (ByteString)
import Data.List (nubBy, sort)
import Data.Maybe (catMaybes, fromMaybe, isNothing)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Time
import Data.Tuple (swap)
import Hedgehog (Gen)
import qualified Hedgehog.Internal.Gen as Hog
import Hedgehog.Internal.Seed (Seed)
import qualified Hedgehog.Internal.Seed as Hog
import qualified Hedgehog.Internal.Tree as Hog
import Shelly hiding (get, sub)
import Shelly.Lifted (MonadSh, liftSh, sub)
import System.FilePath.Posix (takeBaseName)
import Verismith.Config
import Verismith.CounterEg (CounterEg (..))
import Verismith.EMI
import Verismith.Reduce
import Verismith.Report
import Verismith.Result
import Verismith.Tool.Icarus
import Verismith.Tool.Internal
import Verismith.Tool.Yosys
import Verismith.Utils
import Verismith.Verilog.AST
import Verismith.Verilog.CodeGen
import Prelude hiding (FilePath)

data FuzzOpts = FuzzOpts
  { FuzzOpts -> Maybe FilePath
_fuzzOptsOutput :: !(Maybe FilePath),
    FuzzOpts -> Bool
_fuzzOptsForced :: !Bool,
    FuzzOpts -> Bool
_fuzzOptsKeepAll :: !Bool,
    FuzzOpts -> Int
_fuzzOptsIterations :: {-# UNPACK #-} !Int,
    FuzzOpts -> Bool
_fuzzOptsNoSim :: !Bool,
    FuzzOpts -> Bool
_fuzzOptsNoEquiv :: !Bool,
    FuzzOpts -> Bool
_fuzzOptsNoReduction :: !Bool,
    FuzzOpts -> Config
_fuzzOptsConfig :: {-# UNPACK #-} !Config,
    FuzzOpts -> FilePath
_fuzzDataDir :: !FilePath,
    FuzzOpts -> Bool
_fuzzOptsCrossCheck :: !Bool,
    FuzzOpts -> Maybe Text
_fuzzOptsChecker :: !(Maybe Text)
  }
  deriving (Int -> FuzzOpts -> ShowS
[FuzzOpts] -> ShowS
FuzzOpts -> FilePath
(Int -> FuzzOpts -> ShowS)
-> (FuzzOpts -> FilePath) -> ([FuzzOpts] -> ShowS) -> Show FuzzOpts
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FuzzOpts -> ShowS
showsPrec :: Int -> FuzzOpts -> ShowS
$cshow :: FuzzOpts -> FilePath
show :: FuzzOpts -> FilePath
$cshowList :: [FuzzOpts] -> ShowS
showList :: [FuzzOpts] -> ShowS
Show, FuzzOpts -> FuzzOpts -> Bool
(FuzzOpts -> FuzzOpts -> Bool)
-> (FuzzOpts -> FuzzOpts -> Bool) -> Eq FuzzOpts
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FuzzOpts -> FuzzOpts -> Bool
== :: FuzzOpts -> FuzzOpts -> Bool
$c/= :: FuzzOpts -> FuzzOpts -> Bool
/= :: FuzzOpts -> FuzzOpts -> Bool
Eq)

$(makeLenses ''FuzzOpts)

defaultFuzzOpts :: FuzzOpts
defaultFuzzOpts :: FuzzOpts
defaultFuzzOpts =
  FuzzOpts
    { _fuzzOptsOutput :: Maybe FilePath
_fuzzOptsOutput = Maybe FilePath
forall a. Maybe a
Nothing,
      _fuzzOptsForced :: Bool
_fuzzOptsForced = Bool
False,
      _fuzzOptsKeepAll :: Bool
_fuzzOptsKeepAll = Bool
False,
      _fuzzOptsIterations :: Int
_fuzzOptsIterations = Int
1,
      _fuzzOptsNoSim :: Bool
_fuzzOptsNoSim = Bool
False,
      _fuzzOptsNoEquiv :: Bool
_fuzzOptsNoEquiv = Bool
False,
      _fuzzOptsNoReduction :: Bool
_fuzzOptsNoReduction = Bool
False,
      _fuzzOptsConfig :: Config
_fuzzOptsConfig = Config
defaultConfig,
      _fuzzDataDir :: FilePath
_fuzzDataDir = Text -> FilePath
fromText Text
".",
      _fuzzOptsCrossCheck :: Bool
_fuzzOptsCrossCheck = Bool
False,
      _fuzzOptsChecker :: Maybe Text
_fuzzOptsChecker = Maybe Text
forall a. Maybe a
Nothing
    }

data FuzzEnv = FuzzEnv
  { FuzzEnv -> [SynthTool]
_getSynthesisers :: ![SynthTool],
    FuzzEnv -> [SimTool]
_getSimulators :: ![SimTool],
    FuzzEnv -> Yosys
_yosysInstance :: {-# UNPACK #-} !Yosys,
    FuzzEnv -> FuzzOpts
_fuzzEnvOpts :: {-# UNPACK #-} !FuzzOpts
  }
  deriving (FuzzEnv -> FuzzEnv -> Bool
(FuzzEnv -> FuzzEnv -> Bool)
-> (FuzzEnv -> FuzzEnv -> Bool) -> Eq FuzzEnv
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FuzzEnv -> FuzzEnv -> Bool
== :: FuzzEnv -> FuzzEnv -> Bool
$c/= :: FuzzEnv -> FuzzEnv -> Bool
/= :: FuzzEnv -> FuzzEnv -> Bool
Eq, Int -> FuzzEnv -> ShowS
[FuzzEnv] -> ShowS
FuzzEnv -> FilePath
(Int -> FuzzEnv -> ShowS)
-> (FuzzEnv -> FilePath) -> ([FuzzEnv] -> ShowS) -> Show FuzzEnv
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FuzzEnv -> ShowS
showsPrec :: Int -> FuzzEnv -> ShowS
$cshow :: FuzzEnv -> FilePath
show :: FuzzEnv -> FilePath
$cshowList :: [FuzzEnv] -> ShowS
showList :: [FuzzEnv] -> ShowS
Show)

$(makeLenses ''FuzzEnv)

data FuzzState = FuzzState
  { FuzzState -> [SynthResult]
_fuzzSynthResults :: ![SynthResult],
    FuzzState -> [SimResult]
_fuzzSimResults :: ![SimResult],
    FuzzState -> [SynthStatus]
_fuzzSynthStatus :: ![SynthStatus]
  }
  deriving (FuzzState -> FuzzState -> Bool
(FuzzState -> FuzzState -> Bool)
-> (FuzzState -> FuzzState -> Bool) -> Eq FuzzState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FuzzState -> FuzzState -> Bool
== :: FuzzState -> FuzzState -> Bool
$c/= :: FuzzState -> FuzzState -> Bool
/= :: FuzzState -> FuzzState -> Bool
Eq, Int -> FuzzState -> ShowS
[FuzzState] -> ShowS
FuzzState -> FilePath
(Int -> FuzzState -> ShowS)
-> (FuzzState -> FilePath)
-> ([FuzzState] -> ShowS)
-> Show FuzzState
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FuzzState -> ShowS
showsPrec :: Int -> FuzzState -> ShowS
$cshow :: FuzzState -> FilePath
show :: FuzzState -> FilePath
$cshowList :: [FuzzState] -> ShowS
showList :: [FuzzState] -> ShowS
Show)

$(makeLenses ''FuzzState)

type Frequency a = [(Seed, a)] -> [(Int, Gen (Seed, a))]

-- | The main type for the fuzzing, which contains an environment that can be
-- read from and the current state of all the results.
type Fuzz m = StateT FuzzState (ReaderT FuzzEnv m)

type MonadFuzz m = (MonadBaseControl IO m, MonadIO m, MonadSh m)

runFuzz :: (MonadIO m) => FuzzOpts -> Yosys -> Fuzz Sh a -> m a
runFuzz :: forall (m :: * -> *) a.
MonadIO m =>
FuzzOpts -> Yosys -> Fuzz Sh a -> m a
runFuzz FuzzOpts
fo Yosys
yos Fuzz Sh a
m = Sh a -> m a
forall (m :: * -> *) a. MonadIO m => Sh a -> m a
shelly (Sh a -> m a) -> Sh a -> m a
forall a b. (a -> b) -> a -> b
$ FuzzOpts -> Yosys -> Fuzz Sh a -> Sh a
forall (m :: * -> *) b.
Monad m =>
FuzzOpts -> Yosys -> Fuzz m b -> m b
runFuzz' FuzzOpts
fo Yosys
yos Fuzz Sh a
m

runFuzz' :: (Monad m) => FuzzOpts -> Yosys -> Fuzz m b -> m b
runFuzz' :: forall (m :: * -> *) b.
Monad m =>
FuzzOpts -> Yosys -> Fuzz m b -> m b
runFuzz' FuzzOpts
fo Yosys
yos Fuzz m b
m =
  ReaderT FuzzEnv m b -> FuzzEnv -> m b
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
    (Fuzz m b -> FuzzState -> ReaderT FuzzEnv m b
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Fuzz m b
m ([SynthResult] -> [SimResult] -> [SynthStatus] -> FuzzState
FuzzState [] [] []))
    ( FuzzEnv
        { _getSynthesisers :: [SynthTool]
_getSynthesisers =
            ( [SynthTool] -> [SynthTool]
forall a. NFData a => a -> a
force ([SynthTool] -> [SynthTool]) -> [SynthTool] -> [SynthTool]
forall a b. (a -> b) -> a -> b
$
                SynthTool
defaultIdentitySynth SynthTool -> [SynthTool] -> [SynthTool]
forall a. a -> [a] -> [a]
:
                (SynthDescription -> SynthTool
descriptionToSynth (SynthDescription -> SynthTool)
-> [SynthDescription] -> [SynthTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config
conf Config
-> Getting [SynthDescription] Config [SynthDescription]
-> [SynthDescription]
forall s a. s -> Getting a s a -> a
^. Getting [SynthDescription] Config [SynthDescription]
Lens' Config [SynthDescription]
configSynthesisers)
            ),
          _getSimulators :: [SimTool]
_getSimulators = ([SimTool] -> [SimTool]
forall a. NFData a => a -> a
force ([SimTool] -> [SimTool]) -> [SimTool] -> [SimTool]
forall a b. (a -> b) -> a -> b
$ SimDescription -> SimTool
descriptionToSim (SimDescription -> SimTool) -> [SimDescription] -> [SimTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config
conf Config
-> Getting [SimDescription] Config [SimDescription]
-> [SimDescription]
forall s a. s -> Getting a s a -> a
^. Getting [SimDescription] Config [SimDescription]
Lens' Config [SimDescription]
configSimulators),
          _yosysInstance :: Yosys
_yosysInstance = Yosys
yos,
          _fuzzEnvOpts :: FuzzOpts
_fuzzEnvOpts = FuzzOpts
fo
        }
    )
  where
    conf :: Config
conf = FuzzOpts -> Config
_fuzzOptsConfig FuzzOpts
fo

askConfig :: (Monad m) => Fuzz m Config
askConfig :: forall (m :: * -> *). Monad m => Fuzz m Config
askConfig = (FuzzEnv -> Config) -> StateT FuzzState (ReaderT FuzzEnv m) Config
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (FuzzOpts -> Config
_fuzzOptsConfig (FuzzOpts -> Config) -> (FuzzEnv -> FuzzOpts) -> FuzzEnv -> Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzEnv -> FuzzOpts
_fuzzEnvOpts)

askOpts :: (Monad m) => Fuzz m FuzzOpts
askOpts :: forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts = (FuzzEnv -> FuzzOpts)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FuzzEnv -> FuzzOpts
_fuzzEnvOpts

genMethod :: Config -> Maybe Seed -> Gen a -> m (Seed, a)
genMethod Config
conf Maybe Seed
seed Gen a
gen =
  case Text -> Text
T.toLower (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Config
conf Config -> Getting Text Config Text -> Text
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const Text ConfProperty)
-> Config -> Const Text Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const Text ConfProperty)
 -> Config -> Const Text Config)
-> ((Text -> Const Text Text)
    -> ConfProperty -> Const Text ConfProperty)
-> Getting Text Config Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Const Text Text)
-> ConfProperty -> Const Text ConfProperty
Lens' ConfProperty Text
propSampleMethod of
    Text
"hat" -> do
      Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT Text
"Using the hat function"
      Frequency a -> m (Seed, a)
forall {m :: * -> *}.
(MonadSh m, MonadIO m) =>
Frequency a -> m (Seed, a)
sv Frequency a
forall a. Frequency a
hatFreqs
    Text
"mean" -> do
      Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT Text
"Using the mean function"
      Frequency a -> m (Seed, a)
forall {m :: * -> *}.
(MonadSh m, MonadIO m) =>
Frequency a -> m (Seed, a)
sv Frequency a
forall a. Source a => Frequency a
meanFreqs
    Text
"median" -> do
      Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT Text
"Using the median function"
      Frequency a -> m (Seed, a)
forall {m :: * -> *}.
(MonadSh m, MonadIO m) =>
Frequency a -> m (Seed, a)
sv Frequency a
forall a. Frequency a
medianFreqs
    Text
_ -> do
      Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT Text
"Using first seed"
      Maybe Seed -> Gen a -> m (Seed, a)
forall (m :: * -> *) a.
MonadSh m =>
Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed Maybe Seed
seed Gen a
gen
  where
    sv :: Frequency a -> m (Seed, a)
sv Frequency a
a = Frequency a -> Int -> Maybe Seed -> Gen a -> m (Seed, a)
forall (m :: * -> *) a.
(MonadSh m, MonadIO m, Source a, Ord a) =>
Frequency a -> Int -> Maybe Seed -> Gen a -> m (Seed, a)
sampleVerilog Frequency a
a (Config
conf Config -> Getting Int Config Int -> Int
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const Int ConfProperty)
-> Config -> Const Int Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const Int ConfProperty)
 -> Config -> Const Int Config)
-> ((Int -> Const Int Int)
    -> ConfProperty -> Const Int ConfProperty)
-> Getting Int Config Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Const Int Int) -> ConfProperty -> Const Int ConfProperty
Lens' ConfProperty Int
propSampleSize) Maybe Seed
seed Gen a
gen

relativeFuzzReport :: (MonadSh m) => FuzzReport -> m FuzzReport
relativeFuzzReport :: forall (m :: * -> *). MonadSh m => FuzzReport -> m FuzzReport
relativeFuzzReport fr :: FuzzReport
fr@(FuzzReport FilePath
dir [SynthResult]
_ [SimResult]
_ [SynthStatus]
_ Int
_ NominalDiffTime
_ NominalDiffTime
_ NominalDiffTime
_) = Sh FuzzReport -> m FuzzReport
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh FuzzReport -> m FuzzReport) -> Sh FuzzReport -> m FuzzReport
forall a b. (a -> b) -> a -> b
$ do
  FilePath
newPath <- FilePath -> Sh FilePath
relPath FilePath
dir
  FuzzReport -> Sh FuzzReport
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (FuzzReport -> Sh FuzzReport) -> FuzzReport -> Sh FuzzReport
forall a b. (a -> b) -> a -> b
$ ((FilePath -> Identity FilePath)
-> FuzzReport -> Identity FuzzReport
Lens' FuzzReport FilePath
fuzzDir ((FilePath -> Identity FilePath)
 -> FuzzReport -> Identity FuzzReport)
-> FilePath -> FuzzReport -> FuzzReport
forall s t a b. ASetter s t a b -> b -> s -> t
.~ FilePath
newPath) FuzzReport
fr

filterSynth :: SynthResult -> Bool
filterSynth :: SynthResult -> Bool
filterSynth (SynthResult SynthTool
_ SynthTool
_ (Pass ()
_) NominalDiffTime
_) = Bool
True
filterSynth SynthResult
_ = Bool
False

filterSim :: SimResult -> Bool
filterSim :: SimResult -> Bool
filterSim (SimResult SynthTool
_ SimTool
_ [ByteString]
_ (Pass ByteString
_) NominalDiffTime
_) = Bool
True
filterSim SimResult
_ = Bool
False

filterSynthStat :: SynthStatus -> Bool
filterSynthStat :: SynthStatus -> Bool
filterSynthStat (SynthStatus SynthTool
_ (Pass ()
_) NominalDiffTime
_) = Bool
True
filterSynthStat SynthStatus
_ = Bool
False

passedFuzz :: FuzzReport -> Bool
passedFuzz :: FuzzReport -> Bool
passedFuzz (FuzzReport FilePath
_ [SynthResult]
synth [SimResult]
sim [SynthStatus]
synthstat Int
_ NominalDiffTime
_ NominalDiffTime
_ NominalDiffTime
_) =
  (Int
passedSynth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
passedSim Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
passedSynthStat) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
  where
    passedSynth :: Int
passedSynth = [SynthResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SynthResult] -> Int) -> [SynthResult] -> Int
forall a b. (a -> b) -> a -> b
$ (SynthResult -> Bool) -> [SynthResult] -> [SynthResult]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SynthResult -> Bool) -> SynthResult -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynthResult -> Bool
filterSynth) [SynthResult]
synth
    passedSim :: Int
passedSim = [SimResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SimResult] -> Int) -> [SimResult] -> Int
forall a b. (a -> b) -> a -> b
$ (SimResult -> Bool) -> [SimResult] -> [SimResult]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SimResult -> Bool) -> SimResult -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimResult -> Bool
filterSim) [SimResult]
sim
    passedSynthStat :: Int
passedSynthStat = [SynthStatus] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([SynthStatus] -> Int) -> [SynthStatus] -> Int
forall a b. (a -> b) -> a -> b
$ (SynthStatus -> Bool) -> [SynthStatus] -> [SynthStatus]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SynthStatus -> Bool) -> SynthStatus -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynthStatus -> Bool
filterSynthStat) [SynthStatus]
synthstat

synthesisers :: (Monad m) => Fuzz m [SynthTool]
synthesisers :: forall (m :: * -> *). Monad m => Fuzz m [SynthTool]
synthesisers = ReaderT FuzzEnv m [SynthTool]
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthTool]
forall (m :: * -> *) a. Monad m => m a -> StateT FuzzState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReaderT FuzzEnv m [SynthTool]
 -> StateT FuzzState (ReaderT FuzzEnv m) [SynthTool])
-> ReaderT FuzzEnv m [SynthTool]
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthTool]
forall a b. (a -> b) -> a -> b
$ (FuzzEnv -> [SynthTool]) -> ReaderT FuzzEnv m [SynthTool]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks FuzzEnv -> [SynthTool]
_getSynthesisers

-- simulators :: (Monad m) => Fuzz () m [SimTool]
-- simulators = lift $ asks getSimulators

combinations :: [a] -> [b] -> [(a, b)]
combinations :: forall a b. [a] -> [b] -> [(a, b)]
combinations [a]
l1 [b]
l2 = [(a
x, b
y) | a
x <- [a]
l1, b
y <- [b]
l2]

logT :: (MonadSh m) => Text -> m ()
logT :: forall (m :: * -> *). MonadSh m => Text -> m ()
logT = Sh () -> m ()
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> m ()) -> (Text -> Sh ()) -> Text -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Sh ()
logger

timeit :: (MonadIO m, MonadSh m) => m a -> m (NominalDiffTime, a)
timeit :: forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
m a -> m (NominalDiffTime, a)
timeit m a
a = do
  UTCTime
start <- IO UTCTime -> m UTCTime
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO UTCTime
getCurrentTime
  a
result <- m a
a
  UTCTime
end <- IO UTCTime -> m UTCTime
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO UTCTime
getCurrentTime
  (NominalDiffTime, a) -> m (NominalDiffTime, a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
end UTCTime
start, a
result)

synthesis :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
synthesis :: forall (m :: * -> *) ann.
(MonadBaseControl IO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
synthesis SourceInfo ann
src = do
  [SynthTool]
synth <- Fuzz m [SynthTool]
forall (m :: * -> *). Monad m => Fuzz m [SynthTool]
synthesisers
  [(NominalDiffTime, Result Failed ())]
resTimes <- Sh [(NominalDiffTime, Result Failed ())]
-> StateT
     FuzzState (ReaderT FuzzEnv m) [(NominalDiffTime, Result Failed ())]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [(NominalDiffTime, Result Failed ())]
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      [(NominalDiffTime, Result Failed ())])
-> Sh [(NominalDiffTime, Result Failed ())]
-> StateT
     FuzzState (ReaderT FuzzEnv m) [(NominalDiffTime, Result Failed ())]
forall a b. (a -> b) -> a -> b
$ (SynthTool -> Sh (NominalDiffTime, Result Failed ()))
-> [SynthTool] -> Sh [(NominalDiffTime, Result Failed ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SynthTool -> Sh (NominalDiffTime, Result Failed ())
forall {a}.
Synthesiser a =>
a -> Sh (NominalDiffTime, Result Failed ())
exec [SynthTool]
synth
  ([SynthStatus] -> Identity [SynthStatus])
-> FuzzState -> Identity FuzzState
Lens' FuzzState [SynthStatus]
fuzzSynthStatus
    (([SynthStatus] -> Identity [SynthStatus])
 -> FuzzState -> Identity FuzzState)
-> [SynthStatus] -> Fuzz m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= [(Result Failed (), NominalDiffTime) -> SynthStatus]
-> [(Result Failed (), NominalDiffTime)] -> [SynthStatus]
forall a b. [a -> b] -> [a] -> [b]
applyList ((Result Failed () -> NominalDiffTime -> SynthStatus)
-> (Result Failed (), NominalDiffTime) -> SynthStatus
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Result Failed () -> NominalDiffTime -> SynthStatus)
 -> (Result Failed (), NominalDiffTime) -> SynthStatus)
-> (SynthTool
    -> Result Failed () -> NominalDiffTime -> SynthStatus)
-> SynthTool
-> (Result Failed (), NominalDiffTime)
-> SynthStatus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynthTool -> Result Failed () -> NominalDiffTime -> SynthStatus
SynthStatus (SynthTool -> (Result Failed (), NominalDiffTime) -> SynthStatus)
-> [SynthTool]
-> [(Result Failed (), NominalDiffTime) -> SynthStatus]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SynthTool]
synth) (((NominalDiffTime, Result Failed ())
 -> (Result Failed (), NominalDiffTime))
-> [(NominalDiffTime, Result Failed ())]
-> [(Result Failed (), NominalDiffTime)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NominalDiffTime, Result Failed ())
-> (Result Failed (), NominalDiffTime)
forall a b. (a, b) -> (b, a)
swap [(NominalDiffTime, Result Failed ())]
resTimes)
  Sh () -> Fuzz m ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> Fuzz m ()) -> Sh () -> Fuzz m ()
forall a b. (a -> b) -> a -> b
$ [(NominalDiffTime, Result Failed ())] -> Sh ()
forall s. Show s => s -> Sh ()
inspect [(NominalDiffTime, Result Failed ())]
resTimes
  where
    exec :: a -> Sh (NominalDiffTime, Result Failed ())
exec a
a = Text
-> Sh (Result Failed ()) -> Sh (NominalDiffTime, Result Failed ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"synthesis with " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Tool a => a -> Text
toText a
a) (Sh (Result Failed ()) -> Sh (NominalDiffTime, Result Failed ()))
-> (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh ()
-> Sh (NominalDiffTime, Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh () -> Sh (NominalDiffTime, Result Failed ()))
-> ResultT Failed Sh () -> Sh (NominalDiffTime, Result Failed ())
forall a b. (a -> b) -> a -> b
$ do
      Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ())
-> (Text -> Sh ()) -> Text -> ResultT Failed Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Sh ()
mkdir_p (FilePath -> Sh ()) -> (Text -> FilePath) -> Text -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
fromText (Text -> ResultT Failed Sh ()) -> Text -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ a -> Text
forall a. Tool a => a -> Text
toText a
a
      FilePath -> ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop (Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ a -> Text
forall a. Tool a => a -> Text
toText a
a) (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ a -> SourceInfo ann -> ResultT Failed Sh ()
forall ann. Show ann => a -> SourceInfo ann -> ResultT Failed Sh ()
forall a ann.
(Synthesiser a, Show ann) =>
a -> SourceInfo ann -> ResultT Failed Sh ()
runSynth a
a SourceInfo ann
src

passedSynthesis :: (MonadSh m) => Fuzz m [SynthTool]
passedSynthesis :: forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
passedSynthesis = (SynthStatus -> SynthTool) -> [SynthStatus] -> [SynthTool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SynthStatus -> SynthTool
toSynth ([SynthStatus] -> [SynthTool])
-> (FuzzState -> [SynthStatus]) -> FuzzState -> [SynthTool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SynthStatus -> Bool) -> [SynthStatus] -> [SynthStatus]
forall a. (a -> Bool) -> [a] -> [a]
filter SynthStatus -> Bool
passed ([SynthStatus] -> [SynthStatus])
-> (FuzzState -> [SynthStatus]) -> FuzzState -> [SynthStatus]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SynthStatus]
_fuzzSynthStatus (FuzzState -> [SynthTool])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    passed :: SynthStatus -> Bool
passed (SynthStatus SynthTool
_ (Pass ()
_) NominalDiffTime
_) = Bool
True
    passed SynthStatus
_ = Bool
False
    toSynth :: SynthStatus -> SynthTool
toSynth (SynthStatus SynthTool
s Result Failed ()
_ NominalDiffTime
_) = SynthTool
s

failedSynthesis :: (MonadSh m) => Fuzz m [SynthTool]
failedSynthesis :: forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
failedSynthesis = (SynthStatus -> SynthTool) -> [SynthStatus] -> [SynthTool]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SynthStatus -> SynthTool
toSynth ([SynthStatus] -> [SynthTool])
-> (FuzzState -> [SynthStatus]) -> FuzzState -> [SynthTool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SynthStatus -> Bool) -> [SynthStatus] -> [SynthStatus]
forall a. (a -> Bool) -> [a] -> [a]
filter SynthStatus -> Bool
failed ([SynthStatus] -> [SynthStatus])
-> (FuzzState -> [SynthStatus]) -> FuzzState -> [SynthStatus]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SynthStatus]
_fuzzSynthStatus (FuzzState -> [SynthTool])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthTool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    failed :: SynthStatus -> Bool
failed (SynthStatus SynthTool
_ (Fail Failed
SynthFail) NominalDiffTime
_) = Bool
True
    failed SynthStatus
_ = Bool
False
    toSynth :: SynthStatus -> SynthTool
toSynth (SynthStatus SynthTool
s Result Failed ()
_ NominalDiffTime
_) = SynthTool
s

make :: (MonadSh m) => FilePath -> m ()
make :: forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
f = Sh () -> m ()
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> m ()) -> Sh () -> m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Sh ()
mkdir_p FilePath
f

pop :: (MonadBaseControl IO m, MonadSh m) => FilePath -> m a -> m a
pop :: forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
f m a
a = do
  FilePath
dir <- Sh FilePath -> m FilePath
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh Sh FilePath
pwd
  m a -> m () -> m a
forall (m :: * -> *) a b.
MonadBaseControl IO m =>
m a -> m b -> m a
finally (Sh () -> m ()
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (FilePath -> Sh ()
cd FilePath
f) m () -> m a -> m a
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m a
a) (m () -> m a) -> (Sh () -> m ()) -> Sh () -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sh () -> m ()
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> m a) -> Sh () -> m a
forall a b. (a -> b) -> a -> b
$ FilePath -> Sh ()
cd FilePath
dir

applyList :: [a -> b] -> [a] -> [b]
applyList :: forall a b. [a -> b] -> [a] -> [b]
applyList [a -> b]
a [a]
b = (a -> b, a) -> b
forall {t} {t}. (t -> t, t) -> t
apply' ((a -> b, a) -> b) -> [(a -> b, a)] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a -> b] -> [a] -> [(a -> b, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a -> b]
a [a]
b where apply' :: (t -> t, t) -> t
apply' (t -> t
a', t
b') = t -> t
a' t
b'

applyLots :: (a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e]
applyLots :: forall a b c d e.
(a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e]
applyLots a -> b -> c -> d -> e
func [(a, b)]
a [(c, d)]
b = [(c, d) -> e] -> [(c, d)] -> [e]
forall a b. [a -> b] -> [a] -> [b]
applyList ((c -> d -> e) -> (c, d) -> e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((c -> d -> e) -> (c, d) -> e)
-> ((a, b) -> c -> d -> e) -> (a, b) -> (c, d) -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> c -> d -> e) -> (a, b) -> c -> d -> e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c -> d -> e
func ((a, b) -> (c, d) -> e) -> [(a, b)] -> [(c, d) -> e]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, b)]
a) [(c, d)]
b

toSynthResult ::
  [(SynthTool, SynthTool)] ->
  [(NominalDiffTime, Result Failed ())] ->
  [SynthResult]
toSynthResult :: [(SynthTool, SynthTool)]
-> [(NominalDiffTime, Result Failed ())] -> [SynthResult]
toSynthResult [(SynthTool, SynthTool)]
a [(NominalDiffTime, Result Failed ())]
b = (SynthTool
 -> SynthTool -> Result Failed () -> NominalDiffTime -> SynthResult)
-> [(SynthTool, SynthTool)]
-> [(Result Failed (), NominalDiffTime)]
-> [SynthResult]
forall a b c d e.
(a -> b -> c -> d -> e) -> [(a, b)] -> [(c, d)] -> [e]
applyLots SynthTool
-> SynthTool -> Result Failed () -> NominalDiffTime -> SynthResult
SynthResult [(SynthTool, SynthTool)]
a ([(Result Failed (), NominalDiffTime)] -> [SynthResult])
-> [(Result Failed (), NominalDiffTime)] -> [SynthResult]
forall a b. (a -> b) -> a -> b
$ ((NominalDiffTime, Result Failed ())
 -> (Result Failed (), NominalDiffTime))
-> [(NominalDiffTime, Result Failed ())]
-> [(Result Failed (), NominalDiffTime)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NominalDiffTime, Result Failed ())
-> (Result Failed (), NominalDiffTime)
forall a b. (a, b) -> (b, a)
swap [(NominalDiffTime, Result Failed ())]
b

toSimResult ::
  SimTool ->
  [ByteString] ->
  [SynthTool] ->
  [(NominalDiffTime, Result Failed ByteString)] ->
  [SimResult]
toSimResult :: SimTool
-> [ByteString]
-> [SynthTool]
-> [(NominalDiffTime, Result Failed ByteString)]
-> [SimResult]
toSimResult SimTool
sima [ByteString]
bs [SynthTool]
as [(NominalDiffTime, Result Failed ByteString)]
b =
  [(Result Failed ByteString, NominalDiffTime) -> SimResult]
-> [(Result Failed ByteString, NominalDiffTime)] -> [SimResult]
forall a b. [a -> b] -> [a] -> [b]
applyList
    ( [(Result Failed ByteString -> NominalDiffTime -> SimResult)
 -> (Result Failed ByteString, NominalDiffTime) -> SimResult]
-> [Result Failed ByteString -> NominalDiffTime -> SimResult]
-> [(Result Failed ByteString, NominalDiffTime) -> SimResult]
forall a b. [a -> b] -> [a] -> [b]
applyList
        (((Result Failed ByteString -> NominalDiffTime -> SimResult)
 -> (Result Failed ByteString, NominalDiffTime) -> SimResult)
-> [(Result Failed ByteString -> NominalDiffTime -> SimResult)
    -> (Result Failed ByteString, NominalDiffTime) -> SimResult]
forall a. a -> [a]
repeat (Result Failed ByteString -> NominalDiffTime -> SimResult)
-> (Result Failed ByteString, NominalDiffTime) -> SimResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry)
        ([[ByteString]
 -> Result Failed ByteString -> NominalDiffTime -> SimResult]
-> [[ByteString]]
-> [Result Failed ByteString -> NominalDiffTime -> SimResult]
forall a b. [a -> b] -> [a] -> [b]
applyList ([SimTool
 -> [ByteString]
 -> Result Failed ByteString
 -> NominalDiffTime
 -> SimResult]
-> [SimTool]
-> [[ByteString]
    -> Result Failed ByteString -> NominalDiffTime -> SimResult]
forall a b. [a -> b] -> [a] -> [b]
applyList (SynthTool
-> SimTool
-> [ByteString]
-> Result Failed ByteString
-> NominalDiffTime
-> SimResult
SimResult (SynthTool
 -> SimTool
 -> [ByteString]
 -> Result Failed ByteString
 -> NominalDiffTime
 -> SimResult)
-> [SynthTool]
-> [SimTool
    -> [ByteString]
    -> Result Failed ByteString
    -> NominalDiffTime
    -> SimResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SynthTool]
as) (SimTool -> [SimTool]
forall a. a -> [a]
repeat SimTool
sima)) ([ByteString] -> [[ByteString]]
forall a. a -> [a]
repeat [ByteString]
bs))
    )
    ([(Result Failed ByteString, NominalDiffTime)] -> [SimResult])
-> [(Result Failed ByteString, NominalDiffTime)] -> [SimResult]
forall a b. (a -> b) -> a -> b
$ ((NominalDiffTime, Result Failed ByteString)
 -> (Result Failed ByteString, NominalDiffTime))
-> [(NominalDiffTime, Result Failed ByteString)]
-> [(Result Failed ByteString, NominalDiffTime)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NominalDiffTime, Result Failed ByteString)
-> (Result Failed ByteString, NominalDiffTime)
forall a b. (a, b) -> (b, a)
swap [(NominalDiffTime, Result Failed ByteString)]
b

toolRun :: (MonadIO m, MonadSh m, Show a) => Text -> m a -> m (NominalDiffTime, a)
toolRun :: forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun Text
t m a
m = do
  Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"Running " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t
  (NominalDiffTime, a)
s <- m a -> m (NominalDiffTime, a)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
m a -> m (NominalDiffTime, a)
timeit m a
m
  Text -> m ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"Finished " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (NominalDiffTime, a) -> Text
forall a. Show a => a -> Text
showT (NominalDiffTime, a)
s
  (NominalDiffTime, a) -> m (NominalDiffTime, a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime, a)
s

equivalence :: (MonadBaseControl IO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
equivalence :: forall (m :: * -> *) ann.
(MonadBaseControl IO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
equivalence SourceInfo ann
src = do
  Bool
doCrossCheck <- (FuzzOpts -> Bool)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) Bool
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> Bool
_fuzzOptsCrossCheck StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  FilePath
datadir <- (FuzzOpts -> FilePath)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> FilePath
_fuzzDataDir StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  Maybe Text
checker <- (FuzzOpts -> Maybe Text)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) (Maybe Text)
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> Maybe Text
_fuzzOptsChecker StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  [SynthTool]
synth <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
passedSynthesis
  Config
conf <- (FuzzOpts -> Config)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) Config
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> Config
_fuzzOptsConfig StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  let synthComb :: [(SynthTool, SynthTool)]
synthComb =
        if Bool
doCrossCheck
          then ((SynthTool, SynthTool) -> (SynthTool, SynthTool) -> Bool)
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (SynthTool, SynthTool) -> (SynthTool, SynthTool) -> Bool
forall {a}. Eq a => (a, a) -> (a, a) -> Bool
tupEq ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> [(SynthTool, SynthTool)]
-> [(SynthTool, SynthTool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SynthTool, SynthTool) -> Bool)
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SynthTool -> SynthTool -> Bool) -> (SynthTool, SynthTool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SynthTool -> SynthTool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a b. (a -> b) -> a -> b
$ [SynthTool] -> [SynthTool] -> [(SynthTool, SynthTool)]
forall a b. [a] -> [b] -> [(a, b)]
combinations [SynthTool]
synth [SynthTool]
synth
          else ((SynthTool, SynthTool) -> (SynthTool, SynthTool) -> Bool)
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (SynthTool, SynthTool) -> (SynthTool, SynthTool) -> Bool
forall {a}. Eq a => (a, a) -> (a, a) -> Bool
tupEq ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> [(SynthTool, SynthTool)]
-> [(SynthTool, SynthTool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SynthTool, SynthTool) -> Bool)
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SynthTool -> SynthTool -> Bool) -> (SynthTool, SynthTool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SynthTool -> SynthTool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)])
-> [(SynthTool, SynthTool)] -> [(SynthTool, SynthTool)]
forall a b. (a -> b) -> a -> b
$ (,) SynthTool
defaultIdentitySynth (SynthTool -> (SynthTool, SynthTool))
-> [SynthTool] -> [(SynthTool, SynthTool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SynthTool]
synth
  [(NominalDiffTime, Result Failed ())]
resTimes <- Sh [(NominalDiffTime, Result Failed ())]
-> StateT
     FuzzState (ReaderT FuzzEnv m) [(NominalDiffTime, Result Failed ())]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [(NominalDiffTime, Result Failed ())]
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      [(NominalDiffTime, Result Failed ())])
-> Sh [(NominalDiffTime, Result Failed ())]
-> StateT
     FuzzState (ReaderT FuzzEnv m) [(NominalDiffTime, Result Failed ())]
forall a b. (a -> b) -> a -> b
$ ((SynthTool, SynthTool) -> Sh (NominalDiffTime, Result Failed ()))
-> [(SynthTool, SynthTool)]
-> Sh [(NominalDiffTime, Result Failed ())]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((SynthTool -> SynthTool -> Sh (NominalDiffTime, Result Failed ()))
-> (SynthTool, SynthTool) -> Sh (NominalDiffTime, Result Failed ())
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Maybe Text
-> Maybe Text
-> FilePath
-> SynthTool
-> SynthTool
-> Sh (NominalDiffTime, Result Failed ())
forall {a} {b}.
(Synthesiser a, Synthesiser b) =>
Maybe Text
-> Maybe Text
-> FilePath
-> a
-> b
-> Sh (NominalDiffTime, Result Failed ())
equiv (Config
conf Config -> Getting (Maybe Text) Config (Maybe Text) -> Maybe Text
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const (Maybe Text) ConfProperty)
-> Config -> Const (Maybe Text) Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const (Maybe Text) ConfProperty)
 -> Config -> Const (Maybe Text) Config)
-> ((Maybe Text -> Const (Maybe Text) (Maybe Text))
    -> ConfProperty -> Const (Maybe Text) ConfProperty)
-> Getting (Maybe Text) Config (Maybe Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Text -> Const (Maybe Text) (Maybe Text))
-> ConfProperty -> Const (Maybe Text) ConfProperty
Lens' ConfProperty (Maybe Text)
propDefaultYosys) Maybe Text
checker FilePath
datadir)) [(SynthTool, SynthTool)]
synthComb
  ([SynthResult] -> Identity [SynthResult])
-> FuzzState -> Identity FuzzState
Lens' FuzzState [SynthResult]
fuzzSynthResults (([SynthResult] -> Identity [SynthResult])
 -> FuzzState -> Identity FuzzState)
-> [SynthResult] -> Fuzz m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= [(SynthTool, SynthTool)]
-> [(NominalDiffTime, Result Failed ())] -> [SynthResult]
toSynthResult [(SynthTool, SynthTool)]
synthComb [(NominalDiffTime, Result Failed ())]
resTimes
  Sh () -> Fuzz m ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> Fuzz m ()) -> Sh () -> Fuzz m ()
forall a b. (a -> b) -> a -> b
$ [(NominalDiffTime, Result Failed ())] -> Sh ()
forall s. Show s => s -> Sh ()
inspect [(NominalDiffTime, Result Failed ())]
resTimes
  where
    tupEq :: (a, a) -> (a, a) -> Bool
tupEq (a
a, a
b) (a
a', a
b') = (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a' Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b') Bool -> Bool -> Bool
|| (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b' Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a')
    equiv :: Maybe Text
-> Maybe Text
-> FilePath
-> a
-> b
-> Sh (NominalDiffTime, Result Failed ())
equiv Maybe Text
yosysloc Maybe Text
checker FilePath
datadir a
a b
b =
      Text
-> Sh (Result Failed ()) -> Sh (NominalDiffTime, Result Failed ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"equivalence check for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Tool a => a -> Text
toText a
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
b)
        (Sh (Result Failed ()) -> Sh (NominalDiffTime, Result Failed ()))
-> (ResultT Failed Sh () -> Sh (Result Failed ()))
-> ResultT Failed Sh ()
-> Sh (NominalDiffTime, Result Failed ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh () -> Sh (Result Failed ())
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT
        (ResultT Failed Sh () -> Sh (NominalDiffTime, Result Failed ()))
-> ResultT Failed Sh () -> Sh (NominalDiffTime, Result Failed ())
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> ResultT Failed Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
          FilePath -> ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
            Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ()) -> Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
              FilePath -> FilePath -> Sh ()
cp
                ( Text -> FilePath
fromText Text
".."
                    FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText (a -> Text
forall a. Tool a => a -> Text
toText a
a)
                    FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> a -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput a
a
                )
                (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ a -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput a
a
              FilePath -> FilePath -> Sh ()
cp
                ( Text -> FilePath
fromText Text
".."
                    FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText (b -> Text
forall a. Tool a => a -> Text
toText b
b)
                    FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
b
                )
                (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
b
              FilePath -> Text -> Sh ()
writefile FilePath
"rtl.v" (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> Text
forall a. Source a => a -> Text
genSource SourceInfo ann
src
            ResultT Failed Sh () -> ResultT Failed Sh ()
forall (m :: * -> *) a. MonadShControl m => m a -> m a
sub (ResultT Failed Sh () -> ResultT Failed Sh ())
-> ResultT Failed Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
              ResultT Failed Sh ()
-> (Text -> ResultT Failed Sh ())
-> Maybe Text
-> ResultT Failed Sh ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> ResultT Failed Sh ()
forall a. a -> ResultT Failed Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ())
-> (Text -> Sh ()) -> Text -> ResultT Failed Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Sh ()
prependToPath (FilePath -> Sh ()) -> (Text -> FilePath) -> Text -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
fromText) Maybe Text
yosysloc
              Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
forall a b ann.
(Synthesiser a, Synthesiser b, Show ann) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo ann -> ResultT Failed Sh ()
runEquiv Maybe Text
checker FilePath
datadir a
a b
b SourceInfo ann
src
      where
        dir :: FilePath
dir = Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"equiv_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Tool a => a -> Text
toText a
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
b

simulation :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo ann) -> Fuzz m ()
simulation :: forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
simulation SourceInfo ann
src = do
  FilePath
datadir <- (FuzzOpts -> FilePath)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> FilePath
_fuzzDataDir StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  [SynthTool]
synth <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
passedSynthesis
  [(SynthTool, Maybe CounterEg)]
counterEgs <- Fuzz m [(SynthTool, Maybe CounterEg)]
forall (m :: * -> *).
MonadSh m =>
Fuzz m [(SynthTool, Maybe CounterEg)]
failEquivWithIdentityCE
  [ByteString]
vals <- IO [ByteString]
-> StateT FuzzState (ReaderT FuzzEnv m) [ByteString]
forall a. IO a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [ByteString]
 -> StateT FuzzState (ReaderT FuzzEnv m) [ByteString])
-> IO [ByteString]
-> StateT FuzzState (ReaderT FuzzEnv m) [ByteString]
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Int -> Int -> IO [ByteString]
generateByteString Maybe Int
forall a. Maybe a
Nothing Int
32 Int
20
  (NominalDiffTime, Result Failed ByteString)
ident <- Sh (NominalDiffTime, Result Failed ByteString)
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     (NominalDiffTime, Result Failed ByteString)
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh (NominalDiffTime, Result Failed ByteString)
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      (NominalDiffTime, Result Failed ByteString))
-> Sh (NominalDiffTime, Result Failed ByteString)
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ FilePath
-> [ByteString]
-> Maybe ByteString
-> SynthTool
-> Sh (NominalDiffTime, Result Failed ByteString)
forall {b}.
Synthesiser b =>
FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
vals Maybe ByteString
forall a. Maybe a
Nothing SynthTool
defaultIdentitySynth
  [(NominalDiffTime, Result Failed ByteString)]
resTimes <- Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [(NominalDiffTime, Result Failed ByteString)]
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      [(NominalDiffTime, Result Failed ByteString)])
-> Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a b. (a -> b) -> a -> b
$ (SynthTool -> Sh (NominalDiffTime, Result Failed ByteString))
-> [SynthTool] -> Sh [(NominalDiffTime, Result Failed ByteString)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath
-> [ByteString]
-> Maybe ByteString
-> SynthTool
-> Sh (NominalDiffTime, Result Failed ByteString)
forall {b}.
Synthesiser b =>
FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
vals (Result Failed ByteString -> Maybe ByteString
forall a b. Result a b -> Maybe b
justPass (Result Failed ByteString -> Maybe ByteString)
-> Result Failed ByteString -> Maybe ByteString
forall a b. (a -> b) -> a -> b
$ (NominalDiffTime, Result Failed ByteString)
-> Result Failed ByteString
forall a b. (a, b) -> b
snd (NominalDiffTime, Result Failed ByteString)
ident)) [SynthTool]
synth
  [(NominalDiffTime, Result Failed ByteString)]
resTimes2 <- Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [(NominalDiffTime, Result Failed ByteString)]
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      [(NominalDiffTime, Result Failed ByteString)])
-> Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a b. (a -> b) -> a -> b
$ ((SynthTool, Maybe CounterEg)
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> [(SynthTool, Maybe CounterEg)]
-> Sh [(NominalDiffTime, Result Failed ByteString)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath
-> (SynthTool, Maybe CounterEg)
-> Sh (NominalDiffTime, Result Failed ByteString)
forall {b}.
Synthesiser b =>
FilePath
-> (b, Maybe CounterEg)
-> Sh (NominalDiffTime, Result Failed ByteString)
simCounterEg FilePath
datadir) [(SynthTool, Maybe CounterEg)]
counterEgs
  ([SimResult] -> Identity [SimResult])
-> FuzzState -> Identity FuzzState
Lens' FuzzState [SimResult]
fuzzSimResults (([SimResult] -> Identity [SimResult])
 -> FuzzState -> Identity FuzzState)
-> [SimResult] -> Fuzz m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SimTool
-> [ByteString]
-> [SynthTool]
-> [(NominalDiffTime, Result Failed ByteString)]
-> [SimResult]
toSimResult SimTool
defaultIcarusSim [ByteString]
vals [SynthTool]
synth [(NominalDiffTime, Result Failed ByteString)]
resTimes
  Sh () -> Fuzz m ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh
    (Sh () -> Fuzz m ())
-> ([Result FilePath FilePath] -> Sh ())
-> [Result FilePath FilePath]
-> Fuzz m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Result FilePath FilePath] -> Sh ()
forall s. Show s => s -> Sh ()
inspect
    ([Result FilePath FilePath] -> Fuzz m ())
-> [Result FilePath FilePath] -> Fuzz m ()
forall a b. (a -> b) -> a -> b
$ (\(NominalDiffTime
_, Result Failed ByteString
r) -> (Failed -> FilePath)
-> (ByteString -> FilePath)
-> Result Failed ByteString
-> Result FilePath FilePath
forall a b c d. (a -> b) -> (c -> d) -> Result a c -> Result b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Failed -> FilePath
forall a. Show a => a -> FilePath
show (Text -> FilePath
T.unpack (Text -> FilePath)
-> (ByteString -> Text) -> ByteString -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Text
T.take Int
10 (Text -> Text) -> (ByteString -> Text) -> ByteString -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
showBS) Result Failed ByteString
r)
      ((NominalDiffTime, Result Failed ByteString)
 -> Result FilePath FilePath)
-> [(NominalDiffTime, Result Failed ByteString)]
-> [Result FilePath FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NominalDiffTime, Result Failed ByteString)
ident (NominalDiffTime, Result Failed ByteString)
-> [(NominalDiffTime, Result Failed ByteString)]
-> [(NominalDiffTime, Result Failed ByteString)]
forall a. a -> [a] -> [a]
: [(NominalDiffTime, Result Failed ByteString)]
resTimes)
  where
    sim :: FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
b Maybe ByteString
i b
a = Text
-> Sh (Result Failed ByteString)
-> Sh (NominalDiffTime, Result Failed ByteString)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"simulation for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a) (Sh (Result Failed ByteString)
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> (ResultT Failed Sh ByteString -> Sh (Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh ByteString -> Sh (Result Failed ByteString)
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh ByteString
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ do
      FilePath -> ResultT Failed Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
      FilePath
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString)
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall a b. (a -> b) -> a -> b
$ do
        Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ()) -> Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> FilePath -> Sh ()
cp (Text -> FilePath
fromText Text
".." FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText (b -> Text
forall a. Tool a => a -> Text
toText b
a) FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a) (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$
            b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a
          FilePath -> Text -> Sh ()
writefile FilePath
"rtl.v" (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> Text
forall a. Source a => a -> Text
genSource SourceInfo ann
src
        FilePath
-> Icarus
-> b
-> SourceInfo ann
-> [ByteString]
-> Maybe ByteString
-> ResultT Failed Sh ByteString
forall b ann.
(Synthesiser b, Show ann) =>
FilePath
-> Icarus
-> b
-> SourceInfo ann
-> [ByteString]
-> Maybe ByteString
-> ResultT Failed Sh ByteString
runSimIc FilePath
datadir Icarus
defaultIcarus b
a SourceInfo ann
src [ByteString]
b Maybe ByteString
i
      where
        dir :: FilePath
dir = Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"simulation_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a
    simCounterEg :: FilePath
-> (b, Maybe CounterEg)
-> Sh (NominalDiffTime, Result Failed ByteString)
simCounterEg FilePath
datadir (b
a, Maybe CounterEg
Nothing) = Text
-> Sh (Result Failed ByteString)
-> Sh (NominalDiffTime, Result Failed ByteString)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"counter-example simulation for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a) (Sh (Result Failed ByteString)
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> (Result Failed ByteString -> Sh (Result Failed ByteString))
-> Result Failed ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result Failed ByteString -> Sh (Result Failed ByteString)
forall a. a -> Sh a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Failed ByteString
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> Result Failed ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ Failed -> Result Failed ByteString
forall a b. a -> Result a b
Fail Failed
EmptyFail
    simCounterEg FilePath
datadir (b
a, Just CounterEg
b) = Text
-> Sh (Result Failed ByteString)
-> Sh (NominalDiffTime, Result Failed ByteString)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"counter-example simulation for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a) (Sh (Result Failed ByteString)
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> (ResultT Failed Sh ByteString -> Sh (Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh ByteString -> Sh (Result Failed ByteString)
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh ByteString
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ do
      FilePath -> ResultT Failed Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
      FilePath
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString)
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall a b. (a -> b) -> a -> b
$ do
        Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ()) -> Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> FilePath -> Sh ()
cp (Text -> FilePath
fromText Text
".." FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText (b -> Text
forall a. Tool a => a -> Text
toText b
a) FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a) (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$ b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a
          FilePath -> Text -> Sh ()
writefile FilePath
"syn_identity.v" (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> Text
forall a. Source a => a -> Text
genSource SourceInfo ann
src
        ByteString
ident <- FilePath
-> Icarus
-> SynthTool
-> SourceInfo ann
-> CounterEg
-> Maybe ByteString
-> ResultT Failed Sh ByteString
forall b ann.
(Synthesiser b, Show ann) =>
FilePath
-> Icarus
-> b
-> SourceInfo ann
-> CounterEg
-> Maybe ByteString
-> ResultT Failed Sh ByteString
runSimIcEC FilePath
datadir Icarus
defaultIcarus SynthTool
defaultIdentitySynth SourceInfo ann
src CounterEg
b Maybe ByteString
forall a. Maybe a
Nothing
        FilePath
-> Icarus
-> b
-> SourceInfo ann
-> CounterEg
-> Maybe ByteString
-> ResultT Failed Sh ByteString
forall b ann.
(Synthesiser b, Show ann) =>
FilePath
-> Icarus
-> b
-> SourceInfo ann
-> CounterEg
-> Maybe ByteString
-> ResultT Failed Sh ByteString
runSimIcEC FilePath
datadir Icarus
defaultIcarus b
a SourceInfo ann
src CounterEg
b (ByteString -> Maybe ByteString
forall a. a -> Maybe a
Just ByteString
ident)
      where
        dir :: FilePath
dir = Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"countereg_sim_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a

simulationEMI :: (MonadIO m, MonadSh m, Show ann) => (SourceInfo (EMIInputs ann)) -> Fuzz m ()
simulationEMI :: forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
SourceInfo (EMIInputs ann) -> Fuzz m ()
simulationEMI SourceInfo (EMIInputs ann)
src = do
  FilePath
datadir <- (FuzzOpts -> FilePath)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> FilePath
_fuzzDataDir StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  [SynthTool]
synth <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
passedSynthesis
  [(SynthTool, Maybe CounterEg)]
counterEgs <- Fuzz m [(SynthTool, Maybe CounterEg)]
forall (m :: * -> *).
MonadSh m =>
Fuzz m [(SynthTool, Maybe CounterEg)]
failEquivWithIdentityCE
  [ByteString]
vals <- IO [ByteString]
-> StateT FuzzState (ReaderT FuzzEnv m) [ByteString]
forall a. IO a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [ByteString]
 -> StateT FuzzState (ReaderT FuzzEnv m) [ByteString])
-> IO [ByteString]
-> StateT FuzzState (ReaderT FuzzEnv m) [ByteString]
forall a b. (a -> b) -> a -> b
$ Maybe Int -> Int -> Int -> IO [ByteString]
generateByteString Maybe Int
forall a. Maybe a
Nothing Int
32 Int
100
  (NominalDiffTime, Result Failed ByteString)
ident <- Sh (NominalDiffTime, Result Failed ByteString)
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     (NominalDiffTime, Result Failed ByteString)
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh (NominalDiffTime, Result Failed ByteString)
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      (NominalDiffTime, Result Failed ByteString))
-> Sh (NominalDiffTime, Result Failed ByteString)
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ FilePath
-> [ByteString]
-> Maybe ByteString
-> SynthTool
-> Sh (NominalDiffTime, Result Failed ByteString)
forall {b}.
Synthesiser b =>
FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
vals Maybe ByteString
forall a. Maybe a
Nothing SynthTool
defaultIdentitySynth
  [(NominalDiffTime, Result Failed ByteString)]
resTimes <- Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [(NominalDiffTime, Result Failed ByteString)]
 -> StateT
      FuzzState
      (ReaderT FuzzEnv m)
      [(NominalDiffTime, Result Failed ByteString)])
-> Sh [(NominalDiffTime, Result Failed ByteString)]
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     [(NominalDiffTime, Result Failed ByteString)]
forall a b. (a -> b) -> a -> b
$ (SynthTool -> Sh (NominalDiffTime, Result Failed ByteString))
-> [SynthTool] -> Sh [(NominalDiffTime, Result Failed ByteString)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath
-> [ByteString]
-> Maybe ByteString
-> SynthTool
-> Sh (NominalDiffTime, Result Failed ByteString)
forall {b}.
Synthesiser b =>
FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
vals (Result Failed ByteString -> Maybe ByteString
forall a b. Result a b -> Maybe b
justPass (Result Failed ByteString -> Maybe ByteString)
-> Result Failed ByteString -> Maybe ByteString
forall a b. (a -> b) -> a -> b
$ (NominalDiffTime, Result Failed ByteString)
-> Result Failed ByteString
forall a b. (a, b) -> b
snd (NominalDiffTime, Result Failed ByteString)
ident)) [SynthTool]
synth
  ([SimResult] -> Identity [SimResult])
-> FuzzState -> Identity FuzzState
Lens' FuzzState [SimResult]
fuzzSimResults (([SimResult] -> Identity [SimResult])
 -> FuzzState -> Identity FuzzState)
-> [SimResult] -> Fuzz m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SimTool
-> [ByteString]
-> [SynthTool]
-> [(NominalDiffTime, Result Failed ByteString)]
-> [SimResult]
toSimResult SimTool
defaultIcarusSim [ByteString]
vals [SynthTool]
synth [(NominalDiffTime, Result Failed ByteString)]
resTimes
  Sh () -> Fuzz m ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh
    (Sh () -> Fuzz m ())
-> ([Result FilePath FilePath] -> Sh ())
-> [Result FilePath FilePath]
-> Fuzz m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Result FilePath FilePath] -> Sh ()
forall s. Show s => s -> Sh ()
inspect
    ([Result FilePath FilePath] -> Fuzz m ())
-> [Result FilePath FilePath] -> Fuzz m ()
forall a b. (a -> b) -> a -> b
$ (\(NominalDiffTime
_, Result Failed ByteString
r) -> (Failed -> FilePath)
-> (ByteString -> FilePath)
-> Result Failed ByteString
-> Result FilePath FilePath
forall a b c d. (a -> b) -> (c -> d) -> Result a c -> Result b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Failed -> FilePath
forall a. Show a => a -> FilePath
show (Text -> FilePath
T.unpack (Text -> FilePath)
-> (ByteString -> Text) -> ByteString -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Text
T.take Int
10 (Text -> Text) -> (ByteString -> Text) -> ByteString -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
showBS) Result Failed ByteString
r)
      ((NominalDiffTime, Result Failed ByteString)
 -> Result FilePath FilePath)
-> [(NominalDiffTime, Result Failed ByteString)]
-> [Result FilePath FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((NominalDiffTime, Result Failed ByteString)
ident (NominalDiffTime, Result Failed ByteString)
-> [(NominalDiffTime, Result Failed ByteString)]
-> [(NominalDiffTime, Result Failed ByteString)]
forall a. a -> [a] -> [a]
: [(NominalDiffTime, Result Failed ByteString)]
resTimes)
  where
    sim :: FilePath
-> [ByteString]
-> Maybe ByteString
-> b
-> Sh (NominalDiffTime, Result Failed ByteString)
sim FilePath
datadir [ByteString]
b Maybe ByteString
i b
a = Text
-> Sh (Result Failed ByteString)
-> Sh (NominalDiffTime, Result Failed ByteString)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m, Show a) =>
Text -> m a -> m (NominalDiffTime, a)
toolRun (Text
"simulation for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a) (Sh (Result Failed ByteString)
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> (ResultT Failed Sh ByteString -> Sh (Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ResultT Failed Sh ByteString -> Sh (Result Failed ByteString)
forall a (m :: * -> *) b. ResultT a m b -> m (Result a b)
runResultT (ResultT Failed Sh ByteString
 -> Sh (NominalDiffTime, Result Failed ByteString))
-> ResultT Failed Sh ByteString
-> Sh (NominalDiffTime, Result Failed ByteString)
forall a b. (a -> b) -> a -> b
$ do
      FilePath -> ResultT Failed Sh ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
dir
      FilePath
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
dir (ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString)
-> ResultT Failed Sh ByteString -> ResultT Failed Sh ByteString
forall a b. (a -> b) -> a -> b
$ do
        Sh () -> ResultT Failed Sh ()
forall a. Sh a -> ResultT Failed Sh a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> ResultT Failed Sh ()) -> Sh () -> ResultT Failed Sh ()
forall a b. (a -> b) -> a -> b
$ do
          FilePath -> FilePath -> Sh ()
cp (Text -> FilePath
fromText Text
".." FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> Text -> FilePath
fromText (b -> Text
forall a. Tool a => a -> Text
toText b
a) FilePath -> ShowS
forall filepath1 filepath2.
(ToFilePath filepath1, ToFilePath filepath2) =>
filepath1 -> filepath2 -> FilePath
</> b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a) (FilePath -> Sh ()) -> FilePath -> Sh ()
forall a b. (a -> b) -> a -> b
$
            b -> FilePath
forall a. Synthesiser a => a -> FilePath
synthOutput b
a
          FilePath -> Text -> Sh ()
writefile FilePath
"rtl.v" (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo (EMIInputs ann) -> Text
forall a. Source a => a -> Text
genSource SourceInfo (EMIInputs ann)
src
        [Identifier]
-> FilePath
-> Icarus
-> b
-> SourceInfo ()
-> [ByteString]
-> Maybe ByteString
-> ResultT Failed Sh ByteString
forall b ann.
(Synthesiser b, Show ann) =>
[Identifier]
-> FilePath
-> Icarus
-> b
-> SourceInfo ann
-> [ByteString]
-> Maybe ByteString
-> ResultT Failed Sh ByteString
runSimIcEMI (SourceInfo (EMIInputs ann) -> [Identifier]
forall a. SourceInfo (EMIInputs a) -> [Identifier]
getTopEMIIdent SourceInfo (EMIInputs ann)
src) FilePath
datadir Icarus
defaultIcarus b
a (SourceInfo (EMIInputs ann) -> SourceInfo ()
forall a. SourceInfo a -> SourceInfo ()
forall (m :: * -> *) a. Annotations m => m a -> m ()
clearAnn SourceInfo (EMIInputs ann)
src) [ByteString]
b Maybe ByteString
i
      where
        dir :: FilePath
dir = Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"emi_sim_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. Tool a => a -> Text
toText b
a

failEquivWithIdentity :: (MonadSh m) => Fuzz m [SynthResult]
failEquivWithIdentity :: forall (m :: * -> *). MonadSh m => Fuzz m [SynthResult]
failEquivWithIdentity = (SynthResult -> Bool) -> [SynthResult] -> [SynthResult]
forall a. (a -> Bool) -> [a] -> [a]
filter SynthResult -> Bool
withIdentity ([SynthResult] -> [SynthResult])
-> (FuzzState -> [SynthResult]) -> FuzzState -> [SynthResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SynthResult]
_fuzzSynthResults (FuzzState -> [SynthResult])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    withIdentity :: SynthResult -> Bool
withIdentity (SynthResult (IdentitySynth Identity
_) SynthTool
_ (Fail (EquivFail Maybe CounterEg
_)) NominalDiffTime
_) = Bool
True
    withIdentity (SynthResult SynthTool
_ (IdentitySynth Identity
_) (Fail (EquivFail Maybe CounterEg
_)) NominalDiffTime
_) = Bool
True
    withIdentity SynthResult
_ = Bool
False

failEquivWithIdentityCE :: (MonadSh m) => Fuzz m [(SynthTool, Maybe CounterEg)]
failEquivWithIdentityCE :: forall (m :: * -> *).
MonadSh m =>
Fuzz m [(SynthTool, Maybe CounterEg)]
failEquivWithIdentityCE = [Maybe (SynthTool, Maybe CounterEg)]
-> [(SynthTool, Maybe CounterEg)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (SynthTool, Maybe CounterEg)]
 -> [(SynthTool, Maybe CounterEg)])
-> (FuzzState -> [Maybe (SynthTool, Maybe CounterEg)])
-> FuzzState
-> [(SynthTool, Maybe CounterEg)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SynthResult -> Maybe (SynthTool, Maybe CounterEg))
-> [SynthResult] -> [Maybe (SynthTool, Maybe CounterEg)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SynthResult -> Maybe (SynthTool, Maybe CounterEg)
withIdentity ([SynthResult] -> [Maybe (SynthTool, Maybe CounterEg)])
-> (FuzzState -> [SynthResult])
-> FuzzState
-> [Maybe (SynthTool, Maybe CounterEg)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SynthResult]
_fuzzSynthResults (FuzzState -> [(SynthTool, Maybe CounterEg)])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT
     FuzzState (ReaderT FuzzEnv m) [(SynthTool, Maybe CounterEg)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    withIdentity :: SynthResult -> Maybe (SynthTool, Maybe CounterEg)
withIdentity (SynthResult (IdentitySynth Identity
_) SynthTool
s (Fail (EquivFail Maybe CounterEg
c)) NominalDiffTime
_) = (SynthTool, Maybe CounterEg) -> Maybe (SynthTool, Maybe CounterEg)
forall a. a -> Maybe a
Just (SynthTool
s, Maybe CounterEg
c)
    withIdentity (SynthResult SynthTool
s (IdentitySynth Identity
_) (Fail (EquivFail Maybe CounterEg
c)) NominalDiffTime
_) = (SynthTool, Maybe CounterEg) -> Maybe (SynthTool, Maybe CounterEg)
forall a. a -> Maybe a
Just (SynthTool
s, Maybe CounterEg
c)
    withIdentity SynthResult
_ = Maybe (SynthTool, Maybe CounterEg)
forall a. Maybe a
Nothing

failedSimulations :: (MonadSh m) => Fuzz m [SimResult]
failedSimulations :: forall (m :: * -> *). MonadSh m => Fuzz m [SimResult]
failedSimulations = (SimResult -> Bool) -> [SimResult] -> [SimResult]
forall a. (a -> Bool) -> [a] -> [a]
filter SimResult -> Bool
failedSim ([SimResult] -> [SimResult])
-> (FuzzState -> [SimResult]) -> FuzzState -> [SimResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SimResult]
_fuzzSimResults (FuzzState -> [SimResult])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT FuzzState (ReaderT FuzzEnv m) [SimResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    failedSim :: SimResult -> Bool
failedSim (SimResult SynthTool
_ SimTool
_ [ByteString]
_ (Fail (SimFail ByteString
_)) NominalDiffTime
_) = Bool
True
    failedSim SimResult
_ = Bool
False

passEquiv :: (MonadSh m) => Fuzz m [SynthResult]
passEquiv :: forall (m :: * -> *). MonadSh m => Fuzz m [SynthResult]
passEquiv = (SynthResult -> Bool) -> [SynthResult] -> [SynthResult]
forall a. (a -> Bool) -> [a] -> [a]
filter SynthResult -> Bool
withIdentity ([SynthResult] -> [SynthResult])
-> (FuzzState -> [SynthResult]) -> FuzzState -> [SynthResult]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FuzzState -> [SynthResult]
_fuzzSynthResults (FuzzState -> [SynthResult])
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
-> StateT FuzzState (ReaderT FuzzEnv m) [SynthResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  where
    withIdentity :: SynthResult -> Bool
withIdentity (SynthResult SynthTool
_ SynthTool
_ (Pass ()
_) NominalDiffTime
_) = Bool
True
    withIdentity SynthResult
_ = Bool
False

-- | Always reduces with respect to 'Identity'.
reduction :: (MonadSh m) => SourceInfo ann -> Fuzz m ()
reduction :: forall (m :: * -> *) ann. MonadSh m => SourceInfo ann -> Fuzz m ()
reduction SourceInfo ann
rsrc = do
  FilePath
datadir <- (FuzzOpts -> FilePath)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> FilePath
_fuzzDataDir StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  Maybe Text
checker <- (FuzzOpts -> Maybe Text)
-> StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
-> StateT FuzzState (ReaderT FuzzEnv m) (Maybe Text)
forall a b.
(a -> b)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FuzzOpts -> Maybe Text
_fuzzOptsChecker StateT FuzzState (ReaderT FuzzEnv m) FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  [SynthResult]
fails <- Fuzz m [SynthResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthResult]
failEquivWithIdentity
  [SynthTool]
synthFails <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
failedSynthesis
  [SimResult]
simFails <- Fuzz m [SimResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SimResult]
failedSimulations
  [()]
_ <- Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()])
-> Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a b. (a -> b) -> a -> b
$ (SynthResult -> Sh ()) -> [SynthResult] -> Sh [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Maybe Text -> FilePath -> SynthResult -> Sh ()
red Maybe Text
checker FilePath
datadir) [SynthResult]
fails
  [()]
_ <- Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()])
-> Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a b. (a -> b) -> a -> b
$ (SynthTool -> Sh ()) -> [SynthTool] -> Sh [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SynthTool -> Sh ()
forall {a}. Synthesiser a => a -> Sh ()
redSynth [SynthTool]
synthFails
  [()]
_ <- Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()])
-> Sh [()] -> StateT FuzzState (ReaderT FuzzEnv m) [()]
forall a b. (a -> b) -> a -> b
$ (SimResult -> Sh ()) -> [SimResult] -> Sh [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath -> SimResult -> Sh ()
redSim FilePath
datadir) [SimResult]
simFails
  () -> Fuzz m ()
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    red :: Maybe Text -> FilePath -> SynthResult -> Sh ()
red Maybe Text
checker FilePath
datadir (SynthResult SynthTool
a SynthTool
b Result Failed ()
_ NominalDiffTime
_) = do
      SourceInfo ()
r <- Maybe Text
-> FilePath
-> SynthTool
-> SynthTool
-> SourceInfo ()
-> Sh (SourceInfo ())
forall a b (m :: * -> *).
(Synthesiser a, Synthesiser b, MonadSh m) =>
Maybe Text
-> FilePath -> a -> b -> SourceInfo () -> m (SourceInfo ())
reduceSynth Maybe Text
checker FilePath
datadir SynthTool
a SynthTool
b SourceInfo ()
src
      FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"reduce_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SynthTool -> Text
forall a. Tool a => a -> Text
toText SynthTool
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SynthTool -> Text
forall a. Tool a => a -> Text
toText SynthTool
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".v") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo () -> Text
forall a. Source a => a -> Text
genSource SourceInfo ()
r
    redSynth :: a -> Sh ()
redSynth a
a = do
      SourceInfo ()
r <- a -> SourceInfo () -> Sh (SourceInfo ())
forall a (m :: * -> *).
(Synthesiser a, MonadSh m) =>
a -> SourceInfo () -> m (SourceInfo ())
reduceSynthesis a
a SourceInfo ()
src
      FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"reduce_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Tool a => a -> Text
toText a
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".v") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo () -> Text
forall a. Source a => a -> Text
genSource SourceInfo ()
r
    redSim :: FilePath -> SimResult -> Sh ()
redSim FilePath
datadir (SimResult SynthTool
t SimTool
_ [ByteString]
bs Result Failed ByteString
_ NominalDiffTime
_) = do
      SourceInfo ()
r <- FilePath
-> [ByteString] -> SynthTool -> SourceInfo () -> Sh (SourceInfo ())
forall a (m :: * -> *).
(Synthesiser a, MonadSh m) =>
FilePath -> [ByteString] -> a -> SourceInfo () -> m (SourceInfo ())
reduceSimIc FilePath
datadir [ByteString]
bs SynthTool
t SourceInfo ()
src
      FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText (Text -> FilePath) -> Text -> FilePath
forall a b. (a -> b) -> a -> b
$ Text
"reduce_sim_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SynthTool -> Text
forall a. Tool a => a -> Text
toText SynthTool
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
".v") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ SourceInfo () -> Text
forall a. Source a => a -> Text
genSource SourceInfo ()
r
    src :: SourceInfo ()
src = SourceInfo ann -> SourceInfo ()
forall a. SourceInfo a -> SourceInfo ()
forall (m :: * -> *) a. Annotations m => m a -> m ()
clearAnn SourceInfo ann
rsrc

titleRun ::
  (MonadIO m, MonadSh m) => Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun :: forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
t Fuzz m a
f = do
  Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Text
"### Starting " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ###"
  (NominalDiffTime
diff, a
res) <- Fuzz m a -> Fuzz m (NominalDiffTime, a)
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
m a -> m (NominalDiffTime, a)
timeit Fuzz m a
f
  Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Text
"### Finished " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> NominalDiffTime -> Text
forall a. Show a => a -> Text
showT NominalDiffTime
diff Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") ###"
  (NominalDiffTime, a) -> Fuzz m (NominalDiffTime, a)
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime
diff, a
res)

whenMaybe :: (Applicative m) => Bool -> m a -> m (Maybe a)
whenMaybe :: forall (m :: * -> *) a. Applicative m => Bool -> m a -> m (Maybe a)
whenMaybe Bool
b m a
x = if Bool
b then a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> m a -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
x else Maybe a -> m (Maybe a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
forall a. Maybe a
Nothing

getTime :: (Num n) => Maybe (n, a) -> n
getTime :: forall n a. Num n => Maybe (n, a) -> n
getTime = n -> ((n, a) -> n) -> Maybe (n, a) -> n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe n
0 (n, a) -> n
forall a b. (a, b) -> a
fst

generateSample ::
  (MonadIO m, MonadSh m, Show ann) =>
  Fuzz m (Seed, (SourceInfo ann)) ->
  Fuzz m (Seed, (SourceInfo ann))
generateSample :: forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
generateSample Fuzz m (Seed, SourceInfo ann)
f = do
  Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT Text
"Sampling Verilog from generator"
  (NominalDiffTime
t, v :: (Seed, SourceInfo ann)
v@(Seed
s, SourceInfo ann
_)) <- Fuzz m (Seed, SourceInfo ann)
-> StateT
     FuzzState
     (ReaderT FuzzEnv m)
     (NominalDiffTime, (Seed, SourceInfo ann))
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
m a -> m (NominalDiffTime, a)
timeit Fuzz m (Seed, SourceInfo ann)
f
  Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Text
"Chose " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Seed -> Text
forall a. Show a => a -> Text
showT Seed
s
  Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => Text -> m ()
logT (Text -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Text
"Generated Verilog (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> NominalDiffTime -> Text
forall a. Show a => a -> Text
showT NominalDiffTime
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Seed, SourceInfo ann)
v

verilogSize :: (Source a) => a -> Int
verilogSize :: forall a. Source a => a -> Int
verilogSize = [FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([FilePath] -> Int) -> (a -> [FilePath]) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines (FilePath -> [FilePath]) -> (a -> FilePath) -> a -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> FilePath) -> (a -> Text) -> a -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Text
forall a. Source a => a -> Text
genSource

sampleVerilog ::
  (MonadSh m, MonadIO m, Source a, Ord a) =>
  Frequency a ->
  Int ->
  Maybe Seed ->
  Gen a ->
  m (Seed, a)
sampleVerilog :: forall (m :: * -> *) a.
(MonadSh m, MonadIO m, Source a, Ord a) =>
Frequency a -> Int -> Maybe Seed -> Gen a -> m (Seed, a)
sampleVerilog Frequency a
_ Int
_ seed :: Maybe Seed
seed@(Just Seed
_) Gen a
gen = Maybe Seed -> Gen a -> m (Seed, a)
forall (m :: * -> *) a.
MonadSh m =>
Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed Maybe Seed
seed Gen a
gen
sampleVerilog Frequency a
freq Int
n Maybe Seed
Nothing Gen a
gen = do
  [(Seed, a)]
res <- Int -> m (Seed, a) -> m [(Seed, a)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (m (Seed, a) -> m [(Seed, a)]) -> m (Seed, a) -> m [(Seed, a)]
forall a b. (a -> b) -> a -> b
$ Maybe Seed -> Gen a -> m (Seed, a)
forall (m :: * -> *) a.
MonadSh m =>
Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed Maybe Seed
forall a. Maybe a
Nothing Gen a
gen
  let sizes :: [Int]
sizes = ((Seed, a) -> Int) -> [(Seed, a)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Seed, a) -> Int
forall {a} {a}. Source a => (a, a) -> Int
getSize [(Seed, a)]
res
  let samples :: [(Seed, a)]
samples = ((Int, (Seed, a)) -> (Seed, a))
-> [(Int, (Seed, a))] -> [(Seed, a)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, (Seed, a)) -> (Seed, a)
forall a b. (a, b) -> b
snd ([(Int, (Seed, a))] -> [(Seed, a)])
-> ([(Int, (Seed, a))] -> [(Int, (Seed, a))])
-> [(Int, (Seed, a))]
-> [(Seed, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, (Seed, a))] -> [(Int, (Seed, a))]
forall a. Ord a => [a] -> [a]
sort ([(Int, (Seed, a))] -> [(Seed, a)])
-> [(Int, (Seed, a))] -> [(Seed, a)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [(Seed, a)] -> [(Int, (Seed, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
sizes [(Seed, a)]
res
  IO (Seed, a) -> m (Seed, a)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Seed, a) -> m (Seed, a)) -> IO (Seed, a) -> m (Seed, a)
forall a b. (a -> b) -> a -> b
$ Gen (Seed, a) -> IO (Seed, a)
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Hog.sample (Gen (Seed, a) -> IO (Seed, a))
-> ([(Int, Gen (Seed, a))] -> Gen (Seed, a))
-> [(Int, Gen (Seed, a))]
-> IO (Seed, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, Gen (Seed, a))] -> Gen (Seed, a)
forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Hog.frequency ([(Int, Gen (Seed, a))] -> IO (Seed, a))
-> [(Int, Gen (Seed, a))] -> IO (Seed, a)
forall a b. (a -> b) -> a -> b
$ Frequency a
freq [(Seed, a)]
samples
  where
    getSize :: (a, a) -> Int
getSize (a
_, a
s) = a -> Int
forall a. Source a => a -> Int
verilogSize a
s

hatFreqs :: Frequency a
hatFreqs :: forall a. Frequency a
hatFreqs [(Seed, a)]
l = [Int] -> [Gen (Seed, a)] -> [(Int, Gen (Seed, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
hat ((Seed, a) -> Gen (Seed, a)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Seed, a) -> Gen (Seed, a)) -> [(Seed, a)] -> [Gen (Seed, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Seed, a)]
l)
  where
    h :: Int
h = [(Seed, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Seed, a)]
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    hat :: [Int]
hat = (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
h) (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
negate (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
h Int -> Int -> Int
forall a. Num a => a -> a -> a
-) (Int -> Int) -> [Int] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. [(Seed, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Seed, a)]
l]

meanFreqs :: (Source a) => Frequency a
meanFreqs :: forall a. Source a => Frequency a
meanFreqs [(Seed, a)]
l = [Int] -> [Gen (Seed, a)] -> [(Int, Gen (Seed, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
hat ((Seed, a) -> Gen (Seed, a)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Seed, a) -> Gen (Seed, a)) -> [(Seed, a)] -> [Gen (Seed, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Seed, a)]
l)
  where
    hat :: [Int]
hat = Int -> Int
forall {a}. Num a => Int -> a
calc (Int -> Int) -> [Int] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
sizes
    calc :: Int -> a
calc Int
i = if Int -> Int
forall a. Num a => a -> a
abs (Int
mean Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
min_ then a
1 else a
0
    mean :: Int
mean = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int]
sizes Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` [(Seed, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Seed, a)]
l
    min_ :: Int
min_ = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
abs (Int -> Int) -> (Int -> Int) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int
mean Int -> Int -> Int
forall a. Num a => a -> a -> a
-) (Int -> Int) -> [Int] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int]
sizes
    sizes :: [Int]
sizes = a -> Int
forall a. Source a => a -> Int
verilogSize (a -> Int) -> ((Seed, a) -> a) -> (Seed, a) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seed, a) -> a
forall a b. (a, b) -> b
snd ((Seed, a) -> Int) -> [(Seed, a)] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Seed, a)]
l

medianFreqs :: Frequency a
medianFreqs :: forall a. Frequency a
medianFreqs [(Seed, a)]
l = [Int] -> [Gen (Seed, a)] -> [(Int, Gen (Seed, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
hat ((Seed, a) -> Gen (Seed, a)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Seed, a) -> Gen (Seed, a)) -> [(Seed, a)] -> [Gen (Seed, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Seed, a)]
l)
  where
    h :: Int
h = [(Seed, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Seed, a)]
l Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
    hat :: [Int]
hat = Int -> Int
forall {a}. Num a => Int -> a
set_ (Int -> Int) -> [Int] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1 .. [(Seed, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Seed, a)]
l]
    set_ :: Int -> a
set_ Int
n = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
h then a
1 else a
0

fuzz :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzz :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzz Gen (SourceInfo ann)
gen = do
  Config
conf <- Fuzz m Config
forall (m :: * -> *). Monad m => Fuzz m Config
askConfig
  FuzzOpts
opts <- Fuzz m FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  let seed :: Maybe Seed
seed = Config
conf Config -> Getting (Maybe Seed) Config (Maybe Seed) -> Maybe Seed
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Config -> Const (Maybe Seed) Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const (Maybe Seed) ConfProperty)
 -> Config -> Const (Maybe Seed) Config)
-> ((Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
    -> ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Getting (Maybe Seed) Config (Maybe Seed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
-> ConfProperty -> Const (Maybe Seed) ConfProperty
Lens' ConfProperty (Maybe Seed)
propSeed
  (Seed
seed', SourceInfo ann
src) <- Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
generateSample (Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann))
-> Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
forall a b. (a -> b) -> a -> b
$ Config
-> Maybe Seed
-> Gen (SourceInfo ann)
-> Fuzz m (Seed, SourceInfo ann)
forall {m :: * -> *} {a}.
(MonadSh m, MonadIO m, Source a, Ord a) =>
Config -> Maybe Seed -> Gen a -> m (Seed, a)
genMethod Config
conf Maybe Seed
seed Gen (SourceInfo ann)
gen
  let size :: Int
size = [FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([FilePath] -> Int) -> (Text -> [FilePath]) -> Text -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines (FilePath -> [FilePath])
-> (Text -> FilePath) -> Text -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> Int) -> Text -> Int
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> Text
forall a. Source a => a -> Text
genSource SourceInfo ann
src
  Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh
    (Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> (Config -> Sh ())
-> Config
-> StateT FuzzState (ReaderT FuzzEnv m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text -> Sh ()
writefile FilePath
"config.toml"
    (Text -> Sh ()) -> (Config -> Text) -> Config -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Text
encodeConfig
    (Config -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Config -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Config
conf
      Config -> (Config -> Config) -> Config
forall a b. a -> (a -> b) -> b
& (ConfProperty -> Identity ConfProperty)
-> Config -> Identity Config
Lens' Config ConfProperty
configProperty
        ((ConfProperty -> Identity ConfProperty)
 -> Config -> Identity Config)
-> ((Maybe Seed -> Identity (Maybe Seed))
    -> ConfProperty -> Identity ConfProperty)
-> (Maybe Seed -> Identity (Maybe Seed))
-> Config
-> Identity Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Seed -> Identity (Maybe Seed))
-> ConfProperty -> Identity ConfProperty
Lens' ConfProperty (Maybe Seed)
propSeed
        ((Maybe Seed -> Identity (Maybe Seed))
 -> Config -> Identity Config)
-> Seed -> Config -> Config
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Seed
seed'
  (NominalDiffTime
tsynth, ()
_) <- Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Synthesis" (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann.
(MonadBaseControl IO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
synthesis SourceInfo ann
src
  (NominalDiffTime
tequiv, ()
_) <-
    if (FuzzOpts -> Bool
_fuzzOptsNoEquiv FuzzOpts
opts)
      then (NominalDiffTime, ()) -> Fuzz m (NominalDiffTime, ())
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime
0, ()
forall a. Monoid a => a
mempty)
      else Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Equivalence Check" (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann.
(MonadBaseControl IO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
equivalence SourceInfo ann
src
  (NominalDiffTime
_, ()
_) <-
    if (FuzzOpts -> Bool
_fuzzOptsNoSim FuzzOpts
opts)
      then (NominalDiffTime, ()) -> Fuzz m (NominalDiffTime, ())
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime
0, ()
forall a. Monoid a => a
mempty)
      else Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Simulation" (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
simulation SourceInfo ann
src
  [SynthResult]
fails <- Fuzz m [SynthResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthResult]
failEquivWithIdentity
  [SimResult]
failedSim <- Fuzz m [SimResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SimResult]
failedSimulations
  [SynthTool]
synthFails <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
failedSynthesis
  Maybe (NominalDiffTime, ())
redResult <-
    Bool
-> Fuzz m (NominalDiffTime, ())
-> StateT
     FuzzState (ReaderT FuzzEnv m) (Maybe (NominalDiffTime, ()))
forall (m :: * -> *) a. Applicative m => Bool -> m a -> m (Maybe a)
whenMaybe
      ( Bool -> Bool
not ([SimResult] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SimResult]
failedSim Bool -> Bool -> Bool
&& [SynthResult] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SynthResult]
fails Bool -> Bool -> Bool
&& [SynthTool] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SynthTool]
synthFails)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (FuzzOpts -> Bool
_fuzzOptsNoReduction FuzzOpts
opts)
      )
      (Fuzz m (NominalDiffTime, ())
 -> StateT
      FuzzState (ReaderT FuzzEnv m) (Maybe (NominalDiffTime, ())))
-> (StateT FuzzState (ReaderT FuzzEnv m) ()
    -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> StateT
     FuzzState (ReaderT FuzzEnv m) (Maybe (NominalDiffTime, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Reduction"
      (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> StateT
      FuzzState (ReaderT FuzzEnv m) (Maybe (NominalDiffTime, ())))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> StateT
     FuzzState (ReaderT FuzzEnv m) (Maybe (NominalDiffTime, ()))
forall a b. (a -> b) -> a -> b
$ SourceInfo ann -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann. MonadSh m => SourceInfo ann -> Fuzz m ()
reduction SourceInfo ann
src
  FuzzState
state_ <- StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  FilePath
currdir <- Sh FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh Sh FilePath
pwd
  let vi :: Getting c FuzzState c -> c
vi = (Getting c FuzzState c -> FuzzState -> c)
-> FuzzState -> Getting c FuzzState c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Getting c FuzzState c -> FuzzState -> c
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view FuzzState
state_
  let report :: FuzzReport
report =
        FilePath
-> [SynthResult]
-> [SimResult]
-> [SynthStatus]
-> Int
-> NominalDiffTime
-> NominalDiffTime
-> NominalDiffTime
-> FuzzReport
FuzzReport
          FilePath
currdir
          (Getting [SynthResult] FuzzState [SynthResult] -> [SynthResult]
forall {c}. Getting c FuzzState c -> c
vi Getting [SynthResult] FuzzState [SynthResult]
Lens' FuzzState [SynthResult]
fuzzSynthResults)
          (Getting [SimResult] FuzzState [SimResult] -> [SimResult]
forall {c}. Getting c FuzzState c -> c
vi Getting [SimResult] FuzzState [SimResult]
Lens' FuzzState [SimResult]
fuzzSimResults)
          (Getting [SynthStatus] FuzzState [SynthStatus] -> [SynthStatus]
forall {c}. Getting c FuzzState c -> c
vi Getting [SynthStatus] FuzzState [SynthStatus]
Lens' FuzzState [SynthStatus]
fuzzSynthStatus)
          Int
size
          NominalDiffTime
tsynth
          NominalDiffTime
tequiv
          (Maybe (NominalDiffTime, ()) -> NominalDiffTime
forall n a. Num n => Maybe (n, a) -> n
getTime Maybe (NominalDiffTime, ())
redResult)
  FuzzReport -> Fuzz m FuzzReport
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return FuzzReport
report

fuzzInDirG ::
  (MonadFuzz m, Ord ann, Show ann) =>
  (Gen (SourceInfo ann) -> Fuzz m FuzzReport) ->
  Gen (SourceInfo ann) ->
  Fuzz m FuzzReport
fuzzInDirG :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDirG Gen (SourceInfo ann) -> Fuzz m FuzzReport
f Gen (SourceInfo ann)
src = do
  FuzzOpts
fuzzOpts <- Fuzz m FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  let fp :: FilePath
fp = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
"fuzz" (Maybe FilePath -> FilePath) -> Maybe FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FuzzOpts -> Maybe FilePath
_fuzzOptsOutput FuzzOpts
fuzzOpts
  FilePath -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
fp
  FuzzReport
res <- FilePath -> Fuzz m FuzzReport -> Fuzz m FuzzReport
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
fp (Fuzz m FuzzReport -> Fuzz m FuzzReport)
-> Fuzz m FuzzReport -> Fuzz m FuzzReport
forall a b. (a -> b) -> a -> b
$ Gen (SourceInfo ann) -> Fuzz m FuzzReport
f Gen (SourceInfo ann)
src
  Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ do
    FilePath -> Text -> Sh ()
writefile (FilePath
fp FilePath -> Text -> FilePath
forall filepath.
ToFilePath filepath =>
filepath -> Text -> FilePath
<.> Text
"html") (Text -> Sh ()) -> Text -> Sh ()
forall a b. (a -> b) -> a -> b
$ Text -> FuzzReport -> Text
printResultReport (FilePath -> Text
bname FilePath
fp) FuzzReport
res
    Bool -> Sh () -> Sh ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FuzzReport -> Bool
passedFuzz FuzzReport
res Bool -> Bool -> Bool
&& Bool -> Bool
not (FuzzOpts -> Bool
_fuzzOptsKeepAll FuzzOpts
fuzzOpts)) (Sh () -> Sh ()) -> Sh () -> Sh ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Sh ()
rm_rf FilePath
fp
  FuzzReport -> Fuzz m FuzzReport
forall (m :: * -> *). MonadSh m => FuzzReport -> m FuzzReport
relativeFuzzReport FuzzReport
res
  where
    bname :: FilePath -> Text
bname = FilePath -> Text
T.pack (FilePath -> Text) -> ShowS -> FilePath -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeBaseName ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> FilePath) -> (FilePath -> Text) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
toTextIgnore

fuzzMultipleG ::
  (MonadFuzz m, Ord ann, Show ann) =>
  (Gen (SourceInfo ann) -> Fuzz m FuzzReport) ->
  Gen (SourceInfo ann) ->
  Fuzz m [FuzzReport]
fuzzMultipleG :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultipleG Gen (SourceInfo ann) -> Fuzz m FuzzReport
f Gen (SourceInfo ann)
src = do
  FuzzOpts
fuzzOpts <- Fuzz m FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  let seed :: Maybe Seed
seed = (FuzzOpts -> Config
_fuzzOptsConfig FuzzOpts
fuzzOpts) Config -> Getting (Maybe Seed) Config (Maybe Seed) -> Maybe Seed
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Config -> Const (Maybe Seed) Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const (Maybe Seed) ConfProperty)
 -> Config -> Const (Maybe Seed) Config)
-> ((Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
    -> ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Getting (Maybe Seed) Config (Maybe Seed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
-> ConfProperty -> Const (Maybe Seed) ConfProperty
Lens' ConfProperty (Maybe Seed)
propSeed
  FilePath
x <- case FuzzOpts -> Maybe FilePath
_fuzzOptsOutput FuzzOpts
fuzzOpts of
    Maybe FilePath
Nothing -> do
      ZonedTime
ct <- IO ZonedTime -> StateT FuzzState (ReaderT FuzzEnv m) ZonedTime
forall a. IO a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ZonedTime
getZonedTime
      FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath)
-> ShowS
-> FilePath
-> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
fromText
        (Text -> FilePath) -> (FilePath -> Text) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
T.pack
        (FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath)
-> FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"output_"
          FilePath -> ShowS
forall a. Semigroup a => a -> a -> a
<> TimeLocale -> FilePath -> ZonedTime -> FilePath
forall t. FormatTime t => TimeLocale -> FilePath -> t -> FilePath
formatTime TimeLocale
defaultTimeLocale FilePath
"%Y-%m-%d_%H-%M-%S" ZonedTime
ct
    Just FilePath
f -> FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
f
  FilePath -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *). MonadSh m => FilePath -> m ()
make FilePath
x
  FilePath -> Fuzz m [FuzzReport] -> Fuzz m [FuzzReport]
forall (m :: * -> *) a.
(MonadBaseControl IO m, MonadSh m) =>
FilePath -> m a -> m a
pop FilePath
x (Fuzz m [FuzzReport] -> Fuzz m [FuzzReport])
-> Fuzz m [FuzzReport] -> Fuzz m [FuzzReport]
forall a b. (a -> b) -> a -> b
$ do
    [FuzzReport]
results <-
      if Maybe Seed -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Seed
seed
        then [Int] -> (Int -> Fuzz m FuzzReport) -> Fuzz m [FuzzReport]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
1 .. (FuzzOpts -> Int
_fuzzOptsIterations FuzzOpts
fuzzOpts)] Int -> Fuzz m FuzzReport
forall {a}. Show a => a -> Fuzz m FuzzReport
fuzzDir'
        else (FuzzReport -> [FuzzReport] -> [FuzzReport]
forall a. a -> [a] -> [a]
: []) (FuzzReport -> [FuzzReport])
-> Fuzz m FuzzReport -> Fuzz m [FuzzReport]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Fuzz m FuzzReport
forall {a}. Show a => a -> Fuzz m FuzzReport
fuzzDir' (Int
1 :: Int)
    Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> (Text -> Sh ())
-> Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text -> Sh ()
writefile (Text -> FilePath
fromText Text
"index" FilePath -> Text -> FilePath
forall filepath.
ToFilePath filepath =>
filepath -> Text -> FilePath
<.> Text
"html") (Text -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Text -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$
      Text -> [FuzzReport] -> Text
printSummary
        Text
"Fuzz Summary"
        [FuzzReport]
results
    [FuzzReport] -> Fuzz m [FuzzReport]
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return [FuzzReport]
results
  where
    fuzzDir' :: a -> Fuzz m FuzzReport
fuzzDir' a
n' =
      (FuzzEnv -> FuzzEnv) -> Fuzz m FuzzReport -> Fuzz m FuzzReport
forall a.
(FuzzEnv -> FuzzEnv)
-> StateT FuzzState (ReaderT FuzzEnv m) a
-> StateT FuzzState (ReaderT FuzzEnv m) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local
        ( (FuzzOpts -> Identity FuzzOpts) -> FuzzEnv -> Identity FuzzEnv
Lens' FuzzEnv FuzzOpts
fuzzEnvOpts ((FuzzOpts -> Identity FuzzOpts) -> FuzzEnv -> Identity FuzzEnv)
-> ((Maybe FilePath -> Identity (Maybe FilePath))
    -> FuzzOpts -> Identity FuzzOpts)
-> (Maybe FilePath -> Identity (Maybe FilePath))
-> FuzzEnv
-> Identity FuzzEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe FilePath -> Identity (Maybe FilePath))
-> FuzzOpts -> Identity FuzzOpts
Lens' FuzzOpts (Maybe FilePath)
fuzzOptsOutput
            ((Maybe FilePath -> Identity (Maybe FilePath))
 -> FuzzEnv -> Identity FuzzEnv)
-> Maybe FilePath -> FuzzEnv -> FuzzEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath)
-> (Text -> FilePath) -> Text -> Maybe FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
fromText (Text -> Maybe FilePath) -> Text -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ Text
"fuzz_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. Show a => a -> Text
showT a
n')
        )
        (Fuzz m FuzzReport -> Fuzz m FuzzReport)
-> Fuzz m FuzzReport -> Fuzz m FuzzReport
forall a b. (a -> b) -> a -> b
$ (Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDirG Gen (SourceInfo ann) -> Fuzz m FuzzReport
f Gen (SourceInfo ann)
src

sampleSeed :: (MonadSh m) => Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed :: forall (m :: * -> *) a.
MonadSh m =>
Maybe Seed -> Gen a -> m (Seed, a)
sampleSeed Maybe Seed
s Gen a
gen =
  Sh (Seed, a) -> m (Seed, a)
forall a. Sh a -> m a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh (Sh (Seed, a) -> m (Seed, a)) -> Sh (Seed, a) -> m (Seed, a)
forall a b. (a -> b) -> a -> b
$
    let loop :: t -> m (Seed, a)
loop t
n =
          if t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
<= t
0
            then
              FilePath -> m (Seed, a)
forall a. HasCallStack => FilePath -> a
error
                FilePath
"Hedgehog.Gen.sample: too many discards, could not generate a sample"
            else do
              Seed
seed <- m Seed -> (Seed -> m Seed) -> Maybe Seed -> m Seed
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Seed
forall (m :: * -> *). MonadIO m => m Seed
Hog.random Seed -> m Seed
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Seed
s
              case Size -> Seed -> Gen a -> Maybe (Tree a)
forall a. Size -> Seed -> Gen a -> Maybe (Tree a)
Hog.evalGen Size
30 Seed
seed Gen a
gen of
                Maybe (Tree a)
Nothing ->
                  t -> m (Seed, a)
loop (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1)
                Just Tree a
x ->
                  (Seed, a) -> m (Seed, a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seed
seed, Tree a -> a
forall a. Tree a -> a
Hog.treeValue Tree a
x)
     in Int -> Sh (Seed, a)
forall {t} {m :: * -> *}.
(Ord t, Num t, MonadIO m) =>
t -> m (Seed, a)
loop (Int
100 :: Int)

fuzzEMI :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzEMI :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzEMI Gen (SourceInfo (EMIInputs ann))
gen = do
  Config
conf <- Fuzz m Config
forall (m :: * -> *). Monad m => Fuzz m Config
askConfig
  FuzzOpts
opts <- Fuzz m FuzzOpts
forall (m :: * -> *). Monad m => Fuzz m FuzzOpts
askOpts
  let seed :: Maybe Seed
seed = Config
conf Config -> Getting (Maybe Seed) Config (Maybe Seed) -> Maybe Seed
forall s a. s -> Getting a s a -> a
^. (ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Config -> Const (Maybe Seed) Config
Lens' Config ConfProperty
configProperty ((ConfProperty -> Const (Maybe Seed) ConfProperty)
 -> Config -> Const (Maybe Seed) Config)
-> ((Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
    -> ConfProperty -> Const (Maybe Seed) ConfProperty)
-> Getting (Maybe Seed) Config (Maybe Seed)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Seed -> Const (Maybe Seed) (Maybe Seed))
-> ConfProperty -> Const (Maybe Seed) ConfProperty
Lens' ConfProperty (Maybe Seed)
propSeed
  (Seed
seed', SourceInfo (EMIInputs ann)
src) <- Fuzz m (Seed, SourceInfo (EMIInputs ann))
-> Fuzz m (Seed, SourceInfo (EMIInputs ann))
forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
Fuzz m (Seed, SourceInfo ann) -> Fuzz m (Seed, SourceInfo ann)
generateSample (Fuzz m (Seed, SourceInfo (EMIInputs ann))
 -> Fuzz m (Seed, SourceInfo (EMIInputs ann)))
-> Fuzz m (Seed, SourceInfo (EMIInputs ann))
-> Fuzz m (Seed, SourceInfo (EMIInputs ann))
forall a b. (a -> b) -> a -> b
$ Config
-> Maybe Seed
-> Gen (SourceInfo (EMIInputs ann))
-> Fuzz m (Seed, SourceInfo (EMIInputs ann))
forall {m :: * -> *} {a}.
(MonadSh m, MonadIO m, Source a, Ord a) =>
Config -> Maybe Seed -> Gen a -> m (Seed, a)
genMethod Config
conf Maybe Seed
seed Gen (SourceInfo (EMIInputs ann))
gen
  let size :: Int
size = [FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([FilePath] -> Int) -> (Text -> [FilePath]) -> Text -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines (FilePath -> [FilePath])
-> (Text -> FilePath) -> Text -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack (Text -> Int) -> Text -> Int
forall a b. (a -> b) -> a -> b
$ SourceInfo (EMIInputs ann) -> Text
forall a. Source a => a -> Text
genSource SourceInfo (EMIInputs ann)
src
  Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh
    (Sh () -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> (Config -> Sh ())
-> Config
-> StateT FuzzState (ReaderT FuzzEnv m) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text -> Sh ()
writefile FilePath
"config.toml"
    (Text -> Sh ()) -> (Config -> Text) -> Config -> Sh ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Text
encodeConfig
    (Config -> StateT FuzzState (ReaderT FuzzEnv m) ())
-> Config -> StateT FuzzState (ReaderT FuzzEnv m) ()
forall a b. (a -> b) -> a -> b
$ Config
conf
      Config -> (Config -> Config) -> Config
forall a b. a -> (a -> b) -> b
& (ConfProperty -> Identity ConfProperty)
-> Config -> Identity Config
Lens' Config ConfProperty
configProperty
        ((ConfProperty -> Identity ConfProperty)
 -> Config -> Identity Config)
-> ((Maybe Seed -> Identity (Maybe Seed))
    -> ConfProperty -> Identity ConfProperty)
-> (Maybe Seed -> Identity (Maybe Seed))
-> Config
-> Identity Config
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Seed -> Identity (Maybe Seed))
-> ConfProperty -> Identity ConfProperty
Lens' ConfProperty (Maybe Seed)
propSeed
        ((Maybe Seed -> Identity (Maybe Seed))
 -> Config -> Identity Config)
-> Seed -> Config -> Config
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ Seed
seed'
  (NominalDiffTime
tsynth, ()
_) <- Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Synthesis" (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall a b. (a -> b) -> a -> b
$ SourceInfo (EMIInputs ann)
-> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann.
(MonadBaseControl IO m, MonadSh m, Show ann) =>
SourceInfo ann -> Fuzz m ()
synthesis SourceInfo (EMIInputs ann)
src
  (NominalDiffTime
_, ()
_) <-
    if (FuzzOpts -> Bool
_fuzzOptsNoSim FuzzOpts
opts)
      then (NominalDiffTime, ()) -> Fuzz m (NominalDiffTime, ())
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime
0, ()
forall a. Monoid a => a
mempty)
      else Text
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall (m :: * -> *) a.
(MonadIO m, MonadSh m) =>
Text -> Fuzz m a -> Fuzz m (NominalDiffTime, a)
titleRun Text
"Simulation" (StateT FuzzState (ReaderT FuzzEnv m) ()
 -> Fuzz m (NominalDiffTime, ()))
-> StateT FuzzState (ReaderT FuzzEnv m) ()
-> Fuzz m (NominalDiffTime, ())
forall a b. (a -> b) -> a -> b
$ SourceInfo (EMIInputs ann)
-> StateT FuzzState (ReaderT FuzzEnv m) ()
forall (m :: * -> *) ann.
(MonadIO m, MonadSh m, Show ann) =>
SourceInfo (EMIInputs ann) -> Fuzz m ()
simulationEMI SourceInfo (EMIInputs ann)
src
  [SynthResult]
fails <- Fuzz m [SynthResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthResult]
failEquivWithIdentity
  [SimResult]
failedSim <- Fuzz m [SimResult]
forall (m :: * -> *). MonadSh m => Fuzz m [SimResult]
failedSimulations
  [SynthTool]
synthFails <- Fuzz m [SynthTool]
forall (m :: * -> *). MonadSh m => Fuzz m [SynthTool]
failedSynthesis
  FuzzState
state_ <- StateT FuzzState (ReaderT FuzzEnv m) FuzzState
forall s (m :: * -> *). MonadState s m => m s
get
  FilePath
currdir <- Sh FilePath -> StateT FuzzState (ReaderT FuzzEnv m) FilePath
forall a. Sh a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. MonadSh m => Sh a -> m a
liftSh Sh FilePath
pwd
  let vi :: Getting c FuzzState c -> c
vi = (Getting c FuzzState c -> FuzzState -> c)
-> FuzzState -> Getting c FuzzState c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip Getting c FuzzState c -> FuzzState -> c
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view FuzzState
state_
  let report :: FuzzReport
report =
        FilePath
-> [SynthResult]
-> [SimResult]
-> [SynthStatus]
-> Int
-> NominalDiffTime
-> NominalDiffTime
-> NominalDiffTime
-> FuzzReport
FuzzReport
          FilePath
currdir
          (Getting [SynthResult] FuzzState [SynthResult] -> [SynthResult]
forall {c}. Getting c FuzzState c -> c
vi Getting [SynthResult] FuzzState [SynthResult]
Lens' FuzzState [SynthResult]
fuzzSynthResults)
          (Getting [SimResult] FuzzState [SimResult] -> [SimResult]
forall {c}. Getting c FuzzState c -> c
vi Getting [SimResult] FuzzState [SimResult]
Lens' FuzzState [SimResult]
fuzzSimResults)
          (Getting [SynthStatus] FuzzState [SynthStatus] -> [SynthStatus]
forall {c}. Getting c FuzzState c -> c
vi Getting [SynthStatus] FuzzState [SynthStatus]
Lens' FuzzState [SynthStatus]
fuzzSynthStatus)
          Int
size
          NominalDiffTime
tsynth
          NominalDiffTime
0
          NominalDiffTime
0
  FuzzReport -> Fuzz m FuzzReport
forall a. a -> StateT FuzzState (ReaderT FuzzEnv m) a
forall (m :: * -> *) a. Monad m => a -> m a
return FuzzReport
report

fuzzInDir :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDir :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDir = (Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDirG Gen (SourceInfo ann) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzz

fuzzInDirEMI :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzInDirEMI :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzInDirEMI = (Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport)
-> Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzzInDirG Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzEMI

fuzzMultiple :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultiple :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultiple = (Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultipleG Gen (SourceInfo ann) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo ann) -> Fuzz m FuzzReport
fuzz

fuzzMultipleEMI :: (MonadFuzz m, Ord ann, Show ann) => Gen (SourceInfo (EMIInputs ann)) -> Fuzz m [FuzzReport]
fuzzMultipleEMI :: forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m [FuzzReport]
fuzzMultipleEMI = (Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport)
-> Gen (SourceInfo (EMIInputs ann)) -> Fuzz m [FuzzReport]
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
(Gen (SourceInfo ann) -> Fuzz m FuzzReport)
-> Gen (SourceInfo ann) -> Fuzz m [FuzzReport]
fuzzMultipleG Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
forall (m :: * -> *) ann.
(MonadFuzz m, Ord ann, Show ann) =>
Gen (SourceInfo (EMIInputs ann)) -> Fuzz m FuzzReport
fuzzEMI