-
Notifications
You must be signed in to change notification settings - Fork 483
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Builtins] Monomorphize 'makeKnown' #4421
Changes from 19 commits
ab46d64
be641e9
6364cc7
3156484
0f6819c
55a8882
c894010
c00c67c
be24fc9
4954a86
36dac78
9a19955
668fa12
4dd1a04
f7df467
dde10a5
cda7279
f313374
89b3e44
3f62375
75175cb
b070d8d
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,27 +1,22 @@ | ||
{-# LANGUAGE RankNTypes #-} | ||
|
||
module PlutusCore.Builtin.Emitter | ||
( Emitter (..) | ||
, emitM | ||
, runEmitter | ||
, emit | ||
) where | ||
|
||
import Control.Monad.Trans.Writer.Strict (Writer, runWriter, tell) | ||
import Data.DList as DList | ||
import Data.Text (Text) | ||
|
||
-- | 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. | ||
-- | A monad for logging. | ||
newtype Emitter a = Emitter | ||
{ 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 $ \emit -> f emit <*> a emit | ||
{ unEmitter :: Writer (DList Text) a | ||
} deriving newtype (Functor, Applicative, Monad) | ||
|
||
instance Monad Emitter where | ||
Emitter a >>= f = Emitter $ \emit -> a emit >>= \x -> unEmitter (f x) emit | ||
runEmitter :: Emitter a -> (a, DList Text) | ||
runEmitter = runWriter . unEmitter | ||
{-# INLINE runEmitter #-} | ||
|
||
emitM :: Text -> Emitter () | ||
emitM text = Emitter ($ text) | ||
emit :: Text -> Emitter () | ||
emit = Emitter . tell . pure | ||
{-# INLINE emit #-} |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -72,6 +72,7 @@ import Control.Monad.Except | |
import Control.Monad.ST | ||
import Control.Monad.ST.Unsafe | ||
import Data.Array hiding (index) | ||
import Data.DList (DList) | ||
import Data.Hashable (Hashable) | ||
import Data.Kind qualified as GHC | ||
import Data.Semigroup (stimes) | ||
|
@@ -284,7 +285,7 @@ defaultSlippage :: Slippage | |
defaultSlippage = 200 | ||
|
||
-- | The CEK machine is parameterized over an emitter function, similar to 'CekBudgetSpender'. | ||
type CekEmitter uni fun s = Text -> CekM uni fun s () | ||
type CekEmitter uni fun s = DList Text -> CekM uni fun s () | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It's a bit sad that the monomorphization of There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Thinking about it, I feel like it was actually stupid to add There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Also in the CK machine for consistency? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can you add a comment here regardless of what you do? |
||
|
||
-- | Runtime emitter info, similar to 'ExBudgetInfo'. | ||
data CekEmitterInfo uni fun s = CekEmitterInfo { | ||
|
@@ -555,7 +556,11 @@ evalBuiltinApp | |
evalBuiltinApp fun term env runtime@(BuiltinRuntime sch x cost) = case sch of | ||
RuntimeSchemeResult -> do | ||
spendBudgetCek (BBuiltinApp fun) cost | ||
makeKnown ?cekEmitter (Just term) x | ||
let !(errOrRes, logs) = makeKnownRun (Just term) x | ||
?cekEmitter logs | ||
case errOrRes of | ||
Left err -> throwMakeKnownErrorWithCause err | ||
Right res -> pure res | ||
_ -> pure $ VBuiltin fun term env runtime | ||
{-# INLINE evalBuiltinApp #-} | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I managed to get myself worried here about whether you could build up massive lists of strings at low cost. I suppose you could only do that inside a builtin though, so it shouldn't be an issue. It doesn't matter if someone uses
trace
many times for example because the contents will be dumped each time it returns.