{-# 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 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
    | SumInteger
    | Const
    | Id
    | IdAssumeBool
    | IdAssumeCheckBool
    | IdSomeConstantBool
    | 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 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
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)
    deriving anyclass (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
tySch FoldArgs args res
toF (BuiltinRuntimeOptions RuntimeScheme (Length args)
runSch ToRuntimeDenotationType val (Length args)
immF ToRuntimeDenotationType val (Length args)
defF CostingPart (UniOf val) fun1 -> ToCostingType (Length args)
toExF) ->
            TypeScheme val args res
-> FoldArgs args res
-> BuiltinRuntimeOptions
     (Length args)
     val
     (CostingPart (UniOf val) fun1, CostingPart uni fun2)
-> BuiltinMeaning
     val (CostingPart (UniOf val) fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> BuiltinRuntimeOptions (Length args) val cost
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (RuntimeScheme (Length args)
-> ToRuntimeDenotationType val (Length args)
-> ToRuntimeDenotationType val (Length args)
-> ((CostingPart (UniOf val) fun1, CostingPart uni fun2)
    -> ToCostingType (Length args))
-> BuiltinRuntimeOptions
     (Length args)
     val
     (CostingPart (UniOf val) fun1, CostingPart uni fun2)
forall (n :: Peano) val cost.
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToRuntimeDenotationType val n
-> (cost -> ToCostingType n)
-> BuiltinRuntimeOptions n val cost
BuiltinRuntimeOptions RuntimeScheme (Length args)
runSch ToRuntimeDenotationType val (Length args)
immF ToRuntimeDenotationType val (Length args)
defF (CostingPart (UniOf val) fun1 -> ToCostingType (Length args)
toExF (CostingPart (UniOf val) fun1 -> ToCostingType (Length args))
-> ((CostingPart (UniOf val) fun1, CostingPart uni fun2)
    -> CostingPart (UniOf val) fun1)
-> (CostingPart (UniOf val) fun1, CostingPart uni fun2)
-> ToCostingType (Length 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
tySch FoldArgs args res
toF (BuiltinRuntimeOptions RuntimeScheme (Length args)
runSch ToRuntimeDenotationType val (Length args)
immF ToRuntimeDenotationType val (Length args)
defF CostingPart (UniOf val) fun2 -> ToCostingType (Length args)
toExF) ->
            TypeScheme val args res
-> FoldArgs args res
-> BuiltinRuntimeOptions
     (Length args) val (CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> BuiltinRuntimeOptions (Length args) val cost
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (RuntimeScheme (Length args)
-> ToRuntimeDenotationType val (Length args)
-> ToRuntimeDenotationType val (Length args)
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> ToCostingType (Length args))
-> BuiltinRuntimeOptions
     (Length args) val (CostingPart uni fun1, CostingPart uni fun2)
forall (n :: Peano) val cost.
RuntimeScheme n
-> ToRuntimeDenotationType val n
-> ToRuntimeDenotationType val n
-> (cost -> ToCostingType n)
-> BuiltinRuntimeOptions n val cost
BuiltinRuntimeOptions RuntimeScheme (Length args)
runSch ToRuntimeDenotationType val (Length args)
immF ToRuntimeDenotationType val (Length args)
defF (CostingPart uni fun2 -> ToCostingType (Length args)
CostingPart (UniOf val) fun2 -> ToCostingType (Length args)
toExF (CostingPart uni fun2 -> ToCostingType (Length args))
-> ((CostingPart uni fun1, CostingPart uni fun2)
    -> CostingPart uni fun2)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> ToCostingType (Length 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 = UnliftingMode
-> (BuiltinCostModel, ())
-> BuiltinsRuntime (Either DefaultFun ExtensionFun) term
forall cost (uni :: * -> *) fun val.
(cost ~ CostingPart uni fun, HasConstantIn uni val,
 ToBuiltinMeaning uni fun) =>
UnliftingMode -> cost -> BuiltinsRuntime fun val
toBuiltinsRuntime UnliftingMode
defaultUnliftingMode (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 => MakeKnownIn DefaultUni term Void where
    makeKnown :: Maybe cause -> Void -> MakeKnownM cause term
makeKnown Maybe cause
_ = Void -> MakeKnownM cause term
forall a. Void -> a
absurd
instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
    readKnown :: Maybe cause -> term -> ReadKnownM cause Void
readKnown Maybe cause
mayCause term
_ = AReview KnownTypeError UnliftingError
-> UnliftingError -> Maybe cause -> ReadKnownM 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 KnownTypeError UnliftingError
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Can't unlift a 'Void'" Maybe cause
mayCause

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
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)
    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
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)
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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])
            () -> ToCostingType (Length '[Integer])
forall a. Monoid a => a
mempty  -- Whatever.

    toBuiltinMeaning ExtensionFun
SumInteger =
        ([Integer] -> Integer)
-> (() -> ToCostingType (Length '[[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 -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum :: [Integer] -> Integer)
            () -> ToCostingType (Length '[[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)))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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)))
-> (()
    -> ToCostingType
         (Length '[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 -> ToCostingType (Length 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
IdAssumeBool =
        (Opaque val Bool -> Opaque val Bool)
-> (() -> ToCostingType (Length '[Opaque val 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 -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            (Opaque val Bool -> Opaque val Bool
forall a. a -> a
Prelude.id :: Opaque val Bool -> Opaque val Bool)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
IdAssumeCheckBool =
        (Opaque val Bool -> EvaluationResult Bool)
-> (() -> ToCostingType (Length '[Opaque val 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 -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            Opaque val Bool -> EvaluationResult Bool
idAssumeCheckBoolPlc
            () -> ToCostingType (Length '[Opaque val Bool])
forall a. Monoid a => a
mempty  -- Whatever.
      where
        idAssumeCheckBoolPlc :: Opaque val Bool -> EvaluationResult Bool
        idAssumeCheckBoolPlc :: Opaque val Bool -> EvaluationResult Bool
idAssumeCheckBoolPlc Opaque val Bool
val =
            case Maybe Any
-> Opaque val Bool
-> Either
     (ErrorWithCause UnliftingError Any)
     (Some (ValueOf (UniOf (Opaque val Bool))))
forall term err cause.
(HasConstant term, AsUnliftingError err) =>
Maybe cause
-> term
-> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf term)))
asConstant @_ @UnliftingError Maybe Any
forall a. Maybe a
Nothing Opaque val Bool
val of
                Right (Some (ValueOf DefaultUniBool b)) -> a -> EvaluationResult a
forall a. a -> EvaluationResult a
EvaluationSuccess a
b
                Either
  (ErrorWithCause UnliftingError Any)
  (Some (ValueOf (UniOf (Opaque val Bool))))
_                                       -> EvaluationResult Bool
forall a. EvaluationResult a
EvaluationFailure

    toBuiltinMeaning ExtensionFun
IdSomeConstantBool =
        (SomeConstant uni Bool -> EvaluationResult Bool)
-> (() -> ToCostingType (Length '[SomeConstant DefaultUni 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 -> ToCostingType (Length args)) -> BuiltinMeaning val cost
makeBuiltinMeaning
            SomeConstant uni Bool -> EvaluationResult Bool
idSomeConstantBoolPlc
            () -> ToCostingType (Length '[SomeConstant DefaultUni Bool])
forall a. Monoid a => a
mempty  -- Whatever.
      where
        idSomeConstantBoolPlc :: SomeConstant uni Bool -> EvaluationResult Bool
        idSomeConstantBoolPlc :: SomeConstant uni Bool -> EvaluationResult Bool
idSomeConstantBoolPlc = \case
            SomeConstant (Some (ValueOf uni (Esc a)
DefaultUniBool a
b)) -> a -> EvaluationResult a
forall a. a -> EvaluationResult a
EvaluationSuccess a
b
            SomeConstant uni Bool
_                                              -> EvaluationResult Bool
forall a. EvaluationResult a
EvaluationFailure

    toBuiltinMeaning ExtensionFun
IdFInteger =
        (Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
 -> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 (f `TyAppRep` 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))))
-> (()
    -> ToCostingType
         (Length '[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 -> ToCostingType (Length 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)))))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 (TyVarRep f `TyAppRep` TyVarRep a))
                => afa -> afa)
            (\()
_ ExMemory
_ -> ExCPU -> ExMemory -> ExBudget
ExBudget ExCPU
1 ExMemory
0)

    toBuiltinMeaning ExtensionFun
FailingSucc =
        (Integer -> Integer)
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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)
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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)
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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)
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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)))
-> (()
    -> ToCostingType
         (Length '[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 -> ToCostingType (Length 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)]))
-> (()
    -> ToCostingType
         (Length '[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 -> ToCostingType (Length 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))
-> (() -> ToCostingType (Length '[])) -> 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 -> ToCostingType (Length 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)))
-> (() -> ToCostingType (Length '[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 -> ToCostingType (Length 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)))
-> (() -> ToCostingType (Length '[])) -> 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 -> ToCostingType (Length 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)))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 ()
-> ToCostingType
     (Length
        '[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))))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 ()
-> ToCostingType
     (Length
        '[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))))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 ()
-> ToCostingType
     (Length
        '[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))]))
-> (()
    -> ToCostingType
         (Length
            '[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 -> ToCostingType (Length 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 ()
-> ToCostingType
     (Length
        '[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