{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}
-- on 9.2.4 this is the flag that suppresses the above warning
{-# OPTIONS -Wno-missing-signatures #-}
-- 9.6 notices that all the constraints on 'TestTypesFromTheUniverseAreAllKnown'
-- are redundant (which they are), but we don't care because it only exists
-- to test that some constraints are solvable
{-# OPTIONS -Wno-redundant-constraints #-}

{-# LANGUAGE BangPatterns             #-}
{-# 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 TupleSections            #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
#include "MachDeps.h"

-- effectfully: to the best of my experimentation, -O2 here improves
-- performance, but it's not clear why. This needs to be investigated.
{-# OPTIONS_GHC -O2 #-}

-- | The universe used by default and its instances.
module PlutusCore.Default.Universe
    ( DefaultUni (..)
    , pattern DefaultUniList
    , pattern DefaultUniArray
    , pattern DefaultUniPair
    , noMoreTypeFunctions
    , module Export  -- Re-exporting universes infrastructure for convenience.
    ) where

import PlutusCore.Builtin
import PlutusPrelude

import PlutusCore.Core.Type (Type (..))
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 (Data)
import PlutusCore.Evaluation.Machine.ExMemoryUsage (IntegerCostedLiterally (..),
                                                    NumBytesCostedAsNumWords (..))
import PlutusCore.Pretty.Extra (juxtRenderContext)

import Control.Monad.Except (throwError)
import Data.ByteString (ByteString)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Proxy (Proxy (Proxy))
import Data.Text (Text)
import Data.Text qualified as Text
import Data.Typeable (typeRep)
import Data.Vector qualified as Vector
import Data.Vector.Strict qualified as Strict (Vector)
import Data.Word (Word16, Word32, Word64)
import GHC.Exts (inline, oneShot)
import Text.PrettyBy.Fixity (RenderContext, inContextM, juxtPrettyM)
import Universe as Export

{- Note [PLC types and universes]
We encode built-in types in PLC as tags for Haskell types (the latter are also called meta-types),
see Note [Universes]. A built-in type in PLC is an inhabitant of

    Some (TypeIn uni)

where @uni@ is some universe, i.e. a collection of tags that have meta-types associated with them.

A value of a built-in type is a regular Haskell value stored in

    Some (ValueOf uni)

(together with the tag associated with its type) and such a value is also called a meta-constant.

The default universe has the following constructor (pattern synonym actually):

    DefaultUniList :: !(DefaultUni a) -> DefaultUni [a]

But note that this doesn't directly lead to interop between Plutus Core and Haskell, i.e. you can't
have a meta-list whose elements are of a PLC type. You can only have a meta-list constant with
elements of a meta-type (i.e. a type from the universe).

However it is possible to apply a built-in type to an arbitrary PLC/PIR type, since we can embed
a type of an arbitrary kind into 'Type' and then apply it via 'TyApp'. But we only use it to
get polymorphic built-in functions over polymorphic built-in types, since it's not possible
to juggle values of polymorphic built-in types instantiated with non-built-in types at runtime
(it's not even possible to represent such a value in the AST, even though it's possible to represent
such a 'Type').

Finally, it is not necessary to allow embedding PLC terms into meta-constants.
We already allow built-in functions with polymorphic types. There might be a way to utilize this
feature and have meta-constructors as built-in functions.
-}

-- See Note [Representing polymorphism].
-- | The universe used by default.
data DefaultUni a where
    DefaultUniInteger :: DefaultUni (Esc Integer)
    DefaultUniByteString :: DefaultUni (Esc ByteString)
    DefaultUniString :: DefaultUni (Esc Text)
    DefaultUniUnit :: DefaultUni (Esc ())
    DefaultUniBool :: DefaultUni (Esc Bool)
    DefaultUniProtoArray :: DefaultUni (Esc Strict.Vector)
    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)

-- GHC infers crazy types for these two and the straightforward ones break pattern matching,
-- so we just leave GHC with its craziness.
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 $mDefaultUniArray :: forall {r} {a}.
DefaultUni a
-> (forall {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
    (a ~ Esc (f a1), Esc f ~ Esc Vector) =>
    DefaultUni (Esc a1) -> r)
-> ((# #) -> r)
-> r
$bDefaultUniArray :: forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc Vector) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniArray uniA =
    DefaultUniProtoArray `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
    -- We define 'geq' manually instead of using 'deriveGEq', because the latter creates a single
    -- recursive definition and we want two instead. The reason why we want two is because this
    -- allows GHC to inline the initial step that appears non-recursive to GHC, because recursion
    -- is hidden in the other function that is marked as @OPAQUE@ and is chosen by GHC as a
    -- loop-breaker, see https://wiki.haskell.org/Inlining_and_Specialisation#What_is_a_loop-breaker
    -- (we're not really sure if this is a reliable solution, but if it stops working, we won't miss
    -- very much and we've failed to settle on any other approach).
    --
    -- This trick gives us a 1% speedup across validation benchmarks (some are up to 4% faster) and
    -- a more sensible generated Core where things like @geq DefaulUniBool@ are reduced away.
    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
DefaultUniProtoArray DefaultUni a2
a2 = do
            DefaultUni a2
DefaultUniProtoArray <- 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 #-}

-- | For pleasing the coverage checker.
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)
DefaultUniProtoArray           = 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
DefaultUniProtoArray           -> InContextM RenderContext (Doc ann)
"array"
        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

-- | This always pretty-prints parens around type applications (e.g. @(list bool)@) and
-- doesn't pretty-print them otherwise (e.g. @integer@).
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

-- | Elaborate a built-in type (see 'ElaborateBuiltin') from 'DefaultUni'.
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` Strict.Vector where
    knownUni :: DefaultUni (Esc Vector)
knownUni = DefaultUni (Esc Vector)
DefaultUniProtoArray
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 (Strict.Vector a) =>
    KnownTypeAst tyname DefaultUni (Strict.Vector 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 (Strict.Vector a) =>
    ReadKnownIn DefaultUni term (Strict.Vector 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 (Strict.Vector a) =>
    MakeKnownIn DefaultUni term (Strict.Vector 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

-- If this tells you an instance is missing, add it right above, following the pattern.
instance TestTypesFromTheUniverseAreAllKnown DefaultUni

{- Note [Integral types as Integer]
Technically our universe only contains 'Integer', but many of the builtin functions that we would
like to use work over 'Int', 'Word8' etc.

This is inconvenient and also error-prone: dealing with a function that takes an 'Int' or 'Word8'
means carefully downcasting the 'Integer', running the function, potentially upcasting at the end.
And it's easy to get wrong by e.g. blindly using 'fromInteger' or 'fromIntegral'.

Moreover, there is a latent risk here: if we *were* to build on a 32-bit architecture, then programs
which use arguments between @maxBound :: Int32@ and @maxBound :: Int64@ would behave differently!

So, what to do? We adopt the following strategy:
- We allow lifting/unlifting bounded integral types such as 'Word8' or 'Int64' via 'Integer',
  including a safe upcast in 'makeKnown' (which we could have on any architecture, but we only add
  it for 64-bit for uniformity) and a safe checked downcast in 'readKnown'.
- We allow lifting/unlifting 'Int' via 'Int64' and 'Word' via 'Word64', constraining the conversion
  between them to 64-bit architectures where this conversion is safe.

Doing this effectively bans builds on 32-bit systems, but that's fine, since we don't care about
supporting 32-bit systems anyway, and this way any attempts to build on them will fail fast.
-}

-- | For deriving 'KnownTypeAst', 'MakeKnown' and 'ReadKnown' instances via 'Integer'.
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 =
        -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
        -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
        -- (go figure why).
        (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) ->
            -- We don't make use here of 'toIntegralSized' because of performance considerations,
            -- see: https://gitlab.haskell.org/ghc/ghc/-/issues/19641
            -- TODO: benchmark an alternative 'integerToIntMaybe', modified from @ghc-bignum@
            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 BuiltinError -> ReadKnownM (AsInteger a)
forall a. BuiltinError -> Either BuiltinError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (BuiltinError -> ReadKnownM (AsInteger a))
-> (Text -> BuiltinError) -> Text -> ReadKnownM (AsInteger a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> BuiltinError
operationalUnliftingError (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
-- See Note [Integral types as Integer].
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 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 =
        -- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
        -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
        -- (go figure why).
        (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) ->
            -- TODO: benchmark alternatives:signumInteger,integerIsNegative,integerToNaturalThrow
            if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
            -- TODO: benchmark alternatives: ghc>=9 integerToNatural
            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 BuiltinError -> ReadKnownM Natural
forall a. BuiltinError -> Either BuiltinError a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (BuiltinError -> ReadKnownM Natural)
-> (Text -> BuiltinError) -> Text -> ReadKnownM Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> BuiltinError
operationalUnliftingError (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 #-}

outOfBoundsErr :: Pretty a => a -> Vector.Vector term -> Text
outOfBoundsErr :: forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr a
x Vector term
branches = [Text] -> Text
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    [ Text
"'case "
    , a -> Text
forall str a. (Pretty a, Render str) => a -> str
display a
x
    , Text
"' is out of bounds for the given number of branches: "
    , Int -> Text
forall str a. (Pretty a, Render str) => a -> str
display (Int -> Text) -> Int -> Text
forall a b. (a -> b) -> a -> b
$ Vector term -> Int
forall a. Vector a -> Int
Vector.length Vector term
branches
    ]

instance AnnotateCaseBuiltin DefaultUni where
    annotateCaseBuiltin :: forall term ann.
(UniOf term ~ DefaultUni) =>
Type TyName DefaultUni ann
-> [term] -> Either Text [(term, [Type TyName DefaultUni ann])]
annotateCaseBuiltin Type TyName DefaultUni ann
ty [term]
branches = case Type TyName DefaultUni ann
ty of
        TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniUnit)    ->
          case [term]
branches of
            [term
x] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right ([(term, [Type TyName DefaultUni ann])]
 -> Either Text [(term, [Type TyName DefaultUni ann])])
-> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ [(term
x, [])]
            [term]
_   -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on unit only allows exactly one branch"
        TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniBool)    ->
          case [term]
branches of
            [term
f]    -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right ([(term, [Type TyName DefaultUni ann])]
 -> Either Text [(term, [Type TyName DefaultUni ann])])
-> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ [(term
f, [])]
            [term
f, term
t] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right ([(term, [Type TyName DefaultUni ann])]
 -> Either Text [(term, [Type TyName DefaultUni ann])])
-> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ [(term
f, []), (term
t, [])]
            [term]
_      -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on bool requires exactly one branch or two branches"
        TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniInteger) ->
          [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right ([(term, [Type TyName DefaultUni ann])]
 -> Either Text [(term, [Type TyName DefaultUni ann])])
-> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ (term -> (term, [Type TyName DefaultUni ann]))
-> [term] -> [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> [a] -> [b]
map (, []) [term]
branches
        listTy :: Type TyName DefaultUni ann
listTy@(TyApp ann
_ (TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoList)) Type TyName DefaultUni ann
argTy) ->
          case [term]
branches of
            [term
cons]      -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
cons, [Type TyName DefaultUni ann
argTy, Type TyName DefaultUni ann
listTy])]
            [term
cons, term
nil] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
cons, [Type TyName DefaultUni ann
argTy, Type TyName DefaultUni ann
listTy]), (term
nil, [])]
            [term]
_           -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on list requires exactly one branch or two branches"
        (TyApp ann
_ (TyApp ann
_ (TyBuiltin ann
_ (SomeTypeIn DefaultUni (Esc a)
DefaultUniProtoPair)) Type TyName DefaultUni ann
lTyArg) Type TyName DefaultUni ann
rTyArg) ->
          case [term]
branches of
            [term
f] -> [(term, [Type TyName DefaultUni ann])]
-> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. b -> Either a b
Right [(term
f, [Type TyName DefaultUni ann
lTyArg, Type TyName DefaultUni ann
rTyArg])]
            [term]
_   -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left Text
"Casing on pair requires exactly one branch"
        Type TyName DefaultUni ann
_                 -> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. a -> Either a b
Left (Text -> Either Text [(term, [Type TyName DefaultUni ann])])
-> Text -> Either Text [(term, [Type TyName DefaultUni ann])]
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Text
forall str a. (Pretty a, Render str) => a -> str
display (() () -> Type TyName DefaultUni ann -> Type TyName DefaultUni ()
forall a b.
a -> Type TyName DefaultUni b -> Type TyName DefaultUni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName DefaultUni ann
ty) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" isn't supported in 'case'"

instance CaseBuiltin DefaultUni where
    caseBuiltin :: forall term.
(UniOf term ~ DefaultUni) =>
Some (ValueOf DefaultUni)
-> Vector term
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
caseBuiltin someVal :: Some (ValueOf DefaultUni)
someVal@(Some (ValueOf DefaultUni (Esc a)
uni a
x)) Vector term
branches = case DefaultUni (Esc a)
uni of
        DefaultUni (Esc a)
DefaultUniUnit
          | Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
len   -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> HeadSpine a b
HeadOnly (term -> HeadSpine term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0
          | Bool
otherwise -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
        DefaultUni (Esc a)
DefaultUniBool -> case a
x of
            -- We allow there to be only one branch as long as the scrutinee is 'False'.
            -- This is strictly to save size by not having the 'True' branch if it was gonna be
            -- 'Error' anyway.
            a
Bool
False | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
|| Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> HeadSpine a b
HeadOnly (term -> HeadSpine term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0
            a
Bool
True  |             Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> HeadSpine a b
HeadOnly (term -> HeadSpine term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
1
            a
_                            -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left  (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
        DefaultUni (Esc a)
DefaultUniInteger
            | a
0 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
len -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> HeadSpine a b
HeadOnly (term -> HeadSpine term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Integer -> Int
forall a. Num a => Integer -> a
fromInteger a
Integer
x
            | Bool
otherwise                   -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left  (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
        DefaultUniList DefaultUni (Esc a1)
ty
            | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ->
              case a
x of
                [] -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left Text
"Expected non-empty list, got empty list for casing list"
                (a1
y : [a1]
ys) -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> [b] -> HeadSpine a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
ty a1
y, DefaultUni (Esc a) -> a -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a)
uni a
[a1]
ys]
            | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 ->
              case a
x of
                []       -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> HeadSpine a b
HeadOnly (term -> HeadSpine term (Some (ValueOf DefaultUni)))
-> term -> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. (a -> b) -> a -> b
$ Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
1
                (a1
y : [a1]
ys) -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> [b] -> HeadSpine a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
ty a1
y, DefaultUni (Esc a) -> a -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a)
uni a
[a1]
ys]
            | Bool
otherwise            -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
        DefaultUniPair DefaultUni (Esc a2)
tyL DefaultUni (Esc a1)
tyR
            | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ->
              case a
x of
                (a2
l, a1
r) -> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. b -> Either a b
Right (HeadSpine term (Some (ValueOf DefaultUni))
 -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> HeadSpine term (Some (ValueOf DefaultUni))
-> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ term
-> [Some (ValueOf DefaultUni)]
-> HeadSpine term (Some (ValueOf DefaultUni))
forall a b. a -> [b] -> HeadSpine a b
headSpine (Vector term
branches Vector term -> Int -> term
forall a. Vector a -> Int -> a
Vector.! Int
0) [DefaultUni (Esc a2) -> a2 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a2)
DefaultUni (Esc a2)
tyL a2
l, DefaultUni (Esc a1) -> a1 -> Some (ValueOf DefaultUni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf DefaultUni (Esc a1)
DefaultUni (Esc a1)
tyR a1
r]
            | Bool
otherwise -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ Some (ValueOf DefaultUni) -> Vector term -> Text
forall a term. Pretty a => a -> Vector term -> Text
outOfBoundsErr Some (ValueOf DefaultUni)
someVal Vector term
branches
        DefaultUni (Esc a)
_ -> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. a -> Either a b
Left (Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni))))
-> Text -> Either Text (HeadSpine term (Some (ValueOf DefaultUni)))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> Text
forall str a. (Pretty a, Render str) => a -> str
display DefaultUni (Esc a)
uni Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" isn't supported in 'case'"
      where
        !len :: Int
len = Vector term -> Int
forall a. Vector a -> Int
Vector.length Vector term
branches
    {-# INLINE caseBuiltin #-}

{- Note [Stable encoding of tags]
'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'
and 'decodeUni' must be amended only in a backwards compatible manner.

See Note [Stable encoding of TPLC]
-}

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` Strict.Vector
        , constr `Permits` (,)
        , constr `Permits` Data
        , constr `Permits` BLS12_381.G1.Element
        , constr `Permits` BLS12_381.G2.Element
        , constr `Permits` BLS12_381.Pairing.MlResult
        )

    -- See Note [Stable encoding of tags].
    -- IF YOU'RE GETTING A WARNING HERE, DON'T FORGET TO AMEND 'withDecodedUni' RIGHT BELOW.
    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]
    encodeUni DefaultUni a
DefaultUniProtoArray           = [Int
12]

    -- See Note [Decoding universes].
    -- See Note [Stable encoding of tags].
    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
12 -> DefaultUni (Esc Vector) -> DecodeUniM r
forall k (a :: k). Typeable k => DefaultUni (Esc a) -> DecodeUniM r
k DefaultUni (Esc Vector)
DefaultUniProtoArray
        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)
DefaultUniProtoArray `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