-- | The universe used by default and its instances.

{-# OPTIONS -fno-warn-missing-pattern-synonym-signatures #-}

{-# LANGUAGE BlockArguments        #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- effectfully: to the best of my experimentation, -O2 here improves performance, however by
-- inspecting GHC Core I was only able to see a difference in how the 'KnownTypeIn' instance for
-- 'Int' is compiled (one more call is inlined with -O2). This needs to be investigated.
{-# OPTIONS_GHC -O2 #-}

module PlutusCore.Default.Universe
    ( DefaultUni (..)
    , pattern DefaultUniList
    , pattern DefaultUniPair
    , module Export  -- Re-exporting universes infrastructure for convenience.
    ) where

import PlutusCore.Builtin
import PlutusCore.Data
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import PlutusCore.Parsable

import Control.Applicative
import Data.ByteString qualified as BS
import Data.Foldable
import Data.Proxy
import Data.Text qualified as Text
import GHC.Exts (inline, oneShot)
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 necessarily the case that we need 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 BS.ByteString)
    DefaultUniString     :: DefaultUni (Esc Text.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)

-- GHC infers crazy types for these two and the straightforward ones break pattern matching,
-- so we just leave GHC with its craziness.
pattern $bDefaultUniList :: DefaultUni (Esc a1) -> DefaultUni a
$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)
-> (Void# -> r)
-> r
DefaultUniList uniA =
    DefaultUniProtoList `DefaultUniApply` uniA
pattern $bDefaultUniPair :: DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
$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)
-> (Void# -> r)
-> r
DefaultUniPair uniA uniB =
    DefaultUniProtoPair `DefaultUniApply` uniA `DefaultUniApply` uniB

deriveGEq ''DefaultUni
deriveGCompare ''DefaultUni

-- | For pleasing the coverage checker.
noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d)) -> any
noMoreTypeFunctions :: 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 :: 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 (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc f)
uniF of SingKind k
_ `SingKindArrow` SingKind l
cod -> SingKind k
SingKind l
cod
    toSingKind DefaultUni (Esc a)
DefaultUniData           = SingKind k
forall k. KnownKind k => SingKind k
knownKind

instance HasUniApply DefaultUni where
    matchUniApply :: 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

instance GShow DefaultUni where gshowsPrec :: Int -> DefaultUni a -> ShowS
gshowsPrec = Int -> DefaultUni a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance Show (DefaultUni a) where
    show :: DefaultUni a -> String
show DefaultUni a
DefaultUniInteger             = String
"integer"
    show DefaultUni a
DefaultUniByteString          = String
"bytestring"
    show DefaultUni a
DefaultUniString              = String
"string"
    show DefaultUni a
DefaultUniUnit                = String
"unit"
    show DefaultUni a
DefaultUniBool                = String
"bool"
    show DefaultUni a
DefaultUniProtoList           = String
"list"
    show DefaultUni a
DefaultUniProtoPair           = String
"pair"
    show (DefaultUni (Esc f)
uniF `DefaultUniApply` DefaultUni (Esc a)
uniB) = case DefaultUni (Esc f)
uniF of
        DefaultUni (Esc f)
DefaultUniProtoList                          -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"list (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
DefaultUniProtoPair                          -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"pair (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a)
uniA   -> [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"pair (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniA, String
") (", DefaultUni (Esc a) -> String
forall a. Show a => a -> String
show DefaultUni (Esc a)
uniB, String
")"]
        DefaultUni (Esc f)
uniG `DefaultUniApply` DefaultUni (Esc a)
_ `DefaultUniApply` DefaultUni (Esc a)
_ -> DefaultUni (Esc f) -> String
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
uniG
    show DefaultUni a
DefaultUniData = String
"data"

-- See Note [Parsing horribly broken].
instance Parsable (SomeTypeIn (Kinded DefaultUni)) where
    parse :: Text -> Maybe (SomeTypeIn (Kinded DefaultUni))
parse Text
"bool"       = SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (Kinded DefaultUni (Esc Bool) -> SomeTypeIn (Kinded DefaultUni))
-> Kinded DefaultUni (Esc Bool)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc Bool) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc Bool)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> Kinded DefaultUni (Esc Bool)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Bool) -> Kinded DefaultUni (Esc Bool)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded DefaultUni (Esc Bool)
DefaultUniBool
    parse Text
"bytestring" = SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (Kinded DefaultUni (Esc ByteString)
    -> SomeTypeIn (Kinded DefaultUni))
-> Kinded DefaultUni (Esc ByteString)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc ByteString)
-> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc ByteString)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> Kinded DefaultUni (Esc ByteString)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc ByteString) -> Kinded DefaultUni (Esc ByteString)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded DefaultUni (Esc ByteString)
DefaultUniByteString
    parse Text
"string"     = SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (Kinded DefaultUni (Esc Text) -> SomeTypeIn (Kinded DefaultUni))
-> Kinded DefaultUni (Esc Text)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc Text) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc Text)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> Kinded DefaultUni (Esc Text)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Text) -> Kinded DefaultUni (Esc Text)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded DefaultUni (Esc Text)
DefaultUniString
    parse Text
"integer"    = SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (Kinded DefaultUni (Esc Integer)
    -> SomeTypeIn (Kinded DefaultUni))
-> Kinded DefaultUni (Esc Integer)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc Integer) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc Integer)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> Kinded DefaultUni (Esc Integer)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Integer) -> Kinded DefaultUni (Esc Integer)
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded DefaultUni (Esc Integer)
DefaultUniInteger
    parse Text
"unit"       = SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (Kinded DefaultUni (Esc ()) -> SomeTypeIn (Kinded DefaultUni))
-> Kinded DefaultUni (Esc ())
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc ()) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc ())
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> Kinded DefaultUni (Esc ())
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc ()) -> Kinded DefaultUni (Esc ())
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded DefaultUni (Esc ())
DefaultUniUnit
    parse Text
text         = [Maybe (SomeTypeIn (Kinded DefaultUni))]
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
        [ do
            Text
aT <- Text -> Text -> Maybe Text
Text.stripPrefix Text
"[" Text
text Maybe Text -> (Text -> Maybe Text) -> Maybe Text
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> Text -> Maybe Text
Text.stripSuffix Text
"]"
            SomeTypeIn (Kinded a) <- Text -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. Parsable a => Text -> Maybe a
parse Text
aT
            k :~: *
Refl <- DefaultUni (Esc a) -> Maybe (k :~: *)
forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar @DefaultUni DefaultUni (Esc a)
a
            SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (DefaultUni (Esc [a]) -> SomeTypeIn (Kinded DefaultUni))
-> DefaultUni (Esc [a])
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc [a]) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc [a]) -> SomeTypeIn (Kinded DefaultUni))
-> (DefaultUni (Esc [a]) -> Kinded DefaultUni (Esc [a]))
-> DefaultUni (Esc [a])
-> SomeTypeIn (Kinded DefaultUni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc [a]) -> Kinded DefaultUni (Esc [a])
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded (DefaultUni (Esc [a]) -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> DefaultUni (Esc [a]) -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> DefaultUni (Esc [a])
forall a k1 k2 (f :: k1 -> k2) (a1 :: k1).
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList DefaultUni (Esc a)
a
        , do
            Text
abT <- Text -> Text -> Maybe Text
Text.stripPrefix Text
"(" Text
text Maybe Text -> (Text -> Maybe Text) -> Maybe Text
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> Text -> Maybe Text
Text.stripSuffix Text
")"
            -- Note that we don't allow whitespace after @,@ (but we could).
            -- Anyway, looking for a single comma is just plain wrong, as we may have a nested
            -- tuple (and it can be left- or right- or both-nested), so we're running into
            -- the same parsing problem as with constants.
            case Text -> Text -> [Text]
Text.splitOn Text
"," Text
abT of
                [Text
aT, Text
bT] -> do
                    SomeTypeIn (Kinded a) <- Text -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. Parsable a => Text -> Maybe a
parse Text
aT
                    k :~: *
Refl <- DefaultUni (Esc a) -> Maybe (k :~: *)
forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar @DefaultUni DefaultUni (Esc a)
a
                    SomeTypeIn (Kinded b) <- Text -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. Parsable a => Text -> Maybe a
parse Text
bT
                    k :~: *
Refl <- DefaultUni (Esc a) -> Maybe (k :~: *)
forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar @DefaultUni DefaultUni (Esc a)
b
                    SomeTypeIn (Kinded DefaultUni)
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. a -> Maybe a
Just (SomeTypeIn (Kinded DefaultUni)
 -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> (DefaultUni (Esc (a, a)) -> SomeTypeIn (Kinded DefaultUni))
-> DefaultUni (Esc (a, a))
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kinded DefaultUni (Esc (a, a)) -> SomeTypeIn (Kinded DefaultUni)
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (Kinded DefaultUni (Esc (a, a)) -> SomeTypeIn (Kinded DefaultUni))
-> (DefaultUni (Esc (a, a)) -> Kinded DefaultUni (Esc (a, a)))
-> DefaultUni (Esc (a, a))
-> SomeTypeIn (Kinded DefaultUni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc (a, a)) -> Kinded DefaultUni (Esc (a, a))
forall k (uni :: * -> *) (a :: k).
Typeable k =>
uni (Esc a) -> Kinded uni (Esc a)
Kinded (DefaultUni (Esc (a, a)) -> Maybe (SomeTypeIn (Kinded DefaultUni)))
-> DefaultUni (Esc (a, a))
-> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> DefaultUni (Esc a) -> DefaultUni (Esc (a, a))
forall a k1 k2 (f1 :: k1 -> k2) (a1 :: k1) k3 k4 (f2 :: k3 -> k4)
       (a2 :: k3).
(a ~ Esc (f1 a1), Esc f1 ~ Esc (f2 a2), Esc f2 ~ Esc (,)) =>
DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> DefaultUni a
DefaultUniPair DefaultUni (Esc a)
a DefaultUni (Esc a)
b
                [Text]
_ -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall a. Maybe a
Nothing
        ]

instance DefaultUni `Contains` Integer       where knownUni :: DefaultUni (Esc Integer)
knownUni = DefaultUni (Esc Integer)
DefaultUniInteger
instance DefaultUni `Contains` BS.ByteString where knownUni :: DefaultUni (Esc ByteString)
knownUni = DefaultUni (Esc ByteString)
DefaultUniByteString
instance DefaultUni `Contains` Text.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` 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 KnownBuiltinTypeAst DefaultUni Integer       => KnownTypeAst DefaultUni Integer
instance KnownBuiltinTypeAst DefaultUni BS.ByteString => KnownTypeAst DefaultUni BS.ByteString
instance KnownBuiltinTypeAst DefaultUni Text.Text     => KnownTypeAst DefaultUni Text.Text
instance KnownBuiltinTypeAst DefaultUni ()            => KnownTypeAst DefaultUni ()
instance KnownBuiltinTypeAst DefaultUni Bool          => KnownTypeAst DefaultUni Bool
instance KnownBuiltinTypeAst DefaultUni [a]           => KnownTypeAst DefaultUni [a]
instance KnownBuiltinTypeAst DefaultUni (a, b)        => KnownTypeAst DefaultUni (a, b)
instance KnownBuiltinTypeAst DefaultUni Data          => KnownTypeAst DefaultUni Data

instance KnownBuiltinTypeIn DefaultUni term Integer       => KnownTypeIn DefaultUni term Integer
instance KnownBuiltinTypeIn DefaultUni term BS.ByteString => KnownTypeIn DefaultUni term BS.ByteString
instance KnownBuiltinTypeIn DefaultUni term Text.Text     => KnownTypeIn DefaultUni term Text.Text
instance KnownBuiltinTypeIn DefaultUni term ()            => KnownTypeIn DefaultUni term ()
instance KnownBuiltinTypeIn DefaultUni term Bool          => KnownTypeIn DefaultUni term Bool
instance KnownBuiltinTypeIn DefaultUni term [a]           => KnownTypeIn DefaultUni term [a]
instance KnownBuiltinTypeIn DefaultUni term (a, b)        => KnownTypeIn DefaultUni term (a, b)
instance KnownBuiltinTypeIn DefaultUni term Data          => KnownTypeIn DefaultUni term Data

-- If this tells you a 'KnownTypeIn' instance is missing, add it right above, following the pattern
-- (you'll also need to add a 'KnownTypeAst' instance as well).
instance TestTypesFromTheUniverseAreAllKnown DefaultUni

{- Note [Int as Integer]
We represent 'Int' as 'Integer' in PLC and check that an 'Integer' fits into 'Int' when
unlifting constants fo type 'Int' and fail with an evaluation failure (via 'AsEvaluationFailure')
if it doesn't. We couldn't fail via 'AsUnliftingError', because an out-of-bounds error is not an
internal one -- it's a normal evaluation failure, but unlifting errors have this connotation of
being "internal".
-}

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

-- See Note [Int as Integer].
instance HasConstantIn DefaultUni term => KnownTypeIn DefaultUni term Int where
    makeKnown :: (Text -> m ()) -> Maybe cause -> Int -> m term
makeKnown Text -> m ()
emit Maybe cause
mayCause = (Text -> m ()) -> Maybe cause -> Integer -> m term
forall (uni :: * -> *) val a err cause (m :: * -> *).
(KnownTypeIn uni val a, MonadError (ErrorWithCause err cause) m,
 AsEvaluationFailure err) =>
(Text -> m ()) -> Maybe cause -> a -> m val
makeKnown Text -> m ()
emit Maybe cause
mayCause (Integer -> m term) -> (Int -> Integer) -> Int -> m term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
    {-# INLINE makeKnown #-}

    readKnown :: Maybe cause -> term -> Either (ErrorWithCause err cause) Int
readKnown Maybe cause
mayCause term
term =
        -- See Note [Performance of KnownTypeIn instances].
        -- Funnily, we don't need 'inline' here, unlike in the default implementation of 'readKnown'
        -- (go figure why).
        (Maybe cause -> term -> Either (ErrorWithCause err cause) Integer)
-> Maybe cause -> term -> Either (ErrorWithCause err cause) Integer
forall a. a -> a
inline Maybe cause -> term -> Either (ErrorWithCause err cause) Integer
forall val a err cause.
(AsUnliftingError err, KnownBuiltinType val a) =>
Maybe cause -> val -> Either (ErrorWithCause err cause) a
readKnownConstant Maybe cause
mayCause term
term Either (ErrorWithCause err cause) Integer
-> (Integer -> Either (ErrorWithCause err cause) Int)
-> Either (ErrorWithCause err cause) Int
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Integer -> Either (ErrorWithCause err cause) Int)
-> Integer -> Either (ErrorWithCause err cause) Int
oneShot \(Integer
i :: Integer) ->
            if Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
minBound :: Int) 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
<= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
forall a. Bounded a => a
maxBound :: Int)
                then Int -> Either (ErrorWithCause err cause) Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Either (ErrorWithCause err cause) Int)
-> Int -> Either (ErrorWithCause err cause) Int
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
                else AReview err ()
-> () -> Maybe cause -> Either (ErrorWithCause err cause) Int
forall exc e t term (m :: * -> *) x.
(exc ~ ErrorWithCause e term, MonadError exc m) =>
AReview e t -> t -> Maybe term -> m x
throwingWithCause AReview err ()
forall err. AsEvaluationFailure err => Prism' err ()
_EvaluationFailure () Maybe cause
mayCause
    {-# INLINE readKnown #-}

{- 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 PLC]
-}

instance Closed DefaultUni where
    type DefaultUni `Everywhere` constr =
        ( constr `Permits` Integer
        , constr `Permits` BS.ByteString
        , constr `Permits` Text.Text
        , constr `Permits` ()
        , constr `Permits` Bool
        , constr `Permits` []
        , constr `Permits` (,)
        , constr `Permits` Data
        )

    -- See Note [Stable encoding of tags].
    -- IF YOU'RE GETTING A WARNING HERE, DON'T FORGET TO AMEND 'withDecodedUni' RIGHT BELOW.
    encodeUni :: 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 (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 (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc a)
uniA
    encodeUni DefaultUni a
DefaultUniData              = [Int
8]

    -- See Note [Decoding universes].
    -- See Note [Stable encoding of tags].
    withDecodedUni :: (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 (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 r.
Closed DefaultUni =>
(forall k (a :: k).
 Typeable k =>
 DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
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 r.
Closed DefaultUni =>
(forall k (a :: k).
 Typeable k =>
 DefaultUni (Esc a) -> DecodeUniM r)
-> DecodeUniM r
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
_ -> DecodeUniM r
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 :: 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
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniA 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
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
bring proxy constr
p DefaultUni (Esc a)
DefaultUni (Esc a)
uniB 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