{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Renaming of PIR terms. Import this module to bring the @PLC.Rename (Term tyname name uni fun ann)@
-- instance in scope.
module PlutusIR.Transform.Rename
    ( renameTermM
    , renameProgramM
    ) where

import PlutusPrelude

import PlutusIR
import PlutusIR.Mark

import PlutusCore qualified as PLC
import PlutusCore.Name qualified as PLC
import PlutusCore.Rename.Internal qualified as PLC

import Control.Monad.Reader
import Control.Monad.Trans.Cont (ContT (..))

{- Note [Renaming of mutually recursive bindings]
The 'RenameM' monad is a newtype wrapper around @ReaderT renaming Quote@, so in order to bring
a name into the scope we need to use the following pattern:

    withFreshenedX :: X -> (X -> RenameM renaming c) -> RenameM renaming c

where an 'X' is some value that has names inside and the second argument is a continuation that
expects to receive this value, but with all the names freshened and with the mappings from the
old uniques to the new ones saved. For the latter reason we can't just write

    freshenX :: X -> RenameM renaming X

because if you write

    freshenX x >>= \xFr -> ...

then the mappings from the uniques of 'x' to the uniques of 'xFr' do not exist in @...@.

Two problems arise:

1. If you have a list of @X@s and then an @Y@ and then another list of @Z@s and you need to freshen
   all of those, it's not nice to compose @withFreshened*@ functions at all. In order to make these
   functions composable, we can wrap them in the 'ContT' monad. See e.g. 'renameDatatypeCM' below.
2. Handling of mutually recursive bindings requires to bring a bunch of bindings in scope first and
   only then to rename their RHSs. I.e. one part of a 'ScopedRenameM' computation must be performed
   immediately (brinding names in scope) and the other part must be postponed until all bindings
   are in scope (renaming of RHSs). We will refer to this scheme as "two-stage renaming".

   Hence we have the following pattern:

       renameXCM :: X -> ContT c PLC.ScopedRenameM (PLC.ScopedRenameM X)

   where an 'X' is some value that defines some names and has types/terms that need to be renamed.
   The first 'PLC.ScopedRenameM' is for bringing names (the first stage) in scope and the second
   'PLC.ScopedRenameM' is for performing the renaming (the second stage).
-}

{- Note [Weird IR data types]
We don't attempt to recognize in the renamer a family of mutually recursive data types where two
or more data types have the same name, so the renamer's behavior in that case is undefined.
The same applies to a data type having identically named constructors or when a constructor has
the same name as the matcher etc.

The AST of Plutus IR allows us to represent some weird data types like

    data D where
        C : integer -> (\d -> d) D

    data D where
        C : (\d -> d) (integer -> D)

We don't pretend that we can handle those at all. The renamer calls 'error' upon seeing anything of
this kind.

However this one:

    data D x where
        C : all D. D x -> D x

is perfectly unambiguous:

1. the head (@D@) of the application (@D x@) in the type of the result (after @->@) has to refer to
   the data type being defined and so @all D@ is not supposed to result in shadowing there
2. @all D@ shadows the name of the data type everywhere before the final @->@, so it does not matter
   whether @D@ is recursive or not as any @D@ before the final @->@ refers to the @all@-bound @D@
   regardless of recursivity.

Note that @all D@ is existential quantification and the type checker wasn't able to handle that at
the time this note was written.

Similarly, in

    data D D where
        C : D -> D

the parameter shadows the data type before @->@ and does not shadow it afterwards regardless of
recursivity.

Note also that for example the following:

    data D1 x where
        C1 : all x. D1 x

is not existential quantification and should mean the same thing as

    data D2 x where
        C2 : D2 x

but also was blowing up the type checker at the time the note was written.

Haskell agrees that these two data types are isomorphic:

    data D1 x where
        C1 :: forall x. D1 x

    data D2 x where
        C2 :: D2 x

    d12 :: D1 x -> D2 x
    d12 C1 = C2

    d21 :: D2 x -> D1 x
    d21 C2 = C1

Note @D1@ only requires @GADTSyntax@ and not full-blown @GADTs@.

Speaking of GADTs, the following data type:

    data D D where
        C : D D

is only unambiguous if we stipulate that GADTs are not allowed in Plutus IR (otherwise the last
@D@ could be an index referring to the data type rather than the parameter).

So what we do in the renamer is rename everything as normal apart from the head of the application
after the final @->@ in the type of a constructor (let's call that "the final head"). Instead, the
final head is renamed in the context that the whole data type is renamed in plus the name of the
data type, which ensures that neither parameters nor @all@-bound variables in the type of the
constructor can shadow the name of the data type in the final head. This effectively bans the
GADT interpretation of the @data D D@ example from the above thus removing ambiguity.

This agrees perfectly with what we need to do to handle recursivity in constructors, see
Note [Renaming of constructors].
-}

{- Note [Renaming of constructors]
Consider the following data type:

    data Loop where
        MkLoop : Loop -> Loop

Whether the occurrence of @Loop@ before @->@ in the type of @MkLoop@ refers to @Loop@-the-data-type
or not depends on whether the data type is declared as recursive or not. However the occurrence of
@Loop@ after @->@ always refers to @Loop@-the-data-type. So we can't just directly rename the type
of a constructor with some general 'renameTypeM' stuff, we have to actually traverse the type and
rename things before the final @->@ differently depending on recursivity without doing so for the
final type as was discussed in Note [Weird IR data types].

However the current context is stored inside the 'RenameT' transformer and changing it manually
would be quite unpleasant as 'RenameT' is designed specifically to abstract these details out.
Instead, we provide a function that captures the current context in a 'Restorer' that allows us
to restore that context later. We use the capturing function twice: right before binding the name
of a data type and right after, which gives us two respective restorers. The former restorer is
used when type checking constructors of non-recursive data types: binding the name of data type
ensures that the data type is visible after the 'DatatypeBind' entry of the corresponding @let@
and using the restorer ensures that the name of the data type is not visible in the type of
constructors (as the data type is non-recursive) apart from the final head. And since recursivity
has no impact on how the final head is renamed, we use the right-after-the-name-of-the-data-type
restorer once we reach the final head. This gives us a single function for renaming types of
constructors in both the recursive and non-recursive cases letting us handle recursivity with a
single line in the function renaming a data type.
-}

{- Note [Mutual vs non-mutual recursion]
Note [Renaming of mutually recursive bindings] describes how we handle recursive bindings.
There's nothing special about the way we handle non-recursive ones, however it's worth saying
explicitly that in

    let nonrec x = <...>

@x@ is not visible in @<...>@, which makes it hard to share code between functions that handle
recursive and non-recursive bindings, so we don't.

Note [Renaming of constructors] describes how we managed to handle types of constructors of
recursive and non-recursive data types with a single function.
-}

instance PLC.HasUniques (Term tyname name uni fun ann) => PLC.Rename (Term tyname name uni fun ann) where
    -- See Note [Marking]
    rename :: Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
rename = (Term tyname name uni fun ann -> m ())
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Term tyname name uni fun ann -> m ()
forall tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m) =>
Term tyname name uni fun ann -> m ()
markNonFreshTerm (Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
    -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RenameT ScopedRenaming m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall ren (m :: * -> *) a. Monoid ren => RenameT ren m a -> m a
PLC.runRenameT (RenameT ScopedRenaming m (Term tyname name uni fun ann)
 -> m (Term tyname name uni fun ann))
-> (Term tyname name uni fun ann
    -> RenameT ScopedRenaming m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> m (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term tyname name uni fun ann
-> RenameT ScopedRenaming m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM

instance PLC.HasUniques (Term tyname name uni fun ann) => PLC.Rename (Program tyname name uni fun ann) where
    rename :: Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
rename (Program ann
ann Term tyname name uni fun ann
term) = ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
Program ann
ann (Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Program tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
PLC.rename Term tyname name uni fun ann
term

-- See Note [Renaming of constructors].
-- | A wrapper around a function restoring some old context of the renamer.
newtype Restorer m = Restorer
    { Restorer m -> forall a. m a -> m a
unRestorer :: forall a. m a -> m a
    }

-- | Capture the current context in a 'Restorer'.
captureContext :: MonadReader ren m => ContT c m (Restorer m)
captureContext :: ContT c m (Restorer m)
captureContext = ((Restorer m -> m c) -> m c) -> ContT c m (Restorer m)
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((Restorer m -> m c) -> m c) -> ContT c m (Restorer m))
-> ((Restorer m -> m c) -> m c) -> ContT c m (Restorer m)
forall a b. (a -> b) -> a -> b
$ \Restorer m -> m c
k -> do
    ren
env <- m ren
forall r (m :: * -> *). MonadReader r m => m r
ask
    Restorer m -> m c
k (Restorer m -> m c) -> Restorer m -> m c
forall a b. (a -> b) -> a -> b
$ (forall a. m a -> m a) -> Restorer m
forall (m :: * -> *). (forall a. m a -> m a) -> Restorer m
Restorer ((forall a. m a -> m a) -> Restorer m)
-> (forall a. m a -> m a) -> Restorer m
forall a b. (a -> b) -> a -> b
$ (ren -> ren) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((ren -> ren) -> m a -> m a) -> (ren -> ren) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ren -> ren -> ren
forall a b. a -> b -> a
const ren
env

type MonadRename m = (PLC.MonadQuote m, MonadReader PLC.ScopedRenaming m)

-- | Rename the type of a constructor given a restorer dropping all variables bound after the
-- name of the data type.
renameConstrTypeM
    :: (MonadRename m, PLC.HasUniques (Type tyname uni ann))
    => Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM :: Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM (Restorer forall a. m a -> m a
restoreAfterData) = Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM where
    renameSpineM :: Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM (TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
ty) =
        tyname
-> (tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
 MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName tyname
name ((tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann))
-> (tyname -> m (Type tyname uni ann)) -> m (Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ \tyname
nameFr -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
nameFr Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM Type tyname uni ann
ty
    renameSpineM (TyFun ann
ann Type tyname uni ann
dom Type tyname uni ann
cod) = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
dom m (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
renameSpineM Type tyname uni ann
cod
    renameSpineM Type tyname uni ann
ty = Type tyname uni ann -> m (Type tyname uni ann)
renameResultM Type tyname uni ann
ty

    renameResultM :: Type tyname uni ann -> m (Type tyname uni ann)
renameResultM (TyApp ann
ann Type tyname uni ann
fun Type tyname uni ann
arg) = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
renameResultM Type tyname uni ann
fun m (Type tyname uni ann -> Type tyname uni ann)
-> m (Type tyname uni ann) -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
arg
    renameResultM (TyVar ann
ann tyname
name) = ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (tyname -> Type tyname uni ann)
-> m tyname -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m tyname -> m tyname
forall a. m a -> m a
restoreAfterData (tyname -> m tyname
forall ren unique name (m :: * -> *).
(HasRenaming ren unique, HasUnique name unique,
 MonadReader ren m) =>
name -> m name
PLC.renameNameM tyname
name)
    renameResultM Type tyname uni ann
_ =
        [Char] -> m (Type tyname uni ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: a constructor returns something that is not an iterated application of a type variable"

-- | Rename the name of a constructor immediately and defer renaming of its type until the second
-- stage where all mutually recursive data types (if any) are bound.
renameConstrCM
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Restorer m
    -> VarDecl tyname name uni fun ann
    -> ContT c m (m (VarDecl tyname name uni fun ann))
renameConstrCM :: Restorer m
-> VarDecl tyname name uni fun ann
-> ContT c m (m (VarDecl tyname name uni fun ann))
renameConstrCM Restorer m
restorerAfterData (VarDecl ann
ann name
name Type tyname uni ann
ty) = do
    name
nameFr <- ((name -> m c) -> m c) -> ContT c m name
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((name -> m c) -> m c) -> ContT c m name)
-> ((name -> m c) -> m c) -> ContT c m name
forall a b. (a -> b) -> a -> b
$ name -> (name -> m c) -> m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
 MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
name
    m (VarDecl tyname name uni fun ann)
-> ContT c m (m (VarDecl tyname name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (VarDecl tyname name uni fun ann)
 -> ContT c m (m (VarDecl tyname name uni fun ann)))
-> m (VarDecl tyname name uni fun ann)
-> ContT c m (m (VarDecl tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
ann name
nameFr (Type tyname uni ann -> VarDecl tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (VarDecl tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
(MonadRename m, HasUniques (Type tyname uni ann)) =>
Restorer m -> Type tyname uni ann -> m (Type tyname uni ann)
renameConstrTypeM Restorer m
restorerAfterData Type tyname uni ann
ty

-- | Apply a function to a value in the non-recursive case and return the value unchanged otherwise.
onNonRec :: Recursivity -> (a -> a) -> a -> a
onNonRec :: Recursivity -> (a -> a) -> a -> a
onNonRec Recursivity
NonRec a -> a
f a
x = a -> a
f a
x
onNonRec Recursivity
Rec    a -> a
_ a
x = a
x

-- See Note [Weird IR data types]
-- See Note [Renaming of constructors] (and make sure you understand all the intricacies in it
-- before toucing this function).
-- | Rename a 'Datatype' in the CPS-transformed 'ScopedRenameM' monad.
renameDatatypeCM
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Recursivity
    -> Datatype tyname name uni fun ann
    -> ContT c m (m (Datatype tyname name uni fun ann))
renameDatatypeCM :: Recursivity
-> Datatype tyname name uni fun ann
-> ContT c m (m (Datatype tyname name uni fun ann))
renameDatatypeCM Recursivity
recy (Datatype ann
x TyVarDecl tyname ann
dataDecl [TyVarDecl tyname ann]
params name
matchName [VarDecl tyname name uni fun ann]
constrs) = do
    -- The first stage (the data type itself, its constructors and its matcher get renamed).
    -- Note that all of these are visible downstream.
    Restorer m
restorerBeforeData <- ContT c m (Restorer m)
forall ren (m :: * -> *) c.
MonadReader ren m =>
ContT c m (Restorer m)
captureContext
    TyVarDecl tyname ann
dataDeclFr         <- ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m c) -> m c)
 -> ContT c m (TyVarDecl tyname ann))
-> ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall a b. (a -> b) -> a -> b
$ TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
dataDecl
    Restorer m
restorerAfterData  <- ContT c m (Restorer m)
forall ren (m :: * -> *) c.
MonadReader ren m =>
ContT c m (Restorer m)
captureContext
    [m (VarDecl tyname name uni fun ann)]
constrsRen         <- (VarDecl tyname name uni fun ann
 -> ContT c m (m (VarDecl tyname name uni fun ann)))
-> [VarDecl tyname name uni fun ann]
-> ContT c m [m (VarDecl tyname name uni fun ann)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Restorer m
-> VarDecl tyname name uni fun ann
-> ContT c m (m (VarDecl tyname name uni fun ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Restorer m
-> VarDecl tyname name uni fun ann
-> ContT c m (m (VarDecl tyname name uni fun ann))
renameConstrCM Restorer m
restorerAfterData) [VarDecl tyname name uni fun ann]
constrs
    name
matchNameFr        <- ((name -> m c) -> m c) -> ContT c m name
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((name -> m c) -> m c) -> ContT c m name)
-> ((name -> m c) -> m c) -> ContT c m name
forall a b. (a -> b) -> a -> b
$ name -> (name -> m c) -> m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
 MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
matchName
    -- The second stage (the type parameters and types of constructors get renamed).
    -- Note that parameters are only visible in the types of constructors and not downstream.
    m (Datatype tyname name uni fun ann)
-> ContT c m (m (Datatype tyname name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Datatype tyname name uni fun ann)
 -> ContT c m (m (Datatype tyname name uni fun ann)))
-> (m (Datatype tyname name uni fun ann)
    -> m (Datatype tyname name uni fun ann))
-> m (Datatype tyname name uni fun ann)
-> ContT c m (m (Datatype tyname name uni fun ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Recursivity
-> (m (Datatype tyname name uni fun ann)
    -> m (Datatype tyname name uni fun ann))
-> m (Datatype tyname name uni fun ann)
-> m (Datatype tyname name uni fun ann)
forall a. Recursivity -> (a -> a) -> a -> a
onNonRec Recursivity
recy (Restorer m -> forall a. m a -> m a
forall (m :: * -> *). Restorer m -> forall a. m a -> m a
unRestorer Restorer m
restorerBeforeData) (m (Datatype tyname name uni fun ann)
 -> ContT c m (m (Datatype tyname name uni fun ann)))
-> m (Datatype tyname name uni fun ann)
-> ContT c m (m (Datatype tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$
        ContT (Datatype tyname name uni fun ann) m [TyVarDecl tyname ann]
-> ([TyVarDecl tyname ann] -> m (Datatype tyname name uni fun ann))
-> m (Datatype tyname name uni fun ann)
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT ((TyVarDecl tyname ann
 -> ContT
      (Datatype tyname name uni fun ann) m (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> ContT
     (Datatype tyname name uni fun ann) m [TyVarDecl tyname ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (((TyVarDecl tyname ann -> m (Datatype tyname name uni fun ann))
 -> m (Datatype tyname name uni fun ann))
-> ContT
     (Datatype tyname name uni fun ann) m (TyVarDecl tyname ann)
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m (Datatype tyname name uni fun ann))
  -> m (Datatype tyname name uni fun ann))
 -> ContT
      (Datatype tyname name uni fun ann) m (TyVarDecl tyname ann))
-> (TyVarDecl tyname ann
    -> (TyVarDecl tyname ann -> m (Datatype tyname name uni fun ann))
    -> m (Datatype tyname name uni fun ann))
-> TyVarDecl tyname ann
-> ContT
     (Datatype tyname name uni fun ann) m (TyVarDecl tyname ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl tyname ann
-> (TyVarDecl tyname ann -> m (Datatype tyname name uni fun ann))
-> m (Datatype tyname name uni fun ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl) [TyVarDecl tyname ann]
params) (([TyVarDecl tyname ann] -> m (Datatype tyname name uni fun ann))
 -> m (Datatype tyname name uni fun ann))
-> ([TyVarDecl tyname ann] -> m (Datatype tyname name uni fun ann))
-> m (Datatype tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \[TyVarDecl tyname ann]
paramsFr ->
            ann
-> TyVarDecl tyname ann
-> [TyVarDecl tyname ann]
-> name
-> [VarDecl tyname name uni fun ann]
-> Datatype tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype ann
x TyVarDecl tyname ann
dataDeclFr [TyVarDecl tyname ann]
paramsFr name
matchNameFr ([VarDecl tyname name uni fun ann]
 -> Datatype tyname name uni fun ann)
-> m [VarDecl tyname name uni fun ann]
-> m (Datatype tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m (VarDecl tyname name uni fun ann)]
-> m [VarDecl tyname name uni fun ann]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [m (VarDecl tyname name uni fun ann)]
constrsRen

-- | Rename a 'Binding' from a non-recursive family in the CPS-transformed 'ScopedRenameM' monad.
renameBindingNonRecC
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Binding tyname name uni fun ann
    -> ContT c m (Binding tyname name uni fun ann)
-- Unlike in the recursive case we don't have any stage separation here.
--
-- 'TypeBind' is the simplest case: the body of the binding gets renamed first, then the name of
-- the binding is brought in scope (not the other way around! As that would bring the name of the
-- binding in scope in its own body, which is very wrong in the non-recursive case) and the
-- renamed 'TypeBind' is passed to the continuation.
--
-- 'TermBind' also requires us to discharge the computation returning a variable with a renamed term-- before feeding the continuation. The reason why 'withFreshenedVarDecl' provides the caller with a
-- computation rather than a pure term is because that is how we bring mutually recursive bindings
-- in scope first without renaming their types right away (as those can reference type bindings from
-- the same family) while still being able to perform the renaming later. But we don't need that
-- stage separation in the non-recursive case, hence the type of the binding is renamed right away.
--
-- 'DatatypeBind' is handled the same way as 'TermBind' except all the work is performed in
-- 'renameDatatypeCM' and here we just unwrap from 'ContT' and perform all the renaming saved for
-- stage two immediately just like in the 'TermBind' case and for the same reason.
renameBindingNonRecC :: Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
renameBindingNonRecC Binding tyname name uni fun ann
binding = ((Binding tyname name uni fun ann -> m c) -> m c)
-> ContT c m (Binding tyname name uni fun ann)
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((Binding tyname name uni fun ann -> m c) -> m c)
 -> ContT c m (Binding tyname name uni fun ann))
-> ((Binding tyname name uni fun ann -> m c) -> m c)
-> ContT c m (Binding tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \Binding tyname name uni fun ann -> m c
cont -> case Binding tyname name uni fun ann
binding of
    TermBind ann
x Strictness
s VarDecl tyname name uni fun ann
var Term tyname name uni fun ann
term -> do
        Term tyname name uni fun ann
termFr <- Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
        VarDecl tyname name uni fun ann
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
forall tyname name (uni :: * -> *) fun ann (m :: * -> *) c.
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
VarDecl tyname name uni fun ann
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
PLC.withFreshenedVarDecl VarDecl tyname name uni fun ann
var ((m (VarDecl tyname name uni fun ann) -> m c) -> m c)
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \m (VarDecl tyname name uni fun ann)
varRen -> do
            VarDecl tyname name uni fun ann
varFr <- m (VarDecl tyname name uni fun ann)
varRen
            Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> Binding tyname name uni fun ann -> m c
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni fun ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
s VarDecl tyname name uni fun ann
varFr Term tyname name uni fun ann
termFr
    TypeBind ann
x TyVarDecl tyname ann
var Type tyname uni ann
ty -> do
        Type tyname uni ann
tyFr <- Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
        TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
var ((TyVarDecl tyname ann -> m c) -> m c)
-> (TyVarDecl tyname ann -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \TyVarDecl tyname ann
varFr ->
            Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> Binding tyname name uni fun ann -> m c
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
varFr Type tyname uni ann
tyFr
    DatatypeBind ann
x Datatype tyname name uni fun ann
datatype -> do
        ContT c m (m (Datatype tyname name uni fun ann))
-> (m (Datatype tyname name uni fun ann) -> m c) -> m c
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT (Recursivity
-> Datatype tyname name uni fun ann
-> ContT c m (m (Datatype tyname name uni fun ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> Datatype tyname name uni fun ann
-> ContT c m (m (Datatype tyname name uni fun ann))
renameDatatypeCM Recursivity
NonRec Datatype tyname name uni fun ann
datatype) ((m (Datatype tyname name uni fun ann) -> m c) -> m c)
-> (m (Datatype tyname name uni fun ann) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \m (Datatype tyname name uni fun ann)
datatypeRen ->
            m (Datatype tyname name uni fun ann)
datatypeRen m (Datatype tyname name uni fun ann)
-> (Datatype tyname name uni fun ann -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Binding tyname name uni fun ann -> m c
cont (Binding tyname name uni fun ann -> m c)
-> (Datatype tyname name uni fun ann
    -> Binding tyname name uni fun ann)
-> Datatype tyname name uni fun ann
-> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Datatype tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind ann
x

-- | Rename a 'Binding' from a recursive family in the CPS-transformed 'ScopedRenameM' monad.
renameBindingRecCM
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Binding tyname name uni fun ann
    -> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM :: Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM = \case
    TermBind ann
x Strictness
s VarDecl tyname name uni fun ann
var Term tyname name uni fun ann
term -> do
        -- The first stage (the variable gets renamed).
        m (VarDecl tyname name uni fun ann)
varRen <- ((m (VarDecl tyname name uni fun ann) -> m c) -> m c)
-> ContT c m (m (VarDecl tyname name uni fun ann))
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((m (VarDecl tyname name uni fun ann) -> m c) -> m c)
 -> ContT c m (m (VarDecl tyname name uni fun ann)))
-> ((m (VarDecl tyname name uni fun ann) -> m c) -> m c)
-> ContT c m (m (VarDecl tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ VarDecl tyname name uni fun ann
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
forall tyname name (uni :: * -> *) fun ann (m :: * -> *) c.
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
VarDecl tyname name uni fun ann
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
PLC.withFreshenedVarDecl VarDecl tyname name uni fun ann
var
        -- The second stage (the type of the variable and the RHS get renamed).
        m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
 -> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> Strictness
-> VarDecl tyname name uni fun ann
-> Term tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind ann
x Strictness
s (VarDecl tyname name uni fun ann
 -> Term tyname name uni fun ann -> Binding tyname name uni fun ann)
-> m (VarDecl tyname name uni fun ann)
-> m (Term tyname name uni fun ann
      -> Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (VarDecl tyname name uni fun ann)
varRen m (Term tyname name uni fun ann -> Binding tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
    TypeBind ann
x TyVarDecl tyname ann
var Type tyname uni ann
ty -> do
        -- The first stage (the variable gets renamed).
        TyVarDecl tyname ann
varFr <- ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((TyVarDecl tyname ann -> m c) -> m c)
 -> ContT c m (TyVarDecl tyname ann))
-> ((TyVarDecl tyname ann -> m c) -> m c)
-> ContT c m (TyVarDecl tyname ann)
forall a b. (a -> b) -> a -> b
$ TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
forall ren tyname (uni :: * -> *) ann (m :: * -> *) c.
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
PLC.withFreshenedTyVarDecl TyVarDecl tyname ann
var
        -- The second stage (the RHS gets renamed).
        m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
 -> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> TyVarDecl tyname ann
-> Type tyname uni ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind ann
x TyVarDecl tyname ann
varFr (Type tyname uni ann -> Binding tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
    DatatypeBind ann
x Datatype tyname name uni fun ann
datatype -> do
        -- The first stage.
        m (Datatype tyname name uni fun ann)
datatypeRen <- Recursivity
-> Datatype tyname name uni fun ann
-> ContT c m (m (Datatype tyname name uni fun ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> Datatype tyname name uni fun ann
-> ContT c m (m (Datatype tyname name uni fun ann))
renameDatatypeCM Recursivity
Rec Datatype tyname name uni fun ann
datatype
        -- The second stage.
        m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (Binding tyname name uni fun ann)
 -> ContT c m (m (Binding tyname name uni fun ann)))
-> m (Binding tyname name uni fun ann)
-> ContT c m (m (Binding tyname name uni fun ann))
forall a b. (a -> b) -> a -> b
$ ann
-> Datatype tyname name uni fun ann
-> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind ann
x (Datatype tyname name uni fun ann
 -> Binding tyname name uni fun ann)
-> m (Datatype tyname name uni fun ann)
-> m (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Datatype tyname name uni fun ann)
datatypeRen

-- | Replace the uniques in the names stored in a bunch of bindings by new uniques,
-- save the mapping from the old uniques to the new ones, rename the RHSs and
-- supply the updated bindings to a continuation.
withFreshenedBindings
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Recursivity
    -> NonEmpty (Binding tyname name uni fun ann)
    -> (NonEmpty (Binding tyname name uni fun ann) -> m c)
    -> m c
withFreshenedBindings :: Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> m c
withFreshenedBindings Recursivity
recy NonEmpty (Binding tyname name uni fun ann)
binds NonEmpty (Binding tyname name uni fun ann) -> m c
cont = case Recursivity
recy of
    -- Bring each binding in scope, rename its RHS straight away, collect all the results and
    -- supply them to the continuation.
    Recursivity
NonRec -> ContT c m (NonEmpty (Binding tyname name uni fun ann))
-> (NonEmpty (Binding tyname name uni fun ann) -> m c) -> m c
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT ((Binding tyname name uni fun ann
 -> ContT c m (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> ContT c m (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (Binding tyname name uni fun ann)
renameBindingNonRecC NonEmpty (Binding tyname name uni fun ann)
binds) NonEmpty (Binding tyname name uni fun ann) -> m c
cont
    -- First bring all bindinds in scope and only then rename their RHSs and
    -- supply the results to the continuation.
    Recursivity
Rec    -> ContT c m (NonEmpty (m (Binding tyname name uni fun ann)))
-> (NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT ((Binding tyname name uni fun ann
 -> ContT c m (m (Binding tyname name uni fun ann)))
-> NonEmpty (Binding tyname name uni fun ann)
-> ContT c m (NonEmpty (m (Binding tyname name uni fun ann)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Binding tyname name uni fun ann
-> ContT c m (m (Binding tyname name uni fun ann))
renameBindingRecCM NonEmpty (Binding tyname name uni fun ann)
binds) ((NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c)
-> (NonEmpty (m (Binding tyname name uni fun ann)) -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ NonEmpty (m (Binding tyname name uni fun ann))
-> m (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (NonEmpty (m (Binding tyname name uni fun ann))
 -> m (NonEmpty (Binding tyname name uni fun ann)))
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> NonEmpty (m (Binding tyname name uni fun ann))
-> m c
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> NonEmpty (Binding tyname name uni fun ann) -> m c
cont

-- | Rename a 'Term' in the 'ScopedRenameM' monad.
renameTermM
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM :: Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM = \case
    Let ann
x Recursivity
r NonEmpty (Binding tyname name uni fun ann)
binds Term tyname name uni fun ann
term ->
        Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann)
    -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann c.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> (NonEmpty (Binding tyname name uni fun ann) -> m c)
-> m c
withFreshenedBindings Recursivity
r NonEmpty (Binding tyname name uni fun ann)
binds ((NonEmpty (Binding tyname name uni fun ann)
  -> m (Term tyname name uni fun ann))
 -> m (Term tyname name uni fun ann))
-> (NonEmpty (Binding tyname name uni fun ann)
    -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \NonEmpty (Binding tyname name uni fun ann)
bindsFr ->
            ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
x Recursivity
r NonEmpty (Binding tyname name uni fun ann)
bindsFr (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
    Var ann
x name
name ->
        ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var ann
x (name -> Term tyname name uni fun ann)
-> m name -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> name -> m name
forall ren unique name (m :: * -> *).
(HasRenaming ren unique, HasUnique name unique,
 MonadReader ren m) =>
name -> m name
PLC.renameNameM name
name
    TyAbs ann
x tyname
name Kind ann
kind Term tyname name uni fun ann
body ->
        tyname
-> (tyname -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
 MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName tyname
name ((tyname -> m (Term tyname name uni fun ann))
 -> m (Term tyname name uni fun ann))
-> (tyname -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \tyname
nameFr ->
            ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs ann
x tyname
nameFr Kind ann
kind (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
    LamAbs ann
x name
name Type tyname uni ann
ty Term tyname name uni fun ann
body ->
        name
-> (name -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, MonadQuote m,
 MonadReader ren m) =>
name -> (name -> m c) -> m c
PLC.withFreshenedName name
name ((name -> m (Term tyname name uni fun ann))
 -> m (Term tyname name uni fun ann))
-> (name -> m (Term tyname name uni fun ann))
-> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ \name
nameFr ->
            ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ann
x name
nameFr (Type tyname uni ann
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
    Apply ann
x Term tyname name uni fun ann
fun Term tyname name uni fun ann
arg ->
        ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply ann
x (Term tyname name uni fun ann
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
fun m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
arg
    Constant ann
x Some (ValueOf uni)
con ->
        Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant ann
x Some (ValueOf uni)
con
    Builtin ann
x fun
bi ->
        Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term tyname name uni fun ann -> m (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann -> fun -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin ann
x fun
bi
    TyInst ann
x Term tyname name uni fun ann
term Type tyname uni ann
ty ->
        ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst ann
x (Term tyname name uni fun ann
 -> Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Type tyname uni ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term m (Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
    Error ann
x Type tyname uni ann
ty ->
        ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error ann
x (Type tyname uni ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann) -> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
ty
    IWrap ann
x Type tyname uni ann
pat Type tyname uni ann
arg Term tyname name uni fun ann
term ->
        ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Type tyname uni a
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
IWrap ann
x (Type tyname uni ann
 -> Type tyname uni ann
 -> Term tyname name uni fun ann
 -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Type tyname uni ann
      -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
pat m (Type tyname uni ann
   -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni ann -> m (Type tyname uni ann)
forall ren tyname (uni :: * -> *) ann (m :: * -> *).
(HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann),
 MonadQuote m, MonadReader ren m) =>
Type tyname uni ann -> m (Type tyname uni ann)
PLC.renameTypeM Type tyname uni ann
arg m (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
    Unwrap ann
x Term tyname name uni fun ann
term ->
        ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Term tyname name uni fun a -> Term tyname name uni fun a
Unwrap ann
x (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term

-- | Rename a 'Term' in the 'ScopedRenameM' monad.
renameProgramM
    :: (MonadRename m, PLC.HasUniques (Term tyname name uni fun ann))
    => Program tyname name uni fun ann -> m (Program tyname name uni fun ann)
renameProgramM :: Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
renameProgramM (Program ann
ann Term tyname name uni fun ann
term) = ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
Program ann
ann (Term tyname name uni fun ann -> Program tyname name uni fun ann)
-> m (Term tyname name uni fun ann)
-> m (Program tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall (m :: * -> *) tyname name (uni :: * -> *) fun ann.
(MonadRename m, HasUniques (Term tyname name uni fun ann)) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term