{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.LFresh
-- Copyright  : (c) 2011, Stephanie Weirich
-- License    : BSD3 (See LFresh.hs)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Local freshness monad.
{-
Copyright (c)2011, Stephanie Weirich

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

    * Redistributions of source code must retain the above copyright
      notice, this list of conditions and the following disclaimer.

    * Redistributions in binary form must reproduce the above
      copyright notice, this list of conditions and the following
      disclaimer in the documentation and/or other materials provided
      with the distribution.

    * Neither the name of Stephanie Weirich nor the names of other
      contributors may be used to endorse or promote products derived
      from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-}
-- we expect deprecation warnings about Control.Monad.Trans.Error
{-# OPTIONS_GHC -Wwarn #-}
{-# LANGUAGE CPP
             , GeneralizedNewtypeDeriving
             , FlexibleInstances
             , MultiParamTypeClasses
             , StandaloneDeriving
             , UndecidableInstances #-}
module Unbound.Generics.LocallyNameless.LFresh
       (
         -- * The 'LFresh' class

         LFresh(..),

         LFreshM, runLFreshM, contLFreshM,
         LFreshMT(..), runLFreshMT, contLFreshMT

       ) where

import Data.Set (Set)
import qualified Data.Set as S

import Data.Monoid
import Data.Typeable (Typeable)

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.Reader
import Control.Monad.Identity
import Control.Applicative (Applicative, Alternative)

import Control.Monad.Trans.Cont
#if !MIN_VERSION_transformers(0,6,0)
import Control.Monad.Trans.Error
#endif
import Control.Monad.Trans.Except
import Control.Monad.Trans.Identity
#if !MIN_VERSION_transformers(0,6,0)
import Control.Monad.Trans.List
#endif
import Control.Monad.Trans.Maybe
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 Unbound.Generics.LocallyNameless.Name

-- | This is the class of monads that support freshness in an
--   (implicit) local scope.  Generated names are fresh for the current
--   local scope, not necessarily globally fresh.
class Monad m => LFresh m where
  -- | Pick a new name that is fresh for the current (implicit) scope.
  lfresh  :: Typeable a => Name a -> m (Name a)
  -- | Avoid the given names when freshening in the subcomputation,
  --   that is, add the given names to the in-scope set.
  avoid   :: [AnyName] -> m a -> m a
  -- | Get the set of names currently being avoided.
  getAvoids :: m (Set AnyName)

-- | The LFresh monad transformer.  Keeps track of a set of names to
-- avoid, and when asked for a fresh one will choose the first numeric
-- prefix of the given name which is currently unused.
newtype LFreshMT m a = LFreshMT { forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT :: ReaderT (Set AnyName) m a }
  deriving
    ( (forall a b. (a -> b) -> LFreshMT m a -> LFreshMT m b)
-> (forall a b. a -> LFreshMT m b -> LFreshMT m a)
-> Functor (LFreshMT m)
forall a b. a -> LFreshMT m b -> LFreshMT m a
forall a b. (a -> b) -> LFreshMT m a -> LFreshMT m b
forall (m :: * -> *) a b.
Functor m =>
a -> LFreshMT m b -> LFreshMT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> LFreshMT m a -> LFreshMT 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) -> LFreshMT m a -> LFreshMT m b
fmap :: forall a b. (a -> b) -> LFreshMT m a -> LFreshMT m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> LFreshMT m b -> LFreshMT m a
<$ :: forall a b. a -> LFreshMT m b -> LFreshMT m a
Functor
    , Functor (LFreshMT m)
Functor (LFreshMT m)
-> (forall a. a -> LFreshMT m a)
-> (forall a b.
    LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b)
-> (forall a b c.
    (a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c)
-> (forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b)
-> (forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m a)
-> Applicative (LFreshMT m)
forall a. a -> LFreshMT m a
forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m a
forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b
forall a b. LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b
forall a b c.
(a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT 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
forall {m :: * -> *}. Applicative m => Functor (LFreshMT m)
forall (m :: * -> *) a. Applicative m => a -> LFreshMT m a
forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m a
forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m b
forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c
$cpure :: forall (m :: * -> *) a. Applicative m => a -> LFreshMT m a
pure :: forall a. a -> LFreshMT m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b
<*> :: forall a b. LFreshMT m (a -> b) -> LFreshMT m a -> LFreshMT m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c
liftA2 :: forall a b c.
(a -> b -> c) -> LFreshMT m a -> LFreshMT m b -> LFreshMT m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m b
*> :: forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m a
<* :: forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m a
Applicative
    , Applicative (LFreshMT m)
Applicative (LFreshMT m)
-> (forall a. LFreshMT m a)
-> (forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT m a)
-> (forall a. LFreshMT m a -> LFreshMT m [a])
-> (forall a. LFreshMT m a -> LFreshMT m [a])
-> Alternative (LFreshMT m)
forall a. LFreshMT m a
forall a. LFreshMT m a -> LFreshMT m [a]
forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT 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 :: * -> *}. Alternative m => Applicative (LFreshMT m)
forall (m :: * -> *) a. Alternative m => LFreshMT m a
forall (m :: * -> *) a.
Alternative m =>
LFreshMT m a -> LFreshMT m [a]
forall (m :: * -> *) a.
Alternative m =>
LFreshMT m a -> LFreshMT m a -> LFreshMT m a
$cempty :: forall (m :: * -> *) a. Alternative m => LFreshMT m a
empty :: forall a. LFreshMT m a
$c<|> :: forall (m :: * -> *) a.
Alternative m =>
LFreshMT m a -> LFreshMT m a -> LFreshMT m a
<|> :: forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT m a
$csome :: forall (m :: * -> *) a.
Alternative m =>
LFreshMT m a -> LFreshMT m [a]
some :: forall a. LFreshMT m a -> LFreshMT m [a]
$cmany :: forall (m :: * -> *) a.
Alternative m =>
LFreshMT m a -> LFreshMT m [a]
many :: forall a. LFreshMT m a -> LFreshMT m [a]
Alternative
    , Applicative (LFreshMT m)
Applicative (LFreshMT m)
-> (forall a b.
    LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b)
-> (forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b)
-> (forall a. a -> LFreshMT m a)
-> Monad (LFreshMT m)
forall a. a -> LFreshMT m a
forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b
forall a b. LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b
forall {m :: * -> *}. Monad m => Applicative (LFreshMT m)
forall (m :: * -> *) a. Monad m => a -> LFreshMT m a
forall (m :: * -> *) a b.
Monad m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m b
forall (m :: * -> *) a b.
Monad m =>
LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT 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 =>
LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b
>>= :: forall a b. LFreshMT m a -> (a -> LFreshMT m b) -> LFreshMT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
LFreshMT m a -> LFreshMT m b -> LFreshMT m b
>> :: forall a b. LFreshMT m a -> LFreshMT m b -> LFreshMT m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> LFreshMT m a
return :: forall a. a -> LFreshMT m a
Monad
    , Monad (LFreshMT m)
Monad (LFreshMT m)
-> (forall a. IO a -> LFreshMT m a) -> MonadIO (LFreshMT m)
forall a. IO a -> LFreshMT m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {m :: * -> *}. MonadIO m => Monad (LFreshMT m)
forall (m :: * -> *) a. MonadIO m => IO a -> LFreshMT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> LFreshMT m a
liftIO :: forall a. IO a -> LFreshMT m a
MonadIO
    , Monad (LFreshMT m)
Alternative (LFreshMT m)
Alternative (LFreshMT m)
-> Monad (LFreshMT m)
-> (forall a. LFreshMT m a)
-> (forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT m a)
-> MonadPlus (LFreshMT m)
forall a. LFreshMT m a
forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT m a
forall {m :: * -> *}. MonadPlus m => Monad (LFreshMT m)
forall {m :: * -> *}. MonadPlus m => Alternative (LFreshMT m)
forall (m :: * -> *) a. MonadPlus m => LFreshMT m a
forall (m :: * -> *) a.
MonadPlus m =>
LFreshMT m a -> LFreshMT m a -> LFreshMT 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 => LFreshMT m a
mzero :: forall a. LFreshMT m a
$cmplus :: forall (m :: * -> *) a.
MonadPlus m =>
LFreshMT m a -> LFreshMT m a -> LFreshMT m a
mplus :: forall a. LFreshMT m a -> LFreshMT m a -> LFreshMT m a
MonadPlus
    , Monad (LFreshMT m)
Monad (LFreshMT m)
-> (forall a. (a -> LFreshMT m a) -> LFreshMT m a)
-> MonadFix (LFreshMT m)
forall a. (a -> LFreshMT m a) -> LFreshMT m a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
forall {m :: * -> *}. MonadFix m => Monad (LFreshMT m)
forall (m :: * -> *) a.
MonadFix m =>
(a -> LFreshMT m a) -> LFreshMT m a
$cmfix :: forall (m :: * -> *) a.
MonadFix m =>
(a -> LFreshMT m a) -> LFreshMT m a
mfix :: forall a. (a -> LFreshMT m a) -> LFreshMT m a
MonadFix
    , Monad (LFreshMT m)
Monad (LFreshMT m)
-> (forall e a. Exception e => e -> LFreshMT m a)
-> MonadThrow (LFreshMT m)
forall e a. Exception e => e -> LFreshMT m a
forall (m :: * -> *).
Monad m -> (forall e a. Exception e => e -> m a) -> MonadThrow m
forall {m :: * -> *}. MonadThrow m => Monad (LFreshMT m)
forall (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> LFreshMT m a
$cthrowM :: forall (m :: * -> *) e a.
(MonadThrow m, Exception e) =>
e -> LFreshMT m a
throwM :: forall e a. Exception e => e -> LFreshMT m a
MonadThrow
    , MonadThrow (LFreshMT m)
MonadThrow (LFreshMT m)
-> (forall e a.
    Exception e =>
    LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a)
-> MonadCatch (LFreshMT m)
forall e a.
Exception e =>
LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a
forall {m :: * -> *}. MonadCatch m => MonadThrow (LFreshMT m)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT 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) =>
LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a
catch :: forall e a.
Exception e =>
LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a
MonadCatch
    , MonadCatch (LFreshMT m)
MonadCatch (LFreshMT m)
-> (forall b.
    ((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
    -> LFreshMT m b)
-> (forall b.
    ((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
    -> LFreshMT m b)
-> (forall a b c.
    LFreshMT m a
    -> (a -> ExitCase b -> LFreshMT m c)
    -> (a -> LFreshMT m b)
    -> LFreshMT m (b, c))
-> MonadMask (LFreshMT m)
forall b.
((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
forall a b c.
LFreshMT m a
-> (a -> ExitCase b -> LFreshMT m c)
-> (a -> LFreshMT m b)
-> LFreshMT m (b, c)
forall {m :: * -> *}. MonadMask m => MonadCatch (LFreshMT m)
forall (m :: * -> *) b.
MonadMask m =>
((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
forall (m :: * -> *) a b c.
MonadMask m =>
LFreshMT m a
-> (a -> ExitCase b -> LFreshMT m c)
-> (a -> LFreshMT m b)
-> LFreshMT 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. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
mask :: forall b.
((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
$cuninterruptibleMask :: forall (m :: * -> *) b.
MonadMask m =>
((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
uninterruptibleMask :: forall b.
((forall a. LFreshMT m a -> LFreshMT m a) -> LFreshMT m b)
-> LFreshMT m b
$cgeneralBracket :: forall (m :: * -> *) a b c.
MonadMask m =>
LFreshMT m a
-> (a -> ExitCase b -> LFreshMT m c)
-> (a -> LFreshMT m b)
-> LFreshMT m (b, c)
generalBracket :: forall a b c.
LFreshMT m a
-> (a -> ExitCase b -> LFreshMT m c)
-> (a -> LFreshMT m b)
-> LFreshMT m (b, c)
MonadMask
    )

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

-- | Run an 'LFreshMT' computation in an empty context.
runLFreshMT :: LFreshMT m a -> m a
runLFreshMT :: forall (m :: * -> *) a. LFreshMT m a -> m a
runLFreshMT LFreshMT m a
m = LFreshMT m a -> Set AnyName -> m a
forall (m :: * -> *) a. LFreshMT m a -> Set AnyName -> m a
contLFreshMT LFreshMT m a
m Set AnyName
forall a. Set a
S.empty

-- | Run an 'LFreshMT' computation given a set of names to avoid.
contLFreshMT :: LFreshMT m a -> Set AnyName -> m a
contLFreshMT :: forall (m :: * -> *) a. LFreshMT m a -> Set AnyName -> m a
contLFreshMT (LFreshMT ReaderT (Set AnyName) m a
m) = ReaderT (Set AnyName) m a -> Set AnyName -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (Set AnyName) m a
m

instance Monad m => LFresh (LFreshMT m) where
  lfresh :: forall a. Typeable a => Name a -> LFreshMT m (Name a)
lfresh Name a
nm = ReaderT (Set AnyName) m (Name a) -> LFreshMT m (Name a)
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m (Name a) -> LFreshMT m (Name a))
-> ReaderT (Set AnyName) m (Name a) -> LFreshMT m (Name a)
forall a b. (a -> b) -> a -> b
$ do
    let s :: String
s = Name a -> String
forall a. Name a -> String
name2String Name a
nm
    Set AnyName
used <- ReaderT (Set AnyName) m (Set AnyName)
forall r (m :: * -> *). MonadReader r m => m r
ask
    Name a -> ReaderT (Set AnyName) m (Name a)
forall a. a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name a -> ReaderT (Set AnyName) m (Name a))
-> Name a -> ReaderT (Set AnyName) m (Name a)
forall a b. (a -> b) -> a -> b
$ [Name a] -> Name a
forall a. HasCallStack => [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 :: forall a. [AnyName] -> LFreshMT m a -> LFreshMT m a
avoid [AnyName]
names = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> LFreshMT m a
-> LFreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set AnyName -> Set AnyName)
-> ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m a
forall a.
(Set AnyName -> Set AnyName)
-> ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m 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)) (ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m a)
-> (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> LFreshMT m a
-> ReaderT (Set AnyName) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT

  getAvoids :: LFreshMT m (Set AnyName)
getAvoids = ReaderT (Set AnyName) m (Set AnyName) -> LFreshMT m (Set AnyName)
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT ReaderT (Set AnyName) m (Set AnyName)
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | A convenient monad which is an instance of 'LFresh'.  It keeps
--   track of a set of names to avoid, and when asked for a fresh one
--   will choose the first unused numerical name.
type LFreshM = LFreshMT Identity

-- | Run a LFreshM computation in an empty context.
runLFreshM :: LFreshM a -> a
runLFreshM :: forall a. LFreshM a -> a
runLFreshM = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (LFreshM a -> Identity a) -> LFreshM a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshM a -> Identity a
forall (m :: * -> *) a. LFreshMT m a -> m a
runLFreshMT

-- | Run a LFreshM computation given a set of names to avoid.
contLFreshM :: LFreshM a -> Set AnyName -> a
contLFreshM :: forall a. LFreshM a -> Set AnyName -> a
contLFreshM LFreshM a
m = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a)
-> (Set AnyName -> Identity a) -> Set AnyName -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshM a -> Set AnyName -> Identity a
forall (m :: * -> *) a. LFreshMT m a -> Set AnyName -> m a
contLFreshMT LFreshM a
m

instance LFresh m => LFresh (ContT r m) where
  lfresh :: forall a. Typeable a => Name a -> ContT r m (Name a)
lfresh = m (Name a) -> ContT r m (Name a)
forall (m :: * -> *) a. Monad m => m a -> ContT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> ContT r m (Name a))
-> (Name a -> m (Name a)) -> Name a -> ContT r m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> ContT r m a -> ContT r m a
avoid  = (m r -> m r) -> ContT r m a -> ContT r m a
forall {k} (m :: k -> *) (r :: k) a.
(m r -> m r) -> ContT r m a -> ContT r m a
mapContT ((m r -> m r) -> ContT r m a -> ContT r m a)
-> ([AnyName] -> m r -> m r)
-> [AnyName]
-> ContT r m a
-> ContT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m r -> m r
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: ContT r m (Set AnyName)
getAvoids = m (Set AnyName) -> ContT r m (Set AnyName)
forall (m :: * -> *) a. Monad m => m a -> ContT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

#if !MIN_VERSION_transformers(0,6,0)
instance (Error e, LFresh m) => LFresh (ErrorT e m) where
  lfresh :: forall a. Typeable a => Name a -> ErrorT e m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> ErrorT e m a -> ErrorT e m a
avoid  = (m (Either e a) -> m (Either e a)) -> ErrorT e m a -> ErrorT e m a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ErrorT e m a -> ErrorT e' n b
mapErrorT ((m (Either e a) -> m (Either e a))
 -> ErrorT e m a -> ErrorT e m a)
-> ([AnyName] -> m (Either e a) -> m (Either e a))
-> [AnyName]
-> ErrorT e m a
-> ErrorT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (Either e a) -> m (Either e a)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: ErrorT e m (Set AnyName)
getAvoids = m (Set AnyName) -> ErrorT e m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids
#endif

instance LFresh m => LFresh (ExceptT e m) where
  lfresh :: forall a. Typeable a => Name a -> ExceptT e m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> ExceptT e m a -> ExceptT e m a
avoid = (m (Either e a) -> m (Either e a))
-> ExceptT e m a -> ExceptT e m a
forall (m :: * -> *) e a (n :: * -> *) e' b.
(m (Either e a) -> n (Either e' b))
-> ExceptT e m a -> ExceptT e' n b
mapExceptT ((m (Either e a) -> m (Either e a))
 -> ExceptT e m a -> ExceptT e m a)
-> ([AnyName] -> m (Either e a) -> m (Either e a))
-> [AnyName]
-> ExceptT e m a
-> ExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (Either e a) -> m (Either e a)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: ExceptT e m (Set AnyName)
getAvoids = m (Set AnyName) -> ExceptT e m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance LFresh m => LFresh (IdentityT m) where
  lfresh :: forall a. Typeable a => Name a -> IdentityT m (Name a)
lfresh = m (Name a) -> IdentityT m (Name a)
forall (m :: * -> *) a. Monad m => m a -> IdentityT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> IdentityT m (Name a))
-> (Name a -> m (Name a)) -> Name a -> IdentityT m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> IdentityT m a -> IdentityT m a
avoid  = (m a -> m a) -> IdentityT m a -> IdentityT m a
forall {k1} {k2} (m :: k1 -> *) (a :: k1) (n :: k2 -> *) (b :: k2).
(m a -> n b) -> IdentityT m a -> IdentityT n b
mapIdentityT ((m a -> m a) -> IdentityT m a -> IdentityT m a)
-> ([AnyName] -> m a -> m a)
-> [AnyName]
-> IdentityT m a
-> IdentityT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m a -> m a
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: IdentityT m (Set AnyName)
getAvoids = m (Set AnyName) -> IdentityT m (Set AnyName)
forall (m :: * -> *) a. Monad m => m a -> IdentityT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

#if !MIN_VERSION_transformers(0,6,0)
instance LFresh m => LFresh (ListT m) where
  lfresh :: forall a. Typeable a => Name a -> ListT m (Name a)
lfresh = m (Name a) -> ListT m (Name a)
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Name a) -> ListT m (Name a))
-> (Name a -> m (Name a)) -> Name a -> ListT m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> ListT m a -> ListT m a
avoid  = (m [a] -> m [a]) -> ListT m a -> ListT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m [a] -> n [b]) -> ListT m a -> ListT n b
mapListT ((m [a] -> m [a]) -> ListT m a -> ListT m a)
-> ([AnyName] -> m [a] -> m [a])
-> [AnyName]
-> ListT m a
-> ListT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m [a] -> m [a]
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: ListT m (Set AnyName)
getAvoids = m (Set AnyName) -> ListT m (Set AnyName)
forall (m :: * -> *) a. Monad m => m a -> ListT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids
#endif

instance LFresh m => LFresh (MaybeT m) where
  lfresh :: forall a. Typeable a => Name a -> MaybeT m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> MaybeT m a -> MaybeT m a
avoid  = (m (Maybe a) -> m (Maybe a)) -> MaybeT m a -> MaybeT m a
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b
mapMaybeT ((m (Maybe a) -> m (Maybe a)) -> MaybeT m a -> MaybeT m a)
-> ([AnyName] -> m (Maybe a) -> m (Maybe a))
-> [AnyName]
-> MaybeT m a
-> MaybeT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (Maybe a) -> m (Maybe a)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: MaybeT m (Set AnyName)
getAvoids = m (Set AnyName) -> MaybeT m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance LFresh m => LFresh (ReaderT r m) where
  lfresh :: forall a. Typeable a => Name a -> ReaderT r m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> ReaderT r m a -> ReaderT r m a
avoid  = (m a -> m a) -> ReaderT r m a -> ReaderT r m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((m a -> m a) -> ReaderT r m a -> ReaderT r m a)
-> ([AnyName] -> m a -> m a)
-> [AnyName]
-> ReaderT r m a
-> ReaderT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m a -> m a
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: ReaderT r m (Set AnyName)
getAvoids = m (Set AnyName) -> ReaderT r m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance LFresh m => LFresh (Lazy.StateT s m) where
  lfresh :: forall a. Typeable a => Name a -> StateT s m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> StateT s m a -> StateT s m a
avoid  = (m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
Lazy.mapStateT ((m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a)
-> ([AnyName] -> m (a, s) -> m (a, s))
-> [AnyName]
-> StateT s m a
-> StateT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (a, s) -> m (a, s)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: StateT s m (Set AnyName)
getAvoids = m (Set AnyName) -> StateT s m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance LFresh m => LFresh (Strict.StateT s m) where
  lfresh :: forall a. Typeable a => Name a -> StateT s m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> StateT s m a -> StateT s m a
avoid  = (m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
Strict.mapStateT ((m (a, s) -> m (a, s)) -> StateT s m a -> StateT s m a)
-> ([AnyName] -> m (a, s) -> m (a, s))
-> [AnyName]
-> StateT s m a
-> StateT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (a, s) -> m (a, s)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: StateT s m (Set AnyName)
getAvoids = m (Set AnyName) -> StateT s m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance (Monoid w, LFresh m) => LFresh (Lazy.WriterT w m) where
  lfresh :: forall a. Typeable a => Name a -> WriterT w m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> WriterT w m a -> WriterT w m a
avoid  = (m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a
forall (m :: * -> *) a w (n :: * -> *) b w'.
(m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
Lazy.mapWriterT ((m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a)
-> ([AnyName] -> m (a, w) -> m (a, w))
-> [AnyName]
-> WriterT w m a
-> WriterT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (a, w) -> m (a, w)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: WriterT w m (Set AnyName)
getAvoids = m (Set AnyName) -> WriterT w m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

instance (Monoid w, LFresh m) => LFresh (Strict.WriterT w m) where
  lfresh :: forall a. Typeable a => Name a -> WriterT w m (Name a)
lfresh = 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. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh
  avoid :: forall a. [AnyName] -> WriterT w m a -> WriterT w m a
avoid  = (m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a
forall (m :: * -> *) a w (n :: * -> *) b w'.
(m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
Strict.mapWriterT ((m (a, w) -> m (a, w)) -> WriterT w m a -> WriterT w m a)
-> ([AnyName] -> m (a, w) -> m (a, w))
-> [AnyName]
-> WriterT w m a
-> WriterT w m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AnyName] -> m (a, w) -> m (a, w)
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid
  getAvoids :: WriterT w m (Set AnyName)
getAvoids = m (Set AnyName) -> WriterT w m (Set AnyName)
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 (Set AnyName)
forall (m :: * -> *). LFresh m => m (Set AnyName)
getAvoids

-- Instances for applying LFreshMT to other monads

instance MonadTrans LFreshMT where
  lift :: forall (m :: * -> *) a. Monad m => m a -> LFreshMT m a
lift = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> (m a -> ReaderT (Set AnyName) m a) -> m a -> LFreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. Monad m => m a -> ReaderT (Set AnyName) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance CC.MonadCont m => CC.MonadCont (LFreshMT m) where
  callCC :: forall a b. ((a -> LFreshMT m b) -> LFreshMT m a) -> LFreshMT m a
callCC (a -> LFreshMT m b) -> LFreshMT m a
c = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> ReaderT (Set AnyName) m a -> LFreshMT m a
forall a b. (a -> b) -> a -> b
$ ((a -> ReaderT (Set AnyName) m b) -> ReaderT (Set AnyName) m a)
-> ReaderT (Set AnyName) m a
forall a b.
((a -> ReaderT (Set AnyName) m b) -> ReaderT (Set AnyName) m a)
-> ReaderT (Set AnyName) m a
forall (m :: * -> *) a b. MonadCont m => ((a -> m b) -> m a) -> m a
CC.callCC (LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> ((a -> ReaderT (Set AnyName) m b) -> LFreshMT m a)
-> (a -> ReaderT (Set AnyName) m b)
-> ReaderT (Set AnyName) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\a -> ReaderT (Set AnyName) m b
k -> (a -> LFreshMT m b) -> LFreshMT m a
c (ReaderT (Set AnyName) m b -> LFreshMT m b
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m b -> LFreshMT m b)
-> (a -> ReaderT (Set AnyName) m b) -> a -> LFreshMT m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReaderT (Set AnyName) m b
k)))

instance EC.MonadError e m => EC.MonadError e (LFreshMT m) where
  throwError :: forall a. e -> LFreshMT m a
throwError = m a -> LFreshMT m a
forall (m :: * -> *) a. Monad m => m a -> LFreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> LFreshMT m a) -> (e -> m a) -> e -> LFreshMT 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. LFreshMT m a -> (e -> LFreshMT m a) -> LFreshMT m a
catchError LFreshMT m a
m e -> LFreshMT m a
h = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> ReaderT (Set AnyName) m a -> LFreshMT m a
forall a b. (a -> b) -> a -> b
$ ReaderT (Set AnyName) m a
-> (e -> ReaderT (Set AnyName) m a) -> ReaderT (Set AnyName) m a
forall a.
ReaderT (Set AnyName) m a
-> (e -> ReaderT (Set AnyName) m a) -> ReaderT (Set AnyName) m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
EC.catchError (LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT LFreshMT m a
m) (LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> (e -> LFreshMT m a) -> e -> ReaderT (Set AnyName) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> LFreshMT m a
h)

instance StC.MonadState s m => StC.MonadState s (LFreshMT m) where
  get :: LFreshMT m s
get = m s -> LFreshMT m s
forall (m :: * -> *) a. Monad m => m a -> LFreshMT 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 -> LFreshMT m ()
put = m () -> LFreshMT m ()
forall (m :: * -> *) a. Monad m => m a -> LFreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> LFreshMT m ()) -> (s -> m ()) -> s -> LFreshMT 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 (LFreshMT m) where
  ask :: LFreshMT m r
ask   = m r -> LFreshMT m r
forall (m :: * -> *) a. Monad m => m a -> LFreshMT 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) -> LFreshMT m a -> LFreshMT m a
local r -> r
f = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> LFreshMT m a
-> LFreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m a -> m a)
-> ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((r -> r) -> m a -> m a
forall a. (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
RC.local r -> r
f) (ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m a)
-> (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> LFreshMT m a
-> ReaderT (Set AnyName) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT

instance WC.MonadWriter w m => WC.MonadWriter w (LFreshMT m) where
  tell :: w -> LFreshMT m ()
tell   = m () -> LFreshMT m ()
forall (m :: * -> *) a. Monad m => m a -> LFreshMT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> LFreshMT m ()) -> (w -> m ()) -> w -> LFreshMT 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. LFreshMT m a -> LFreshMT m (a, w)
listen = ReaderT (Set AnyName) m (a, w) -> LFreshMT m (a, w)
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m (a, w) -> LFreshMT m (a, w))
-> (LFreshMT m a -> ReaderT (Set AnyName) m (a, w))
-> LFreshMT m a
-> LFreshMT m (a, w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m (a, w)
forall a.
ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m (a, w)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
WC.listen (ReaderT (Set AnyName) m a -> ReaderT (Set AnyName) m (a, w))
-> (LFreshMT m a -> ReaderT (Set AnyName) m a)
-> LFreshMT m a
-> ReaderT (Set AnyName) m (a, w)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshMT m a -> ReaderT (Set AnyName) m a
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT
  pass :: forall a. LFreshMT m (a, w -> w) -> LFreshMT m a
pass   = ReaderT (Set AnyName) m a -> LFreshMT m a
forall (m :: * -> *) a. ReaderT (Set AnyName) m a -> LFreshMT m a
LFreshMT (ReaderT (Set AnyName) m a -> LFreshMT m a)
-> (LFreshMT m (a, w -> w) -> ReaderT (Set AnyName) m a)
-> LFreshMT m (a, w -> w)
-> LFreshMT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT (Set AnyName) m (a, w -> w) -> ReaderT (Set AnyName) m a
forall a.
ReaderT (Set AnyName) m (a, w -> w) -> ReaderT (Set AnyName) m a
forall w (m :: * -> *) a. MonadWriter w m => m (a, w -> w) -> m a
WC.pass (ReaderT (Set AnyName) m (a, w -> w) -> ReaderT (Set AnyName) m a)
-> (LFreshMT m (a, w -> w) -> ReaderT (Set AnyName) m (a, w -> w))
-> LFreshMT m (a, w -> w)
-> ReaderT (Set AnyName) m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LFreshMT m (a, w -> w) -> ReaderT (Set AnyName) m (a, w -> w)
forall (m :: * -> *) a. LFreshMT m a -> ReaderT (Set AnyName) m a
unLFreshMT