{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
module Disco.Effects.Fresh where
import Disco.Effects.Counter
import Disco.Names (QName, localName)
import Polysemy
import Polysemy.ConstraintAbsorber
import qualified Unbound.Generics.LocallyNameless as U
import Unbound.Generics.LocallyNameless.Name
data Fresh m a where
Fresh :: Name x -> Fresh m (Name x)
makeSem ''Fresh
runFresh' :: Integer -> Sem (Fresh ': r) a -> Sem r a
runFresh' :: forall (r :: EffectRow) a. Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
i =
forall (r :: EffectRow) a.
Integer -> Sem (Counter : r) a -> Sem r a
runCounter' Integer
i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (e1 :: Effect) (e2 :: Effect) (r :: EffectRow) a.
FirstOrder e1 "reinterpret" =>
(forall (rInitial :: EffectRow) x.
e1 (Sem rInitial) x -> Sem (e2 : r) x)
-> Sem (e1 : r) a -> Sem (e2 : r) a
reinterpret \case
Fresh Name x
x -> case Name x
x of
Fn String
s Integer
_ -> forall a. String -> Integer -> Name a
Fn String
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow). Member Counter r => Sem r Integer
next
nm :: Name x
nm@Bn {} -> forall (m :: * -> *) a. Monad m => a -> m a
return Name x
nm
runFresh :: Sem (Fresh ': r) a -> Sem r a
runFresh :: forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh = forall (r :: EffectRow) a. Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
0
runFresh1 :: Sem (Fresh ': r) a -> Sem r a
runFresh1 :: forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh1 = forall (r :: EffectRow) a. Integer -> Sem (Fresh : r) a -> Sem r a
runFresh' Integer
1
unbind :: (Member Fresh r, U.Alpha p, U.Alpha t) => U.Bind p t -> Sem r (p, t)
unbind :: forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind Bind p t
b = forall (r :: EffectRow) a.
Member Fresh r =>
(Fresh (Sem r) => Sem r a) -> Sem r a
absorbFresh (forall p t (m :: * -> *).
(Alpha p, Alpha t, Fresh m) =>
Bind p t -> m (p, t)
U.unbind Bind p t
b)
freshQ :: (Member Fresh r) => String -> Sem r (QName a)
freshQ :: forall (r :: EffectRow) a.
Member Fresh r =>
String -> Sem r (QName a)
freshQ String
s = forall a. Name a -> QName a
localName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh (forall a. String -> Name a
string2Name String
s)
absorbFresh :: Member Fresh r => (U.Fresh (Sem r) => Sem r a) -> Sem r a
absorbFresh :: forall (r :: EffectRow) a.
Member Fresh r =>
(Fresh (Sem r) => Sem r a) -> Sem r a
absorbFresh = forall (p :: (* -> *) -> Constraint) (x :: (* -> *) -> * -> * -> *)
d (r :: EffectRow) a.
d
-> (forall s. Reifies s d :- p (x (Sem r) s))
-> (p (Sem r) => Sem r a)
-> Sem r a
absorbWithSem @U.Fresh @Action (forall (m :: * -> *).
(forall x. Name x -> m (Name x)) -> FreshDict m
FreshDict forall (r :: EffectRow) x.
Member Fresh r =>
Name x -> Sem r (Name x)
fresh) (forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub forall (a :: Constraint). a => Dict a
Dict)
{-# INLINEABLE absorbFresh #-}
newtype FreshDict m = FreshDict {forall (m :: * -> *). FreshDict m -> forall x. Name x -> m (Name x)
fresh_ :: forall x. Name x -> m (Name x)}
newtype Action m s' a = Action (m a)
deriving (forall a b. a -> Action m s' b -> Action m s' a
forall a b. (a -> b) -> Action m s' a -> Action m s' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) k (s' :: k) a b.
Functor m =>
a -> Action m s' b -> Action m s' a
forall (m :: * -> *) k (s' :: k) a b.
Functor m =>
(a -> b) -> Action m s' a -> Action m s' b
<$ :: forall a b. a -> Action m s' b -> Action m s' a
$c<$ :: forall (m :: * -> *) k (s' :: k) a b.
Functor m =>
a -> Action m s' b -> Action m s' a
fmap :: forall a b. (a -> b) -> Action m s' a -> Action m s' b
$cfmap :: forall (m :: * -> *) k (s' :: k) a b.
Functor m =>
(a -> b) -> Action m s' a -> Action m s' b
Functor, forall a. a -> Action m s' a
forall a b. Action m s' a -> Action m s' b -> Action m s' a
forall a b. Action m s' a -> Action m s' b -> Action m s' b
forall a b. Action m s' (a -> b) -> Action m s' a -> Action m s' b
forall a b c.
(a -> b -> c) -> Action m s' a -> Action m s' b -> Action m s' 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
forall {m :: * -> *} {k} {s' :: k}.
Applicative m =>
Functor (Action m s')
forall (m :: * -> *) k (s' :: k) a.
Applicative m =>
a -> Action m s' a
forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' a -> Action m s' b -> Action m s' a
forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' a -> Action m s' b -> Action m s' b
forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' (a -> b) -> Action m s' a -> Action m s' b
forall (m :: * -> *) k (s' :: k) a b c.
Applicative m =>
(a -> b -> c) -> Action m s' a -> Action m s' b -> Action m s' c
<* :: forall a b. Action m s' a -> Action m s' b -> Action m s' a
$c<* :: forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' a -> Action m s' b -> Action m s' a
*> :: forall a b. Action m s' a -> Action m s' b -> Action m s' b
$c*> :: forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' a -> Action m s' b -> Action m s' b
liftA2 :: forall a b c.
(a -> b -> c) -> Action m s' a -> Action m s' b -> Action m s' c
$cliftA2 :: forall (m :: * -> *) k (s' :: k) a b c.
Applicative m =>
(a -> b -> c) -> Action m s' a -> Action m s' b -> Action m s' c
<*> :: forall a b. Action m s' (a -> b) -> Action m s' a -> Action m s' b
$c<*> :: forall (m :: * -> *) k (s' :: k) a b.
Applicative m =>
Action m s' (a -> b) -> Action m s' a -> Action m s' b
pure :: forall a. a -> Action m s' a
$cpure :: forall (m :: * -> *) k (s' :: k) a.
Applicative m =>
a -> Action m s' a
Applicative, forall a. a -> Action m s' a
forall a b. Action m s' a -> Action m s' b -> Action m s' b
forall a b. Action m s' a -> (a -> Action m s' b) -> Action m s' 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
forall {m :: * -> *} {k} {s' :: k}.
Monad m =>
Applicative (Action m s')
forall (m :: * -> *) k (s' :: k) a. Monad m => a -> Action m s' a
forall (m :: * -> *) k (s' :: k) a b.
Monad m =>
Action m s' a -> Action m s' b -> Action m s' b
forall (m :: * -> *) k (s' :: k) a b.
Monad m =>
Action m s' a -> (a -> Action m s' b) -> Action m s' b
return :: forall a. a -> Action m s' a
$creturn :: forall (m :: * -> *) k (s' :: k) a. Monad m => a -> Action m s' a
>> :: forall a b. Action m s' a -> Action m s' b -> Action m s' b
$c>> :: forall (m :: * -> *) k (s' :: k) a b.
Monad m =>
Action m s' a -> Action m s' b -> Action m s' b
>>= :: forall a b. Action m s' a -> (a -> Action m s' b) -> Action m s' b
$c>>= :: forall (m :: * -> *) k (s' :: k) a b.
Monad m =>
Action m s' a -> (a -> Action m s' b) -> Action m s' b
Monad)
instance
( Monad m
, Reifies s' (FreshDict m)
) =>
U.Fresh (Action m s')
where
fresh :: forall a. Name a -> Action m s' (Name a)
fresh Name a
x = forall {k} {k} (m :: k -> *) (s' :: k) (a :: k).
m a -> Action m s' a
Action forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). FreshDict m -> forall x. Name x -> m (Name x)
fresh_ (forall {k} (s :: k) a (proxy :: k -> *).
Reifies s a =>
proxy s -> a
reflect forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
Proxy @s') Name a
x
{-# INLINEABLE fresh #-}