-- | The CK machine.

{-# LANGUAGE DeriveAnyClass            #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

module PlutusCore.Evaluation.Machine.Ck
    ( EvaluationResult (..)
    , CkEvaluationException
    , CkM
    , CkValue
    , extractEvaluationResult
    , runCk
    , evaluateCk
    , evaluateCkNoEmit
    , unsafeEvaluateCk
    , unsafeEvaluateCkNoEmit
    , readKnownCk
    ) where

import PlutusPrelude

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import PlutusCore.Name
import PlutusCore.Pretty (PrettyConfigPlc, PrettyConst)

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.ST
import Data.Array
import Data.DList (DList)
import Data.DList qualified as DList
import Data.STRef
import Data.Text (Text)
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))
    deriving stock (Int -> CkValue uni fun -> ShowS
[CkValue uni fun] -> ShowS
CkValue uni fun -> String
(Int -> CkValue uni fun -> ShowS)
-> (CkValue uni fun -> String)
-> ([CkValue uni fun] -> ShowS)
-> Show (CkValue uni fun)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> CkValue uni fun -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CkValue uni fun] -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CkValue uni fun -> String
showList :: [CkValue uni fun] -> ShowS
$cshowList :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CkValue uni fun] -> ShowS
show :: CkValue uni fun -> String
$cshow :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CkValue uni fun -> String
showsPrec :: Int -> CkValue uni fun -> ShowS
$cshowsPrec :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> CkValue uni fun -> ShowS
Show)

-- | Take pieces of a possibly partial builtin application and either create a 'CkValue' using
-- 'makeKnown' or a partial builtin application depending on whether the built-in function is
-- fully saturated or not.
evalBuiltinApp
    :: Term TyName Name uni fun ()
    -> BuiltinRuntime (CkValue uni fun)
    -> CkM uni fun s (CkValue uni fun)
evalBuiltinApp :: Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp Term TyName Name uni fun ()
term runtime :: BuiltinRuntime (CkValue uni fun)
runtime@(BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CkValue uni fun) n
getX ToCostingType n
_) = case RuntimeScheme n
sch of
    RuntimeScheme n
RuntimeSchemeResult -> do
        let (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun)
errOrRes, DList Text
logs) = Emitter
  (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun),
    DList Text)
forall a. Emitter a -> (a, DList Text)
runEmitter (Emitter
   (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun))
 -> (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun),
     DList Text))
-> Emitter
     (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun),
    DList Text)
forall a b. (a -> b) -> a -> b
$ ExceptT
  (ErrorWithCause KnownTypeError ()) Emitter (CkValue uni fun)
-> Emitter
     (Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT
  (ErrorWithCause KnownTypeError ()) Emitter (CkValue uni fun)
ToRuntimeDenotationType (CkValue uni fun) n
getX
        DList Text -> CkM uni fun s ()
forall (uni :: * -> *) fun s. DList Text -> CkM uni fun s ()
emitCkM DList Text
logs
        case Either (ErrorWithCause KnownTypeError ()) (CkValue uni fun)
errOrRes of
            Left ErrorWithCause KnownTypeError ()
err  -> ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
-> CkM uni fun s (CkValue uni fun)
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err,
 AsEvaluationFailure err) =>
ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause (ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
 -> CkM uni fun s (CkValue uni fun))
-> ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
-> CkM uni fun s (CkValue uni fun)
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
term Term TyName Name uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
            Right CkValue uni fun
res -> CkValue uni fun -> CkM uni fun s (CkValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CkValue uni fun
res
    RuntimeScheme n
_ -> CkValue uni fun -> CkM uni fun s (CkValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CkValue uni fun -> CkM uni fun s (CkValue uni fun))
-> CkValue uni fun -> CkM uni fun s (CkValue uni fun)
forall a b. (a -> b) -> a -> b
$ 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

ckValueToTerm :: CkValue uni fun -> Term TyName Name uni fun ()
ckValueToTerm :: 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

data CkEnv uni fun s = CkEnv
    { 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".
    , CkEnv uni fun s -> Maybe (STRef s (DList Text))
ckEnvMayEmitRef :: Maybe (STRef s (DList Text))
    }

instance (Closed uni, GShow uni, uni `Everywhere` PrettyConst, Pretty fun) =>
            PrettyBy PrettyConfigPlc (CkValue uni fun) where
    prettyBy :: PrettyConfigPlc -> CkValue uni fun -> Doc ann
prettyBy PrettyConfigPlc
cfg = 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
showList :: [CkUserError] -> ShowS
$cshowList :: [CkUserError] -> ShowS
show :: CkUserError -> String
$cshow :: CkUserError -> String
showsPrec :: Int -> CkUserError -> ShowS
$cshowsPrec :: Int -> CkUserError -> ShowS
Show, CkUserError -> CkUserError -> Bool
(CkUserError -> CkUserError -> Bool)
-> (CkUserError -> CkUserError -> Bool) -> Eq CkUserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CkUserError -> CkUserError -> Bool
$c/= :: CkUserError -> CkUserError -> Bool
== :: CkUserError -> CkUserError -> Bool
$c== :: 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
$cto :: forall x. Rep CkUserError x -> CkUserError
$cfrom :: forall x. CkUserError -> Rep CkUserError x
Generic)
    deriving anyclass (CkUserError -> ()
(CkUserError -> ()) -> NFData CkUserError
forall a. (a -> ()) -> NFData a
rnf :: CkUserError -> ()
$crnf :: CkUserError -> ()
NFData)

-- | The CK machine-specific 'EvaluationException'.
type CkEvaluationException uni fun =
    EvaluationException CkUserError (MachineError fun) (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 :: p () (f ()) -> p CkUserError (f CkUserError)
_EvaluationFailure = CkUserError -> Prism' CkUserError ()
forall err. Eq err => err -> Prism' err ()
_EvaluationFailureVia CkUserError
CkEvaluationFailure

instance Pretty CkUserError where
    pretty :: 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 :: 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 (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 (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 (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 :: Maybe cause
-> CkValue uni fun
-> Either
     (ErrorWithCause err cause)
     (Some (ValueOf (UniOf (CkValue uni fun))))
asConstant Maybe cause
_        (VCon Some (ValueOf uni)
val) = Some (ValueOf uni)
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Some (ValueOf uni)
val
    asConstant Maybe cause
mayCause CkValue uni fun
_          = Maybe cause
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall err cause (m :: * -> *) r.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err) =>
Maybe cause -> m r
throwNotAConstant Maybe cause
mayCause

    fromConstant :: Some (ValueOf (UniOf (CkValue uni fun))) -> CkValue uni fun
fromConstant = Some (ValueOf (UniOf (CkValue uni fun))) -> CkValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CkValue uni fun
VCon

data Frame uni fun
    = FrameApplyFun (CkValue uni fun)                       -- ^ @[V _]@
    | FrameApplyArg (Term TyName Name uni fun ())           -- ^ @[_ N]@
    | FrameTyInstArg (Type TyName uni ())                   -- ^ @{_ A}@
    | FrameUnwrap                                           -- ^ @(unwrap _)@
    | FrameIWrap (Type TyName uni ()) (Type TyName uni ())  -- ^ @(iwrap A B _)@

type Context uni fun = [Frame uni fun]

runCkM
    :: 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)
-> 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 (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure (Either (CkEvaluationException uni fun) a
errOrRes, [Text]
logs)

-- | Substitute a 'Term' for a variable in a 'Term' that can contain duplicate binders.
-- Do not descend under binders that bind the same variable as the one we're substituting for.
substituteDb
    :: Eq name
    => name -> Term tyname name uni fun () -> Term tyname name uni fun () -> Term tyname name uni fun ()
substituteDb :: name
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
substituteDb name
varFor Term tyname name uni fun ()
new = Term tyname name uni fun () -> Term tyname name uni fun ()
go where
    go :: Term tyname name uni fun () -> Term tyname name uni fun ()
go = \case
         Var      () name
var          -> if name
var name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
varFor then Term tyname name uni fun ()
new else () -> name -> Term tyname name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () name
var
         TyAbs    () tyname
tyn Kind ()
ty 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
tyn Kind ()
ty (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
body)
         LamAbs   () name
var 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
var Type tyname uni ()
ty (name -> Term tyname name uni fun () -> Term tyname name uni fun ()
goUnder name
var Term tyname name uni fun ()
body)
         Apply    () Term tyname name uni fun ()
fun Term tyname name uni fun ()
arg      -> ()
-> 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 tyname name uni fun ()
go Term tyname name uni fun ()
fun) (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
arg)
         Constant () Some (ValueOf uni)
constant     -> () -> 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)
constant
         TyInst   () Term tyname name uni fun ()
fun Type tyname uni ()
arg      -> ()
-> 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 tyname name uni fun ()
go Term tyname name uni fun ()
fun) Type tyname uni ()
arg
         Unwrap   () Term tyname name uni fun ()
term         -> () -> 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
Unwrap   () (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term)
         IWrap    () Type tyname uni ()
pat Type tyname uni ()
arg Term tyname name uni fun ()
term -> ()
-> 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 ()
pat Type tyname uni ()
arg (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term)
         b :: Term tyname name uni fun ()
b@Builtin{}              -> Term tyname name uni fun ()
b
         e :: Term tyname name uni fun ()
e@Error  {}              -> Term tyname name uni fun ()
e
    goUnder :: name -> Term tyname name uni fun () -> Term tyname name uni fun ()
goUnder name
var Term tyname name uni fun ()
term = if name
var name -> name -> Bool
forall a. Eq a => a -> a -> Bool
== name
varFor then Term tyname name uni fun ()
term else Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term

-- | Substitute a 'Type' for a type variable in a 'Term' that can contain duplicate binders.
-- Do not descend under binders that bind the same type variable as the one we're substituting for.
substTyInTerm
    :: Eq tyname
    => tyname -> Type tyname uni () -> Term tyname name uni fun () -> Term tyname name uni fun ()
substTyInTerm :: tyname
-> Type tyname uni ()
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
substTyInTerm tyname
tn0 Type tyname uni ()
ty0 = Term tyname name uni fun () -> Term tyname name uni fun ()
go where
    go :: Term tyname name uni fun () -> Term tyname name uni fun ()
go = \case
         v :: Term tyname name uni fun ()
v@Var{}                 -> Term tyname name uni fun ()
v
         c :: Term tyname name uni fun ()
c@Constant{}            -> Term tyname name uni fun ()
c
         b :: Term tyname name uni fun ()
b@Builtin{}             -> Term tyname name uni fun ()
b
         TyAbs   () tyname
tn Kind ()
ty 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 ()
ty (tyname
-> Term tyname name uni fun () -> Term tyname name uni fun ()
goUnder tyname
tn Term tyname name uni fun ()
body)
         LamAbs  () name
var 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
var (Type tyname uni () -> Type tyname uni ()
goTy Type tyname uni ()
ty) (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
body)
         Apply   () Term tyname name uni fun ()
fun Term tyname name uni fun ()
arg      -> ()
-> 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 tyname name uni fun ()
go Term tyname name uni fun ()
fun) (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
arg)
         TyInst  () Term tyname name uni fun ()
fun Type tyname uni ()
ty       -> ()
-> 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 tyname name uni fun ()
go Term tyname name uni fun ()
fun) (Type tyname uni () -> Type tyname uni ()
goTy Type tyname uni ()
ty)
         Unwrap  () Term tyname name uni fun ()
term         -> () -> 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
Unwrap  () (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term)
         IWrap   () Type tyname uni ()
pat Type tyname uni ()
arg Term tyname name uni fun ()
term -> ()
-> 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 () -> Type tyname uni ()
goTy Type tyname uni ()
pat) (Type tyname uni () -> Type tyname uni ()
goTy Type tyname uni ()
arg) (Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term)
         Error   () Type tyname uni ()
ty           -> () -> Type tyname uni () -> Term tyname name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error   () (Type tyname uni () -> Type tyname uni ()
goTy Type tyname uni ()
ty)
    goUnder :: tyname
-> Term tyname name uni fun () -> Term tyname name uni fun ()
goUnder tyname
tn Term tyname name uni fun ()
term = if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Term tyname name uni fun ()
term else Term tyname name uni fun () -> Term tyname name uni fun ()
go Term tyname name uni fun ()
term
    goTy :: Type tyname uni () -> Type tyname uni ()
goTy = tyname
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *).
Eq tyname =>
tyname
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
substTyInTy tyname
tn0 Type tyname uni ()
ty0

-- | Substitute a 'Type' for a type variable in a 'Type' that can contain duplicate binders.
-- Do not descend under binders that bind the same type variable as the one we're substituting for.
substTyInTy
    :: Eq tyname
    => tyname -> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
substTyInTy :: tyname
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
substTyInTy tyname
tn0 Type tyname uni ()
ty0 = Type tyname uni () -> Type tyname uni ()
go where
    go :: Type tyname uni () -> Type tyname uni ()
go = \case
         TyVar    () tyname
tn      -> if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Type tyname uni ()
ty0 else () -> tyname -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () tyname
tn
         TyFun    () Type tyname uni ()
ty1 Type tyname uni ()
ty2 -> ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun    () (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty1) (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty2)
         TyIFix   () Type tyname uni ()
ty1 Type tyname uni ()
ty2 -> ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix   () (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty1) (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty2)
         TyApp    () Type tyname uni ()
ty1 Type tyname uni ()
ty2 -> ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp    () (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty1) (Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty2)
         TyForall () tyname
tn Kind ()
k Type tyname uni ()
ty -> () -> tyname -> Kind () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () tyname
tn Kind ()
k (tyname -> Type tyname uni () -> Type tyname uni ()
goUnder tyname
tn Type tyname uni ()
ty)
         TyLam    () tyname
tn Kind ()
k Type tyname uni ()
ty -> () -> tyname -> Kind () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam    () tyname
tn Kind ()
k (tyname -> Type tyname uni () -> Type tyname uni ()
goUnder tyname
tn Type tyname uni ()
ty)
         bt :: Type tyname uni ()
bt@TyBuiltin{}      -> Type tyname uni ()
bt
    goUnder :: tyname -> Type tyname uni () -> Type tyname uni ()
goUnder tyname
tn Type tyname uni ()
ty = if tyname
tn tyname -> tyname -> Bool
forall a. Eq a => a -> a -> Bool
== tyname
tn0 then Type tyname uni ()
ty else Type tyname uni () -> Type tyname uni ()
go Type tyname uni ()
ty

-- 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 ▷ error A    ↦ ◆
(|>)
    :: Ix fun
    => Context uni fun -> Term TyName Name uni fun () -> CkM uni fun s (Term TyName Name uni fun ())
Context uni fun
stack |> :: 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 fun (uni :: * -> *) s.
Ix fun =>
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
FrameApplyArg 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 fun (uni :: * -> *) s.
Ix fun =>
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 fun (uni :: * -> *) s.
Ix fun =>
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 fun (uni :: * -> *) s.
Ix fun =>
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 fun (uni :: * -> *) s.
Ix fun =>
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 fun (uni :: * -> *) s.
Ix fun =>
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 <- (CkEnv uni fun s
 -> ReaderT
      (CkEnv uni fun s)
      (ExceptT (CkEvaluationException uni fun) (ST s))
      (BuiltinRuntime (CkValue uni fun)))
-> ReaderT
     (CkEnv uni fun s)
     (ExceptT (CkEvaluationException uni fun) (ST s))
     (BuiltinRuntime (CkValue uni fun))
forall r (m :: * -> *) a. MonadReader r m => (r -> m a) -> m a
asksM ((CkEnv uni fun s
  -> ReaderT
       (CkEnv uni fun s)
       (ExceptT (CkEvaluationException uni fun) (ST s))
       (BuiltinRuntime (CkValue uni fun)))
 -> ReaderT
      (CkEnv uni fun s)
      (ExceptT (CkEvaluationException uni fun) (ST s))
      (BuiltinRuntime (CkValue uni fun)))
-> (CkEnv uni fun s
    -> ReaderT
         (CkEnv uni fun s)
         (ExceptT (CkEvaluationException uni fun) (ST s))
         (BuiltinRuntime (CkValue uni fun)))
-> ReaderT
     (CkEnv uni fun s)
     (ExceptT (CkEvaluationException uni fun) (ST s))
     (BuiltinRuntime (CkValue uni fun))
forall a b. (a -> b) -> a -> b
$ fun
-> BuiltinsRuntime fun (CkValue uni fun)
-> ReaderT
     (CkEnv uni fun s)
     (ExceptT (CkEvaluationException uni fun) (ST s))
     (BuiltinRuntime (CkValue uni fun))
forall err cause (m :: * -> *) fun val.
(MonadError (ErrorWithCause err cause) m, AsMachineError err fun,
 Ix fun) =>
fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val)
lookupBuiltin fun
bn (BuiltinsRuntime fun (CkValue uni fun)
 -> ReaderT
      (CkEnv uni fun s)
      (ExceptT (CkEvaluationException uni fun) (ST s))
      (BuiltinRuntime (CkValue uni fun)))
-> (CkEnv uni fun s -> BuiltinsRuntime fun (CkValue uni fun))
-> CkEnv uni fun s
-> ReaderT
     (CkEnv uni fun s)
     (ExceptT (CkEvaluationException uni fun) (ST 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
    Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
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 fun (uni :: * -> *) s.
Ix fun =>
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
_     |> Error{}                 =
    AReview
  (EvaluationError CkUserError (MachineError fun))
  (EvaluationError CkUserError (MachineError fun))
-> EvaluationError CkUserError (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 CkUserError (MachineError fun))
  (EvaluationError CkUserError (MachineError fun))
forall r user internal.
AsEvaluationError r user internal =>
Prism' r (EvaluationError user internal)
_EvaluationError (CkUserError -> EvaluationError CkUserError (MachineError fun)
forall user internal. user -> EvaluationError user internal
UserEvaluationError 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 CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (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 , [(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
(<|)
    :: Ix fun
    => Context uni fun -> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
[]                         <| :: Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
val     = Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name uni fun ()
 -> CkM uni fun s (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> CkM uni fun 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  : Context uni fun
stack <| CkValue uni fun
fun     = Context uni fun
-> Type TyName uni ()
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
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 CkValue uni fun
fun
FrameApplyArg Term TyName Name uni fun ()
arg  : Context uni fun
stack <| CkValue uni fun
fun     = CkValue uni fun -> Frame uni fun
forall (uni :: * -> *) fun. CkValue uni fun -> Frame uni fun
FrameApplyFun CkValue uni fun
fun 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 fun (uni :: * -> *) s.
Ix fun =>
Context uni fun
-> Term TyName Name uni fun ()
-> CkM uni fun s (Term TyName Name uni fun ())
|> Term TyName Name uni fun ()
arg
FrameApplyFun CkValue uni fun
fun  : Context uni fun
stack <| CkValue uni fun
arg     = Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
Context uni fun
-> CkValue uni fun
-> CkValue uni fun
-> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate Context uni fun
stack CkValue uni fun
fun CkValue uni fun
arg
FrameIWrap Type TyName uni ()
pat Type TyName uni ()
arg : Context uni fun
stack <| CkValue uni fun
value   = Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
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        : Context uni fun
stack <| CkValue uni fun
wrapped = case CkValue uni fun
wrapped of
    VIWrap Type TyName uni ()
_ Type TyName uni ()
_ CkValue uni fun
term -> Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
term
    CkValue uni fun
_               ->
        AReview
  (EvaluationError CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonWrapUnwrappedMachineError (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
wrapped

-- | 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
    :: Ix fun
    => Context uni fun
    -> Type TyName uni ()
    -> CkValue uni fun
    -> CkM uni fun s (Term TyName Name uni fun ())
instantiateEvaluate :: 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 fun (uni :: * -> *) s.
Ix fun =>
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 :: * -> *) name fun.
Eq tyname =>
tyname
-> Type tyname uni ()
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
substTyInTerm TyName
tn Type TyName uni ()
ty Term TyName Name uni fun ()
body -- No kind check - too expensive at run time.
instantiateEvaluate Context uni fun
stack Type TyName uni ()
ty (VBuiltin Term TyName Name uni fun ()
term (BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CkValue uni fun) n
f ToCostingType n
exF)) = 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 RuntimeScheme n
sch 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.
        RuntimeSchemeAll RuntimeScheme n
schK -> do
            let runtime' :: BuiltinRuntime (CkValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CkValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CkValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schK ToRuntimeDenotationType (CkValue uni fun) n
f ToCostingType n
exF
            CkValue uni fun
res <- Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
forall (uni :: * -> *) fun s.
Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp Term TyName Name uni fun ()
term' BuiltinRuntime (CkValue uni fun)
runtime'
            Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
res
        RuntimeScheme n
_ -> AReview
  (EvaluationError CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (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 CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (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
    :: Ix fun
    => Context uni fun
    -> CkValue uni fun
    -> CkValue uni fun
    -> CkM uni fun s (Term TyName Name uni fun ())
applyEvaluate :: 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 fun (uni :: * -> *) s.
Ix fun =>
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.
Eq name =>
name
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
-> Term tyname name uni fun ()
substituteDb 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 RuntimeScheme n
sch ToRuntimeDenotationType (CkValue uni fun) n
f ToCostingType n
exF)) 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 RuntimeScheme n
sch of
        -- It's only possible to apply a builtin application if the builtin expects a term
        -- argument next.
        RuntimeSchemeArrow RuntimeScheme n
schB -> case ToRuntimeDenotationType (CkValue uni fun) n
CkValue uni fun
-> ReadKnownM () (ToRuntimeDenotationType (CkValue uni fun) n)
f CkValue uni fun
arg of
            Left ErrorWithCause KnownTypeError ()
err -> ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
-> CkM uni fun s (Term TyName Name uni fun ())
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err,
 AsEvaluationFailure err) =>
ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause (ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
 -> CkM uni fun s (Term TyName Name uni fun ()))
-> ErrorWithCause KnownTypeError (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 ()
argTerm Term TyName Name uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term TyName Name uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
            Right ToRuntimeDenotationType (CkValue uni fun) n
y  -> do
                -- The CK machine does not support costing, so we just apply the costing function
                -- to 'mempty'.
                let runtime' :: BuiltinRuntime (CkValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CkValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CkValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schB ToRuntimeDenotationType (CkValue uni fun) n
y (ToCostingType n
ExMemory -> ToCostingType n
exF ExMemory
forall a. Monoid a => a
mempty)
                CkValue uni fun
res <- Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
forall (uni :: * -> *) fun s.
Term TyName Name uni fun ()
-> BuiltinRuntime (CkValue uni fun)
-> CkM uni fun s (CkValue uni fun)
evalBuiltinApp Term TyName Name uni fun ()
term' BuiltinRuntime (CkValue uni fun)
runtime'
                Context uni fun
stack Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
forall fun (uni :: * -> *) s.
Ix fun =>
Context uni fun
-> CkValue uni fun -> CkM uni fun s (Term TyName Name uni fun ())
<| CkValue uni fun
res
        RuntimeScheme n
_ ->
            AReview
  (EvaluationError CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (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 CkUserError (MachineError fun)) (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 CkUserError (MachineError fun)) (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (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
    :: Ix fun
    => 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)
-> 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
      (CkEvaluationException 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
       (CkEvaluationException uni fun) (Term TyName Name uni fun ()),
     [Text]))
-> (forall s. CkM uni fun s (Term TyName Name uni fun ()))
-> (Either
      (CkEvaluationException 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 fun (uni :: * -> *) s.
Ix fun =>
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
    :: Ix fun
    => 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)
-> 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 :: * -> *).
Ix fun =>
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
    :: Ix fun
    => 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)
-> 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 :: * -> *).
Ix fun =>
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

-- | Evaluate a term using the CK machine with logging enabled. May throw a 'CkEvaluationException'.
unsafeEvaluateCk
    :: ( GShow uni, Closed uni
       , Typeable uni, Typeable fun, uni `Everywhere` PrettyConst
       , Pretty fun, Ix fun
       )
    => BuiltinsRuntime fun (CkValue uni fun)
    -> Term TyName Name uni fun ()
    -> (EvaluationResult (Term TyName Name uni fun ()), [Text])
unsafeEvaluateCk :: BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> (EvaluationResult (Term TyName Name uni fun ()), [Text])
unsafeEvaluateCk BuiltinsRuntime fun (CkValue uni fun)
runtime = (Either
   (EvaluationException
      CkUserError (MachineError fun) (Term TyName Name uni fun ()))
   (Term TyName Name uni fun ())
 -> EvaluationResult (Term TyName Name uni fun ()))
-> (Either
      (EvaluationException
         CkUserError (MachineError fun) (Term TyName Name uni fun ()))
      (Term TyName Name uni fun ()),
    [Text])
-> (EvaluationResult (Term TyName Name uni fun ()), [Text])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Either
  (EvaluationException
     CkUserError (MachineError fun) (Term TyName Name uni fun ()))
  (Term TyName Name uni fun ())
-> EvaluationResult (Term TyName Name uni fun ())
forall internal term user a.
(PrettyPlc internal, PrettyPlc term, Typeable internal,
 Typeable term) =>
Either (EvaluationException user internal term) a
-> EvaluationResult a
unsafeExtractEvaluationResult ((Either
    (EvaluationException
       CkUserError (MachineError fun) (Term TyName Name uni fun ()))
    (Term TyName Name uni fun ()),
  [Text])
 -> (EvaluationResult (Term TyName Name uni fun ()), [Text]))
-> (Term TyName Name uni fun ()
    -> (Either
          (EvaluationException
             CkUserError (MachineError fun) (Term TyName Name uni fun ()))
          (Term TyName Name uni fun ()),
        [Text]))
-> Term TyName Name uni fun ()
-> (EvaluationResult (Term TyName Name uni fun ()), [Text])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> (Either
      (EvaluationException
         CkUserError (MachineError fun) (Term TyName Name uni fun ()))
      (Term TyName Name uni fun ()),
    [Text])
forall fun (uni :: * -> *).
Ix fun =>
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

-- | Evaluate a term using the CK machine with logging disabled. May throw a 'CkEvaluationException'.
unsafeEvaluateCkNoEmit
    :: ( GShow uni, Closed uni
       , Typeable uni, Typeable fun, uni `Everywhere` PrettyConst
       , Pretty fun, Ix fun
       )
    => BuiltinsRuntime fun (CkValue uni fun)
    -> Term TyName Name uni fun ()
    -> EvaluationResult (Term TyName Name uni fun ())
unsafeEvaluateCkNoEmit :: BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> EvaluationResult (Term TyName Name uni fun ())
unsafeEvaluateCkNoEmit BuiltinsRuntime fun (CkValue uni fun)
runtime = Either
  (EvaluationException
     CkUserError (MachineError fun) (Term TyName Name uni fun ()))
  (Term TyName Name uni fun ())
-> EvaluationResult (Term TyName Name uni fun ())
forall internal term user a.
(PrettyPlc internal, PrettyPlc term, Typeable internal,
 Typeable term) =>
Either (EvaluationException user internal term) a
-> EvaluationResult a
unsafeExtractEvaluationResult (Either
   (EvaluationException
      CkUserError (MachineError fun) (Term TyName Name uni fun ()))
   (Term TyName Name uni fun ())
 -> EvaluationResult (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun ()
    -> Either
         (EvaluationException
            CkUserError (MachineError fun) (Term TyName Name uni fun ()))
         (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> EvaluationResult (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinsRuntime fun (CkValue uni fun)
-> Term TyName Name uni fun ()
-> Either
     (EvaluationException
        CkUserError (MachineError fun) (Term TyName Name uni fun ()))
     (Term TyName Name uni fun ())
forall fun (uni :: * -> *).
Ix fun =>
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

-- | Unlift a value using the CK machine.
readKnownCk
    :: (Ix fun, 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)
-> 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 :: * -> *).
Ix fun =>
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, AsUnliftingError err, AsEvaluationFailure err) =>
val -> Either (ErrorWithCause err val) a
readKnownSelf