{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}
{-# OPTIONS -Wno-missing-signatures #-}
{-# OPTIONS -Wno-redundant-constraints #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#include "MachDeps.h"
{-# OPTIONS_GHC -O2 #-}
module PlutusCore.Default.Universe
( DefaultUni (..)
, pattern DefaultUniList
, pattern DefaultUniPair
, noMoreTypeFunctions
, module Export
) where
import PlutusPrelude
import PlutusCore.Builtin
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
import PlutusCore.Data
import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
ListCostedByLength (..),
NumBytesCostedAsNumWords (..))
import PlutusCore.Pretty.Extra
import Data.ByteString (ByteString)
import Data.Int
import Data.Proxy
import Data.Text (Text)
import Data.Text qualified as Text
import Data.Typeable (typeRep)
import Data.Word
import GHC.Exts (inline, oneShot)
import Text.PrettyBy.Fixity
import Universe as Export
data DefaultUni a where
DefaultUniInteger :: DefaultUni (Esc Integer)
DefaultUniByteString :: DefaultUni (Esc ByteString)
DefaultUniString :: DefaultUni (Esc Text)
DefaultUniUnit :: DefaultUni (Esc ())
DefaultUniBool :: DefaultUni (Esc Bool)
DefaultUniProtoList :: DefaultUni (Esc [])
DefaultUniProtoPair :: DefaultUni (Esc (,))
DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
DefaultUniData :: DefaultUni (Esc Data)
DefaultUniBLS12_381_G1_Element :: DefaultUni (Esc BLS12_381.G1.Element)
DefaultUniBLS12_381_G2_Element :: DefaultUni (Esc BLS12_381.G2.Element)
DefaultUniBLS12_381_MlResult :: DefaultUni (Esc BLS12_381.Pairing.MlResult)
pattern $mDefaultUniList :: forall {r} {a}.
DefaultUni a
-> (forall {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> r)
-> ((# #) -> r)
-> r
$bDefaultUniList :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList uniA =
DefaultUniProtoList `DefaultUniApply` uniA
pattern $mDefaultUniPair :: forall {r} {a}.
DefaultUni a
-> (forall {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) -> r)
-> ((# #) -> r)
-> r
$bDefaultUniPair :: 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 uniA uniB =
DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB
instance GEq DefaultUni where
geq :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geq = DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqStep where
geqStep :: DefaultUni a1 -> DefaultUni a2 -> Maybe (a1 :~: a2)
geqStep :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqStep DefaultUni a1
DefaultUniInteger DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniInteger <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniByteString DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniByteString <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniString DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniString <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniUnit DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniUnit <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniBool DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniBool <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniProtoList DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniProtoList <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniProtoPair DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniProtoPair <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep (DefaultUniApply DefaultUni (Esc f)
f1 DefaultUni (Esc a)
x1) DefaultUni a2
a2 = do
DefaultUniApply DefaultUni (Esc f)
f2 DefaultUni (Esc a)
x2 <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
Esc f :~: Esc f
Refl <- DefaultUni (Esc f) -> DefaultUni (Esc f) -> Maybe (Esc f :~: Esc f)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqRec DefaultUni (Esc f)
f1 DefaultUni (Esc f)
f2
Esc a :~: Esc a
Refl <- DefaultUni (Esc a) -> DefaultUni (Esc a) -> Maybe (Esc a :~: Esc a)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqRec DefaultUni (Esc a)
x1 DefaultUni (Esc a)
x2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniData DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniData <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniBLS12_381_G1_Element DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniBLS12_381_G1_Element <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniBLS12_381_G2_Element DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniBLS12_381_G2_Element <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
geqStep DefaultUni a1
DefaultUniBLS12_381_MlResult DefaultUni a2
a2 = do
DefaultUni a2
DefaultUniBLS12_381_MlResult <- DefaultUni a2 -> Maybe (DefaultUni a2)
forall a. a -> Maybe a
Just DefaultUni a2
a2
(a1 :~: a2) -> Maybe (a1 :~: a2)
forall a. a -> Maybe a
Just a1 :~: a1
a1 :~: a2
forall {k} (a :: k). a :~: a
Refl
{-# INLINE geqStep #-}
geqRec :: DefaultUni a1 -> DefaultUni a2 -> Maybe (a1 :~: a2)
geqRec :: forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqRec = DefaultUni a1 -> DefaultUni a2 -> Maybe (a1 :~: a2)
forall a b. DefaultUni a -> DefaultUni b -> Maybe (a :~: b)
geqStep
{-# OPAQUE geqRec #-}
noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d)) -> any
noMoreTypeFunctions :: forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a)
_) = DefaultUni (Esc f) -> any
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
instance ToKind DefaultUni where
toSingKind :: forall k (a :: k). DefaultUni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc a)
DefaultUniInteger = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniByteString = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniString = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniUnit = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniBool = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniProtoList = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniProtoPair = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind (DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
_) = case DefaultUni (Esc f) -> SingKind (k -> k)
forall k (a :: k). DefaultUni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc f)
uniF of SingKind k1
_ `SingKindArrow` SingKind l
cod -> SingKind k
SingKind l
cod
toSingKind DefaultUni (Esc a)
DefaultUniData = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element = SingKind k
forall k. KnownKind k => SingKind k
knownKind
toSingKind DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult = SingKind k
forall k. KnownKind k => SingKind k
knownKind
instance HasUniApply DefaultUni where
uniApply :: forall {k} {k} (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
uniApply = DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
forall {k} {k} (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
DefaultUniApply
matchUniApply :: forall tb r.
DefaultUni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r)
-> r
matchUniApply (DefaultUniApply DefaultUni (Esc f)
f DefaultUni (Esc a)
a) r
_ forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
h = DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
h DefaultUni (Esc f)
f DefaultUni (Esc a)
a
matchUniApply DefaultUni tb
_ r
z forall k l (f :: k -> l) (a :: k).
(tb ~ Esc (f a)) =>
DefaultUni (Esc f) -> DefaultUni (Esc a) -> r
_ = r
z
deriving stock instance Show (DefaultUni a)
instance GShow DefaultUni where gshowsPrec :: forall a. Int -> DefaultUni a -> ShowS
gshowsPrec = Int -> DefaultUni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance PrettyBy RenderContext (DefaultUni a) where
prettyBy :: forall ann. RenderContext -> DefaultUni a -> Doc ann
prettyBy = (DefaultUni a -> InContextM RenderContext (Doc ann))
-> RenderContext -> DefaultUni a -> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((DefaultUni a -> InContextM RenderContext (Doc ann))
-> RenderContext -> DefaultUni a -> Doc ann)
-> (DefaultUni a -> InContextM RenderContext (Doc ann))
-> RenderContext
-> DefaultUni a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
DefaultUni a
DefaultUniInteger -> InContextM RenderContext (Doc ann)
"integer"
DefaultUni a
DefaultUniByteString -> InContextM RenderContext (Doc ann)
"bytestring"
DefaultUni a
DefaultUniString -> InContextM RenderContext (Doc ann)
"string"
DefaultUni a
DefaultUniUnit -> InContextM RenderContext (Doc ann)
"unit"
DefaultUni a
DefaultUniBool -> InContextM RenderContext (Doc ann)
"bool"
DefaultUni a
DefaultUniProtoList -> InContextM RenderContext (Doc ann)
"list"
DefaultUni a
DefaultUniProtoPair -> InContextM RenderContext (Doc ann)
"pair"
DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
uniA -> DefaultUni (Esc f)
uniF DefaultUni (Esc f)
-> DefaultUni (Esc a) -> InContextM RenderContext (Doc ann)
forall config env (m :: * -> *) a b ann.
(MonadPrettyContext config env m, PrettyBy config a,
PrettyBy config b) =>
a -> b -> m (Doc ann)
`juxtPrettyM` DefaultUni (Esc a)
uniA
DefaultUni a
DefaultUniData -> InContextM RenderContext (Doc ann)
"data"
DefaultUni a
DefaultUniBLS12_381_G1_Element -> InContextM RenderContext (Doc ann)
"bls12_381_G1_element"
DefaultUni a
DefaultUniBLS12_381_G2_Element -> InContextM RenderContext (Doc ann)
"bls12_381_G2_element"
DefaultUni a
DefaultUniBLS12_381_MlResult -> InContextM RenderContext (Doc ann)
"bls12_381_mlresult"
instance PrettyBy RenderContext (SomeTypeIn DefaultUni) where
prettyBy :: forall ann. RenderContext -> SomeTypeIn DefaultUni -> Doc ann
prettyBy RenderContext
config (SomeTypeIn DefaultUni (Esc a)
uni) = RenderContext -> DefaultUni (Esc a) -> Doc ann
forall ann. RenderContext -> DefaultUni (Esc a) -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy RenderContext
config DefaultUni (Esc a)
uni
instance Pretty (DefaultUni a) where
pretty :: forall ann. DefaultUni a -> Doc ann
pretty = RenderContext -> DefaultUni a -> Doc ann
forall ann. RenderContext -> DefaultUni a -> Doc ann
forall config a ann. PrettyBy config a => config -> a -> Doc ann
prettyBy RenderContext
juxtRenderContext
instance Pretty (SomeTypeIn DefaultUni) where
pretty :: forall ann. SomeTypeIn DefaultUni -> Doc ann
pretty (SomeTypeIn DefaultUni (Esc a)
uni) = DefaultUni (Esc a) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. DefaultUni (Esc a) -> Doc ann
pretty DefaultUni (Esc a)
uni
type ElaborateBuiltinDefaultUni :: forall a. a -> a
type family ElaborateBuiltinDefaultUni x where
ElaborateBuiltinDefaultUni (f x) = ElaborateBuiltinDefaultUni f `TyAppRep` x
ElaborateBuiltinDefaultUni x = BuiltinHead x
type instance ElaborateBuiltin DefaultUni x = ElaborateBuiltinDefaultUni x
instance (DefaultUni `Contains` f, DefaultUni `Contains` a) => DefaultUni `Contains` f a where
knownUni :: DefaultUni (Esc (f a))
knownUni = DefaultUni (Esc f)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
forall {k} {k} (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
`DefaultUniApply` DefaultUni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni
instance DefaultUni `Contains` Integer where
knownUni :: DefaultUni (Esc Integer)
knownUni = DefaultUni (Esc Integer)
DefaultUniInteger
instance DefaultUni `Contains` ByteString where
knownUni :: DefaultUni (Esc ByteString)
knownUni = DefaultUni (Esc ByteString)
DefaultUniByteString
instance DefaultUni `Contains` Text where
knownUni :: DefaultUni (Esc Text)
knownUni = DefaultUni (Esc Text)
DefaultUniString
instance DefaultUni `Contains` () where
knownUni :: DefaultUni (Esc ())
knownUni = DefaultUni (Esc ())
DefaultUniUnit
instance DefaultUni `Contains` Bool where
knownUni :: DefaultUni (Esc Bool)
knownUni = DefaultUni (Esc Bool)
DefaultUniBool
instance DefaultUni `Contains` [] where
knownUni :: DefaultUni (Esc [])
knownUni = DefaultUni (Esc [])
DefaultUniProtoList
instance DefaultUni `Contains` (,) where
knownUni :: DefaultUni (Esc (,))
knownUni = DefaultUni (Esc (,))
DefaultUniProtoPair
instance DefaultUni `Contains` Data where
knownUni :: DefaultUni (Esc Data)
knownUni = DefaultUni (Esc Data)
DefaultUniData
instance DefaultUni `Contains` BLS12_381.G1.Element where
knownUni :: DefaultUni (Esc Element)
knownUni = DefaultUni (Esc Element)
DefaultUniBLS12_381_G1_Element
instance DefaultUni `Contains` BLS12_381.G2.Element where
knownUni :: DefaultUni (Esc Element)
knownUni = DefaultUni (Esc Element)
DefaultUniBLS12_381_G2_Element
instance DefaultUni `Contains` BLS12_381.Pairing.MlResult where
knownUni :: DefaultUni (Esc MlResult)
knownUni = DefaultUni (Esc MlResult)
DefaultUniBLS12_381_MlResult
instance KnownBuiltinTypeAst tyname DefaultUni Integer =>
KnownTypeAst tyname DefaultUni Integer
instance KnownBuiltinTypeAst tyname DefaultUni ByteString =>
KnownTypeAst tyname DefaultUni ByteString
instance KnownBuiltinTypeAst tyname DefaultUni Text =>
KnownTypeAst tyname DefaultUni Text
instance KnownBuiltinTypeAst tyname DefaultUni () =>
KnownTypeAst tyname DefaultUni ()
instance KnownBuiltinTypeAst tyname DefaultUni Bool =>
KnownTypeAst tyname DefaultUni Bool
instance KnownBuiltinTypeAst tyname DefaultUni [a] =>
KnownTypeAst tyname DefaultUni [a]
instance KnownBuiltinTypeAst tyname DefaultUni (a, b) =>
KnownTypeAst tyname DefaultUni (a, b)
instance KnownBuiltinTypeAst tyname DefaultUni Data =>
KnownTypeAst tyname DefaultUni Data
instance KnownBuiltinTypeAst tyname DefaultUni BLS12_381.G1.Element =>
KnownTypeAst tyname DefaultUni BLS12_381.G1.Element
instance KnownBuiltinTypeAst tyname DefaultUni BLS12_381.G2.Element =>
KnownTypeAst tyname DefaultUni BLS12_381.G2.Element
instance KnownBuiltinTypeAst tyname DefaultUni BLS12_381.Pairing.MlResult =>
KnownTypeAst tyname DefaultUni BLS12_381.Pairing.MlResult
instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Integer
instance KnownBuiltinTypeIn DefaultUni term ByteString =>
ReadKnownIn DefaultUni term ByteString
instance KnownBuiltinTypeIn DefaultUni term Text =>
ReadKnownIn DefaultUni term Text
instance KnownBuiltinTypeIn DefaultUni term () =>
ReadKnownIn DefaultUni term ()
instance KnownBuiltinTypeIn DefaultUni term Bool =>
ReadKnownIn DefaultUni term Bool
instance KnownBuiltinTypeIn DefaultUni term Data =>
ReadKnownIn DefaultUni term Data
instance KnownBuiltinTypeIn DefaultUni term [a] =>
ReadKnownIn DefaultUni term [a]
instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
ReadKnownIn DefaultUni term (a, b)
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
ReadKnownIn DefaultUni term BLS12_381.G1.Element
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G2.Element =>
ReadKnownIn DefaultUni term BLS12_381.G2.Element
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.Pairing.MlResult =>
ReadKnownIn DefaultUni term BLS12_381.Pairing.MlResult
instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Integer
instance KnownBuiltinTypeIn DefaultUni term ByteString =>
MakeKnownIn DefaultUni term ByteString
instance KnownBuiltinTypeIn DefaultUni term Text =>
MakeKnownIn DefaultUni term Text
instance KnownBuiltinTypeIn DefaultUni term () =>
MakeKnownIn DefaultUni term ()
instance KnownBuiltinTypeIn DefaultUni term Bool =>
MakeKnownIn DefaultUni term Bool
instance KnownBuiltinTypeIn DefaultUni term Data =>
MakeKnownIn DefaultUni term Data
instance KnownBuiltinTypeIn DefaultUni term [a] =>
MakeKnownIn DefaultUni term [a]
instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
MakeKnownIn DefaultUni term (a, b)
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
MakeKnownIn DefaultUni term BLS12_381.G1.Element
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G2.Element =>
MakeKnownIn DefaultUni term BLS12_381.G2.Element
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.Pairing.MlResult =>
MakeKnownIn DefaultUni term BLS12_381.Pairing.MlResult
instance TestTypesFromTheUniverseAreAllKnown DefaultUni
newtype AsInteger a = AsInteger
{ forall a. AsInteger a -> a
unAsInteger :: a
}
instance KnownTypeAst tyname DefaultUni (AsInteger a) where
type IsBuiltin _ _ = 'False
type ToHoles _ _ = '[]
type ToBinds _ acc _ = acc
typeAst :: Type tyname DefaultUni ()
typeAst = Proxy Integer -> Type tyname DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst (Proxy Integer -> Type tyname DefaultUni ())
-> Proxy Integer -> Type tyname DefaultUni ()
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Integer
instance (KnownBuiltinTypeIn DefaultUni term Integer, Integral a) =>
MakeKnownIn DefaultUni term (AsInteger a) where
makeKnown :: AsInteger a -> BuiltinResult term
makeKnown = Integer -> BuiltinResult term
forall (uni :: * -> *) val a.
MakeKnownIn uni val a =>
a -> BuiltinResult val
makeKnown (Integer -> BuiltinResult term)
-> (AsInteger a -> Integer) -> AsInteger a -> BuiltinResult term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger (a -> Integer) -> (AsInteger a -> a) -> AsInteger a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsInteger a -> a
forall a. AsInteger a -> a
unAsInteger
{-# INLINE makeKnown #-}
instance (KnownBuiltinTypeIn DefaultUni term Integer, Integral a, Bounded a, Typeable a) =>
ReadKnownIn DefaultUni term (AsInteger a) where
readKnown :: term -> ReadKnownM (AsInteger a)
readKnown term
term =
(term -> ReadKnownM Integer) -> term -> ReadKnownM Integer
forall a. a -> a
inline term -> ReadKnownM Integer
forall val a. KnownBuiltinType val a => val -> ReadKnownM a
readKnownConstant term
term ReadKnownM Integer
-> (Integer -> ReadKnownM (AsInteger a))
-> ReadKnownM (AsInteger a)
forall a b.
Either BuiltinError a
-> (a -> Either BuiltinError b) -> Either BuiltinError b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Integer -> ReadKnownM (AsInteger a))
-> Integer -> ReadKnownM (AsInteger a)
forall a b. (a -> b) -> a -> b
oneShot \(Integer
i :: Integer) ->
if a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
forall a. Bounded a => a
minBound :: a) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a
forall a. Bounded a => a
maxBound :: a)
then AsInteger a -> ReadKnownM (AsInteger a)
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AsInteger a -> ReadKnownM (AsInteger a))
-> (a -> AsInteger a) -> a -> ReadKnownM (AsInteger a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AsInteger a
forall a. a -> AsInteger a
AsInteger (a -> ReadKnownM (AsInteger a)) -> a -> ReadKnownM (AsInteger a)
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
else AReview BuiltinError UnliftingError
-> UnliftingError -> ReadKnownM (AsInteger a)
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
_OperationalUnliftingError (UnliftingError -> ReadKnownM (AsInteger a))
-> (Text -> UnliftingError) -> Text -> ReadKnownM (AsInteger a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> UnliftingError
MkUnliftingError (Text -> ReadKnownM (AsInteger a))
-> Text -> ReadKnownM (AsInteger a)
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
[ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
i
, Text
" is not within the bounds of "
, String -> Text
Text.pack (String -> Text) -> (Proxy a -> String) -> Proxy a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRep -> String
forall a. Show a => a -> String
show (TypeRep -> String) -> (Proxy a -> TypeRep) -> Proxy a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a -> Text) -> Proxy a -> Text
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a
]
{-# INLINE readKnown #-}
#if WORD_SIZE_IN_BITS == 64
deriving via AsInteger Int instance
KnownTypeAst tyname DefaultUni Int
deriving via AsInteger Int instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Int
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Int where
readKnown :: term -> ReadKnownM Int
readKnown term
term = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int64 @Int (Int64 -> Int) -> Either BuiltinError Int64 -> ReadKnownM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Either BuiltinError Int64
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown term
term
{-# INLINE readKnown #-}
deriving via AsInteger Word instance
KnownTypeAst tyname DefaultUni Word
deriving via AsInteger Word instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Word
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Word where
readKnown :: term -> ReadKnownM Word
readKnown term
term = forall a b. (Integral a, Num b) => a -> b
fromIntegral @Word64 @Word (Word64 -> Word) -> Either BuiltinError Word64 -> ReadKnownM Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> term -> Either BuiltinError Word64
forall (uni :: * -> *) val a.
ReadKnownIn uni val a =>
val -> ReadKnownM a
readKnown term
term
{-# INLINE readKnown #-}
#endif
deriving via AsInteger Int8 instance
KnownTypeAst tyname DefaultUni Int8
deriving via AsInteger Int8 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Int8
deriving via AsInteger Int8 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Int8
deriving via AsInteger Int16 instance
KnownTypeAst tyname DefaultUni Int16
deriving via AsInteger Int16 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Int16
deriving via AsInteger Int16 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Int16
deriving via AsInteger Int32 instance
KnownTypeAst tyname DefaultUni Int32
deriving via AsInteger Int32 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Int32
deriving via AsInteger Int32 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Int32
deriving via AsInteger Int64 instance
KnownTypeAst tyname DefaultUni Int64
deriving via AsInteger Int64 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Int64
deriving via AsInteger Int64 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Int64
deriving via AsInteger Word8 instance
KnownTypeAst tyname DefaultUni Word8
deriving via AsInteger Word8 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Word8
deriving via AsInteger Word8 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Word8
deriving via AsInteger Word16 instance
KnownTypeAst tyname DefaultUni Word16
deriving via AsInteger Word16 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Word16
deriving via AsInteger Word16 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Word16
deriving via AsInteger Word32 instance
KnownTypeAst tyname DefaultUni Word32
deriving via AsInteger Word32 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Word32
deriving via AsInteger Word32 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Word32
deriving via AsInteger Word64 instance
KnownTypeAst tyname DefaultUni Word64
deriving via AsInteger Word64 instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Word64
deriving via AsInteger Word64 instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term Word64
deriving newtype instance
KnownTypeAst tyname DefaultUni NumBytesCostedAsNumWords
deriving newtype instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term NumBytesCostedAsNumWords
deriving newtype instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term NumBytesCostedAsNumWords
deriving newtype instance
KnownTypeAst tyname DefaultUni IntegerCostedLiterally
deriving newtype instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term IntegerCostedLiterally
deriving newtype instance KnownBuiltinTypeIn DefaultUni term Integer =>
ReadKnownIn DefaultUni term IntegerCostedLiterally
deriving newtype instance KnownTypeAst tyname DefaultUni a =>
KnownTypeAst tyname DefaultUni (ListCostedByLength a)
deriving newtype instance KnownBuiltinTypeIn DefaultUni term [a] =>
MakeKnownIn DefaultUni term (ListCostedByLength a)
deriving newtype instance KnownBuiltinTypeIn DefaultUni term [a] =>
ReadKnownIn DefaultUni term (ListCostedByLength a)
deriving via AsInteger Natural instance
KnownTypeAst tyname DefaultUni Natural
deriving via AsInteger Natural instance KnownBuiltinTypeIn DefaultUni term Integer =>
MakeKnownIn DefaultUni term Natural
instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni term Natural where
readKnown :: term -> ReadKnownM Natural
readKnown term
term =
(term -> ReadKnownM Integer) -> term -> ReadKnownM Integer
forall a. a -> a
inline term -> ReadKnownM Integer
forall val a. KnownBuiltinType val a => val -> ReadKnownM a
readKnownConstant term
term ReadKnownM Integer
-> (Integer -> ReadKnownM Natural) -> ReadKnownM Natural
forall a b.
Either BuiltinError a
-> (a -> Either BuiltinError b) -> Either BuiltinError b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Integer -> ReadKnownM Natural) -> Integer -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
oneShot \(Integer
i :: Integer) ->
if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
then Natural -> ReadKnownM Natural
forall a. a -> Either BuiltinError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Natural -> ReadKnownM Natural) -> Natural -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i
else AReview BuiltinError UnliftingError
-> UnliftingError -> ReadKnownM Natural
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
_OperationalUnliftingError (UnliftingError -> ReadKnownM Natural)
-> (Text -> UnliftingError) -> Text -> ReadKnownM Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> UnliftingError
MkUnliftingError (Text -> ReadKnownM Natural) -> Text -> ReadKnownM Natural
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
[ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
i
, Text
" is not within the bounds of Natural"
]
{-# INLINE readKnown #-}
instance Closed DefaultUni where
type DefaultUni `Everywhere` constr =
( constr `Permits` Integer
, constr `Permits` ByteString
, constr `Permits` Text
, constr `Permits` ()
, constr `Permits` Bool
, constr `Permits` []
, constr `Permits` (,)
, constr `Permits` Data
, constr `Permits` BLS12_381.G1.Element
, constr `Permits` BLS12_381.G2.Element
, constr `Permits` BLS12_381.Pairing.MlResult
)
encodeUni :: forall a. DefaultUni a -> [Int]
encodeUni DefaultUni a
DefaultUniInteger = [Int
0]
encodeUni DefaultUni a
DefaultUniByteString = [Int
1]
encodeUni DefaultUni a
DefaultUniString = [Int
2]
encodeUni DefaultUni a
DefaultUniUnit = [Int
3]
encodeUni DefaultUni a
DefaultUniBool = [Int
4]
encodeUni DefaultUni a
DefaultUniProtoList = [Int
5]
encodeUni DefaultUni a
DefaultUniProtoPair = [Int
6]
encodeUni (DefaultUniApply DefaultUni (Esc f)
uniF DefaultUni (Esc a)
uniA) = Int
7 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: DefaultUni (Esc f) -> [Int]
forall a. DefaultUni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc f)
uniF [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a) -> [Int]
forall a. DefaultUni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc a)
uniA
encodeUni DefaultUni a
DefaultUniData = [Int
8]
encodeUni DefaultUni a
DefaultUniBLS12_381_G1_Element = [Int
9]
encodeUni DefaultUni a
DefaultUniBLS12_381_G2_Element = [Int
10]
encodeUni DefaultUni a
DefaultUniBLS12_381_MlResult = [Int
11]
withDecodedUni :: forall r.
(forall k (a :: k).
Typeable k =>
DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k = DecodeUniM Int
peelUniTag DecodeUniM Int -> (Int -> DecodeUniM r) -> DecodeUniM r
forall a b. DecodeUniM a -> (a -> DecodeUniM b) -> DecodeUniM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Int
0 -> DefaultUni (Esc Integer) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Integer)
DefaultUniInteger
Int
1 -> DefaultUni (Esc ByteString) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc ByteString)
DefaultUniByteString
Int
2 -> DefaultUni (Esc Text) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Text)
DefaultUniString
Int
3 -> DefaultUni (Esc ()) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc ())
DefaultUniUnit
Int
4 -> DefaultUni (Esc Bool) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Bool)
DefaultUniBool
Int
5 -> DefaultUni (Esc []) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc [])
DefaultUniProtoList
Int
6 -> DefaultUni (Esc (,)) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc (,))
DefaultUniProtoPair
Int
7 ->
forall (uni :: * -> *) r.
Closed uni =>
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni @DefaultUni ((forall k (a :: k).
Typeable k =>
DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r)
-> (forall k (a :: k).
Typeable k =>
DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ \DefaultUni (Esc a)
uniF ->
forall (uni :: * -> *) r.
Closed uni =>
(forall k (a :: k). Typeable k => uni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
withDecodedUni @DefaultUni ((forall k (a :: k).
Typeable k =>
DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r)
-> (forall k (a :: k).
Typeable k =>
DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ \DefaultUni (Esc a)
uniA ->
DefaultUni (Esc a)
-> DefaultUni (Esc a)
-> (forall {b}. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
-> DecodeUniM r
forall a ab (f :: ab) (x :: a) (uni :: * -> *) (m :: * -> *) r.
(Typeable ab, Typeable a, MonadPlus m) =>
uni (Esc f)
-> uni (Esc x)
-> (forall b. (Typeable b, ab ~ (a -> b)) => m r)
-> m r
withApplicable DefaultUni (Esc a)
uniF DefaultUni (Esc a)
uniA ((forall {b}. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
-> DecodeUniM r)
-> (forall {b}. (Typeable b, k ~ (k -> b)) => DecodeUniM r)
-> DecodeUniM r
forall a b. (a -> b) -> a -> b
$
DefaultUni (Esc (a a)) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k (DefaultUni (Esc (a a)) -> DecodeUniM r)
-> DefaultUni (Esc (a a)) -> DecodeUniM r
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a)
DefaultUni (Esc a)
uniF DefaultUni (Esc a) -> DefaultUni (Esc a) -> DefaultUni (Esc (a a))
forall {k} {k} (f :: k -> k) (a :: k).
DefaultUni (Esc f) -> DefaultUni (Esc a) -> DefaultUni (Esc (f a))
`DefaultUniApply` DefaultUni (Esc a)
uniA
Int
8 -> DefaultUni (Esc Data) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Data)
DefaultUniData
Int
9 -> DefaultUni (Esc Element) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Element)
DefaultUniBLS12_381_G1_Element
Int
10 -> DefaultUni (Esc Element) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Element)
DefaultUniBLS12_381_G2_Element
Int
11 -> DefaultUni (Esc MlResult) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc MlResult)
DefaultUniBLS12_381_MlResult
Int
_ -> DecodeUniM r
forall a. DecodeUniM a
forall (f :: * -> *) a. Alternative f => f a
empty
bring
:: forall constr a r proxy. DefaultUni `Everywhere` constr
=> proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring :: forall (constr :: * -> Constraint) a r
(proxy :: (* -> Constraint) -> *).
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniInteger constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniByteString constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniString constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniUnit constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBool constr a => r
r = r
constr a => r
r
bring proxy constr
p (DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a)
uniA) constr a => r
r =
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA r
constr a => r
constr a => r
r
bring proxy constr
p (DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
uniA `DefaultUniApply` DefaultUni (Esc a)
uniB) constr a => r
r =
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA ((constr a => r) -> r) -> (constr a => r) -> r
forall a b. (a -> b) -> a -> b
$ proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
forall (uni :: * -> *) (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
(proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniB r
constr a => r
constr a => r
r
bring proxy constr
_ (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_) constr a => r
_ =
DefaultUni (Esc f) -> r
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniData constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element constr a => r
r = r
constr a => r
r
bring proxy constr
_ DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult constr a => r
r = r
constr a => r
r