{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Examples.Builtins where
import PlutusCore
import PlutusCore.Builtin
import PlutusCore.Data
import PlutusCore.Evaluation.Machine.BuiltinCostModel
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExBudgetStream
import PlutusCore.Evaluation.Result (evaluationFailure)
import PlutusCore.Pretty
import PlutusCore.StdLib.Data.ScottList qualified as Plc
import Control.Concurrent.MVar
import Control.Exception
import Control.Monad
import Data.Default.Class
import Data.Either
import Data.Kind qualified as GHC (Type)
import Data.Proxy
import Data.Some.GADT qualified as GADT
import Data.Tuple
import Data.Void
import GHC.Generics
import GHC.Ix
import GHC.TypeLits as GHC
import Prettyprinter
import System.IO.Unsafe (unsafeInterleaveIO, unsafePerformIO)
import System.Mem (performMinorGC)
import System.Mem.Weak (addFinalizer)
instance (Bounded a, Bounded b) => Bounded (Either a b) where
minBound :: Either a b
minBound = a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Bounded a => a
minBound
maxBound :: Either a b
maxBound = b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Bounded a => a
maxBound
size :: forall a. (Bounded a, Enum a) => Int
size :: forall a. (Bounded a, Enum a) => Int
size = a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
maxBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
- a -> Int
forall a. Enum a => a -> Int
fromEnum (a
forall a. Bounded a => a
minBound :: a) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
instance (Eq a, Eq b, Bounded a, Bounded b, Enum a, Enum b) => Enum (Either a b) where
succ :: Either a b -> Either a b
succ (Left a
x)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
maxBound = b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Bounded a => a
minBound
| Bool
otherwise = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
succ a
x
succ (Right b
y)
| b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. Bounded a => a
maxBound = [Char] -> Either a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds"
| Bool
otherwise = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> b
forall a. Enum a => a -> a
succ b
y
pred :: Either a b -> Either a b
pred (Left a
x)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
minBound = [Char] -> Either a b
forall a. HasCallStack => [Char] -> a
error [Char]
"Out of bounds"
| Bool
otherwise = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
pred a
x
pred (Right b
y)
| b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
forall a. Bounded a => a
minBound = a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Bounded a => a
maxBound
| Bool
otherwise = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> b
forall a. Enum a => a -> a
pred b
y
toEnum :: Int -> Either a b
toEnum Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
s = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> a
forall a. Enum a => Int -> a
toEnum Int
i
| Bool
otherwise = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> b
forall a. Enum a => Int -> a
toEnum (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
s)
where s :: Int
s = forall a. (Bounded a, Enum a) => Int
size @a
fromEnum :: Either a b -> Int
fromEnum (Left a
x) = a -> Int
forall a. Enum a => a -> Int
fromEnum a
x
fromEnum (Right b
y) = forall a. (Bounded a, Enum a) => Int
size @a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ b -> Int
forall a. Enum a => a -> Int
fromEnum b
y
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
data ExtensionFun
= Factorial
| ForallFortyTwo
| SumInteger
| Const
| Id
| IdAssumeBool
| IdAssumeCheckBool
| IdSomeConstantBool
| IdIntegerAsBool
| IdFInteger
| IdList
| IdRank2
| ScottToMetaUnit
| FailingSucc
| ExpensiveSucc
| FailingPlus
| ExpensivePlus
| IsConstant
| UnsafeCoerce
| UnsafeCoerceEl
| Undefined
| Absurd
| ErrorPrime
| Comma
| BiconstPair
| Swap
| SwapEls
| ExtensionVersion
| TrackCosts
| IntNoIntegerNoWord
deriving stock (Int -> ExtensionFun -> ShowS
[ExtensionFun] -> ShowS
ExtensionFun -> [Char]
(Int -> ExtensionFun -> ShowS)
-> (ExtensionFun -> [Char])
-> ([ExtensionFun] -> ShowS)
-> Show ExtensionFun
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExtensionFun -> ShowS
showsPrec :: Int -> ExtensionFun -> ShowS
$cshow :: ExtensionFun -> [Char]
show :: ExtensionFun -> [Char]
$cshowList :: [ExtensionFun] -> ShowS
showList :: [ExtensionFun] -> ShowS
Show, ExtensionFun -> ExtensionFun -> Bool
(ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool) -> Eq ExtensionFun
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExtensionFun -> ExtensionFun -> Bool
== :: ExtensionFun -> ExtensionFun -> Bool
$c/= :: ExtensionFun -> ExtensionFun -> Bool
/= :: ExtensionFun -> ExtensionFun -> Bool
Eq, Eq ExtensionFun
Eq ExtensionFun =>
(ExtensionFun -> ExtensionFun -> Ordering)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> Bool)
-> (ExtensionFun -> ExtensionFun -> ExtensionFun)
-> (ExtensionFun -> ExtensionFun -> ExtensionFun)
-> Ord ExtensionFun
ExtensionFun -> ExtensionFun -> Bool
ExtensionFun -> ExtensionFun -> Ordering
ExtensionFun -> ExtensionFun -> ExtensionFun
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ExtensionFun -> ExtensionFun -> Ordering
compare :: ExtensionFun -> ExtensionFun -> Ordering
$c< :: ExtensionFun -> ExtensionFun -> Bool
< :: ExtensionFun -> ExtensionFun -> Bool
$c<= :: ExtensionFun -> ExtensionFun -> Bool
<= :: ExtensionFun -> ExtensionFun -> Bool
$c> :: ExtensionFun -> ExtensionFun -> Bool
> :: ExtensionFun -> ExtensionFun -> Bool
$c>= :: ExtensionFun -> ExtensionFun -> Bool
>= :: ExtensionFun -> ExtensionFun -> Bool
$cmax :: ExtensionFun -> ExtensionFun -> ExtensionFun
max :: ExtensionFun -> ExtensionFun -> ExtensionFun
$cmin :: ExtensionFun -> ExtensionFun -> ExtensionFun
min :: ExtensionFun -> ExtensionFun -> ExtensionFun
Ord, Int -> ExtensionFun
ExtensionFun -> Int
ExtensionFun -> [ExtensionFun]
ExtensionFun -> ExtensionFun
ExtensionFun -> ExtensionFun -> [ExtensionFun]
ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
(ExtensionFun -> ExtensionFun)
-> (ExtensionFun -> ExtensionFun)
-> (Int -> ExtensionFun)
-> (ExtensionFun -> Int)
-> (ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> (ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun])
-> Enum ExtensionFun
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ExtensionFun -> ExtensionFun
succ :: ExtensionFun -> ExtensionFun
$cpred :: ExtensionFun -> ExtensionFun
pred :: ExtensionFun -> ExtensionFun
$ctoEnum :: Int -> ExtensionFun
toEnum :: Int -> ExtensionFun
$cfromEnum :: ExtensionFun -> Int
fromEnum :: ExtensionFun -> Int
$cenumFrom :: ExtensionFun -> [ExtensionFun]
enumFrom :: ExtensionFun -> [ExtensionFun]
$cenumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromThen :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromTo :: ExtensionFun -> ExtensionFun -> [ExtensionFun]
$cenumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
enumFromThenTo :: ExtensionFun -> ExtensionFun -> ExtensionFun -> [ExtensionFun]
Enum, ExtensionFun
ExtensionFun -> ExtensionFun -> Bounded ExtensionFun
forall a. a -> a -> Bounded a
$cminBound :: ExtensionFun
minBound :: ExtensionFun
$cmaxBound :: ExtensionFun
maxBound :: ExtensionFun
Bounded, Ord ExtensionFun
Ord ExtensionFun =>
((ExtensionFun, ExtensionFun) -> [ExtensionFun])
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Int)
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Int)
-> ((ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool)
-> ((ExtensionFun, ExtensionFun) -> Int)
-> ((ExtensionFun, ExtensionFun) -> Int)
-> Ix ExtensionFun
(ExtensionFun, ExtensionFun) -> Int
(ExtensionFun, ExtensionFun) -> [ExtensionFun]
(ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
(ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
forall a.
Ord a =>
((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
$crange :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
range :: (ExtensionFun, ExtensionFun) -> [ExtensionFun]
$cindex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
index :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cunsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
unsafeIndex :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Int
$cinRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
inRange :: (ExtensionFun, ExtensionFun) -> ExtensionFun -> Bool
$crangeSize :: (ExtensionFun, ExtensionFun) -> Int
rangeSize :: (ExtensionFun, ExtensionFun) -> Int
$cunsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
unsafeRangeSize :: (ExtensionFun, ExtensionFun) -> Int
Ix, (forall x. ExtensionFun -> Rep ExtensionFun x)
-> (forall x. Rep ExtensionFun x -> ExtensionFun)
-> Generic ExtensionFun
forall x. Rep ExtensionFun x -> ExtensionFun
forall x. ExtensionFun -> Rep ExtensionFun x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExtensionFun -> Rep ExtensionFun x
from :: forall x. ExtensionFun -> Rep ExtensionFun x
$cto :: forall x. Rep ExtensionFun x -> ExtensionFun
to :: forall x. Rep ExtensionFun x -> ExtensionFun
Generic)
deriving anyclass (Eq ExtensionFun
Eq ExtensionFun =>
(Int -> ExtensionFun -> Int)
-> (ExtensionFun -> Int) -> Hashable ExtensionFun
Int -> ExtensionFun -> Int
ExtensionFun -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> ExtensionFun -> Int
hashWithSalt :: Int -> ExtensionFun -> Int
$chash :: ExtensionFun -> Int
hash :: ExtensionFun -> Int
Hashable)
instance Pretty ExtensionFun where pretty :: forall ann. ExtensionFun -> Doc ann
pretty = ExtensionFun -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow
instance (ToBuiltinMeaning uni fun1, ToBuiltinMeaning uni fun2
, Default (BuiltinSemanticsVariant fun1), Default (BuiltinSemanticsVariant fun2)
) => ToBuiltinMeaning uni (Either fun1 fun2) where
type CostingPart uni (Either fun1 fun2) = (CostingPart uni fun1, CostingPart uni fun2)
data BuiltinSemanticsVariant (Either fun1 fun2) =
PairV (BuiltinSemanticsVariant fun1) (BuiltinSemanticsVariant fun2)
toBuiltinMeaning :: forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant (Either fun1 fun2)
-> Either fun1 fun2
-> BuiltinMeaning val (CostingPart uni (Either fun1 fun2))
toBuiltinMeaning (PairV BuiltinSemanticsVariant fun1
semvarL BuiltinSemanticsVariant fun2
_) (Left fun1
fun) = case BuiltinSemanticsVariant fun1
-> fun1 -> BuiltinMeaning val (CostingPart (UniOf val) fun1)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun1
-> fun1 -> BuiltinMeaning val (CostingPart (UniOf val) fun1)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun1
semvarL fun1
fun of
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF CostingPart (UniOf val) fun1 -> BuiltinRuntime val
denot ->
TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (CostingPart uni fun1 -> BuiltinRuntime val
CostingPart (UniOf val) fun1 -> BuiltinRuntime val
denot (CostingPart uni fun1 -> BuiltinRuntime val)
-> ((CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun1)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun1
forall a b. (a, b) -> a
fst)
toBuiltinMeaning (PairV BuiltinSemanticsVariant fun1
_ BuiltinSemanticsVariant fun2
semvarR) (Right fun2
fun) = case BuiltinSemanticsVariant fun2
-> fun2 -> BuiltinMeaning val (CostingPart (UniOf val) fun2)
forall val.
HasMeaningIn (UniOf val) val =>
BuiltinSemanticsVariant fun2
-> fun2 -> BuiltinMeaning val (CostingPart (UniOf val) fun2)
forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning BuiltinSemanticsVariant fun2
semvarR fun2
fun of
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF CostingPart (UniOf val) fun2 -> BuiltinRuntime val
denot ->
TypeScheme val args res
-> FoldArgs args res
-> ((CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val)
-> BuiltinMeaning val (CostingPart uni fun1, CostingPart uni fun2)
forall val cost (args :: [*]) res.
TypeScheme val args res
-> FoldArgs args res
-> (cost -> BuiltinRuntime val)
-> BuiltinMeaning val cost
BuiltinMeaning TypeScheme val args res
tySch FoldArgs args res
toF (CostingPart uni fun2 -> BuiltinRuntime val
CostingPart (UniOf val) fun2 -> BuiltinRuntime val
denot (CostingPart uni fun2 -> BuiltinRuntime val)
-> ((CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun2)
-> (CostingPart uni fun1, CostingPart uni fun2)
-> BuiltinRuntime val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CostingPart uni fun1, CostingPart uni fun2)
-> CostingPart uni fun2
forall a b. (a, b) -> b
snd)
instance (Default (BuiltinSemanticsVariant fun1), Default (BuiltinSemanticsVariant fun2))
=> Default (BuiltinSemanticsVariant (Either fun1 fun2)) where
def :: BuiltinSemanticsVariant (Either fun1 fun2)
def = BuiltinSemanticsVariant fun1
-> BuiltinSemanticsVariant fun2
-> BuiltinSemanticsVariant (Either fun1 fun2)
forall fun1 fun2.
BuiltinSemanticsVariant fun1
-> BuiltinSemanticsVariant fun2
-> BuiltinSemanticsVariant (Either fun1 fun2)
PairV BuiltinSemanticsVariant fun1
forall a. Default a => a
def BuiltinSemanticsVariant fun2
forall a. Default a => a
def
newtype MetaForall name a = MetaForall a
instance
( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq
, KnownKind kind, KnownTypeAst tyname uni a
) => KnownTypeAst tyname uni (MetaForall name a) where
type IsBuiltin _ (MetaForall name a) = 'False
type ToHoles _ _ (MetaForall name a) = '[TypeHole a]
type ToBinds uni acc (MetaForall name a) = ToBinds uni (Insert ('GADT.Some name) acc) a
typeAst :: Type tyname uni ()
typeAst = Proxy a -> Type tyname uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
instance MakeKnownIn DefaultUni term a => MakeKnownIn DefaultUni term (MetaForall name a) where
makeKnown :: MetaForall name a -> BuiltinResult (HeadSpine term)
makeKnown (MetaForall a
x) = a -> BuiltinResult (HeadSpine term)
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult (HeadSpine val)
makeKnown a
x
data PlcListRep (a :: GHC.Type)
instance (tyname ~ TyName, KnownTypeAst tyname uni a) =>
KnownTypeAst tyname uni (PlcListRep a) where
type IsBuiltin _ (PlcListRep a) = 'False
type ToHoles _ _ (PlcListRep a) = '[RepHole a]
type ToBinds uni acc (PlcListRep a) = ToBinds uni acc a
typeAst :: Type tyname uni ()
typeAst = ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type tyname uni ()
Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
Plc.listTy (Type tyname uni () -> Type tyname uni ())
-> (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Type tyname uni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy a -> Type tyname uni ()) -> Proxy a -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
instance tyname ~ TyName => KnownTypeAst tyname DefaultUni Void where
type IsBuiltin _ _ = 'False
type ToHoles _ _ _ = '[]
type ToBinds _ acc _ = acc
typeAst :: Type tyname DefaultUni ()
typeAst = Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ()
forall a. Quote a -> a
runQuote (Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ())
-> Quote (Type tyname DefaultUni ()) -> Type tyname DefaultUni ()
forall a b. (a -> b) -> a -> b
$ do
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ()))
-> Type tyname DefaultUni () -> Quote (Type tyname DefaultUni ())
forall a b. (a -> b) -> a -> b
$ ()
-> tyname
-> Kind ()
-> Type tyname DefaultUni ()
-> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () tyname
TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type tyname DefaultUni () -> Type tyname DefaultUni ())
-> Type tyname DefaultUni () -> Type tyname DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> tyname -> Type tyname DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () tyname
TyName
a
instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where
makeKnown :: Void -> BuiltinResult (HeadSpine term)
makeKnown = Void -> BuiltinResult (HeadSpine term)
forall a. Void -> a
absurd
instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
readKnown :: term -> ReadKnownM Void
readKnown term
_ = AReview BuiltinError UnliftingError
-> UnliftingError -> ReadKnownM Void
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview BuiltinError UnliftingError
forall err. AsBuiltinError err => Prism' err UnliftingError
Prism' BuiltinError UnliftingError
_StructuralUnliftingError UnliftingError
"Can't unlift to 'Void'"
data BuiltinErrorCall = BuiltinErrorCall
deriving stock (Int -> BuiltinErrorCall -> ShowS
[BuiltinErrorCall] -> ShowS
BuiltinErrorCall -> [Char]
(Int -> BuiltinErrorCall -> ShowS)
-> (BuiltinErrorCall -> [Char])
-> ([BuiltinErrorCall] -> ShowS)
-> Show BuiltinErrorCall
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinErrorCall -> ShowS
showsPrec :: Int -> BuiltinErrorCall -> ShowS
$cshow :: BuiltinErrorCall -> [Char]
show :: BuiltinErrorCall -> [Char]
$cshowList :: [BuiltinErrorCall] -> ShowS
showList :: [BuiltinErrorCall] -> ShowS
Show, BuiltinErrorCall -> BuiltinErrorCall -> Bool
(BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> (BuiltinErrorCall -> BuiltinErrorCall -> Bool)
-> Eq BuiltinErrorCall
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
== :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
$c/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
/= :: BuiltinErrorCall -> BuiltinErrorCall -> Bool
Eq)
deriving anyclass (Show BuiltinErrorCall
Typeable BuiltinErrorCall
(Typeable BuiltinErrorCall, Show BuiltinErrorCall) =>
(BuiltinErrorCall -> SomeException)
-> (SomeException -> Maybe BuiltinErrorCall)
-> (BuiltinErrorCall -> [Char])
-> Exception BuiltinErrorCall
SomeException -> Maybe BuiltinErrorCall
BuiltinErrorCall -> [Char]
BuiltinErrorCall -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> [Char]) -> Exception e
$ctoException :: BuiltinErrorCall -> SomeException
toException :: BuiltinErrorCall -> SomeException
$cfromException :: SomeException -> Maybe BuiltinErrorCall
fromException :: SomeException -> Maybe BuiltinErrorCall
$cdisplayException :: BuiltinErrorCall -> [Char]
displayException :: BuiltinErrorCall -> [Char]
Exception)
class Whatever a where
whatever :: a
instance Whatever b => Whatever (a -> b) where
whatever :: a -> b
whatever a
_ = b
forall a. Whatever a => a
whatever
instance Whatever ExBudgetStream where
whatever :: ExBudgetStream
whatever = ExBudget -> ExBudgetStream
ExBudgetLast ExBudget
forall a. Monoid a => a
mempty
instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where
type CostingPart uni ExtensionFun = ()
data BuiltinSemanticsVariant ExtensionFun =
ExtensionFunSemanticsVariant0
| ExtensionFunSemanticsVariant1
| ExtensionFunSemanticsVariant2
| ExtensionFunSemanticsVariant3
| ExtensionFunSemanticsVariant4
deriving stock (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
(BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> Eq (BuiltinSemanticsVariant ExtensionFun)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
== :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c/= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
/= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
Eq, Eq (BuiltinSemanticsVariant ExtensionFun)
Eq (BuiltinSemanticsVariant ExtensionFun) =>
(BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun)
-> Ord (BuiltinSemanticsVariant ExtensionFun)
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
compare :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Ordering
$c< :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
< :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c<= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
<= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c> :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
> :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$c>= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
>= :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun -> Bool
$cmax :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
max :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$cmin :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
min :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
Ord, Int -> BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun -> Int
BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
(BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun)
-> (Int -> BuiltinSemanticsVariant ExtensionFun)
-> (BuiltinSemanticsVariant ExtensionFun -> Int)
-> (BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun])
-> (BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun])
-> Enum (BuiltinSemanticsVariant ExtensionFun)
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
succ :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$cpred :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
pred :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
$ctoEnum :: Int -> BuiltinSemanticsVariant ExtensionFun
toEnum :: Int -> BuiltinSemanticsVariant ExtensionFun
$cfromEnum :: BuiltinSemanticsVariant ExtensionFun -> Int
fromEnum :: BuiltinSemanticsVariant ExtensionFun -> Int
$cenumFrom :: BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFrom :: BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromThen :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromThen :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
$cenumFromThenTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
enumFromThenTo :: BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> [BuiltinSemanticsVariant ExtensionFun]
Enum, BuiltinSemanticsVariant ExtensionFun
BuiltinSemanticsVariant ExtensionFun
-> BuiltinSemanticsVariant ExtensionFun
-> Bounded (BuiltinSemanticsVariant ExtensionFun)
forall a. a -> a -> Bounded a
$cminBound :: BuiltinSemanticsVariant ExtensionFun
minBound :: BuiltinSemanticsVariant ExtensionFun
$cmaxBound :: BuiltinSemanticsVariant ExtensionFun
maxBound :: BuiltinSemanticsVariant ExtensionFun
Bounded, Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
[BuiltinSemanticsVariant ExtensionFun] -> ShowS
BuiltinSemanticsVariant ExtensionFun -> [Char]
(Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS)
-> (BuiltinSemanticsVariant ExtensionFun -> [Char])
-> ([BuiltinSemanticsVariant ExtensionFun] -> ShowS)
-> Show (BuiltinSemanticsVariant ExtensionFun)
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
showsPrec :: Int -> BuiltinSemanticsVariant ExtensionFun -> ShowS
$cshow :: BuiltinSemanticsVariant ExtensionFun -> [Char]
show :: BuiltinSemanticsVariant ExtensionFun -> [Char]
$cshowList :: [BuiltinSemanticsVariant ExtensionFun] -> ShowS
showList :: [BuiltinSemanticsVariant ExtensionFun] -> ShowS
Show)
toBuiltinMeaning :: forall val. HasMeaningIn uni val
=> BuiltinSemanticsVariant ExtensionFun
-> ExtensionFun
-> BuiltinMeaning val ()
toBuiltinMeaning :: forall val.
HasMeaningIn uni val =>
BuiltinSemanticsVariant ExtensionFun
-> ExtensionFun -> BuiltinMeaning val ()
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Factorial =
(Integer -> Integer)
-> (() -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Integer -> Integer)
-> (cost -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(\(Integer
n :: Integer) -> [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Integer
1..Integer
n])
() -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ForallFortyTwo =
MetaForall ('TyNameRep "a" 0) Integer
-> (()
-> FoldArgs
(GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
MetaForall ('TyNameRep "a" 0) Integer
-> (cost
-> FoldArgs
(GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
MetaForall ('TyNameRep "a" 0) Integer
forallFortyTwo
() -> ExBudgetStream
()
-> FoldArgs
(GetArgs (MetaForall ('TyNameRep "a" 0) Integer)) ExBudgetStream
forall a. Whatever a => a
whatever
where
forallFortyTwo :: MetaForall ('TyNameRep @GHC.Type "a" 0) Integer
forallFortyTwo :: MetaForall ('TyNameRep "a" 0) Integer
forallFortyTwo = Integer -> MetaForall ('TyNameRep "a" 0) Integer
forall {k} (name :: k) a. a -> MetaForall name a
MetaForall Integer
42
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
SumInteger =
([Integer] -> Integer)
-> (() -> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
([Integer] -> Integer)
-> (cost
-> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum :: [Integer] -> Integer)
() -> FoldArgs (GetArgs ([Integer] -> Integer)) ExBudgetStream
() -> [Integer] -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Const =
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a b. a -> b -> a
const
()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream
()
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Id =
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. a -> a
Prelude.id
()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream
()
-> Opaque val (TyVarRep ('TyNameRep "a" 0))
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdAssumeBool =
(Opaque val Bool -> Opaque val Bool)
-> (()
-> FoldArgs
(GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val Bool -> Opaque val Bool)
-> (cost
-> FoldArgs
(GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(Opaque val Bool -> Opaque val Bool
forall a. a -> a
Prelude.id :: Opaque val Bool -> Opaque val Bool)
()
-> FoldArgs
(GetArgs (Opaque val Bool -> Opaque val Bool)) ExBudgetStream
() -> Opaque val Bool -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdAssumeCheckBool =
(Opaque val Bool -> BuiltinResult Bool)
-> (()
-> FoldArgs
(GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val Bool -> BuiltinResult Bool)
-> (cost
-> FoldArgs
(GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val Bool -> BuiltinResult Bool
idAssumeCheckBoolPlc
()
-> FoldArgs
(GetArgs (Opaque val Bool -> BuiltinResult Bool)) ExBudgetStream
() -> Opaque val Bool -> ExBudgetStream
forall a. Whatever a => a
whatever
where
idAssumeCheckBoolPlc :: Opaque val Bool -> BuiltinResult Bool
idAssumeCheckBoolPlc :: Opaque val Bool -> BuiltinResult Bool
idAssumeCheckBoolPlc Opaque val Bool
val =
case Opaque val Bool
-> Either BuiltinError (Some (ValueOf (UniOf (Opaque val Bool))))
forall term.
HasConstant term =>
term -> Either BuiltinError (Some (ValueOf (UniOf term)))
asConstant Opaque val Bool
val of
Right (Some (ValueOf DefaultUni (Esc a)
DefaultUniBool a
b)) -> Bool -> BuiltinResult Bool
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Bool
b
Either BuiltinError (Some (ValueOf (UniOf (Opaque val Bool))))
_ -> BuiltinResult Bool
forall err. AsEvaluationFailure err => err
evaluationFailure
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdSomeConstantBool =
(SomeConstant uni Bool -> BuiltinResult Bool)
-> (()
-> FoldArgs
(GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni Bool -> BuiltinResult Bool)
-> (cost
-> FoldArgs
(GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant uni Bool -> BuiltinResult Bool
idSomeConstantBoolPlc
()
-> FoldArgs
(GetArgs (SomeConstant uni Bool -> BuiltinResult Bool))
ExBudgetStream
() -> SomeConstant DefaultUni Bool -> ExBudgetStream
forall a. Whatever a => a
whatever
where
idSomeConstantBoolPlc :: SomeConstant uni Bool -> BuiltinResult Bool
idSomeConstantBoolPlc :: SomeConstant uni Bool -> BuiltinResult Bool
idSomeConstantBoolPlc = \case
SomeConstant (Some (ValueOf uni (Esc a)
DefaultUni (Esc a)
DefaultUniBool a
b)) -> Bool -> BuiltinResult Bool
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Bool
b
SomeConstant uni Bool
_ -> BuiltinResult Bool
forall err. AsEvaluationFailure err => err
evaluationFailure
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdIntegerAsBool =
(SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
idIntegerAsBool
()
-> FoldArgs
(GetArgs
(SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)))
ExBudgetStream
() -> SomeConstant DefaultUni Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
where
idIntegerAsBool :: SomeConstant uni Integer -> BuiltinResult (SomeConstant uni Integer)
idIntegerAsBool :: SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
idIntegerAsBool = \case
con :: SomeConstant uni Integer
con@(SomeConstant (Some (ValueOf uni (Esc a)
DefaultUni (Esc a)
DefaultUniBool a
_))) -> SomeConstant uni Integer
-> BuiltinResult (SomeConstant uni Integer)
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeConstant uni Integer
con
SomeConstant uni Integer
_ -> BuiltinResult (SomeConstant uni Integer)
forall err. AsEvaluationFailure err => err
evaluationFailure
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdFInteger =
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (()
-> FoldArgs
(GetArgs
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer))
-> (cost
-> FoldArgs
(GetArgs
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(fi -> fi
forall a. a -> a
forall {fi} {f :: * -> *}.
(fi ~ Opaque val (TyAppRep f Integer)) =>
fi -> fi
Prelude.id :: fi ~ Opaque val (f `TyAppRep` Integer) => fi -> fi)
()
-> FoldArgs
(GetArgs
(Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)))
ExBudgetStream
()
-> Opaque val (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer)
-> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdList =
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0))))
-> (()
-> FoldArgs
(GetArgs
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0))))
-> (cost
-> FoldArgs
(GetArgs
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(la -> la
forall a. a -> a
forall {la} {a}. (la ~ Opaque val (PlcListRep a)) => la -> la
Prelude.id :: la ~ Opaque val (PlcListRep a) => la -> la)
()
-> FoldArgs
(GetArgs
(Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream
()
-> Opaque val (PlcListRep (TyVarRep ('TyNameRep "a" 0)))
-> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IdRank2 =
(Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1)))))
-> (()
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1)))))
-> (cost
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(afa -> afa
forall a. a -> a
forall {afa} {a :: TyNameRep (*)} {f :: TyNameRep (* -> *)}.
(afa
~ Opaque
val (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a)))) =>
afa -> afa
Prelude.id
:: afa ~ Opaque val (TyForallRep @GHC.Type a (TyVarRep f `TyAppRep` TyVarRep a))
=> afa -> afa)
()
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))))
ExBudgetStream
()
-> Opaque
val
(TyForallRep
('TyNameRep "b" 1)
(TyAppRep
(TyVarRep ('TyNameRep "f" 0)) (TyVarRep ('TyNameRep "b" 1))))
-> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ScottToMetaUnit =
(Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ())
-> (()
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ()))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ())
-> (cost
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ()))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
((\Opaque val (TyForallRep a (va -> va))
_ -> ())
:: va ~ TyVarRep a
=> Opaque val (TyForallRep a (va -> va)) -> ())
()
-> FoldArgs
(GetArgs
(Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ()))
ExBudgetStream
()
-> Opaque
val
(TyForallRep
('TyNameRep "a" 0)
(TyVarRep ('TyNameRep "a" 0) -> TyVarRep ('TyNameRep "a" 0)))
-> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
FailingSucc =
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(Integer -> Integer)
(\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
() -> FoldArgs (GetArgs (Integer -> Integer)) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ExpensiveSucc =
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(Integer -> Integer)
(\Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
(\()
_ Integer
_ -> ExBudget -> ExBudgetStream
ExBudgetLast (ExBudget -> ExBudgetStream) -> ExBudget -> ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
FailingPlus =
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(Integer -> Integer -> Integer)
(\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
()
-> FoldArgs
(GetArgs (Integer -> Integer -> Integer)) ExBudgetStream
() -> Integer -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ExpensivePlus =
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(Integer -> Integer -> Integer)
(\Integer
_ Integer
_ -> BuiltinErrorCall -> Integer
forall a e. Exception e => e -> a
throw BuiltinErrorCall
BuiltinErrorCall)
(\()
_ Integer
_ Integer
_ -> ExBudget -> ExBudgetStream
ExBudgetLast (ExBudget -> ExBudgetStream) -> ExBudget -> ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExRestrictingBudget -> ExBudget
unExRestrictingBudget ExRestrictingBudget
enormousBudget)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
IsConstant =
(Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool)
-> (()
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool)
-> (cost
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool
forall a. Opaque val a -> Bool
isConstantPlc
()
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)) -> Bool))
ExBudgetStream
() -> Opaque val (TyVarRep ('TyNameRep "a" 0)) -> ExBudgetStream
forall a. Whatever a => a
whatever
where
isConstantPlc :: Opaque val a -> Bool
isConstantPlc :: forall a. Opaque val a -> Bool
isConstantPlc = Either BuiltinError (Some (ValueOf DefaultUni)) -> Bool
forall a b. Either a b -> Bool
isRight (Either BuiltinError (Some (ValueOf DefaultUni)) -> Bool)
-> (Opaque val a
-> Either BuiltinError (Some (ValueOf DefaultUni)))
-> Opaque val a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Opaque val a
-> Either BuiltinError (Some (ValueOf (UniOf (Opaque val a))))
Opaque val a -> Either BuiltinError (Some (ValueOf DefaultUni))
forall term.
HasConstant term =>
term -> Either BuiltinError (Some (ValueOf (UniOf term)))
asConstant
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
UnsafeCoerce =
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1)))
-> (cost
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))
forall a b. Opaque val a -> Opaque val b
unsafeCoercePlc
()
-> FoldArgs
(GetArgs
(Opaque val (TyVarRep ('TyNameRep "a" 0))
-> Opaque val (TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream
() -> Opaque val (TyVarRep ('TyNameRep "a" 0)) -> ExBudgetStream
forall a. Whatever a => a
whatever
where
unsafeCoercePlc :: Opaque val a -> Opaque val b
unsafeCoercePlc :: forall a b. Opaque val a -> Opaque val b
unsafeCoercePlc = val -> Opaque val b
forall val rep. val -> Opaque val rep
Opaque (val -> Opaque val b)
-> (Opaque val a -> val) -> Opaque val a -> Opaque val b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Opaque val a -> val
forall val rep. Opaque val rep -> val
unOpaque
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
UnsafeCoerceEl =
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)]))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)]))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])
forall a b.
SomeConstant DefaultUni [a]
-> BuiltinResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc
()
-> FoldArgs
(GetArgs
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> BuiltinResult
(SomeConstant DefaultUni [TyVarRep ('TyNameRep "b" 1)])))
ExBudgetStream
()
-> SomeConstant DefaultUni [TyVarRep ('TyNameRep "a" 0)]
-> ExBudgetStream
forall a. Whatever a => a
whatever
where
unsafeCoerceElPlc
:: SomeConstant DefaultUni [a] -> BuiltinResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc :: forall a b.
SomeConstant DefaultUni [a]
-> BuiltinResult (SomeConstant DefaultUni [b])
unsafeCoerceElPlc (SomeConstant (Some (ValueOf DefaultUni (Esc a)
uniList a
xs))) = do
DefaultUniList DefaultUni (Esc a1)
_ <- DefaultUni (Esc a) -> BuiltinResult (DefaultUni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DefaultUni (Esc a)
uniList
SomeConstant DefaultUni [b]
-> BuiltinResult (SomeConstant DefaultUni [b])
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant DefaultUni [b]
-> BuiltinResult (SomeConstant DefaultUni [b]))
-> SomeConstant DefaultUni [b]
-> BuiltinResult (SomeConstant DefaultUni [b])
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant DefaultUni [b]) (Esc a)
-> a -> SomeConstant DefaultUni [b]
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf UniOf (SomeConstant DefaultUni [b]) (Esc a)
DefaultUni (Esc a)
uniList a
xs
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Undefined =
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> (()
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
Opaque val (TyVarRep ('TyNameRep "a" 0))
-> (cost
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. HasCallStack => a
undefined
()
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Absurd =
(Void -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
-> FoldArgs
(GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(Void -> Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
-> FoldArgs
(GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))
forall a. Void -> a
absurd
()
-> FoldArgs
(GetArgs (Void -> Opaque val (TyVarRep ('TyNameRep "a" 0))))
ExBudgetStream
()
-> Void
-> FoldArgs
(GetArgs (Opaque val (TyVarRep ('TyNameRep "a" 0)))) ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
ErrorPrime =
BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (()
-> FoldArgs
(GetArgs
(BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))
-> (cost
-> FoldArgs
(GetArgs
(BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
(BuiltinResult a
forall {a}. BuiltinResult a
forall err. AsEvaluationFailure err => err
evaluationFailure :: forall a. BuiltinResult a)
() -> ExBudgetStream
()
-> FoldArgs
(GetArgs
(BuiltinResult (Opaque val (TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Comma =
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
forall a b.
SomeConstant uni a -> SomeConstant uni b -> SomeConstant uni (a, b)
commaPlc
()
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
ExBudgetStream
()
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
where
commaPlc
:: SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
commaPlc :: forall a b.
SomeConstant uni a -> SomeConstant uni b -> SomeConstant uni (a, b)
commaPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniA a
x))) (SomeConstant (Some (ValueOf uni (Esc a)
uniB a
y))) =
UniOf (SomeConstant uni (a, b)) (Esc (a, a))
-> (a, a) -> SomeConstant uni (a, b)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf (DefaultUni (Esc a) -> DefaultUni (Esc a) -> DefaultUni (Esc (a, a))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
{f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair uni (Esc a)
DefaultUni (Esc a)
uniA uni (Esc a)
DefaultUni (Esc a)
uniB) (a
x, a
y)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
BiconstPair =
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))
forall a b.
SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
biconstPairPlc
()
-> FoldArgs
(GetArgs
(SomeConstant uni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant uni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1)))))
ExBudgetStream
()
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0))
-> SomeConstant DefaultUni (TyVarRep ('TyNameRep "b" 1))
-> SomeConstant
DefaultUni
(TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
where
biconstPairPlc
:: SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
biconstPairPlc :: forall a b.
SomeConstant uni a
-> SomeConstant uni b
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
biconstPairPlc
(SomeConstant (Some (ValueOf uni (Esc a)
uniA a
x)))
(SomeConstant (Some (ValueOf uni (Esc a)
uniB a
y)))
(SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
_))) = do
DefaultUniPair DefaultUni (Esc a2)
uniA' DefaultUni (Esc a1)
uniB' <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
Just Esc a :~: Esc a2
Refl <- Maybe (Esc a :~: Esc a2)
-> BuiltinResult (Maybe (Esc a :~: Esc a2))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a2)
-> BuiltinResult (Maybe (Esc a :~: Esc a2)))
-> Maybe (Esc a :~: Esc a2)
-> BuiltinResult (Maybe (Esc a :~: Esc a2))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniA uni (Esc a) -> uni (Esc a2) -> Maybe (Esc a :~: Esc a2)
forall a b. uni a -> uni b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a2)
DefaultUni (Esc a2)
uniA'
Just Esc a :~: Esc a1
Refl <- Maybe (Esc a :~: Esc a1)
-> BuiltinResult (Maybe (Esc a :~: Esc a1))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Esc a :~: Esc a1)
-> BuiltinResult (Maybe (Esc a :~: Esc a1)))
-> Maybe (Esc a :~: Esc a1)
-> BuiltinResult (Maybe (Esc a :~: Esc a1))
forall a b. (a -> b) -> a -> b
$ uni (Esc a)
uniB uni (Esc a) -> uni (Esc a1) -> Maybe (Esc a :~: Esc a1)
forall a b. uni a -> uni b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` uni (Esc a1)
DefaultUni (Esc a1)
uniB'
SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (a, b))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b)))
-> SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (a, b))
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant uni (a, b)) (Esc (a, a))
-> (a, a) -> SomeConstant uni (a, b)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf uni (Esc a)
UniOf (SomeConstant uni (a, b)) (Esc (a, a))
uniPairAB (a
x, a
y)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
Swap =
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0))))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0))))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))
forall a b.
SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (b, a))
swapPlc
()
-> FoldArgs
(GetArgs
(SomeConstant
uni (TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> BuiltinResult
(SomeConstant
uni (TyVarRep ('TyNameRep "b" 1), TyVarRep ('TyNameRep "a" 0)))))
ExBudgetStream
()
-> SomeConstant
DefaultUni
(TyVarRep ('TyNameRep "a" 0), TyVarRep ('TyNameRep "b" 1))
-> ExBudgetStream
forall a. Whatever a => a
whatever
where
swapPlc
:: SomeConstant uni (a, b)
-> BuiltinResult (SomeConstant uni (b, a))
swapPlc :: forall a b.
SomeConstant uni (a, b) -> BuiltinResult (SomeConstant uni (b, a))
swapPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniPairAB a
p))) = do
DefaultUniPair DefaultUni (Esc a2)
uniA DefaultUni (Esc a1)
uniB <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniPairAB
SomeConstant uni (b, a) -> BuiltinResult (SomeConstant uni (b, a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni (b, a)
-> BuiltinResult (SomeConstant uni (b, a)))
-> SomeConstant uni (b, a)
-> BuiltinResult (SomeConstant uni (b, a))
forall a b. (a -> b) -> a -> b
$ UniOf (SomeConstant uni (b, a)) (Esc (a1, a2))
-> (a1, a2) -> SomeConstant uni (b, a)
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf (DefaultUni (Esc a1)
-> DefaultUni (Esc a2) -> DefaultUni (Esc (a1, a2))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
{f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair DefaultUni (Esc a1)
uniB DefaultUni (Esc a2)
uniA) ((a2, a1) -> a1
forall a b. (a, b) -> b
snd a
(a2, a1)
p, (a2, a1) -> a2
forall a b. (a, b) -> a
fst a
(a2, a1)
p)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_semvar ExtensionFun
SwapEls =
(SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))]))
-> (()
-> FoldArgs
(GetArgs
(SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
ExBudgetStream)
-> BuiltinMeaning val ()
forall cost.
(SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))]))
-> (cost
-> FoldArgs
(GetArgs
(SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
ExBudgetStream)
-> BuiltinMeaning val cost
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])
forall a.
SomeConstant uni [SomeConstant uni (a, Bool)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc
()
-> FoldArgs
(GetArgs
(SomeConstant
uni [SomeConstant uni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> BuiltinResult
(SomeConstant
uni [SomeConstant uni (Bool, TyVarRep ('TyNameRep "a" 0))])))
ExBudgetStream
()
-> SomeConstant
DefaultUni
[SomeConstant DefaultUni (TyVarRep ('TyNameRep "a" 0), Bool)]
-> ExBudgetStream
forall a. Whatever a => a
whatever
where
swapElsPlc
:: SomeConstant uni [SomeConstant uni (a, Bool)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc :: forall a.
SomeConstant uni [SomeConstant uni (a, Bool)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
swapElsPlc (SomeConstant (Some (ValueOf uni (Esc a)
uniList a
xs))) = do
DefaultUniList (DefaultUniPair DefaultUni (Esc a2)
uniA DefaultUni (Esc a1)
DefaultUniBool) <- uni (Esc a) -> BuiltinResult (uni (Esc a))
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure uni (Esc a)
uniList
let uniList' :: DefaultUni (Esc [(Bool, a2)])
uniList' = DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)])
forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList (DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)]))
-> DefaultUni (Esc (Bool, a2)) -> DefaultUni (Esc [(Bool, a2)])
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Bool)
-> DefaultUni (Esc a2) -> DefaultUni (Esc (Bool, a2))
forall {a} {k1} {k2} {f1 :: k1 -> k2} {a1 :: k1} {k3} {k4}
{f2 :: k3 -> k4} {a2 :: k3}.
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair DefaultUni (Esc Bool)
DefaultUniBool DefaultUni (Esc a2)
uniA
SomeConstant uni [SomeConstant uni (Bool, a)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall a. a -> BuiltinResult a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeConstant uni [SomeConstant uni (Bool, a)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)]))
-> ([(Bool, a2)] -> SomeConstant uni [SomeConstant uni (Bool, a)])
-> [(Bool, a2)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniOf
(SomeConstant uni [SomeConstant uni (Bool, a)]) (Esc [(Bool, a2)])
-> [(Bool, a2)] -> SomeConstant uni [SomeConstant uni (Bool, a)]
forall a term. HasConstant term => UniOf term (Esc a) -> a -> term
fromValueOf UniOf
(SomeConstant uni [SomeConstant uni (Bool, a)]) (Esc [(Bool, a2)])
DefaultUni (Esc [(Bool, a2)])
uniList' ([(Bool, a2)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)]))
-> [(Bool, a2)]
-> BuiltinResult (SomeConstant uni [SomeConstant uni (Bool, a)])
forall a b. (a -> b) -> a -> b
$ ((a2, Bool) -> (Bool, a2)) -> [(a2, Bool)] -> [(Bool, a2)]
forall a b. (a -> b) -> [a] -> [b]
map (a2, Bool) -> (Bool, a2)
forall a b. (a, b) -> (b, a)
swap a
[(a2, Bool)]
xs
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
semvar ExtensionFun
ExtensionVersion =
forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(() -> Integer)
(\()
_ -> case BuiltinSemanticsVariant ExtensionFun
semvar of
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant0 -> Integer
0
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant1 -> Integer
1
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant2 -> Integer
2
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant3 -> Integer
3
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant4 -> Integer
4)
() -> FoldArgs (GetArgs (() -> Integer)) ExBudgetStream
() -> () -> ExBudgetStream
forall a. Whatever a => a
whatever
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
_ ExtensionFun
TrackCosts = IO (BuiltinMeaning val ()) -> BuiltinMeaning val ()
forall a. IO a -> a
unsafePerformIO (IO (BuiltinMeaning val ()) -> BuiltinMeaning val ())
-> IO (BuiltinMeaning val ()) -> BuiltinMeaning val ()
forall a b. (a -> b) -> a -> b
$ do
MVar Integer
pendingGcVar <- Integer -> IO (MVar Integer)
forall a. a -> IO (MVar a)
newMVar Integer
0
MVar [Integer]
numsOfGcedVar <- [Integer] -> IO (MVar [Integer])
forall a. a -> IO (MVar a)
newMVar []
let
finalize :: IO ()
finalize =
MVar Integer -> IO (Maybe Integer)
forall a. MVar a -> IO (Maybe a)
tryTakeMVar MVar Integer
pendingGcVar IO (Maybe Integer) -> (Maybe Integer -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe Integer
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just Integer
pendingGc -> do
()
_ <- MVar [Integer] -> ([Integer] -> IO [Integer]) -> IO ()
forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ MVar [Integer]
numsOfGcedVar (([Integer] -> IO [Integer]) -> IO ())
-> ([Integer] -> IO [Integer]) -> IO ()
forall a b. (a -> b) -> a -> b
$ [Integer] -> IO [Integer]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Integer] -> IO [Integer])
-> ([Integer] -> [Integer]) -> [Integer] -> IO [Integer]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer
pendingGc Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
:)
MVar Integer -> Integer -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar Integer
pendingGcVar Integer
0
regBudget :: ExBudget -> IO ()
regBudget ExBudget
budget = do
Integer
pendingGc <- MVar Integer -> IO Integer
forall a. MVar a -> IO a
takeMVar MVar Integer
pendingGcVar
let pendingGc' :: Integer
pendingGc' = Integer -> Integer
forall a. Enum a => a -> a
succ Integer
pendingGc
MVar Integer -> Integer -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar Integer
pendingGcVar Integer
pendingGc'
ExBudget -> IO () -> IO ()
forall key. key -> IO () -> IO ()
addFinalizer ExBudget
budget IO ()
finalize
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
pendingGc' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
100) IO ()
performMinorGC
regBudgets :: ExBudgetStream -> IO ExBudgetStream
regBudgets (ExBudgetLast ExBudget
budget) = do
ExBudget -> IO ()
regBudget ExBudget
budget
IO ()
finalize
Integer
_ <- MVar Integer -> IO Integer
forall a. MVar a -> IO a
takeMVar MVar Integer
pendingGcVar
ExBudgetStream -> IO ExBudgetStream
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExBudgetStream -> IO ExBudgetStream)
-> ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudget -> ExBudgetStream
ExBudgetLast ExBudget
budget
regBudgets (ExBudgetCons ExBudget
budget ExBudgetStream
budgets) = do
ExBudget -> IO ()
regBudget ExBudget
budget
ExBudgetStream
budgets' <- IO ExBudgetStream -> IO ExBudgetStream
forall a. IO a -> IO a
unsafeInterleaveIO (IO ExBudgetStream -> IO ExBudgetStream)
-> IO ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudgetStream -> IO ExBudgetStream
regBudgets ExBudgetStream
budgets
ExBudgetStream -> IO ExBudgetStream
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExBudgetStream -> IO ExBudgetStream)
-> ExBudgetStream -> IO ExBudgetStream
forall a b. (a -> b) -> a -> b
$ ExBudget -> ExBudgetStream -> ExBudgetStream
ExBudgetCons ExBudget
budget ExBudgetStream
budgets'
linear1 :: ModelOneArgument
linear1 = OneVariableLinearFunction -> ModelOneArgument
ModelOneArgumentLinearInX (OneVariableLinearFunction -> ModelOneArgument)
-> OneVariableLinearFunction -> ModelOneArgument
forall a b. (a -> b) -> a -> b
$ Intercept -> Slope -> OneVariableLinearFunction
OneVariableLinearFunction Intercept
1 Slope
1
model :: CostingFun ModelOneArgument
model = ModelOneArgument -> ModelOneArgument -> CostingFun ModelOneArgument
forall model. model -> model -> CostingFun model
CostingFun ModelOneArgument
linear1 ModelOneArgument
linear1
BuiltinMeaning val () -> IO (BuiltinMeaning val ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BuiltinMeaning val () -> IO (BuiltinMeaning val ()))
-> BuiltinMeaning val () -> IO (BuiltinMeaning val ())
forall a b. (a -> b) -> a -> b
$ forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning
@(Data -> [Integer])
(\Data
_ -> IO [Integer] -> [Integer]
forall a. IO a -> a
unsafePerformIO (IO [Integer] -> [Integer]) -> IO [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [Integer]
forall a. [a] -> [a]
reverse ([Integer] -> [Integer]) -> IO [Integer] -> IO [Integer]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MVar [Integer] -> IO [Integer]
forall a. MVar a -> IO a
readMVar MVar [Integer]
numsOfGcedVar)
(\()
_ -> IO ExBudgetStream -> ExBudgetStream
forall a. IO a -> a
unsafePerformIO (IO ExBudgetStream -> ExBudgetStream)
-> (Data -> IO ExBudgetStream) -> Data -> ExBudgetStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExBudgetStream -> IO ExBudgetStream
regBudgets (ExBudgetStream -> IO ExBudgetStream)
-> (Data -> ExBudgetStream) -> Data -> IO ExBudgetStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostingFun ModelOneArgument -> Data -> ExBudgetStream
forall a1.
ExMemoryUsage a1 =>
CostingFun ModelOneArgument -> a1 -> ExBudgetStream
runCostingFunOneArgument CostingFun ModelOneArgument
model)
toBuiltinMeaning BuiltinSemanticsVariant ExtensionFun
semvar ExtensionFun
IntNoIntegerNoWord =
case BuiltinSemanticsVariant ExtensionFun
semvar of
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant0 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Int -> ()) Int -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Int -> ())) ExBudgetStream
() -> Int -> ExBudgetStream
forall a. Whatever a => a
whatever
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant1 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Integer -> ()) Integer -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Integer -> ())) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant2 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Integer -> ()) Integer -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Integer -> ())) ExBudgetStream
() -> Integer -> ExBudgetStream
forall a. Whatever a => a
whatever
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant3 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Word -> ()) Word -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Word -> ())) ExBudgetStream
() -> Word -> ExBudgetStream
forall a. Whatever a => a
whatever
BuiltinSemanticsVariant ExtensionFun
R:BuiltinSemanticsVariantExtensionFun
ExtensionFunSemanticsVariant4 -> forall a val cost.
MakeBuiltinMeaning a val =>
a
-> (cost -> FoldArgs (GetArgs a) ExBudgetStream)
-> BuiltinMeaning val cost
makeBuiltinMeaning @(Word -> ()) Word -> ()
forall a. Monoid a => a
mempty () -> FoldArgs (GetArgs (Word -> ())) ExBudgetStream
() -> Word -> ExBudgetStream
forall a. Whatever a => a
whatever
instance Default (BuiltinSemanticsVariant ExtensionFun) where
def :: BuiltinSemanticsVariant ExtensionFun
def = BuiltinSemanticsVariant ExtensionFun
forall a. Bounded a => a
maxBound