In dev: Purify pirouette using a pure solve function, no more IO from the symbolic engine.

[VictorCMiraldo]

In #99 we remove the explicit calls to a monadic solver session from the symbolic engine; Solving issue #106 will remove enough dependencies that will enable us to completely removing IO from the symbolic engine: it shouldn't be in any type, including the interface functions. Pirouette will be totally "pure" at that point.

For the record, here's the proposed solve function:

{-# NOINLINE solve #-}
solve :: forall domain res . Solve domain => Ctx domain -> Problem domain res -> res
solve ctx = unsafePerformIO $ do
  -- Launch all our worker processes similar to how we did it in TypedProcess2.hs; but now
  -- we end up with a list of MVars, which we will protect in another MVar.
  allProcs <- launchAll @domain ctx >>= newMStack

  -- Finally, we return the actual closure, the internals make sure
  -- to use 'withMVar' to not mess up the command/response pairs.
  return $ \problem -> unsafePerformIO $ do
    ms <- popMStack allProcs
    r <- withMVar ms $ \solver -> do
      -- TODO: what happens in an exception? For now, we just loose a solver but we shouldn't
      -- add it to the pool of workers and just retry the problem. In a future implementation
      -- we could try launching it again
      solveProblem @domain problem solver
    pushMStack ms allProcs
    return r

launchAll :: forall domain . Solve domain => Ctx domain -> IO [MVar X.Solver]
launchAll ctx = replicateM numCapabilities $ do
  s <- X.launchSolverWithFinalizer "cvc4 --lang=smt2 --incremental --fmf-fun" debug0
  initSolver @domain ctx s
  newMVar s
  where
    -- TODO: these constants should become parameters at some point; the solver command too!

    numCapabilities :: Int
    numCapabilities = 4

    debug0 :: Bool
    debug0 = False

-- * Async Locks

type Lock = MVar ()

newLock :: IO Lock
newLock = newMVar ()

withLock :: Lock -> IO a -> IO a
withLock lock act = withMVar lock $ Prelude.const act

-- * Async Queues

-- |A MStack is a MVar that satisfies the invariant that it never contains
-- an empty list; if that's the case then the MVar is empty.
type MStack a = (Lock, MVar [a])

newMStack :: [a] -> IO (MStack a)
newMStack [] = (,) <$> newLock <*> newEmptyMVar
newMStack xs = (,) <$> newLock <*> newMVar xs

pushMStack :: a -> MStack a -> IO ()
pushMStack a (l, q) = withLock l $ do
  mas <- tryTakeMVar q
  case mas of
    Nothing -> putMVar q [a]
    Just as0 -> putMVar q (a:as0)

popMStack :: MStack a -> IO a
popMStack (l, q) = withLock l $ do
  xss <- takeMVar q
  case xss of
    [] -> error "invariant disrespected; MStack should never be empty"
    [x] -> return x
    (x:xs) -> putMVar q xs >> return x