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

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

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

import Control.Monad.Reader

-- | A wrapper for signifying that the value inside of it satisfies global uniqueness.
--
-- It's safe to call 'unRenamed', it's not safe to call 'Renamed', hence the latter is only exported
-- from this internal module and should not be exported from the main API.
--
-- Don't provide any instances allowing the user to create a 'Renamed' (even out of an existing one
-- like with 'Functor').
newtype Renamed a = Renamed
    { forall a. Renamed a -> a
unRenamed :: a
    } deriving stock (Int -> Renamed a -> ShowS
[Renamed a] -> ShowS
Renamed a -> String
(Int -> Renamed a -> ShowS)
-> (Renamed a -> String)
-> ([Renamed a] -> ShowS)
-> Show (Renamed a)
forall a. Show a => Int -> Renamed a -> ShowS
forall a. Show a => [Renamed a] -> ShowS
forall a. Show a => Renamed a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Renamed a -> ShowS
showsPrec :: Int -> Renamed a -> ShowS
$cshow :: forall a. Show a => Renamed a -> String
show :: Renamed a -> String
$cshowList :: forall a. Show a => [Renamed a] -> ShowS
showList :: [Renamed a] -> ShowS
Show, Renamed a -> Renamed a -> Bool
(Renamed a -> Renamed a -> Bool)
-> (Renamed a -> Renamed a -> Bool) -> Eq (Renamed a)
forall a. Eq a => Renamed a -> Renamed a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Renamed a -> Renamed a -> Bool
== :: Renamed a -> Renamed a -> Bool
$c/= :: forall a. Eq a => Renamed a -> Renamed a -> Bool
/= :: Renamed a -> Renamed a -> Bool
Eq)

-- | @Dupable a@ is isomorphic to @a@, but the only way to extract the @a@ is via 'liftDupable'
-- (defined in the main API module because of a constraint requirement) which renames the stored
-- value along the way. This type is used whenever
--
-- 1. preserving global uniqueness is required
-- 2. some value may be used multiple times
--
-- so we annotate such a value with 'Dupable' and call 'liftDupable' at each usage, which ensures
-- global uniqueness is preserved.
--
-- 'unDupable' is not supposed to be exported. Don't provide any instances allowing the user to
-- access the underlying value.
newtype Dupable a = Dupable
    { forall a. Dupable a -> a
unDupable :: a
    } deriving stock (Int -> Dupable a -> ShowS
[Dupable a] -> ShowS
Dupable a -> String
(Int -> Dupable a -> ShowS)
-> (Dupable a -> String)
-> ([Dupable a] -> ShowS)
-> Show (Dupable a)
forall a. Show a => Int -> Dupable a -> ShowS
forall a. Show a => [Dupable a] -> ShowS
forall a. Show a => Dupable a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Dupable a -> ShowS
showsPrec :: Int -> Dupable a -> ShowS
$cshow :: forall a. Show a => Dupable a -> String
show :: Dupable a -> String
$cshowList :: forall a. Show a => [Dupable a] -> ShowS
showList :: [Dupable a] -> ShowS
Show, Dupable a -> Dupable a -> Bool
(Dupable a -> Dupable a -> Bool)
-> (Dupable a -> Dupable a -> Bool) -> Eq (Dupable a)
forall a. Eq a => Dupable a -> Dupable a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Dupable a -> Dupable a -> Bool
== :: Dupable a -> Dupable a -> Bool
$c/= :: forall a. Eq a => Dupable a -> Dupable a -> Bool
/= :: Dupable a -> Dupable a -> Bool
Eq)

-- | 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 :: 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
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 ann
    -> (m (VarDecl tyname name uni ann) -> m c)
    -> m c
withFreshenedVarDecl :: forall tyname name (uni :: * -> *) fun ann (m :: * -> *) c.
(HasUniques (Term tyname name uni fun ann), MonadQuote m,
 MonadReader ScopedRenaming m) =>
VarDecl tyname name uni ann
-> (m (VarDecl tyname name uni ann) -> m c) -> m c
withFreshenedVarDecl (VarDecl ann
ann name
name Type tyname uni ann
ty) m (VarDecl tyname name uni 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 ann) -> m c
cont (m (VarDecl tyname name uni ann) -> m c)
-> m (VarDecl tyname name uni ann) -> m c
forall a b. (a -> b) -> a -> b
$ ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann name
nameFr (Type tyname uni ann -> VarDecl tyname name uni ann)
-> m (Type tyname uni ann) -> m (VarDecl tyname name 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

-- | 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 :: 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 (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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 (TySOP ann
ann [[Type tyname uni ann]]
tyls)            = ann -> [[Type tyname uni ann]] -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann ([[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])
-> [[Type tyname uni ann]] -> m [[Type tyname uni ann]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (([Type tyname uni ann] -> m [Type tyname uni ann])
 -> [[Type tyname uni ann]] -> m [[Type tyname uni ann]])
-> ((Type tyname uni ann -> m (Type tyname uni ann))
    -> [Type tyname uni ann] -> m [Type tyname uni ann])
-> (Type tyname uni ann -> m (Type tyname uni ann))
-> [[Type tyname uni ann]]
-> m [[Type tyname uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> m (Type tyname uni ann))
-> [Type tyname uni ann] -> m [Type tyname uni ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) 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]]
tyls
renameTypeM ty :: Type tyname uni ann
ty@TyBuiltin{}              = Type tyname uni ann -> m (Type tyname uni ann)
forall a. a -> m a
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 :: 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 (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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 a b. m (a -> b) -> m a -> m b
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 (Constr ann
ann Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es)       = ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr ann
ann (Type tyname uni ann
 -> Word64
 -> [Term tyname name uni fun ann]
 -> Term tyname name uni fun ann)
-> m (Type tyname uni ann)
-> m (Word64
      -> [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 (Word64
   -> [Term tyname name uni fun ann] -> Term tyname name uni fun ann)
-> m Word64
-> m ([Term tyname name uni fun ann]
      -> Term tyname name uni fun ann)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Word64 -> m Word64
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
i 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 a b. m (a -> b) -> m a -> m b
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))
-> [Term tyname name uni fun ann]
-> m [Term tyname name uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse 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]
es
renameTermM (Case ann
ann Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs)       = ann
-> Type tyname uni 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
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case ann
ann (Type tyname uni ann
 -> Term tyname name uni fun 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] -> 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] -> 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 a b. m (a -> b) -> m a -> m b
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 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 a b. m (a -> b) -> m a -> m b
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))
-> [Term tyname name uni fun ann]
-> m [Term tyname name uni fun ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse 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]
cs
renameTermM con :: Term tyname name uni fun ann
con@Constant{}             = Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
forall a. a -> m a
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 a. a -> m a
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 :: forall tyname name (uni :: * -> *) fun ann (m :: * -> *).
(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 ann
ann Version
ver Term tyname name uni fun ann
term) = ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program ann
ann Version
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