-- | The monad that the renamer runs in and related infrastructure.

{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}

module PlutusCore.Rename.Monad
    ( RenameT (..)
    , ScopedRenameT
    , Renaming (..)
    , TypeRenaming
    , ScopedRenaming (..)
    , HasRenaming (..)
    , scopedRenamingTypes
    , scopedRenamingTerms
    , runRenameT
    , lookupNameM
    , renameNameM
    , withFreshenedName
    , withRenamedName
    ) where

import PlutusPrelude

import PlutusCore.Name
import PlutusCore.Quote

import Control.Lens
import Control.Monad.Reader

-- | The monad the renamer runs in.
newtype RenameT ren m a = RenameT
    { RenameT ren m a -> ReaderT ren m a
unRenameT :: ReaderT ren m a
    } deriving newtype
        ( a -> RenameT ren m b -> RenameT ren m a
(a -> b) -> RenameT ren m a -> RenameT ren m b
(forall a b. (a -> b) -> RenameT ren m a -> RenameT ren m b)
-> (forall a b. a -> RenameT ren m b -> RenameT ren m a)
-> Functor (RenameT ren m)
forall a b. a -> RenameT ren m b -> RenameT ren m a
forall a b. (a -> b) -> RenameT ren m a -> RenameT ren m b
forall ren (m :: * -> *) a b.
Functor m =>
a -> RenameT ren m b -> RenameT ren m a
forall ren (m :: * -> *) a b.
Functor m =>
(a -> b) -> RenameT ren m a -> RenameT ren m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RenameT ren m b -> RenameT ren m a
$c<$ :: forall ren (m :: * -> *) a b.
Functor m =>
a -> RenameT ren m b -> RenameT ren m a
fmap :: (a -> b) -> RenameT ren m a -> RenameT ren m b
$cfmap :: forall ren (m :: * -> *) a b.
Functor m =>
(a -> b) -> RenameT ren m a -> RenameT ren m b
Functor, Functor (RenameT ren m)
a -> RenameT ren m a
Functor (RenameT ren m)
-> (forall a. a -> RenameT ren m a)
-> (forall a b.
    RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b)
-> (forall a b c.
    (a -> b -> c)
    -> RenameT ren m a -> RenameT ren m b -> RenameT ren m c)
-> (forall a b.
    RenameT ren m a -> RenameT ren m b -> RenameT ren m b)
-> (forall a b.
    RenameT ren m a -> RenameT ren m b -> RenameT ren m a)
-> Applicative (RenameT ren m)
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
RenameT ren m a -> RenameT ren m b -> RenameT ren m a
RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b
(a -> b -> c)
-> RenameT ren m a -> RenameT ren m b -> RenameT ren m c
forall a. a -> RenameT ren m a
forall a b. RenameT ren m a -> RenameT ren m b -> RenameT ren m a
forall a b. RenameT ren m a -> RenameT ren m b -> RenameT ren m b
forall a b.
RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b
forall a b c.
(a -> b -> c)
-> RenameT ren m a -> RenameT ren m b -> RenameT ren m c
forall ren (m :: * -> *). Applicative m => Functor (RenameT ren m)
forall ren (m :: * -> *) a. Applicative m => a -> RenameT ren m a
forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m a
forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b
forall ren (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> RenameT ren m a -> RenameT ren m b -> RenameT ren 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
<* :: RenameT ren m a -> RenameT ren m b -> RenameT ren m a
$c<* :: forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m a
*> :: RenameT ren m a -> RenameT ren m b -> RenameT ren m b
$c*> :: forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
liftA2 :: (a -> b -> c)
-> RenameT ren m a -> RenameT ren m b -> RenameT ren m c
$cliftA2 :: forall ren (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> RenameT ren m a -> RenameT ren m b -> RenameT ren m c
<*> :: RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b
$c<*> :: forall ren (m :: * -> *) a b.
Applicative m =>
RenameT ren m (a -> b) -> RenameT ren m a -> RenameT ren m b
pure :: a -> RenameT ren m a
$cpure :: forall ren (m :: * -> *) a. Applicative m => a -> RenameT ren m a
$cp1Applicative :: forall ren (m :: * -> *). Applicative m => Functor (RenameT ren m)
Applicative, Applicative (RenameT ren m)
RenameT ren m a
Applicative (RenameT ren m)
-> (forall a. RenameT ren m a)
-> (forall a.
    RenameT ren m a -> RenameT ren m a -> RenameT ren m a)
-> (forall a. RenameT ren m a -> RenameT ren m [a])
-> (forall a. RenameT ren m a -> RenameT ren m [a])
-> Alternative (RenameT ren m)
RenameT ren m a -> RenameT ren m a -> RenameT ren m a
RenameT ren m a -> RenameT ren m [a]
RenameT ren m a -> RenameT ren m [a]
forall a. RenameT ren m a
forall a. RenameT ren m a -> RenameT ren m [a]
forall a. RenameT ren m a -> RenameT ren m a -> RenameT ren m a
forall ren (m :: * -> *).
Alternative m =>
Applicative (RenameT ren m)
forall ren (m :: * -> *) a. Alternative m => RenameT ren m a
forall ren (m :: * -> *) a.
Alternative m =>
RenameT ren m a -> RenameT ren m [a]
forall ren (m :: * -> *) a.
Alternative m =>
RenameT ren m a -> RenameT ren m a -> RenameT ren 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
many :: RenameT ren m a -> RenameT ren m [a]
$cmany :: forall ren (m :: * -> *) a.
Alternative m =>
RenameT ren m a -> RenameT ren m [a]
some :: RenameT ren m a -> RenameT ren m [a]
$csome :: forall ren (m :: * -> *) a.
Alternative m =>
RenameT ren m a -> RenameT ren m [a]
<|> :: RenameT ren m a -> RenameT ren m a -> RenameT ren m a
$c<|> :: forall ren (m :: * -> *) a.
Alternative m =>
RenameT ren m a -> RenameT ren m a -> RenameT ren m a
empty :: RenameT ren m a
$cempty :: forall ren (m :: * -> *) a. Alternative m => RenameT ren m a
$cp1Alternative :: forall ren (m :: * -> *).
Alternative m =>
Applicative (RenameT ren m)
Alternative, Applicative (RenameT ren m)
a -> RenameT ren m a
Applicative (RenameT ren m)
-> (forall a b.
    RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren m b)
-> (forall a b.
    RenameT ren m a -> RenameT ren m b -> RenameT ren m b)
-> (forall a. a -> RenameT ren m a)
-> Monad (RenameT ren m)
RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren m b
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
forall a. a -> RenameT ren m a
forall a b. RenameT ren m a -> RenameT ren m b -> RenameT ren m b
forall a b.
RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren m b
forall ren (m :: * -> *). Monad m => Applicative (RenameT ren m)
forall ren (m :: * -> *) a. Monad m => a -> RenameT ren m a
forall ren (m :: * -> *) a b.
Monad m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
forall ren (m :: * -> *) a b.
Monad m =>
RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren 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
return :: a -> RenameT ren m a
$creturn :: forall ren (m :: * -> *) a. Monad m => a -> RenameT ren m a
>> :: RenameT ren m a -> RenameT ren m b -> RenameT ren m b
$c>> :: forall ren (m :: * -> *) a b.
Monad m =>
RenameT ren m a -> RenameT ren m b -> RenameT ren m b
>>= :: RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren m b
$c>>= :: forall ren (m :: * -> *) a b.
Monad m =>
RenameT ren m a -> (a -> RenameT ren m b) -> RenameT ren m b
$cp1Monad :: forall ren (m :: * -> *). Monad m => Applicative (RenameT ren m)
Monad
        , MonadReader ren
        , Monad (RenameT ren m)
Monad (RenameT ren m)
-> (forall a. Quote a -> RenameT ren m a)
-> MonadQuote (RenameT ren m)
Quote a -> RenameT ren m a
forall a. Quote a -> RenameT ren m a
forall ren (m :: * -> *). MonadQuote m => Monad (RenameT ren m)
forall ren (m :: * -> *) a.
MonadQuote m =>
Quote a -> RenameT ren m a
forall (m :: * -> *).
Monad m -> (forall a. Quote a -> m a) -> MonadQuote m
liftQuote :: Quote a -> RenameT ren m a
$cliftQuote :: forall ren (m :: * -> *) a.
MonadQuote m =>
Quote a -> RenameT ren m a
$cp1MonadQuote :: forall ren (m :: * -> *). MonadQuote m => Monad (RenameT ren m)
MonadQuote
        )

-- | A renaming is a mapping from old uniques to new ones.
newtype Renaming unique = Renaming
    { Renaming unique -> UniqueMap unique unique
unRenaming :: UniqueMap unique unique
    } deriving newtype (b -> Renaming unique -> Renaming unique
NonEmpty (Renaming unique) -> Renaming unique
Renaming unique -> Renaming unique -> Renaming unique
(Renaming unique -> Renaming unique -> Renaming unique)
-> (NonEmpty (Renaming unique) -> Renaming unique)
-> (forall b.
    Integral b =>
    b -> Renaming unique -> Renaming unique)
-> Semigroup (Renaming unique)
forall b. Integral b => b -> Renaming unique -> Renaming unique
forall unique. NonEmpty (Renaming unique) -> Renaming unique
forall unique.
Renaming unique -> Renaming unique -> Renaming unique
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall unique b.
Integral b =>
b -> Renaming unique -> Renaming unique
stimes :: b -> Renaming unique -> Renaming unique
$cstimes :: forall unique b.
Integral b =>
b -> Renaming unique -> Renaming unique
sconcat :: NonEmpty (Renaming unique) -> Renaming unique
$csconcat :: forall unique. NonEmpty (Renaming unique) -> Renaming unique
<> :: Renaming unique -> Renaming unique -> Renaming unique
$c<> :: forall unique.
Renaming unique -> Renaming unique -> Renaming unique
Semigroup, Semigroup (Renaming unique)
Renaming unique
Semigroup (Renaming unique)
-> Renaming unique
-> (Renaming unique -> Renaming unique -> Renaming unique)
-> ([Renaming unique] -> Renaming unique)
-> Monoid (Renaming unique)
[Renaming unique] -> Renaming unique
Renaming unique -> Renaming unique -> Renaming unique
forall unique. Semigroup (Renaming unique)
forall unique. Renaming unique
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall unique. [Renaming unique] -> Renaming unique
forall unique.
Renaming unique -> Renaming unique -> Renaming unique
mconcat :: [Renaming unique] -> Renaming unique
$cmconcat :: forall unique. [Renaming unique] -> Renaming unique
mappend :: Renaming unique -> Renaming unique -> Renaming unique
$cmappend :: forall unique.
Renaming unique -> Renaming unique -> Renaming unique
mempty :: Renaming unique
$cmempty :: forall unique. Renaming unique
$cp1Monoid :: forall unique. Semigroup (Renaming unique)
Monoid)

-- | A type-level renaming.
-- Needed for instantiating functions running over types in generic @RenameT ren m@ to
-- a particular type of renaming.
type TypeRenaming = Renaming TypeUnique

-- | A class that specifies which 'Renaming' a @ren@ has inside.
-- A @ren@ can contain several 'Renaming's (like 'Scoped', for example).
class Coercible unique Unique => HasRenaming ren unique where
    renaming :: Lens' ren (Renaming unique)

-- | Scoping-aware mapping from locally unique uniques to globally unique uniques.
data ScopedRenaming = ScopedRenaming
    { ScopedRenaming -> Renaming TypeUnique
_scopedRenamingTypes :: Renaming TypeUnique
    , ScopedRenaming -> Renaming TermUnique
_scopedRenamingTerms :: Renaming TermUnique
    }

makeLenses ''ScopedRenaming

type ScopedRenameT = RenameT ScopedRenaming

instance Semigroup ScopedRenaming where
    ScopedRenaming Renaming TypeUnique
types1 Renaming TermUnique
terms1 <> :: ScopedRenaming -> ScopedRenaming -> ScopedRenaming
<> ScopedRenaming Renaming TypeUnique
types2 Renaming TermUnique
terms2 =
        Renaming TypeUnique -> Renaming TermUnique -> ScopedRenaming
ScopedRenaming (Renaming TypeUnique
types1 Renaming TypeUnique -> Renaming TypeUnique -> Renaming TypeUnique
forall a. Semigroup a => a -> a -> a
<> Renaming TypeUnique
types2) (Renaming TermUnique
terms1 Renaming TermUnique -> Renaming TermUnique -> Renaming TermUnique
forall a. Semigroup a => a -> a -> a
<> Renaming TermUnique
terms2)

instance Monoid ScopedRenaming where
    mempty :: ScopedRenaming
mempty = Renaming TypeUnique -> Renaming TermUnique -> ScopedRenaming
ScopedRenaming Renaming TypeUnique
forall a. Monoid a => a
mempty Renaming TermUnique
forall a. Monoid a => a
mempty

instance (Coercible unique1 Unique, unique1 ~ unique2) =>
        HasRenaming (Renaming unique1) unique2 where
    renaming :: (Renaming unique2 -> f (Renaming unique2))
-> Renaming unique1 -> f (Renaming unique1)
renaming = (Renaming unique2 -> f (Renaming unique2))
-> Renaming unique1 -> f (Renaming unique1)
forall a. a -> a
id

instance HasRenaming ScopedRenaming TypeUnique where
    renaming :: (Renaming TypeUnique -> f (Renaming TypeUnique))
-> ScopedRenaming -> f ScopedRenaming
renaming = (Renaming TypeUnique -> f (Renaming TypeUnique))
-> ScopedRenaming -> f ScopedRenaming
Lens' ScopedRenaming (Renaming TypeUnique)
scopedRenamingTypes ((Renaming TypeUnique -> f (Renaming TypeUnique))
 -> ScopedRenaming -> f ScopedRenaming)
-> ((Renaming TypeUnique -> f (Renaming TypeUnique))
    -> Renaming TypeUnique -> f (Renaming TypeUnique))
-> (Renaming TypeUnique -> f (Renaming TypeUnique))
-> ScopedRenaming
-> f ScopedRenaming
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Renaming TypeUnique -> f (Renaming TypeUnique))
-> Renaming TypeUnique -> f (Renaming TypeUnique)
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
renaming

instance HasRenaming ScopedRenaming TermUnique where
    renaming :: (Renaming TermUnique -> f (Renaming TermUnique))
-> ScopedRenaming -> f ScopedRenaming
renaming = (Renaming TermUnique -> f (Renaming TermUnique))
-> ScopedRenaming -> f ScopedRenaming
Lens' ScopedRenaming (Renaming TermUnique)
scopedRenamingTerms ((Renaming TermUnique -> f (Renaming TermUnique))
 -> ScopedRenaming -> f ScopedRenaming)
-> ((Renaming TermUnique -> f (Renaming TermUnique))
    -> Renaming TermUnique -> f (Renaming TermUnique))
-> (Renaming TermUnique -> f (Renaming TermUnique))
-> ScopedRenaming
-> f ScopedRenaming
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Renaming TermUnique -> f (Renaming TermUnique))
-> Renaming TermUnique -> f (Renaming TermUnique)
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
renaming

-- | Run a 'RenameT' computation with an empty renaming.
runRenameT :: Monoid ren => RenameT ren m a -> m a
runRenameT :: RenameT ren m a -> m a
runRenameT (RenameT ReaderT ren m a
a) = ReaderT ren m a -> ren -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT ren m a
a ren
forall a. Monoid a => a
mempty

-- | Map the underlying representation of 'Renaming'.
mapRenaming
    :: (UniqueMap unique unique -> UniqueMap unique unique)
    -> Renaming unique
    -> Renaming unique
mapRenaming :: (UniqueMap unique unique -> UniqueMap unique unique)
-> Renaming unique -> Renaming unique
mapRenaming = (UniqueMap unique unique -> UniqueMap unique unique)
-> Renaming unique -> Renaming unique
coerce

-- | Save the mapping from the @unique@ of a name to a new @unique@.
insertByNameM
    :: (HasUnique name unique, HasRenaming ren unique)
    => name -> unique -> ren -> ren
insertByNameM :: name -> unique -> ren -> ren
insertByNameM name
name = ASetter ren ren (Renaming unique) (Renaming unique)
-> (Renaming unique -> Renaming unique) -> ren -> ren
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter ren ren (Renaming unique) (Renaming unique)
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
renaming ((Renaming unique -> Renaming unique) -> ren -> ren)
-> (unique -> Renaming unique -> Renaming unique)
-> unique
-> ren
-> ren
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UniqueMap unique unique -> UniqueMap unique unique)
-> Renaming unique -> Renaming unique
forall unique.
(UniqueMap unique unique -> UniqueMap unique unique)
-> Renaming unique -> Renaming unique
mapRenaming ((UniqueMap unique unique -> UniqueMap unique unique)
 -> Renaming unique -> Renaming unique)
-> (unique -> UniqueMap unique unique -> UniqueMap unique unique)
-> unique
-> Renaming unique
-> Renaming unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. name
-> unique -> UniqueMap unique unique -> UniqueMap unique unique
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName name
name

-- | Look up the new unique a name got mapped to.
lookupNameM
    :: (HasUnique name unique, HasRenaming ren unique, MonadReader ren m)
    => name -> m (Maybe unique)
lookupNameM :: name -> m (Maybe unique)
lookupNameM name
name = (ren -> Maybe unique) -> m (Maybe unique)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((ren -> Maybe unique) -> m (Maybe unique))
-> (ren -> Maybe unique) -> m (Maybe unique)
forall a b. (a -> b) -> a -> b
$ name -> UniqueMap unique unique -> Maybe unique
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName name
name (UniqueMap unique unique -> Maybe unique)
-> (ren -> UniqueMap unique unique) -> ren -> Maybe unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Renaming unique -> UniqueMap unique unique
forall unique. Renaming unique -> UniqueMap unique unique
unRenaming (Renaming unique -> UniqueMap unique unique)
-> (ren -> Renaming unique) -> ren -> UniqueMap unique unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Renaming unique) ren (Renaming unique)
-> ren -> Renaming unique
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Renaming unique) ren (Renaming unique)
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
renaming

-- | Rename a name that has a unique inside.
renameNameM
    :: (HasRenaming ren unique, HasUnique name unique, MonadReader ren m)
    => name -> m name
renameNameM :: name -> m name
renameNameM name
name = do
    Maybe unique
mayUniqNew <- name -> m (Maybe unique)
forall name unique ren (m :: * -> *).
(HasUnique name unique, HasRenaming ren unique,
 MonadReader ren m) =>
name -> m (Maybe unique)
lookupNameM name
name
    name -> m name
forall (f :: * -> *) a. Applicative f => a -> f a
pure (name -> m name) -> name -> m name
forall a b. (a -> b) -> a -> b
$ case Maybe unique
mayUniqNew of
        Maybe unique
Nothing      -> name
name
        Just unique
uniqNew -> name
name name -> (name -> name) -> name
forall a b. a -> (a -> b) -> b
& (unique -> Identity unique) -> name -> Identity name
forall a unique. HasUnique a unique => Lens' a unique
unique ((unique -> Identity unique) -> name -> Identity name)
-> unique -> name -> name
forall s t a b. ASetter s t a b -> b -> s -> t
.~ unique
uniqNew

-- | Replace the unique in a name by a new unique, save the mapping
-- from the old unique to the new one and supply the updated value to a continuation.
withFreshenedName
    :: (HasRenaming ren unique, HasUnique name unique, MonadQuote m, MonadReader ren m)
    => name -> (name -> m c) -> m c
withFreshenedName :: name -> (name -> m c) -> m c
withFreshenedName name
nameOld name -> m c
k = do
    unique
uniqNew <- Unique -> unique
coerce (Unique -> unique) -> m Unique -> m unique
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Unique
forall (m :: * -> *). MonadQuote m => m Unique
freshUnique
    (ren -> ren) -> m c -> m c
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (name -> unique -> ren -> ren
forall name unique ren.
(HasUnique name unique, HasRenaming ren unique) =>
name -> unique -> ren -> ren
insertByNameM name
nameOld unique
uniqNew) (m c -> m c) -> m c -> m c
forall a b. (a -> b) -> a -> b
$ name -> m c
k (name
nameOld name -> (name -> name) -> name
forall a b. a -> (a -> b) -> b
& (unique -> Identity unique) -> name -> Identity name
forall a unique. HasUnique a unique => Lens' a unique
unique ((unique -> Identity unique) -> name -> Identity name)
-> unique -> name -> name
forall s t a b. ASetter s t a b -> b -> s -> t
.~ unique
uniqNew)

-- | Run a 'RenameT' computation in the environment extended by the mapping from an old name
-- to a new one.
withRenamedName
    :: (HasRenaming ren unique, HasUnique name unique, MonadReader ren m)
    => name -> name -> m c -> m c
withRenamedName :: name -> name -> m c -> m c
withRenamedName name
old name
new = (ren -> ren) -> m c -> m c
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ren -> ren) -> m c -> m c) -> (ren -> ren) -> m c -> m c
forall a b. (a -> b) -> a -> b
$ name -> unique -> ren -> ren
forall name unique ren.
(HasUnique name unique, HasRenaming ren unique) =>
name -> unique -> ren -> ren
insertByNameM name
old (name
new name -> Getting unique name unique -> unique
forall s a. s -> Getting a s a -> a
^. Getting unique name unique
forall a unique. HasUnique a unique => Lens' a unique
unique)