{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
module Disco.Effects.LFresh where
import Data.Set (Set)
import qualified Data.Set as S
import Data.Typeable (Typeable)
import Polysemy
import Polysemy.ConstraintAbsorber
import Polysemy.Reader
import qualified Unbound.Generics.LocallyNameless as U
import Unbound.Generics.LocallyNameless.Name
data LFresh m a where
Lfresh :: Typeable a => Name a -> LFresh m (Name a)
Avoid :: [AnyName] -> m a -> LFresh m a
GetAvoids :: LFresh m (Set AnyName)
makeSem ''LFresh
runLFresh :: Sem (LFresh ': r) a -> Sem r a
runLFresh :: Sem (LFresh : r) a -> Sem r a
runLFresh = Set AnyName -> Sem (Reader (Set AnyName) : r) a -> Sem r a
forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader Set AnyName
forall a. Set a
S.empty (Sem (Reader (Set AnyName) : r) a -> Sem r a)
-> (Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a)
-> Sem (LFresh : r) a
-> Sem r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a
forall (r :: [(* -> *) -> * -> *]) a.
Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a
runLFresh'
runLFresh' :: Sem (LFresh ': r) a -> Sem (Reader (Set AnyName) ': r) a
runLFresh' :: Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a
runLFresh'
= (forall (rInitial :: [(* -> *) -> * -> *]) x.
LFresh (Sem rInitial) x
-> Tactical LFresh (Sem rInitial) (Reader (Set AnyName) : r) x)
-> Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a
forall (e1 :: (* -> *) -> * -> *) (e2 :: (* -> *) -> * -> *)
(r :: [(* -> *) -> * -> *]) a.
(forall (rInitial :: [(* -> *) -> * -> *]) x.
e1 (Sem rInitial) x -> Tactical e1 (Sem rInitial) (e2 : r) x)
-> Sem (e1 : r) a -> Sem (e2 : r) a
reinterpretH @_ @(Reader (Set AnyName)) \case
Lfresh nm -> do
let s :: String
s = Name a -> String
forall a. Name a -> String
name2String Name a
nm
Set AnyName
used <- Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(Set AnyName)
forall i (r :: [(* -> *) -> * -> *]).
Member (Reader i) r =>
Sem r i
ask
Name a
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f (Name a))
forall (f :: * -> *) a (e :: (* -> *) -> * -> *) (m :: * -> *)
(r :: [(* -> *) -> * -> *]).
Functor f =>
a -> Sem (WithTactics e f m r) (f a)
pureT (Name a
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f (Name a)))
-> Name a
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f (Name a))
forall a b. (a -> b) -> a -> b
$ [Name a] -> Name a
forall a. [a] -> a
head ((Name a -> Bool) -> [Name a] -> [Name a]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Name a
x -> Bool -> Bool
not (AnyName -> Set AnyName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
x) Set AnyName
used))
((Integer -> Name a) -> [Integer] -> [Name a]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Integer -> Name a
forall a. String -> Integer -> Name a
makeName String
s) [Integer
0..]))
Avoid names m -> do
Sem (LFresh : Reader (Set AnyName) : r) (f x)
m' <- Sem rInitial x
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(Sem (LFresh : Reader (Set AnyName) : r) (f x))
forall (m :: * -> *) a (e :: (* -> *) -> * -> *) (f :: * -> *)
(r :: [(* -> *) -> * -> *]).
m a -> Sem (WithTactics e f m r) (Sem (e : r) (f a))
runT Sem rInitial x
m
Sem (Reader (Set AnyName) : r) (f x)
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f x)
forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *]) a.
Sem r a -> Sem (e : r) a
raise (Sem (Reader (Set AnyName) : Reader (Set AnyName) : r) (f x)
-> Sem (Reader (Set AnyName) : r) (f x)
forall (e :: (* -> *) -> * -> *) (r :: [(* -> *) -> * -> *]) a.
Member e r =>
Sem (e : r) a -> Sem r a
subsume (Sem (LFresh : Reader (Set AnyName) : r) (f x)
-> Sem (Reader (Set AnyName) : Reader (Set AnyName) : r) (f x)
forall (r :: [(* -> *) -> * -> *]) a.
Sem (LFresh : r) a -> Sem (Reader (Set AnyName) : r) a
runLFresh' ((Set AnyName -> Set AnyName)
-> Sem (LFresh : Reader (Set AnyName) : r) (f x)
-> Sem (LFresh : Reader (Set AnyName) : r) (f x)
forall i (r :: [(* -> *) -> * -> *]) a.
Member (Reader i) r =>
(i -> i) -> Sem r a -> Sem r a
local (Set AnyName -> Set AnyName -> Set AnyName
forall a. Ord a => Set a -> Set a -> Set a
S.union ([AnyName] -> Set AnyName
forall a. Ord a => [a] -> Set a
S.fromList [AnyName]
names)) Sem (LFresh : Reader (Set AnyName) : r) (f x)
m')))
LFresh (Sem rInitial) x
GetAvoids -> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r)) x
forall i (r :: [(* -> *) -> * -> *]).
Member (Reader i) r =>
Sem r i
ask Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r)) x
-> (x
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f x))
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f x)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x
-> Sem
(WithTactics LFresh f (Sem rInitial) (Reader (Set AnyName) : r))
(f x)
forall (f :: * -> *) a (e :: (* -> *) -> * -> *) (m :: * -> *)
(r :: [(* -> *) -> * -> *]).
Functor f =>
a -> Sem (WithTactics e f m r) (f a)
pureT
lunbind
:: (Member LFresh r, U.Alpha p, U.Alpha t)
=> U.Bind p t -> ((p,t) -> Sem r c) -> Sem r c
lunbind :: Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind p t
b (p, t) -> Sem r c
k = (LFresh (Sem r) => Sem r c) -> Sem r c
forall (r :: [(* -> *) -> * -> *]) a.
Member LFresh r =>
(LFresh (Sem r) => Sem r a) -> Sem r a
absorbLFresh (Bind p t -> ((p, t) -> Sem r c) -> Sem r c
forall (m :: * -> *) p t c.
(LFresh m, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> m c) -> m c
U.lunbind Bind p t
b (p, t) -> Sem r c
k)
absorbLFresh :: Member LFresh r => (U.LFresh (Sem r) => Sem r a) -> Sem r a
absorbLFresh :: (LFresh (Sem r) => Sem r a) -> Sem r a
absorbLFresh = LFreshDict (Sem r)
-> (forall s.
Reifies s (LFreshDict (Sem r)) :- LFresh (Action (Sem r) s))
-> (LFresh (Sem r) => Sem r a)
-> Sem r a
forall (p :: (* -> *) -> Constraint) (x :: (* -> *) -> * -> * -> *)
d (r :: [(* -> *) -> * -> *]) a.
d
-> (forall s. Reifies s d :- p (x (Sem r) s))
-> (p (Sem r) => Sem r a)
-> Sem r a
absorbWithSem @U.LFresh @Action ((forall a. Typeable a => Name a -> Sem r (Name a))
-> (forall a. [AnyName] -> Sem r a -> Sem r a)
-> Sem r (Set AnyName)
-> LFreshDict (Sem r)
forall (m :: * -> *).
(forall a. Typeable a => Name a -> m (Name a))
-> (forall a. [AnyName] -> m a -> m a)
-> m (Set AnyName)
-> LFreshDict m
LFreshDict forall (r :: [(* -> *) -> * -> *]) a.
(Member LFresh r, Typeable a) =>
Name a -> Sem r (Name a)
forall a. Typeable a => Name a -> Sem r (Name a)
lfresh forall (r :: [(* -> *) -> * -> *]) a.
Member LFresh r =>
[AnyName] -> Sem r a -> Sem r a
forall a. [AnyName] -> Sem r a -> Sem r a
avoid Sem r (Set AnyName)
forall (r :: [(* -> *) -> * -> *]).
Member LFresh r =>
Sem r (Set AnyName)
getAvoids) ((Reifies s (LFreshDict (Sem r)) =>
Dict (LFresh (Action (Sem r) s)))
-> Reifies s (LFreshDict (Sem r)) :- LFresh (Action (Sem r) s)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Reifies s (LFreshDict (Sem r)) => Dict (LFresh (Action (Sem r) s))
forall (a :: Constraint). a => Dict a
Dict)
{-# INLINEABLE absorbLFresh #-}
data LFreshDict m = LFreshDict
{ LFreshDict m -> forall a. Typeable a => Name a -> m (Name a)
lfresh_ :: forall a. Typeable a => Name a -> m (Name a)
, LFreshDict m -> forall a. [AnyName] -> m a -> m a
avoid_ :: forall a. [AnyName] -> m a -> m a
, LFreshDict m -> m (Set AnyName)
getAvoids_ :: m (Set AnyName)
}
newtype Action m s' a = Action (m a)
deriving (a -> Action m s' b -> Action m s' a
(a -> b) -> Action m s' a -> Action m s' b
(forall a b. (a -> b) -> Action m s' a -> Action m s' b)
-> (forall a b. a -> Action m s' b -> Action m s' a)
-> Functor (Action m s')
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
<$ :: 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 :: (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, Functor (Action m s')
a -> Action m s' a
Functor (Action m s')
-> (forall a. a -> Action m s' a)
-> (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 a b. Action m s' a -> Action m s' b -> Action m s' b)
-> (forall a b. Action m s' a -> Action m s' b -> Action m s' a)
-> Applicative (Action m s')
Action m s' a -> Action m s' b -> Action m s' b
Action m s' a -> Action m s' b -> Action m s' a
Action m s' (a -> b) -> Action m s' a -> Action m s' b
(a -> b -> c) -> Action m s' a -> Action m s' b -> Action m s' c
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
<* :: 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
*> :: 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 :: (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
<*> :: 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 :: a -> Action m s' a
$cpure :: forall (m :: * -> *) k (s' :: k) a.
Applicative m =>
a -> Action m s' a
$cp1Applicative :: forall (m :: * -> *) k (s' :: k).
Applicative m =>
Functor (Action m s')
Applicative, Applicative (Action m s')
a -> Action m s' a
Applicative (Action m s')
-> (forall a b.
Action m s' a -> (a -> Action m s' b) -> Action m s' b)
-> (forall a b. Action m s' a -> Action m s' b -> Action m s' b)
-> (forall a. a -> Action m s' a)
-> Monad (Action m s')
Action m s' a -> (a -> Action m s' b) -> Action m s' b
Action m s' a -> Action m s' b -> Action m s' b
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 :: a -> Action m s' a
$creturn :: forall (m :: * -> *) k (s' :: k) a. Monad m => a -> Action m s' a
>> :: 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
>>= :: 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
$cp1Monad :: forall (m :: * -> *) k (s' :: k).
Monad m =>
Applicative (Action m s')
Monad)
instance ( Monad m
, Reifies s' (LFreshDict m)
) => U.LFresh (Action m s') where
lfresh :: Name a -> Action m s' (Name a)
lfresh Name a
x = m (Name a) -> Action m s' (Name a)
forall k k (m :: k -> *) (s' :: k) (a :: k). m a -> Action m s' a
Action (m (Name a) -> Action m s' (Name a))
-> m (Name a) -> Action m s' (Name a)
forall a b. (a -> b) -> a -> b
$ LFreshDict m -> Name a -> m (Name a)
forall (m :: * -> *).
LFreshDict m -> forall a. Typeable a => Name a -> m (Name a)
lfresh_ (Proxy s' -> LFreshDict m
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s' -> LFreshDict m) -> Proxy s' -> LFreshDict m
forall a b. (a -> b) -> a -> b
$ Proxy s'
forall k (t :: k). Proxy t
Proxy @s') Name a
x
{-# INLINEABLE lfresh #-}
avoid :: [AnyName] -> Action m s' a -> Action m s' a
avoid [AnyName]
xs (Action m a
m) = m a -> Action m s' a
forall k k (m :: k -> *) (s' :: k) (a :: k). m a -> Action m s' a
Action (m a -> Action m s' a) -> m a -> Action m s' a
forall a b. (a -> b) -> a -> b
$ LFreshDict m -> [AnyName] -> m a -> m a
forall (m :: * -> *).
LFreshDict m -> forall a. [AnyName] -> m a -> m a
avoid_ (Proxy s' -> LFreshDict m
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s' -> LFreshDict m) -> Proxy s' -> LFreshDict m
forall a b. (a -> b) -> a -> b
$ Proxy s'
forall k (t :: k). Proxy t
Proxy @s') [AnyName]
xs m a
m
{-# INLINEABLE avoid #-}
getAvoids :: Action m s' (Set AnyName)
getAvoids = m (Set AnyName) -> Action m s' (Set AnyName)
forall k k (m :: k -> *) (s' :: k) (a :: k). m a -> Action m s' a
Action (m (Set AnyName) -> Action m s' (Set AnyName))
-> m (Set AnyName) -> Action m s' (Set AnyName)
forall a b. (a -> b) -> a -> b
$ LFreshDict m -> m (Set AnyName)
forall (m :: * -> *). LFreshDict m -> m (Set AnyName)
getAvoids_ (Proxy s' -> LFreshDict m
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s' -> LFreshDict m) -> Proxy s' -> LFreshDict m
forall a b. (a -> b) -> a -> b
$ Proxy s'
forall k (t :: k). Proxy t
Proxy @s')
{-# INLINEABLE getAvoids #-}