    {-|
    Description : A typeclass and monad transformers for generating nonces.
    Copyright   : (c) Galois, Inc 2014-2019
    Maintainer  : Eddy Westbrook <westbrook@galois.com>

    This module provides a typeclass and monad transformers for generating
    nonces.
    -}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE TypeFamilies #-}
    module Data.Parameterized.Nonce.Transformers
      ( MonadNonce(..)
      , NonceT(..)
      , NonceST
      , NonceIO
      , getNonceSTGen
      , runNonceST
      , runNonceIO
      , module Data.Parameterized.Nonce
      ) where

    import Control.Monad.Reader
    import Control.Monad.ST
    import Control.Monad.State
    import Data.Kind

    import Data.Parameterized.Nonce

    -- | A 'MonadNonce' is a monad that can generate fresh 'Nonce's in a given set
    -- (where we view the phantom type parameter of 'Nonce' as a designator of the
    -- set that the 'Nonce' came from).
    class Monad m => MonadNonce m where
      type NonceSet m :: Type
      freshNonceM :: forall k (tp :: k) . m (Nonce (NonceSet m) tp)

    -- | This transformer adds a nonce generator to a given monad.
    newtype NonceT s m a =
      NonceT { forall s (m :: * -> *) a.
    NonceT s m a -> ReaderT (NonceGenerator m s) m a
    runNonceT :: ReaderT (NonceGenerator m s) m a }
      deriving ((forall a b. (a -> b) -> NonceT s m a -> NonceT s m b)
    -> (forall a b. a -> NonceT s m b -> NonceT s m a)
    -> Functor (NonceT s m)
    forall a b. a -> NonceT s m b -> NonceT s m a
    forall a b. (a -> b) -> NonceT s m a -> NonceT s m b
    forall s (m :: * -> *) a b.
    Functor m =>
    a -> NonceT s m b -> NonceT s m a
    forall s (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> NonceT s m a -> NonceT s m b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall s (m :: * -> *) a b.
    Functor m =>
    (a -> b) -> NonceT s m a -> NonceT s m b
    fmap :: forall a b. (a -> b) -> NonceT s m a -> NonceT s m b
    $c<$ :: forall s (m :: * -> *) a b.
    Functor m =>
    a -> NonceT s m b -> NonceT s m a
    <$ :: forall a b. a -> NonceT s m b -> NonceT s m a
    Functor, Functor (NonceT s m)
    Functor (NonceT s m) =>
    (forall a. a -> NonceT s m a)
    -> (forall a b.
        NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b)
    -> (forall a b c.
        (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c)
    -> (forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b)
    -> (forall a b. NonceT s m a -> NonceT s m b -> NonceT s m a)
    -> Applicative (NonceT s m)
    forall a. a -> NonceT s m a
    forall a b. NonceT s m a -> NonceT s m b -> NonceT s m a
    forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b
    forall a b. NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
    forall a b c.
    (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
    forall s (m :: * -> *). Applicative m => Functor (NonceT s m)
    forall s (m :: * -> *) a. Applicative m => a -> NonceT s m a
    forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m a -> NonceT s m b -> NonceT s m a
    forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m a -> NonceT s m b -> NonceT s m b
    forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
    forall s (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall s (m :: * -> *) a. Applicative m => a -> NonceT s m a
    pure :: forall a. a -> NonceT s m a
    $c<*> :: forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
    <*> :: forall a b. NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
    $cliftA2 :: forall s (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
    liftA2 :: forall a b c.
    (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
    $c*> :: forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m a -> NonceT s m b -> NonceT s m b
    *> :: forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b
    $c<* :: forall s (m :: * -> *) a b.
    Applicative m =>
    NonceT s m a -> NonceT s m b -> NonceT s m a
    <* :: forall a b. NonceT s m a -> NonceT s m b -> NonceT s m a
    Applicative, Applicative (NonceT s m)
    Applicative (NonceT s m) =>
    (forall a b. NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b)
    -> (forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b)
    -> (forall a. a -> NonceT s m a)
    -> Monad (NonceT s m)
    forall a. a -> NonceT s m a
    forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b
    forall a b. NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b
    forall s (m :: * -> *). Monad m => Applicative (NonceT s m)
    forall s (m :: * -> *) a. Monad m => a -> NonceT s m a
    forall s (m :: * -> *) a b.
    Monad m =>
    NonceT s m a -> NonceT s m b -> NonceT s m b
    forall s (m :: * -> *) a b.
    Monad m =>
    NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall s (m :: * -> *) a b.
    Monad m =>
    NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b
    >>= :: forall a b. NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b
    $c>> :: forall s (m :: * -> *) a b.
    Monad m =>
    NonceT s m a -> NonceT s m b -> NonceT s m b
    >> :: forall a b. NonceT s m a -> NonceT s m b -> NonceT s m b
    $creturn :: forall s (m :: * -> *) a. Monad m => a -> NonceT s m a
    return :: forall a. a -> NonceT s m a
    Monad)

    instance MonadTrans (NonceT s) where
      lift :: forall (m :: * -> *) a. Monad m => m a -> NonceT s m a
    lift m a
    m = ReaderT (NonceGenerator m s) m a -> NonceT s m a
    forall s (m :: * -> *) a.
    ReaderT (NonceGenerator m s) m a -> NonceT s m a
    NonceT (ReaderT (NonceGenerator m s) m a -> NonceT s m a)
    -> ReaderT (NonceGenerator m s) m a -> NonceT s m a
    forall a b. (a -> b) -> a -> b
    $ m a -> ReaderT (NonceGenerator m s) m a
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT (NonceGenerator m s) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift m a
    m

    instance Monad m => MonadNonce (NonceT s m) where
      type NonceSet (NonceT s m) = s
      freshNonceM :: forall k (tp :: k). NonceT s m (Nonce (NonceSet (NonceT s m)) tp)
    freshNonceM = ReaderT (NonceGenerator m s) m (Nonce (NonceSet (NonceT s m)) tp)
    -> NonceT s m (Nonce (NonceSet (NonceT s m)) tp)
    forall s (m :: * -> *) a.
    ReaderT (NonceGenerator m s) m a -> NonceT s m a
    NonceT (ReaderT (NonceGenerator m s) m (Nonce (NonceSet (NonceT s m)) tp)
     -> NonceT s m (Nonce (NonceSet (NonceT s m)) tp))
    -> ReaderT
         (NonceGenerator m s) m (Nonce (NonceSet (NonceT s m)) tp)
    -> NonceT s m (Nonce (NonceSet (NonceT s m)) tp)
    forall a b. (a -> b) -> a -> b
    $ m (Nonce s tp) -> ReaderT (NonceGenerator m s) m (Nonce s tp)
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ReaderT (NonceGenerator m s) m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Nonce s tp) -> ReaderT (NonceGenerator m s) m (Nonce s tp))
    -> (NonceGenerator m s -> m (Nonce s tp))
    -> NonceGenerator m s
    -> ReaderT (NonceGenerator m s) m (Nonce s tp)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NonceGenerator m s -> m (Nonce s tp)
    forall (m :: * -> *) s k (tp :: k).
    NonceGenerator m s -> m (Nonce s tp)
    freshNonce (NonceGenerator m s -> ReaderT (NonceGenerator m s) m (Nonce s tp))
    -> ReaderT (NonceGenerator m s) m (NonceGenerator m s)
    -> ReaderT (NonceGenerator m s) m (Nonce s tp)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT (NonceGenerator m s) m (NonceGenerator m s)
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    instance MonadNonce m => MonadNonce (StateT s m) where
      type NonceSet (StateT s m) = NonceSet m
      freshNonceM :: forall k (tp :: k). StateT s m (Nonce (NonceSet (StateT s m)) tp)
    freshNonceM = m (Nonce (NonceSet (StateT s m)) tp)
    -> StateT s m (Nonce (NonceSet (StateT s m)) tp)
    forall (m :: * -> *) a. Monad m => m a -> StateT s m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m (Nonce (NonceSet (StateT s m)) tp)
     -> StateT s m (Nonce (NonceSet (StateT s m)) tp))
    -> m (Nonce (NonceSet (StateT s m)) tp)
    -> StateT s m (Nonce (NonceSet (StateT s m)) tp)
    forall a b. (a -> b) -> a -> b
    $ m (Nonce (NonceSet m) tp)
    m (Nonce (NonceSet (StateT s m)) tp)
    forall k (tp :: k). m (Nonce (NonceSet m) tp)
    forall (m :: * -> *) k (tp :: k).
    MonadNonce m =>
    m (Nonce (NonceSet m) tp)
    freshNonceM

    -- | Helper type to build a 'MonadNonce' from the 'ST' monad.
    type NonceST t s = NonceT s (ST t)

    -- | Helper type to build a 'MonadNonce' from the 'IO' monad.
    type NonceIO s = NonceT s IO

    -- | Return the actual 'NonceGenerator' used in an 'ST' computation.
    getNonceSTGen :: NonceST t s (NonceGenerator (ST t) s)
    getNonceSTGen :: forall t s. NonceST t s (NonceGenerator (ST t) s)
    getNonceSTGen = ReaderT (NonceGenerator (ST t) s) (ST t) (NonceGenerator (ST t) s)
    -> NonceT s (ST t) (NonceGenerator (ST t) s)
    forall s (m :: * -> *) a.
    ReaderT (NonceGenerator m s) m a -> NonceT s m a
    NonceT ReaderT (NonceGenerator (ST t) s) (ST t) (NonceGenerator (ST t) s)
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    -- | Run a 'NonceST' computation with a fresh 'NonceGenerator'.
    runNonceST :: (forall t s. NonceST t s a) -> a
    runNonceST :: forall a. (forall t s. NonceST t s a) -> a
    runNonceST forall t s. NonceST t s a
    m = (forall s. ST s a) -> a
    forall a. (forall s. ST s a) -> a
    runST ((forall s. ST s a) -> a) -> (forall s. ST s a) -> a
    forall a b. (a -> b) -> a -> b
    $ (forall s. NonceGenerator (ST s) s -> ST s a) -> ST s a
    forall t r. (forall s. NonceGenerator (ST t) s -> ST t r) -> ST t r
    withSTNonceGenerator ((forall s. NonceGenerator (ST s) s -> ST s a) -> ST s a)
    -> (forall s. NonceGenerator (ST s) s -> ST s a) -> ST s a
    forall a b. (a -> b) -> a -> b
    $ ReaderT (NonceGenerator (ST s) s) (ST s) a
    -> NonceGenerator (ST s) s -> ST s a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (ReaderT (NonceGenerator (ST s) s) (ST s) a
     -> NonceGenerator (ST s) s -> ST s a)
    -> ReaderT (NonceGenerator (ST s) s) (ST s) a
    -> NonceGenerator (ST s) s
    -> ST s a
    forall a b. (a -> b) -> a -> b
    $ NonceT s (ST s) a -> ReaderT (NonceGenerator (ST s) s) (ST s) a
    forall s (m :: * -> *) a.
    NonceT s m a -> ReaderT (NonceGenerator m s) m a
    runNonceT NonceT s (ST s) a
    forall t s. NonceST t s a
    m

    -- | Run a 'NonceIO' computation with a fresh 'NonceGenerator' inside 'IO'.
    runNonceIO :: (forall s. NonceIO s a) -> IO a
    runNonceIO :: forall a. (forall s. NonceIO s a) -> IO a
    runNonceIO forall s. NonceIO s a
    m = (forall s. NonceGenerator IO s -> IO a) -> IO a
    forall r. (forall s. NonceGenerator IO s -> IO r) -> IO r
    withIONonceGenerator ((forall s. NonceGenerator IO s -> IO a) -> IO a)
    -> (forall s. NonceGenerator IO s -> IO a) -> IO a
    forall a b. (a -> b) -> a -> b
    $ ReaderT (NonceGenerator IO s) IO a -> NonceGenerator IO s -> IO a
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (ReaderT (NonceGenerator IO s) IO a -> NonceGenerator IO s -> IO a)
    -> ReaderT (NonceGenerator IO s) IO a
    -> NonceGenerator IO s
    -> IO a
    forall a b. (a -> b) -> a -> b
    $ NonceT s IO a -> ReaderT (NonceGenerator IO s) IO a
    forall s (m :: * -> *) a.
    NonceT s m a -> ReaderT (NonceGenerator m s) m a
    runNonceT NonceT s IO a
    forall s. NonceIO s a
    m