Skip to content

Commit

Permalink
[Builtins] Optimize 'MakeKnownM'
Browse files Browse the repository at this point in the history
  • Loading branch information
effectfully committed May 5, 2022
1 parent ffa3178 commit baaddd2
Show file tree
Hide file tree
Showing 6 changed files with 87 additions and 31 deletions.
86 changes: 72 additions & 14 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -18,20 +18,18 @@ module PlutusCore.Builtin.KnownType
, throwKnownTypeErrorWithCause
, KnownBuiltinTypeIn
, KnownBuiltinType
, MakeKnownM
, MakeKnownM (..)
, ReadKnownM
, liftReadKnownM
, readKnownConstant
, MakeKnownIn (..)
, MakeKnown
, ReadKnownIn (..)
, ReadKnown
, makeKnownRun
, makeKnownOrFail
, readKnownSelf
) where

import PlutusPrelude (reoption)

import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.Polymorphism
Expand Down Expand Up @@ -195,12 +193,74 @@ a ton of instances (and add new ones whenever we need them), wrap and unwrap all

-- See Note [MakeKnownM and ReadKnownM being type synonyms].
-- | The monad that 'makeKnown' runs in.
type MakeKnownM = ExceptT KnownTypeError Emitter
data MakeKnownM a
= MakeKnownFailure !(DList Text) !KnownTypeError
| MakeKnownSuccess !a
| MakeKnownSuccessWithLogs !(DList Text) !a

withEmitMakeKnownM :: DList Text -> MakeKnownM a -> MakeKnownM a
withEmitMakeKnownM logs1 (MakeKnownSuccessWithLogs logs2 x) =
MakeKnownSuccessWithLogs (logs1 <> logs2) x
withEmitMakeKnownM logs1 (MakeKnownSuccess x) =
MakeKnownSuccessWithLogs logs1 x
withEmitMakeKnownM logs1 (MakeKnownFailure logs2 err) =
MakeKnownFailure (logs1 <> logs2) err
{-# INLINE withEmitMakeKnownM #-}

instance Functor MakeKnownM where
fmap _ (MakeKnownFailure logs err) = MakeKnownFailure logs err
fmap f (MakeKnownSuccess a) = MakeKnownSuccess (f a)
fmap f (MakeKnownSuccessWithLogs logs a) = MakeKnownSuccessWithLogs logs (f a)
{-# INLINE fmap #-}

_ <$ MakeKnownFailure logs err = MakeKnownFailure logs err
x <$ MakeKnownSuccess _ = MakeKnownSuccess x
x <$ MakeKnownSuccessWithLogs logs _ = MakeKnownSuccessWithLogs logs x
{-# INLINE (<$) #-}

instance Applicative MakeKnownM where
pure = MakeKnownSuccess
{-# INLINE pure #-}

MakeKnownFailure logs err <*> _ =
MakeKnownFailure logs err
MakeKnownSuccess _ <*> MakeKnownFailure logs err =
MakeKnownFailure logs err
MakeKnownSuccess f <*> MakeKnownSuccess x =
MakeKnownSuccess (f x)
MakeKnownSuccess f <*> MakeKnownSuccessWithLogs logs x =
MakeKnownSuccessWithLogs logs (f x)
MakeKnownSuccessWithLogs logs1 _ <*> MakeKnownFailure logs2 err =
MakeKnownFailure (logs1 <> logs2) err
MakeKnownSuccessWithLogs logs f <*> MakeKnownSuccess x =
MakeKnownSuccessWithLogs logs (f x)
MakeKnownSuccessWithLogs logs1 f <*> MakeKnownSuccessWithLogs logs2 x =
MakeKnownSuccessWithLogs (logs1 <> logs2) (f x)
{-# INLINE (<*>) #-}

MakeKnownFailure logs err *> _ = MakeKnownFailure logs err
MakeKnownSuccess _ *> a = a
MakeKnownSuccessWithLogs logs1 _ *> a = withEmitMakeKnownM logs1 a
{-# INLINE (*>) #-}

instance Monad MakeKnownM where
MakeKnownFailure logs err >>= _ = MakeKnownFailure logs err
MakeKnownSuccess x >>= f = f x
MakeKnownSuccessWithLogs logs x >>= f = withEmitMakeKnownM logs $ f x
{-# INLINE (>>=) #-}

(>>) = (*>)
{-# INLINE (>>) #-}

-- See Note [MakeKnownM and ReadKnownM being type synonyms].
-- | The monad that 'readKnown' runs in.
type ReadKnownM = Either KnownTypeError

liftReadKnownM :: ReadKnownM a -> MakeKnownM a
liftReadKnownM (Left err) = MakeKnownFailure mempty err
liftReadKnownM (Right x) = MakeKnownSuccess x
{-# INLINE liftReadKnownM #-}

-- See Note [Unlifting values of built-in types].
-- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
readKnownConstant :: forall val a. KnownBuiltinType val a => val -> ReadKnownM a
Expand Down Expand Up @@ -253,15 +313,12 @@ class uni ~ UniOf val => ReadKnownIn uni val a where

type ReadKnown val = ReadKnownIn (UniOf val) val

makeKnownRun
:: MakeKnownIn uni val a
=> a -> (ReadKnownM val, DList Text)
makeKnownRun = runEmitter . runExceptT . makeKnown
{-# INLINE makeKnownRun #-}

-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
makeKnownOrFail = reoption . fst . makeKnownRun
makeKnownOrFail x = case makeKnown x of
MakeKnownFailure _ _ -> EvaluationFailure
MakeKnownSuccess val -> EvaluationSuccess val
MakeKnownSuccessWithLogs _ val -> EvaluationSuccess val
{-# INLINE makeKnownOrFail #-}

-- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
Expand All @@ -274,7 +331,7 @@ readKnownSelf val = either (throwKnownTypeErrorWithCause val) pure $ readKnown v
{-# INLINE readKnownSelf #-}

instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
makeKnown EvaluationFailure = throwing_ _EvaluationFailure
makeKnown EvaluationFailure = MakeKnownFailure mempty KnownTypeEvaluationFailure
makeKnown (EvaluationSuccess x) = makeKnown x
{-# INLINE makeKnown #-}

Expand All @@ -291,7 +348,8 @@ instance
readKnown _ = throwing _UnliftingError "Panic: 'TypeError' was bypassed"

instance MakeKnownIn uni val a => MakeKnownIn uni val (Emitter a) where
makeKnown = lift >=> makeKnown
makeKnown a = case runEmitter a of
(x, logs) -> withEmitMakeKnownM logs $ makeKnown x
{-# INLINE makeKnown #-}

instance
Expand Down
3 changes: 1 addition & 2 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Name

import Control.Monad.Except
import Data.Array
import Data.Kind qualified as GHC
import Data.Proxy
Expand Down Expand Up @@ -177,7 +176,7 @@ instance (res ~ res', Typeable res, KnownTypeAst (UniOf val) res, MakeKnown val

-- For deferred unlifting we need to lift the 'ReadKnownM' action into 'MakeKnownM',
-- hence 'liftEither'.
toDeferredF getRes = liftEither getRes >>= makeKnown
toDeferredF getRes = liftReadKnownM getRes >>= makeKnown
{-# INLINE toDeferredF #-}

-- | Every term-level argument becomes as 'TypeSchemeArrow'.
Expand Down
4 changes: 2 additions & 2 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
Original file line number Diff line number Diff line change
Expand Up @@ -104,8 +104,8 @@ data UnliftingMode
-- instantiating '_broToExF' with a cost model to get the costing function for the builtin.
data BuiltinRuntimeOptions n val cost = BuiltinRuntimeOptions
{ _broRuntimeScheme :: RuntimeScheme n
, _broImmediateF :: ToRuntimeDenotationType val n
, _broDeferredF :: ToRuntimeDenotationType val n
, _broImmediateF :: ~(ToRuntimeDenotationType val n)
, _broDeferredF :: ~(ToRuntimeDenotationType val n)
, _broToExF :: cost -> ToCostingType n
}

Expand Down
10 changes: 4 additions & 6 deletions plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/Ck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -67,12 +67,10 @@ evalBuiltinApp
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp term runtime@(BuiltinRuntime sch getX _) = case sch of
RuntimeSchemeResult -> do
let (errOrRes, logs) = runEmitter $ runExceptT getX
emitCkM logs
case errOrRes of
Left err -> throwKnownTypeErrorWithCause term err
Right res -> pure res
RuntimeSchemeResult -> case getX of
MakeKnownFailure logs err -> emitCkM logs *> throwKnownTypeErrorWithCause term err
MakeKnownSuccess x -> pure x
MakeKnownSuccessWithLogs logs x -> emitCkM logs $> x
_ -> pure $ VBuiltin term runtime

ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
Expand Down
4 changes: 2 additions & 2 deletions plutus-core/plutus-core/test/Evaluation/Spec.hs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ prop_builtinsDon'tThrow bn = property $ do
mbErr <-
liftIO $
catch
(($> Nothing) . evaluate . runEmitter . runExceptT $ eval args)
(($> Nothing) . evaluate $ eval args)
(pure . pure)
whenJust mbErr $ \(e :: SomeException) -> do
annotate "Builtin function evaluation failed"
Expand All @@ -79,7 +79,7 @@ prop_builtinsDon'tThrow bn = property $ do
MakeKnownM Term
go sch f args = case (sch, args) of
(RuntimeSchemeArrow sch', a : as) -> do
res <- liftEither (f a)
res <- liftReadKnownM (f a)
go sch' res as
(RuntimeSchemeResult, []) -> f
(RuntimeSchemeAll sch', _) -> go sch' f args
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -565,11 +565,12 @@ evalBuiltinApp
evalBuiltinApp fun term env runtime@(BuiltinRuntime sch getX cost) = case sch of
RuntimeSchemeResult -> do
spendBudgetCek (BBuiltinApp fun) cost
let !(errOrRes, logs) = runEmitter $ runExceptT getX
?cekEmitter logs
case errOrRes of
Left err -> throwKnownTypeErrorWithCause term err
Right res -> pure res
case getX of
MakeKnownFailure logs err -> do
?cekEmitter logs
throwKnownTypeErrorWithCause term err
MakeKnownSuccess x -> pure x
MakeKnownSuccessWithLogs logs x -> ?cekEmitter logs $> x
_ -> pure $ VBuiltin fun term env runtime
{-# INLINE evalBuiltinApp #-}

Expand Down

0 comments on commit baaddd2

Please sign in to comment.