{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module PlutusCore.Quote
( runQuoteT
, runQuote
, freshUnique
, freshName
, freshTyName
, freshenName
, freshenTyName
, QuoteT (..)
, Quote
, MonadQuote
, FreshState
, liftQuote
, markNonFreshBelow
, markNonFresh
, markNonFreshMax
) where
import PlutusPrelude (fromMaybe)
import PlutusCore.Name.Unique (Name (Name), TyName (TyName), Unique (..))
import Control.Monad.Except (ExceptT, MonadError)
import Control.Monad.Fix (MonadFix)
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Morph as MM
import Control.Monad.Reader (MonadReader, ReaderT)
import Control.Monad.State (MonadState (..), StateT, evalStateT, modify)
import Control.Monad.Trans.Maybe
import Control.Monad.Writer (MonadWriter)
import Data.Functor.Identity
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as Text
import Hedgehog (GenT, PropertyT)
type FreshState = Unique
emptyFreshState :: FreshState
emptyFreshState :: FreshState
emptyFreshState = Int -> FreshState
Unique Int
0
newtype QuoteT m a = QuoteT {forall (m :: * -> *) a. QuoteT m a -> StateT FreshState m a
unQuoteT :: StateT FreshState m a}
deriving newtype
( (forall a b. (a -> b) -> QuoteT m a -> QuoteT m b)
-> (forall a b. a -> QuoteT m b -> QuoteT m a)
-> Functor (QuoteT m)
forall a b. a -> QuoteT m b -> QuoteT m a
forall a b. (a -> b) -> QuoteT m a -> QuoteT m b
forall (m :: * -> *) a b.
Functor m =>
a -> QuoteT m b -> QuoteT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> QuoteT m a -> QuoteT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> QuoteT m a -> QuoteT m b
fmap :: forall a b. (a -> b) -> QuoteT m a -> QuoteT m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> QuoteT m b -> QuoteT m a
<$ :: forall a b. a -> QuoteT m b -> QuoteT m a
Functor
, Functor (QuoteT m)
Functor (QuoteT m) =>
(forall a. a -> QuoteT m a)
-> (forall a b. QuoteT m (a -> b) -> QuoteT m a -> QuoteT m b)
-> (forall a b c.
(a -> b -> c) -> QuoteT m a -> QuoteT m b -> QuoteT m c)
-> (forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b)
-> (forall a b. QuoteT m a -> QuoteT m b -> QuoteT m a)
-> Applicative (QuoteT m)
forall a. a -> QuoteT m a
forall a b. QuoteT m a -> QuoteT m b -> QuoteT m a
forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b
forall a b. QuoteT m (a -> b) -> QuoteT m a -> QuoteT m b
forall a b c.
(a -> b -> c) -> QuoteT m a -> QuoteT m b -> QuoteT m c
forall (m :: * -> *). Monad m => Functor (QuoteT m)
forall (m :: * -> *) a. Monad m => a -> QuoteT m a
forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m a
forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m b
forall (m :: * -> *) a b.
Monad m =>
QuoteT m (a -> b) -> QuoteT m a -> QuoteT m b
forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> QuoteT m a -> QuoteT m b -> QuoteT m 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
$cpure :: forall (m :: * -> *) a. Monad m => a -> QuoteT m a
pure :: forall a. a -> QuoteT m a
$c<*> :: forall (m :: * -> *) a b.
Monad m =>
QuoteT m (a -> b) -> QuoteT m a -> QuoteT m b
<*> :: forall a b. QuoteT m (a -> b) -> QuoteT m a -> QuoteT m b
$cliftA2 :: forall (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> QuoteT m a -> QuoteT m b -> QuoteT m c
liftA2 :: forall a b c.
(a -> b -> c) -> QuoteT m a -> QuoteT m b -> QuoteT m c
$c*> :: forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m b
*> :: forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b
$c<* :: forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m a
<* :: forall a b. QuoteT m a -> QuoteT m b -> QuoteT m a
Applicative
, Applicative (QuoteT m)
Applicative (QuoteT m) =>
(forall a b. QuoteT m a -> (a -> QuoteT m b) -> QuoteT m b)
-> (forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b)
-> (forall a. a -> QuoteT m a)
-> Monad (QuoteT m)
forall a. a -> QuoteT m a
forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b
forall a b. QuoteT m a -> (a -> QuoteT m b) -> QuoteT m b
forall (m :: * -> *). Monad m => Applicative (QuoteT m)
forall (m :: * -> *) a. Monad m => a -> QuoteT m a
forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m b
forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> (a -> QuoteT m b) -> QuoteT m 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
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> (a -> QuoteT m b) -> QuoteT m b
>>= :: forall a b. QuoteT m a -> (a -> QuoteT m b) -> QuoteT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
QuoteT m a -> QuoteT m b -> QuoteT m b
>> :: forall a b. QuoteT m a -> QuoteT m b -> QuoteT m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> QuoteT m a
return :: forall a. a -> QuoteT m a
Monad
, (forall (m :: * -> *). Monad m => Monad (QuoteT m)) =>
(forall (m :: * -> *) a. Monad m => m a -> QuoteT m a)
-> MonadTrans QuoteT
forall (m :: * -> *). Monad m => Monad (QuoteT m)
forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *). Monad m => Monad (t m)) =>
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
$clift :: forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
lift :: forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
MonadTrans
, Monad (QuoteT m)
Monad (QuoteT m) =>
(forall a. (a -> QuoteT m a) -> QuoteT m a) -> MonadFix (QuoteT m)
forall a. (a -> QuoteT m a) -> QuoteT m a
forall (m :: * -> *).
Monad m =>
(forall a. (a -> m a) -> m a) -> MonadFix m
forall (m :: * -> *). MonadFix m => Monad (QuoteT m)
forall (m :: * -> *) a.
MonadFix m =>
(a -> QuoteT m a) -> QuoteT m a
$cmfix :: forall (m :: * -> *) a.
MonadFix m =>
(a -> QuoteT m a) -> QuoteT m a
mfix :: forall a. (a -> QuoteT m a) -> QuoteT m a
MonadFix
, (forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> QuoteT m b -> QuoteT n b)
-> MFunctor QuoteT
forall {k} (t :: (* -> *) -> k -> *).
(forall (m :: * -> *) (n :: * -> *) (b :: k).
Monad m =>
(forall a. m a -> n a) -> t m b -> t n b)
-> MFunctor t
forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> QuoteT m b -> QuoteT n b
$choist :: forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> QuoteT m b -> QuoteT n b
hoist :: forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> QuoteT m b -> QuoteT n b
MM.MFunctor
, MonadError e
, MonadReader r
, Monad (QuoteT m)
Monad (QuoteT m) =>
(forall a. IO a -> QuoteT m a) -> MonadIO (QuoteT m)
forall a. IO a -> QuoteT m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (QuoteT m)
forall (m :: * -> *) a. MonadIO m => IO a -> QuoteT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> QuoteT m a
liftIO :: forall a. IO a -> QuoteT m a
MonadIO
, MonadWriter w
)
instance MonadState s m => MonadState s (QuoteT m) where
get :: QuoteT m s
get = m s -> QuoteT m s
forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: * -> *). MonadState s m => m s
get
put :: s -> QuoteT m ()
put = m () -> QuoteT m ()
forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> QuoteT m ()) -> (s -> m ()) -> s -> QuoteT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
state :: forall a. (s -> (a, s)) -> QuoteT m a
state = m a -> QuoteT m a
forall (m :: * -> *) a. Monad m => m a -> QuoteT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> QuoteT m a)
-> ((s -> (a, s)) -> m a) -> (s -> (a, s)) -> QuoteT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> m a
forall a. (s -> (a, s)) -> m a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state
class Monad m => MonadQuote m where
liftQuote :: Quote a -> m a
default liftQuote :: (MonadQuote n, MonadTrans t, t n ~ m) => Quote a -> m a
liftQuote = n a -> m a
n a -> t n a
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n a -> m a) -> (Quote a -> n a) -> Quote a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quote a -> n a
forall a. Quote a -> n a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote
instance (Monad m) => MonadQuote (QuoteT m) where
liftQuote :: forall a. Quote a -> QuoteT m a
liftQuote = (forall a. Identity a -> m a) -> QuoteT Identity a -> QuoteT m a
forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
(b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
forall (m :: * -> *) (n :: * -> *) b.
Monad m =>
(forall a. m a -> n a) -> QuoteT m b -> QuoteT n b
MM.hoist (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> m a) -> (Identity a -> a) -> Identity a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> a
forall a. Identity a -> a
runIdentity)
instance MonadQuote m => MonadQuote (StateT s m)
instance MonadQuote m => MonadQuote (MaybeT m)
instance MonadQuote m => MonadQuote (ExceptT e m)
instance MonadQuote m => MonadQuote (ReaderT r m)
instance MonadQuote m => MonadQuote (GenT m)
instance MonadQuote m => MonadQuote (PropertyT m)
runQuoteT :: Monad m => QuoteT m a -> m a
runQuoteT :: forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT QuoteT m a
q = StateT FreshState m a -> FreshState -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (QuoteT m a -> StateT FreshState m a
forall (m :: * -> *) a. QuoteT m a -> StateT FreshState m a
unQuoteT QuoteT m a
q) FreshState
emptyFreshState
type Quote = QuoteT Identity
runQuote :: Quote a -> a
runQuote :: forall a. Quote a -> a
runQuote = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (Quote a -> Identity a) -> Quote a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Quote a -> Identity a
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT
freshUnique :: MonadQuote m => m Unique
freshUnique :: forall (m :: * -> *). MonadQuote m => m FreshState
freshUnique = Quote FreshState -> m FreshState
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote FreshState -> m FreshState)
-> Quote FreshState -> m FreshState
forall a b. (a -> b) -> a -> b
$ do
FreshState
nextU <- StateT FreshState Identity FreshState -> Quote FreshState
forall (m :: * -> *) a. StateT FreshState m a -> QuoteT m a
QuoteT StateT FreshState Identity FreshState
forall s (m :: * -> *). MonadState s m => m s
get
StateT FreshState Identity () -> QuoteT Identity ()
forall (m :: * -> *) a. StateT FreshState m a -> QuoteT m a
QuoteT (StateT FreshState Identity () -> QuoteT Identity ())
-> StateT FreshState Identity () -> QuoteT Identity ()
forall a b. (a -> b) -> a -> b
$ FreshState -> StateT FreshState Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (FreshState -> StateT FreshState Identity ())
-> FreshState -> StateT FreshState Identity ()
forall a b. (a -> b) -> a -> b
$ Int -> FreshState
Unique (FreshState -> Int
unUnique FreshState
nextU Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
FreshState -> Quote FreshState
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FreshState
nextU
freshName :: MonadQuote m => Text.Text -> m Name
freshName :: forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
str = Text -> FreshState -> Name
Name Text
str (FreshState -> Name) -> m FreshState -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m FreshState
forall (m :: * -> *). MonadQuote m => m FreshState
freshUnique
freshenName :: MonadQuote m => Name -> m Name
freshenName :: forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName (Name Text
str FreshState
_) = Text -> FreshState -> Name
Name Text
str (FreshState -> Name) -> m FreshState -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m FreshState
forall (m :: * -> *). MonadQuote m => m FreshState
freshUnique
freshTyName :: MonadQuote m => Text.Text -> m TyName
freshTyName :: forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName = (Name -> TyName) -> m Name -> m TyName
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> TyName
TyName (m Name -> m TyName) -> (Text -> m Name) -> Text -> m TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName
freshenTyName :: MonadQuote m => TyName -> m TyName
freshenTyName :: forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName (TyName Name
name) = Name -> TyName
TyName (Name -> TyName) -> m Name -> m TyName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> m Name
forall (m :: * -> *). MonadQuote m => Name -> m Name
freshenName Name
name
markNonFreshBelow :: MonadQuote m => Unique -> m ()
markNonFreshBelow :: forall (m :: * -> *). MonadQuote m => FreshState -> m ()
markNonFreshBelow = QuoteT Identity () -> m ()
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity () -> m ())
-> (FreshState -> QuoteT Identity ()) -> FreshState -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT FreshState Identity () -> QuoteT Identity ()
forall (m :: * -> *) a. StateT FreshState m a -> QuoteT m a
QuoteT (StateT FreshState Identity () -> QuoteT Identity ())
-> (FreshState -> StateT FreshState Identity ())
-> FreshState
-> QuoteT Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FreshState -> FreshState) -> StateT FreshState Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((FreshState -> FreshState) -> StateT FreshState Identity ())
-> (FreshState -> FreshState -> FreshState)
-> FreshState
-> StateT FreshState Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshState -> FreshState -> FreshState
forall a. Ord a => a -> a -> a
max
markNonFresh :: MonadQuote m => Unique -> m ()
markNonFresh :: forall (m :: * -> *). MonadQuote m => FreshState -> m ()
markNonFresh = FreshState -> m ()
forall (m :: * -> *). MonadQuote m => FreshState -> m ()
markNonFreshBelow (FreshState -> m ())
-> (FreshState -> FreshState) -> FreshState -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshState -> FreshState
forall a. Enum a => a -> a
succ
markNonFreshMax :: MonadQuote m => Set Unique -> m ()
markNonFreshMax :: forall (m :: * -> *). MonadQuote m => Set FreshState -> m ()
markNonFreshMax = FreshState -> m ()
forall (m :: * -> *). MonadQuote m => FreshState -> m ()
markNonFresh (FreshState -> m ())
-> (Set FreshState -> FreshState) -> Set FreshState -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreshState -> Maybe FreshState -> FreshState
forall a. a -> Maybe a -> a
fromMaybe (Int -> FreshState
Unique Int
0) (Maybe FreshState -> FreshState)
-> (Set FreshState -> Maybe FreshState)
-> Set FreshState
-> FreshState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FreshState -> Maybe FreshState
forall a. Set a -> Maybe a
Set.lookupMax