{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators  #-}

{-# LANGUAGE StrictData     #-}

module PlutusCore.Builtin.Runtime where

import PlutusPrelude

import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.Meaning
import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception

import Control.Lens (ix, (^?))
import Control.Monad.Except
import Data.Array
import Data.Kind qualified as GHC (Type)
import PlutusCore.Builtin.KnownType

-- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
data RuntimeScheme val (args :: [GHC.Type]) res where
    RuntimeSchemeResult
        :: KnownTypeIn (UniOf val) val res
        => RuntimeScheme val '[] res
    RuntimeSchemeArrow
        :: KnownTypeIn (UniOf val) val arg
        => RuntimeScheme val args res
        -> RuntimeScheme val (arg ': args) res
    RuntimeSchemeAll
        :: RuntimeScheme val args res
        -> RuntimeScheme val args res

-- We tried instantiating 'BuiltinMeaning' on the fly and that was slower than precaching
-- 'BuiltinRuntime's.
-- | A 'BuiltinRuntime' represents a possibly partial builtin application.
-- We get an initial 'BuiltinRuntime' representing an empty builtin application (i.e. just the
-- builtin with no arguments) by instantiating (via 'toBuiltinRuntime') a 'BuiltinMeaning'.
--
-- A 'BuiltinRuntime' contains info that is used during evaluation:
--
-- 1. the 'TypeScheme' of the uninstantiated part of the builtin. I.e. initially it's the type
--      scheme of the whole builtin, but applying or type-instantiating the builtin peels off
--      the corresponding constructor from the type scheme
-- 2. the (possibly partially instantiated) denotation
-- 3. the (possibly partially instantiated) costing function
--
-- All the three are in sync in terms of partial instantiatedness due to 'TypeScheme' being a
-- GADT and 'FoldArgs' and 'FoldArgsEx' operating on the index of that GADT.
data BuiltinRuntime val =
    forall args res. BuiltinRuntime
        (RuntimeScheme val args res)
        ~(FoldArgs args res)  -- Must be lazy, because we don't want to compute the denotation when
                              -- it's fully saturated before figuring out what it's going to cost.
        ~(FoldArgsEx args)    -- We make this lazy, so that evaluators that don't care about costing
                              -- can put @undefined@ here. TODO: we should test if making this
                              -- strict introduces any measurable speedup.

-- | A 'BuiltinRuntime' for each builtin from a set of builtins.
newtype BuiltinsRuntime fun val = BuiltinsRuntime
    { BuiltinsRuntime fun val -> Array fun (BuiltinRuntime val)
unBuiltinRuntime :: Array fun (BuiltinRuntime val)
    }

-- | Convert a 'TypeScheme' to a 'RuntimeScheme'.
typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme :: TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme TypeScheme val args res
TypeSchemeResult       = RuntimeScheme val args res
forall val res.
KnownTypeIn (UniOf val) val res =>
RuntimeScheme val '[] res
RuntimeSchemeResult
typeSchemeToRuntimeScheme (TypeSchemeArrow TypeScheme val args res
schB) =
    RuntimeScheme val args res -> RuntimeScheme val (arg : args) res
forall val arg (args :: [*]) res.
KnownTypeIn (UniOf val) val arg =>
RuntimeScheme val args res -> RuntimeScheme val (arg : args) res
RuntimeSchemeArrow (RuntimeScheme val args res -> RuntimeScheme val (arg : args) res)
-> RuntimeScheme val args res -> RuntimeScheme val (arg : args) res
forall a b. (a -> b) -> a -> b
$ TypeScheme val args res -> RuntimeScheme val args res
forall val (args :: [*]) res.
TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme TypeScheme val args res
schB
typeSchemeToRuntimeScheme (TypeSchemeAll Proxy '(text, uniq, kind)
_ TypeScheme val args res
schK) =
    RuntimeScheme val args res -> RuntimeScheme val args res
forall val (args :: [*]) res.
RuntimeScheme val args res -> RuntimeScheme val args res
RuntimeSchemeAll (RuntimeScheme val args res -> RuntimeScheme val args res)
-> RuntimeScheme val args res -> RuntimeScheme val args res
forall a b. (a -> b) -> a -> b
$ TypeScheme val args res -> RuntimeScheme val args res
forall val (args :: [*]) res.
TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme TypeScheme val args res
schK

-- | Instantiate a 'BuiltinMeaning' given denotations of built-in functions and a cost model.
toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost
cost (BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
f cost -> FoldArgsEx args
exF) =
    RuntimeScheme val args res
-> FoldArgs args res -> FoldArgsEx args -> BuiltinRuntime val
forall val (args :: [*]) res.
RuntimeScheme val args res
-> FoldArgs args res -> FoldArgsEx args -> BuiltinRuntime val
BuiltinRuntime (TypeScheme val args res -> RuntimeScheme val args res
forall val (args :: [*]) res.
TypeScheme val args res -> RuntimeScheme val args res
typeSchemeToRuntimeScheme TypeScheme val args res
sch) FoldArgs args res
f (cost -> FoldArgsEx args
exF cost
cost)

-- | Calculate runtime info for all built-in functions given denotations of builtins
-- and a cost model.
toBuiltinsRuntime
    :: (cost ~ CostingPart uni fun, HasConstantIn uni val, ToBuiltinMeaning uni fun)
    => cost -> BuiltinsRuntime fun val
toBuiltinsRuntime :: cost -> BuiltinsRuntime fun val
toBuiltinsRuntime cost
cost =
    Array fun (BuiltinRuntime val) -> BuiltinsRuntime fun val
forall fun val.
Array fun (BuiltinRuntime val) -> BuiltinsRuntime fun val
BuiltinsRuntime (Array fun (BuiltinRuntime val) -> BuiltinsRuntime fun val)
-> ((fun -> BuiltinRuntime val) -> Array fun (BuiltinRuntime val))
-> (fun -> BuiltinRuntime val)
-> BuiltinsRuntime fun val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fun -> BuiltinRuntime val) -> Array fun (BuiltinRuntime val)
forall i a. (Bounded i, Enum i, Ix i) => (i -> a) -> Array i a
tabulateArray ((fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val)
-> (fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
forall a b. (a -> b) -> a -> b
$ cost -> BuiltinMeaning val cost -> BuiltinRuntime val
forall cost val.
cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost
cost (BuiltinMeaning val cost -> BuiltinRuntime val)
-> (fun -> BuiltinMeaning val cost) -> fun -> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. fun -> BuiltinMeaning val cost
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasConstantIn uni val) =>
fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning

-- | Look up the runtime info of a built-in function during evaluation.
lookupBuiltin
    :: (MonadError (ErrorWithCause err cause) m, AsMachineError err fun, Ix fun)
    => fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val)
-- @Data.Array@ doesn't seem to have a safe version of @(!)@, hence we use a prism.
lookupBuiltin :: fun -> BuiltinsRuntime fun val -> m (BuiltinRuntime val)
lookupBuiltin fun
fun (BuiltinsRuntime Array fun (BuiltinRuntime val)
env) = case Array fun (BuiltinRuntime val)
env Array fun (BuiltinRuntime val)
-> Getting
     (First (BuiltinRuntime val))
     (Array fun (BuiltinRuntime val))
     (BuiltinRuntime val)
-> Maybe (BuiltinRuntime val)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Index (Array fun (BuiltinRuntime val))
-> Traversal'
     (Array fun (BuiltinRuntime val))
     (IxValue (Array fun (BuiltinRuntime val)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix fun
Index (Array fun (BuiltinRuntime val))
fun of
    Maybe (BuiltinRuntime val)
Nothing  -> AReview err (MachineError fun)
-> MachineError fun -> Maybe cause -> m (BuiltinRuntime val)
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview err (MachineError fun)
forall r fun. AsMachineError r fun => Prism' r (MachineError fun)
_MachineError (fun -> MachineError fun
forall fun. fun -> MachineError fun
UnknownBuiltin fun
fun) Maybe cause
forall a. Maybe a
Nothing
    Just BuiltinRuntime val
bri -> BuiltinRuntime val -> m (BuiltinRuntime val)
forall (f :: * -> *) a. Applicative f => a -> f a
pure BuiltinRuntime val
bri