{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Evaluation.Machine.Ck
( EvaluationResult (..)
, CkEvaluationException
, CkM
, CkValue
, runCk
, splitStructuralOperational
, unsafeSplitStructuralOperational
, evaluateCk
, evaluateCkNoEmit
, readKnownCk
) where
import PlutusPrelude
import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Evaluation.Result
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Subst
import Control.Lens ((^?))
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.ST
import Data.DList (DList)
import Data.DList qualified as DList
import Data.List.Extras (wix)
import Data.STRef
import Data.Text (Text)
import Data.Word
import Universe
infix 4 |>, <|
instance Show (BuiltinRuntime (CkValue uni fun)) where
show :: BuiltinRuntime (CkValue uni fun) -> String
show BuiltinRuntime (CkValue uni fun)
_ = String
"<builtin_runtime>"
data CkValue uni fun =
VCon (Some (ValueOf uni))
| VTyAbs TyName (Kind ()) (Term TyName Name uni fun ())
| VLamAbs Name (Type TyName uni ()) (Term TyName Name uni fun ())
| VIWrap (Type TyName uni ()) (Type TyName uni ()) (CkValue uni fun)
| VBuiltin (Term TyName Name uni fun ()) (BuiltinRuntime (CkValue uni fun))
| VConstr (Type TyName uni ()) Word64 [CkValue uni fun]
deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Closed uni)
=> Show (CkValue uni fun)
ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm :: forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm = \case
VCon Some (ValueOf uni)
val -> () -> Some (ValueOf uni) -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant () Some (ValueOf uni)
val
VTyAbs TyName
tn Kind ()
k Term TyName Name uni fun ()
body -> ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
tn Kind ()
k Term TyName Name uni fun ()
body
VLamAbs Name
name Type TyName uni ()
ty Term TyName Name uni fun ()
body -> ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
name Type TyName uni ()
ty Term TyName Name uni fun ()
body
VIWrap Type TyName uni ()
ty1 Type TyName uni ()
ty2 CkValue uni fun
val -> ()
-> Type TyName uni ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap () Type TyName uni ()
ty1 Type TyName uni ()
ty2 (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
val
VBuiltin Term TyName Name uni fun ()
term BuiltinRuntime (CkValue uni fun)
_ -> Term TyName Name uni fun ()
term
VConstr Type TyName uni ()
ty Word64
i [CkValue uni fun]
es -> ()
-> Type TyName uni ()
-> Word64
-> [Term TyName Name uni fun ()]
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr () Type TyName uni ()
ty Word64
i ((CkValue uni fun -> Term TyName Name uni fun ())
-> [CkValue uni fun] -> [Term TyName Name uni fun ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm [CkValue uni fun]
es)
data CkEnv uni fun s = CkEnv
{ forall (uni :: * -> *) fun s.
CkEnv uni fun s -> BuiltinsRuntime fun (CkValue uni fun)
ckEnvRuntime :: BuiltinsRuntime fun (CkValue uni fun)
, forall (uni :: * -> *) fun s.
CkEnv uni fun s -> Maybe (STRef s (DList Text))
ckEnvMayEmitRef :: Maybe (STRef s (DList Text))
}
instance (PrettyUni uni, Pretty fun) => PrettyBy PrettyConfigPlc (CkValue uni fun) where
prettyBy :: forall ann. PrettyConfigPlc -> CkValue uni fun -> Doc ann
prettyBy PrettyConfigPlc
cfg = PrettyConfigPlc -> Term TyName Name uni fun () -> Doc ann
forall ann.
PrettyConfigPlc -> Term TyName Name uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg (Term TyName Name uni fun () -> Doc ann)
-> (CkValue uni fun -> Term TyName Name uni fun ())
-> CkValue uni fun
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm
data CkUserError =
CkEvaluationFailure
deriving stock (Int -> CkUserError -> ShowS
[CkUserError] -> ShowS
CkUserError -> String
(Int -> CkUserError -> ShowS)
-> (CkUserError -> String)
-> ([CkUserError] -> ShowS)
-> Show CkUserError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CkUserError -> ShowS
showsPrec :: Int -> CkUserError -> ShowS
$cshow :: CkUserError -> String
show :: CkUserError -> String
$cshowList :: [CkUserError] -> ShowS
showList :: [CkUserError] -> ShowS
Show, CkUserError -> CkUserError -> Bool
(CkUserError -> CkUserError -> Bool)
-> (CkUserError -> CkUserError -> Bool) -> Eq CkUserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CkUserError -> CkUserError -> Bool
== :: CkUserError -> CkUserError -> Bool
$c/= :: CkUserError -> CkUserError -> Bool
/= :: CkUserError -> CkUserError -> Bool
Eq, (forall x. CkUserError -> Rep CkUserError x)
-> (forall x. Rep CkUserError x -> CkUserError)
-> Generic CkUserError
forall x. Rep CkUserError x -> CkUserError
forall x. CkUserError -> Rep CkUserError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CkUserError -> Rep CkUserError x
from :: forall x. CkUserError -> Rep CkUserError x
$cto :: forall x. Rep CkUserError x -> CkUserError
to :: forall x. Rep CkUserError x -> CkUserError
Generic)
deriving anyclass (CkUserError -> ()
(CkUserError -> ()) -> NFData CkUserError
forall a. (a -> ()) -> NFData a
$crnf :: CkUserError -> ()
rnf :: CkUserError -> ()
NFData)
type CkEvaluationException uni fun =
EvaluationException (MachineError fun) CkUserError (Term TyName Name uni fun ())
type CkM uni fun s =
ReaderT (CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun)
(ST s))
instance AsEvaluationFailure CkUserError where
_EvaluationFailure :: Prism' CkUserError ()
_EvaluationFailure = CkUserError -> Prism' CkUserError ()
forall err. Eq err => err -> Prism' err ()
_EvaluationFailureVia CkUserError
CkEvaluationFailure
instance AsUnliftingError CkUserError where
_UnliftingError :: Prism' CkUserError UnliftingError
_UnliftingError = CkUserError -> Prism' CkUserError UnliftingError
forall err. Pretty err => err -> Prism' err UnliftingError
_UnliftingErrorVia CkUserError
CkEvaluationFailure
instance Pretty CkUserError where
pretty :: forall ann. CkUserError -> Doc ann
pretty CkUserError
CkEvaluationFailure = Doc ann
"The provided Plutus code called 'error'."
emitCkM :: DList Text -> CkM uni fun s ()
emitCkM :: forall (uni :: * -> *) fun s. DList Text -> CkM uni fun s ()
emitCkM DList Text
logs = do
Maybe (STRef s (DList Text))
mayLogsRef <- (CkEnv uni fun s -> Maybe (STRef s (DList Text)))
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Maybe (STRef s (DList Text)))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks CkEnv uni fun s -> Maybe (STRef s (DList Text))
forall (uni :: * -> *) fun s.
CkEnv uni fun s -> Maybe (STRef s (DList Text))
ckEnvMayEmitRef
case Maybe (STRef s (DList Text))
mayLogsRef of
Maybe (STRef s (DList Text))
Nothing -> () -> CkM uni fun s ()
forall a.
a
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just STRef s (DList Text)
logsRef -> ExceptT (CkEvaluationException uni fun) (ST s) ()
-> CkM uni fun s ()
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT (CkEnv uni fun s) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT (CkEvaluationException uni fun) (ST s) ()
-> CkM uni fun s ())
-> (ST s () -> ExceptT (CkEvaluationException uni fun) (ST s) ())
-> ST s ()
-> CkM uni fun s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ST s () -> ExceptT (CkEvaluationException uni fun) (ST s) ()
forall (m :: * -> *) a.
Monad m =>
m a -> ExceptT (CkEvaluationException uni fun) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ST s () -> CkM uni fun s ()) -> ST s () -> CkM uni fun s ()
forall a b. (a -> b) -> a -> b
$ STRef s (DList Text) -> (DList Text -> DList Text) -> ST s ()
forall s a. STRef s a -> (a -> a) -> ST s ()
modifySTRef STRef s (DList Text)
logsRef (DList Text -> DList Text -> DList Text
forall a. DList a -> DList a -> DList a
`DList.append` DList Text
logs)
type instance UniOf (CkValue uni fun) = uni
instance HasConstant (CkValue uni fun) where
asConstant :: CkValue uni fun
-> Either BuiltinError (Some (ValueOf (UniOf (CkValue uni fun))))
asConstant (VCon Some (ValueOf uni)
val) = Some (ValueOf uni) -> Either BuiltinError (Some (ValueOf uni))
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
asConstant CkValue uni fun
_ = Either BuiltinError (Some (ValueOf uni))
Either BuiltinError (Some (ValueOf (UniOf (CkValue uni fun))))
forall (m :: * -> *) void. MonadError BuiltinError m => m void
throwNotAConstant
fromConstant :: Some (ValueOf (UniOf (CkValue uni fun))) -> CkValue uni fun
fromConstant = Some (ValueOf uni) -> CkValue uni fun
Some (ValueOf (UniOf (CkValue uni fun))) -> CkValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CkValue uni fun
VCon
data Frame uni fun
= FrameAwaitArg (CkValue uni fun)
| FrameAwaitFunTerm (Term TyName Name uni fun ())
| FrameAwaitFunValue (CkValue uni fun)
| FrameTyInstArg (Type TyName uni ())
| FrameUnwrap
| FrameIWrap (Type TyName uni ()) (Type TyName uni ())
| FrameConstr (Type TyName uni ()) Word64 [Term TyName Name uni fun ()] [CkValue uni fun]
| FrameCase [Term TyName Name uni fun ()]
deriving stock instance (GShow uni, Closed uni, uni `Everywhere` Show, Show fun) =>
Show (Frame uni fun)
type Context uni fun = [Frame uni fun]
instance ExMemoryUsage (CkValue uni fun) where
memoryUsage :: CkValue uni fun -> CostRose
memoryUsage = String -> CkValue uni fun -> CostRose
forall a. HasCallStack => String -> a
error String
"Internal error: 'memoryUsage' for 'CkValue' is not supposed to be forced"
runCkM
:: BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> (forall s. CkM uni fun s a)
-> (Either (CkEvaluationException uni fun) a, [Text])
runCkM :: forall fun (uni :: * -> *) a.
BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> (forall s. CkM uni fun s a)
-> (Either (CkEvaluationException uni fun) a, [Text])
runCkM BuiltinsRuntime fun (CkValue uni fun)
runtime Bool
emitting forall s. CkM uni fun s a
a = (forall s. ST s (Either (CkEvaluationException uni fun) a, [Text]))
-> (Either (CkEvaluationException uni fun) a, [Text])
forall a. (forall s. ST s a) -> a
runST ((forall s.
ST s (Either (CkEvaluationException uni fun) a, [Text]))
-> (Either (CkEvaluationException uni fun) a, [Text]))
-> (forall s.
ST s (Either (CkEvaluationException uni fun) a, [Text]))
-> (Either (CkEvaluationException uni fun) a, [Text])
forall a b. (a -> b) -> a -> b
$ do
Maybe (STRef s (DList Text))
mayLogsRef <- if Bool
emitting then STRef s (DList Text) -> Maybe (STRef s (DList Text))
forall a. a -> Maybe a
Just (STRef s (DList Text) -> Maybe (STRef s (DList Text)))
-> ST s (STRef s (DList Text))
-> ST s (Maybe (STRef s (DList Text)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DList Text -> ST s (STRef s (DList Text))
forall a s. a -> ST s (STRef s a)
newSTRef DList Text
forall a. DList a
DList.empty else Maybe (STRef s (DList Text)) -> ST s (Maybe (STRef s (DList Text)))
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (STRef s (DList Text))
forall a. Maybe a
Nothing
Either (CkEvaluationException uni fun) a
errOrRes <- ExceptT (CkEvaluationException uni fun) (ST s) a
-> ST s (Either (CkEvaluationException uni fun) a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (CkEvaluationException uni fun) (ST s) a
-> ST s (Either (CkEvaluationException uni fun) a))
-> (CkEnv uni fun s
-> ExceptT (CkEvaluationException uni fun) (ST s) a)
-> CkEnv uni fun s
-> ST s (Either (CkEvaluationException uni fun) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
-> CkEnv uni fun s
-> ExceptT (CkEvaluationException uni fun) (ST s) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
forall s. CkM uni fun s a
a (CkEnv uni fun s
-> ST s (Either (CkEvaluationException uni fun) a))
-> CkEnv uni fun s
-> ST s (Either (CkEvaluationException uni fun) a)
forall a b. (a -> b) -> a -> b
$ BuiltinsRuntime fun (CkValue uni fun)
-> Maybe (STRef s (DList Text)) -> CkEnv uni fun s
forall (uni :: * -> *) fun s.
BuiltinsRuntime fun (CkValue uni fun)
-> Maybe (STRef s (DList Text)) -> CkEnv uni fun s
CkEnv BuiltinsRuntime fun (CkValue uni fun)
runtime Maybe (STRef s (DList Text))
mayLogsRef
[Text]
logs <- case Maybe (STRef s (DList Text))
mayLogsRef of
Maybe (STRef s (DList Text))
Nothing -> [Text] -> ST s [Text]
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just STRef s (DList Text)
logsRef -> DList Text -> [Text]
forall a. DList a -> [a]
DList.toList (DList Text -> [Text]) -> ST s (DList Text) -> ST s [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STRef s (DList Text) -> ST s (DList Text)
forall s a. STRef s a -> ST s a
readSTRef STRef s (DList Text)
logsRef
(Either (CkEvaluationException uni fun) a, [Text])
-> ST s (Either (CkEvaluationException uni fun) a, [Text])
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (CkEvaluationException uni fun) a
errOrRes, [Text]
logs)
(|>)
:: Context uni fun -> Term TyName Name uni fun () -> CkM uni fun s (Term TyName Name uni fun ())
Context uni fun
stack |> :: forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> TyInst ()
_ Term TyName Name uni fun ()
fun Type TyName uni ()
ty = Type TyName uni () -> Frame uni fun
forall (uni :: * -> *) fun. Type TyName uni () -> Frame uni fun
FrameTyInstArg Type TyName uni ()
ty Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
fun
Context uni fun
stack |> Apply ()
_ Term TyName Name uni fun ()
fun Term TyName Name uni fun ()
arg = Term TyName Name uni fun () -> Frame uni fun
forall (uni :: * -> *) fun.
Term TyName Name uni fun () -> Frame uni fun
FrameAwaitFunTerm Term TyName Name uni fun ()
arg Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
fun
Context uni fun
stack |> IWrap ()
_ Type TyName uni ()
pat Type TyName uni ()
arg Term TyName Name uni fun ()
term = Type TyName uni () -> Type TyName uni () -> Frame uni fun
forall (uni :: * -> *) fun.
Type TyName uni () -> Type TyName uni () -> Frame uni fun
FrameIWrap Type TyName uni ()
pat Type TyName uni ()
arg Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
term
Context uni fun
stack |> Unwrap ()
_ Term TyName Name uni fun ()
term = Frame uni fun
forall (uni :: * -> *) fun. Frame uni fun
FrameUnwrap Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
term
Context uni fun
stack |> TyAbs ()
_ TyName
tn Kind ()
k Term TyName Name uni fun ()
term = Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| TyName -> Kind () -> Term TyName Name uni fun () -> CkValue uni fun
forall (uni :: * -> *) fun.
TyName -> Kind () -> Term TyName Name uni fun () -> CkValue uni fun
VTyAbs TyName
tn Kind ()
k Term TyName Name uni fun ()
term
Context uni fun
stack |> LamAbs ()
_ Name
name Type TyName uni ()
ty Term TyName Name uni fun ()
body = Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> CkValue uni fun
forall (uni :: * -> *) fun.
Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> CkValue uni fun
VLamAbs Name
name Type TyName uni ()
ty Term TyName Name uni fun ()
body
Context uni fun
stack |> Builtin ()
_ fun
bn = do
BuiltinRuntime (CkValue uni fun)
runtime <- fun
-> BuiltinsRuntime fun (CkValue uni fun)
-> BuiltinRuntime (CkValue uni fun)
forall fun val.
fun -> BuiltinsRuntime fun val -> BuiltinRuntime val
lookupBuiltin fun
bn (BuiltinsRuntime fun (CkValue uni fun)
-> BuiltinRuntime (CkValue uni fun))
-> (CkEnv uni fun s -> BuiltinsRuntime fun (CkValue uni fun))
-> CkEnv uni fun s
-> BuiltinRuntime (CkValue uni fun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CkEnv uni fun s -> BuiltinsRuntime fun (CkValue uni fun)
forall (uni :: * -> *) fun s.
CkEnv uni fun s -> BuiltinsRuntime fun (CkValue uni fun)
ckEnvRuntime (CkEnv uni fun s -> BuiltinRuntime (CkValue uni fun))
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(CkEnv uni fun s)
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(BuiltinRuntime (CkValue uni fun))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(CkEnv uni fun s)
forall r (m :: * -> *). MonadReader r m => m r
ask
Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun) -> CkValue uni fun
forall (uni :: * -> *) fun.
Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun) -> CkValue uni fun
VBuiltin (() -> fun -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () fun
bn) BuiltinRuntime (CkValue uni fun)
runtime
Context uni fun
stack |> Constant ()
_ Some (ValueOf uni)
val = Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Some (ValueOf uni) -> CkValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CkValue uni fun
VCon Some (ValueOf uni)
val
Context uni fun
stack |> Constr ()
_ Type TyName uni ()
ty Word64
i [Term TyName Name uni fun ()]
es = case [Term TyName Name uni fun ()]
es of
[] -> Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Type TyName uni ()
-> Word64 -> [CkValue uni fun] -> CkValue uni fun
forall (uni :: * -> *) fun.
Type TyName uni ()
-> Word64 -> [CkValue uni fun] -> CkValue uni fun
VConstr Type TyName uni ()
ty Word64
i []
Term TyName Name uni fun ()
t : [Term TyName Name uni fun ()]
ts -> Type TyName uni ()
-> Word64
-> [Term TyName Name uni fun ()]
-> [CkValue uni fun]
-> Frame uni fun
forall (uni :: * -> *) fun.
Type TyName uni ()
-> Word64
-> [Term TyName Name uni fun ()]
-> [CkValue uni fun]
-> Frame uni fun
FrameConstr Type TyName uni ()
ty Word64
i [Term TyName Name uni fun ()]
ts [] Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
t
Context uni fun
stack |> Case ()
_ Type TyName uni ()
_ Term TyName Name uni fun ()
arg [Term TyName Name uni fun ()]
cs = [Term TyName Name uni fun ()] -> Frame uni fun
forall (uni :: * -> *) fun.
[Term TyName Name uni fun ()] -> Frame uni fun
FrameCase [Term TyName Name uni fun ()]
cs Frame uni fun -> Context uni fun -> Context uni fun
forall a. a -> [a] -> [a]
: Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
arg
Context uni fun
_ |> Error{} =
AReview
(EvaluationError (MachineError fun) CkUserError)
(EvaluationError (MachineError fun) CkUserError)
-> EvaluationError (MachineError fun) CkUserError
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError)
(EvaluationError (MachineError fun) CkUserError)
forall r structural operational.
AsEvaluationError r structural operational =>
Prism' r (EvaluationError structural operational)
Prism'
(EvaluationError (MachineError fun) CkUserError)
(EvaluationError (MachineError fun) CkUserError)
_EvaluationError (CkUserError -> EvaluationError (MachineError fun) CkUserError
forall structural operational.
operational -> EvaluationError structural operational
OperationalEvaluationError CkUserError
CkEvaluationFailure) Maybe (Term TyName Name uni fun ())
forall a. Maybe a
Nothing
Context uni fun
_ |> var :: Term TyName Name uni fun ()
var@Var{} =
AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
OpenTermEvaluatedMachineError (Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ()))
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just Term TyName Name uni fun ()
var
(<|)
:: Context uni fun -> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
[] <| :: forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
val = Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall a.
a
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
val
FrameTyInstArg Type TyName uni ()
ty : [Frame uni fun]
stack <| CkValue uni fun
fun = [Frame uni fun]
-> Type TyName uni ()
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Type TyName uni ()
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
instantiateEvaluate [Frame uni fun]
stack Type TyName uni ()
ty CkValue uni fun
fun
FrameAwaitFunTerm Term TyName Name uni fun ()
arg : [Frame uni fun]
stack <| CkValue uni fun
fun = CkValue uni fun -> Frame uni fun
forall (uni :: * -> *) fun. CkValue uni fun -> Frame uni fun
FrameAwaitArg CkValue uni fun
fun Frame uni fun -> [Frame uni fun] -> [Frame uni fun]
forall a. a -> [a] -> [a]
: [Frame uni fun]
stack [Frame uni fun]
-> Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
arg
FrameAwaitArg CkValue uni fun
fun : [Frame uni fun]
stack <| CkValue uni fun
arg = [Frame uni fun]
-> CkValue uni fun
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate [Frame uni fun]
stack CkValue uni fun
fun CkValue uni fun
arg
FrameAwaitFunValue CkValue uni fun
arg : [Frame uni fun]
stack <| CkValue uni fun
fun = [Frame uni fun]
-> CkValue uni fun
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate [Frame uni fun]
stack CkValue uni fun
fun CkValue uni fun
arg
FrameIWrap Type TyName uni ()
pat Type TyName uni ()
arg : [Frame uni fun]
stack <| CkValue uni fun
value = [Frame uni fun]
stack [Frame uni fun]
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Type TyName uni ()
-> Type TyName uni () -> CkValue uni fun -> CkValue uni fun
forall (uni :: * -> *) fun.
Type TyName uni ()
-> Type TyName uni () -> CkValue uni fun -> CkValue uni fun
VIWrap Type TyName uni ()
pat Type TyName uni ()
arg CkValue uni fun
value
Frame uni fun
FrameUnwrap : [Frame uni fun]
stack <| CkValue uni fun
wrapped = case CkValue uni fun
wrapped of
VIWrap Type TyName uni ()
_ Type TyName uni ()
_ CkValue uni fun
term -> [Frame uni fun]
stack [Frame uni fun]
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
term
CkValue uni fun
_ ->
AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonWrapUnwrappedMachineError (Maybe (Term TyName Name uni fun ())
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ()))
-> Maybe (Term TyName Name uni fun ())
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just (Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
wrapped
FrameConstr Type TyName uni ()
ty Word64
i [Term TyName Name uni fun ()]
todo [CkValue uni fun]
done : [Frame uni fun]
stack <| CkValue uni fun
e =
let done' :: [CkValue uni fun]
done' = CkValue uni fun
eCkValue uni fun -> [CkValue uni fun] -> [CkValue uni fun]
forall a. a -> [a] -> [a]
:[CkValue uni fun]
done
in case [Term TyName Name uni fun ()]
todo of
Term TyName Name uni fun ()
t : [Term TyName Name uni fun ()]
ts -> Type TyName uni ()
-> Word64
-> [Term TyName Name uni fun ()]
-> [CkValue uni fun]
-> Frame uni fun
forall (uni :: * -> *) fun.
Type TyName uni ()
-> Word64
-> [Term TyName Name uni fun ()]
-> [CkValue uni fun]
-> Frame uni fun
FrameConstr Type TyName uni ()
ty Word64
i [Term TyName Name uni fun ()]
ts [CkValue uni fun]
done' Frame uni fun -> [Frame uni fun] -> [Frame uni fun]
forall a. a -> [a] -> [a]
: [Frame uni fun]
stack [Frame uni fun]
-> Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
t
[] -> [Frame uni fun]
stack [Frame uni fun]
-> CkValue uni fun
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Type TyName uni ()
-> Word64 -> [CkValue uni fun] -> CkValue uni fun
forall (uni :: * -> *) fun.
Type TyName uni ()
-> Word64 -> [CkValue uni fun] -> CkValue uni fun
VConstr Type TyName uni ()
ty Word64
i ([CkValue uni fun] -> [CkValue uni fun]
forall a. [a] -> [a]
reverse [CkValue uni fun]
done')
FrameCase [Term TyName Name uni fun ()]
cs : [Frame uni fun]
stack <| CkValue uni fun
e = case CkValue uni fun
e of
VConstr Type TyName uni ()
_ Word64
i [CkValue uni fun]
args -> case [Term TyName Name uni fun ()]
cs [Term TyName Name uni fun ()]
-> Getting
(First (Term TyName Name uni fun ()))
[Term TyName Name uni fun ()]
(Term TyName Name uni fun ())
-> Maybe (Term TyName Name uni fun ())
forall s a. s -> Getting (First a) s a -> Maybe a
^? Word64
-> Traversal'
[Term TyName Name uni fun ()] (Term TyName Name uni fun ())
forall a. Word64 -> Traversal' [a] a
wix Word64
i of
Just Term TyName Name uni fun ()
t -> [CkValue uni fun] -> [Frame uni fun] -> [Frame uni fun]
forall {uni :: * -> *} {fun}.
[CkValue uni fun] -> [Frame uni fun] -> [Frame uni fun]
go ([CkValue uni fun] -> [CkValue uni fun]
forall a. [a] -> [a]
reverse [CkValue uni fun]
args) [Frame uni fun]
stack [Frame uni fun]
-> Term TyName Name uni fun ()
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
t
where
go :: [CkValue uni fun] -> [Frame uni fun] -> [Frame uni fun]
go [] [Frame uni fun]
s = [Frame uni fun]
s
go (CkValue uni fun
arg:[CkValue uni fun]
rest) [Frame uni fun]
s = [CkValue uni fun] -> [Frame uni fun] -> [Frame uni fun]
go [CkValue uni fun]
rest (CkValue uni fun -> Frame uni fun
forall (uni :: * -> *) fun. CkValue uni fun -> Frame uni fun
FrameAwaitFunValue CkValue uni fun
arg Frame uni fun -> [Frame uni fun] -> [Frame uni fun]
forall a. a -> [a] -> [a]
: [Frame uni fun]
s)
Maybe (Term TyName Name uni fun ())
Nothing -> AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError (Word64 -> MachineError fun
forall fun. Word64 -> MachineError fun
MissingCaseBranch Word64
i) (Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just (Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
e)
CkValue uni fun
_ -> AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
(Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonConstrScrutinized (Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just (Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
e)
transferSpine :: Spine (CkValue uni fun) -> Context uni fun -> Context uni fun
transferSpine :: forall (uni :: * -> *) fun.
Spine (CkValue uni fun) -> Context uni fun -> Context uni fun
transferSpine Spine (CkValue uni fun)
args Context uni fun
ctx = (CkValue uni fun -> Context uni fun -> Context uni fun)
-> Context uni fun -> Spine (CkValue uni fun) -> Context uni fun
forall a b. (a -> b -> b) -> b -> Spine a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Frame uni fun -> Context uni fun -> Context uni fun)
-> (CkValue uni fun -> Frame uni fun)
-> CkValue uni fun
-> Context uni fun
-> Context uni fun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CkValue uni fun -> Frame uni fun
forall (uni :: * -> *) fun. CkValue uni fun -> Frame uni fun
FrameAwaitFunValue) Context uni fun
ctx Spine (CkValue uni fun)
args
returnCkHeadSpine
:: Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
returnCkHeadSpine :: forall (uni :: * -> *) fun s.
Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
returnCkHeadSpine Context uni fun
stack (HeadOnly CkValue uni fun
x) = Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
x
returnCkHeadSpine Context uni fun
stack (HeadSpine CkValue uni fun
f Spine (CkValue uni fun)
xs) = Spine (CkValue uni fun) -> Context uni fun -> Context uni fun
forall (uni :: * -> *) fun.
Spine (CkValue uni fun) -> Context uni fun -> Context uni fun
transferSpine Spine (CkValue uni fun)
xs Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
f
evalBuiltinApp
:: Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
evalBuiltinApp :: forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
evalBuiltinApp Context uni fun
stack Term TyName Name uni fun ()
term BuiltinRuntime (CkValue uni fun)
runtime = case BuiltinRuntime (CkValue uni fun)
runtime of
BuiltinCostedResult ExBudgetStream
_ BuiltinResult (HeadSpine (CkValue uni fun))
getFXs -> case BuiltinResult (HeadSpine (CkValue uni fun))
getFXs of
BuiltinSuccess HeadSpine (CkValue uni fun)
fXs -> Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
returnCkHeadSpine Context uni fun
stack HeadSpine (CkValue uni fun)
fXs
BuiltinSuccessWithLogs DList Text
logs HeadSpine (CkValue uni fun)
fXs -> DList Text -> CkM uni fun s ()
forall (uni :: * -> *) fun s. DList Text -> CkM uni fun s ()
emitCkM DList Text
logs CkM uni fun s ()
-> CkM uni fun s (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b.
ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
b
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> HeadSpine (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
returnCkHeadSpine Context uni fun
stack HeadSpine (CkValue uni fun)
fXs
BuiltinFailure DList Text
logs BuiltinError
err -> DList Text -> CkM uni fun s ()
forall (uni :: * -> *) fun s. DList Text -> CkM uni fun s ()
emitCkM DList Text
logs CkM uni fun s ()
-> CkM uni fun s (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b.
ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
a
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
b
-> ReaderT
(CkEnv uni fun s)
(ExceptT (CkEvaluationException uni fun) (ST s))
b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Term TyName Name uni fun ()
-> BuiltinError -> CkM uni fun s (Term TyName Name uni fun ())
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m,
AsUnliftingEvaluationError err, AsEvaluationFailure err) =>
cause -> BuiltinError -> m void
throwBuiltinErrorWithCause Term TyName Name uni fun ()
term BuiltinError
err
BuiltinRuntime (CkValue uni fun)
_ -> Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun) -> CkValue uni fun
forall (uni :: * -> *) fun.
Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun) -> CkValue uni fun
VBuiltin Term TyName Name uni fun ()
term BuiltinRuntime (CkValue uni fun)
runtime
instantiateEvaluate
:: Context uni fun
-> Type TyName uni ()
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
instantiateEvaluate :: forall (uni :: * -> *) fun s.
Context uni fun
-> Type TyName uni ()
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
instantiateEvaluate Context uni fun
stack Type TyName uni ()
ty (VTyAbs TyName
tn Kind ()
_k Term TyName Name uni fun ()
body) =
Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> TyName
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname (uni :: * -> *) a name fun.
Eq tyname =>
tyname
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
termSubstClosedType TyName
tn Type TyName uni ()
ty Term TyName Name uni fun ()
body
instantiateEvaluate Context uni fun
stack Type TyName uni ()
ty (VBuiltin Term TyName Name uni fun ()
term BuiltinRuntime (CkValue uni fun)
runtime) = do
let term' :: Term TyName Name uni fun ()
term' = ()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name uni fun ()
term Type TyName uni ()
ty
case BuiltinRuntime (CkValue uni fun)
runtime of
BuiltinExpectForce BuiltinRuntime (CkValue uni fun)
runtime' -> Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
evalBuiltinApp Context uni fun
stack Term TyName Name uni fun ()
term' BuiltinRuntime (CkValue uni fun)
runtime'
BuiltinRuntime (CkValue uni fun)
_ -> AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
BuiltinTermArgumentExpectedMachineError (Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just Term TyName Name uni fun ()
term')
instantiateEvaluate Context uni fun
_ Type TyName uni ()
_ CkValue uni fun
val =
AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonPolymorphicInstantiationMachineError (Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ()))
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just (Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
val
applyEvaluate
:: Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate :: forall (uni :: * -> *) fun s.
Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate Context uni fun
stack (VLamAbs Name
name Type TyName uni ()
_ Term TyName Name uni fun ()
body) CkValue uni fun
arg =
Context uni fun
stack Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Name
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall name tyname (uni :: * -> *) fun a.
Eq name =>
name
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
termSubstClosedTerm Name
name (CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
arg) Term TyName Name uni fun ()
body
applyEvaluate Context uni fun
stack (VBuiltin Term TyName Name uni fun ()
term BuiltinRuntime (CkValue uni fun)
runtime) CkValue uni fun
arg = do
let argTerm :: Term TyName Name uni fun ()
argTerm = CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
arg
term' :: Term TyName Name uni fun ()
term' = ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name uni fun ()
term Term TyName Name uni fun ()
argTerm
case BuiltinRuntime (CkValue uni fun)
runtime of
BuiltinExpectArgument CkValue uni fun -> BuiltinRuntime (CkValue uni fun)
f -> do
Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
evalBuiltinApp Context uni fun
stack Term TyName Name uni fun ()
term' (BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ()))
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> BuiltinRuntime (CkValue uni fun)
f CkValue uni fun
arg
BuiltinRuntime (CkValue uni fun)
_ ->
AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
UnexpectedBuiltinTermArgumentMachineError (Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just Term TyName Name uni fun ()
term')
applyEvaluate Context uni fun
_ CkValue uni fun
val CkValue uni fun
_ =
AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
-> MachineError fun
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
Prism'
(EvaluationError (MachineError fun) CkUserError) (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonFunctionalApplicationMachineError (Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ()))
-> Maybe (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun () -> Maybe (Term TyName Name uni fun ())
forall a. a -> Maybe a
Just (Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Maybe (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ CkValue uni fun -> Term TyName Name uni fun ()
forall (uni :: * -> *) fun.
CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm CkValue uni fun
val
runCk
:: BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either (CkEvaluationException uni fun) (Term TyName Name uni fun ()), [Text])
runCk :: forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
runCk BuiltinsRuntime fun (CkValue uni fun)
runtime Bool
emitting Term TyName Name uni fun ()
term = BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> (forall {s}. CkM uni fun s (Term TyName Name uni fun ()))
-> (Either
(ErrorWithCause
(EvaluationError (MachineError fun) CkUserError)
(Term TyName Name uni fun ()))
(Term TyName Name uni fun ()),
[Text])
forall fun (uni :: * -> *) a.
BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> (forall s. CkM uni fun s a)
-> (Either (CkEvaluationException uni fun) a, [Text])
runCkM BuiltinsRuntime fun (CkValue uni fun)
runtime Bool
emitting ((forall {s}. CkM uni fun s (Term TyName Name uni fun ()))
-> (Either
(ErrorWithCause
(EvaluationError (MachineError fun) CkUserError)
(Term TyName Name uni fun ()))
(Term TyName Name uni fun ()),
[Text]))
-> (forall {s}. CkM uni fun s (Term TyName Name uni fun ()))
-> (Either
(ErrorWithCause
(EvaluationError (MachineError fun) CkUserError)
(Term TyName Name uni fun ()))
(Term TyName Name uni fun ()),
[Text])
forall a b. (a -> b) -> a -> b
$ [] [Frame uni fun]
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (uni :: * -> *) fun s.
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
term
evaluateCk
:: BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> (Either (CkEvaluationException uni fun) (Term TyName Name uni fun ()), [Text])
evaluateCk :: forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
evaluateCk BuiltinsRuntime fun (CkValue uni fun)
runtime = BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
runCk BuiltinsRuntime fun (CkValue uni fun)
runtime Bool
True
evaluateCkNoEmit
:: BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit :: forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit BuiltinsRuntime fun (CkValue uni fun)
runtime = (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ())
forall a b. (a, b) -> a
fst ((Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text]))
-> Term TyName Name uni fun ()
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Bool
-> Term TyName Name uni fun ()
-> (Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()),
[Text])
runCk BuiltinsRuntime fun (CkValue uni fun)
runtime Bool
False
readKnownCk
:: ReadKnown (Term TyName Name uni fun ()) a
=> BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) a
readKnownCk :: forall (uni :: * -> *) fun a.
ReadKnown (Term TyName Name uni fun ()) a =>
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) a
readKnownCk BuiltinsRuntime fun (CkValue uni fun)
runtime = BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ())
forall fun (uni :: * -> *).
BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ())
evaluateCkNoEmit BuiltinsRuntime fun (CkValue uni fun)
runtime (Term TyName Name uni fun ()
-> Either
(CkEvaluationException uni fun) (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) a)
-> Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Term TyName Name uni fun ()
-> Either (CkEvaluationException uni fun) a
forall val a err.
(ReadKnown val a, AsUnliftingEvaluationError err,
AsEvaluationFailure err) =>
val -> Either (ErrorWithCause err val) a
readKnownSelf