-- | The user-facing API of the renamer.

{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE UndecidableInstances #-}

module PlutusCore.Rename
    ( Renamed (unRenamed)
    , Rename (..)
    , getRenamed
    , Dupable
    , dupable
    , liftDupable
    ) where

import PlutusPrelude

import PlutusCore.Core
import PlutusCore.Mark
import PlutusCore.Name.Unique
import PlutusCore.Quote
import PlutusCore.Rename.Internal

{- Note [Marking]
We use functions from the @markNonFresh*@ family in order to ensure that bound variables never get
renamed to free ones. This means types/terms/etc are processed twice: once by a @markNonFresh*@
function and once for the actual renaming. We may consider later to do some kind of meta-circular
programming trick in order to perform renaming in a single pass.
-}

-- | The class of things that can be renamed.
-- I.e. things that are capable of satisfying the global uniqueness condition.
class Rename a where
    -- | Rename 'Unique's so that they're globally unique.
    -- In case there are any free variables, they must be left untouched and bound variables
    -- must not get renamed to free ones.
    -- Must always assign new names to bound variables,
    -- so that @rename@ can be used for alpha-renaming as well.
    rename :: MonadQuote m => a -> m a

-- | 'rename' a value and wrap the result in 'Renamed', so that it can be passed around and it's
-- visible in the types that the thing inside satisfies global uniqueness.
getRenamed :: (Rename a, MonadQuote m) => a -> m (Renamed a)
getRenamed :: forall a (m :: * -> *).
(Rename a, MonadQuote m) =>
a -> m (Renamed a)
getRenamed = (a -> Renamed a) -> m a -> m (Renamed a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Renamed a
forall a. a -> Renamed a
Renamed (m a -> m (Renamed a)) -> (a -> m a) -> a -> m (Renamed a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *). MonadQuote m => a -> m a
rename

-- | Wrap a value in 'Dupable'.
dupable :: a -> Dupable a
dupable :: forall a. a -> Dupable a
dupable = a -> Dupable a
forall a. a -> Dupable a
Dupable

-- | Extract the value stored in a @Dupable a@ and rename it.
liftDupable :: (MonadQuote m, Rename a) => Dupable a -> m a
liftDupable :: forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable = Quote a -> m a
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote a -> m a) -> (Dupable a -> Quote a) -> Dupable a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Quote a
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *). MonadQuote m => a -> m a
rename (a -> Quote a) -> (Dupable a -> a) -> Dupable a -> Quote a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dupable a -> a
forall a. Dupable a -> a
unDupable

instance HasUniques (Type tyname uni ann) => Rename (Type tyname uni ann) where
    -- See Note [Marking].
    rename :: forall (m :: * -> *).
MonadQuote m =>
Type tyname uni ann -> m (Type tyname uni ann)
rename = (Type tyname uni ann -> m ())
-> Type tyname uni ann -> m (Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Type tyname uni ann -> m ()
forall tyname (uni :: * -> *) ann (m :: * -> *).
(HasUniques (Type tyname uni ann), MonadQuote m) =>
Type tyname uni ann -> m ()
markNonFreshType (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 (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall ren (m :: * -> *) a. Monoid ren => RenameT ren m a -> m a
runRenameT @TypeRenaming (RenameT TypeRenaming m (Type tyname uni ann)
 -> m (Type tyname uni ann))
-> (Type tyname uni ann
    -> RenameT TypeRenaming 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 -> RenameT TypeRenaming 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

instance HasUniques (Term tyname name uni fun ann) => Rename (Term tyname name uni fun ann) where
    -- See Note [Marking].
    rename :: forall (m :: * -> *).
MonadQuote m =>
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
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 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

instance HasUniques (Program tyname name uni fun ann) =>
    Rename (Program tyname name uni fun ann) where
    -- See Note [Marking].
    rename :: forall (m :: * -> *).
MonadQuote m =>
Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
rename = (Program tyname name uni fun ann -> m ())
-> Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> f b) -> a -> f a
through Program tyname name uni fun ann -> m ()
forall tyname name (m :: * -> *) (uni :: * -> *) fun ann.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
 MonadQuote m) =>
Program tyname name uni fun ann -> m ()
markNonFreshProgram (Program tyname name uni fun ann
 -> m (Program tyname name uni fun ann))
-> (Program tyname name uni fun ann
    -> m (Program tyname name uni fun ann))
-> Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> RenameT ScopedRenaming m (Program tyname name uni fun ann)
-> m (Program tyname name uni fun ann)
forall ren (m :: * -> *) a. Monoid ren => RenameT ren m a -> m a
runRenameT (RenameT ScopedRenaming m (Program tyname name uni fun ann)
 -> m (Program tyname name uni fun ann))
-> (Program tyname name uni fun ann
    -> RenameT ScopedRenaming m (Program tyname name uni fun ann))
-> Program tyname name uni fun ann
-> m (Program tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program tyname name uni fun ann
-> RenameT ScopedRenaming m (Program tyname name uni fun ann)
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

instance Rename a => Rename (Normalized a) where
    rename :: forall (m :: * -> *).
MonadQuote m =>
Normalized a -> m (Normalized a)
rename = (a -> m a) -> Normalized a -> m (Normalized a)
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) -> Normalized a -> f (Normalized b)
traverse a -> m a
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
forall (m :: * -> *). MonadQuote m => a -> m a
rename