-- |
-- Module     : Unbound.Generics.LocallyNameless.Fresh
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Global freshness monad.
{-# LANGUAGE CPP, GeneralizedNewtypeDeriving,
             FlexibleInstances, MultiParamTypeClasses,
             StandaloneDeriving,
             UndecidableInstances
  #-}
-- (we expect deprecation warnings about Control.Monad.Trans.Error)
{-# OPTIONS_GHC -Wwarn #-}
module Unbound.Generics.LocallyNameless.Fresh where

import Control.Applicative (Applicative, Alternative)
import Control.Monad ()

import Control.Monad.Identity

import Control.Monad.Catch (MonadThrow, MonadCatch, MonadMask)
#if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail
#endif
#if MIN_VERSION_mtl(2,3,0)
import Control.Monad (MonadPlus)
import Control.Monad.Fix (MonadFix)
#endif
import Control.Monad.Trans
import Control.Monad.Trans.Except
#if !MIN_VERSION_transformers(0,6,0)
import Control.Monad.Trans.Error
#endif
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Reader
import Control.Monad.Trans.State.Lazy as Lazy
import Control.Monad.Trans.State.Strict as Strict
import Control.Monad.Trans.Writer.Lazy as Lazy
import Control.Monad.Trans.Writer.Strict as Strict

import qualified Control.Monad.Cont.Class as CC
import qualified Control.Monad.Error.Class as EC
import qualified Control.Monad.State.Class as StC
import qualified Control.Monad.Reader.Class as RC
import qualified Control.Monad.Writer.Class as WC

import Data.Monoid (Monoid)

import qualified Control.Monad.State as St

import Unbound.Generics.LocallyNameless.Name

-- | The @Fresh@ type class governs monads which can generate new
--   globally unique 'Name's based on a given 'Name'.
class Monad m => Fresh m where

  -- | Generate a new globally unique name based on the given one.
  fresh :: Name a -> m (Name a)


-- | The @FreshM@ monad transformer.  Keeps track of the lowest index
--   still globally unused, and increments the index every time it is
--   asked for a fresh name.
newtype FreshMT m a = FreshMT { forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT :: St.StateT Integer m a }
  deriving
    ( (forall a b. (a -> b) -> FreshMT m a -> FreshMT m b)
-> (forall a b. a -> FreshMT m b -> FreshMT m a)
-> Functor (FreshMT m)
forall a b. a -> FreshMT m b -> FreshMT m a
forall a b. (a -> b) -> FreshMT m a -> FreshMT m b
forall (m :: * -> *) a b.
Functor m =>
a -> FreshMT m b -> FreshMT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> FreshMT m a -> FreshMT 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 (m :: * -> *) a b.
Functor m =>
(a -> b) -> FreshMT m a -> FreshMT m b
fmap :: forall a b. (a -> b) -> FreshMT m a -> FreshMT m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> FreshMT m b -> FreshMT m a
<$ :: forall a b. a -> FreshMT m b -> FreshMT m a
Functor
    , Functor (FreshMT m)
Functor (FreshMT m)
-> (forall a. a -> FreshMT m a)
-> (forall a b. FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b)
-> (forall a b c.
    (a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT m c)
-> (forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b)
-> (forall a b. FreshMT m a -> FreshMT m b -> FreshMT m a)
-> Applicative (FreshMT m)
forall a. a -> FreshMT m a
forall a b. FreshMT m a -> FreshMT m b -> FreshMT m a
forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b
forall a b. FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b
forall a b c.
(a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT m c
forall {m :: * -> *}. Monad m => Functor (FreshMT m)
forall (m :: * -> *) a. Monad m => a -> FreshMT m a
forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m a
forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m b
forall (m :: * -> *) a b.
Monad m =>
FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT 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 (m :: * -> *) a. Monad m => a -> FreshMT m a
pure :: forall a. a -> FreshMT m a
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b
<*> :: forall a b. FreshMT m (a -> b) -> FreshMT m a -> FreshMT m b
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT m c
liftA2 :: forall a b c.
(a -> b -> c) -> FreshMT m a -> FreshMT m b -> FreshMT m c
$c*> :: forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m b
*> :: forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b
$c<* :: forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m a
<* :: forall a b. FreshMT m a -> FreshMT m b -> FreshMT m a
Applicative
    , Applicative (FreshMT m)
Applicative (FreshMT m)
-> (forall a. FreshMT m a)
-> (forall a. FreshMT m a -> FreshMT m a -> FreshMT m a)
-> (forall a. FreshMT m a -> FreshMT m [a])
-> (forall a. FreshMT m a -> FreshMT m [a])
-> Alternative (FreshMT m)
forall a. FreshMT m a
forall a. FreshMT m a -> FreshMT m [a]
forall a. FreshMT m a -> FreshMT m a -> FreshMT m a
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall {m :: * -> *}. MonadPlus m => Applicative (FreshMT m)
forall (m :: * -> *) a. MonadPlus m => FreshMT m a
forall (m :: * -> *) a. MonadPlus m => FreshMT m a -> FreshMT m [a]
forall (m :: * -> *) a.
MonadPlus m =>
FreshMT m a -> FreshMT m a -> FreshMT m a
$cempty :: forall (m :: * -> *) a. MonadPlus m => FreshMT m a
empty :: forall a. FreshMT m a
$c<|> :: forall (m :: * -> *) a.
MonadPlus m =>
FreshMT m a -> FreshMT m a -> FreshMT m a
<|> :: forall a. FreshMT m a -> FreshMT m a -> FreshMT m a
$csome :: forall (m :: * -> *) a. MonadPlus m => FreshMT m a -> FreshMT m [a]
some :: forall a. FreshMT m a -> FreshMT m [a]
$cmany :: forall (m :: * -> *) a. MonadPlus m => FreshMT m a -> FreshMT m [a]
many :: forall a. FreshMT m a -> FreshMT m [a]
Alternative
    , Applicative (FreshMT m)
Applicative (FreshMT m)
-> (forall a b. FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b)
-> (forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b)
-> (forall a. a -> FreshMT m a)
-> Monad (FreshMT m)
forall a. a -> FreshMT m a
forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b
forall a b. FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b
forall (m :: * -> *). Monad m => Applicative (FreshMT m)
forall (m :: * -> *) a. Monad m => a -> FreshMT m a
forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m b
forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> (a -> FreshMT m b) -> FreshMT 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 (m :: * -> *) a b.
Monad m =>
FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b
>>= :: forall a b. FreshMT m a -> (a -> FreshMT m b) -> FreshMT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
FreshMT m a -> FreshMT m b -> FreshMT m b
>> :: forall a b. FreshMT m a -> FreshMT m b -> FreshMT m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> FreshMT m a
return :: forall a. a -> FreshMT m a
Monad
    , Monad (FreshMT m)
Monad (FreshMT m)
-> (forall a. IO a -> FreshMT m a) -> MonadIO (FreshMT m)
forall a. IO a -> FreshMT m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {m :: * -> *}. MonadIO m => Monad (FreshMT m)
forall (m :: * -> *) a. MonadIO m => IO a -> FreshMT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> FreshMT m a
liftIO :: forall a. IO a -> FreshMT m a
MonadIO
    , Monad (FreshMT m)
Alternative (FreshMT m)
Alternative (FreshMT m)
-> Monad (FreshMT m)
-> (forall a. FreshMT m a)
-> (forall a. FreshMT m a -> FreshMT m a -> FreshMT m a)
-> MonadPlus (FreshMT m)
forall a. FreshMT m a
forall a. FreshMT m a -> FreshMT m a -> FreshMT m a
forall {m :: * -> *}. MonadPlus m => Monad (FreshMT m)
forall (m :: * -> *). MonadPlus m => Alternative (FreshMT m)
forall (m :: * -> *) a. MonadPlus m => FreshMT m a
forall (m :: * -> *) a.
MonadPlus m =>
FreshMT m a -> FreshMT m a -> FreshMT m a
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
$cmzero :: forall (m :: * -> *) a. MonadPlus m => FreshMT m a
mzero :: forall a. FreshMT m a
$cmplus :: forall (m :: * -> *) a.
MonadPlus m =>
FreshMT m a -> FreshMT m a -> FreshMT m a
mplus :: forall a. FreshMT m a -> FreshMT m a -> FreshMT m a
MonadPlus
    , Monad (FreshMT m)
Monad (FreshMT m)
-> (forall a. (a -> FreshMT m a) -> FreshMT m a)
-> MonadFix (FreshMT m)
forall a. (a -> FreshMT m a) -> FreshMT m a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
forall {m :: * -> *}. MonadFix m => Monad (FreshMT m)
forall (m :: * -> *) a.
MonadFix m =>
(a -> FreshMT m a) -> FreshMT m a
$cmfix :: forall (m :: * -> *) a.
MonadFix m =>
(a -> FreshMT m a) -> FreshMT m a
mfix :: forall a. (a -> FreshMT m a) -> FreshMT m a
MonadFix
    , Monad (FreshMT m)
Monad (FreshMT m)
-> (forall e a. Exception e => e -> FreshMT m a)
-> MonadThrow (FreshMT m)
forall e a. Exception e => e -> FreshMT m a
forall (m :: * -> *).
Monad m -> (forall e a. Exception e => e -> m a) -> MonadThrow m
forall {m :: * -> *}. MonadThrow m => Monad (FreshMT m)
forall (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> FreshMT m a
$cthrowM :: forall (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> FreshMT m a
throwM :: forall e a. Exception e => e -> FreshMT m a
MonadThrow
    , MonadThrow (FreshMT m)
MonadThrow (FreshMT m)
-> (forall e a.
    Exception e =>
    FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a)
-> MonadCatch (FreshMT m)
forall e a.
Exception e =>
FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a
forall {m :: * -> *}. MonadCatch m => MonadThrow (FreshMT m)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a
forall (m :: * -> *).
MonadThrow m
-> (forall e a. Exception e => m a -> (e -> m a) -> m a)
-> MonadCatch m
$ccatch :: forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a
catch :: forall e a.
Exception e =>
FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a
MonadCatch
    , MonadCatch (FreshMT m)
MonadCatch (FreshMT m)
-> (forall b.
    ((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
    -> FreshMT m b)
-> (forall b.
    ((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
    -> FreshMT m b)
-> (forall a b c.
    FreshMT m a
    -> (a -> ExitCase b -> FreshMT m c)
    -> (a -> FreshMT m b)
    -> FreshMT m (b, c))
-> MonadMask (FreshMT m)
forall b.
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
forall a b c.
FreshMT m a
-> (a -> ExitCase b -> FreshMT m c)
-> (a -> FreshMT m b)
-> FreshMT m (b, c)
forall {m :: * -> *}. MonadMask m => MonadCatch (FreshMT m)
forall (m :: * -> *) b.
MonadMask m =>
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
forall (m :: * -> *) a b c.
MonadMask m =>
FreshMT m a
-> (a -> ExitCase b -> FreshMT m c)
-> (a -> FreshMT m b)
-> FreshMT m (b, c)
forall (m :: * -> *).
MonadCatch m
-> (forall b. ((forall a. m a -> m a) -> m b) -> m b)
-> (forall b. ((forall a. m a -> m a) -> m b) -> m b)
-> (forall a b c.
    m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c))
-> MonadMask m
$cmask :: forall (m :: * -> *) b.
MonadMask m =>
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
mask :: forall b.
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
$cuninterruptibleMask :: forall (m :: * -> *) b.
MonadMask m =>
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
uninterruptibleMask :: forall b.
((forall a. FreshMT m a -> FreshMT m a) -> FreshMT m b)
-> FreshMT m b
$cgeneralBracket :: forall (m :: * -> *) a b c.
MonadMask m =>
FreshMT m a
-> (a -> ExitCase b -> FreshMT m c)
-> (a -> FreshMT m b)
-> FreshMT m (b, c)
generalBracket :: forall a b c.
FreshMT m a
-> (a -> ExitCase b -> FreshMT m c)
-> (a -> FreshMT m b)
-> FreshMT m (b, c)
MonadMask
    )

#if MIN_VERSION_base(4,9,0)
deriving instance Fail.MonadFail m => Fail.MonadFail (FreshMT m)
#endif

-- | Run a 'FreshMT' computation (with the global index starting at zero).
runFreshMT :: Monad m => FreshMT m a -> m a
runFreshMT :: forall (m :: * -> *) a. Monad m => FreshMT m a -> m a
runFreshMT FreshMT m a
m = FreshMT m a -> Integer -> m a
forall (m :: * -> *) a. Monad m => FreshMT m a -> Integer -> m a
contFreshMT FreshMT m a
m Integer
0

-- | Run a 'FreshMT' computation given a starting index for fresh name
--   generation.
contFreshMT :: Monad m => FreshMT m a -> Integer -> m a
contFreshMT :: forall (m :: * -> *) a. Monad m => FreshMT m a -> Integer -> m a
contFreshMT (FreshMT StateT Integer m a
m) = StateT Integer m a -> Integer -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
St.evalStateT StateT Integer m a
m

instance MonadTrans FreshMT where
  lift :: forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
lift = StateT Integer m a -> FreshMT m a
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m a -> FreshMT m a)
-> (m a -> StateT Integer m a) -> m a -> FreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT Integer m a
forall (m :: * -> *) a. Monad m => m a -> StateT Integer m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance CC.MonadCont m => CC.MonadCont (FreshMT m) where
  callCC :: forall a b. ((a -> FreshMT m b) -> FreshMT m a) -> FreshMT m a
callCC (a -> FreshMT m b) -> FreshMT m a
c = StateT Integer m a -> FreshMT m a
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m a -> FreshMT m a)
-> StateT Integer m a -> FreshMT m a
forall a b. (a -> b) -> a -> b
$ ((a -> StateT Integer m b) -> StateT Integer m a)
-> StateT Integer m a
forall a b.
((a -> StateT Integer m b) -> StateT Integer m a)
-> StateT Integer m a
forall (m :: * -> *) a b. MonadCont m => ((a -> m b) -> m a) -> m a
CC.callCC (FreshMT m a -> StateT Integer m a
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT (FreshMT m a -> StateT Integer m a)
-> ((a -> StateT Integer m b) -> FreshMT m a)
-> (a -> StateT Integer m b)
-> StateT Integer m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\a -> StateT Integer m b
k -> (a -> FreshMT m b) -> FreshMT m a
c (StateT Integer m b -> FreshMT m b
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m b -> FreshMT m b)
-> (a -> StateT Integer m b) -> a -> FreshMT m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT Integer m b
k)))

instance EC.MonadError e m => EC.MonadError e (FreshMT m) where
  throwError :: forall a. e -> FreshMT m a
throwError = m a -> FreshMT m a
forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> FreshMT m a) -> (e -> m a) -> e -> FreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall a. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
EC.throwError
  catchError :: forall a. FreshMT m a -> (e -> FreshMT m a) -> FreshMT m a
catchError FreshMT m a
m e -> FreshMT m a
h = StateT Integer m a -> FreshMT m a
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m a -> FreshMT m a)
-> StateT Integer m a -> FreshMT m a
forall a b. (a -> b) -> a -> b
$ StateT Integer m a
-> (e -> StateT Integer m a) -> StateT Integer m a
forall a.
StateT Integer m a
-> (e -> StateT Integer m a) -> StateT Integer m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
EC.catchError (FreshMT m a -> StateT Integer m a
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT FreshMT m a
m) (FreshMT m a -> StateT Integer m a
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT (FreshMT m a -> StateT Integer m a)
-> (e -> FreshMT m a) -> e -> StateT Integer m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> FreshMT m a
h)

instance StC.MonadState s m => StC.MonadState s (FreshMT m) where
  get :: FreshMT m s
get = m s -> FreshMT m s
forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: * -> *). MonadState s m => m s
StC.get
  put :: s -> FreshMT m ()
put = m () -> FreshMT m ()
forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> FreshMT m ()) -> (s -> m ()) -> s -> FreshMT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
StC.put

instance RC.MonadReader r m => RC.MonadReader r (FreshMT m) where
  ask :: FreshMT m r
ask   = m r -> FreshMT m r
forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
RC.ask
  local :: forall a. (r -> r) -> FreshMT m a -> FreshMT m a
local r -> r
f = StateT Integer m a -> FreshMT m a
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m a -> FreshMT m a)
-> (FreshMT m a -> StateT Integer m a)
-> FreshMT m a
-> FreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> r) -> StateT Integer m a -> StateT Integer m a
forall a. (r -> r) -> StateT Integer m a -> StateT Integer m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
RC.local r -> r
f (StateT Integer m a -> StateT Integer m a)
-> (FreshMT m a -> StateT Integer m a)
-> FreshMT m a
-> StateT Integer m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshMT m a -> StateT Integer m a
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT

instance WC.MonadWriter w m => WC.MonadWriter w (FreshMT m) where
  tell :: w -> FreshMT m ()
tell   = m () -> FreshMT m ()
forall (m :: * -> *) a. Monad m => m a -> FreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> FreshMT m ()) -> (w -> m ()) -> w -> FreshMT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
WC.tell
  listen :: forall a. FreshMT m a -> FreshMT m (a, w)
listen = StateT Integer m (a, w) -> FreshMT m (a, w)
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m (a, w) -> FreshMT m (a, w))
-> (FreshMT m a -> StateT Integer m (a, w))
-> FreshMT m a
-> FreshMT m (a, w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT Integer m a -> StateT Integer m (a, w)
forall a. StateT Integer m a -> StateT Integer m (a, w)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
WC.listen (StateT Integer m a -> StateT Integer m (a, w))
-> (FreshMT m a -> StateT Integer m a)
-> FreshMT m a
-> StateT Integer m (a, w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshMT m a -> StateT Integer m a
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT
  pass :: forall a. FreshMT m (a, w -> w) -> FreshMT m a
pass   = StateT Integer m a -> FreshMT m a
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m a -> FreshMT m a)
-> (FreshMT m (a, w -> w) -> StateT Integer m a)
-> FreshMT m (a, w -> w)
-> FreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT Integer m (a, w -> w) -> StateT Integer m a
forall a. StateT Integer m (a, w -> w) -> StateT Integer m a
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
WC.pass (StateT Integer m (a, w -> w) -> StateT Integer m a)
-> (FreshMT m (a, w -> w) -> StateT Integer m (a, w -> w))
-> FreshMT m (a, w -> w)
-> StateT Integer m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshMT m (a, w -> w) -> StateT Integer m (a, w -> w)
forall (m :: * -> *) a. FreshMT m a -> StateT Integer m a
unFreshMT


instance Monad m => Fresh (FreshMT m) where
  fresh :: forall a. Name a -> FreshMT m (Name a)
fresh (Fn String
s Integer
_) = StateT Integer m (Name a) -> FreshMT m (Name a)
forall (m :: * -> *) a. StateT Integer m a -> FreshMT m a
FreshMT (StateT Integer m (Name a) -> FreshMT m (Name a))
-> StateT Integer m (Name a) -> FreshMT m (Name a)
forall a b. (a -> b) -> a -> b
$ do
    Integer
n <- StateT Integer m Integer
forall s (m :: * -> *). MonadState s m => m s
St.get
    Integer -> StateT Integer m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
St.put (Integer -> StateT Integer m ()) -> Integer -> StateT Integer m ()
forall a b. (a -> b) -> a -> b
$! Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    Name a -> StateT Integer m (Name a)
forall a. a -> StateT Integer m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name a -> StateT Integer m (Name a))
-> Name a -> StateT Integer m (Name a)
forall a b. (a -> b) -> a -> b
$ (String -> Integer -> Name a
forall a. String -> Integer -> Name a
Fn String
s Integer
n)
  fresh nm :: Name a
nm@(Bn {}) = Name a -> FreshMT m (Name a)
forall a. a -> FreshMT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Name a
nm

#if !MIN_VERSION_transformers(0,6,0)
instance (Error e, Fresh m) => Fresh (ErrorT e m) where
  fresh :: forall a. Name a -> ErrorT e m (Name a)
fresh = m (Name a) -> ErrorT e m (Name a)
forall (m :: * -> *) a. Monad m => m a -> ErrorT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> ErrorT e m (Name a))
-> (Name a -> m (Name a)) -> Name a -> ErrorT e m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh
#endif

instance Fresh m => Fresh (ExceptT e m) where
  fresh :: forall a. Name a -> ExceptT e m (Name a)
fresh = m (Name a) -> ExceptT e m (Name a)
forall (m :: * -> *) a. Monad m => m a -> ExceptT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> ExceptT e m (Name a))
-> (Name a -> m (Name a)) -> Name a -> ExceptT e m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance Fresh m => Fresh (MaybeT m) where
  fresh :: forall a. Name a -> MaybeT m (Name a)
fresh = m (Name a) -> MaybeT m (Name a)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> MaybeT m (Name a))
-> (Name a -> m (Name a)) -> Name a -> MaybeT m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance Fresh m => Fresh (ReaderT r m) where
  fresh :: forall a. Name a -> ReaderT r m (Name a)
fresh = m (Name a) -> ReaderT r m (Name a)
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> ReaderT r m (Name a))
-> (Name a -> m (Name a)) -> Name a -> ReaderT r m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance Fresh m => Fresh (Lazy.StateT s m) where
  fresh :: forall a. Name a -> StateT s m (Name a)
fresh = m (Name a) -> StateT s m (Name a)
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 (Name a) -> StateT s m (Name a))
-> (Name a -> m (Name a)) -> Name a -> StateT s m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance Fresh m => Fresh (Strict.StateT s m) where
  fresh :: forall a. Name a -> StateT s m (Name a)
fresh = m (Name a) -> StateT s m (Name a)
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 (Name a) -> StateT s m (Name a))
-> (Name a -> m (Name a)) -> Name a -> StateT s m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance (Monoid w, Fresh m) => Fresh (Lazy.WriterT w m) where
  fresh :: forall a. Name a -> WriterT w m (Name a)
fresh = m (Name a) -> WriterT w m (Name a)
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> WriterT w m (Name a))
-> (Name a -> m (Name a)) -> Name a -> WriterT w m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

instance (Monoid w, Fresh m) => Fresh (Strict.WriterT w m) where
  fresh :: forall a. Name a -> WriterT w m (Name a)
fresh = m (Name a) -> WriterT w m (Name a)
forall (m :: * -> *) a. Monad m => m a -> WriterT w m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> WriterT w m (Name a))
-> (Name a -> m (Name a)) -> Name a -> WriterT w m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh

------------------------------------------------------------
-- FreshM monad

-- | A convenient monad which is an instance of 'Fresh'.  It keeps
--   track of a global index used for generating fresh names, which is
--   incremented every time 'fresh' is called.
type FreshM = FreshMT Identity

-- | Run a FreshM computation (with the global index starting at zero).
runFreshM :: FreshM a -> a
runFreshM :: forall a. FreshM a -> a
runFreshM = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (FreshM a -> Identity a) -> FreshM a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshM a -> Identity a
forall (m :: * -> *) a. Monad m => FreshMT m a -> m a
runFreshMT

-- | Run a FreshM computation given a starting index.
contFreshM :: FreshM a -> Integer -> a
contFreshM :: forall a. FreshM a -> Integer -> a
contFreshM FreshM a
m = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (Integer -> Identity a) -> Integer -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshM a -> Integer -> Identity a
forall (m :: * -> *) a. Monad m => FreshMT m a -> Integer -> m a
contFreshMT FreshM a
m