{-|
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 { NonceT s m a -> ReaderT (NonceGenerator m s) m a
runNonceT :: ReaderT (NonceGenerator m s) m a }
  deriving (a -> NonceT s m b -> NonceT s m a
(a -> b) -> NonceT s m a -> NonceT s m b
(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
<$ :: a -> NonceT s m b -> NonceT s m a
$c<$ :: forall s (m :: * -> *) a b.
Functor m =>
a -> NonceT s m b -> NonceT s m a
fmap :: (a -> b) -> NonceT s m a -> NonceT s m b
$cfmap :: forall s (m :: * -> *) a b.
Functor m =>
(a -> b) -> NonceT s m a -> NonceT s m b
Functor, Functor (NonceT s m)
a -> NonceT s m a
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)
NonceT s m a -> NonceT s m b -> NonceT s m b
NonceT s m a -> NonceT s m b -> NonceT s m a
NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
(a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
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
<* :: NonceT s m a -> NonceT s m b -> NonceT s m a
$c<* :: forall s (m :: * -> *) a b.
Applicative m =>
NonceT s m a -> NonceT s m b -> NonceT s m a
*> :: 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 b
liftA2 :: (a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
$cliftA2 :: forall s (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> NonceT s m a -> NonceT s m b -> NonceT s m c
<*> :: NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
$c<*> :: forall s (m :: * -> *) a b.
Applicative m =>
NonceT s m (a -> b) -> NonceT s m a -> NonceT s m b
pure :: a -> NonceT s m a
$cpure :: forall s (m :: * -> *) a. Applicative m => a -> NonceT s m a
$cp1Applicative :: forall s (m :: * -> *). Applicative m => Functor (NonceT s m)
Applicative, Applicative (NonceT s m)
a -> NonceT s m a
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)
NonceT s m a -> (a -> NonceT s m b) -> NonceT s m b
NonceT s m a -> NonceT s m b -> NonceT s m b
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
return :: a -> NonceT s m a
$creturn :: forall s (m :: * -> *) a. Monad m => a -> NonceT s m a
>> :: NonceT s m 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
>>= :: 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 -> (a -> NonceT s m b) -> NonceT s m b
$cp1Monad :: forall s (m :: * -> *). Monad m => Applicative (NonceT s m)
Monad)

instance MonadTrans (NonceT s) where
  lift :: 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 (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 :: NonceT s m (Nonce (NonceSet (NonceT s m)) tp)
freshNonceM = ReaderT (NonceGenerator m s) m (Nonce s tp)
-> NonceT s m (Nonce s tp)
forall s (m :: * -> *) a.
ReaderT (NonceGenerator m s) m a -> NonceT s m a
NonceT (ReaderT (NonceGenerator m s) m (Nonce s tp)
 -> NonceT s m (Nonce s tp))
-> ReaderT (NonceGenerator m s) m (Nonce s tp)
-> NonceT s m (Nonce s tp)
forall a b. (a -> b) -> a -> b
$ m (Nonce s tp) -> ReaderT (NonceGenerator m s) m (Nonce s tp)
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 :: StateT s m (Nonce (NonceSet (StateT s m)) tp)
freshNonceM = m (Nonce (NonceSet m) tp) -> StateT s m (Nonce (NonceSet m) tp)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Nonce (NonceSet m) tp) -> StateT s m (Nonce (NonceSet m) tp))
-> m (Nonce (NonceSet m) tp) -> StateT s m (Nonce (NonceSet m) tp)
forall a b. (a -> b) -> a -> b
$ 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 :: NonceST t s (NonceGenerator (ST t) s)
getNonceSTGen = ReaderT (NonceGenerator (ST t) s) (ST t) (NonceGenerator (ST t) s)
-> NonceST t s (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 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 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