-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Utils.ExtractIO
-- Copyright : (c) Brian Schroeder
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Helper typeclass for interoperation with APIs which take IO actions in
-- negative position.
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Utils.ExtractIO where

import Control.Monad.Except      (ExceptT(ExceptT), runExceptT)
import Control.Monad.IO.Class    (MonadIO)
import Control.Monad.Trans.Maybe (MaybeT(MaybeT), runMaybeT)

import qualified Control.Monad.Writer.Lazy   as LW
import qualified Control.Monad.Writer.Strict as SW

-- | Monads which support 'IO' operations and can extract all 'IO' behavior for
-- interoperation with functions like 'Control.Concurrent.catches', which takes
-- an 'IO' action in negative position. This function can not be implemented
-- for transformers like @ReaderT r@ or @StateT s@, whose resultant 'IO'
-- actions are a function of some environment or state.
class MonadIO m => ExtractIO m where
    -- | Law: the @m a@ yielded by 'IO' is pure with respect to 'IO'.
    extractIO :: m a -> IO (m a)

-- | Trivial IO extraction for 'IO'.
instance ExtractIO IO where
    extractIO :: IO a -> IO (IO a)
extractIO = IO a -> IO (IO a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | IO extraction for 'MaybeT'.
instance ExtractIO m => ExtractIO (MaybeT m) where
    extractIO :: MaybeT m a -> IO (MaybeT m a)
extractIO = (m (Maybe a) -> MaybeT m a) -> IO (m (Maybe a)) -> IO (MaybeT m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (m (Maybe a)) -> IO (MaybeT m a))
-> (MaybeT m a -> IO (m (Maybe a)))
-> MaybeT m a
-> IO (MaybeT m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe a) -> IO (m (Maybe a))
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m (Maybe a) -> IO (m (Maybe a)))
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> IO (m (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m a -> m (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT

-- | IO extraction for 'ExceptT'.
instance ExtractIO m => ExtractIO (ExceptT e m) where
    extractIO :: ExceptT e m a -> IO (ExceptT e m a)
extractIO = (m (Either e a) -> ExceptT e m a)
-> IO (m (Either e a)) -> IO (ExceptT e m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (IO (m (Either e a)) -> IO (ExceptT e m a))
-> (ExceptT e m a -> IO (m (Either e a)))
-> ExceptT e m a
-> IO (ExceptT e m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Either e a) -> IO (m (Either e a))
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m (Either e a) -> IO (m (Either e a)))
-> (ExceptT e m a -> m (Either e a))
-> ExceptT e m a
-> IO (m (Either e a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT e m a -> m (Either e a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT

-- | IO extraction for lazy 'LW.WriterT'.
instance (Monoid w, ExtractIO m) => ExtractIO (LW.WriterT w m) where
    extractIO :: WriterT w m a -> IO (WriterT w m a)
extractIO = (m (a, w) -> WriterT w m a) -> IO (m (a, w)) -> IO (WriterT w m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
LW.WriterT (IO (m (a, w)) -> IO (WriterT w m a))
-> (WriterT w m a -> IO (m (a, w)))
-> WriterT w m a
-> IO (WriterT w m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (a, w) -> IO (m (a, w))
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m (a, w) -> IO (m (a, w)))
-> (WriterT w m a -> m (a, w)) -> WriterT w m a -> IO (m (a, w))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT w m a -> m (a, w)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
LW.runWriterT

-- | IO extraction for strict 'SW.WriterT'.
instance (Monoid w, ExtractIO m) => ExtractIO (SW.WriterT w m) where
    extractIO :: WriterT w m a -> IO (WriterT w m a)
extractIO = (m (a, w) -> WriterT w m a) -> IO (m (a, w)) -> IO (WriterT w m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (a, w) -> WriterT w m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
SW.WriterT (IO (m (a, w)) -> IO (WriterT w m a))
-> (WriterT w m a -> IO (m (a, w)))
-> WriterT w m a
-> IO (WriterT w m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (a, w) -> IO (m (a, w))
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m (a, w) -> IO (m (a, w)))
-> (WriterT w m a -> m (a, w)) -> WriterT w m a -> IO (m (a, w))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT w m a -> m (a, w)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
SW.runWriterT