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

-- | The user-facing API of the renamer.
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