{-# OPTIONS_GHC -fno-warn-orphans               #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}

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

module PlutusCore.Examples.Builtins where

import PlutusCore
import PlutusCore.Builtin
import PlutusCore.Data
import PlutusCore.Evaluation.Machine.BuiltinCostModel
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Result (evaluationFailure)
import PlutusCore.Pretty

import PlutusCore.StdLib.Data.ScottList qualified as Plc

import Control.Concurrent.MVar
import Control.Exception
import Control.Monad
import Data.Default.Class
import Data.Either
import Data.Kind qualified as GHC (Type)
import Data.Proxy
import Data.Some.GADT qualified as GADT
import Data.Tuple
import Data.Void
import GHC.Generics
import GHC.Ix
import GHC.TypeLits
import Prettyprinter
import System.IO.Unsafe (unsafeInterleaveIO, unsafePerformIO)
import System.Mem (performMinorGC)
import System.Mem.Weak (addFinalizer)

instance (Bounded a, Bounded b) => Bounded (Either a b) where
    minBound :: Either a b
minBound = a -> Either a b
forall a b. a -> Either a b
Left  a
forall a. Bounded a => a
minBound
    maxBound :: Either a b
maxBound = b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Bounded a => a
maxBound

size :: forall a. (Bounded a, Enum a) => Int
size :: forall a. (Bounded a, Enum a) => Int
size = a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
maxBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
- a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
minBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

-- >>> map fromEnum [Left False .. Right GT]
-- [0,1,2,3,4]
-- >>> map toEnum [0 .. 4] :: [Either Bool Ordering]
-- [Left False,Left True,Right LT,Right EQ,Right GT]
instance (Eq a, Eq b, Bounded a, Bounded b, Enum a, Enum b) => Enum (Either a b) where
    succ :: Either a b -> Either a b
succ (Left a
x)
        | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
maxBound = b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Bounded a => a
minBound
        | Bool
otherwise     = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
succ a
x
    succ (Right b
y)
        | b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. Bounded a => a
maxBound = [Char] -> Either a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds"
        | Bool
otherwise     = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> b
forall a. Enum a => a -> a
succ b
y

    pred :: Either a b -> Either a b
pred (Left a
x)
        | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
minBound = [Char] -> Either a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds"
        | Bool
otherwise     = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
pred a
x
    pred (Right b
y)
        | b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. Bounded a => a
minBound = a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Bounded a => a
maxBound
        | Bool
otherwise     = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> b
forall a. Enum a => a -> a
pred b
y

    toEnum :: Int -> Either a b
toEnum Int
i
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
s     = a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> a
forall a. Enum a => Int -> a
toEnum Int
i
        | Bool
otherwise = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> b
forall a. Enum a => Int -> a
toEnum (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
s)
        where s :: Int
s = forall a. (Bounded a, Enum a) => Int
size @a

    fromEnum :: Either a b -> Int
fromEnum (Left  a
x) = a -> Int
forall a. Enum a => a -> Int
fromEnum a
x
    fromEnum (Right b
y) = forall a. (Bounded a, Enum a) => Int
size @a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ b -> Int
forall a. Enum a => a -> Int
fromEnum b
y

-- >>> import GHC.Ix
-- >>> map (unsafeIndex (Left False, Right GT)) [Left False .. Right GT]
-- [0,1,2,3,4]
-- >>> let bounds = (Left (False, EQ), Right (True, GT)) in map (unsafeIndex bounds) $ range bounds
-- [0,1,2,3,4,5,6,7,8,9]
instance (Bounded a, Bounded b, Ix a, Ix b) => Ix (Either a b) where
    range :: (Either a b, Either a b) -> [Either a b]
range (Right b
_, Left  a
_) = []
    range (Right b
x, Right b
y) = (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right ((b, b) -> [b]
forall a. Ix a => (a, a) -> [a]
range (b
x, b
y))
    range (Left  a
x, Right b
y) = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left ((a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range (a
x, a
forall a. Bounded a => a
maxBound)) [Either a b] -> [Either a b] -> [Either a b]
forall a. [a] -> [a] -> [a]
++ (b -> Either a b) -> [b] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map b -> Either a b
forall a b. b -> Either a b
Right ((b, b) -> [b]
forall a. Ix a => (a, a) -> [a]
range (b
forall a. Bounded a => a
minBound, b
y))
    range (Left  a
x, Left  a
y) = (a -> Either a b) -> [a] -> [Either a b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either a b
forall a b. a -> Either a b
Left ((a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range (a
x, a
y))

    unsafeIndex :: (Either a b, Either a b) -> Either a b -> Int
unsafeIndex (Right b
_, Either a b
_) (Left  a
_) = [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds"
    unsafeIndex (Left  a
x, Either a b
n) (Left  a
i) = (a, a) -> a -> Int
forall a. Ix a => (a, a) -> a -> Int
unsafeIndex (a
x, a -> Either a b -> a
forall a b. a -> Either a b -> a
fromLeft a
forall a. Bounded a => a
maxBound Either a b
n) a
i
    unsafeIndex (Right b
x, Either a b
n) (Right b
i) = (b, b) -> b -> Int
forall a. Ix a => (a, a) -> a -> Int
unsafeIndex (b
x, b -> Either a b -> b
forall b a. b -> Either a b -> b
fromRight ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds") Either a b
n) b
i
    unsafeIndex (Left  a
x, Either a b
n) (Right b
i) =
        (a, a) -> a -> Int
forall a. Ix a => (a, a) -> a -> Int
unsafeIndex (a
x, a
forall a. Bounded a => a
maxBound) a
forall a. Bounded a => a
maxBound Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+
            (b, b) -> b -> Int
forall a. Ix a => (a, a) -> a -> Int
unsafeIndex (b
forall a. Bounded a => a
minBound, b -> Either a b -> b
forall b a. b -> Either a b -> b
fromRight ([Char] -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds") Either a b
n) b
i

    inRange :: (Either a b, Either a b) -> Either a b -> Bool
inRange (Either a b
m, Either a b
n) Either a b
i = Either a b
m Either a b -> Either a b -> Bool
forall a. Ord a => a -> a -> Bool
<= Either a b
i Bool -> Bool -> Bool
&& Either a b
i Either a b -> Either a b -> Bool
forall a. Ord a => a -> a -> Bool
<= Either a b
n

-- See Note [Representable built-in functions over polymorphic built-in types]
data ExtensionFun
    = Factorial
    | ForallFortyTwo  -- A builtin for @42 :: forall a. Integer@.
    | SumInteger
    | Const
    | Id
    | IdAssumeBool
    | IdAssumeCheckBool
    | IdSomeConstantBool
    | IdIntegerAsBool
    | IdFInteger
    | IdList
    | IdRank2
    | ScottToMetaUnit
    -- The next four are for testing that costing always precedes actual evaluation.
    | FailingSucc
    | ExpensiveSucc
    | FailingPlus
    | ExpensivePlus
    | IsConstant
    | UnsafeCoerce
    | UnsafeCoerceEl
    | Undefined
    | Absurd
    | ErrorPrime  -- Like 'Error', but a builtin. What do we even need 'Error' for at this point?
                  -- Who knows what machinery a tick could break, hence the @Prime@ part.
    | Comma
    | BiconstPair  -- A safe version of 'Comma' as discussed in Note [Representable built-in
                   -- functions over polymorphic built-in types].
    | Swap  -- For checking that permuting type arguments of a polymorphic built-in works correctly.
    | SwapEls  -- For checking that nesting polymorphic built-in types and instantiating them with
               -- a mix of monomorphic types and type variables works correctly.
    | ExtensionVersion -- Reflect the version of the Extension
    | TrackCosts  -- For checking that each cost is released and can be picked up by GC once it's
                  -- accounted for in the evaluator.
    | IntNoIntegerNoWord  -- For testing the signature dump test.
    deriving stock (Int -> ExtensionFun -> ShowS
[ExtensionFun] -> ShowS
ExtensionFun -> [Char]
(Int -> ExtensionFun -> ShowS)
-> (ExtensionFun -> [Char])
-> ([ExtensionFun] -> ShowS)
-> Show ExtensionFun
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExtensionFun -> ShowS
showsPrec :: Int -> ExtensionFun -> ShowS
$cshow :: ExtensionFun -> [Char]
show :: ExtensionFun -> [Char]
$cshowList :: [ExtensionFun] -> ShowS
showList :: [ExtensionFun] -> ShowS
Show, ExtensionFun -> ExtensionFun -> Bool
(ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool) -> Eq ExtensionFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExtensionFun -> ExtensionFun -> Bool
== :: ExtensionFun -> ExtensionFun -> Bool
$c/= :: ExtensionFun -> ExtensionFun -> Bool
/= :: ExtensionFun -> ExtensionFun -> Bool
Eq, Eq ExtensionFun
Eq ExtensionFun =>
(ExtensionFun -> ExtensionFun -> Ordering)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> ExtensionFun)
-> (ExtensionFun -> ExtensionFun -> ExtensionFun)
-> Ord ExtensionFun
ExtensionFun -> ExtensionFun -> Bool
ExtensionFun -> ExtensionFun -> Ordering
ExtensionFun -> ExtensionFun -> ExtensionFun
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
$ccompare :: ExtensionFun -> ExtensionFun -> Ordering
compare :: ExtensionFun -> ExtensionFun -> Ordering
$c< :: ExtensionFun -> ExtensionFun -> Bool
< :: ExtensionFun -> ExtensionFun -> Bool
$c<= :: ExtensionFun -> ExtensionFun -> Bool
<= :: ExtensionFun -> ExtensionFun -> Bool
$c> :: ExtensionFun -> ExtensionFun -> Bool
> :: ExtensionFun -> ExtensionFun -> Bool
$c>= :: ExtensionFun -> ExtensionFun -> Bool
>= :: ExtensionFun -> ExtensionFun -> Bool
$cmax :: ExtensionFun -> ExtensionFun -> ExtensionFun
max :: ExtensionFun -> ExtensionFun -> ExtensionFun
$cmin :: ExtensionFun -> ExtensionFun -> ExtensionFun
min :: ExtensionFun -> ExtensionFun -> ExtensionFun
Ord, Int -> ExtensionFun
ExtensionFun -> Int
ExtensionFun -> [ExtensionFun]
ExtensionFun -> ExtensionFun
ExtensionFun -> ExtensionFun -> [ExtensionFun]
ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
(ExtensionFun -> ExtensionFun)
-> (ExtensionFun -> ExtensionFun)
-> (Int -> ExtensionFun)
-> (ExtensionFun -> Int)
-> (ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> Enum ExtensionFun
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ExtensionFun -> ExtensionFun
succ :: ExtensionFun -> ExtensionFun
$cpred :: ExtensionFun -> ExtensionFun
pred :: ExtensionFun -> ExtensionFun
$ctoEnum :: Int -> ExtensionFun
toEnum :: Int -> ExtensionFun
$cfromEnum :: ExtensionFun -> Int
fromEnum :: ExtensionFun -> Int
$cenumFrom :: ExtensionFun -> [ExtensionFun]
enumFrom :: ExtensionFun -> [ExtensionFun]
$cenumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
Enum, ExtensionFun
ExtensionFun -> ExtensionFun -> Bounded ExtensionFun
forall a. a -> a -> Bounded a
$cminBound :: ExtensionFun
minBound :: ExtensionFun
$cmaxBound :: ExtensionFun
maxBound :: ExtensionFun
Bounded, Ord ExtensionFun
Ord ExtensionFun =>
((ExtensionFun, ExtensionFun) -> [ExtensionFun])
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Int)
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Int)
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool)
-> ((ExtensionFun, ExtensionFun) -> Int)
-> ((ExtensionFun, ExtensionFun) -> Int)
-> Ix ExtensionFun
(ExtensionFun, ExtensionFun) -> Int
(ExtensionFun, ExtensionFun) -> [ExtensionFun]
(ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
(ExtensionFun, ExtensionFun) -> ExtensionFun -> 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
$crange :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
range :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
$cindex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
index :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cunsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
unsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cinRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
inRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
$crangeSize :: (ExtensionFun, ExtensionFun) -> Int
rangeSize :: (ExtensionFun, ExtensionFun) -> Int
$cunsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
unsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
Ix, (forall x. ExtensionFun -> Rep ExtensionFun x)
-> (forall x. Rep ExtensionFun x -> ExtensionFun)
-> Generic ExtensionFun
forall x. Rep ExtensionFun x -> ExtensionFun
forall x. ExtensionFun -> Rep ExtensionFun x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExtensionFun -> Rep ExtensionFun x
from :: forall x. ExtensionFun -> Rep ExtensionFun x
$cto :: forall x. Rep ExtensionFun x -> ExtensionFun
to :: forall x. Rep ExtensionFun x -> ExtensionFun
Generic)
    deriving anyclass (Eq ExtensionFun
Eq ExtensionFun =>
(Int -> ExtensionFun -> Int)
-> (ExtensionFun -> Int) -> Hashable ExtensionFun
Int -> ExtensionFun -> Int
ExtensionFun -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> ExtensionFun -> Int
hashWithSalt :: Int -> ExtensionFun -> Int
$chash :: ExtensionFun -> Int
hash :: ExtensionFun -> Int
Hashable)

instance Pretty ExtensionFun where pretty :: forall ann. ExtensionFun -> Doc ann
pretty = ExtensionFun -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2
         , Default (BuiltinSemanticsVariant fun1), Default (BuiltinSemanticsVariant fun2)
         ) => ToBuiltinMeaning uni (Either fun1 fun2) where

    type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)

    data BuiltinSemanticsVariant (Either fun1 fun2) =
        PairV (BuiltinSemanticsVariant fun1) (BuiltinSemanticsVariant fun2)
    toBuiltinMeaning :: forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant (Either fun1 fun2)
-> Either fun1 fun2
-> BuiltinMeaning val (CostingPart uni (Either fun1 fun2))
toBuiltinMeaning (PairV BuiltinSemanticsVariant fun1
semvarL BuiltinSemanticsVariant fun2
_) (Left  fun1
fun) = case BuiltinSemanticsVariant fun1
-> fun1 -> BuiltinMeaning val (CostingPart (UniOf val) fun1)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun1
-> fun1 -> BuiltinMeaning val (CostingPart (UniOf val) fun1)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun1
semvarL fun1
fun of
        BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF CostingPart (UniOf val) fun1 -> BuiltinRuntime val
denot ->
            TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> BuiltinRuntime val)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (CostingPart uni fun1 -> BuiltinRuntime val
CostingPart (UniOf val) fun1 -> BuiltinRuntime val
denot (CostingPart uni fun1 -> BuiltinRuntime val)
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> CostingPart uni fun1)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun1
forall a b. (a, b) -> a
fst)
    toBuiltinMeaning (PairV BuiltinSemanticsVariant fun1
_ BuiltinSemanticsVariant fun2
semvarR) (Right fun2
fun) = case BuiltinSemanticsVariant fun2
-> fun2 -> BuiltinMeaning val (CostingPart (UniOf val) fun2)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun2
-> fun2 -> BuiltinMeaning val (CostingPart (UniOf val) fun2)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun2
semvarR fun2
fun of
        BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF CostingPart (UniOf val) fun2 -> BuiltinRuntime val
denot ->
            TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> BuiltinRuntime val)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (CostingPart uni fun2 -> BuiltinRuntime val
CostingPart (UniOf val) fun2 -> BuiltinRuntime val
denot (CostingPart uni fun2 -> BuiltinRuntime val)
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> CostingPart uni fun2)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun2
forall a b. (a, b) -> b
snd)

instance (Default (BuiltinSemanticsVariant fun1), Default (BuiltinSemanticsVariant fun2))
         => Default (BuiltinSemanticsVariant (Either fun1 fun2)) where
    def :: BuiltinSemanticsVariant (Either fun1 fun2)
def = BuiltinSemanticsVariant fun1
-> BuiltinSemanticsVariant fun2
-> BuiltinSemanticsVariant (Either fun1 fun2)
forall fun1 fun2.
BuiltinSemanticsVariant fun1
-> BuiltinSemanticsVariant fun2
-> BuiltinSemanticsVariant (Either fun1 fun2)
PairV BuiltinSemanticsVariant fun1
forall a. Default a => a
def BuiltinSemanticsVariant fun2
forall a. Default a => a
def

-- | Normally @forall@ in the type of a Haskell function gets detected and instantiated
-- automatically, however there's no way of doing that for a @forall@ that binds a never referenced
-- type variable. Which is OK, because that would be a pretty weird builtin, however it's definable
-- and for the purpose of testing we do introduce such a builtin, hence this definition allowing us
-- to create an @all@ that binds a never referenced type variable in Plutus while still using
-- 'makeBuiltinMeaning'.
newtype MetaForall name a = MetaForall a
instance
        ( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
        , KnownKind kind, KnownTypeAst tyname uni a
        ) => KnownTypeAst tyname uni (MetaForall name a) where
    type IsBuiltin _ (MetaForall name a) = 'False
    type ToHoles _ (MetaForall name a) = '[TypeHole a]
    type ToBinds uni acc (MetaForall name a) = ToBinds uni (Insert ('GADT.Some name) acc) a
    typeAst :: Type tyname uni ()
typeAst = Proxy a -> Type tyname uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
instance MakeKnownIn DefaultUni term a => MakeKnownIn DefaultUni term (MetaForall name a) where
    makeKnown :: MetaForall name a -> BuiltinResult term
makeKnown (MetaForall a
x) = a -> BuiltinResult term
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult val
makeKnown a
x
-- 'ReadKnownIn' doesn't make sense for 'MetaForall'.

data PlcListRep (a :: GHC.Type)
instance (tyname ~ TyName, KnownTypeAst tyname uni a) =>
        KnownTypeAst tyname uni (PlcListRep a) where
    type IsBuiltin _ (PlcListRep a) = 'False
    type ToHoles _ (PlcListRep a) = '[RepHole a]
    type ToBinds uni acc (PlcListRep a) = ToBinds uni acc a
    typeAst :: Type tyname uni ()
typeAst = ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type tyname uni ()
Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.listTy (Type tyname uni () -> Type tyname uni ())
-> (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Type tyname uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a

instance tyname ~ TyName => KnownTypeAst tyname DefaultUni Void where
    type IsBuiltin _ _ = 'False
    type ToHoles _ _ = '[]
    type ToBinds _ acc _ = acc
    typeAst :: Type tyname DefaultUni ()
typeAst = Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ()
forall a. Quote a -> a
runQuote (Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ())
-> Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ()
forall a b. (a -> b) -> a -> b
$ do
        TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
        Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ()))
-> Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ())
forall a b. (a -> b) -> a -> b
$ ()
-> tyname
-> Kind ()
-> Type tyname DefaultUni ()
-> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () tyname
TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type tyname DefaultUni () -> Type tyname DefaultUni ())
-> Type tyname DefaultUni () -> Type tyname DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> tyname -> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () tyname
TyName
a
instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where
    makeKnown :: Void -> BuiltinResult term
makeKnown = Void -> BuiltinResult term
forall a. Void -> a
absurd
instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
    readKnown :: term -> ReadKnownM Void
readKnown term
_ = AReview BuiltinError UnliftingError
-> UnliftingError -> ReadKnownM Void
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview BuiltinError UnliftingError
forall err. AsBuiltinError err => Prism' err UnliftingError
Prism' BuiltinError UnliftingError
_StructuralUnliftingError UnliftingError
"Can't unlift to 'Void'"

data BuiltinErrorCall = BuiltinErrorCall
    deriving stock (Int -> BuiltinErrorCall -> ShowS
[BuiltinErrorCall] -> ShowS
BuiltinErrorCall -> [Char]
(Int -> BuiltinErrorCall -> ShowS)
-> (BuiltinErrorCall -> [Char])
-> ([BuiltinErrorCall] -> ShowS)
-> Show BuiltinErrorCall
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinErrorCall -> ShowS
showsPrec :: Int -> BuiltinErrorCall -> ShowS
$cshow :: BuiltinErrorCall -> [Char]
show :: BuiltinErrorCall -> [Char]
$cshowList :: [BuiltinErrorCall] -> ShowS
showList :: [BuiltinErrorCall] -> ShowS
Show, BuiltinErrorCall -> BuiltinErrorCall -> Bool
(BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> (BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> Eq BuiltinErrorCall
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
$c/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
Eq)
    deriving anyclass (Show BuiltinErrorCall
Typeable BuiltinErrorCall
(Typeable BuiltinErrorCall, Show BuiltinErrorCall) =>
(BuiltinErrorCall -> SomeException)
-> (SomeException -> Maybe BuiltinErrorCall)
-> (BuiltinErrorCall -> [Char])
-> Exception BuiltinErrorCall
SomeException -> Maybe BuiltinErrorCall
BuiltinErrorCall -> [Char]
BuiltinErrorCall -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> [Char]) -> Exception e
$ctoException :: BuiltinErrorCall -> SomeException
toException :: BuiltinErrorCall -> SomeException
$cfromException :: SomeException -> Maybe BuiltinErrorCall
fromException :: SomeException -> Maybe BuiltinErrorCall
$cdisplayException :: BuiltinErrorCall -> [Char]
displayException :: BuiltinErrorCall -> [Char]
Exception)

-- | For the most part we don't care about costing functions of example builtins, hence this class
-- for being explicit about not caring.
class Whatever a where
    -- | The costing function of a builtin whose costing function doesn't matter.
    whatever :: a

instance Whatever b => Whatever (a -> b) where
    whatever :: a -> b
whatever a
_ = b
forall a. Whatever a => a
whatever

instance Whatever ExBudgetStream where
    whatever :: ExBudgetStream
whatever = ExBudget -> ExBudgetStream
ExBudgetLast ExBudget
forall a. Monoid a => a
mempty

-- See Note [Representable built-in functions over polymorphic built-in types].
-- We have lists in the universe and so we can define a function like @\x -> [x, x]@ that duplicates
-- the constant that it receives. Should memory consumption of that function be linear in the number
-- of duplicates that the function creates? I think, no:
--
-- 1. later we can call @head@ over the resulting list thus not duplicating anything in the end
-- 2. any monomorphic builtin touching a duplicated constant will automatically
--    add it to the current budget. And if we never touch the duplicate again and just keep it
--    around, then it won't ever increase memory consumption. And any other node will be taken into
--    account automatically as well: just think that having @\x -> f x x@ as a PLC term is supposed
--    to be handled correctly by design
instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
    type CostingPart uni ExtensionFun = ()

    data BuiltinSemanticsVariant ExtensionFun =
              ExtensionFunSemanticsVariant0
            | ExtensionFunSemanticsVariant1
            | ExtensionFunSemanticsVariant2
            | ExtensionFunSemanticsVariant3
            | ExtensionFunSemanticsVariant4
        deriving stock (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
(BuiltinSemanticsVariant ExtensionFun
 -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> Eq (BuiltinSemanticsVariant ExtensionFun)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
== :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c/= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
/= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
Eq, Eq (BuiltinSemanticsVariant ExtensionFun)
Eq (BuiltinSemanticsVariant ExtensionFun) =>
(BuiltinSemanticsVariant ExtensionFun
 -> BuiltinSemanticsVariant ExtensionFun -> Ordering)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun)
-> Ord (BuiltinSemanticsVariant ExtensionFun)
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
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
$ccompare :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
compare :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
$c< :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
< :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c<= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
<= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c> :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
> :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c>= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
>= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$cmax :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
max :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$cmin :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
min :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
Ord, Int -> BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun -> Int
BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
(BuiltinSemanticsVariant ExtensionFun
 -> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun)
-> (Int -> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun -> Int)
-> (BuiltinSemanticsVariant ExtensionFun
    -> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> BuiltinSemanticsVariant ExtensionFun
    -> [BuiltinSemanticsVariant ExtensionFun])
-> Enum (BuiltinSemanticsVariant ExtensionFun)
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
succ :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$cpred :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
pred :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$ctoEnum :: Int -> BuiltinSemanticsVariant ExtensionFun
toEnum :: Int -> BuiltinSemanticsVariant ExtensionFun
$cfromEnum :: BuiltinSemanticsVariant ExtensionFun -> Int
fromEnum :: BuiltinSemanticsVariant ExtensionFun -> Int
$cenumFrom :: BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFrom :: BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromThen :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromThen :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromThenTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromThenTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
Enum, BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> Bounded (BuiltinSemanticsVariant ExtensionFun)
forall a. a -> a -> Bounded a
$cminBound :: BuiltinSemanticsVariant ExtensionFun
minBound :: BuiltinSemanticsVariant ExtensionFun
$cmaxBound :: BuiltinSemanticsVariant ExtensionFun
maxBound :: BuiltinSemanticsVariant ExtensionFun
Bounded, Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
[BuiltinSemanticsVariant ExtensionFun] -> ShowS
BuiltinSemanticsVariant ExtensionFun -> [Char]
(Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS)
-> (BuiltinSemanticsVariant ExtensionFun -> [Char])
-> ([BuiltinSemanticsVariant ExtensionFun] -> ShowS)
-> Show (BuiltinSemanticsVariant ExtensionFun)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
showsPrec :: Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
$cshow :: BuiltinSemanticsVariant ExtensionFun -> [Char]
show :: BuiltinSemanticsVariant ExtensionFun -> [Char]
$cshowList :: [BuiltinSemanticsVariant ExtensionFun] -> ShowS
showList :: [BuiltinSemanticsVariant ExtensionFun] -> ShowS
Show)

    toBuiltinMeaning :: forall val. HasMeaningIn uni val
                     => BuiltinSemanticsVariant ExtensionFun
                     -> ExtensionFun
                     -> BuiltinMeaning val ()

    toBuiltinMeaning :: forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant ExtensionFun
-> ExtensionFun -> BuiltinMeaning val ()
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Factorial =
        (Integer -> Integer)
-> (() -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Integer -> Integer)
-> (cost -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (\(Integer
n :: Integer) -> [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Integer
1..Integer
n])
            () -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ForallFortyTwo =
        MetaForall ('TyNameRep "a" 0) Integer
-> (()
    -> FoldArgs
         (GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
MetaForall ('TyNameRep "a" 0) Integer
-> (cost
    -> FoldArgs
         (GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            MetaForall ('TyNameRep "a" 0) Integer
forallFortyTwo
            () -> ExBudgetStream
()
-> FoldArgs
     (GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream
forall a. Whatever a => a
whatever
      where
        forallFortyTwo :: MetaForall ('TyNameRep @GHC.Type "a" 0) Integer
        forallFortyTwo :: MetaForall ('TyNameRep "a" 0) Integer
forallFortyTwo = Integer -> MetaForall ('TyNameRep "a" 0) Integer
forall {k} (name :: k) a. a -> MetaForall name a
MetaForall Integer
42

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
SumInteger =
        ([Integer] -> Integer)
-> (() -> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
([Integer] -> Integer)
-> (cost
    -> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum :: [Integer] -> Integer)
            () -> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream
() -> [Integer] -> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Const =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "b" 1))
             -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "b" 1))
             -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a b. a -> b -> a
const
            ()
-> FoldArgs
     (GetArgs
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
         -> Opaque val (TyVarRep ('TyNameRep "b" 1))
         -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
     ExBudgetStream
()
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> FoldArgs
     (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Id =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. a -> a
Prelude.id
            ()
-> FoldArgs
     (GetArgs
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
         -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
     ExBudgetStream
()
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
-> FoldArgs
     (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdAssumeBool =
        (Opaque val Bool -> Opaque val Bool)
-> (()
    -> FoldArgs
         (GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val Bool -> Opaque val Bool)
-> (cost
    -> FoldArgs
         (GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (Opaque val Bool -> Opaque val Bool
forall a. a -> a
Prelude.id :: Opaque val Bool -> Opaque val Bool)
            ()
-> FoldArgs
     (GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream
() -> Opaque val Bool -> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdAssumeCheckBool =
        (Opaque val Bool -> BuiltinResult Bool)
-> (()
    -> FoldArgs
         (GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val Bool -> BuiltinResult Bool)
-> (cost
    -> FoldArgs
         (GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val Bool -> BuiltinResult Bool
idAssumeCheckBoolPlc
            ()
-> FoldArgs
     (GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream
() -> Opaque val Bool -> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        idAssumeCheckBoolPlc :: Opaque val Bool -> BuiltinResult Bool
        idAssumeCheckBoolPlc :: Opaque val Bool -> BuiltinResult Bool
idAssumeCheckBoolPlc Opaque val Bool
val =
            case Opaque val Bool
-> Either BuiltinError (Some (ValueOf (UniOf (Opaque val Bool))))
forall term.
HasConstant term =>
term -> Either BuiltinError (Some (ValueOf (UniOf term)))
asConstant Opaque val Bool
val of
                Right (Some (ValueOf DefaultUni (Esc a)
DefaultUniBool a
b)) -> Bool -> BuiltinResult Bool
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Bool
b
                Either BuiltinError (Some (ValueOf (UniOf (Opaque val Bool))))
_                                       -> BuiltinResult Bool
forall err. AsEvaluationFailure err => err
evaluationFailure

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdSomeConstantBool =
        (SomeConstant uni Bool -> BuiltinResult Bool)
-> (()
    -> FoldArgs
         (GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni Bool -> BuiltinResult Bool)
-> (cost
    -> FoldArgs
         (GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni Bool -> BuiltinResult Bool
idSomeConstantBoolPlc
            ()
-> FoldArgs
     (GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
     ExBudgetStream
() -> SomeConstant DefaultUni Bool -> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        idSomeConstantBoolPlc :: SomeConstant uni Bool -> BuiltinResult Bool
        idSomeConstantBoolPlc :: SomeConstant uni Bool -> BuiltinResult Bool
idSomeConstantBoolPlc = \case
            SomeConstant (Some (ValueOf uni (Esc a)
DefaultUni (Esc a)
DefaultUniBool a
b)) -> Bool -> BuiltinResult Bool
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Bool
b
            SomeConstant uni Bool
_                                              -> BuiltinResult Bool
forall err. AsEvaluationFailure err => err
evaluationFailure

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdIntegerAsBool =
        (SomeConstant uni Integer
 -> BuiltinResult (SomeConstant uni Integer))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant uni Integer
             -> BuiltinResult (SomeConstant uni Integer)))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni Integer
 -> BuiltinResult (SomeConstant uni Integer))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant uni Integer
             -> BuiltinResult (SomeConstant uni Integer)))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
idIntegerAsBool
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant uni Integer
         -> BuiltinResult (SomeConstant uni Integer)))
     ExBudgetStream
() -> SomeConstant DefaultUni Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        idIntegerAsBool :: SomeConstant uni Integer -> BuiltinResult (SomeConstant uni Integer)
        idIntegerAsBool :: SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
idIntegerAsBool = \case
            con :: SomeConstant uni Integer
con@(SomeConstant (Some (ValueOf uni (Esc a)
DefaultUni (Esc a)
DefaultUniBool a
_))) -> SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeConstant uni Integer
con
            SomeConstant uni Integer
_                                                    -> BuiltinResult (SomeConstant uni Integer)
forall err. AsEvaluationFailure err => err
evaluationFailure

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdFInteger =
        (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
 -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
             -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
 -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
             -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (fi -> fi
forall a. a -> a
forall {fi} {f :: * -> *}.
(fi ~ Opaque val (TyAppRep f Integer)) =>
fi -> fi
Prelude.id :: fi ~ Opaque val (f `TyAppRep` Integer) => fi -> fi)
            ()
-> FoldArgs
     (GetArgs
        (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
         -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
     ExBudgetStream
()
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdList =
        (Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
 -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0))))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
             -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
 -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0))))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
             -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (la -> la
forall a. a -> a
forall {la} {a}. (la ~ Opaque val (PlcListRep a)) => la -> la
Prelude.id :: la ~ Opaque val (PlcListRep a) => la -> la)
            ()
-> FoldArgs
     (GetArgs
        (Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
         -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
     ExBudgetStream
()
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdRank2 =
        (Opaque
   val
   (TyForallRep
      ('TyNameRep "b" 1)
      (TyAppRep
         (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
 -> Opaque
      val
      (TyForallRep
         ('TyNameRep "b" 1)
         (TyAppRep
            (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1)))))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque
               val
               (TyForallRep
                  ('TyNameRep "b" 1)
                  (TyAppRep
                     (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
             -> Opaque
                  val
                  (TyForallRep
                     ('TyNameRep "b" 1)
                     (TyAppRep
                        (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque
   val
   (TyForallRep
      ('TyNameRep "b" 1)
      (TyAppRep
         (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
 -> Opaque
      val
      (TyForallRep
         ('TyNameRep "b" 1)
         (TyAppRep
            (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1)))))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque
               val
               (TyForallRep
                  ('TyNameRep "b" 1)
                  (TyAppRep
                     (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
             -> Opaque
                  val
                  (TyForallRep
                     ('TyNameRep "b" 1)
                     (TyAppRep
                        (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (afa -> afa
forall a. a -> a
forall {afa} {a :: TyNameRep (*)} {f :: TyNameRep (* -> *)}.
(afa
 ~ Opaque
     val (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a)))) =>
afa -> afa
Prelude.id
                :: afa ~ Opaque val (TyForallRep @GHC.Type a (TyVarRep f `TyAppRep` TyVarRep a))
                => afa -> afa)
            ()
-> FoldArgs
     (GetArgs
        (Opaque
           val
           (TyForallRep
              ('TyNameRep "b" 1)
              (TyAppRep
                 (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
         -> Opaque
              val
              (TyForallRep
                 ('TyNameRep "b" 1)
                 (TyAppRep
                    (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
     ExBudgetStream
()
-> Opaque
     val
     (TyForallRep
        ('TyNameRep "b" 1)
        (TyAppRep
           (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ScottToMetaUnit =
        (Opaque
   val
   (TyForallRep
      ('TyNameRep "a" 0)
      (Opaque val (TyVarRep ('TyNameRep "a" 0))
       -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
 -> ())
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque
               val
               (TyForallRep
                  ('TyNameRep "a" 0)
                  (Opaque val (TyVarRep ('TyNameRep "a" 0))
                   -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
             -> ()))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque
   val
   (TyForallRep
      ('TyNameRep "a" 0)
      (Opaque val (TyVarRep ('TyNameRep "a" 0))
       -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
 -> ())
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque
               val
               (TyForallRep
                  ('TyNameRep "a" 0)
                  (Opaque val (TyVarRep ('TyNameRep "a" 0))
                   -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
             -> ()))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            ((\Opaque val (TyForallRep a (oa -> oa))
_ -> ())
                -- @(->)@ switches from the Rep context to the Type one. We could make @(->)@
                -- preserve the current context, but there's no such notion in the current
                -- elaboration machinery and we'd better not complicate it further just for the sake
                -- of tests looking a bit nicer. Instead we simply wrap the 'TyVarRep' with 'Opaque'
                -- (unlike in the case of @IdRank2@ where 'TyAppRep' preserves the Rep context).
                :: oa ~ Opaque val (TyVarRep a)
                => Opaque val (TyForallRep a (oa -> oa)) -> ())
            ()
-> FoldArgs
     (GetArgs
        (Opaque
           val
           (TyForallRep
              ('TyNameRep "a" 0)
              (Opaque val (TyVarRep ('TyNameRep "a" 0))
               -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         -> ()))
     ExBudgetStream
()
-> Opaque
     val
     (TyForallRep
        ('TyNameRep "a" 0)
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
         -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
-> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
FailingSucc =
        forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer)
            (\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            () -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ExpensiveSucc =
        forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer)
            (\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ Integer
_ -> ExBudget -> ExBudgetStream
ExBudgetLast (ExBudget -> ExBudgetStream) -> ExBudget -> ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
FailingPlus =
        forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer -> Integer)
            (\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            ()
-> FoldArgs
     (GetArgs (Integer -> Integer -> Integer)) ExBudgetStream
() -> Integer -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ExpensivePlus =
        forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer -> Integer)
            (\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ Integer
_ Integer
_ -> ExBudget -> ExBudgetStream
ExBudgetLast (ExBudget -> ExBudgetStream) -> ExBudget -> ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IsConstant =
        (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool)
-> (()
    -> FoldArgs
         (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool)
-> (cost
    -> FoldArgs
         (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool
forall a. Opaque val a -> Bool
isConstantPlc
            ()
-> FoldArgs
     (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
     ExBudgetStream
() -> Opaque val (TyVarRep ('TyNameRep "a" 0)) -> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        -- The type signature is just for clarity, it's not required.
        isConstantPlc :: Opaque val a -> Bool
        isConstantPlc :: forall a. Opaque val a -> Bool
isConstantPlc = Either BuiltinError (Some (ValueOf DefaultUni)) -> Bool
forall a b. Either a b -> Bool
isRight (Either BuiltinError (Some (ValueOf DefaultUni)) -> Bool)
-> (Opaque val a
    -> Either BuiltinError (Some (ValueOf DefaultUni)))
-> Opaque val a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Opaque val a
-> Either BuiltinError (Some (ValueOf (UniOf (Opaque val a))))
Opaque val a -> Either BuiltinError (Some (ValueOf DefaultUni))
forall term.
HasConstant term =>
term -> Either BuiltinError (Some (ValueOf (UniOf term)))
asConstant

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
UnsafeCoerce =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (()
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "b" 1))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (cost
    -> FoldArgs
         (GetArgs
            (Opaque val (TyVarRep ('TyNameRep "a" 0))
             -> Opaque val (TyVarRep ('TyNameRep "b" 1))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
forall a b. Opaque val a -> Opaque val b
unsafeCoercePlc
            ()
-> FoldArgs
     (GetArgs
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
         -> Opaque val (TyVarRep ('TyNameRep "b" 1))))
     ExBudgetStream
() -> Opaque val (TyVarRep ('TyNameRep "a" 0)) -> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        -- The type signature is just for clarity, it's not required.
        unsafeCoercePlc :: Opaque val a -> Opaque val b
        unsafeCoercePlc :: forall a b. Opaque val a -> Opaque val b
unsafeCoercePlc = val -> Opaque val b
forall val rep. val -> Opaque val rep
Opaque (val -> Opaque val b)
-> (Opaque val a -> val) -> Opaque val a -> Opaque val b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Opaque val a -> val
forall val rep. Opaque val rep -> val
unOpaque

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
UnsafeCoerceEl =
        (SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
 -> BuiltinResult
      (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)]))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
             -> BuiltinResult
                  (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
 -> BuiltinResult
      (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)]))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
             -> BuiltinResult
                  (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
     (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])
forall a b.
SomeConstant DefaultUni [a]
-> BuiltinResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
         -> BuiltinResult
              (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
     ExBudgetStream
()
-> SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        unsafeCoerceElPlc
            :: SomeConstant DefaultUni [a] -> BuiltinResult (SomeConstant DefaultUni [b])
        unsafeCoerceElPlc :: forall a b.
SomeConstant DefaultUni [a]
-> BuiltinResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc (SomeConstant (Some (ValueOf DefaultUni (Esc a)
uniList a
xs))) = do
            DefaultUniList DefaultUni (Esc a1)
_ <- DefaultUni (Esc a) -> BuiltinResult (DefaultUni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc a)
uniList
            SomeConstant DefaultUni [b]
-> BuiltinResult (SomeConstant DefaultUni [b])
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant DefaultUni [b]
 -> BuiltinResult (SomeConstant DefaultUni [b]))
-> SomeConstant DefaultUni [b]
-> BuiltinResult (SomeConstant DefaultUni [b])
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant DefaultUni [b]) (Esc a)
-> a -> SomeConstant DefaultUni [b]
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf UniOf (SomeConstant DefaultUni [b]) (Esc a)
DefaultUni (Esc a)
uniList a
xs

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Undefined =
        Opaque val (TyVarRep ('TyNameRep "a" 0))
-> (()
    -> FoldArgs
         (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> (cost
    -> FoldArgs
         (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. HasCallStack => a
undefined
            ()
-> FoldArgs
     (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Absurd =
        (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
    -> FoldArgs
         (GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Void -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
    -> FoldArgs
         (GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. Void -> a
absurd
            ()
-> FoldArgs
     (GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
     ExBudgetStream
()
-> Void
-> FoldArgs
     (GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ErrorPrime =
        BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
    -> FoldArgs
         (GetArgs
            (BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
    -> FoldArgs
         (GetArgs
            (BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            (BuiltinResult a
forall {a}. BuiltinResult a
forall err. AsEvaluationFailure err => err
evaluationFailure :: forall a. BuiltinResult a)
            () -> ExBudgetStream
()
-> FoldArgs
     (GetArgs
        (BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
     ExBudgetStream
forall a. Whatever a => a
whatever

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Comma =
        (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
             -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
             -> SomeConstant
                  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
             -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
             -> SomeConstant
                  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
     uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
forall a b.
SomeConstant uni a -> SomeConstant uni b -> SomeConstant uni (a, b)
commaPlc
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
         -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
         -> SomeConstant
              uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
     ExBudgetStream
()
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        commaPlc
            :: SomeConstant uni a
            -> SomeConstant uni b
            -> SomeConstant uni (a, b)
        commaPlc :: forall a b.
SomeConstant uni a -> SomeConstant uni b -> SomeConstant uni (a, b)
commaPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniA a
x))) (SomeConstant (Some (ValueOf uni (Esc a)
uniB a
y))) =
            UniOf (SomeConstant uni (a, b)) (Esc (a, a))
-> (a, a) -> SomeConstant uni (a, b)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf (DefaultUni (Esc a) -> DefaultUni (Esc a) -> DefaultUni (Esc (a, a))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
       {f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair uni (Esc a)
DefaultUni (Esc a)
uniA uni (Esc a)
DefaultUni (Esc a)
uniB) (a
x, a
y)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
BiconstPair =
        (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> BuiltinResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
             -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
             -> SomeConstant
                  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
             -> BuiltinResult
                  (SomeConstant
                     uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> BuiltinResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
             -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
             -> SomeConstant
                  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
             -> BuiltinResult
                  (SomeConstant
                     uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
     uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
     (SomeConstant
        uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
forall a b.
SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
biconstPairPlc
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
         -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
         -> SomeConstant
              uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
         -> BuiltinResult
              (SomeConstant
                 uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
     ExBudgetStream
()
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
     DefaultUni
     (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        biconstPairPlc
            :: SomeConstant uni a
            -> SomeConstant uni b
            -> SomeConstant uni (a, b)
            -> BuiltinResult (SomeConstant uni (a, b))
        biconstPairPlc :: forall a b.
SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
biconstPairPlc
            (SomeConstant (Some (ValueOf uni (Esc a)
uniA a
x)))
            (SomeConstant (Some (ValueOf uni (Esc a)
uniB a
y)))
            (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
_))) = do
                DefaultUniPair DefaultUni (Esc a2)
uniA' DefaultUni (Esc a1)
uniB' <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
                Just Esc a :~: Esc a2
Refl <- Maybe (Esc a :~: Esc a2)
-> BuiltinResult (Maybe (Esc a :~: Esc a2))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a2)
 -> BuiltinResult (Maybe (Esc a :~: Esc a2)))
-> Maybe (Esc a :~: Esc a2)
-> BuiltinResult (Maybe (Esc a :~: Esc a2))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniA uni (Esc a) -> uni (Esc a2) -> Maybe (Esc a :~: Esc a2)
forall a b. uni a -> uni b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a2)
DefaultUni (Esc a2)
uniA'
                Just Esc a :~: Esc a1
Refl <- Maybe (Esc a :~: Esc a1)
-> BuiltinResult (Maybe (Esc a :~: Esc a1))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a1)
 -> BuiltinResult (Maybe (Esc a :~: Esc a1)))
-> Maybe (Esc a :~: Esc a1)
-> BuiltinResult (Maybe (Esc a :~: Esc a1))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniB uni (Esc a) -> uni (Esc a1) -> Maybe (Esc a :~: Esc a1)
forall a b. uni a -> uni b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a1)
DefaultUni (Esc a1)
uniB'
                SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (a, b))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni (a, b)
 -> BuiltinResult (SomeConstant uni (a, b)))
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant uni (a, b)) (Esc (a, a))
-> (a, a) -> SomeConstant uni (a, b)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf uni (Esc a)
UniOf (SomeConstant uni (a, b)) (Esc (a, a))
uniPairAB (a
x, a
y)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Swap =
        (SomeConstant
   uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> BuiltinResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0))))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant
               uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
             -> BuiltinResult
                  (SomeConstant
                     uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant
   uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> BuiltinResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0))))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant
               uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
             -> BuiltinResult
                  (SomeConstant
                     uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant
  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
     (SomeConstant
        uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))
forall a b.
SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (b, a))
swapPlc
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant
           uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
         -> BuiltinResult
              (SomeConstant
                 uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
     ExBudgetStream
()
-> SomeConstant
     DefaultUni
     (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        swapPlc
            :: SomeConstant uni (a, b)
            -> BuiltinResult (SomeConstant uni (b, a))
        swapPlc :: forall a b.
SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (b, a))
swapPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
p))) = do
            DefaultUniPair DefaultUni (Esc a2)
uniA DefaultUni (Esc a1)
uniB <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
            SomeConstant uni (b, a) -> BuiltinResult (SomeConstant uni (b, a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni (b, a)
 -> BuiltinResult (SomeConstant uni (b, a)))
-> SomeConstant uni (b, a)
-> BuiltinResult (SomeConstant uni (b, a))
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant uni (b, a)) (Esc (a1, a2))
-> (a1, a2) -> SomeConstant uni (b, a)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf (DefaultUni (Esc a1)
-> DefaultUni (Esc a2) -> DefaultUni (Esc (a1, a2))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
       {f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair DefaultUni (Esc a1)
uniB DefaultUni (Esc a2)
uniA) ((a2, a1) -> a1
forall a b. (a, b) -> b
snd a
(a2, a1)
p, (a2, a1) -> a2
forall a b. (a, b) -> a
fst a
(a2, a1)
p)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
SwapEls =
        (SomeConstant
   uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
 -> BuiltinResult
      (SomeConstant
         uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))]))
-> (()
    -> FoldArgs
         (GetArgs
            (SomeConstant
               uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
             -> BuiltinResult
                  (SomeConstant
                     uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
         ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant
   uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
 -> BuiltinResult
      (SomeConstant
         uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))]))
-> (cost
    -> FoldArgs
         (GetArgs
            (SomeConstant
               uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
             -> BuiltinResult
                  (SomeConstant
                     uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
         ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant
  uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
     (SomeConstant
        uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])
forall a.
SomeConstant uni [SomeConstant uni (a, Bool)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc
            ()
-> FoldArgs
     (GetArgs
        (SomeConstant
           uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
         -> BuiltinResult
              (SomeConstant
                 uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
     ExBudgetStream
()
-> SomeConstant
     DefaultUni
     [SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> ExBudgetStream
forall a. Whatever a => a
whatever
      where
        -- The type reads as @[(a, Bool)] -> [(Bool, a)]@.
        swapElsPlc
            :: SomeConstant uni [SomeConstant uni (a, Bool)]
            -> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
        swapElsPlc :: forall a.
SomeConstant uni [SomeConstant uni (a, Bool)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniList a
xs))) = do
            DefaultUniList (DefaultUniPair DefaultUni (Esc a2)
uniA DefaultUni (Esc a1)
DefaultUniBool) <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniList
            let uniList' :: DefaultUni (Esc [(Bool, a2)])
uniList' = DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)])
forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList (DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)]))
-> DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)])
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Bool)
-> DefaultUni (Esc a2) -> DefaultUni (Esc (Bool, a2))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
       {f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair DefaultUni (Esc Bool)
DefaultUniBool DefaultUni (Esc a2)
uniA
            SomeConstant uni [SomeConstant uni (Bool, a)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni [SomeConstant uni (Bool, a)]
 -> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)]))
-> ([(Bool, a2)] -> SomeConstant uni [SomeConstant uni (Bool, a)])
-> [(Bool, a2)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniOf
  (SomeConstant uni [SomeConstant uni (Bool, a)]) (Esc [(Bool, a2)])
-> [(Bool, a2)] -> SomeConstant uni [SomeConstant uni (Bool, a)]
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf UniOf
  (SomeConstant uni [SomeConstant uni (Bool, a)]) (Esc [(Bool, a2)])
DefaultUni (Esc [(Bool, a2)])
uniList' ([(Bool, a2)]
 -> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)]))
-> [(Bool, a2)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall a b. (a -> b) -> a -> b
$ ((a2, Bool) -> (Bool, a2)) -> [(a2, Bool)] -> [(Bool, a2)]
forall a b. (a -> b) -> [a] -> [b]
map (a2, Bool) -> (Bool, a2)
forall a b. (a, b) -> (b, a)
swap a
[(a2, Bool)]
xs

    -- A dummy builtin to reflect the builtin-version of the 'ExtensionFun'.
    -- See Note [Builtin semantics variants]
    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
semvar ExtensionFun
ExtensionVersion =
        forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(() -> Integer)
            (\()
_ -> case BuiltinSemanticsVariant ExtensionFun
semvar of
                BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant0 -> Integer
0
                BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant1 -> Integer
1
                BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant2 -> Integer
2
                BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant3 -> Integer
3
                BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant4 -> Integer
4)
            () -> FoldArgs (GetArgs (() -> Integer)) ExBudgetStream
() -> () -> ExBudgetStream
forall a. Whatever a => a
whatever

    -- We want to know if the CEK machine releases individual budgets after accounting for them and
    -- one way to ensure that is to check that individual budgets are GCed in chunks rather than all
    -- at once when evaluation of the builtin finishes. This builtin returns a list of the maximum
    -- numbers of individual budgets retained between GC calls. If the returned list is long (for
    -- some definition of "long", see the tests), then chances are individual budgets are not
    -- retained unnecessarily, and if it's too short (again, see the tests), then they are.
    --
    -- We track how many budgets get GCed by attaching a finalizer (see "System.Mem.Weak") to each
    -- of them.
    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_ ExtensionFun
TrackCosts = IO (BuiltinMeaning val ()) -> BuiltinMeaning val ()
forall a. IO a -> a
unsafePerformIO (IO (BuiltinMeaning val ()) -> BuiltinMeaning val ())
-> IO (BuiltinMeaning val ()) -> BuiltinMeaning val ()
forall a b. (a -> b) -> a -> b
$ do
        -- A variable for storing the number of elements from the stream of budgets pending GC.
        MVar Integer
pendingGcVar <- Integer -> IO (MVar Integer)
forall a. a -> IO (MVar a)
newMVar Integer
0
        -- A variable for storing all the final numbers from @pendingGcVar@ appearing there right
        -- before another GC is triggered. We store the results in reverse order for fast consing
        -- and then 'reverse' them in the denotation of the builtin.
        MVar [Integer]
numsOfGcedVar <- [Integer] -> IO (MVar [Integer])
forall a. a -> IO (MVar a)
newMVar []
        let -- A function to run when GC picks up an individual budget.
            finalize :: IO ()
finalize =
                MVar Integer -> IO (Maybe Integer)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar Integer
pendingGcVar IO (Maybe Integer) -> (Maybe Integer -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    -- If @pendingGcVar@ happens to be empty, we say that no budgets were released
                    -- and don't update @pendingGcVar@. I.e. this entire testing machinery can
                    -- affect how budgets are retained, but the impact of the 'MVar' business is
                    -- negligible, since @pendingGcVar@ is filled immediately after it's emptied.
                    Maybe Integer
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                    -- If @pendingGcVar@ is not empty, then we cons its content to the resulting
                    -- list and put @0@ as the new content of the variable.
                    Just Integer
pendingGc -> do
                        ()
_ <- MVar [Integer] -> ([Integer] -> IO [Integer]) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar [Integer]
numsOfGcedVar (([Integer] -> IO [Integer]) -> IO ())
-> ([Integer] -> IO [Integer]) -> IO ()
forall a b. (a -> b) -> a -> b
$ [Integer] -> IO [Integer]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Integer] -> IO [Integer])
-> ([Integer] -> [Integer]) -> [Integer] -> IO [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
pendingGc Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
:)
                        MVar Integer -> Integer -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar Integer
pendingGcVar Integer
0

            -- Register an element of the stream of budgets by incrementing the counter storing the
            -- number of elements pending GC and attaching the @finalize@ finalizer to the element.
            regBudget :: ExBudget -> IO ()
regBudget ExBudget
budget = do
                Integer
pendingGc <- MVar Integer -> IO Integer
forall a. MVar a -> IO a
takeMVar MVar Integer
pendingGcVar
                let pendingGc' :: Integer
pendingGc' = Integer -> Integer
forall a. Enum a => a -> a
succ Integer
pendingGc
                MVar Integer -> Integer -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar Integer
pendingGcVar Integer
pendingGc'
                ExBudget -> IO () -> IO ()
forall key. key -> IO () -> IO ()
addFinalizer ExBudget
budget IO ()
finalize
                -- We need to trigger GC occasionally (otherwise it can easily take more than 100k
                -- elements before GC is triggered and the number can go much higher depending on
                -- the RTS options), so we picked 100 elements as a cutoff number. Doing GC less
                -- often makes tests slower, doing GC more often requires us to generate longer
                -- streams in tests in order to observe meaningful results making tests slower.
                Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
pendingGc' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
100) IO ()
performMinorGC

            -- Call @regBudget@ over each element of the stream of budgets.
            regBudgets :: ExBudgetStream -> IO ExBudgetStream
regBudgets (ExBudgetLast ExBudget
budget) = do
                ExBudget -> IO ()
regBudget ExBudget
budget
                -- Run @finalize@ one final time before returning the last budget.
                IO ()
finalize
                -- Make all outstanding finalizers inert, so that we don't mix up budgets GCed
                -- during spending with budgets GCed right after spending finishes.
                Integer
_ <- MVar Integer -> IO Integer
forall a. MVar a -> IO a
takeMVar MVar Integer
pendingGcVar
                ExBudgetStream -> IO ExBudgetStream
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExBudgetStream -> IO ExBudgetStream)
-> ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudget -> ExBudgetStream
ExBudgetLast ExBudget
budget
            regBudgets (ExBudgetCons ExBudget
budget ExBudgetStream
budgets) = do
                ExBudget -> IO ()
regBudget ExBudget
budget
                -- Without 'unsafeInterleaveIO' this function would traverse the entire stream
                -- before returning anything, which isn't what costing functions normally do and so
                -- we don't want to have such behavior in a test.
                ExBudgetStream
budgets' <- IO ExBudgetStream -> IO ExBudgetStream
forall a. IO a -> IO a
unsafeInterleaveIO (IO ExBudgetStream -> IO ExBudgetStream)
-> IO ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudgetStream -> IO ExBudgetStream
regBudgets ExBudgetStream
budgets
                ExBudgetStream -> IO ExBudgetStream
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExBudgetStream -> IO ExBudgetStream)
-> ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudget -> ExBudgetStream -> ExBudgetStream
ExBudgetCons ExBudget
budget ExBudgetStream
budgets'

            -- Just a random model that keeps the costs coming from the 'ExMemoryUsage' instance.
            linear1 :: ModelOneArgument
linear1 = OneVariableLinearFunction -> ModelOneArgument
ModelOneArgumentLinearInX (OneVariableLinearFunction -> ModelOneArgument)
-> OneVariableLinearFunction -> ModelOneArgument
forall a b. (a -> b) -> a -> b
$ Intercept -> Slope -> OneVariableLinearFunction
OneVariableLinearFunction Intercept
1 Slope
1
            model :: CostingFun ModelOneArgument
model   = ModelOneArgument -> ModelOneArgument -> CostingFun ModelOneArgument
forall model. model -> model -> CostingFun model
CostingFun ModelOneArgument
linear1 ModelOneArgument
linear1
        BuiltinMeaning val () -> IO (BuiltinMeaning val ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BuiltinMeaning val () -> IO (BuiltinMeaning val ()))
-> BuiltinMeaning val () -> IO (BuiltinMeaning val ())
forall a b. (a -> b) -> a -> b
$ forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Data -> [Integer])
            (\Data
_ -> IO [Integer] -> [Integer]
forall a. IO a -> a
unsafePerformIO (IO [Integer] -> [Integer]) -> IO [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [Integer]
forall a. [a] -> [a]
reverse ([Integer] -> [Integer]) -> IO [Integer] -> IO [Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVar [Integer] -> IO [Integer]
forall a. MVar a -> IO a
readMVar MVar [Integer]
numsOfGcedVar)
            (\()
_ -> IO ExBudgetStream -> ExBudgetStream
forall a. IO a -> a
unsafePerformIO (IO ExBudgetStream -> ExBudgetStream)
-> (Data -> IO ExBudgetStream) -> Data -> ExBudgetStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExBudgetStream -> IO ExBudgetStream
regBudgets (ExBudgetStream -> IO ExBudgetStream)
-> (Data -> ExBudgetStream) -> Data -> IO ExBudgetStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostingFun ModelOneArgument -> Data -> ExBudgetStream
forall a1.
ExMemoryUsage a1 =>
CostingFun ModelOneArgument -> a1 -> ExBudgetStream
runCostingFunOneArgument CostingFun ModelOneArgument
model)

    toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
semvar ExtensionFun
IntNoIntegerNoWord =
        case BuiltinSemanticsVariant ExtensionFun
semvar of
            BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant0 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Int     -> ()) Int -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Int -> ())) ExBudgetStream
() -> Int -> ExBudgetStream
forall a. Whatever a => a
whatever
            BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant1 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Integer -> ()) Integer -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Integer -> ())) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
            BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant2 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Integer -> ()) Integer -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Integer -> ())) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
            BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant3 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Word    -> ()) Word -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Word -> ())) ExBudgetStream
() -> Word -> ExBudgetStream
forall a. Whatever a => a
whatever
            BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant4 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Word    -> ()) Word -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Word -> ())) ExBudgetStream
() -> Word -> ExBudgetStream
forall a. Whatever a => a
whatever

instance Default (BuiltinSemanticsVariant ExtensionFun) where
    def :: BuiltinSemanticsVariant ExtensionFun
def = BuiltinSemanticsVariant ExtensionFun
forall a. Bounded a => a
maxBound