{-# 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 :: (x -> a) -> m a
construct x -> a
f = (x -> a) -> m x -> m a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap x -> a
f m x
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 :: (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 = (x -> x -> n (b, x, x)) -> VFreshT x n b
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 (VFreshT x m a -> x -> x -> m (a, x, x)
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 :: m a -> x -> n a
evalFreshT m a
m x
init = (a, x) -> a
forall a b. (a, b) -> a
fst ((a, x) -> a) -> n (a, x) -> n a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> x -> n (a, x)
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 :: m a -> x -> n x
execFreshT m a
m x
init = (a, x) -> x
forall a b. (a, b) -> b
snd ((a, x) -> x) -> n (a, x) -> n x
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> x -> n (a, x)
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 (a -> VFreshT x m b -> VFreshT x m a
(a -> b) -> VFreshT x m a -> VFreshT x m b
(forall a b. (a -> b) -> VFreshT x m a -> VFreshT x m b)
-> (forall a b. a -> VFreshT x m b -> VFreshT x m a)
-> Functor (VFreshT x m)
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
<$ :: 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 :: (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, Functor (VFreshT x m)
a -> VFreshT x m a
Functor (VFreshT x m)
-> (forall a. a -> VFreshT x m a)
-> (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 a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b)
-> (forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m a)
-> Applicative (VFreshT x m)
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
VFreshT x m a -> VFreshT x m b -> VFreshT x m a
VFreshT x m (a -> b) -> VFreshT x m a -> VFreshT x m b
(a -> b -> c) -> VFreshT x m a -> VFreshT x m b -> VFreshT x m c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> VFreshT x m a
$cpure :: forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
$cp1Applicative :: forall x (m :: Type -> Type). Monad m => Functor (VFreshT x m)
Applicative, Applicative (VFreshT x m)
a -> VFreshT x m a
Applicative (VFreshT x m)
-> (forall a b.
    VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b)
-> (forall a b. VFreshT x m a -> VFreshT x m b -> VFreshT x m b)
-> (forall a. a -> VFreshT x m a)
-> Monad (VFreshT x m)
VFreshT x m a -> (a -> VFreshT x m b) -> VFreshT x m b
VFreshT x m a -> VFreshT x m b -> VFreshT x m b
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 :: a -> VFreshT x m a
$creturn :: forall x (m :: Type -> Type) a. Monad m => a -> VFreshT x m a
>> :: 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
>>= :: 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
$cp1Monad :: forall x (m :: Type -> Type). Monad m => Applicative (VFreshT x m)
Monad, Monad (VFreshT x m)
Monad (VFreshT x m)
-> (forall a. (a -> VFreshT x m a) -> VFreshT x m a)
-> MonadFix (VFreshT x m)
(a -> VFreshT x m a) -> VFreshT x m a
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 :: (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
$cp1MonadFix :: forall x (m :: Type -> Type). MonadFix m => Monad (VFreshT x m)
MonadFix, m a -> VFreshT x m a
(forall (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a)
-> MonadTrans (VFreshT x)
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 :: m a -> VFreshT x m a
$clift :: forall x (m :: Type -> Type) a. Monad m => m a -> VFreshT x m a
MonadTrans, Monad (VFreshT x m)
Monad (VFreshT x m)
-> (forall a. IO a -> VFreshT x m a) -> MonadIO (VFreshT x m)
IO a -> VFreshT x m a
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 :: IO a -> VFreshT x m a
$cliftIO :: forall x (m :: Type -> Type) a. MonadIO m => IO a -> VFreshT x m a
$cp1MonadIO :: forall x (m :: Type -> Type). MonadIO m => Monad (VFreshT x m)
MonadIO, MonadReader r, MonadState s, RunFreshT x m)
newtype HFreshT x m a = HFreshT (FreshT x m a) deriving newtype (a -> HFreshT x m b -> HFreshT x m a
(a -> b) -> HFreshT x m a -> HFreshT x m b
(forall a b. (a -> b) -> HFreshT x m a -> HFreshT x m b)
-> (forall a b. a -> HFreshT x m b -> HFreshT x m a)
-> Functor (HFreshT x m)
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
<$ :: 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 :: (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, Functor (HFreshT x m)
a -> HFreshT x m a
Functor (HFreshT x m)
-> (forall a. a -> HFreshT x m a)
-> (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 a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b)
-> (forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m a)
-> Applicative (HFreshT x m)
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
HFreshT x m a -> HFreshT x m b -> HFreshT x m a
HFreshT x m (a -> b) -> HFreshT x m a -> HFreshT x m b
(a -> b -> c) -> HFreshT x m a -> HFreshT x m b -> HFreshT x m c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> HFreshT x m a
$cpure :: forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
$cp1Applicative :: forall x (m :: Type -> Type). Monad m => Functor (HFreshT x m)
Applicative, Applicative (HFreshT x m)
a -> HFreshT x m a
Applicative (HFreshT x m)
-> (forall a b.
    HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b)
-> (forall a b. HFreshT x m a -> HFreshT x m b -> HFreshT x m b)
-> (forall a. a -> HFreshT x m a)
-> Monad (HFreshT x m)
HFreshT x m a -> (a -> HFreshT x m b) -> HFreshT x m b
HFreshT x m a -> HFreshT x m b -> HFreshT x m b
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 :: a -> HFreshT x m a
$creturn :: forall x (m :: Type -> Type) a. Monad m => a -> HFreshT x m a
>> :: 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
>>= :: 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
$cp1Monad :: forall x (m :: Type -> Type). Monad m => Applicative (HFreshT x m)
Monad, Monad (HFreshT x m)
Monad (HFreshT x m)
-> (forall a. (a -> HFreshT x m a) -> HFreshT x m a)
-> MonadFix (HFreshT x m)
(a -> HFreshT x m a) -> HFreshT x m a
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 :: (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
$cp1MonadFix :: forall x (m :: Type -> Type). MonadFix m => Monad (HFreshT x m)
MonadFix, m a -> HFreshT x m a
(forall (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a)
-> MonadTrans (HFreshT x)
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 :: m a -> HFreshT x m a
$clift :: forall x (m :: Type -> Type) a. Monad m => m a -> HFreshT x m a
MonadTrans, Monad (HFreshT x m)
Monad (HFreshT x m)
-> (forall a. IO a -> HFreshT x m a) -> MonadIO (HFreshT x m)
IO a -> HFreshT x m a
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 :: IO a -> HFreshT x m a
$cliftIO :: forall x (m :: Type -> Type) a. MonadIO m => IO a -> HFreshT x m a
$cp1MonadIO :: forall x (m :: Type -> Type). MonadIO m => Monad (HFreshT x m)
MonadIO, MonadReader r, MonadState s, RunFreshT x m)
newtype FreshT x m a = FreshT {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 :: FreshT x n a -> x -> n (a, x)
runFreshT FreshT x n a
k x
init =
    do (a
x, x
_, x
max) <- FreshT x n a -> x -> x -> n (a, x, x)
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
       (a, x) -> n (a, x)
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 :: m a -> x -> (a, x)
runFresh m a
mx = Identity (a, x) -> (a, x)
forall a. Identity a -> a
runIdentity (Identity (a, x) -> (a, x))
-> (x -> Identity (a, x)) -> x -> (a, x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> x -> Identity (a, x)
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 :: m a -> x -> a
evalFresh m a
mx = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (x -> Identity a) -> x -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> x -> Identity a
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 :: m a -> x -> x
execFresh m a
mx = Identity x -> x
forall a. Identity a -> a
runIdentity (Identity x -> x) -> (x -> Identity x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> x -> Identity x
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 :: (x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT = FreshT x m a -> VFreshT x m a
forall x (m :: Type -> Type) a. FreshT x m a -> VFreshT x m a
VFreshT (FreshT x m a -> VFreshT x m a)
-> ((x -> x -> m (a, x, x)) -> FreshT x m a)
-> (x -> x -> m (a, x, x))
-> VFreshT x m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> x -> m (a, x, x)) -> FreshT x m a
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 :: VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT (VFreshT FreshT x m a
f) = FreshT x m a -> x -> x -> m (a, x, x)
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 :: (x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT = FreshT x m a -> HFreshT x m a
forall x (m :: Type -> Type) a. FreshT x m a -> HFreshT x m a
HFreshT (FreshT x m a -> HFreshT x m a)
-> ((x -> x -> m (a, x, x)) -> FreshT x m a)
-> (x -> x -> m (a, x, x))
-> HFreshT x m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> x -> m (a, x, x)) -> FreshT x m a
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 :: HFreshT x m a -> x -> x -> m (a, x, x)
unHFreshT (HFreshT FreshT x m a
f) = FreshT x m a -> x -> x -> m (a, x, x)
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 :: (a -> b) -> FreshT x f a -> FreshT x f b
fmap a -> b
f (FreshT x -> x -> f (a, x, x)
k) = (x -> x -> f (b, x, x)) -> FreshT x f b
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> ((a, x, x) -> (b, x, x)) -> f (a, x, x) -> f (b, x, x)
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 :: a -> FreshT x m a
pure a
x = (x -> x -> m (a, x, x)) -> FreshT x m a
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> (a, x, x) -> m (a, x, x)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a
x, x
cur, x
max))
  {-# INLINE liftA2 #-}
  liftA2 :: (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) = (x -> x -> m (c, x, x)) -> FreshT x m c
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'
       (c, x, x) -> m (c, x, x)
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 :: a -> FreshT x m a
return = a -> FreshT x m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure
  {-# INLINE (>>=) #-}
  (FreshT x -> x -> m (a, x, x)
mx) >>= :: FreshT x m a -> (a -> FreshT x m b) -> FreshT x m b
>>= a -> FreshT x m b
f = (x -> x -> m (b, x, x)) -> FreshT x m b
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
       FreshT x m b -> x -> x -> m (b, x, x)
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 :: (a -> FreshT x m a) -> FreshT x m a
mfix a -> FreshT x m a
f = (x -> x -> m (a, x, x)) -> FreshT x m a
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
max -> ((a, x, x) -> m (a, x, x)) -> m (a, x, x)
forall (m :: Type -> Type) a. MonadFix m => (a -> m a) -> m a
mfix (\ ~(a
x, x
_, x
_) -> FreshT x m a -> x -> x -> m (a, 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 :: m a -> FreshT x m a
lift m a
m = (x -> x -> m (a, x, x)) -> FreshT x m a
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
       (a, x, x) -> m (a, x, x)
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 = (x -> x -> m (x, x, x)) -> VFreshT x m x
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> VFreshT x m a
vFreshT (\x
cur x
m -> (x, x, x) -> m (x, x, x)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (x
cur, x
cur, x -> x -> x
forall a. Ord a => a -> a -> a
max x
m x
cur))
  newScope :: VFreshT x m a -> VFreshT x m a
newScope VFreshT x m a
scoped = (x -> x -> m (a, x, x)) -> VFreshT x m a
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') <- VFreshT x m a -> x -> x -> m (a, x, x)
forall x (m :: Type -> Type) a.
VFreshT x m a -> x -> x -> m (a, x, x)
unVFreshT VFreshT x m a
scoped (x -> x
forall a. Enum a => a -> a
succ x
cur) x
max
       (a, x, x) -> m (a, x, x)
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 = (x -> x -> m (x, x, x)) -> HFreshT x m x
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> HFreshT x m a
hFreshT (\x
cur x
m -> (x, x, x) -> m (x, x, x)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (x
cur, x -> x
forall a. Enum a => a -> a
succ x
cur, x -> x -> x
forall a. Ord a => a -> a -> a
max x
m x
cur))
  newScope :: HFreshT x m a -> HFreshT x m a
newScope HFreshT x m a
scoped = (x -> x -> m (a, x, x)) -> HFreshT x m a
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') <- HFreshT x m a -> x -> x -> m (a, x, x)
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
       (a, x, x) -> m (a, x, x)
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 :: IO a -> FreshT x m a
liftIO = m a -> FreshT x m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> FreshT x m a) -> (IO a -> m a) -> IO a -> FreshT x m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
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 = m r -> FreshT x m r
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: Type -> Type). MonadReader r m => m r
ask
  local :: (r -> r) -> FreshT x m a -> FreshT x m a
local r -> r
f FreshT x m a
m = (x -> x -> m (a, x, x)) -> FreshT x m a
forall x (m :: Type -> Type) a.
(x -> x -> m (a, x, x)) -> FreshT x m a
FreshT (\x
cur x
next -> (r -> r) -> m (a, x, x) -> m (a, x, x)
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local r -> r
f (FreshT x m a -> x -> x -> m (a, x, x)
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 = m s -> FreshT x m s
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: Type -> Type). MonadState s m => m s
get
  put :: s -> FreshT x m ()
put = m () -> FreshT x m ()
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> FreshT x m ()) -> (s -> m ()) -> s -> FreshT x m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put