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

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

module PlutusCore.Examples.Builtins where

import PlutusCore
import PlutusCore.Builtin
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Pretty

import PlutusCore.StdLib.Data.ScottList qualified as Plc

import Control.Exception
import Data.Either
import Data.Hashable (Hashable)
import Data.Kind qualified as GHC (Type)
import Data.Proxy
import Data.Tuple
import Data.Void
import GHC.Generics
import GHC.Ix
import Prettyprinter

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 :: 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 = (Bounded a, Enum a) => Int
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) = (Bounded a, Enum a) => Int
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
    | Const
    | Id
    | IdFInteger
    | IdList
    | IdRank2
    -- The next four are for testing that costing always precedes actual evaluation.
    | FailingSucc
    | ExpensiveSucc
    | FailingPlus
    | ExpensivePlus
    | 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.
    deriving (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
showList :: [ExtensionFun] -> ShowS
$cshowList :: [ExtensionFun] -> ShowS
show :: ExtensionFun -> [Char]
$cshow :: ExtensionFun -> [Char]
showsPrec :: Int -> ExtensionFun -> ShowS
$cshowsPrec :: Int -> ExtensionFun -> ShowS
Show, ExtensionFun -> ExtensionFun -> Bool
(ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool) -> Eq ExtensionFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtensionFun -> ExtensionFun -> Bool
$c/= :: ExtensionFun -> ExtensionFun -> Bool
== :: ExtensionFun -> ExtensionFun -> Bool
$c== :: 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
min :: ExtensionFun -> ExtensionFun -> ExtensionFun
$cmin :: ExtensionFun -> ExtensionFun -> ExtensionFun
max :: ExtensionFun -> ExtensionFun -> ExtensionFun
$cmax :: ExtensionFun -> ExtensionFun -> ExtensionFun
>= :: ExtensionFun -> ExtensionFun -> Bool
$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
compare :: ExtensionFun -> ExtensionFun -> Ordering
$ccompare :: ExtensionFun -> ExtensionFun -> Ordering
$cp1Ord :: Eq 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
enumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFrom :: ExtensionFun -> [ExtensionFun]
$cenumFrom :: ExtensionFun -> [ExtensionFun]
fromEnum :: ExtensionFun -> Int
$cfromEnum :: ExtensionFun -> Int
toEnum :: Int -> ExtensionFun
$ctoEnum :: Int -> ExtensionFun
pred :: ExtensionFun -> ExtensionFun
$cpred :: ExtensionFun -> ExtensionFun
succ :: ExtensionFun -> ExtensionFun
$csucc :: ExtensionFun -> ExtensionFun
Enum, ExtensionFun
ExtensionFun -> ExtensionFun -> Bounded ExtensionFun
forall a. a -> a -> Bounded a
maxBound :: ExtensionFun
$cmaxBound :: ExtensionFun
minBound :: ExtensionFun
$cminBound :: 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
unsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
$cunsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
rangeSize :: (ExtensionFun, ExtensionFun) -> Int
$crangeSize :: (ExtensionFun, ExtensionFun) -> Int
inRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
$cinRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
unsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cunsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
index :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cindex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
range :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
$crange :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
$cp1Ix :: Ord ExtensionFun
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
$cto :: forall x. Rep ExtensionFun x -> ExtensionFun
$cfrom :: forall x. ExtensionFun -> Rep ExtensionFun x
Generic, Int -> ExtensionFun -> Int
ExtensionFun -> Int
(Int -> ExtensionFun -> Int)
-> (ExtensionFun -> Int) -> Hashable ExtensionFun
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ExtensionFun -> Int
$chash :: ExtensionFun -> Int
hashWithSalt :: Int -> ExtensionFun -> Int
$chashWithSalt :: Int -> ExtensionFun -> Int
Hashable)

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

instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2) =>
            ToBuiltinMeaning uni (Either fun1 fun2) where
    type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)

    toBuiltinMeaning :: Either fun1 fun2
-> BuiltinMeaning val (CostingPart uni (Either fun1 fun2))
toBuiltinMeaning (Left  fun1
fun) = case fun1 -> BuiltinMeaning val (CostingPart (UniOf val) fun1)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasConstantIn uni val) =>
fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning fun1
fun of
        BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
toF CostingPart (UniOf val) fun1 -> FoldArgsEx args
toExF -> TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart (UniOf val) fun1, CostingPart uni fun2)
    -> FoldArgsEx args)
-> BuiltinMeaning
     val (CostingPart (UniOf val) fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> FoldArgsEx args)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
toF (CostingPart (UniOf val) fun1 -> FoldArgsEx args
toExF (CostingPart (UniOf val) fun1 -> FoldArgsEx args)
-> ((CostingPart (UniOf val) fun1, CostingPart uni fun2)
    -> CostingPart (UniOf val) fun1)
-> (CostingPart (UniOf val) fun1, CostingPart uni fun2)
-> FoldArgsEx args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CostingPart (UniOf val) fun1, CostingPart uni fun2)
-> CostingPart (UniOf val) fun1
forall a b. (a, b) -> a
fst)
    toBuiltinMeaning (Right fun2
fun) = case fun2 -> BuiltinMeaning val (CostingPart (UniOf val) fun2)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasConstantIn uni val) =>
fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning fun2
fun of
        BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
toF CostingPart (UniOf val) fun2 -> FoldArgsEx args
toExF -> TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> FoldArgsEx args)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> FoldArgsEx args)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
sch FoldArgs args res
toF (CostingPart uni fun2 -> FoldArgsEx args
CostingPart (UniOf val) fun2 -> FoldArgsEx args
toExF (CostingPart uni fun2 -> FoldArgsEx args)
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> CostingPart uni fun2)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> FoldArgsEx args
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)

defBuiltinsRuntimeExt
    :: HasConstantIn DefaultUni term
    => BuiltinsRuntime (Either DefaultFun ExtensionFun) term
defBuiltinsRuntimeExt :: BuiltinsRuntime (Either DefaultFun ExtensionFun) term
defBuiltinsRuntimeExt = (BuiltinCostModel, ())
-> BuiltinsRuntime (Either DefaultFun ExtensionFun) term
forall cost (uni :: * -> *) fun val.
(cost ~ CostingPart uni fun, HasConstantIn uni val,
 ToBuiltinMeaning uni fun) =>
cost -> BuiltinsRuntime fun val
toBuiltinsRuntime (BuiltinCostModel
defaultBuiltinCostModel, ())

data PlcListRep (a :: GHC.Type)
instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where
    type ToHoles (PlcListRep a) = '[RepHole a]
    type ToBinds (PlcListRep a) = ToBinds a

    toTypeAst :: proxy (PlcListRep a) -> Type TyName uni ()
toTypeAst proxy (PlcListRep a)
_ = ()
-> 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 ()
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 (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst 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
$ Proxy a
forall k (t :: k). Proxy t
Proxy @a

instance KnownTypeAst DefaultUni Void where
    toTypeAst :: proxy Void -> Type TyName DefaultUni ()
toTypeAst proxy Void
_ = 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 (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
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
a
instance UniOf term ~ DefaultUni => KnownTypeIn DefaultUni term Void where
    makeKnown :: (Text -> m ()) -> Maybe cause -> Void -> m term
makeKnown Text -> m ()
_ Maybe cause
_ = Void -> m term
forall a. Void -> a
absurd
    readKnown :: Maybe cause -> term -> Either (ErrorWithCause err cause) Void
readKnown Maybe cause
mayCause term
_ = AReview err UnliftingError
-> UnliftingError
-> Maybe cause
-> Either (ErrorWithCause err cause) Void
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview err UnliftingError
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Can't unlift a 'Void'" Maybe cause
mayCause

data BuiltinErrorCall = BuiltinErrorCall
    deriving (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
showList :: [BuiltinErrorCall] -> ShowS
$cshowList :: [BuiltinErrorCall] -> ShowS
show :: BuiltinErrorCall -> [Char]
$cshow :: BuiltinErrorCall -> [Char]
showsPrec :: Int -> BuiltinErrorCall -> ShowS
$cshowsPrec :: Int -> BuiltinErrorCall -> ShowS
Show, BuiltinErrorCall -> BuiltinErrorCall -> Bool
(BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> (BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> Eq BuiltinErrorCall
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
$c/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
$c== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
Eq, 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
displayException :: BuiltinErrorCall -> [Char]
$cdisplayException :: BuiltinErrorCall -> [Char]
fromException :: SomeException -> Maybe BuiltinErrorCall
$cfromException :: SomeException -> Maybe BuiltinErrorCall
toException :: BuiltinErrorCall -> SomeException
$ctoException :: BuiltinErrorCall -> SomeException
$cp2Exception :: Show BuiltinErrorCall
$cp1Exception :: Typeable BuiltinErrorCall
Exception)

-- 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 = ()
    toBuiltinMeaning :: forall val. HasConstantIn uni val => ExtensionFun -> BuiltinMeaning val ()

    toBuiltinMeaning :: ExtensionFun -> BuiltinMeaning val ()
toBuiltinMeaning ExtensionFun
Factorial =
        (Integer -> Integer)
-> (() -> FoldArgsEx '[Integer]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (\(Integer
n :: Integer) -> [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Integer
1..Integer
n])
            () -> FoldArgsEx '[Integer]
forall a. Monoid a => a
mempty  -- Whatever.

    toBuiltinMeaning ExtensionFun
Const =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
    -> FoldArgsEx
         '[Opaque val (TyVarRep ('TyNameRep "a" 0)),
           Opaque val (TyVarRep ('TyNameRep "b" 1))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> 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
            (\()
_ ExMemory
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
Id =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (() -> FoldArgsEx '[Opaque val (TyVarRep ('TyNameRep "a" 0))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. a -> a
Prelude.id
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
IdFInteger =
        (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
 -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (()
    -> FoldArgsEx
         '[Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (forall a. a -> a
forall fi (f :: * -> *).
(fi ~ Opaque val (TyAppRep f Integer)) =>
fi -> fi
Prelude.id :: fi ~ Opaque val (TyAppRep f Integer) => fi -> fi)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
IdList =
        (Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
 -> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0))))
-> (()
    -> FoldArgsEx
         '[Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (forall a. a -> a
forall la a. (la ~ Opaque val (PlcListRep a)) => la -> la
Prelude.id :: la ~ Opaque val (PlcListRep a) => la -> la)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning 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)))))
-> (()
    -> FoldArgsEx
         '[Opaque
             val
             (TyForallRep
                ('TyNameRep "b" 1)
                (TyAppRep
                   (TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (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 a (TyAppRep (TyVarRep f) (TyVarRep a)))
                => afa -> afa)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
FailingSucc =
        (Integer -> Integer)
-> (() -> FoldArgsEx '[Integer]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer)
            (\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
ExpensiveSucc =
        (Integer -> Integer)
-> (() -> FoldArgsEx '[Integer]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer)
            (\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ ExMemory
_ -> ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)

    toBuiltinMeaning ExtensionFun
FailingPlus =
        (Integer -> Integer -> Integer)
-> (() -> FoldArgsEx '[Integer, Integer]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer -> Integer)
            (\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ ExMemory
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
ExpensivePlus =
        (Integer -> Integer -> Integer)
-> (() -> FoldArgsEx '[Integer, Integer]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            @(Integer -> Integer -> Integer)
            (\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
            (\()
_ ExMemory
_ ExMemory
_ -> ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)

    toBuiltinMeaning ExtensionFun
UnsafeCoerce =
        (Opaque val (TyVarRep ('TyNameRep "a" 0))
 -> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (() -> FoldArgsEx '[Opaque val (TyVarRep ('TyNameRep "a" 0))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (val -> Opaque val (TyVarRep ('TyNameRep "b" 1))
forall val rep. val -> Opaque val rep
Opaque (val -> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> val)
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Opaque val (TyVarRep ('TyNameRep "a" 0)) -> val
forall val rep. Opaque val rep -> val
unOpaque)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
UnsafeCoerceEl =
        (SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
 -> EvaluationResult
      (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)]))
-> (()
    -> FoldArgsEx
         '[SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> EvaluationResult
     (SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])
forall a b.
SomeConstant DefaultUni [a]
-> EvaluationResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)
      where
        unsafeCoerceElPlc
            :: SomeConstant DefaultUni [a]
            -> EvaluationResult (SomeConstant DefaultUni [b])
        unsafeCoerceElPlc :: SomeConstant DefaultUni [a]
-> EvaluationResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc (SomeConstant (Some (ValueOf DefaultUni (Esc a)
uniList a
xs))) = do
            DefaultUniList DefaultUni (Esc a1)
_ <- DefaultUni (Esc a) -> EvaluationResult (DefaultUni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc a)
uniList
            SomeConstant DefaultUni [b]
-> EvaluationResult (SomeConstant DefaultUni [b])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant DefaultUni [b]
 -> EvaluationResult (SomeConstant DefaultUni [b]))
-> (Some (ValueOf DefaultUni) -> SomeConstant DefaultUni [b])
-> Some (ValueOf DefaultUni)
-> EvaluationResult (SomeConstant DefaultUni [b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> SomeConstant DefaultUni [b]
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Some (ValueOf DefaultUni)
 -> EvaluationResult (SomeConstant DefaultUni [b]))
-> Some (ValueOf DefaultUni)
-> EvaluationResult (SomeConstant DefaultUni [b])
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> a -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a)
uniList a
xs

    toBuiltinMeaning ExtensionFun
Undefined =
        Opaque val (TyVarRep ('TyNameRep "a" 0))
-> (() -> FoldArgsEx '[]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. HasCallStack => a
undefined
            (\()
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
Absurd =
        (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (() -> FoldArgsEx '[Void]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. Void -> a
absurd
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
ErrorPrime =
        EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (() -> FoldArgsEx '[]) -> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning
            EvaluationResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
forall a. EvaluationResult a
EvaluationFailure
            (\()
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
Comma = (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
-> (()
    -> FoldArgsEx
         '[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)),
           SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> 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 ()
-> FoldArgsEx
     '[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)),
       SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))]
forall a. Monoid a => a
mempty where
        commaPlc
            :: SomeConstant uni a
            -> SomeConstant uni b
            -> SomeConstant uni (a, b)
        commaPlc :: 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))) =
            Some (ValueOf DefaultUni) -> SomeConstant DefaultUni (a, b)
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Some (ValueOf DefaultUni) -> SomeConstant DefaultUni (a, b))
-> Some (ValueOf DefaultUni) -> SomeConstant DefaultUni (a, b)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc (a, a)) -> (a, a) -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf (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 ExtensionFun
BiconstPair = (SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
 -> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
 -> SomeConstant
      uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> EvaluationResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
-> (()
    -> FoldArgsEx
         '[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)),
           SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1)),
           SomeConstant
             DefaultUni
             (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> 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))
-> EvaluationResult
     (SomeConstant
        uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
forall a b.
SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> EvaluationResult (SomeConstant uni (a, b))
biconstPairPlc ()
-> FoldArgsEx
     '[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0)),
       SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1)),
       SomeConstant
         DefaultUni
         (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))]
forall a. Monoid a => a
mempty where
        biconstPairPlc
            :: SomeConstant uni a
            -> SomeConstant uni b
            -> SomeConstant uni (a, b)
            -> EvaluationResult (SomeConstant uni (a, b))
        biconstPairPlc :: SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> EvaluationResult (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 uniA' uniB' <- uni (Esc a) -> EvaluationResult (uni (Esc 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)
-> EvaluationResult (Maybe (Esc a :~: Esc a2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a2)
 -> EvaluationResult (Maybe (Esc a :~: Esc a2)))
-> Maybe (Esc a :~: Esc a2)
-> EvaluationResult (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 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)
-> EvaluationResult (Maybe (Esc a :~: Esc a1))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a1)
 -> EvaluationResult (Maybe (Esc a :~: Esc a1)))
-> Maybe (Esc a :~: Esc a1)
-> EvaluationResult (Maybe (Esc a :~: Esc a1))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniB uni (Esc a) -> uni (Esc a1) -> Maybe (Esc a :~: Esc a1)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a1)
DefaultUni (Esc a1)
uniB'
                SomeConstant uni (a, b)
-> EvaluationResult (SomeConstant uni (a, b))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni (a, b)
 -> EvaluationResult (SomeConstant uni (a, b)))
-> (Some (ValueOf uni) -> SomeConstant uni (a, b))
-> Some (ValueOf uni)
-> EvaluationResult (SomeConstant uni (a, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> SomeConstant uni (a, b)
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Some (ValueOf uni) -> EvaluationResult (SomeConstant uni (a, b)))
-> Some (ValueOf uni) -> EvaluationResult (SomeConstant uni (a, b))
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> a -> Some (ValueOf uni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
uniPairAB (a
x, a
y)

    toBuiltinMeaning ExtensionFun
Swap = (SomeConstant
   uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
 -> EvaluationResult
      (SomeConstant
         uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0))))
-> (()
    -> FoldArgsEx
         '[SomeConstant
             DefaultUni
             (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning SomeConstant
  uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> EvaluationResult
     (SomeConstant
        uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))
forall a b.
SomeConstant uni (a, b)
-> EvaluationResult (SomeConstant uni (b, a))
swapPlc ()
-> FoldArgsEx
     '[SomeConstant
         DefaultUni
         (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))]
forall a. Monoid a => a
mempty where
        swapPlc
            :: SomeConstant uni (a, b)
            -> EvaluationResult (SomeConstant uni (b, a))
        swapPlc :: SomeConstant uni (a, b)
-> EvaluationResult (SomeConstant uni (b, a))
swapPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
p))) = do
            DefaultUniPair uniA uniB <- uni (Esc a) -> EvaluationResult (uni (Esc a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
            SomeConstant DefaultUni (b, a)
-> EvaluationResult (SomeConstant DefaultUni (b, a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant DefaultUni (b, a)
 -> EvaluationResult (SomeConstant DefaultUni (b, a)))
-> (Some (ValueOf DefaultUni) -> SomeConstant DefaultUni (b, a))
-> Some (ValueOf DefaultUni)
-> EvaluationResult (SomeConstant DefaultUni (b, a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> SomeConstant DefaultUni (b, a)
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Some (ValueOf DefaultUni)
 -> EvaluationResult (SomeConstant DefaultUni (b, a)))
-> Some (ValueOf DefaultUni)
-> EvaluationResult (SomeConstant DefaultUni (b, a))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc (a1, a2)) -> (a1, a2) -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf (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 ExtensionFun
SwapEls = (SomeConstant
   uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
 -> EvaluationResult
      (SomeConstant
         uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))]))
-> (()
    -> FoldArgsEx
         '[SomeConstant
             DefaultUni
             [SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0), Bool)]])
-> BuiltinMeaning val ()
forall a val cost (binds :: [Some TyNameRep]) (args :: [*]) res
       (j :: Nat).
(binds ~ ToBinds a, args ~ GetArgs a, a ~ FoldArgs args res,
 ElaborateFromTo 0 j val a, KnownPolytype binds val args res a) =>
a -> (cost -> FoldArgsEx args) -> BuiltinMeaning val cost
makeBuiltinMeaning SomeConstant
  uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> EvaluationResult
     (SomeConstant
        uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])
forall a.
SomeConstant uni [SomeConstant uni (a, Bool)]
-> EvaluationResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc ()
-> FoldArgsEx
     '[SomeConstant
         DefaultUni
         [SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0), Bool)]]
forall a. Monoid a => a
mempty where
        -- The type reads as @[(a, Bool)] -> [(Bool, a)]@.
        swapElsPlc
            :: SomeConstant uni [SomeConstant uni (a, Bool)]
            -> EvaluationResult (SomeConstant uni [SomeConstant uni (Bool, a)])
        swapElsPlc :: SomeConstant uni [SomeConstant uni (a, Bool)]
-> EvaluationResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniList a
xs))) = do
            DefaultUniList (DefaultUniPair uniA DefaultUniBool) <- uni (Esc a) -> EvaluationResult (uni (Esc 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 DefaultUni [SomeConstant uni (Bool, a)]
-> EvaluationResult
     (SomeConstant DefaultUni [SomeConstant uni (Bool, a)])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant DefaultUni [SomeConstant uni (Bool, a)]
 -> EvaluationResult
      (SomeConstant DefaultUni [SomeConstant uni (Bool, a)]))
-> ([(Bool, a2)]
    -> SomeConstant DefaultUni [SomeConstant uni (Bool, a)])
-> [(Bool, a2)]
-> EvaluationResult
     (SomeConstant DefaultUni [SomeConstant uni (Bool, a)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni)
-> SomeConstant DefaultUni [SomeConstant uni (Bool, a)]
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Some (ValueOf DefaultUni)
 -> SomeConstant DefaultUni [SomeConstant uni (Bool, a)])
-> ([(Bool, a2)] -> Some (ValueOf DefaultUni))
-> [(Bool, a2)]
-> SomeConstant DefaultUni [SomeConstant uni (Bool, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc [(Bool, a2)])
-> [(Bool, a2)] -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc [(Bool, a2)])
uniList' ([(Bool, a2)]
 -> EvaluationResult
      (SomeConstant DefaultUni [SomeConstant uni (Bool, a)]))
-> [(Bool, a2)]
-> EvaluationResult
     (SomeConstant DefaultUni [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