{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NPlusKPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module UntypedPlutusCore.Evaluation.Machine.Cek.Internal
( EvaluationResult(..)
, CekValue(..)
, CekUserError(..)
, CekEvaluationException
, CekBudgetSpender(..)
, ExBudgetInfo(..)
, ExBudgetMode(..)
, CekEmitter
, CekEmitterInfo(..)
, EmitterMode(..)
, CekM (..)
, ErrorWithCause(..)
, EvaluationError(..)
, ExBudgetCategory(..)
, StepKind(..)
, PrettyUni
, extractEvaluationResult
, runCekDeBruijn
, dischargeCekValue
)
where
import ErrorCode
import PlutusPrelude
import UntypedPlutusCore.Core
import Data.DeBruijnEnv as Env
import PlutusCore.Builtin
import PlutusCore.DeBruijn
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExMemory
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Machine.MachineParameters
import PlutusCore.Evaluation.Result
import PlutusCore.Pretty
import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts (..))
import Control.Lens.Review
import Control.Monad.Catch
import Control.Monad.Except
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.Array hiding (index)
import Data.DList (DList)
import Data.Hashable (Hashable)
import Data.Kind qualified as GHC
import Data.Semigroup (stimes)
import Data.Text (Text)
import Data.Word
import Data.Word64Array.Word8 hiding (Index)
import Prettyprinter
import Universe
data StepKind
= BConst
| BVar
| BLamAbs
| BApply
| BDelay
| BForce
| BBuiltin
deriving stock (Int -> StepKind -> ShowS
[StepKind] -> ShowS
StepKind -> String
(Int -> StepKind -> ShowS)
-> (StepKind -> String) -> ([StepKind] -> ShowS) -> Show StepKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StepKind] -> ShowS
$cshowList :: [StepKind] -> ShowS
show :: StepKind -> String
$cshow :: StepKind -> String
showsPrec :: Int -> StepKind -> ShowS
$cshowsPrec :: Int -> StepKind -> ShowS
Show, StepKind -> StepKind -> Bool
(StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool) -> Eq StepKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StepKind -> StepKind -> Bool
$c/= :: StepKind -> StepKind -> Bool
== :: StepKind -> StepKind -> Bool
$c== :: StepKind -> StepKind -> Bool
Eq, Eq StepKind
Eq StepKind
-> (StepKind -> StepKind -> Ordering)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> Bool)
-> (StepKind -> StepKind -> StepKind)
-> (StepKind -> StepKind -> StepKind)
-> Ord StepKind
StepKind -> StepKind -> Bool
StepKind -> StepKind -> Ordering
StepKind -> StepKind -> StepKind
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: StepKind -> StepKind -> StepKind
$cmin :: StepKind -> StepKind -> StepKind
max :: StepKind -> StepKind -> StepKind
$cmax :: StepKind -> StepKind -> StepKind
>= :: StepKind -> StepKind -> Bool
$c>= :: StepKind -> StepKind -> Bool
> :: StepKind -> StepKind -> Bool
$c> :: StepKind -> StepKind -> Bool
<= :: StepKind -> StepKind -> Bool
$c<= :: StepKind -> StepKind -> Bool
< :: StepKind -> StepKind -> Bool
$c< :: StepKind -> StepKind -> Bool
compare :: StepKind -> StepKind -> Ordering
$ccompare :: StepKind -> StepKind -> Ordering
$cp1Ord :: Eq StepKind
Ord, (forall x. StepKind -> Rep StepKind x)
-> (forall x. Rep StepKind x -> StepKind) -> Generic StepKind
forall x. Rep StepKind x -> StepKind
forall x. StepKind -> Rep StepKind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep StepKind x -> StepKind
$cfrom :: forall x. StepKind -> Rep StepKind x
Generic, Int -> StepKind
StepKind -> Int
StepKind -> [StepKind]
StepKind -> StepKind
StepKind -> StepKind -> [StepKind]
StepKind -> StepKind -> StepKind -> [StepKind]
(StepKind -> StepKind)
-> (StepKind -> StepKind)
-> (Int -> StepKind)
-> (StepKind -> Int)
-> (StepKind -> [StepKind])
-> (StepKind -> StepKind -> [StepKind])
-> (StepKind -> StepKind -> [StepKind])
-> (StepKind -> StepKind -> StepKind -> [StepKind])
-> Enum StepKind
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: StepKind -> StepKind -> StepKind -> [StepKind]
$cenumFromThenTo :: StepKind -> StepKind -> StepKind -> [StepKind]
enumFromTo :: StepKind -> StepKind -> [StepKind]
$cenumFromTo :: StepKind -> StepKind -> [StepKind]
enumFromThen :: StepKind -> StepKind -> [StepKind]
$cenumFromThen :: StepKind -> StepKind -> [StepKind]
enumFrom :: StepKind -> [StepKind]
$cenumFrom :: StepKind -> [StepKind]
fromEnum :: StepKind -> Int
$cfromEnum :: StepKind -> Int
toEnum :: Int -> StepKind
$ctoEnum :: Int -> StepKind
pred :: StepKind -> StepKind
$cpred :: StepKind -> StepKind
succ :: StepKind -> StepKind
$csucc :: StepKind -> StepKind
Enum, StepKind
StepKind -> StepKind -> Bounded StepKind
forall a. a -> a -> Bounded a
maxBound :: StepKind
$cmaxBound :: StepKind
minBound :: StepKind
$cminBound :: StepKind
Bounded)
deriving anyclass (StepKind -> ()
(StepKind -> ()) -> NFData StepKind
forall a. (a -> ()) -> NFData a
rnf :: StepKind -> ()
$crnf :: StepKind -> ()
NFData, Int -> StepKind -> Int
StepKind -> Int
(Int -> StepKind -> Int) -> (StepKind -> Int) -> Hashable StepKind
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: StepKind -> Int
$chash :: StepKind -> Int
hashWithSalt :: Int -> StepKind -> Int
$chashWithSalt :: Int -> StepKind -> Int
Hashable)
cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost :: CekMachineCosts -> StepKind -> ExBudget
cekStepCost CekMachineCosts
costs = \case
StepKind
BConst -> CekMachineCosts -> ExBudget
cekConstCost CekMachineCosts
costs
StepKind
BVar -> CekMachineCosts -> ExBudget
cekVarCost CekMachineCosts
costs
StepKind
BLamAbs -> CekMachineCosts -> ExBudget
cekLamCost CekMachineCosts
costs
StepKind
BApply -> CekMachineCosts -> ExBudget
cekApplyCost CekMachineCosts
costs
StepKind
BDelay -> CekMachineCosts -> ExBudget
cekDelayCost CekMachineCosts
costs
StepKind
BForce -> CekMachineCosts -> ExBudget
cekForceCost CekMachineCosts
costs
StepKind
BBuiltin -> CekMachineCosts -> ExBudget
cekBuiltinCost CekMachineCosts
costs
data ExBudgetCategory fun
= BStep StepKind
| BBuiltinApp fun
| BStartup
deriving stock (Int -> ExBudgetCategory fun -> ShowS
[ExBudgetCategory fun] -> ShowS
ExBudgetCategory fun -> String
(Int -> ExBudgetCategory fun -> ShowS)
-> (ExBudgetCategory fun -> String)
-> ([ExBudgetCategory fun] -> ShowS)
-> Show (ExBudgetCategory fun)
forall fun. Show fun => Int -> ExBudgetCategory fun -> ShowS
forall fun. Show fun => [ExBudgetCategory fun] -> ShowS
forall fun. Show fun => ExBudgetCategory fun -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExBudgetCategory fun] -> ShowS
$cshowList :: forall fun. Show fun => [ExBudgetCategory fun] -> ShowS
show :: ExBudgetCategory fun -> String
$cshow :: forall fun. Show fun => ExBudgetCategory fun -> String
showsPrec :: Int -> ExBudgetCategory fun -> ShowS
$cshowsPrec :: forall fun. Show fun => Int -> ExBudgetCategory fun -> ShowS
Show, ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
(ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> Eq (ExBudgetCategory fun)
forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c/= :: forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
== :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c== :: forall fun.
Eq fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
Eq, Eq (ExBudgetCategory fun)
Eq (ExBudgetCategory fun)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun -> ExBudgetCategory fun -> Bool)
-> (ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun)
-> (ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun)
-> Ord (ExBudgetCategory fun)
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall fun. Ord fun => Eq (ExBudgetCategory fun)
forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
min :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$cmin :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
max :: ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
$cmax :: forall fun.
Ord fun =>
ExBudgetCategory fun
-> ExBudgetCategory fun -> ExBudgetCategory fun
>= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c>= :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
> :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c> :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
<= :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c<= :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
< :: ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
$c< :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Bool
compare :: ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
$ccompare :: forall fun.
Ord fun =>
ExBudgetCategory fun -> ExBudgetCategory fun -> Ordering
$cp1Ord :: forall fun. Ord fun => Eq (ExBudgetCategory fun)
Ord, (forall x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x)
-> (forall x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun)
-> Generic (ExBudgetCategory fun)
forall x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
forall x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall fun x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
forall fun x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
$cto :: forall fun x. Rep (ExBudgetCategory fun) x -> ExBudgetCategory fun
$cfrom :: forall fun x. ExBudgetCategory fun -> Rep (ExBudgetCategory fun) x
Generic)
deriving anyclass (ExBudgetCategory fun -> ()
(ExBudgetCategory fun -> ()) -> NFData (ExBudgetCategory fun)
forall fun. NFData fun => ExBudgetCategory fun -> ()
forall a. (a -> ()) -> NFData a
rnf :: ExBudgetCategory fun -> ()
$crnf :: forall fun. NFData fun => ExBudgetCategory fun -> ()
NFData, Int -> ExBudgetCategory fun -> Int
ExBudgetCategory fun -> Int
(Int -> ExBudgetCategory fun -> Int)
-> (ExBudgetCategory fun -> Int) -> Hashable (ExBudgetCategory fun)
forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
forall fun. Hashable fun => ExBudgetCategory fun -> Int
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ExBudgetCategory fun -> Int
$chash :: forall fun. Hashable fun => ExBudgetCategory fun -> Int
hashWithSalt :: Int -> ExBudgetCategory fun -> Int
$chashWithSalt :: forall fun. Hashable fun => Int -> ExBudgetCategory fun -> Int
Hashable)
instance Show fun => Pretty (ExBudgetCategory fun) where
pretty :: ExBudgetCategory fun -> Doc ann
pretty = ExBudgetCategory fun -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance ExBudgetBuiltin fun (ExBudgetCategory fun) where
exBudgetBuiltin :: fun -> ExBudgetCategory fun
exBudgetBuiltin = fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp
instance Show (BuiltinRuntime (CekValue uni fun)) where
show :: BuiltinRuntime (CekValue uni fun) -> String
show BuiltinRuntime (CekValue uni fun)
_ = String
"<builtin_runtime>"
data CekValue uni fun =
VCon !(Some (ValueOf uni))
| VDelay (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
| VLamAbs NamedDeBruijn (Term NamedDeBruijn uni fun ()) !(CekValEnv uni fun)
| VBuiltin
!fun
(Term NamedDeBruijn uni fun ())
(CekValEnv uni fun)
!(BuiltinRuntime (CekValue uni fun))
deriving stock (Int -> CekValue uni fun -> ShowS
[CekValue uni fun] -> ShowS
CekValue uni fun -> String
(Int -> CekValue uni fun -> ShowS)
-> (CekValue uni fun -> String)
-> ([CekValue uni fun] -> ShowS)
-> Show (CekValue 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 -> CekValue uni fun -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CekValue uni fun] -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CekValue uni fun -> String
showList :: [CekValue uni fun] -> ShowS
$cshowList :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[CekValue uni fun] -> ShowS
show :: CekValue uni fun -> String
$cshow :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
CekValue uni fun -> String
showsPrec :: Int -> CekValue uni fun -> ShowS
$cshowsPrec :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> CekValue uni fun -> ShowS
Show)
type CekValEnv uni fun = RAList (CekValue uni fun)
newtype CekBudgetSpender uni fun s = CekBudgetSpender
{ CekBudgetSpender uni fun s
-> ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
unCekBudgetSpender :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
}
data ExBudgetInfo cost uni fun s = ExBudgetInfo
{ ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender :: !(CekBudgetSpender uni fun s)
, ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal :: !(ST s cost)
, ExBudgetInfo cost uni fun s -> ST s ExBudget
_exBudgetModeGetCumulative :: !(ST s ExBudget)
}
newtype ExBudgetMode cost uni fun = ExBudgetMode
{ ExBudgetMode cost uni fun
-> forall s. ST s (ExBudgetInfo cost uni fun s)
unExBudgetMode :: forall s. ST s (ExBudgetInfo cost uni fun s)
}
type Slippage = Word8
defaultSlippage :: Slippage
defaultSlippage :: Slippage
defaultSlippage = Slippage
200
type CekEmitter uni fun s = DList Text -> CekM uni fun s ()
data CekEmitterInfo uni fun s = CekEmitterInfo {
CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit :: CekEmitter uni fun s
, CekEmitterInfo uni fun s -> ST s [Text]
_cekEmitterInfoGetFinal :: ST s [Text]
}
newtype EmitterMode uni fun = EmitterMode
{ EmitterMode uni fun
-> forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
unEmitterMode :: forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
}
type GivenCekRuntime uni fun = (?cekRuntime :: (BuiltinsRuntime fun (CekValue uni fun)))
type GivenCekEmitter uni fun s = (?cekEmitter :: CekEmitter uni fun s)
type GivenCekSpender uni fun s = (?cekBudgetSpender :: (CekBudgetSpender uni fun s))
type GivenCekSlippage = (?cekSlippage :: Slippage)
type GivenCekCosts = (?cekCosts :: CekMachineCosts)
type GivenCekReqs uni fun s = (GivenCekRuntime uni fun, GivenCekEmitter uni fun s, GivenCekSpender uni fun s, GivenCekSlippage, GivenCekCosts)
data CekUserError
= CekOutOfExError ExRestrictingBudget
| CekEvaluationFailure
deriving stock (Int -> CekUserError -> ShowS
[CekUserError] -> ShowS
CekUserError -> String
(Int -> CekUserError -> ShowS)
-> (CekUserError -> String)
-> ([CekUserError] -> ShowS)
-> Show CekUserError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CekUserError] -> ShowS
$cshowList :: [CekUserError] -> ShowS
show :: CekUserError -> String
$cshow :: CekUserError -> String
showsPrec :: Int -> CekUserError -> ShowS
$cshowsPrec :: Int -> CekUserError -> ShowS
Show, CekUserError -> CekUserError -> Bool
(CekUserError -> CekUserError -> Bool)
-> (CekUserError -> CekUserError -> Bool) -> Eq CekUserError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CekUserError -> CekUserError -> Bool
$c/= :: CekUserError -> CekUserError -> Bool
== :: CekUserError -> CekUserError -> Bool
$c== :: CekUserError -> CekUserError -> Bool
Eq, (forall x. CekUserError -> Rep CekUserError x)
-> (forall x. Rep CekUserError x -> CekUserError)
-> Generic CekUserError
forall x. Rep CekUserError x -> CekUserError
forall x. CekUserError -> Rep CekUserError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CekUserError x -> CekUserError
$cfrom :: forall x. CekUserError -> Rep CekUserError x
Generic)
deriving anyclass (CekUserError -> ()
(CekUserError -> ()) -> NFData CekUserError
forall a. (a -> ()) -> NFData a
rnf :: CekUserError -> ()
$crnf :: CekUserError -> ()
NFData)
instance HasErrorCode CekUserError where
errorCode :: CekUserError -> ErrorCode
errorCode CekEvaluationFailure {} = Natural -> ErrorCode
ErrorCode Natural
37
errorCode CekOutOfExError {} = Natural -> ErrorCode
ErrorCode Natural
36
type CekM :: (GHC.Type -> GHC.Type) -> GHC.Type -> GHC.Type -> GHC.Type -> GHC.Type
newtype CekM uni fun s a = CekM
{ CekM uni fun s a -> ST s a
unCekM :: ST s a
} deriving newtype (a -> CekM uni fun s b -> CekM uni fun s a
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
(forall a b. (a -> b) -> CekM uni fun s a -> CekM uni fun s b)
-> (forall a b. a -> CekM uni fun s b -> CekM uni fun s a)
-> Functor (CekM uni fun s)
forall a b. a -> CekM uni fun s b -> CekM uni fun s a
forall a b. (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (uni :: * -> *) fun s a b.
a -> CekM uni fun s b -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
<$ :: a -> CekM uni fun s b -> CekM uni fun s a
$c<$ :: forall (uni :: * -> *) fun s a b.
a -> CekM uni fun s b -> CekM uni fun s a
fmap :: (a -> b) -> CekM uni fun s a -> CekM uni fun s b
$cfmap :: forall (uni :: * -> *) fun s a b.
(a -> b) -> CekM uni fun s a -> CekM uni fun s b
Functor, Functor (CekM uni fun s)
a -> CekM uni fun s a
Functor (CekM uni fun s)
-> (forall a. a -> CekM uni fun s a)
-> (forall a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b)
-> (forall a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c)
-> (forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b)
-> (forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a)
-> Applicative (CekM uni fun s)
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
forall a. a -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (uni :: * -> *) fun s. Functor (CekM uni fun s)
forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (uni :: * -> *) fun s a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
forall (uni :: * -> *) fun s a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
<* :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
$c<* :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s a
*> :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
$c*> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
liftA2 :: (a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
$cliftA2 :: forall (uni :: * -> *) fun s a b c.
(a -> b -> c)
-> CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s c
<*> :: CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
$c<*> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s (a -> b) -> CekM uni fun s a -> CekM uni fun s b
pure :: a -> CekM uni fun s a
$cpure :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
$cp1Applicative :: forall (uni :: * -> *) fun s. Functor (CekM uni fun s)
Applicative, Applicative (CekM uni fun s)
a -> CekM uni fun s a
Applicative (CekM uni fun s)
-> (forall a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b)
-> (forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b)
-> (forall a. a -> CekM uni fun s a)
-> Monad (CekM uni fun s)
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall a. a -> CekM uni fun s a
forall a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (uni :: * -> *) fun s. Applicative (CekM uni fun s)
forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
return :: a -> CekM uni fun s a
$creturn :: forall (uni :: * -> *) fun s a. a -> CekM uni fun s a
>> :: CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
$c>> :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> CekM uni fun s b -> CekM uni fun s b
>>= :: CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
$c>>= :: forall (uni :: * -> *) fun s a b.
CekM uni fun s a -> (a -> CekM uni fun s b) -> CekM uni fun s b
$cp1Monad :: forall (uni :: * -> *) fun s. Applicative (CekM uni fun s)
Monad)
type CekEvaluationException name uni fun =
EvaluationException CekUserError (MachineError fun) (Term name uni fun ())
type PrettyUni uni fun = (GShow uni, Closed uni, Pretty fun, Typeable uni, Typeable fun, Everywhere uni PrettyConst)
throwingDischarged
:: (PrettyUni uni fun)
=> AReview (EvaluationError CekUserError (MachineError fun)) t
-> t
-> CekValue uni fun
-> CekM uni fun s x
throwingDischarged :: AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview (EvaluationError CekUserError (MachineError fun)) t
l t
t = AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> Maybe (Term NamedDeBruijn uni fun ()) -> CekM uni fun s x
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 CekUserError (MachineError fun)) t
l t
t (Maybe (Term NamedDeBruijn uni fun ()) -> CekM uni fun s x)
-> (CekValue uni fun -> Maybe (Term NamedDeBruijn uni fun ()))
-> CekValue uni fun
-> CekM uni fun s x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just (Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ()))
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> CekValue uni fun
-> Maybe (Term NamedDeBruijn uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue
instance PrettyUni uni fun => MonadError (CekEvaluationException NamedDeBruijn uni fun) (CekM uni fun s) where
throwError :: CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
throwError = ST s a -> CekM uni fun s a
forall (uni :: * -> *) fun s a. ST s a -> CekM uni fun s a
CekM (ST s a -> CekM uni fun s a)
-> (CekEvaluationException NamedDeBruijn uni fun -> ST s a)
-> CekEvaluationException NamedDeBruijn uni fun
-> CekM uni fun s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekEvaluationException NamedDeBruijn uni fun -> ST s a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM
CekM uni fun s a
a catchError :: CekM uni fun s a
-> (CekEvaluationException NamedDeBruijn uni fun
-> CekM uni fun s a)
-> CekM uni fun s a
`catchError` CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
h = ST s a -> CekM uni fun s a
forall (uni :: * -> *) fun s a. ST s a -> CekM uni fun s a
CekM (ST s a -> CekM uni fun s a)
-> (IO a -> ST s a) -> IO a -> CekM uni fun s a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> ST s a
forall a s. IO a -> ST s a
unsafeIOToST (IO a -> CekM uni fun s a) -> IO a -> CekM uni fun s a
forall a b. (a -> b) -> a -> b
$ IO a
aIO IO a
-> (CekEvaluationException NamedDeBruijn uni fun -> IO a) -> IO a
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`catch` CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO where
aIO :: IO a
aIO = CekM uni fun s a -> IO a
forall a. CekM uni fun s a -> IO a
unsafeRunCekM CekM uni fun s a
a
hIO :: CekEvaluationException NamedDeBruijn uni fun -> IO a
hIO = CekM uni fun s a -> IO a
forall a. CekM uni fun s a -> IO a
unsafeRunCekM (CekM uni fun s a -> IO a)
-> (CekEvaluationException NamedDeBruijn uni fun
-> CekM uni fun s a)
-> CekEvaluationException NamedDeBruijn uni fun
-> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekEvaluationException NamedDeBruijn uni fun -> CekM uni fun s a
h
unsafeRunCekM :: CekM uni fun s a -> IO a
unsafeRunCekM :: CekM uni fun s a -> IO a
unsafeRunCekM = ST s a -> IO a
forall s a. ST s a -> IO a
unsafeSTToIO (ST s a -> IO a)
-> (CekM uni fun s a -> ST s a) -> CekM uni fun s a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekM uni fun s a -> ST s a
forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM
instance AsEvaluationFailure CekUserError where
_EvaluationFailure :: p () (f ()) -> p CekUserError (f CekUserError)
_EvaluationFailure = CekUserError -> Prism' CekUserError ()
forall err. Eq err => err -> Prism' err ()
_EvaluationFailureVia CekUserError
CekEvaluationFailure
instance Pretty CekUserError where
pretty :: CekUserError -> Doc ann
pretty (CekOutOfExError (ExRestrictingBudget ExBudget
res)) =
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
cat
[ Doc ann
"The machine terminated part way through evaluation due to overspending the budget."
, Doc ann
"The budget when the machine terminated was:"
, ExBudget -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ExBudget
res
, Doc ann
"Negative numbers indicate the overspent budget; note that this only indicatessthe budget that was needed for the next step, not to run the program to completion."
]
pretty CekUserError
CekEvaluationFailure = Doc ann
"The machine terminated because of an error, either from a built-in function or from an explicit use of 'error'."
spendBudgetCek :: GivenCekSpender uni fun s => ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek :: ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek = let (CekBudgetSpender ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spend) = ?cekBudgetSpender::CekBudgetSpender uni fun s
CekBudgetSpender uni fun s
?cekBudgetSpender in ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spend
dischargeCekValEnv :: forall uni fun. CekValEnv uni fun -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv :: CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
valEnv = Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
0
where
go :: Word64 -> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go :: Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go !Word64
lamCnt = \case
LamAbs ()
ann NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body -> ()
-> NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs ()
ann NamedDeBruijn
name (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go (Word64
lamCntWord64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+Word64
1) Term NamedDeBruijn uni fun ()
body
var :: Term NamedDeBruijn uni fun ()
var@(Var ()
_ (NamedDeBruijn Text
_ Index
ndbnIx)) -> let ix :: Word64
ix = Index -> Word64
coerce Index
ndbnIx :: Word64 in
if Word64
lamCnt Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
ix
then Term NamedDeBruijn uni fun ()
var
else Term NamedDeBruijn uni fun ()
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> Maybe (CekValue uni fun)
-> Term NamedDeBruijn uni fun ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
Term NamedDeBruijn uni fun ()
var
CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue
(CekValEnv uni fun -> Word64 -> Maybe (Element (CekValEnv uni fun))
forall e. DeBruijnEnv e => e -> Word64 -> Maybe (Element e)
Env.index CekValEnv uni fun
valEnv (Word64 -> Maybe (Element (CekValEnv uni fun)))
-> Word64 -> Maybe (Element (CekValEnv uni fun))
forall a b. (a -> b) -> a -> b
$ Word64
ix Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
lamCnt)
Apply ()
ann Term NamedDeBruijn uni fun ()
fun Term NamedDeBruijn uni fun ()
arg -> ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ()
ann (Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
fun) (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
arg
Delay ()
ann Term NamedDeBruijn uni fun ()
term -> ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()
ann (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
term
Force ()
ann Term NamedDeBruijn uni fun ()
term -> ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()
ann (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ Word64
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
go Word64
lamCnt Term NamedDeBruijn uni fun ()
term
Term NamedDeBruijn uni fun ()
t -> Term NamedDeBruijn uni fun ()
t
dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue :: CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue = \case
VCon Some (ValueOf uni)
val -> () -> Some (ValueOf uni) -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term name uni fun ann
Constant () Some (ValueOf uni)
val
VDelay Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env -> CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay () Term NamedDeBruijn uni fun ()
body
VLamAbs (NamedDeBruijn Text
n Index
_ix) Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env ->
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env (Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ())
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall a b. (a -> b) -> a -> b
$ ()
-> NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () (Text -> Index -> NamedDeBruijn
NamedDeBruijn Text
n Index
deBruijnInitIndex) Term NamedDeBruijn uni fun ()
body
VBuiltin fun
_ Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
_ -> CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
dischargeCekValEnv CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
term
instance (Closed uni, GShow uni, uni `Everywhere` PrettyConst, Pretty fun) =>
PrettyBy PrettyConfigPlc (CekValue uni fun) where
prettyBy :: PrettyConfigPlc -> CekValue uni fun -> Doc ann
prettyBy PrettyConfigPlc
cfg = PrettyConfigPlc -> Term NamedDeBruijn uni fun () -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy PrettyConfigPlc
cfg (Term NamedDeBruijn uni fun () -> Doc ann)
-> (CekValue uni fun -> Term NamedDeBruijn uni fun ())
-> CekValue uni fun
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue
type instance UniOf (CekValue uni fun) = uni
instance HasConstant (CekValue uni fun) where
asConstant :: Maybe cause
-> CekValue uni fun
-> Either
(ErrorWithCause err cause)
(Some (ValueOf (UniOf (CekValue 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 CekValue 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 (CekValue uni fun))) -> CekValue uni fun
fromConstant = Some (ValueOf (UniOf (CekValue uni fun))) -> CekValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CekValue uni fun
VCon
data Context uni fun
= FrameApplyFun !(CekValue uni fun) !(Context uni fun)
| FrameApplyArg !(CekValEnv uni fun) (Term NamedDeBruijn uni fun ()) !(Context uni fun)
| FrameForce !(Context uni fun)
| NoFrame
deriving stock (Int -> Context uni fun -> ShowS
[Context uni fun] -> ShowS
Context uni fun -> String
(Int -> Context uni fun -> ShowS)
-> (Context uni fun -> String)
-> ([Context uni fun] -> ShowS)
-> Show (Context 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 -> Context uni fun -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[Context uni fun] -> ShowS
forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Context uni fun -> String
showList :: [Context uni fun] -> ShowS
$cshowList :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
[Context uni fun] -> ShowS
show :: Context uni fun -> String
$cshow :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Context uni fun -> String
showsPrec :: Int -> Context uni fun -> ShowS
$cshowsPrec :: forall (uni :: * -> *) fun.
(Everywhere uni Show, GShow uni, Closed uni, Show fun) =>
Int -> Context uni fun -> ShowS
Show)
toExMemory :: (Closed uni, uni `Everywhere` ExMemoryUsage) => CekValue uni fun -> ExMemory
toExMemory :: CekValue uni fun -> ExMemory
toExMemory = \case
VCon Some (ValueOf uni)
c -> Some (ValueOf uni) -> ExMemory
forall a. ExMemoryUsage a => a -> ExMemory
memoryUsage Some (ValueOf uni)
c
VDelay {} -> ExMemory
1
VLamAbs {} -> ExMemory
1
VBuiltin {} -> ExMemory
1
{-# INLINE toExMemory #-}
tryError :: MonadError e m => m a -> m (Either e a)
tryError :: m a -> m (Either e a)
tryError m a
a = (a -> Either e a
forall a b. b -> Either a b
Right (a -> Either e a) -> m a -> m (Either e a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
a) m (Either e a) -> (e -> m (Either e a)) -> m (Either e a)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (Either e a -> m (Either e a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either e a -> m (Either e a))
-> (e -> Either e a) -> e -> m (Either e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either e a
forall a b. a -> Either a b
Left)
runCekM
:: forall a cost uni fun.
(PrettyUni uni fun)
=> MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost, [Text])
runCekM :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
runCekM (MachineParameters CekMachineCosts
costs BuiltinsRuntime fun (CekValue uni fun)
runtime) (ExBudgetMode forall s. ST s (ExBudgetInfo cost uni fun s)
getExBudgetInfo) (EmitterMode forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode) forall s. GivenCekReqs uni fun s => CekM uni fun s a
a = (forall s.
ST
s
(Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text]))
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
forall a. (forall s. ST s a) -> a
runST ((forall s.
ST
s
(Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text]))
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text]))
-> (forall s.
ST
s
(Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text]))
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
forall a b. (a -> b) -> a -> b
$ do
ExBudgetInfo{CekBudgetSpender uni fun s
_exBudgetModeSpender :: CekBudgetSpender uni fun s
_exBudgetModeSpender :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> CekBudgetSpender uni fun s
_exBudgetModeSpender, ST s cost
_exBudgetModeGetFinal :: ST s cost
_exBudgetModeGetFinal :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s cost
_exBudgetModeGetFinal, ST s ExBudget
_exBudgetModeGetCumulative :: ST s ExBudget
_exBudgetModeGetCumulative :: forall cost (uni :: * -> *) fun s.
ExBudgetInfo cost uni fun s -> ST s ExBudget
_exBudgetModeGetCumulative} <- ST s (ExBudgetInfo cost uni fun s)
forall s. ST s (ExBudgetInfo cost uni fun s)
getExBudgetInfo
CekEmitterInfo{CekEmitter uni fun s
_cekEmitterInfoEmit :: CekEmitter uni fun s
_cekEmitterInfoEmit :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> CekEmitter uni fun s
_cekEmitterInfoEmit, ST s [Text]
_cekEmitterInfoGetFinal :: ST s [Text]
_cekEmitterInfoGetFinal :: forall (uni :: * -> *) fun s.
CekEmitterInfo uni fun s -> ST s [Text]
_cekEmitterInfoGetFinal} <- ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
forall s. ST s ExBudget -> ST s (CekEmitterInfo uni fun s)
getEmitterMode ST s ExBudget
_exBudgetModeGetCumulative
let ?cekRuntime = runtime
?cekEmitter = _cekEmitterInfoEmit
?cekBudgetSpender = _exBudgetModeSpender
?cekCosts = costs
?cekSlippage = defaultSlippage
Either (CekEvaluationException NamedDeBruijn uni fun) a
errOrRes <- CekM
uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
-> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall (uni :: * -> *) fun s a. CekM uni fun s a -> ST s a
unCekM (CekM
uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
-> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a))
-> CekM
uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
-> ST s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall a b. (a -> b) -> a -> b
$ CekM uni fun s a
-> CekM
uni fun s (Either (CekEvaluationException NamedDeBruijn uni fun) a)
forall e (m :: * -> *) a. MonadError e m => m a -> m (Either e a)
tryError CekM uni fun s a
forall s. GivenCekReqs uni fun s => CekM uni fun s a
a
cost
st <- ST s cost
_exBudgetModeGetFinal
[Text]
logs <- ST s [Text]
_cekEmitterInfoGetFinal
(Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
-> ST
s
(Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (CekEvaluationException NamedDeBruijn uni fun) a
errOrRes, cost
st, [Text]
logs)
lookupVarName :: forall uni fun s . (PrettyUni uni fun) => NamedDeBruijn -> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName :: NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName varName :: NamedDeBruijn
varName@(NamedDeBruijn Text
_ Index
varIx) CekValEnv uni fun
varEnv =
case CekValEnv uni fun
varEnv CekValEnv uni fun -> Word64 -> Maybe (Element (CekValEnv uni fun))
forall e. DeBruijnEnv e => e -> Word64 -> Maybe (Element e)
`Env.index` Index -> Word64
coerce Index
varIx of
Maybe (Element (CekValEnv uni fun))
Nothing -> AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue 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 CekUserError (MachineError fun))
(MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
OpenTermEvaluatedMachineError (Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun))
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
var where
var :: Term NamedDeBruijn uni fun ()
var = () -> NamedDeBruijn -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () NamedDeBruijn
varName
Just Element (CekValEnv uni fun)
val -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Element (CekValEnv uni fun)
CekValue uni fun
val
evalBuiltinApp
:: (GivenCekReqs uni fun s, PrettyUni uni fun)
=> fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp :: fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env runtime :: BuiltinRuntime (CekValue uni fun)
runtime@(BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
getX ToCostingType n
cost) = case RuntimeScheme n
sch of
RuntimeScheme n
RuntimeSchemeResult -> do
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek (fun -> ExBudgetCategory fun
forall fun. fun -> ExBudgetCategory fun
BBuiltinApp fun
fun) ExBudget
ToCostingType n
cost
let !(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun)
errOrRes, DList Text
logs) = Emitter
(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
DList Text)
forall a. Emitter a -> (a, DList Text)
runEmitter (Emitter
(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
DList Text))
-> Emitter
(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
-> (Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun),
DList Text)
forall a b. (a -> b) -> a -> b
$ ExceptT
(ErrorWithCause KnownTypeError ()) Emitter (CekValue uni fun)
-> Emitter
(Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT
(ErrorWithCause KnownTypeError ()) Emitter (CekValue uni fun)
ToRuntimeDenotationType (CekValue uni fun) n
getX
?cekEmitter::DList Text -> CekM uni fun s ()
DList Text -> CekM uni fun s ()
?cekEmitter DList Text
logs
case Either (ErrorWithCause KnownTypeError ()) (CekValue uni fun)
errOrRes of
Left ErrorWithCause KnownTypeError ()
err -> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue 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 NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun))
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
term Term NamedDeBruijn uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
Right CekValue uni fun
res -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CekValue uni fun
res
RuntimeScheme n
_ -> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CekValue uni fun -> CekM uni fun s (CekValue uni fun))
-> CekValue uni fun -> CekM uni fun s (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
forall (uni :: * -> *) fun.
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime
{-# INLINE evalBuiltinApp #-}
enterComputeCek
:: forall uni fun s
. (Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s, uni `Everywhere` ExMemoryUsage)
=> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek :: Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek = WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek (Word64 -> WordArray
toWordArray Word64
0) where
computeCek
:: WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek :: WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Var ()
_ NamedDeBruijn
varName) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BVar WordArray
unbudgetedSteps
CekValue uni fun
val <- NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
PrettyUni uni fun =>
NamedDeBruijn
-> CekValEnv uni fun -> CekM uni fun s (CekValue uni fun)
lookupVarName NamedDeBruijn
varName CekValEnv uni fun
env
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx CekValue uni fun
val
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
_ (Constant ()
_ Some (ValueOf uni)
val) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BConst WordArray
unbudgetedSteps
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (Some (ValueOf uni) -> CekValue uni fun
forall (uni :: * -> *) fun. Some (ValueOf uni) -> CekValue uni fun
VCon Some (ValueOf uni)
val)
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (LamAbs ()
_ NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BLamAbs WordArray
unbudgetedSteps
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> CekValue uni fun
forall (uni :: * -> *) fun.
NamedDeBruijn
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> CekValue uni fun
VLamAbs NamedDeBruijn
name Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env)
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Delay ()
_ Term NamedDeBruijn uni fun ()
body) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BDelay WordArray
unbudgetedSteps
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun -> CekValue uni fun
forall (uni :: * -> *) fun.
Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun -> CekValue uni fun
VDelay Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env)
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Force ()
_ Term NamedDeBruijn uni fun ()
body) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BForce WordArray
unbudgetedSteps
WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps' (Context uni fun -> Context uni fun
forall (uni :: * -> *) fun. Context uni fun -> Context uni fun
FrameForce Context uni fun
ctx) CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
body
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env (Apply ()
_ Term NamedDeBruijn uni fun ()
fun Term NamedDeBruijn uni fun ()
arg) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BApply WordArray
unbudgetedSteps
WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps' (CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> Context uni fun
-> Context uni fun
forall (uni :: * -> *) fun.
CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> Context uni fun
-> Context uni fun
FrameApplyArg CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
arg Context uni fun
ctx) CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
fun
computeCek !WordArray
unbudgetedSteps !Context uni fun
ctx !CekValEnv uni fun
env term :: Term NamedDeBruijn uni fun ()
term@(Builtin ()
_ fun
bn) = do
!WordArray
unbudgetedSteps' <- StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend StepKind
BBuiltin WordArray
unbudgetedSteps
BuiltinRuntime (CekValue uni fun)
meaning <- fun
-> BuiltinsRuntime fun (CekValue uni fun)
-> CekM uni fun s (BuiltinRuntime (CekValue 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 ?cekRuntime::BuiltinsRuntime fun (CekValue uni fun)
BuiltinsRuntime fun (CekValue uni fun)
?cekRuntime
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps' Context uni fun
ctx (fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
forall (uni :: * -> *) fun.
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekValue uni fun
VBuiltin fun
bn Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
meaning)
computeCek !WordArray
_ !Context uni fun
_ !CekValEnv uni fun
_ (Error ()
_) =
AReview (CekEvaluationException NamedDeBruijn uni fun) ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall e (m :: * -> *) x. MonadError e m => AReview e () -> m x
throwing_ AReview (CekEvaluationException NamedDeBruijn uni fun) ()
forall err. AsEvaluationFailure err => Prism' err ()
_EvaluationFailure
returnCek
:: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek !WordArray
unbudgetedSteps Context uni fun
NoFrame CekValue uni fun
val = do
WordArray -> CekM uni fun s ()
spendAccumulatedBudget WordArray
unbudgetedSteps
Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue CekValue uni fun
val
returnCek !WordArray
unbudgetedSteps (FrameForce Context uni fun
ctx) CekValue uni fun
fun = WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forceEvaluate WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
fun
returnCek !WordArray
unbudgetedSteps (FrameApplyArg CekValEnv uni fun
argVarEnv Term NamedDeBruijn uni fun ()
arg Context uni fun
ctx) CekValue uni fun
fun =
WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps (CekValue uni fun -> Context uni fun -> Context uni fun
forall (uni :: * -> *) fun.
CekValue uni fun -> Context uni fun -> Context uni fun
FrameApplyFun CekValue uni fun
fun Context uni fun
ctx) CekValEnv uni fun
argVarEnv Term NamedDeBruijn uni fun ()
arg
returnCek !WordArray
unbudgetedSteps (FrameApplyFun CekValue uni fun
fun Context uni fun
ctx) CekValue uni fun
arg =
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
fun CekValue uni fun
arg
forceEvaluate
:: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forceEvaluate :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forceEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VDelay Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env) = WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps Context uni fun
ctx CekValEnv uni fun
env Term NamedDeBruijn uni fun ()
body
forceEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env (BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF)) = do
let term' :: Term NamedDeBruijn uni fun ()
term' = ()
-> Term NamedDeBruijn uni fun () -> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force () Term NamedDeBruijn uni fun ()
term
case RuntimeScheme n
sch of
RuntimeSchemeAll RuntimeScheme n
schK -> do
let runtime' :: BuiltinRuntime (CekValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CekValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CekValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schK ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF
CekValue uni fun
res <- fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
(GivenCekReqs uni fun s, PrettyUni uni fun) =>
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term' CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime'
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
res
RuntimeScheme n
_ ->
AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn 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 CekUserError (MachineError fun))
(MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
BuiltinTermArgumentExpectedMachineError (Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
term')
forceEvaluate !WordArray
_ !Context uni fun
_ CekValue uni fun
val =
AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
-> MachineError fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun t s x.
PrettyUni uni fun =>
AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonPolymorphicInstantiationMachineError CekValue uni fun
val
applyEvaluate
:: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate :: WordArray
-> Context uni fun
-> CekValue uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VLamAbs NamedDeBruijn
_ Term NamedDeBruijn uni fun ()
body CekValEnv uni fun
env) CekValue uni fun
arg =
WordArray
-> Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
computeCek WordArray
unbudgetedSteps Context uni fun
ctx (Element (CekValEnv uni fun)
-> CekValEnv uni fun -> CekValEnv uni fun
forall e. DeBruijnEnv e => Element e -> e -> e
Env.cons Element (CekValEnv uni fun)
CekValue uni fun
arg CekValEnv uni fun
env) Term NamedDeBruijn uni fun ()
body
applyEvaluate !WordArray
unbudgetedSteps !Context uni fun
ctx (VBuiltin fun
fun Term NamedDeBruijn uni fun ()
term CekValEnv uni fun
env (BuiltinRuntime RuntimeScheme n
sch ToRuntimeDenotationType (CekValue uni fun) n
f ToCostingType n
exF)) CekValue uni fun
arg = do
let argTerm :: Term NamedDeBruijn uni fun ()
argTerm = CekValue uni fun -> Term NamedDeBruijn uni fun ()
forall (uni :: * -> *) fun.
CekValue uni fun -> Term NamedDeBruijn uni fun ()
dischargeCekValue CekValue uni fun
arg
term' :: Term NamedDeBruijn uni fun ()
term' = ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
-> Term NamedDeBruijn uni fun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply () Term NamedDeBruijn uni fun ()
term Term NamedDeBruijn uni fun ()
argTerm
case RuntimeScheme n
sch of
RuntimeSchemeArrow RuntimeScheme n
schB -> case ToRuntimeDenotationType (CekValue uni fun) n
CekValue uni fun
-> ReadKnownM () (ToRuntimeDenotationType (CekValue uni fun) n)
f CekValue uni fun
arg of
Left ErrorWithCause KnownTypeError ()
err -> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn 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 NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall a b. (a -> b) -> a -> b
$ Term NamedDeBruijn uni fun ()
argTerm Term NamedDeBruijn uni fun ()
-> ErrorWithCause KnownTypeError ()
-> ErrorWithCause KnownTypeError (Term NamedDeBruijn uni fun ())
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ErrorWithCause KnownTypeError ()
err
Right ToRuntimeDenotationType (CekValue uni fun) n
y -> do
let runtime' :: BuiltinRuntime (CekValue uni fun)
runtime' = RuntimeScheme n
-> ToRuntimeDenotationType (CekValue uni fun) n
-> ToCostingType n
-> BuiltinRuntime (CekValue uni fun)
forall val (n :: Peano).
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToCostingType n
-> BuiltinRuntime val
BuiltinRuntime RuntimeScheme n
schB ToRuntimeDenotationType (CekValue uni fun) n
y (ToCostingType n -> BuiltinRuntime (CekValue uni fun))
-> (ExMemory -> ToCostingType n)
-> ExMemory
-> BuiltinRuntime (CekValue uni fun)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToCostingType n
ExMemory -> ToCostingType n
exF (ExMemory -> BuiltinRuntime (CekValue uni fun))
-> ExMemory -> BuiltinRuntime (CekValue uni fun)
forall a b. (a -> b) -> a -> b
$ CekValue uni fun -> ExMemory
forall (uni :: * -> *) fun.
(Closed uni, Everywhere uni ExMemoryUsage) =>
CekValue uni fun -> ExMemory
toExMemory CekValue uni fun
arg
CekValue uni fun
res <- fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
forall (uni :: * -> *) fun s.
(GivenCekReqs uni fun s, PrettyUni uni fun) =>
fun
-> Term NamedDeBruijn uni fun ()
-> CekValEnv uni fun
-> BuiltinRuntime (CekValue uni fun)
-> CekM uni fun s (CekValue uni fun)
evalBuiltinApp fun
fun Term NamedDeBruijn uni fun ()
term' CekValEnv uni fun
env BuiltinRuntime (CekValue uni fun)
runtime'
WordArray
-> Context uni fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
returnCek WordArray
unbudgetedSteps Context uni fun
ctx CekValue uni fun
res
RuntimeScheme n
_ ->
AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
-> MachineError fun
-> Maybe (Term NamedDeBruijn uni fun ())
-> CekM uni fun s (Term NamedDeBruijn 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 CekUserError (MachineError fun))
(MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
UnexpectedBuiltinTermArgumentMachineError (Term NamedDeBruijn uni fun ()
-> Maybe (Term NamedDeBruijn uni fun ())
forall a. a -> Maybe a
Just Term NamedDeBruijn uni fun ()
term')
applyEvaluate !WordArray
_ !Context uni fun
_ CekValue uni fun
val CekValue uni fun
_ =
AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
-> MachineError fun
-> CekValue uni fun
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun t s x.
PrettyUni uni fun =>
AReview (EvaluationError CekUserError (MachineError fun)) t
-> t -> CekValue uni fun -> CekM uni fun s x
throwingDischarged AReview
(EvaluationError CekUserError (MachineError fun))
(MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError MachineError fun
forall fun. MachineError fun
NonFunctionalApplicationMachineError CekValue uni fun
val
spendAccumulatedBudget :: WordArray -> CekM uni fun s ()
spendAccumulatedBudget :: WordArray -> CekM uni fun s ()
spendAccumulatedBudget !WordArray
unbudgetedSteps = WordArray
-> (Int -> Element WordArray -> CekM uni fun s ())
-> CekM uni fun s ()
forall (f :: * -> *).
Applicative f =>
WordArray -> (Int -> Element WordArray -> f ()) -> f ()
iforWordArray WordArray
unbudgetedSteps Int -> Element WordArray -> CekM uni fun s ()
forall b (uni :: * -> *) fun s.
(Integral b, ?cekBudgetSpender::CekBudgetSpender uni fun s,
?cekCosts::CekMachineCosts) =>
Int -> b -> CekM uni fun s ()
spend
{-# INLINE spend #-}
spend :: Int -> b -> CekM uni fun s ()
spend !Int
i !b
w = Bool -> CekM uni fun s () -> CekM uni fun s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
7) (CekM uni fun s () -> CekM uni fun s ())
-> CekM uni fun s () -> CekM uni fun s ()
forall a b. (a -> b) -> a -> b
$ let kind :: StepKind
kind = Int -> StepKind
forall a. Enum a => Int -> a
toEnum Int
i in ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek (StepKind -> ExBudgetCategory fun
forall fun. StepKind -> ExBudgetCategory fun
BStep StepKind
kind) (b -> ExBudget -> ExBudget
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes b
w (CekMachineCosts -> StepKind -> ExBudget
cekStepCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts StepKind
kind))
stepAndMaybeSpend :: StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend :: StepKind -> WordArray -> CekM uni fun s WordArray
stepAndMaybeSpend !StepKind
kind !WordArray
unbudgetedSteps = do
let !ix :: Index
ix = Int -> Index
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Index) -> Int -> Index
forall a b. (a -> b) -> a -> b
$ StepKind -> Int
forall a. Enum a => a -> Int
fromEnum StepKind
kind
!unbudgetedSteps' :: WordArray
unbudgetedSteps' = Index
-> (Element WordArray -> Element WordArray)
-> WordArray
-> WordArray
overIndex Index
7 (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) (WordArray -> WordArray) -> WordArray -> WordArray
forall a b. (a -> b) -> a -> b
$ Index
-> (Element WordArray -> Element WordArray)
-> WordArray
-> WordArray
overIndex Index
ix (Slippage -> Slippage -> Slippage
forall a. Num a => a -> a -> a
+Slippage
1) WordArray
unbudgetedSteps
!unbudgetedStepsTotal :: Element WordArray
unbudgetedStepsTotal = WordArray -> Index -> Element WordArray
readArray WordArray
unbudgetedSteps' Index
7
if Slippage
Element WordArray
unbudgetedStepsTotal Slippage -> Slippage -> Bool
forall a. Ord a => a -> a -> Bool
>= ?cekSlippage::Slippage
Slippage
?cekSlippage
then WordArray -> CekM uni fun s ()
spendAccumulatedBudget WordArray
unbudgetedSteps' CekM uni fun s ()
-> CekM uni fun s WordArray -> CekM uni fun s WordArray
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WordArray -> CekM uni fun s WordArray
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> WordArray
toWordArray Word64
0)
else WordArray -> CekM uni fun s WordArray
forall (f :: * -> *) a. Applicative f => a -> f a
pure WordArray
unbudgetedSteps'
runCekDeBruijn
:: ( uni `Everywhere` ExMemoryUsage, Ix fun, PrettyUni uni fun)
=> MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term NamedDeBruijn uni fun ()
-> (Either (CekEvaluationException NamedDeBruijn uni fun) (Term NamedDeBruijn uni fun ()), cost, [Text])
runCekDeBruijn :: MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> Term NamedDeBruijn uni fun ()
-> (Either
(CekEvaluationException NamedDeBruijn uni fun)
(Term NamedDeBruijn uni fun ()),
cost, [Text])
runCekDeBruijn MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode Term NamedDeBruijn uni fun ()
term =
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s.
GivenCekReqs uni fun s =>
CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> (Either
(CekEvaluationException NamedDeBruijn uni fun)
(Term NamedDeBruijn uni fun ()),
cost, [Text])
forall a cost (uni :: * -> *) fun.
PrettyUni uni fun =>
MachineParameters CekMachineCosts CekValue uni fun
-> ExBudgetMode cost uni fun
-> EmitterMode uni fun
-> (forall s. GivenCekReqs uni fun s => CekM uni fun s a)
-> (Either (CekEvaluationException NamedDeBruijn uni fun) a, cost,
[Text])
runCekM MachineParameters CekMachineCosts CekValue uni fun
params ExBudgetMode cost uni fun
mode EmitterMode uni fun
emitMode ((forall s.
GivenCekReqs uni fun s =>
CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> (Either
(CekEvaluationException NamedDeBruijn uni fun)
(Term NamedDeBruijn uni fun ()),
cost, [Text]))
-> (forall s.
GivenCekReqs uni fun s =>
CekM uni fun s (Term NamedDeBruijn uni fun ()))
-> (Either
(CekEvaluationException NamedDeBruijn uni fun)
(Term NamedDeBruijn uni fun ()),
cost, [Text])
forall a b. (a -> b) -> a -> b
$ do
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
forall (uni :: * -> *) fun s.
GivenCekSpender uni fun s =>
ExBudgetCategory fun -> ExBudget -> CekM uni fun s ()
spendBudgetCek ExBudgetCategory fun
forall fun. ExBudgetCategory fun
BStartup (CekMachineCosts -> ExBudget
cekStartupCost ?cekCosts::CekMachineCosts
CekMachineCosts
?cekCosts)
Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
forall (uni :: * -> *) fun s.
(Ix fun, PrettyUni uni fun, GivenCekReqs uni fun s,
Everywhere uni ExMemoryUsage) =>
Context uni fun
-> CekValEnv uni fun
-> Term NamedDeBruijn uni fun ()
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
enterComputeCek Context uni fun
forall (uni :: * -> *) fun. Context uni fun
NoFrame CekValEnv uni fun
forall e. DeBruijnEnv e => e
Env.empty Term NamedDeBruijn uni fun ()
term