{-# LANGUAGE FunctionalDependencies,
             GeneralisedNewtypeDeriving,
             DerivingStrategies,
             UndecidableInstances #-}
module Parsley.Internal.Common.Fresh (
    VFreshT, HFreshT, VFresh, HFresh,
    runFreshT, runFresh,
    evalFreshT, evalFresh,
    execFreshT, execFresh,
    MonadFresh(..), construct, mapVFreshT,
    RunFreshT
  ) where

import Control.Applicative        (liftA2)
import Control.Monad.Fix          (MonadFix(..))
import Control.Monad.Identity     (Identity, runIdentity)
import Control.Monad.Reader.Class (MonadReader(..))
import Control.Monad.State.Class  (MonadState(..))
import Control.Monad.Trans        (MonadTrans(..), MonadIO(..))

-- Fresh operations
class Monad m => MonadFresh x m | m -> x where
  newVar :: m x
  newScope :: m a -> m a

construct :: MonadFresh x m => (x -> a) -> m a
construct :: forall x (m :: Type -> Type) a. MonadFresh x m => (x -> a) -> m a
construct x -> a
f = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> a
f forall x (m :: Type -> Type). MonadFresh x m => m x
newVar

mapVFreshT :: (m (a, x, x) -> n (b, x, x)) -> VFreshT x m a -> VFreshT x n b
mapVFreshT :: forall (m :: Type -> Type) a x (n :: Type -> Type) b.
(m (a, x, x) -> n (b, x, x)) -> VFreshT x m a -> VFreshT x n b
mapVFreshT m (a, x, x) -> n (b, x, x)
f VFreshT x m a
m = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT (\x
cur x
max -> m (a, x, x) -> n (b, x, x)
f (forall x (m :: Type -> Type) a.
VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT VFreshT x m a
m x
cur x
max))

class (Monad n, Monad m) => RunFreshT x n m | m -> x, m -> n where
  runFreshT :: m a -> x -> n (a, x)

evalFreshT :: RunFreshT x n m => m a -> x -> n a
evalFreshT :: forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n a
evalFreshT m a
m x
init = forall a b. (a, b) -> a
fst forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n (a, x)
runFreshT m a
m x
init

execFreshT :: RunFreshT x n m => m a -> x -> n x
execFreshT :: forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n x
execFreshT m a
m x
init = forall a b. (a, b) -> b
snd forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n (a, x)
runFreshT m a
m x
init

-- Fresh type
type HFresh x = HFreshT x Identity
type VFresh x = VFreshT x Identity
-- TODO Nominals
newtype VFreshT x m a = VFreshT (FreshT x m a) deriving newtype (forall a b. a -> VFreshT x m b -> VFreshT x m a
forall a b. (a -> b) -> VFreshT x m a -> VFreshT x m b
forall x (m :: Type -> Type) a b.
Functor m =>
a -> VFreshT x m b -> VFreshT x m a
forall x (m :: Type -> Type) a b.
Functor m =>
(a -> b) -> VFreshT x m a -> VFreshT x m b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> VFreshT x m b -> VFreshT x m a
$c<$ :: forall x (m :: Type -> Type) a b.
Functor m =>
a -> VFreshT x m b -> VFreshT x m a
fmap :: forall a b. (a -> b) -> VFreshT x m a -> VFreshT x m b
$cfmap :: forall x (m :: Type -> Type) a b.
Functor m =>
(a -> b) -> VFreshT x m a -> VFreshT x m b
Functor, forall a. a -> VFreshT x m a
forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m a
forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b
forall a b. VFreshT x m (a -> b) -> VFreshT x m a -> VFreshT x m b
forall a b c.
(a -> b -> c) -> VFreshT x m a -> VFreshT x m b -> VFreshT x m c
forall {x} {m :: Type -> Type}. Monad m => Functor (VFreshT x m)
forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m (a -> b) -> VFreshT x m a -> VFreshT x m b
forall x (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> c) -> VFreshT x m a -> VFreshT x m b -> VFreshT x m c
forall (f :: Type -> Type).
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
<* :: forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m a
$c<* :: forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m a
*> :: forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b
$c*> :: forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
liftA2 :: forall a b c.
(a -> b -> c) -> VFreshT x m a -> VFreshT x m b -> VFreshT x m c
$cliftA2 :: forall x (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> c) -> VFreshT x m a -> VFreshT x m b -> VFreshT x m c
<*> :: forall a b. VFreshT x m (a -> b) -> VFreshT x m a -> VFreshT x m b
$c<*> :: forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m (a -> b) -> VFreshT x m a -> VFreshT x m b
pure :: forall a. a -> VFreshT x m a
$cpure :: forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
Applicative, forall a. a -> VFreshT x m a
forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b
forall a b. VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b
forall x (m :: Type -> Type). Monad m => Applicative (VFreshT x m)
forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b
forall (m :: Type -> Type).
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 :: forall a. a -> VFreshT x m a
$creturn :: forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
>> :: forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b
$c>> :: forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
>>= :: forall a b. VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b
$c>>= :: forall x (m :: Type -> Type) a b.
Monad m =>
VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b
Monad, forall a. (a -> VFreshT x m a) -> VFreshT x m a
forall {x} {m :: Type -> Type}. MonadFix m => Monad (VFreshT x m)
forall x (m :: Type -> Type) a.
MonadFix m =>
(a -> VFreshT x m a) -> VFreshT x m a
forall (m :: Type -> Type).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
mfix :: forall a. (a -> VFreshT x m a) -> VFreshT x m a
$cmfix :: forall x (m :: Type -> Type) a.
MonadFix m =>
(a -> VFreshT x m a) -> VFreshT x m a
MonadFix, forall x (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a
forall (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a
forall (t :: (Type -> Type) -> Type -> Type).
(forall (m :: Type -> Type) a. Monad m => m a -> t m a)
-> MonadTrans t
lift :: forall (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a
$clift :: forall x (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a
MonadTrans, forall a. IO a -> VFreshT x m a
forall {x} {m :: Type -> Type}. MonadIO m => Monad (VFreshT x m)
forall x (m :: Type -> Type) a. MonadIO m => IO a -> VFreshT x m a
forall (m :: Type -> Type).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> VFreshT x m a
$cliftIO :: forall x (m :: Type -> Type) a. MonadIO m => IO a -> VFreshT x m a
MonadIO, MonadReader r, MonadState s, RunFreshT x m)
newtype HFreshT x m a = HFreshT (FreshT x m a) deriving newtype (forall a b. a -> HFreshT x m b -> HFreshT x m a
forall a b. (a -> b) -> HFreshT x m a -> HFreshT x m b
forall x (m :: Type -> Type) a b.
Functor m =>
a -> HFreshT x m b -> HFreshT x m a
forall x (m :: Type -> Type) a b.
Functor m =>
(a -> b) -> HFreshT x m a -> HFreshT x m b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> HFreshT x m b -> HFreshT x m a
$c<$ :: forall x (m :: Type -> Type) a b.
Functor m =>
a -> HFreshT x m b -> HFreshT x m a
fmap :: forall a b. (a -> b) -> HFreshT x m a -> HFreshT x m b
$cfmap :: forall x (m :: Type -> Type) a b.
Functor m =>
(a -> b) -> HFreshT x m a -> HFreshT x m b
Functor, forall a. a -> HFreshT x m a
forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m a
forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b
forall a b. HFreshT x m (a -> b) -> HFreshT x m a -> HFreshT x m b
forall a b c.
(a -> b -> c) -> HFreshT x m a -> HFreshT x m b -> HFreshT x m c
forall {x} {m :: Type -> Type}. Monad m => Functor (HFreshT x m)
forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m (a -> b) -> HFreshT x m a -> HFreshT x m b
forall x (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> c) -> HFreshT x m a -> HFreshT x m b -> HFreshT x m c
forall (f :: Type -> Type).
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
<* :: forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m a
$c<* :: forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m a
*> :: forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b
$c*> :: forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
liftA2 :: forall a b c.
(a -> b -> c) -> HFreshT x m a -> HFreshT x m b -> HFreshT x m c
$cliftA2 :: forall x (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> c) -> HFreshT x m a -> HFreshT x m b -> HFreshT x m c
<*> :: forall a b. HFreshT x m (a -> b) -> HFreshT x m a -> HFreshT x m b
$c<*> :: forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m (a -> b) -> HFreshT x m a -> HFreshT x m b
pure :: forall a. a -> HFreshT x m a
$cpure :: forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
Applicative, forall a. a -> HFreshT x m a
forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b
forall a b. HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b
forall x (m :: Type -> Type). Monad m => Applicative (HFreshT x m)
forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b
forall (m :: Type -> Type).
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 :: forall a. a -> HFreshT x m a
$creturn :: forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
>> :: forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b
$c>> :: forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
>>= :: forall a b. HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b
$c>>= :: forall x (m :: Type -> Type) a b.
Monad m =>
HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b
Monad, forall a. (a -> HFreshT x m a) -> HFreshT x m a
forall {x} {m :: Type -> Type}. MonadFix m => Monad (HFreshT x m)
forall x (m :: Type -> Type) a.
MonadFix m =>
(a -> HFreshT x m a) -> HFreshT x m a
forall (m :: Type -> Type).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
mfix :: forall a. (a -> HFreshT x m a) -> HFreshT x m a
$cmfix :: forall x (m :: Type -> Type) a.
MonadFix m =>
(a -> HFreshT x m a) -> HFreshT x m a
MonadFix, forall x (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a
forall (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a
forall (t :: (Type -> Type) -> Type -> Type).
(forall (m :: Type -> Type) a. Monad m => m a -> t m a)
-> MonadTrans t
lift :: forall (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a
$clift :: forall x (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a
MonadTrans, forall a. IO a -> HFreshT x m a
forall {x} {m :: Type -> Type}. MonadIO m => Monad (HFreshT x m)
forall x (m :: Type -> Type) a. MonadIO m => IO a -> HFreshT x m a
forall (m :: Type -> Type).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> HFreshT x m a
$cliftIO :: forall x (m :: Type -> Type) a. MonadIO m => IO a -> HFreshT x m a
MonadIO, MonadReader r, MonadState s, RunFreshT x m)
newtype FreshT x m a = FreshT {forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT :: x -> x -> m (a, x, x)}

instance Monad n => RunFreshT x n (FreshT x n) where
  runFreshT :: forall a. FreshT x n a -> x -> n (a, x)
runFreshT FreshT x n a
k x
init =
    do (a
x, x
_, x
max) <- forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT FreshT x n a
k x
init x
init
       forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x, x
max)

runFresh :: RunFreshT x Identity m => m a -> x -> (a, x)
runFresh :: forall x (m :: Type -> Type) a.
RunFreshT x Identity m =>
m a -> x -> (a, x)
runFresh m a
mx = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n (a, x)
runFreshT m a
mx

evalFresh :: RunFreshT x Identity m => m a -> x -> a
evalFresh :: forall x (m :: Type -> Type) a.
RunFreshT x Identity m =>
m a -> x -> a
evalFresh m a
mx = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n a
evalFreshT m a
mx

execFresh :: RunFreshT x Identity m => m a -> x -> x
execFresh :: forall x (m :: Type -> Type) a.
RunFreshT x Identity m =>
m a -> x -> x
execFresh m a
mx = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (n :: Type -> Type) (m :: Type -> Type) a.
RunFreshT x n m =>
m a -> x -> n x
execFreshT m a
mx

vFreshT :: (x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT :: forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT = forall x (m :: Type -> Type) a. FreshT x m a -> VFreshT x m a
VFreshT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT

unVFreshT :: VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT :: forall x (m :: Type -> Type) a.
VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT (VFreshT FreshT x m a
f) = forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT FreshT x m a
f

hFreshT :: (x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT :: forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT = forall x (m :: Type -> Type) a. FreshT x m a -> HFreshT x m a
HFreshT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT

unHFreshT :: HFreshT x m a -> x -> x -> m (a, x, x)
unHFreshT :: forall x (m :: Type -> Type) a.
HFreshT x m a -> x -> x -> m (a, x, x)
unHFreshT (HFreshT FreshT x m a
f) = forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT FreshT x m a
f

instance Functor f => Functor (FreshT x f) where
  {-# INLINE fmap #-}
  fmap :: forall a b. (a -> b) -> FreshT x f a -> FreshT x f b
fmap a -> b
f (FreshT x -> x -> f (a, x, x)
k) = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
x, x
cur', x
max') -> (a -> b
f a
x, x
cur', x
max')) (x -> x -> f (a, x, x)
k x
cur x
max))

instance Monad m => Applicative (FreshT x m) where
  {-# INLINE pure #-}
  pure :: forall a. a -> FreshT x m a
pure a
x = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a
x, x
cur, x
max))
  {-# INLINE liftA2 #-}
  liftA2 :: forall a b c.
(a -> b -> c) -> FreshT x m a -> FreshT x m b -> FreshT x m c
liftA2 a -> b -> c
f (FreshT x -> x -> m (a, x, x)
mx) (FreshT x -> x -> m (b, x, x)
my) = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max ->
    do (a
x, x
cur', x
max') <- x -> x -> m (a, x, x)
mx x
cur x
max
       (b
y, x
cur'', x
max'') <- x -> x -> m (b, x, x)
my x
cur' x
max'
       forall (m :: Type -> Type) a. Monad m => a -> m a
return (a -> b -> c
f a
x b
y, x
cur'', x
max''))

instance Monad m => Monad (FreshT x m) where
  {-# INLINE return #-}
  return :: forall a. a -> FreshT x m a
return = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  {-# INLINE (>>=) #-}
  (FreshT x -> x -> m (a, x, x)
mx) >>= :: forall a b. FreshT x m a -> (a -> FreshT x m b) -> FreshT x m b
>>= a -> FreshT x m b
f = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max ->
    do (a
x, x
cur', x
max') <- x -> x -> m (a, x, x)
mx x
cur x
max
       forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT (a -> FreshT x m b
f a
x) x
cur' x
max')

instance MonadFix m => MonadFix (FreshT x m) where
  {-# INLINE mfix #-}
  mfix :: forall a. (a -> FreshT x m a) -> FreshT x m a
mfix a -> FreshT x m a
f = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix (\ ~(a
x, x
_, x
_) -> forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT (a -> FreshT x m a
f a
x) x
cur x
max))

instance MonadTrans (FreshT x) where
  {-# INLINE lift #-}
  lift :: forall (m :: Type -> Type) a. Monad m => m a -> FreshT x m a
lift m a
m = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max ->
    do a
x <- m a
m
       forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x, x
cur, x
max))

instance (Monad m, Ord x, Enum x) => MonadFresh x (VFreshT x m) where
  newVar :: VFreshT x m x
newVar = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT (\x
cur x
m -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (x
cur, x
cur, forall a. Ord a => a -> a -> a
max x
m x
cur))
  newScope :: forall a. VFreshT x m a -> VFreshT x m a
newScope VFreshT x m a
scoped = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT (\x
cur x
max ->
    do (a
x, x
_, x
max') <- forall x (m :: Type -> Type) a.
VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT VFreshT x m a
scoped (forall a. Enum a => a -> a
succ x
cur) x
max
       forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x, x
cur, x
max'))

instance (Monad m, Ord x, Enum x) => MonadFresh x (HFreshT x m) where
  newVar :: HFreshT x m x
newVar = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT (\x
cur x
m -> forall (m :: Type -> Type) a. Monad m => a -> m a
return (x
cur, forall a. Enum a => a -> a
succ x
cur, forall a. Ord a => a -> a -> a
max x
m x
cur))
  newScope :: forall a. HFreshT x m a -> HFreshT x m a
newScope HFreshT x m a
scoped = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT (\x
cur x
max ->
    do (a
x, x
_, x
max') <- forall x (m :: Type -> Type) a.
HFreshT x m a -> x -> x -> m (a, x, x)
unHFreshT HFreshT x m a
scoped x
cur x
max
       forall (m :: Type -> Type) a. Monad m => a -> m a
return (a
x, x
cur, x
max'))

instance MonadIO m => MonadIO (FreshT x m) where liftIO :: forall a. IO a -> FreshT x m a
liftIO = forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO
instance MonadReader r m => MonadReader r (FreshT x m) where
  ask :: FreshT x m r
ask = forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: Type -> Type). MonadReader r m => m r
ask
  local :: forall a. (r -> r) -> FreshT x m a -> FreshT x m a
local r -> r
f FreshT x m a
m = forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
next -> forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local r -> r
f (forall x (m :: Type -> Type) a.
FreshT x m a -> x -> x -> m (a, x, x)
unFreshT FreshT x m a
m x
cur x
next))
instance MonadState s m => MonadState s (FreshT x m) where
  get :: FreshT x m s
get = forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: Type -> Type). MonadState s m => m s
get
  put :: s -> FreshT x m ()
put = forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: Type -> Type). MonadState s m => s -> m ()
put