Skip to content

Commit

Permalink
Merge pull request #4230 from effectfully/effectfully/builtins/simpli…
Browse files Browse the repository at this point in the history
…fy-emitter

[Builtins] Simplify 'Emitter'
  • Loading branch information
michaelpj authored Nov 22, 2021
2 parents 57f9020 + 82c9c82 commit e995df9
Show file tree
Hide file tree
Showing 8 changed files with 36 additions and 79 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ instance KnownTypeAst DefaultUni Void where
a <- freshTyName "a"
pure $ TyForall () a (Type ()) $ TyVar () a
instance UniOf term ~ DefaultUni => KnownTypeIn DefaultUni term Void where
makeKnown _ = absurd
makeKnown _ _ = absurd
readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift a 'Void'" mayCause

data BuiltinErrorCall = BuiltinErrorCall
Expand Down
66 changes: 12 additions & 54 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Dynamic/Emit.hs
Original file line number Diff line number Diff line change
@@ -1,69 +1,27 @@
{-# LANGUAGE RankNTypes #-}

module PlutusCore.Constant.Dynamic.Emit
( MonadEmitter (..)
, Emitter (..)
, NoEmitterT (..)
, WithEmitterT (..)
( Emitter (..)
, emitM
) where

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Identity
import Data.Text (Text)

-- | A class for emitting 'Text's in a monadic context (basically, for logging).
class Monad m => MonadEmitter m where
emit :: Text -> m ()

-- | A concrete type implementing 'MonadEmitter'. Useful in signatures of built-in functions that
-- do logging. We don't use any concrete first-order encoding and instead pack a @MonadEmitter m@
-- constraint internally, so that built-in functions that do logging can work in any monad
-- implementing 'MonadEmitter' (for example, @CkM@ or @CekM@).
-- | A monad for logging that does not hardcode any concrete first-order encoding and instead packs
-- a @Monad m@ constraint and a @Text -> m ()@ argument internally, so that built-in functions that
-- do logging can work in any monad (for example, @CkM@ or @CekM@), for which there exists a
-- logging function.
newtype Emitter a = Emitter
{ unEmitter :: forall m. MonadEmitter m => m a
{ unEmitter :: forall m. Monad m => (Text -> m ()) -> m a
} deriving (Functor)

-- newtype-deriving doesn't work with 'Emitter'.
instance Applicative Emitter where
pure x = Emitter $ pure x
Emitter f <*> Emitter a = Emitter $ f <*> a
pure x = Emitter $ \_ -> pure x
Emitter f <*> Emitter a = Emitter $ \emit -> f emit <*> a emit

instance Monad Emitter where
Emitter a >>= f = Emitter $ a >>= unEmitter . f

instance MonadEmitter Emitter where
emit str = Emitter $ emit str

-- | A newtype wrapper for providing a 'MonadEmitter' instance by directly providing the function.
newtype WithEmitterT m a = WithEmitterT
{ unWithEmitterT :: (Text -> m ()) -> m a
} deriving
( Functor, Applicative, Monad
, MonadError e, MonadState s
)
via
ReaderT (Text -> m ()) m

instance Monad m => MonadEmitter (WithEmitterT m) where
emit s = WithEmitterT $ \e -> e s

instance MonadTrans WithEmitterT where
lift a = WithEmitterT $ const a

-- | A newtype wrapper for via-deriving a vacuous 'MonadEmitter' instance for a monad.
newtype NoEmitterT m a = NoEmitterT
{ unNoEmitterT :: m a
} deriving
( Functor, Applicative, Monad
, MonadReader r, MonadError e, MonadState s
)
via
IdentityT m

instance Monad m => MonadEmitter (NoEmitterT m) where
emit _ = pure ()
Emitter a >>= f = Emitter $ \emit -> a emit >>= \x -> unEmitter (f x) emit

instance (MonadEmitter m) => MonadEmitter (ExceptT e m) where
emit = lift . emit
emitM :: Text -> Emitter ()
emitM text = Emitter ($ text)
23 changes: 12 additions & 11 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ import Data.Proxy
import Data.SOP.Constraint
import Data.Some.GADT qualified as GADT
import Data.String
import Data.Text (Text)
import Data.Text qualified as Text
import GHC.Ix
import GHC.TypeLits
Expand Down Expand Up @@ -533,18 +534,18 @@ class (uni ~ UniOf term, KnownTypeAst uni a) => KnownTypeIn uni term a where
-- | Convert a Haskell value to the corresponding PLC term.
-- The inverse of 'readKnown'.
makeKnown
:: ( MonadEmitter m, MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err
:: ( MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err
)
=> Maybe cause -> a -> m term
=> (Text -> m ()) -> Maybe cause -> a -> m term
default makeKnown
:: ( MonadError (ErrorWithCause err cause) m
, KnownBuiltinType term a
)
=> Maybe cause -> a -> m term
=> (Text -> m ()) -> Maybe cause -> a -> m term
-- Forcing the value to avoid space leaks. Note that the value is only forced to WHNF,
-- so care must be taken to ensure that every value of a type from the universe gets forced
-- to NF whenever it's forced to WHNF.
makeKnown _ x = pure . fromConstant . someValue $! x
makeKnown _ _ x = pure . fromConstant . someValue $! x

-- | Convert a PLC term to the corresponding Haskell value.
-- The inverse of 'makeKnown'.
Expand Down Expand Up @@ -607,7 +608,7 @@ instance (MonadError err m, AsEvaluationFailure err) =>
-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
-- For example the monad can be simply 'EvaluationResult'.
makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err) => a -> m term
makeKnownOrFail = unNoCauseT . unNoEmitterT . makeKnown Nothing
makeKnownOrFail = unNoCauseT . makeKnown (\_ -> pure ()) Nothing

instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where
type ToBinds (EvaluationResult a) = ToBinds a
Expand All @@ -616,8 +617,8 @@ instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where

instance (KnownTypeAst uni a, KnownTypeIn uni term a) =>
KnownTypeIn uni term (EvaluationResult a) where
makeKnown mayCause EvaluationFailure = throwingWithCause _EvaluationFailure () mayCause
makeKnown mayCause (EvaluationSuccess x) = makeKnown mayCause x
makeKnown _ mayCause EvaluationFailure = throwingWithCause _EvaluationFailure () mayCause
makeKnown emit mayCause (EvaluationSuccess x) = makeKnown emit mayCause x

-- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
-- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function
Expand All @@ -634,7 +635,7 @@ instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where
toTypeAst _ = toTypeAst $ Proxy @a

instance KnownTypeIn uni term a => KnownTypeIn uni term (Emitter a) where
makeKnown mayCause = unEmitter >=> makeKnown mayCause
makeKnown emit mayCause (Emitter k) = k emit >>= makeKnown emit mayCause
-- TODO: we really should tear 'KnownType' apart into two separate type classes.
readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift an 'Emitter'" mayCause

Expand All @@ -654,7 +655,7 @@ instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant un

instance (HasConstantIn uni term, KnownTypeAst uni rep) =>
KnownTypeIn uni term (SomeConstant uni rep) where
makeKnown _ = pure . fromConstant . unSomeConstant
makeKnown _ _ = pure . fromConstant . unSomeConstant
readKnown mayCause = fmap SomeConstant . asConstant mayCause

-- | For unlifting from the 'Constant' constructor when the stored value is of a polymorphic
Expand All @@ -680,7 +681,7 @@ instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) =>
instance ( uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps
, HasConstantIn uni term
) => KnownTypeIn uni term (SomeConstantPoly uni f reps) where
makeKnown _ = pure . fromConstant . unSomeConstantPoly
makeKnown _ _ = pure . fromConstant . unSomeConstantPoly
readKnown mayCause = fmap SomeConstantPoly . asConstant mayCause

toTyNameAst
Expand Down Expand Up @@ -721,7 +722,7 @@ instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where

instance (term ~ term', uni ~ UniOf term, KnownTypeAst uni rep) =>
KnownTypeIn uni term (Opaque term' rep) where
makeKnown _ = pure . unOpaque
makeKnown _ _ = pure . unOpaque
readKnown _ = pure . Opaque

-- Custom type errors to guide the programmer adding a new built-in function.
Expand Down
2 changes: 1 addition & 1 deletion plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
-- Tracing
toBuiltinMeaning Trace =
makeBuiltinMeaning
(\text a -> a <$ emit @Emitter text)
(\text a -> a <$ emitM text)
(runCostingFunTwoArguments . paramTrace)
-- Pairs
toBuiltinMeaning FstPair =
Expand Down
2 changes: 1 addition & 1 deletion plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ instance KnownTypeAst DefaultUni Int where

-- See Note [Int as Integer].
instance HasConstantIn DefaultUni term => KnownTypeIn DefaultUni term Int where
makeKnown mayCause = makeKnown mayCause . toInteger
makeKnown emit mayCause = makeKnown emit mayCause . toInteger
readKnown mayCause term = do
i :: Integer <- readKnown mayCause term
unless (fromIntegral (minBound :: Int) <= i && i <= fromIntegral (maxBound :: Int)) $
Expand Down
14 changes: 7 additions & 7 deletions plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,7 @@ evalBuiltinApp
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp term runtime@(BuiltinRuntime sch x _) = case sch of
TypeSchemeResult _ -> makeKnown (Just term) x
TypeSchemeResult _ -> makeKnown emitCkM (Just term) x
_ -> pure $ VBuiltin term runtime

ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
Expand Down Expand Up @@ -109,12 +109,12 @@ instance AsEvaluationFailure CkUserError where
instance Pretty CkUserError where
pretty CkEvaluationFailure = "The provided Plutus code called 'error'."

instance MonadEmitter (CkM uni fun s) where
emit str = do
mayLogsRef <- asks ckEnvMayEmitRef
case mayLogsRef of
Nothing -> pure ()
Just logsRef -> lift . lift $ modifySTRef logsRef (`DList.snoc` str)
emitCkM :: Text -> CkM uni fun s ()
emitCkM str = do
mayLogsRef <- asks ckEnvMayEmitRef
case mayLogsRef of
Nothing -> pure ()
Just logsRef -> lift . lift $ modifySTRef logsRef (`DList.snoc` str)

type instance UniOf (CkValue uni fun) = uni

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -115,8 +115,6 @@ newtype EvalM unique name uni fun ann a = EvalM
( Functor, Applicative, Monad
, MonadError (HoasException fun (Value unique name uni fun ann))
)
-- No logging for now.
deriving (MonadEmitter) via (NoEmitterT (EvalM unique name uni fun ann))

makeClassyPrisms ''UserHoasError
makeClassyPrisms ''InternalHoasError
Expand Down Expand Up @@ -210,7 +208,7 @@ evalBuiltinApp
-- Note the absence of 'evalValue'. Same logic as with the CEK machine applies:
-- 'makeKnown' never returns a non-value term.
evalBuiltinApp _ _ (BuiltinRuntime (TypeSchemeResult _) x _) =
makeKnown Nothing x
makeKnown (\_ -> pure ()) Nothing x -- No logging for now.
evalBuiltinApp ann getTerm runtime =
pure . HBuiltin ann $ BuiltinApp getTerm runtime

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -542,7 +542,7 @@ evalBuiltinApp
evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of
TypeSchemeResult _ -> do
spendBudgetCek (BBuiltinApp fun) cost
flip unWithEmitterT ?cekEmitter $ makeKnown (Just term) x
makeKnown ?cekEmitter (Just term) x
_ -> pure $ VBuiltin fun term env runtime
{-# INLINE evalBuiltinApp #-}

Expand Down

0 comments on commit e995df9

Please sign in to comment.