{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module PlutusCore.Default.Builtins where

import PlutusPrelude

import PlutusCore.Builtin
import PlutusCore.Data
import PlutusCore.Default.Universe
import PlutusCore.Evaluation.Machine.BuiltinCostModel
import PlutusCore.Evaluation.Machine.ExMemory
import PlutusCore.Evaluation.Result
import PlutusCore.Pretty

import Codec.Serialise (serialise)
import Crypto (verifyEcdsaSecp256k1Signature, verifyEd25519Signature, verifySchnorrSecp256k1Signature)
import Data.ByteString qualified as BS
import Data.ByteString.Hash qualified as Hash
import Data.ByteString.Lazy qualified as BS (toStrict)
import Data.Char
import Data.Ix
import Data.Text (Text)
import Data.Text.Encoding (decodeUtf8', encodeUtf8)
import Flat hiding (from, to)
import Flat.Decoder
import Flat.Encoder as Flat

-- See Note [Pattern matching on built-in types].
-- TODO: should we have the commonest builtins at the front to have more compact encoding?
-- | Default built-in functions.
--
-- When updating these, make sure to add them to the protocol version listing!
-- See Note [New builtins and protocol versions]
data DefaultFun
    -- Integers
    = AddInteger
    | SubtractInteger
    | MultiplyInteger
    | DivideInteger
    | QuotientInteger
    | RemainderInteger
    | ModInteger
    | EqualsInteger
    | LessThanInteger
    | LessThanEqualsInteger
    -- Bytestrings
    | AppendByteString
    | ConsByteString
    | SliceByteString
    | LengthOfByteString
    | IndexByteString
    | EqualsByteString
    | LessThanByteString
    | LessThanEqualsByteString
    -- Cryptography and hashes
    | Sha2_256
    | Sha3_256
    | Blake2b_256
    | VerifyEd25519Signature  -- formerly verifySignature
    | VerifyEcdsaSecp256k1Signature
    | VerifySchnorrSecp256k1Signature
    -- Strings
    | AppendString
    | EqualsString
    | EncodeUtf8
    | DecodeUtf8
    -- Bool
    | IfThenElse
    -- Unit
    | ChooseUnit
    -- Tracing
    | Trace
    -- Pairs
    | FstPair
    | SndPair
    -- Lists
    | ChooseList
    | MkCons
    | HeadList
    | TailList
    | NullList
    -- Data
    -- It is convenient to have a "choosing" function for a data type that has more than two
    -- constructors to get pattern matching over it and we may end up having multiple such data
    -- types, hence we include the name of the data type as a suffix.
    | ChooseData
    | ConstrData
    | MapData
    | ListData
    | IData
    | BData
    | UnConstrData
    | UnMapData
    | UnListData
    | UnIData
    | UnBData
    | EqualsData
    | SerialiseData
    -- Misc constructors
    -- Constructors that we need for constructing e.g. Data. Polymorphic builtin
    -- constructors are often problematic (See note [Representable built-in
    -- functions over polymorphic built-in types])
    | MkPairData
    | MkNilData
    | MkNilPairData
    deriving stock (Int -> DefaultFun -> ShowS
[DefaultFun] -> ShowS
DefaultFun -> String
(Int -> DefaultFun -> ShowS)
-> (DefaultFun -> String)
-> ([DefaultFun] -> ShowS)
-> Show DefaultFun
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DefaultFun] -> ShowS
$cshowList :: [DefaultFun] -> ShowS
show :: DefaultFun -> String
$cshow :: DefaultFun -> String
showsPrec :: Int -> DefaultFun -> ShowS
$cshowsPrec :: Int -> DefaultFun -> ShowS
Show, DefaultFun -> DefaultFun -> Bool
(DefaultFun -> DefaultFun -> Bool)
-> (DefaultFun -> DefaultFun -> Bool) -> Eq DefaultFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DefaultFun -> DefaultFun -> Bool
$c/= :: DefaultFun -> DefaultFun -> Bool
== :: DefaultFun -> DefaultFun -> Bool
$c== :: DefaultFun -> DefaultFun -> Bool
Eq, Eq DefaultFun
Eq DefaultFun
-> (DefaultFun -> DefaultFun -> Ordering)
-> (DefaultFun -> DefaultFun -> Bool)
-> (DefaultFun -> DefaultFun -> Bool)
-> (DefaultFun -> DefaultFun -> Bool)
-> (DefaultFun -> DefaultFun -> Bool)
-> (DefaultFun -> DefaultFun -> DefaultFun)
-> (DefaultFun -> DefaultFun -> DefaultFun)
-> Ord DefaultFun
DefaultFun -> DefaultFun -> Bool
DefaultFun -> DefaultFun -> Ordering
DefaultFun -> DefaultFun -> DefaultFun
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 :: DefaultFun -> DefaultFun -> DefaultFun
$cmin :: DefaultFun -> DefaultFun -> DefaultFun
max :: DefaultFun -> DefaultFun -> DefaultFun
$cmax :: DefaultFun -> DefaultFun -> DefaultFun
>= :: DefaultFun -> DefaultFun -> Bool
$c>= :: DefaultFun -> DefaultFun -> Bool
> :: DefaultFun -> DefaultFun -> Bool
$c> :: DefaultFun -> DefaultFun -> Bool
<= :: DefaultFun -> DefaultFun -> Bool
$c<= :: DefaultFun -> DefaultFun -> Bool
< :: DefaultFun -> DefaultFun -> Bool
$c< :: DefaultFun -> DefaultFun -> Bool
compare :: DefaultFun -> DefaultFun -> Ordering
$ccompare :: DefaultFun -> DefaultFun -> Ordering
$cp1Ord :: Eq DefaultFun
Ord, Int -> DefaultFun
DefaultFun -> Int
DefaultFun -> [DefaultFun]
DefaultFun -> DefaultFun
DefaultFun -> DefaultFun -> [DefaultFun]
DefaultFun -> DefaultFun -> DefaultFun -> [DefaultFun]
(DefaultFun -> DefaultFun)
-> (DefaultFun -> DefaultFun)
-> (Int -> DefaultFun)
-> (DefaultFun -> Int)
-> (DefaultFun -> [DefaultFun])
-> (DefaultFun -> DefaultFun -> [DefaultFun])
-> (DefaultFun -> DefaultFun -> [DefaultFun])
-> (DefaultFun -> DefaultFun -> DefaultFun -> [DefaultFun])
-> Enum DefaultFun
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 :: DefaultFun -> DefaultFun -> DefaultFun -> [DefaultFun]
$cenumFromThenTo :: DefaultFun -> DefaultFun -> DefaultFun -> [DefaultFun]
enumFromTo :: DefaultFun -> DefaultFun -> [DefaultFun]
$cenumFromTo :: DefaultFun -> DefaultFun -> [DefaultFun]
enumFromThen :: DefaultFun -> DefaultFun -> [DefaultFun]
$cenumFromThen :: DefaultFun -> DefaultFun -> [DefaultFun]
enumFrom :: DefaultFun -> [DefaultFun]
$cenumFrom :: DefaultFun -> [DefaultFun]
fromEnum :: DefaultFun -> Int
$cfromEnum :: DefaultFun -> Int
toEnum :: Int -> DefaultFun
$ctoEnum :: Int -> DefaultFun
pred :: DefaultFun -> DefaultFun
$cpred :: DefaultFun -> DefaultFun
succ :: DefaultFun -> DefaultFun
$csucc :: DefaultFun -> DefaultFun
Enum, DefaultFun
DefaultFun -> DefaultFun -> Bounded DefaultFun
forall a. a -> a -> Bounded a
maxBound :: DefaultFun
$cmaxBound :: DefaultFun
minBound :: DefaultFun
$cminBound :: DefaultFun
Bounded, (forall x. DefaultFun -> Rep DefaultFun x)
-> (forall x. Rep DefaultFun x -> DefaultFun) -> Generic DefaultFun
forall x. Rep DefaultFun x -> DefaultFun
forall x. DefaultFun -> Rep DefaultFun x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DefaultFun x -> DefaultFun
$cfrom :: forall x. DefaultFun -> Rep DefaultFun x
Generic, Ord DefaultFun
Ord DefaultFun
-> ((DefaultFun, DefaultFun) -> [DefaultFun])
-> ((DefaultFun, DefaultFun) -> DefaultFun -> Int)
-> ((DefaultFun, DefaultFun) -> DefaultFun -> Int)
-> ((DefaultFun, DefaultFun) -> DefaultFun -> Bool)
-> ((DefaultFun, DefaultFun) -> Int)
-> ((DefaultFun, DefaultFun) -> Int)
-> Ix DefaultFun
(DefaultFun, DefaultFun) -> Int
(DefaultFun, DefaultFun) -> [DefaultFun]
(DefaultFun, DefaultFun) -> DefaultFun -> Bool
(DefaultFun, DefaultFun) -> DefaultFun -> Int
forall a.
Ord a
-> ((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
unsafeRangeSize :: (DefaultFun, DefaultFun) -> Int
$cunsafeRangeSize :: (DefaultFun, DefaultFun) -> Int
rangeSize :: (DefaultFun, DefaultFun) -> Int
$crangeSize :: (DefaultFun, DefaultFun) -> Int
inRange :: (DefaultFun, DefaultFun) -> DefaultFun -> Bool
$cinRange :: (DefaultFun, DefaultFun) -> DefaultFun -> Bool
unsafeIndex :: (DefaultFun, DefaultFun) -> DefaultFun -> Int
$cunsafeIndex :: (DefaultFun, DefaultFun) -> DefaultFun -> Int
index :: (DefaultFun, DefaultFun) -> DefaultFun -> Int
$cindex :: (DefaultFun, DefaultFun) -> DefaultFun -> Int
range :: (DefaultFun, DefaultFun) -> [DefaultFun]
$crange :: (DefaultFun, DefaultFun) -> [DefaultFun]
$cp1Ix :: Ord DefaultFun
Ix)
    deriving anyclass (DefaultFun -> ()
(DefaultFun -> ()) -> NFData DefaultFun
forall a. (a -> ()) -> NFData a
rnf :: DefaultFun -> ()
$crnf :: DefaultFun -> ()
NFData, Int -> DefaultFun -> Int
DefaultFun -> Int
(Int -> DefaultFun -> Int)
-> (DefaultFun -> Int) -> Hashable DefaultFun
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: DefaultFun -> Int
$chash :: DefaultFun -> Int
hashWithSalt :: Int -> DefaultFun -> Int
$chashWithSalt :: Int -> DefaultFun -> Int
Hashable, PrettyBy PrettyConfigPlc)

{- Note [Textual representation of names of built-in functions]. The plc parser
 parses builtin names by looking at an enumeration of all of the built-in
 functions and checking whether the given name matches the pretty-printed name,
 obtained using the instance below.  Thus the definitive forms of the names of
 the built-in functions are obtained by applying the function below to the
 constructor names above. -}
instance Pretty DefaultFun where
    pretty :: DefaultFun -> Doc ann
pretty DefaultFun
fun = String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ case DefaultFun -> String
forall a. Show a => a -> String
show DefaultFun
fun of
        String
""    -> String
""  -- It's really weird to have a function's name displayed as an empty string,
                     -- but if it's what the 'Show' instance does, the user has asked for it.
        Char
c : String
s -> Char -> Char
toLower Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
s

instance ExMemoryUsage DefaultFun where
    memoryUsage :: DefaultFun -> ExMemory
memoryUsage DefaultFun
_ = ExMemory
1

-- | Turn a function into another function that returns 'EvaluationFailure' when its second argument
-- is 0 or calls the original function otherwise and wraps the result in 'EvaluationSuccess'.
-- Useful for correctly handling `div`, `mod`, etc.
nonZeroArg :: (Integer -> Integer -> Integer) -> Integer -> Integer -> EvaluationResult Integer
nonZeroArg :: (Integer -> Integer -> Integer)
-> Integer -> Integer -> EvaluationResult Integer
nonZeroArg Integer -> Integer -> Integer
_ Integer
_ Integer
0 = EvaluationResult Integer
forall a. EvaluationResult a
EvaluationFailure
nonZeroArg Integer -> Integer -> Integer
f Integer
x Integer
y = Integer -> EvaluationResult Integer
forall a. a -> EvaluationResult a
EvaluationSuccess (Integer -> EvaluationResult Integer)
-> Integer -> EvaluationResult Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
f Integer
x Integer
y

{- Note [How to add a built-in function: simple cases]
This Notes explains how to add a built-in function and how to read definitions of existing built-in
functions. It does not attempt to explain why things the way they are, that is explained in comments
in relevant files (will have a proper overview doc on that, but for now you can check out this
comment: https://github.com/input-output-hk/plutus/issues/4306#issuecomment-1003308938).

In order to add a new built-in function one needs to add a constructor to 'DefaultFun' and handle
it within the @ToBuiltinMeaning uni DefaultFun@ instance like this:

    toBuiltinMeaning <Name> =
        makeBuiltinMeaning
            <denotation>
            <costingFunction>

'makeBuiltinMeaning' creates a Plutus builtin out of its denotation (i.e. Haskell implementation)
and a costing function for it. Once a builtin is added, its Plutus type is kind-checked and printed
to a golden file automatically (consult @git status@).

Below we will enumerate what kind of denotations are accepted by 'makeBuiltinMeaning' without
touching any costing stuff.

1. The simplest example of an accepted denotation is a monomorphic function that takes values of
built-in types and returns a value of a built-in type as well. For example

    encodeUtf8 :: Text -> BS.ByteString

You can feed 'encodeUtf8' directly to 'makeBuiltinMeaning' without specifying any types:

    toBuiltinMeaning EncodeUtf8 =
        makeBuiltinMeaning
            encodeUtf8
            <costingFunction>

This will add the builtin, the only two things that remain are implementing costing for this
builtin (out of the scope of this Note) and handling it within the @Flat DefaultFun@ instance
(see Note [Stable encoding of PLC]).

2. If the type of the denotation has any constrained type variables in it, all of them need to be
instantiated. For example feeding @(+)@ directly to 'makeBuiltinMeaning' will give you an error
message asking to instantiate constrained type variables, which you can do via an explicit type
annotation or type application or using any other way of specifying types.

Here's how it looks with a type application instantiating the type variable of @(+)@:

    toBuiltinMeaning AddInteger =
        makeBuiltinMeaning
            ((+) @Integer)
            <costingFunction>

Or we can specify the whole type of the denotation by type-applying 'makeBuiltinMeaning':

    toBuiltinMeaning AddInteger =
        makeBuiltinMeaning
            @(Integer -> Integer -> Integer)
            (+)
            <costingFunction>

Or we can simply annotate @(+)@ with its monomorphized type:

    toBuiltinMeaning AddInteger =
        makeBuiltinMeaning
            ((+) :: Integer -> Integer -> Integer)
            <costingFunction>

All of these are equivalent.

It works the same way for a built-in function that has monomorphized polymorphic built-in types in
its type signature, for example:

    toBuiltinMeaning SumInteger =
        makeBuiltinMeaning
            (sum :: [Integer] -> Integer)
            <costingFunction>

3. Unconstrained type variables are fine, you don't need to instantiate them (but you may want to if
you want some builtin to be less general than what Haskell infers for its denotation). For example

    toBuiltinMeaning IfThenElse =
        makeBuiltinMeaning
            (\b x y -> if b then x else y)
            <costingFunction>

works alright. The inferred Haskell type of the denotation is

    forall a. Bool -> a -> a -> a

whose counterpart in Plutus is

    all a. bool -> a -> a -> a

and unsurprisingly it's the exact Plutus type of the added builtin.

It may seem like getting the latter from the former is entirely trivial, however
'makeBuiltinMeaning' jumps through quite a few hoops to achieve that and below we'll consider those
of them that are important to know to be able to use 'makeBuiltinMeaning' in cases that are more
complicated than a simple monomorphic or polymorphic function. But for now let's talk about a few
more simple cases.

4. Certain types are not built-in, but can be represented via built-in ones. For example, we don't
have 'Int' as a built-in, but we have 'Integer' and we can represent the former in terms of the
latter. The conversions between the two types are handled by 'makeBuiltinMeaning', so that the user
doesn't need to write them themselves and can just write

    toBuiltinMeaning LengthOfByteString =
        makeBuiltinMeaning
            BS.length
            <costingFunction>

directly (where @BS.length :: BS.ByteString -> Int@).

Note however that while it's always safe to convert an 'Int' to an 'Integer', doing the opposite is
not safe in general, because an 'Integer' may not fit into the range of 'Int'. For this reason

    YOU MUST NEVER USE 'fromIntegral' AND SIMILAR FUNCTIONS THAT CAN SILENTLY UNDER- OR OVERFLOW
    WHEN DEFINING A BUILT-IN FUNCTION

For example defining a builtin that takes an 'Integer' and converts it to an 'Int' using
'fromIntegral' is not allowed under any circumstances and can be a huge vulnerability.

It's completely fine to define a builtin that takes an 'Int' directly, though. How so? That's due
to the fact that the builtin application machinery checks that an 'Integer' is in the bounds of
'Int' before doing the conversion. If the bounds check succeeds, then the 'Integer' gets converted
to the corresponding 'Int', and if it doesn't, then the builtin application fails.

For the list of types that can be converted to/from built-in ones look into the file with the
default universe. If you need to add a new such type, just copy-paste what's done for an existing
one and adjust.

Speaking of builtin application failing:

5. A built-in function can fail. Whenever a builtin fails, evaluation of the whole program fails.
There's a number of ways a builtin can fail:

- as we've just seen a type conversion can fail due to an unsuccessful bounds check
- if the builtin expects, say, a 'Text' argument, but gets fed an 'Integer' argument
- if the builtin expects any constant, but gets fed a non-constant
- if its denotation runs in the 'EvaluationResult' and an 'EvaluationFailure' gets returned

Most of these are not a concern to the user defining a built-in function (conversions are handled
within the builtin application machinery, type mismatches are on the type checker and the person
writing the program etc), however explicitly returning 'EvaluationFailure' from a builtin is
something that happens commonly.

One simple example is a monomorphic function matching on a certain constructor and failing in all
other cases:

    toBuiltinMeaning UnIData =
        makeBuiltinMeaning
            (\case
                I i -> EvaluationSuccess i
                _   -> EvaluationFailure)
            <costingFunction>

The inferred type of the denotation is

    Data -> EvaluationResult Integer

and the Plutus type of the builtin is

    data -> integer

because the error effect is implicit in Plutus.

Returning @EvaluationResult a@ for a type variable @a@ is also fine, i.e. it doesn't matter whether
the denotation is monomorphic or polymorphic w.r.t. failing.

But note that

    'EvaluationResult' MUST BE EXPLICITLY USED FOR ANY FAILING BUILTIN AND THROWING AN EXCEPTION
    VIA 'error' OR 'throw' OR ELSE IS NOT ALLOWED AND CAN BE A HUGE VULNERABILITY. MAKE SURE THAT
    NONE OF THE FUNCTIONS THAT YOU USE TO DEFINE A BUILTIN THROW EXCEPTIONS

An argument of a builtin can't have 'EvaluationResult' in its type -- only the result.

6. A builtin can emit log messages. For that it needs to run in the 'Emitter' monad. The ergonomics
are the same as with 'EvaluationResult': 'Emitter' can't appear in the type of an argument and
polymorphism is fine. For example:

    toBuiltinMeaning Trace =
        makeBuiltinMeaning
            (\text a -> a <$ emitM text)
            <costingFunction>

The inferred type of the denotation is

    forall a. Text -> a -> Emitter a

and the Plutus type of the builtin is

    all a. text -> a -> a

because just like with the error effect, whether a function logs anything or not is not reflected
in its type.

'makeBuiltinMeaning' allows one to nest 'EvaluationResult' inside of 'Emitter' and vice versa,
but as always nesting monads inside of each other without using monad transformers doesn't have good
ergonomics, since computations of such a type can't be chained with a simple @(>>=)@.

This concludes the list of simple cases. Before we jump to the hard ones, we need to talk about how
polymorphism gets elaborated, so read Note [Elaboration of polymorphism] next.
-}

{- Note [Elaboration of polymorphism]
In Note [How to add a built-in function: simple cases] we defined the following builtin:

    toBuiltinMeaning IfThenElse =
        makeBuiltinMeaning
            (\b x y -> if b then x else y)
            <costingFunction>

whose inferred Haskell type is

    forall a. Bool -> a -> a -> a

The way 'makeBuiltinMeaning' handles such a type is by traversing it and instantiating every type
variable. What a type variable gets instantiated to depends on where it appears. When the entire
type of an argument is a single type variable, it gets instantiated to @Opaque val VarN@ where
@VarN@ is pseudocode for "a Haskell type representing a Plutus type variable with 'Unique' N"
For the purpose of this explanation it doesn't matter what @VarN@ actually is and the representation
is subject to change anyway. 'Opaque' however is more fundamental and so we need to talk about it.
Here's how it's defined:

    newtype Opaque val (rep :: GHC.Type) = Opaque
        { unOpaque :: val
        }

I.e. @Opaque val rep@ is a wrapper around @val@, which stands for the type of value that an
evaluator uses (the builtins machinery is designed to work with any evaluator and different
evaluators define their type of values differently, for example 'CkValue' if the type of value for
the CK machine). The idea is simple: in order to apply the denotation of a builtin expecting, say,
an 'Integer' constant we need to actually extract that 'Integer' from the AST of the given value,
but if the denotation is polymorphic over the type of its argument, then we don't need to extract
anything, we can just pass the AST of the value directly to the denotation. I.e. in order for a
polymorphic function to become a monomorphic denotation (denotations are always monomorpic) all type
variables in the type of that function need to be instantiated at the type of value that a given
evaluator uses.

If we used just @val@ rathen than @Opaque val rep@, we'd specialize

    forall a. Bool -> a -> a -> a

to

    Bool -> val -> val -> val

however then we'd need to separately specify the Plutus type of this builtin, since we can't infer
it from all these @val@s in the general case, for example does

    val -> val -> val

stand for

    all a. a -> a -> a

or

    all a b. a -> b -> a

or something else?

So we use the @Opaque val rep@ wrapper, which is basically a @val@ with a @rep@ attached to it where
@rep@ represents the Plutus type of the argument/result, which is how we arrive at

    Bool -> Opaque val Var0 -> Opaque val Var0 -> Opaque val Var0

Not only does this encoding allow us to specify both the Haskell and the Plutus types of the
builtin simultaneously, but it also makes it possible to infer such a type from a regular
polymorphic Haskell function (how that is done is a whole another story), so that we don't even need
to specify any types when creating builtins out of simple polymorphic functions.

If we wanted to specify the type explicitly, we could do it like this (leaving out the @Var0@ thing
for the elaboration machinery to figure out):

    toBuiltinMeaning IfThenElse =
        makeBuiltinMeaning
            @(Bool -> Opaque val _ -> Opaque val _ -> Opaque val _)
            (\b x y -> if b then x else y)
            <costingFunction>

and it would be equivalent to the original definition. We didn't do that, because why bother if
the correct thing gets inferred anyway.

Another thing we could do is define an auxiliary function with a type signature and explicit
'Opaque' while still having explicit polymorphism:

    ifThenElse :: Bool -> Opaque val a -> Opaque val a -> Opaque val a
    ifThenElse b x y = if b then x else y

    toBuiltinMeaning IfThenElse =
        makeBuiltinMeaning
            ifThenElse
            <costingFunction>

This achieves the same, but note how @a@ is now an argument to 'Opaque' rather than the entire type
of an argument. In order for this definition to elaborate to the same type as before @a@ needs to be
instantiated to just @Var0@, as opposed to @Opaque val Var0@, because the 'Opaque' part is
already there, so this is what the elaboration machinery does.

So regardless of which method of defining 'IfThenElse' we choose, the type of its denotation gets
elaborated to the same

    Bool -> Opaque val Var0 -> Opaque val Var0 -> Opaque val Var0

which then gets digested, so that we can compute what Plutus type it corresponds to. The procedure
is simple: collect all distinct type variables, @all@-bind them and replace the usages with the
bound variables. This turns the type above into

    all a. bool -> a -> a -> a

which is the Plutus type of the 'IfThenElse' builtin.

It's of course allowed to have multiple type variables, e.g. in the following snippet:

    toBuiltinMeaning Const =
        makeBuiltinMeaning
            Prelude.const
            <costingFunction>

the Haskell type of 'const' gets inferred as

    forall a b. a -> b -> a

and the elaboration machinery turns that into

    Opaque val Var0 -> Opaque val Var1 -> Opaque val Var0

The elaboration machinery respects the explicitly specified parts of the type and does not attempt
to argue with them. For example if the user insisted that the instantiated type of 'const' had
@Var0@ and @Var1@ swapped:

    Opaque val Var1 -> Opaque val Var0 -> Opaque val Var1

the elaboration machinery wouldn't make a fuss about that.

As a final simple example, consider

    toBuiltinMeaning Trace =
        makeBuiltinMeaning
            (\text a -> a <$ emitM text)
            <costingFunction>

from [How to add a built-in function: simple cases]. The inferred type of the denotation is

    forall a. Text -> a -> Emitter a

which elaborates to

    Text -> Opaque val Var0 -> Emitter (Opaque val Var0)

Elaboration machinery is able to look under 'Emitter' and 'EvaluationResult' even if there's a type
variable inside that does not appear anywhere else in the type signature, for example the inferred
type of the denotation in

    toBuiltinMeaning ErrorPrime =
        makeBuiltinMeaning
            EvaluationFailure
            <costingFunction>

is

    forall a. EvaluationResult a

which gets elaborated to

    EvaluationResult (Opaque val Var0)

from which the final Plutus type of the builtin is computed:

    all a. a

Read Note [How to add a built-in function: complicated cases] next.
-}

{- Note [How to add a built-in function: complicated cases]
Now let's talk about more complicated built-in functions.

1. In Note [Elaboration of polymorphism] we saw how a Haskell type variable gets elaborated to an
@Opaque val VarN@ and we learned that this type can be used directly as opposed to being inferred.
However there exist more ways to use 'Opaque' explicitly. Here's a simple example:

    toBuiltinMeaning IdAssumeBool =
        makeBuiltinMeaning
            (Prelude.id :: Opaque val Bool -> Opaque val Bool)
            <costingFunction>

This creates a built-in function whose Plutus type is

    id : bool -> bool

i.e. the Plutus type signature of the built-in function is the same as with

    toBuiltinMeaning IdBool =
        makeBuiltinMeaning
            (Prelude.id :: Bool -> Bool)
            <costingFunction>

but the two evaluate differently: the former takes a value and returns it right away while the
latter takes a value, extracts a 'Bool' constant out of it and then lifts that constant back into
@val@. The difference is not only in performance (obviously returning something right away is
cheaper than unlifting-then-lifting-back), but also in semantics: the former returns its argument
during evaluation regardless of what that argument is, so if someone generates Untyped Plutus Core
directly, they can apply @IdAssumeBool@ to a term that doesn't evaluate to a 'Bool' constant or
even a constant at all and that won't be a runtime error, while the latter has to be applied to
a term evaluating to a 'Bool' constant in order not to fail at runtime.

2. @val@ in @Opaque val rep@ is not completely arbitrary, it has to implement 'HasConstant', which
makes it possible to unlift @val@ as a constant or lift a constant back into @val@. There's a
'HasConstant' instance for @Opaque val rep@ whenever there's one for @val@, so if we, for some
reason, wanted to have 'Opaque' in the type signature of the denotation, but still unlift the
argument as a 'Bool', we could do that:

    toBuiltinMeaning IdAssumeCheckBool =
        makeBuiltinMeaning
            idAssumeCheckBoolPlc
            <costingFunction>
      where
        idAssumeCheckBoolPlc :: Opaque val Bool -> EvaluationResult Bool
        idAssumeCheckBoolPlc val =
            case asConstant @_ @UnliftingError Nothing val of
                Right (Some (ValueOf DefaultUniBool b)) -> EvaluationSuccess b
                _                                       -> EvaluationFailure

Here in the denotation we unlift the given value as a constant, check that its type tag is
'DefaultUniBool' and return the unlifted 'Bool'. If any of that fails, we return an explicit
'EvaluationFailure'.

This achieves almost the same as 'IdBool', which keeps all the bookkeeping behind the scenes, but
there are a couple of differences:

- 'asConstant' is given 'Nothing' as the cause of a potential failure
- in case of error its message is ignored

We could fix the latter, but changing the former is non-trivial: in general, the cause of a failure
can be an arbitrary term, not just a value, and the meaning of a built-in function doesn't know
anything about general terms, it only deals with values. The cause of a potential failure is
provided to the builtins machinery from the outside (from within the internals of the CEK machine
for example) and refactoring the builtins machinery into being aware of failure causes would force
us to attach a term representation to each argument, which would make for a horrible interface.

3. There's a middle ground between automatic and manual unlifting to 'Bool', one can unlift
automatically to a constant and then unlift manually to 'Bool' using the 'SomeConstant' wrapper:

    newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant
        { unSomeConstant :: Some (ValueOf uni)
        }

'SomeConstant' is similar to 'Opaque' in that it has a @rep@ representing a Plutus type.
The difference is that 'Opaque' is a wrapper around an arbitrary value and 'SomeConstant' is a
wrapper around a constant. 'SomeConstant' allows one to automatically unlift an argument of a
built-in function as a constant with all 'asConstant' business kept behind the scenes, for example:

    toBuiltinMeaning IdSomeConstantBool =
        makeBuiltinMeaning
            idSomeConstantBoolPlc
            <costingFunction>
      where
        idSomeConstantBoolPlc :: SomeConstant uni Bool -> EvaluationResult Bool
        idSomeConstantBoolPlc = \case
            SomeConstant (Some (ValueOf DefaultUniBool b)) -> EvaluationSuccess b
            _                                              -> EvaluationFailure

Note how we no longer call 'asConstant' manually, but still manually match on 'DefaultUniBool'.

So there's a whole range of how "low-level" one can choose to be when defining a built-in function.
However it's not always possible to use automatic unlifting, see next.

4. If we try to define the following built-in function:

    toBuiltinMeaning NullList =
        makeBuiltinMeaning
            (null :: [a] -> Bool)
            <costingFunction>

we'll get an error, saying that a polymorphic built-in type can't be applied to a type variable.
It's not impossible to make it work, see Note [Unlifting values of built-in types], but not in the
general case, plus it has to be very inefficient.

Instead we have to use 'SomeConstant' to automatically unlift to a constant and then check that the
value inside of it is a list (by matching on the type tag):

    toBuiltinMeaning NullList =
        makeBuiltinMeaning
            nullPlc
            <costingFunction>
        where
          nullPlc :: SomeConstant uni [a] -> EvaluationResult Bool
          nullPlc (SomeConstant (Some (ValueOf uniListA xs))) = do
              DefaultUniList _ <- pure uniListA
              pure $ null xs

('EvaluationResult' has a 'MonadFail' instance allowing us to use the @<pat> <- pure <expr>@ idiom)

As before, we have to match on the type tag, because there's no relation between @rep@ from
@SomeConstant uni rep@ and the constant that the built-in function actually receives at runtime
(someone could generate Untyped Plutus Core directly and apply 'nullPlc' to an 'Integer' or
whatever). @rep@ is only for the Plutus type checker to look at, it doesn't influence evaluation
in any way.

Here's a similar built-in function:

    toBuiltinMeaning FstPair =
        makeBuiltinMeaning
            fstPlc
            <costingFunction>
        where
          fstPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque val a)
          fstPlc (SomeConstant (Some (ValueOf uniPairAB xy))) = do
              DefaultUniPair uniA _ <- pure uniPairAB          -- [1]
              pure . fromConstant . someValueOf uniA $ fst xy  -- [2]

In this definition we extract the first element of a pair by checking that the given constant is
indeed a pair [1] and lifting its first element into @val@ using the type tag for the first
element [2] (extracted from the type tag for the whole pair constant [1]).

Note that it's fine to mix automatic unlifting for polymorphism not related to built-in types and
manual unlifting for arguments having non-monomorphized polymorphic built-in types, for example:

    toBuiltinMeaning ChooseList =
        makeBuiltinMeaning
            choosePlc
            <costingFunction>
        where
          choosePlc :: SomeConstant uni [a] -> b -> b -> EvaluationResult b
          choosePlc (SomeConstant (Some (ValueOf uniListA xs))) a b = do
            DefaultUniList _ <- pure uniListA
            pure $ case xs of
                []    -> a
                _ : _ -> b

Here @a@ appears inside @[]@, which is a polymorphic built-in type, and so we have to use
'SomeConstant' and check that the given constant is indeed a list, while @b@ doesn't appear inside
of any built-in type and so we don't need to instantiate it to 'Opaque' manually, the elaboration
machinery will do it for us.

Our final example is this:

    toBuiltinMeaning MkCons =
        makeBuiltinMeaning
            consPlc
            <costingFunction>
        where
          consPlc
              :: SomeConstant uni a -> SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
          consPlc
            (SomeConstant (Some (ValueOf uniA x)))
            (SomeConstant (Some (ValueOf uniListA xs))) = do
                DefaultUniList uniA' <- pure uniListA                -- [1]
                Just Refl <- pure $ uniA `geq` uniA'                 -- [2]
                pure . fromConstant . someValueOf uniListA $ x : xs  -- [3]

Here we prepend an element to a list [3] after checking that the second argument is indeed a
list [1] and that the type tag of the element being prepended equals the type tag for elements of
the list [2] (extracted from the type tag for the whole list constant [1]).
-}

instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where
    type CostingPart uni DefaultFun = BuiltinCostModel
    -- Integers
    toBuiltinMeaning
        :: forall val. HasConstantIn uni val
        => DefaultFun -> BuiltinMeaning val BuiltinCostModel
    toBuiltinMeaning :: DefaultFun -> BuiltinMeaning val BuiltinCostModel
toBuiltinMeaning DefaultFun
AddInteger =
        (Integer -> Integer -> Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Num Integer => Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramAddInteger)
    toBuiltinMeaning DefaultFun
SubtractInteger =
        (Integer -> Integer -> Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((-) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramSubtractInteger)
    toBuiltinMeaning DefaultFun
MultiplyInteger =
        (Integer -> Integer -> Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Num Integer => Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramMultiplyInteger)
    toBuiltinMeaning DefaultFun
DivideInteger =
        (Integer -> Integer -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((Integer -> Integer -> Integer)
-> Integer -> Integer -> EvaluationResult Integer
nonZeroArg Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramDivideInteger)
    toBuiltinMeaning DefaultFun
QuotientInteger =
        (Integer -> Integer -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((Integer -> Integer -> Integer)
-> Integer -> Integer -> EvaluationResult Integer
nonZeroArg Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
quot)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramQuotientInteger)
    toBuiltinMeaning DefaultFun
RemainderInteger =
        (Integer -> Integer -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((Integer -> Integer -> Integer)
-> Integer -> Integer -> EvaluationResult Integer
nonZeroArg Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
rem)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramRemainderInteger)
    toBuiltinMeaning DefaultFun
ModInteger =
        (Integer -> Integer -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((Integer -> Integer -> Integer)
-> Integer -> Integer -> EvaluationResult Integer
nonZeroArg Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramModInteger)
    toBuiltinMeaning DefaultFun
EqualsInteger =
        (Integer -> Integer -> Bool)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Eq Integer => Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramEqualsInteger)
    toBuiltinMeaning DefaultFun
LessThanInteger =
        (Integer -> Integer -> Bool)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Ord Integer => Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramLessThanInteger)
    toBuiltinMeaning DefaultFun
LessThanEqualsInteger =
        (Integer -> Integer -> Bool)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Ord Integer => Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<=) @Integer)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramLessThanEqualsInteger)
    -- Bytestrings
    toBuiltinMeaning DefaultFun
AppendByteString =
        (ByteString -> ByteString -> ByteString)
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> ByteString -> ByteString
BS.append
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramAppendByteString)
    toBuiltinMeaning DefaultFun
ConsByteString =
        (Integer -> ByteString -> ByteString)
-> (BuiltinCostModel
    -> ToCostingType (Length '[Integer, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\Integer
n ByteString
xs -> Word8 -> ByteString -> ByteString
BS.cons (Integer -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral @Integer Integer
n) ByteString
xs)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramConsByteString)
    toBuiltinMeaning DefaultFun
SliceByteString =
        (Int -> Int -> ByteString -> ByteString)
-> (BuiltinCostModel
    -> ToCostingType (Length '[Int, Int, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\Int
start Int
n ByteString
xs -> Int -> ByteString -> ByteString
BS.take Int
n (Int -> ByteString -> ByteString
BS.drop Int
start ByteString
xs))
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramSliceByteString)
    toBuiltinMeaning DefaultFun
LengthOfByteString =
        (ByteString -> Int)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> Int
BS.length
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramLengthOfByteString)
    toBuiltinMeaning DefaultFun
IndexByteString =
        (ByteString -> Int -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString, Int]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\ByteString
xs Int
n -> if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ByteString -> Int
BS.length ByteString
xs then Integer -> EvaluationResult Integer
forall a. a -> EvaluationResult a
EvaluationSuccess (Integer -> EvaluationResult Integer)
-> Integer -> EvaluationResult Integer
forall a b. (a -> b) -> a -> b
$ Word8 -> Integer
forall a. Integral a => a -> Integer
toInteger (Word8 -> Integer) -> Word8 -> Integer
forall a b. (a -> b) -> a -> b
$ ByteString -> Int -> Word8
BS.index ByteString
xs Int
n else EvaluationResult Integer
forall a. EvaluationResult a
EvaluationFailure)
            -- TODO: fix the mess above with `indexMaybe` from `bytestring >= 0.11.0.0`.
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramIndexByteString)
    toBuiltinMeaning DefaultFun
EqualsByteString =
        (ByteString -> ByteString -> Bool)
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Eq ByteString => ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
(==) @BS.ByteString)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramEqualsByteString)
    toBuiltinMeaning DefaultFun
LessThanByteString =
        (ByteString -> ByteString -> Bool)
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Ord ByteString => ByteString -> ByteString -> Bool
forall a. Ord a => a -> a -> Bool
(<) @BS.ByteString)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramLessThanByteString)
    toBuiltinMeaning DefaultFun
LessThanEqualsByteString =
        (ByteString -> ByteString -> Bool)
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Ord ByteString => ByteString -> ByteString -> Bool
forall a. Ord a => a -> a -> Bool
(<=) @BS.ByteString)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramLessThanEqualsByteString)
    -- Cryptography and hashes
    toBuiltinMeaning DefaultFun
Sha2_256 =
        (ByteString -> ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> ByteString
Hash.sha2_256
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramSha2_256)
    toBuiltinMeaning DefaultFun
Sha3_256 =
        (ByteString -> ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> ByteString
Hash.sha3_256
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramSha3_256)
    toBuiltinMeaning DefaultFun
Blake2b_256 =
        (ByteString -> ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> ByteString
Hash.blake2b_256
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramBlake2b_256)
    toBuiltinMeaning DefaultFun
VerifyEd25519Signature =
        (ByteString -> ByteString -> ByteString -> EvaluationResult Bool)
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Alternative EvaluationResult =>
ByteString -> ByteString -> ByteString -> EvaluationResult Bool
forall (f :: * -> *).
Alternative f =>
ByteString -> ByteString -> ByteString -> f Bool
verifyEd25519Signature @EvaluationResult)
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramVerifyEd25519Signature)
    {- Note [ECDSA secp256k1 signature verification].  An ECDSA signature
       consists of a pair of values (r,s), and for each value of r there are in
       fact two valid values of s, one effectively the negative of the other.
       The Bitcoin implementation that underlies `verifyEcdsaSecp256k1Signature`
       expects that the lower of the two possible values of the s component of
       the signature is used, returning `false` immediately if that's not the
       case.  It appears that this restriction is peculiar to Bitcoin, and ECDSA
       schemes in general don't require it.  Thus this function may be more
       restrictive than expected.  See

          https://github.com/bitcoin/bips/blob/master/bip-0146.mediawiki#LOW_S

       and the implementation of secp256k1_ecdsa_verify in

          https://github.com/bitcoin-core/secp256k1.
     -}
    toBuiltinMeaning DefaultFun
VerifyEcdsaSecp256k1Signature =
        (ByteString
 -> ByteString -> ByteString -> Emitter (EvaluationResult Bool))
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString
-> ByteString -> ByteString -> Emitter (EvaluationResult Bool)
verifyEcdsaSecp256k1Signature
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramVerifyEcdsaSecp256k1Signature)
    toBuiltinMeaning DefaultFun
VerifySchnorrSecp256k1Signature =
        (ByteString
 -> ByteString -> ByteString -> Emitter (EvaluationResult Bool))
-> (BuiltinCostModel
    -> ToCostingType (Length '[ByteString, ByteString, ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString
-> ByteString -> ByteString -> Emitter (EvaluationResult Bool)
verifySchnorrSecp256k1Signature
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramVerifySchnorrSecp256k1Signature)
    -- Strings
    toBuiltinMeaning DefaultFun
AppendString =
        (Text -> Text -> Text)
-> (BuiltinCostModel -> ToCostingType (Length '[Text, Text]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Semigroup Text => Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
(<>) @Text)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramAppendString)
    toBuiltinMeaning DefaultFun
EqualsString =
        (Text -> Text -> Bool)
-> (BuiltinCostModel -> ToCostingType (Length '[Text, Text]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Eq Text => Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) @Text)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramEqualsString)
    toBuiltinMeaning DefaultFun
EncodeUtf8 =
        (Text -> ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[Text]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Text -> ByteString
encodeUtf8
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramEncodeUtf8)
    toBuiltinMeaning DefaultFun
DecodeUtf8 =
        (ByteString -> EvaluationResult Text)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (forall a.
(Foldable (Either UnicodeException),
 Alternative EvaluationResult) =>
Either UnicodeException a -> EvaluationResult a
forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Alternative g) =>
f a -> g a
reoption @_ @EvaluationResult (Either UnicodeException Text -> EvaluationResult Text)
-> (ByteString -> Either UnicodeException Text)
-> ByteString
-> EvaluationResult Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Either UnicodeException Text
decodeUtf8')
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramDecodeUtf8)
    -- Bool
    toBuiltinMeaning DefaultFun
IfThenElse =
        (Bool
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            (Bool
               : GetArgs
                   (Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))))))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\Bool
b Opaque val (TyVarRep ('TyNameRep "a" 0))
x Opaque val (TyVarRep ('TyNameRep "a" 0))
y -> if Bool
b then Opaque val (TyVarRep ('TyNameRep "a" 0))
x else Opaque val (TyVarRep ('TyNameRep "a" 0))
y)
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramIfThenElse)
    -- Unit
    toBuiltinMeaning DefaultFun
ChooseUnit =
        (()
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            (()
               : GetArgs
                   (Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))))))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\() Opaque val (TyVarRep ('TyNameRep "a" 0))
a -> Opaque val (TyVarRep ('TyNameRep "a" 0))
a)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramChooseUnit)
    -- Tracing
    toBuiltinMeaning DefaultFun
Trace =
        (Text
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Emitter (Opaque val (TyVarRep ('TyNameRep "a" 0))))
-> (BuiltinCostModel
    -> ToCostingType
         (Length '[Text, Opaque val (TyVarRep ('TyNameRep "a" 0))]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\Text
text Opaque val (TyVarRep ('TyNameRep "a" 0))
a -> Opaque val (TyVarRep ('TyNameRep "a" 0))
a Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Emitter () -> Emitter (Opaque val (TyVarRep ('TyNameRep "a" 0)))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> Emitter ()
emit Text
text)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramTrace)
    -- Pairs
    toBuiltinMeaning DefaultFun
FstPair =
        (SomeConstant
   uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0))))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            '[SomeConstant
                DefaultUni
                (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant
  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
forall a b.
SomeConstant uni (a, b) -> EvaluationResult (Opaque val a)
fstPlc
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramFstPair)
        where
          fstPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque val a)
          fstPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque val a)
fstPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
xy))) = do
              DefaultUniPair uniA _ <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
              Opaque val a -> EvaluationResult (Opaque val a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Opaque val a -> EvaluationResult (Opaque val a))
-> (a2 -> Opaque val a) -> a2 -> EvaluationResult (Opaque val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> Opaque val a
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf DefaultUni) -> Opaque val a)
-> (a2 -> Some (ValueOf DefaultUni)) -> a2 -> Opaque val a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc a2) -> a2 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a2)
DefaultUni (Esc a2)
uniA (a2 -> EvaluationResult (Opaque val a))
-> a2 -> EvaluationResult (Opaque val a)
forall a b. (a -> b) -> a -> b
$ (a2, a1) -> a2
forall a b. (a, b) -> a
fst a
(a2, a1)
xy
          {-# INLINE fstPlc #-}
    toBuiltinMeaning DefaultFun
SndPair =
        (SomeConstant
   uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "b" 1))))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            '[SomeConstant
                DefaultUni
                (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant
  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "b" 1)))
forall a b.
SomeConstant uni (a, b) -> EvaluationResult (Opaque val b)
sndPlc
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramSndPair)
        where
          sndPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque val b)
          sndPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque val b)
sndPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
xy))) = do
              DefaultUniPair _ uniB <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
              Opaque val b -> EvaluationResult (Opaque val b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Opaque val b -> EvaluationResult (Opaque val b))
-> (a1 -> Opaque val b) -> a1 -> EvaluationResult (Opaque val b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> Opaque val b
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf DefaultUni) -> Opaque val b)
-> (a1 -> Some (ValueOf DefaultUni)) -> a1 -> Opaque val b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
uniB (a1 -> EvaluationResult (Opaque val b))
-> a1 -> EvaluationResult (Opaque val b)
forall a b. (a -> b) -> a -> b
$ (a2, a1) -> a1
forall a b. (a, b) -> b
snd a
(a2, a1)
xy
          {-# INLINE sndPlc #-}
    -- Lists
    toBuiltinMeaning DefaultFun
ChooseList =
        (SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
 -> Opaque val (TyVarRep ('TyNameRep "b" 1))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1))
 -> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "b" 1))))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            '[SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)],
              Opaque val (TyVarRep ('TyNameRep "b" 1)),
              Opaque val (TyVarRep ('TyNameRep "b" 1))]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "b" 1)))
forall a b. SomeConstant uni [a] -> b -> b -> EvaluationResult b
choosePlc
            (CostingFun ModelThreeArguments
-> ExMemory -> ExMemory -> ExMemory -> ExBudget
runCostingFunThreeArguments (CostingFun ModelThreeArguments
 -> ExMemory -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelThreeArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelThreeArguments
forall (f :: * -> *).
BuiltinCostModelBase f -> f ModelThreeArguments
paramChooseList)
        where
          choosePlc :: SomeConstant uni [a] -> b -> b -> EvaluationResult b
          choosePlc :: SomeConstant uni [a] -> b -> b -> EvaluationResult b
choosePlc (SomeConstant (Some (ValueOf uni (Esc a)
uniListA a
xs))) b
a b
b = do
            DefaultUniList _ <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniListA
            b -> EvaluationResult b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> EvaluationResult b) -> b -> EvaluationResult b
forall a b. (a -> b) -> a -> b
$ case a
xs of
                []    -> b
a
                _ : _ -> b
b
          {-# INLINE choosePlc #-}
    toBuiltinMeaning DefaultFun
MkCons =
        (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
 -> EvaluationResult (Opaque val [TyVarRep ('TyNameRep "a" 0)]))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            '[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)),
              SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
-> EvaluationResult (Opaque val [TyVarRep ('TyNameRep "a" 0)])
forall a.
SomeConstant uni a
-> SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
consPlc
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramMkCons)
        where
          consPlc
              :: SomeConstant uni a -> SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
          consPlc :: SomeConstant uni a
-> SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
consPlc
            (SomeConstant (Some (ValueOf uni (Esc a)
uniA a
x)))
            (SomeConstant (Some (ValueOf uni (Esc a)
uniListA a
xs))) = do
                DefaultUniList uniA' <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniListA
                -- Checking that the type of the constant is the same as the type of the elements
                -- of the unlifted list. Note that there's no way we could enforce this statically
                -- since in UPLC one can create an ill-typed program that attempts to prepend
                -- a value of the wrong type to a list.
                -- Should that rather give us an 'UnliftingError'? For that we need
                -- https://github.com/input-output-hk/plutus/pull/3035
                Just Esc a :~: Esc a1
Refl <- Maybe (Esc a :~: Esc a1)
-> EvaluationResult (Maybe (Esc a :~: Esc a1))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a1)
 -> EvaluationResult (Maybe (Esc a :~: Esc a1)))
-> Maybe (Esc a :~: Esc a1)
-> EvaluationResult (Maybe (Esc a :~: Esc a1))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniA uni (Esc a) -> uni (Esc a1) -> Maybe (Esc a :~: Esc a1)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a1)
DefaultUni (Esc a1)
uniA'
                Opaque val [a] -> EvaluationResult (Opaque val [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Opaque val [a] -> EvaluationResult (Opaque val [a]))
-> (a -> Opaque val [a]) -> a -> EvaluationResult (Opaque val [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> Opaque val [a]
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf uni) -> Opaque val [a])
-> (a -> Some (ValueOf uni)) -> a -> Opaque val [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> a -> Some (ValueOf uni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
uniListA (a -> EvaluationResult (Opaque val [a]))
-> a -> EvaluationResult (Opaque val [a])
forall a b. (a -> b) -> a -> b
$ a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a
[a]
xs
          {-# INLINE consPlc #-}
    toBuiltinMeaning DefaultFun
HeadList =
        (SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
 -> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0))))
-> (BuiltinCostModel
    -> ToCostingType
         (Length '[SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
-> EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
forall a. SomeConstant uni [a] -> EvaluationResult (Opaque val a)
headPlc
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramHeadList)
        where
          headPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque val a)
          headPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque val a)
headPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniListA a
xs))) = do
              DefaultUniList uniA <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniListA
              x : _ <- a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
xs
              Opaque val a -> EvaluationResult (Opaque val a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Opaque val a -> EvaluationResult (Opaque val a))
-> (Some (ValueOf DefaultUni) -> Opaque val a)
-> Some (ValueOf DefaultUni)
-> EvaluationResult (Opaque val a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> Opaque val a
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf DefaultUni) -> EvaluationResult (Opaque val a))
-> Some (ValueOf DefaultUni) -> EvaluationResult (Opaque val a)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
uniA a1
x
          {-# INLINE headPlc #-}
    toBuiltinMeaning DefaultFun
TailList =
        (SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
 -> EvaluationResult (Opaque val [TyVarRep ('TyNameRep "a" 0)]))
-> (BuiltinCostModel
    -> ToCostingType
         (Length '[SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
-> EvaluationResult (Opaque val [TyVarRep ('TyNameRep "a" 0)])
forall a. SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
tailPlc
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramTailList)
        where
          tailPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
          tailPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque val [a])
tailPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniListA a
xs))) = do
              DefaultUniList _ <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniListA
              _ : xs' <- a -> EvaluationResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
xs
              Opaque val [a] -> EvaluationResult (Opaque val [a])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Opaque val [a] -> EvaluationResult (Opaque val [a]))
-> (Some (ValueOf uni) -> Opaque val [a])
-> Some (ValueOf uni)
-> EvaluationResult (Opaque val [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> Opaque val [a]
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf uni) -> EvaluationResult (Opaque val [a]))
-> Some (ValueOf uni) -> EvaluationResult (Opaque val [a])
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> a -> Some (ValueOf uni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
uniListA a
[a1]
xs'
          {-# INLINE tailPlc #-}
    toBuiltinMeaning DefaultFun
NullList =
        (SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
 -> EvaluationResult Bool)
-> (BuiltinCostModel
    -> ToCostingType
         (Length '[SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni [TyVarRep ('TyNameRep "a" 0)]
-> EvaluationResult Bool
forall a. SomeConstant uni [a] -> EvaluationResult Bool
nullPlc
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramNullList)
        where
          nullPlc :: SomeConstant uni [a] -> EvaluationResult Bool
          nullPlc :: SomeConstant uni [a] -> EvaluationResult Bool
nullPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniListA a
xs))) = do
              DefaultUniList _ <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniListA
              Bool -> EvaluationResult Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> EvaluationResult Bool) -> Bool -> EvaluationResult Bool
forall a b. (a -> b) -> a -> b
$ [a1] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null a
[a1]
xs
          {-# INLINE nullPlc #-}

    -- Data
    toBuiltinMeaning DefaultFun
ChooseData =
        (Data
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (BuiltinCostModel
    -> ToCostingType
         (Length
            (Data
               : GetArgs
                   (Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))
                    -> Opaque val (TyVarRep ('TyNameRep "a" 0))))))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\Data
d
              Opaque val (TyVarRep ('TyNameRep "a" 0))
xConstr
              Opaque val (TyVarRep ('TyNameRep "a" 0))
xMap Opaque val (TyVarRep ('TyNameRep "a" 0))
xList Opaque val (TyVarRep ('TyNameRep "a" 0))
xI Opaque val (TyVarRep ('TyNameRep "a" 0))
xB ->
                  case Data
d of
                    Constr {} -> Opaque val (TyVarRep ('TyNameRep "a" 0))
xConstr
                    Map    {} -> Opaque val (TyVarRep ('TyNameRep "a" 0))
xMap
                    List   {} -> Opaque val (TyVarRep ('TyNameRep "a" 0))
xList
                    I      {} -> Opaque val (TyVarRep ('TyNameRep "a" 0))
xI
                    B      {} -> Opaque val (TyVarRep ('TyNameRep "a" 0))
xB)
            (CostingFun ModelSixArguments
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
runCostingFunSixArguments (CostingFun ModelSixArguments
 -> ExMemory
 -> ExMemory
 -> ExMemory
 -> ExMemory
 -> ExMemory
 -> ExMemory
 -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelSixArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelSixArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelSixArguments
paramChooseData)
    toBuiltinMeaning DefaultFun
ConstrData =
        (Integer -> [Data] -> Data)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer, [Data]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Integer -> [Data] -> Data
Constr
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramConstrData)
    toBuiltinMeaning DefaultFun
MapData =
        ([(Data, Data)] -> Data)
-> (BuiltinCostModel -> ToCostingType (Length '[[(Data, Data)]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            [(Data, Data)] -> Data
Map
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramMapData)
    toBuiltinMeaning DefaultFun
ListData =
        ([Data] -> Data)
-> (BuiltinCostModel -> ToCostingType (Length '[[Data]]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            [Data] -> Data
List
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramListData)
    toBuiltinMeaning DefaultFun
IData =
        (Integer -> Data)
-> (BuiltinCostModel -> ToCostingType (Length '[Integer]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Integer -> Data
I
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramIData)
    toBuiltinMeaning DefaultFun
BData =
        (ByteString -> Data)
-> (BuiltinCostModel -> ToCostingType (Length '[ByteString]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ByteString -> Data
B
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramBData)
    toBuiltinMeaning DefaultFun
UnConstrData =
        (Data -> EvaluationResult (Integer, [Data]))
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\case
                Constr Integer
i [Data]
ds -> (Integer, [Data]) -> EvaluationResult (Integer, [Data])
forall a. a -> EvaluationResult a
EvaluationSuccess (Integer
i, [Data]
ds)
                Data
_           -> EvaluationResult (Integer, [Data])
forall a. EvaluationResult a
EvaluationFailure)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramUnConstrData)
    toBuiltinMeaning DefaultFun
UnMapData =
        (Data -> EvaluationResult [(Data, Data)])
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\case
                Map [(Data, Data)]
es -> [(Data, Data)] -> EvaluationResult [(Data, Data)]
forall a. a -> EvaluationResult a
EvaluationSuccess [(Data, Data)]
es
                Data
_      -> EvaluationResult [(Data, Data)]
forall a. EvaluationResult a
EvaluationFailure)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramUnMapData)
    toBuiltinMeaning DefaultFun
UnListData =
        (Data -> EvaluationResult [Data])
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\case
                List [Data]
ds -> [Data] -> EvaluationResult [Data]
forall a. a -> EvaluationResult a
EvaluationSuccess [Data]
ds
                Data
_       -> EvaluationResult [Data]
forall a. EvaluationResult a
EvaluationFailure)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramUnListData)
    toBuiltinMeaning DefaultFun
UnIData =
        (Data -> EvaluationResult Integer)
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\case
                I Integer
i -> Integer -> EvaluationResult Integer
forall a. a -> EvaluationResult a
EvaluationSuccess Integer
i
                Data
_   -> EvaluationResult Integer
forall a. EvaluationResult a
EvaluationFailure)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramUnIData)
    toBuiltinMeaning DefaultFun
UnBData =
        (Data -> EvaluationResult ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\case
                B ByteString
b -> ByteString -> EvaluationResult ByteString
forall a. a -> EvaluationResult a
EvaluationSuccess ByteString
b
                Data
_   -> EvaluationResult ByteString
forall a. EvaluationResult a
EvaluationFailure)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramUnBData)
    toBuiltinMeaning DefaultFun
EqualsData =
        (Data -> Data -> Bool)
-> (BuiltinCostModel -> ToCostingType (Length '[Data, Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Eq Data => Data -> Data -> Bool
forall a. Eq a => a -> a -> Bool
(==) @Data)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramEqualsData)
    toBuiltinMeaning DefaultFun
SerialiseData =
        (Data -> ByteString)
-> (BuiltinCostModel -> ToCostingType (Length '[Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (ByteString -> ByteString
BS.toStrict (ByteString -> ByteString)
-> (Data -> ByteString) -> Data -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Serialise Data => Data -> ByteString
forall a. Serialise a => a -> ByteString
serialise @Data)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramSerialiseData)
    -- Misc constructors
    toBuiltinMeaning DefaultFun
MkPairData =
        (Data -> Data -> (Data, Data))
-> (BuiltinCostModel -> ToCostingType (Length '[Data, Data]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ((,) @Data @Data)
            (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget
runCostingFunTwoArguments (CostingFun ModelTwoArguments -> ExMemory -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelTwoArguments)
-> BuiltinCostModel
-> ExMemory
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelTwoArguments
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelTwoArguments
paramMkPairData)
    toBuiltinMeaning DefaultFun
MkNilData =
        -- Nullary builtins don't work, so we need a unit argument
        (() -> [Data])
-> (BuiltinCostModel -> ToCostingType (Length '[()]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\() -> [] @Data)
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramMkNilData)
    toBuiltinMeaning DefaultFun
MkNilPairData =
        -- Nullary builtins don't work, so we need a unit argument
        (() -> [(Data, Data)])
-> (BuiltinCostModel -> ToCostingType (Length '[()]))
-> BuiltinMeaning val BuiltinCostModel
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a
-> (cost -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\() -> [] @(Data,Data))
            (CostingFun ModelOneArgument -> ExMemory -> ExBudget
runCostingFunOneArgument (CostingFun ModelOneArgument -> ExMemory -> ExBudget)
-> (BuiltinCostModel -> CostingFun ModelOneArgument)
-> BuiltinCostModel
-> ExMemory
-> ExBudget
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinCostModel -> CostingFun ModelOneArgument
forall (f :: * -> *). BuiltinCostModelBase f -> f ModelOneArgument
paramMkNilPairData)
    -- See Note [Inlining meanings of builtins].
    {-# INLINE toBuiltinMeaning #-}

-- It's set deliberately to give us "extra room" in the binary format to add things without running
-- out of space for tags (expanding the space would change the binary format for people who're
-- implementing it manually). So we have to set it manually.
-- | Using 7 bits to encode builtin tags.
builtinTagWidth :: NumBits
builtinTagWidth :: Int
builtinTagWidth = Int
7

encodeBuiltin :: Word8 -> Flat.Encoding
encodeBuiltin :: Word8 -> Encoding
encodeBuiltin = Int -> Word8 -> Encoding
eBits Int
builtinTagWidth

decodeBuiltin :: Get Word8
decodeBuiltin :: Get Word8
decodeBuiltin = Int -> Get Word8
dBEBits8 Int
builtinTagWidth

-- See Note [Stable encoding of PLC]
instance Flat DefaultFun where
    encode :: DefaultFun -> Encoding
encode = Word8 -> Encoding
encodeBuiltin (Word8 -> Encoding)
-> (DefaultFun -> Word8) -> DefaultFun -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
              DefaultFun
AddInteger                      -> Word8
0
              DefaultFun
SubtractInteger                 -> Word8
1
              DefaultFun
MultiplyInteger                 -> Word8
2
              DefaultFun
DivideInteger                   -> Word8
3
              DefaultFun
QuotientInteger                 -> Word8
4
              DefaultFun
RemainderInteger                -> Word8
5
              DefaultFun
ModInteger                      -> Word8
6
              DefaultFun
EqualsInteger                   -> Word8
7
              DefaultFun
LessThanInteger                 -> Word8
8
              DefaultFun
LessThanEqualsInteger           -> Word8
9

              DefaultFun
AppendByteString                -> Word8
10
              DefaultFun
ConsByteString                  -> Word8
11
              DefaultFun
SliceByteString                 -> Word8
12
              DefaultFun
LengthOfByteString              -> Word8
13
              DefaultFun
IndexByteString                 -> Word8
14
              DefaultFun
EqualsByteString                -> Word8
15
              DefaultFun
LessThanByteString              -> Word8
16
              DefaultFun
LessThanEqualsByteString        -> Word8
17

              DefaultFun
Sha2_256                        -> Word8
18
              DefaultFun
Sha3_256                        -> Word8
19
              DefaultFun
Blake2b_256                     -> Word8
20
              DefaultFun
VerifyEd25519Signature          -> Word8
21
              DefaultFun
VerifyEcdsaSecp256k1Signature   -> Word8
52
              DefaultFun
VerifySchnorrSecp256k1Signature -> Word8
53

              DefaultFun
AppendString                    -> Word8
22
              DefaultFun
EqualsString                    -> Word8
23
              DefaultFun
EncodeUtf8                      -> Word8
24
              DefaultFun
DecodeUtf8                      -> Word8
25

              DefaultFun
IfThenElse                      -> Word8
26

              DefaultFun
ChooseUnit                      -> Word8
27

              DefaultFun
Trace                           -> Word8
28

              DefaultFun
FstPair                         -> Word8
29
              DefaultFun
SndPair                         -> Word8
30

              DefaultFun
ChooseList                      -> Word8
31
              DefaultFun
MkCons                          -> Word8
32
              DefaultFun
HeadList                        -> Word8
33
              DefaultFun
TailList                        -> Word8
34
              DefaultFun
NullList                        -> Word8
35

              DefaultFun
ChooseData                      -> Word8
36
              DefaultFun
ConstrData                      -> Word8
37
              DefaultFun
MapData                         -> Word8
38
              DefaultFun
ListData                        -> Word8
39
              DefaultFun
IData                           -> Word8
40
              DefaultFun
BData                           -> Word8
41
              DefaultFun
UnConstrData                    -> Word8
42
              DefaultFun
UnMapData                       -> Word8
43
              DefaultFun
UnListData                      -> Word8
44
              DefaultFun
UnIData                         -> Word8
45
              DefaultFun
UnBData                         -> Word8
46
              DefaultFun
EqualsData                      -> Word8
47
              DefaultFun
MkPairData                      -> Word8
48
              DefaultFun
MkNilData                       -> Word8
49
              DefaultFun
MkNilPairData                   -> Word8
50
              DefaultFun
SerialiseData                   -> Word8
51

    decode :: Get DefaultFun
decode = Word8 -> Get DefaultFun
forall a (f :: * -> *).
(Eq a, Num a, MonadFail f, Show a) =>
a -> f DefaultFun
go (Word8 -> Get DefaultFun) -> Get Word8 -> Get DefaultFun
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Get Word8
decodeBuiltin
        where go :: a -> f DefaultFun
go a
0  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
AddInteger
              go a
1  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
SubtractInteger
              go a
2  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MultiplyInteger
              go a
3  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
DivideInteger
              go a
4  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
QuotientInteger
              go a
5  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
RemainderInteger
              go a
6  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ModInteger
              go a
7  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
EqualsInteger
              go a
8  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
LessThanInteger
              go a
9  = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
LessThanEqualsInteger
              go a
10 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
AppendByteString
              go a
11 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ConsByteString
              go a
12 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
SliceByteString
              go a
13 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
LengthOfByteString
              go a
14 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
IndexByteString
              go a
15 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
EqualsByteString
              go a
16 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
LessThanByteString
              go a
17 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
LessThanEqualsByteString
              go a
18 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
Sha2_256
              go a
19 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
Sha3_256
              go a
20 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
Blake2b_256
              go a
21 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
VerifyEd25519Signature
              go a
22 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
AppendString
              go a
23 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
EqualsString
              go a
24 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
EncodeUtf8
              go a
25 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
DecodeUtf8
              go a
26 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
IfThenElse
              go a
27 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ChooseUnit
              go a
28 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
Trace
              go a
29 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
FstPair
              go a
30 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
SndPair
              go a
31 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ChooseList
              go a
32 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MkCons
              go a
33 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
HeadList
              go a
34 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
TailList
              go a
35 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
NullList
              go a
36 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ChooseData
              go a
37 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ConstrData
              go a
38 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MapData
              go a
39 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
ListData
              go a
40 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
IData
              go a
41 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
BData
              go a
42 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
UnConstrData
              go a
43 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
UnMapData
              go a
44 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
UnListData
              go a
45 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
UnIData
              go a
46 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
UnBData
              go a
47 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
EqualsData
              go a
48 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MkPairData
              go a
49 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MkNilData
              go a
50 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
MkNilPairData
              go a
51 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
SerialiseData
              go a
52 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
VerifyEcdsaSecp256k1Signature
              go a
53 = DefaultFun -> f DefaultFun
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultFun
VerifySchnorrSecp256k1Signature
              go a
t  = String -> f DefaultFun
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> f DefaultFun) -> String -> f DefaultFun
forall a b. (a -> b) -> a -> b
$ String
"Failed to decode builtin tag, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t

    size :: DefaultFun -> Int -> Int
size DefaultFun
_ Int
n = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
builtinTagWidth