-- | The internal module of the renamer that defines the actual algorithms,
-- but not the user-facing API.

module PlutusCore.Rename.Internal
    ( module Export
    , withFreshenedTyVarDecl
    , withFreshenedVarDecl
    , renameTypeM
    , renameTermM
    , renameProgramM
    ) where

import PlutusCore.Core
import PlutusCore.Name
import PlutusCore.Quote
import PlutusCore.Rename.Monad as Export

import Control.Monad.Reader

-- | Replace the unique in the name stored in a 'TyVarDecl' by a new unique, save the mapping
-- from the old unique to the new one and supply the updated 'TyVarDecl' to a continuation.
withFreshenedTyVarDecl
    :: (HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann), MonadQuote m, MonadReader ren m)
    => TyVarDecl tyname ann
    -> (TyVarDecl tyname ann -> m c)
    -> m c
withFreshenedTyVarDecl :: TyVarDecl tyname ann -> (TyVarDecl tyname ann -> m c) -> m c
withFreshenedTyVarDecl (TyVarDecl ann
ann tyname
name Kind ann
kind) TyVarDecl tyname ann -> m c
cont =
    tyname -> (tyname -> 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
withFreshenedName tyname
name ((tyname -> m c) -> m c) -> (tyname -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \tyname
nameFr -> TyVarDecl tyname ann -> m c
cont (TyVarDecl tyname ann -> m c) -> TyVarDecl tyname ann -> m c
forall a b. (a -> b) -> a -> b
$ ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann tyname
nameFr Kind ann
kind

-- | Replace the unique in the name stored in a 'VarDecl' by a new unique, save the mapping
-- from the old unique to the new one and supply to a continuation the computation that
-- renames the type stored in the updated 'VarDecl'.
-- The reason the continuation receives a computation rather than a pure term is that we may want
-- to bring several term and type variables in scope before renaming the types of term variables.
-- This situation arises when we want to rename a bunch of mutually recursive bindings.
withFreshenedVarDecl
    :: (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
withFreshenedVarDecl :: VarDecl tyname name uni fun ann
-> (m (VarDecl tyname name uni fun ann) -> m c) -> m c
withFreshenedVarDecl (VarDecl ann
ann name
name Type tyname uni ann
ty) m (VarDecl tyname name uni fun ann) -> m c
cont =
    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
withFreshenedName name
name ((name -> m c) -> m c) -> (name -> m c) -> m c
forall a b. (a -> b) -> a -> b
$ \name
nameFr -> m (VarDecl tyname name uni fun ann) -> m c
cont (m (VarDecl tyname name uni fun ann) -> m c)
-> m (VarDecl tyname name uni fun ann) -> m c
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
<$> 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)
renameTypeM Type tyname uni ann
ty

-- | Rename a 'Type' in the 'RenameM' monad.
renameTypeM
    :: (HasRenaming ren TypeUnique, HasUniques (Type tyname uni ann), MonadQuote m, MonadReader ren m)
    => Type tyname uni ann -> m (Type tyname uni ann)
renameTypeM :: Type tyname uni ann -> m (Type tyname uni ann)
renameTypeM (TyLam 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
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
TyLam 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)
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)
renameTypeM Type tyname uni ann
ty
renameTypeM (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
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)
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)
renameTypeM Type tyname uni ann
ty
renameTypeM (TyIFix ann
ann Type tyname uni ann
pat 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
TyIFix 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)
renameTypeM Type tyname uni ann
pat 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)
renameTypeM Type tyname uni ann
arg
renameTypeM (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)
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)
renameTypeM 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)
renameTypeM Type tyname uni ann
arg
renameTypeM (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)
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)
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)
renameTypeM Type tyname uni ann
cod
renameTypeM (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
<$> tyname -> m tyname
forall ren unique name (m :: * -> *).
(HasRenaming ren unique, HasUnique name unique,
 MonadReader ren m) =>
name -> m name
renameNameM tyname
name
renameTypeM ty :: Type tyname uni ann
ty@TyBuiltin{}              = Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni ann
ty

-- | Rename a 'Term' in the 'RenameM' monad.
renameTermM
    :: (HasUniques (Term tyname name uni fun ann), MonadQuote m, MonadReader ScopedRenaming m)
    => 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 (LamAbs ann
ann 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
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 ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs ann
ann 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)
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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
renameTermM (TyAbs ann
ann 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
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 ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs ann
ann 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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
body
renameTermM (IWrap ann
ann 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 ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ann
ann (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)
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)
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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
renameTermM (Apply ann
ann 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 ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply ann
ann (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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
arg
renameTermM (Unwrap ann
ann 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 ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap ann
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)
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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term
renameTermM (Error ann
ann Type tyname uni ann
ty)             = ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error ann
ann (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)
renameTypeM Type tyname uni ann
ty
renameTermM (TyInst ann
ann 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 ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst ann
ann (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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
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)
renameTypeM Type tyname uni ann
ty
renameTermM (Var ann
ann name
name)             = ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var ann
ann (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
renameNameM name
name
renameTermM con :: Term tyname name uni fun ann
con@Constant{}             = 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
con
renameTermM bi :: Term tyname name uni fun ann
bi@Builtin{}               = 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
bi

-- | Rename a 'Program' in the 'RenameM' monad.
renameProgramM
    :: (HasUniques (Program tyname name uni fun ann), MonadQuote m, MonadReader ScopedRenaming m)
    => 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 Version ann
ver Term tyname name uni fun ann
term) = ann
-> Version ann
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version ann
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program ann
ann Version ann
ver (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 tyname name (uni :: * -> *) fun ann (m :: * -> *).
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
renameTermM Term tyname name uni fun ann
term