{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE StandaloneKindSignatures  #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}

{-# LANGUAGE StrictData                #-}

module PlutusCore.Builtin.Meaning where

import PlutusPrelude

import PlutusCore.Builtin.Elaborate
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.KnownKind
import PlutusCore.Builtin.KnownType
import PlutusCore.Builtin.KnownTypeAst
import PlutusCore.Builtin.Runtime
import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Name.Unique

import Data.Array
import Data.Kind qualified as GHC
import Data.Proxy
import Data.Some.GADT
import GHC.Exts (inline, lazy, oneShot)
import GHC.TypeLits

-- | Turn a list of Haskell types @args@ into a functional type ending in @res@.
--
-- >>> :set -XDataKinds
-- >>> :kind! FoldArgs [(), Bool] Integer
-- FoldArgs [(), Bool] Integer :: *
-- = () -> Bool -> Integer
type family FoldArgs args res where
    FoldArgs '[]           res = res
    FoldArgs (arg ': args) res = arg -> FoldArgs args res

-- | The meaning of a built-in function consists of its type represented as a 'TypeScheme',
-- its Haskell denotation and its uninstantiated runtime denotation.
--
-- The 'TypeScheme' of a built-in function is used for example for
--
-- 1. computing the PLC type of the function to be used during type checking
-- 2. getting arity information
-- 3. generating arbitrary values to apply the function to in tests
--
-- The denotation is lazy, so that we don't need to worry about a builtin being bottom
-- (happens in tests). The production path is not affected by that, since only runtime denotations
-- are used for evaluation.
data BuiltinMeaning val cost =
    forall args res. BuiltinMeaning
        (TypeScheme val args res)
        ~(FoldArgs args res)
        (cost -> BuiltinRuntime val)

-- | Constraints available when defining a built-in function.
type HasMeaningIn uni val = (Typeable val, ExMemoryUsage val, HasConstantIn uni val)

-- | A type class for \"each function from a set of built-in functions has a 'BuiltinMeaning'\".
class
        ( Typeable uni
        , Typeable fun
        , Bounded fun
        , Enum fun
        , Ix fun
        , Default (BuiltinSemanticsVariant fun)
        ) => ToBuiltinMeaning uni fun where
    -- | The @cost@ part of 'BuiltinMeaning'.
    type CostingPart uni fun

    -- | See Note [Builtin semantics variants]
    data BuiltinSemanticsVariant fun

    -- | Get the 'BuiltinMeaning' of a built-in function.
    toBuiltinMeaning
        :: HasMeaningIn uni val
        => BuiltinSemanticsVariant fun
        -> fun
        -> BuiltinMeaning val (CostingPart uni fun)

-- | Feed the 'TypeScheme' of the given built-in function to the continuation.
withTypeSchemeOfBuiltinFunction
    :: forall val fun r.
       (ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val, HasConstant val)
    => BuiltinSemanticsVariant fun
    -> fun
    -> (forall args res. TypeScheme val args res -> r)
    -> r
withTypeSchemeOfBuiltinFunction :: forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val,
 HasConstant val) =>
BuiltinSemanticsVariant fun
-> fun
-> (forall (args :: [*]) res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction BuiltinSemanticsVariant fun
semVar fun
fun forall (args :: [*]) res. TypeScheme val args res -> r
k =
    case BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart (UniOf val) fun)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart (UniOf val) fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun
semVar fun
fun of
        BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
_ CostingPart (UniOf val) fun -> BuiltinRuntime val
_ -> TypeScheme val args res -> r
forall (args :: [*]) res. TypeScheme val args res -> r
k TypeScheme val args res
sch

-- | Get the type of a built-in function.
typeOfBuiltinFunction
    :: forall uni fun. ToBuiltinMeaning uni fun
    => BuiltinSemanticsVariant fun
    -> fun
    -> Type TyName uni ()
typeOfBuiltinFunction :: forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
BuiltinSemanticsVariant fun -> fun -> Type TyName uni ()
typeOfBuiltinFunction BuiltinSemanticsVariant fun
semVar fun
fun =
    forall val fun r.
(ToBuiltinMeaning (UniOf val) fun, ExMemoryUsage val, Typeable val,
 HasConstant val) =>
BuiltinSemanticsVariant fun
-> fun
-> (forall (args :: [*]) res. TypeScheme val args res -> r)
-> r
withTypeSchemeOfBuiltinFunction @(Term TyName Name uni fun ()) BuiltinSemanticsVariant fun
semVar fun
fun TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName uni ()
TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName (UniOf (Term TyName Name uni fun ())) ()
forall (args :: [*]) res.
TypeScheme (Term TyName Name uni fun ()) args res
-> Type TyName uni ()
forall val (args :: [*]) res.
TypeScheme val args res -> Type TyName (UniOf val) ()
typeSchemeToType

{- Note [Builtin semantics variants]
The purpose of the "builtin semantics variant" feature is to provide multiple,
different denotations (implementations) for the same builtin(s).  An example use
of this feature is for "fixing" the behaviour of `ConsByteString` builtin to
throw an error instead of overflowing its first argument.

One denotation from each builtin is grouped into a 'BuiltinSemanticsVariant'.
Each Plutus Language version is linked to a specific 'BuiltinSemanticsVariant'
(done by plutus-ledger-api); e.g. plutus-v1 and plutus-v2 are linked to
'DefaultFunSemanticsVariantA' and 'DefaultFunSemanticsVariantB', whereas
plutus-v3 changes the set of denotations to 'DefaultFunSemanticsVariantC' (thus
fixing 'ConsByteString').

Each 'BuiltinSemanticsVariant' (grouping) can change the denotation of one or
more builtins --- or none, but what's the point in that?

This 'BuiltinSemanticsVariant' is modelled as a datatype *associated* to the
@fun@. This associated datatype is required to provide an instance of 'Default'
for quality-of-life purpose; the 'def'ault builtin semantics variant is expected
to point to the builtin semantics variant that the plutus-tx/plutus-ir compiler
is currently targeting.

Note that (old) denotations of a 'BuiltinSemanticsVariant' cannot be removed or
deprecated once published to the chain.

The way that this feature is implemented buys us more than we currently need:
- allows also a versioned change to a builtin's *type signature*, i.e. type of arguments/result as
  well as number of arguments.
- allows also a versioned change to a builtin's cost model parameters

Besides having no need for this currently, it complicates the codebase since the
typechecker now pointlessly wants to know the builtin semantics before
typechecking. To alleviate this, we use the 'Default.def' builtin semantics
variant during typechecking / lifting. @effectfully: the solution to the problem
would be to establish what kind of backwards compatibility we're willing to
maintain and pull all of that into a separate data type and make it a part of
BuiltinMeaning.
-}

{- Note [Automatic derivation of type schemes]
We use two type classes for automatic derivation of type/runtime schemes and runtime denotations:
'KnownPolytype' and 'KnownMonotype'.
The terminology is due to
https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#The_Hindley%E2%80%93Milner_
type_system

Check out the source of "PlutusCore.Builtin.Runtime" for an explanation of what a runtime
denotation is.

'KnownPolytype' and 'KnownMonotype' are responsible for deriving polymorphic and monomorphic types,
respectively.

'KnownPolytype' turns every bound variable into a 'TypeSchemeAll'/'BuiltinExpectForce'. We extract
variables from the type of the Haskell denotation using the 'ToBinds' associated type
family. Variables are collected in the order that they appear in (i.e. just like in Haskell). For
example, processing a type like

      :: ( a ~ Opaque val (TyVarRep ('TyNameRep "a" 0))
         , b ~ Opaque val (TyVarRep ('TyNameRep "b" 1))
         )
      => b -> a -> b

with 'ToBinds' results in the following list of bindings:

    '[ 'Some ('TyNameRep "b" 1), 'Some ('TyNameRep "a" 0) ]

'KnownMonotype' turns every argument that the Haskell denotation of a builtin receives into a
'TypeSchemeArrow'/'BuiltinExpectArgument'. We extract the arguments from the type of the Haskell
denotation using the 'GetArgs' type family.

Higher-kinded type variables are fully supported.

At this point in the pipeline the type of the denotation of a builtin is assumed to be fully
elaborated (i.e. monomorphic).
-}

-- | Chop a function type to get a list of its argument types.
type GetArgs :: GHC.Type -> [GHC.Type]
type family GetArgs a where
    GetArgs (a -> b) = a ': GetArgs b
    GetArgs _        = '[]

{- Note [Merging the denotation and the costing function]
The runtime denotation of a builtin computes both the builtin application and its cost
(see the docs of 'BuiltinRuntime' for details). Doing both at the same time has a number of benefits
(see Note [runCostingFun* API]), however in the user-facing API we want to separate the concepts
of the denotation and the costing function. This is because:

1. the two are fundamentally distinct and we have loads of documentation for each of them
   separately, so conflating them in the actual API would be unnecessary coupling
2. right now it's clear which bits of the definition of a builtin constitute evaluation and which
   ones constitute costing as the two are different arguments to 'makeBuiltinMeaning'. If evaluation
   and costing were intertwined, it would be much harder to review the definition of a builtin
3. ... and it would also be more boilerplate and less clear type signatures

Hence we want 'makeBuiltinMeaning' to take evaluation and costing bits separately and intertwine
them behind the scenes. Which is straightforward: we only need to pass the two together in the
methods of the 'KnownMonotype' and 'KnownPolytype' classes and zip them argument by argument
into a single 'BuiltinRuntime'.
-}

-- | A class that allows us to derive a monotype for a builtin.
-- We could've computed the runtime denotation from the
-- 'TypeScheme' and the denotation of the builtin, but not statically (due to unfolding not working
-- for recursive functions and 'TypeScheme' being recursive, i.e. requiring the conversion function
-- to be recursive), and so it would cause us to retain a lot of evaluation-irrelevant stuff in the
-- constructors of 'BuiltinRuntime', which has to make evaluation slower (we didn't check) and
-- certainly makes the generated Core much harder to read. Technically speaking, we could get
-- a 'RuntimeScheme' from the 'TypeScheme' and the denotation statically if we changed the
-- definition of 'TypeScheme' and made it a singleton, but then the conversion function would have
-- to become a class anyway and we'd just replicate what we have here, except in a much more
-- complicated way.
class KnownMonotype val args res where
    knownMonotype :: TypeScheme val args res

    -- | Convert the denotation of a builtin to its runtime counterpart .
    -- The argument is in 'ReadKnownM', because that's what deferred unlifting amounts to:
    -- passing the action returning the builtin application around until full saturation, which is
    -- when the action actually gets run.
    toMonoF
        :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
        -> BuiltinRuntime val

-- | Once we've run out of term-level arguments, we return a
-- 'TypeSchemeResult'/'RuntimeSchemeResult'.
instance (Typeable res, KnownTypeAst TyName (UniOf val) res, MakeKnown val res) =>
            KnownMonotype val '[] res where
    knownMonotype :: TypeScheme val '[] res
knownMonotype = TypeScheme val '[] res
forall res val.
(Typeable res, KnownTypeAst TyName (UniOf val) res,
 MakeKnown val res) =>
TypeScheme val '[] res
TypeSchemeResult

    toMonoF :: ReadKnownM (FoldArgs '[] res, FoldArgs '[] ExBudgetStream)
-> BuiltinRuntime val
toMonoF =
        (BuiltinError -> BuiltinRuntime val)
-> ((res, ExBudgetStream) -> BuiltinRuntime val)
-> Either BuiltinError (res, ExBudgetStream)
-> BuiltinRuntime val
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            -- Unlifting has failed and we don't care about costing at this point, since we're about
            -- to terminate evaluation anyway, hence we put 'mempty' as the cost of the operation.
            --
            -- Note that putting the cost inside of 'BuiltinResult' is not an option, since forcing
            -- the 'BuiltinResult' computation is exactly forcing the builtin application, which we
            -- can't do before accounting for the cost of the application, i.e. the cost must be
            -- outside of 'BuiltinResult'.
            --
            -- We could introduce a level of indirection and say that a 'BuiltinCostedResult' is
            -- either a budgeting failure or a budgeting success with a cost and a 'BuiltinResult'
            -- computation inside, but that would slow things down a bit and the current strategy is
            -- reasonable enough.
            BuiltinError -> BuiltinRuntime val
forall val. BuiltinError -> BuiltinRuntime val
builtinRuntimeFailure
            (\(res
x, ExBudgetStream
cost) -> ExBudgetStream
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
forall val.
ExBudgetStream
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
BuiltinCostedResult ExBudgetStream
cost (BuiltinResult (HeadSpine val) -> BuiltinRuntime val)
-> BuiltinResult (HeadSpine val) -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ res -> BuiltinResult (HeadSpine val)
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult (HeadSpine val)
makeKnown res
x)
    {-# INLINE toMonoF #-}

{- Note [One-shotting runtime denotations]
In @KnownMonotype val (arg ': args) res@ we 'oneShot' the runtime denotations. Otherwise GHC creates
let-bindings and lifts them out of some of the lambdas in the runtime denotation, which would speed
up partial applications if they were getting reused, but at some point it was verified that we
didn't have any reusage of partial applications: https://github.com/IntersectMBO/plutus/pull/4629

One-shotting the runtime denotations alone made certain game contracts slower by ~9%. A lot of time
was spent on the investigation, but we still don't know why that was happening. Plus, basically any
other change to the builtins machinery would cause the same kind of slowdown, so we just admitted
defeat and decided it wasn't worth investigating the issue further.
Relevant thread: https://github.com/IntersectMBO/plutus/pull/4620

The speedup that adding a call to 'oneShot' gives us, if any, is smaller than our noise threshold,
however it also makes those confusing allocations disappear from the generated Core, which is enough
of a reason to add the call.
-}

{- Note [Strict application in runtime denotations]
Runtime denotations contain strict let-bindings. Those are important: without them GHC thinks that
the argument may not be needed in the end and so creates a thunk for it, which is not only
unnecessary allocation, but also prevents things from being unboxed. The argument may indeed not be
needed in the end, but in that case we've got an evaluation failure and we're about to terminate
evaluation anyway, hence we care much more about optimizing the happy path.
-}

-- | Every term-level argument becomes a 'TypeSchemeArrow'/'RuntimeSchemeArrow'.
instance
        ( Typeable arg, KnownTypeAst TyName (UniOf val) arg, MakeKnown val arg, ReadKnown val arg
        , KnownMonotype val args res
        ) => KnownMonotype val (arg ': args) res where
    knownMonotype :: TypeScheme val (arg : args) res
knownMonotype = TypeScheme val args res -> TypeScheme val (arg : args) res
forall arg val (args1 :: [*]) res.
(Typeable arg, KnownTypeAst TyName (UniOf val) arg,
 MakeKnown val arg, ReadKnown val arg) =>
TypeScheme val args1 res -> TypeScheme val (arg : args1) res
TypeSchemeArrow TypeScheme val args res
forall val (args :: [*]) res.
KnownMonotype val args res =>
TypeScheme val args res
knownMonotype

    -- See Note [One-shotting runtime denotations].
    -- Grow the builtin application within the received action and recurse on the result.
    toMonoF :: ReadKnownM
  (FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
-> BuiltinRuntime val
toMonoF ReadKnownM
  (FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
getBoth = (val -> BuiltinRuntime val) -> BuiltinRuntime val
forall val. (val -> BuiltinRuntime val) -> BuiltinRuntime val
BuiltinExpectArgument ((val -> BuiltinRuntime val) -> BuiltinRuntime val)
-> ((val -> BuiltinRuntime val) -> val -> BuiltinRuntime val)
-> (val -> BuiltinRuntime val)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (val -> BuiltinRuntime val) -> val -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
oneShot ((val -> BuiltinRuntime val) -> BuiltinRuntime val)
-> (val -> BuiltinRuntime val) -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ \val
arg ->
        -- The lazy application of 'toMonoF' ensures that unlifting of the argument will happen
        -- upon full saturation and not before that. This is known as "operationally deferred
        -- unlifting" (as opposed to "operationally immediate unlifting") or "call-by-name
        -- unlifting" (as opposed to "call-by-value unlifting"). We do it this way to guarantee that
        -- the cost of unlifting will be accounted for before unlifting is performed. If we did
        -- unlifting eagerly here, this would make the node do work that is not accounted for until
        -- full saturation is reached, which may never happen if the partial application is thrown
        -- away.
        --
        -- The disadvantage of this approach is that @addInteger 42@ will always unlift @42@ upon
        -- full saturation even if this partial application is saved to a variable. But the way
        -- costing calibration benchmarks are set up, we always evaluate a single application, so
        -- the cost of unlifting is included in the cost of the builtin regardless of whether
        -- there's caching of unlifting or not. Hence the user pays for unlifting anyway and we can
        -- prioritize safety over performance here.
        --
        -- 'oneShot' ensures that GHC doesn't attempt to pull stuff out of the builtin
        -- implementation to create thunks. This would give us a "call-by-need" behavior, which may
        -- sound enticing as it would give us both caching and operationally deferred unlifting, but
        -- this comes at a cost of creating unnecessary thunks in the most common case where there's
        -- no benefit from having caching as the builtin application is going to be computed only
        -- once. So we choose the "call-by-name" behavior and 'oneShot' is what enables that.
        (Either
   BuiltinError (FoldArgs args res, FoldArgs args ExBudgetStream)
 -> BuiltinRuntime val)
-> Either
     BuiltinError (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
oneShot (forall val (args :: [*]) res.
KnownMonotype val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toMonoF @val @args @res) (Either
   BuiltinError (FoldArgs args res, FoldArgs args ExBudgetStream)
 -> BuiltinRuntime val)
-> Either
     BuiltinError (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ do
            (arg -> FoldArgs args res
f, arg -> FoldArgs args ExBudgetStream
exF) <- ReadKnownM
  (FoldArgs (arg : args) res, FoldArgs (arg : args) ExBudgetStream)
Either
  BuiltinError
  (arg -> FoldArgs args res, arg -> FoldArgs args ExBudgetStream)
getBoth
            -- Force the argument that gets passed to the denotation. This seems to help performance
            -- a bit (possibly due to its impact on strictness analysis), plus this way we ensure
            -- that if computing the argument throws an exception (isn't supposed to happen), we'll
            -- catch it in tests.
            !arg
x <- val -> ReadKnownM arg
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown val
arg
            -- See Note [Strict application in runtime denotations].
            let !exY :: FoldArgs args ExBudgetStream
exY = arg -> FoldArgs args ExBudgetStream
exF arg
x
            (FoldArgs args res, FoldArgs args ExBudgetStream)
-> Either
     BuiltinError (FoldArgs args res, FoldArgs args ExBudgetStream)
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (arg -> FoldArgs args res
f arg
x, FoldArgs args ExBudgetStream
exY)
    {-# INLINE toMonoF #-}

-- | A class that allows us to derive a polytype for a builtin.
class KnownMonotype val args res => KnownPolytype (binds :: [Some TyNameRep]) val args res where
    knownPolytype :: TypeScheme val args res

    -- | Convert the denotation of a builtin to its runtime counterpart.
    -- The argument is in 'ReadKnownM', because that's what we need to do:
    -- passing the action returning the builtin application around until full saturation, which is
    -- when the action actually gets run.
    toPolyF
        :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
        -> BuiltinRuntime val

-- | Once we've run out of type-level arguments, we start handling term-level ones.
instance KnownMonotype val args res => KnownPolytype '[] val args res where
    knownPolytype :: TypeScheme val args res
knownPolytype = TypeScheme val args res
forall val (args :: [*]) res.
KnownMonotype val args res =>
TypeScheme val args res
knownMonotype

    toPolyF :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF  = forall val (args :: [*]) res.
KnownMonotype val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toMonoF @val @args @res
    {-# INLINE toPolyF #-}

-- Here we unpack an existentially packed @kind@ and constrain it afterwards!
-- So promoted existentials are true sigmas! If we were at the term level, we'd have to pack
-- @kind@ along with the @KnownKind kind@ constraint, otherwise when we unpack the existential,
-- all information is lost and we can't do anything with @kind@.
-- | Every type-level argument becomes a 'TypeSchemeAll'.
instance (KnownSymbol name, KnownNat uniq, KnownKind kind, KnownPolytype binds val args res) =>
            KnownPolytype ('Some ('TyNameRep @kind name uniq) ': binds) val args res where
    knownPolytype :: TypeScheme val args res
knownPolytype = forall (text :: Symbol) (uniq :: Nat) kind val (args :: [*]) res.
(KnownSymbol text, KnownNat uniq, KnownKind kind) =>
Proxy '(text, uniq, kind)
-> TypeScheme val args res -> TypeScheme val args res
TypeSchemeAll @name @uniq @kind Proxy '(name, uniq, kind)
forall {k} (t :: k). Proxy t
Proxy (TypeScheme val args res -> TypeScheme val args res)
-> TypeScheme val args res -> TypeScheme val args res
forall a b. (a -> b) -> a -> b
$ forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
TypeScheme val args res
knownPolytype @binds

    toPolyF :: ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF = BuiltinRuntime val -> BuiltinRuntime val
forall val. BuiltinRuntime val -> BuiltinRuntime val
BuiltinExpectForce (BuiltinRuntime val -> BuiltinRuntime val)
-> (ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
    -> BuiltinRuntime val)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF @binds @val @args @res
    {-# INLINE toPolyF #-}

-- | Ensure a built-in function is not nullary and throw a nice error otherwise.
type ThrowOnBothEmpty :: [Some TyNameRep] -> [GHC.Type] -> Bool -> GHC.Type -> GHC.Constraint
type family ThrowOnBothEmpty binds args isBuiltin a where
    ThrowOnBothEmpty '[] '[] 'True a =
        TypeError (
            'Text "A built-in function must take at least one type or term argument" ':$$:
            'Text "‘" ':<>: 'ShowType a ':<>: 'Text "’ is a built-in type" ':<>:
            'Text " so you can embed any of its values as a constant" ':$$:
            'Text "If you still want a built-in function, add a dummy ‘()’ argument"
            )
    ThrowOnBothEmpty '[] '[] 'False a =
        TypeError (
            'Text "A built-in function must take at least one type or term argument" ':$$:
            'Text "To fix this error add a dummy ‘()’ argument"
            )
    ThrowOnBothEmpty _ _ _ _ = ()

-- | A function turned into a type class with exactly one fully general instance.
-- We can't package up the constraints of 'makeBuiltinMeaning' (see the instance) into a type or
-- class synonym, because they contain a bunch of variables defined by @~@ or determined via
-- functional dependencies and neither class nor type definitions can handle that
-- (see https://gitlab.haskell.org/ghc/ghc/-/issues/7100). Inlining three lines of constraints
-- whenever we need to call 'makeBuiltinMeaning' over a non-concrete type is a bad option and this
-- abstraction is free anyway, hence its existence.
--
-- The @a@ type variable goes first, because @makeBuiltinMeaning \@A@ is a common pattern.
class MakeBuiltinMeaning a val where
    -- See Note [Automatic derivation of type schemes]
    -- | Construct the meaning for a built-in function by automatically deriving its
    -- 'TypeScheme', given
    --
    -- 1. the denotation of the builtin
    -- 2. an uninstantiated costing function
    makeBuiltinMeaning
        :: a
        -> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
        -> BuiltinMeaning val cost
instance
        ( uni ~ UniOf val, binds ~ ToBinds uni '[] a, args ~ GetArgs a, a ~ FoldArgs args res
        , ThrowOnBothEmpty binds args (IsBuiltin uni a) a
        , ElaborateFromTo uni 0 j val a, KnownPolytype binds val args res
        ) => MakeBuiltinMeaning a val where
    makeBuiltinMeaning :: forall cost.
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning a
f cost -> FoldArgs (GetArgs a) ExBudgetStream
toExF =
        TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning (forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
TypeScheme val args res
knownPolytype @binds @val @args @res) a
FoldArgs args res
f ((cost -> BuiltinRuntime val) -> BuiltinMeaning val cost)
-> (cost -> BuiltinRuntime val) -> BuiltinMeaning val cost
forall a b. (a -> b) -> a -> b
$ \cost
cost ->
            -- In order to make the 'BuiltinRuntime' of a builtin cacheable we need to tell GHC to
            -- create a thunk for it, which we achieve by applying 'lazy' to the 'BuiltinRuntime'
            -- here.
            --
            -- Those thunks however require a lot of care to be properly shared rather than
            -- recreated every time a builtin application is evaluated, see 'toBuiltinsRuntime' for
            -- how we sort it out.
            BuiltinRuntime val -> BuiltinRuntime val
forall a. a -> a
lazy (BuiltinRuntime val -> BuiltinRuntime val)
-> BuiltinRuntime val -> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ case cost -> FoldArgs (GetArgs a) ExBudgetStream
toExF cost
cost of
                -- See Note [Optimizations of runCostingFun*] for why we use strict @case@.
                !FoldArgs (GetArgs a) ExBudgetStream
exF -> forall (binds :: [Some TyNameRep]) val (args :: [*]) res.
KnownPolytype binds val args res =>
ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
toPolyF @binds @val @args @res (ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
 -> BuiltinRuntime val)
-> ReadKnownM (FoldArgs args res, FoldArgs args ExBudgetStream)
-> BuiltinRuntime val
forall a b. (a -> b) -> a -> b
$ (a, FoldArgs args ExBudgetStream)
-> Either BuiltinError (a, FoldArgs args ExBudgetStream)
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
f, FoldArgs args ExBudgetStream
FoldArgs (GetArgs a) ExBudgetStream
exF)
    {-# INLINE makeBuiltinMeaning #-}

-- | Convert a 'BuiltinMeaning' to a 'BuiltinRuntime' given a cost model.
toBuiltinRuntime :: cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime :: forall cost val.
cost -> BuiltinMeaning val cost -> BuiltinRuntime val
toBuiltinRuntime cost
cost (BuiltinMeaning TypeScheme val args res
_ FoldArgs args res
_ cost -> BuiltinRuntime val
denot) = cost -> BuiltinRuntime val
denot cost
cost
{-# INLINE toBuiltinRuntime #-}

-- See Note [Inlining meanings of builtins].
-- | Calculate runtime info for all built-in functions given meanings of builtins (as a constraint),
-- the semantics variant of the set of builtins and a cost model.
toBuiltinsRuntime
    :: (cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun, HasMeaningIn uni val)
    => BuiltinSemanticsVariant fun
    -> cost
    -> BuiltinsRuntime fun val
toBuiltinsRuntime :: forall cost (uni :: * -> *) fun val.
(cost ~ CostingPart uni fun, ToBuiltinMeaning uni fun,
 HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun -> cost -> BuiltinsRuntime fun val
toBuiltinsRuntime BuiltinSemanticsVariant fun
semvar cost
cost =
    -- A call to 'lazy' is to make sure that the returned 'BuiltinsRuntime' is properly cached in a
    -- 'let'-binding. This makes it easier for GHC to optimize the internals of builtins, because
    -- without a 'let'-binding GHC would sometimes refuse to cooperate and push 'toBuiltinRuntime'
    -- to the inside of the inlined 'toBuiltinMeaning' call, creating lots of 'BuiltinMeaning's
    -- instead of 'BuiltinRuntime's with the former hiding the costing optimizations behind a lambda
    -- binding the @cost@ variable, which makes the optimizations useless.
    -- By using 'lazy' we tell GHC to create a separate thunk, which it can properly optimize,
    -- because the other bazillion things don't get in the way. We used to use an explicit
    -- 'let'-binding marked with @OPAQUE@, but that turned out to be unreliable, because GHC
    -- feels free to turn it into a join point instead of a proper thunk.
    BuiltinsRuntime fun val -> BuiltinsRuntime fun val
forall a. a -> a
lazy (BuiltinsRuntime fun val -> BuiltinsRuntime fun val)
-> ((fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val)
-> (fun -> BuiltinRuntime val)
-> BuiltinsRuntime fun val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
forall fun val.
(fun -> BuiltinRuntime val) -> BuiltinsRuntime fun val
BuiltinsRuntime ((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
. (BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost)
-> BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost
forall a. a -> a
inline BuiltinSemanticsVariant fun -> fun -> BuiltinMeaning val cost
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun
semvar
{-# INLINE toBuiltinsRuntime #-}