-- editorconfig-checker-disable-file
-- | The CK machine.

{-# 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 |>, <|

-- See Note [Show instance for BuiltinRuntime] in the CEK machine.
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)
    -- 'Nothing' means no logging. 'DList' is due to the fact that we need efficient append
    -- as we store logs as "latest go last".
    , 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 -- Error has been called or a builtin application has failed
    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)

-- | The CK machine-specific 'EvaluationException'.
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'."

-- The 'DList' is just be consistent with the CEK machine (see Note [DList-based emitting]).
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)                       -- ^ @[V _]@
    | FrameAwaitFunTerm (Term TyName Name uni fun ())       -- ^ @[_ N]@
    | FrameAwaitFunValue (CkValue uni fun)                  -- ^ @[_ V]@
    | FrameTyInstArg (Type TyName uni ())                   -- ^ @{_ A}@
    | FrameUnwrap                                           -- ^ @(unwrap _)@
    | FrameIWrap (Type TyName uni ()) (Type TyName uni ())  -- ^ @(iwrap A B _)@
    | 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]

-- See Note [ExMemoryUsage instances for non-constants].
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)

-- FIXME: make sure that the specification is up to date and that this matches.
-- | The computing part of the CK machine. Rules are as follows:
--
-- > s ▷ {M A}      ↦ s , {_ A}        ▷ M
-- > s ▷ [M N]      ↦ s , [_ N]        ▷ M
-- > s ▷ wrap α A M ↦ s , (wrap α S _) ▷ M
-- > s ▷ unwrap M   ↦ s , (unwrap _)   ▷ M
-- > s ▷ abs α K M  ↦ s ◁ abs α K M
-- > s ▷ lam x A M  ↦ s ◁ lam x A M
-- > s ▷ builtin bn ↦ s ◁ builtin (Builtin () bn) (runtimeOf bn)
-- > s ▷ con cn     ↦ s ◁ con cn
-- > s ▻ constr I T0 .. Tn ↦ s , (constr I _ T1 Tn) ▻ T0
-- > s ▻ case S C0 ... Cn ↦ s , (case _ C0 ... Cn) ▻ S
-- > s ▷ error A    ↦ ◆
(|>)
    :: 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

-- FIXME: make sure that the specification is up to date and that this matches.
-- | The returning part of the CK machine. Rules are as follows:
--
-- > s , {_ A}           ◁ abs α K M  ↦ s         ▷ {A/α}M
-- > s , [_ N]           ◁ V          ↦ s , [V _] ▷ N
-- > s , [_ V1 ... Vm]   ◁ (lam x A M) ↦ s , [_ V2 ... Vm] ▷ [V1/x]M
-- > s , [(lam x A M) _] ◁ V          ↦ s         ▷ [V/x]M
-- > s , {_ A}           ◁ F          ↦ s ◁ {F A}  -- Partially instantiated builtin application.
-- > s , [F _]           ◁ V          ↦ s ◁ [F V]  -- Partially saturated builtin application.
-- > s , [F _]           ◁ V          ↦ s ◁ W      -- Fully saturated builtin application, [F V] ~> W.
-- > s , (wrap α S _)    ◁ V          ↦ s ◁ wrap α S V
-- > s , (unwrap _)      ◁ wrap α A V ↦ s ◁ V
-- > s , (constr I V0 ... Vj-1 _ Tj+1 ... Tn) ◅ Vj ↦ s , (constr i V0 ... Vj _ Tj+2... Tn) ▻ Tj+1
-- > s , (case _ C0 ... CN) ◅ (constr i V1 .. Vm) ↦ s , [_ V1 ... Vm] ▻ Ci
(<|)
    :: 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)

-- | Transfers a 'Spine' onto the stack. The first argument will be at the top of the stack.
--
-- >>> import PlutusCore.Default
-- >>> import PlutusCore.Builtin
-- >>> transferSpine (SpineCons (fromValue (1 :: Integer)) (SpineLast (fromValue (2 :: Integer)))) [FrameUnwrap :: Frame DefaultUni DefaultFun]
-- [FrameAwaitFunValue (VCon (Some (ValueOf DefaultUniInteger 1))),FrameAwaitFunValue (VCon (Some (ValueOf DefaultUniInteger 2))),FrameUnwrap]
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

-- | Evaluate a 'HeadSpine' by pushing the arguments (if any) onto the stack and proceeding with
-- the returning phase of the CK machine, i.e. @<|@.
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

-- | Take a possibly partial builtin application and
--
-- - either create a 'CkValue' by evaluating the application if it's saturated (emitting logs, if
--    any, along the way), potentially failing evaluation
-- - or create a partial builtin application otherwise
--
-- and proceed with the returning phase of the CK machine.
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

-- | Instantiate a term with a type and proceed.
-- In case of 'TyAbs' just ignore the type. Otherwise check if the term is builtin application
-- expecting a type argument, in which case either calculate the builtin application or stick a
-- 'TyInst' on top of its 'Term' representation depending on whether the application is saturated or
-- not. In any other case, fail.
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) =
     -- No kind check - too expensive at run time.
    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
        -- We allow a type argument to appear last in the type of a built-in function,
        -- otherwise we could just assemble a 'VBuiltin' without trying to evaluate the
        -- application.
        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

-- | Apply a function to an argument and proceed.
-- If the function is a lambda, then perform substitution and proceed.
-- If the function is a builtin application then check that it's expecting a term argument,
-- and either calculate the builtin application or stick a 'Apply' on top of its 'Term'
-- representation depending on whether the application is saturated or not.
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
        -- It's only possible to apply a builtin application if the builtin expects a term
        -- argument next.
        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

-- | Evaluate a term using the CK machine with logging enabled.
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

-- | Evaluate a term using the CK machine with logging disabled.
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

-- | Unlift a value using the CK machine.
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