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

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

module PlutusCore.Rename
    ( Rename (..)
    , Dupable
    , liftDupable
    ) where

import PlutusPrelude

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

import Data.Functor.Identity

{- 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

instance HasUniques (Type tyname uni ann) => Rename (Type tyname uni ann) where
    -- See Note [Marking].
    rename :: 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
forall (m :: * -> *) a.
Monoid TypeRenaming =>
RenameT TypeRenaming 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 :: 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 :: 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 :: 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)
traverse a -> m a
forall a (m :: * -> *). (Rename a, MonadQuote m) => a -> m a
rename

-- | @Dupable a@ is isomorphic to @a@, but the only way to extract the @a@ is via 'liftDupable'
-- 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 conditions is preserved.
newtype Dupable a = Dupable
    { 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
showList :: [Dupable a] -> ShowS
$cshowList :: forall a. Show a => [Dupable a] -> ShowS
show :: Dupable a -> String
$cshow :: forall a. Show a => Dupable a -> String
showsPrec :: Int -> Dupable a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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
/= :: Dupable a -> Dupable a -> Bool
$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
Eq, a -> Dupable b -> Dupable a
(a -> b) -> Dupable a -> Dupable b
(forall a b. (a -> b) -> Dupable a -> Dupable b)
-> (forall a b. a -> Dupable b -> Dupable a) -> Functor Dupable
forall a b. a -> Dupable b -> Dupable a
forall a b. (a -> b) -> Dupable a -> Dupable b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Dupable b -> Dupable a
$c<$ :: forall a b. a -> Dupable b -> Dupable a
fmap :: (a -> b) -> Dupable a -> Dupable b
$cfmap :: forall a b. (a -> b) -> Dupable a -> Dupable b
Functor, Dupable a -> Bool
(a -> m) -> Dupable a -> m
(a -> b -> b) -> b -> Dupable a -> b
(forall m. Monoid m => Dupable m -> m)
-> (forall m a. Monoid m => (a -> m) -> Dupable a -> m)
-> (forall m a. Monoid m => (a -> m) -> Dupable a -> m)
-> (forall a b. (a -> b -> b) -> b -> Dupable a -> b)
-> (forall a b. (a -> b -> b) -> b -> Dupable a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dupable a -> b)
-> (forall b a. (b -> a -> b) -> b -> Dupable a -> b)
-> (forall a. (a -> a -> a) -> Dupable a -> a)
-> (forall a. (a -> a -> a) -> Dupable a -> a)
-> (forall a. Dupable a -> [a])
-> (forall a. Dupable a -> Bool)
-> (forall a. Dupable a -> Int)
-> (forall a. Eq a => a -> Dupable a -> Bool)
-> (forall a. Ord a => Dupable a -> a)
-> (forall a. Ord a => Dupable a -> a)
-> (forall a. Num a => Dupable a -> a)
-> (forall a. Num a => Dupable a -> a)
-> Foldable Dupable
forall a. Eq a => a -> Dupable a -> Bool
forall a. Num a => Dupable a -> a
forall a. Ord a => Dupable a -> a
forall m. Monoid m => Dupable m -> m
forall a. Dupable a -> Bool
forall a. Dupable a -> Int
forall a. Dupable a -> [a]
forall a. (a -> a -> a) -> Dupable a -> a
forall m a. Monoid m => (a -> m) -> Dupable a -> m
forall b a. (b -> a -> b) -> b -> Dupable a -> b
forall a b. (a -> b -> b) -> b -> Dupable a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: Dupable a -> a
$cproduct :: forall a. Num a => Dupable a -> a
sum :: Dupable a -> a
$csum :: forall a. Num a => Dupable a -> a
minimum :: Dupable a -> a
$cminimum :: forall a. Ord a => Dupable a -> a
maximum :: Dupable a -> a
$cmaximum :: forall a. Ord a => Dupable a -> a
elem :: a -> Dupable a -> Bool
$celem :: forall a. Eq a => a -> Dupable a -> Bool
length :: Dupable a -> Int
$clength :: forall a. Dupable a -> Int
null :: Dupable a -> Bool
$cnull :: forall a. Dupable a -> Bool
toList :: Dupable a -> [a]
$ctoList :: forall a. Dupable a -> [a]
foldl1 :: (a -> a -> a) -> Dupable a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Dupable a -> a
foldr1 :: (a -> a -> a) -> Dupable a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Dupable a -> a
foldl' :: (b -> a -> b) -> b -> Dupable a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Dupable a -> b
foldl :: (b -> a -> b) -> b -> Dupable a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Dupable a -> b
foldr' :: (a -> b -> b) -> b -> Dupable a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Dupable a -> b
foldr :: (a -> b -> b) -> b -> Dupable a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Dupable a -> b
foldMap' :: (a -> m) -> Dupable a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Dupable a -> m
foldMap :: (a -> m) -> Dupable a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Dupable a -> m
fold :: Dupable m -> m
$cfold :: forall m. Monoid m => Dupable m -> m
Foldable, Functor Dupable
Foldable Dupable
Functor Dupable
-> Foldable Dupable
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Dupable a -> f (Dupable b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Dupable (f a) -> f (Dupable a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Dupable a -> m (Dupable b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Dupable (m a) -> m (Dupable a))
-> Traversable Dupable
(a -> f b) -> Dupable a -> f (Dupable b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Dupable (m a) -> m (Dupable a)
forall (f :: * -> *) a.
Applicative f =>
Dupable (f a) -> f (Dupable a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dupable a -> m (Dupable b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dupable a -> f (Dupable b)
sequence :: Dupable (m a) -> m (Dupable a)
$csequence :: forall (m :: * -> *) a. Monad m => Dupable (m a) -> m (Dupable a)
mapM :: (a -> m b) -> Dupable a -> m (Dupable b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Dupable a -> m (Dupable b)
sequenceA :: Dupable (f a) -> f (Dupable a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Dupable (f a) -> f (Dupable a)
traverse :: (a -> f b) -> Dupable a -> f (Dupable b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dupable a -> f (Dupable b)
$cp2Traversable :: Foldable Dupable
$cp1Traversable :: Functor Dupable
Traversable)
      deriving (Functor Dupable
a -> Dupable a
Functor Dupable
-> (forall a. a -> Dupable a)
-> (forall a b. Dupable (a -> b) -> Dupable a -> Dupable b)
-> (forall a b c.
    (a -> b -> c) -> Dupable a -> Dupable b -> Dupable c)
-> (forall a b. Dupable a -> Dupable b -> Dupable b)
-> (forall a b. Dupable a -> Dupable b -> Dupable a)
-> Applicative Dupable
Dupable a -> Dupable b -> Dupable b
Dupable a -> Dupable b -> Dupable a
Dupable (a -> b) -> Dupable a -> Dupable b
(a -> b -> c) -> Dupable a -> Dupable b -> Dupable c
forall a. a -> Dupable a
forall a b. Dupable a -> Dupable b -> Dupable a
forall a b. Dupable a -> Dupable b -> Dupable b
forall a b. Dupable (a -> b) -> Dupable a -> Dupable b
forall a b c. (a -> b -> c) -> Dupable a -> Dupable b -> Dupable c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Dupable a -> Dupable b -> Dupable a
$c<* :: forall a b. Dupable a -> Dupable b -> Dupable a
*> :: Dupable a -> Dupable b -> Dupable b
$c*> :: forall a b. Dupable a -> Dupable b -> Dupable b
liftA2 :: (a -> b -> c) -> Dupable a -> Dupable b -> Dupable c
$cliftA2 :: forall a b c. (a -> b -> c) -> Dupable a -> Dupable b -> Dupable c
<*> :: Dupable (a -> b) -> Dupable a -> Dupable b
$c<*> :: forall a b. Dupable (a -> b) -> Dupable a -> Dupable b
pure :: a -> Dupable a
$cpure :: forall a. a -> Dupable a
$cp1Applicative :: Functor Dupable
Applicative, Applicative Dupable
a -> Dupable a
Applicative Dupable
-> (forall a b. Dupable a -> (a -> Dupable b) -> Dupable b)
-> (forall a b. Dupable a -> Dupable b -> Dupable b)
-> (forall a. a -> Dupable a)
-> Monad Dupable
Dupable a -> (a -> Dupable b) -> Dupable b
Dupable a -> Dupable b -> Dupable b
forall a. a -> Dupable a
forall a b. Dupable a -> Dupable b -> Dupable b
forall a b. Dupable a -> (a -> Dupable b) -> Dupable b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Dupable a
$creturn :: forall a. a -> Dupable a
>> :: Dupable a -> Dupable b -> Dupable b
$c>> :: forall a b. Dupable a -> Dupable b -> Dupable b
>>= :: Dupable a -> (a -> Dupable b) -> Dupable b
$c>>= :: forall a b. Dupable a -> (a -> Dupable b) -> Dupable b
$cp1Monad :: Applicative Dupable
Monad) via Identity

-- | Extract the value stored in a @Dupable a@ and rename it.
liftDupable :: (MonadQuote m, Rename a) => Dupable a -> m a
liftDupable :: Dupable a -> m a
liftDupable = 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
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