{-# LANGUAGE BlockArguments          #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DefaultSignatures       #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE LambdaCase              #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE OverloadedStrings       #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module PlutusCore.Builtin.KnownType
    ( KnownBuiltinTypeIn
    , KnownBuiltinType
    , readKnownConstant
    , KnownTypeIn (..)
    , KnownType
    , TestTypesFromTheUniverseAreAllKnown
    , readKnownSelf
    , makeKnownOrFail
    ) where

import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.KnownTypeAst
import PlutusCore.Builtin.Polymorphism
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result

import Control.Monad.Except
import Data.Coerce
import Data.Kind qualified as GHC (Type)
import Data.String
import Data.Text (Text)
import GHC.Exts (inline, oneShot)
import Universe

-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a)

-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\".
type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a

{- Note [Performance of KnownTypeIn instances]
It's critically important that 'readKnown' runs in the concrete 'Either' rather than a general
'MonadError'. Changing from the latter to the former gave us a speedup of up to 19%, see
https://github.com/input-output-hk/plutus/pull/4307

The same does not apply to 'makeKnown' however and so we keep 'MonadError' there, see
https://github.com/input-output-hk/plutus/pull/4308
Although there's a different kind of inlining that helps in case of 'makeKnown', see the first
commit and the first comment of https://github.com/input-output-hk/plutus/pull/4251
We don't have it merged currently though, because there's a hope for a better solution.

Even though we don't use 'makeKnown' and 'readKnown' directly over concrete types, it's still
beneficial to inline them, because otherwise GHC compiles each of them to two definitions
(one calling the other) for some reason. So always add an @INLINE@ pragma to all definitions
of 'makeKnown' and 'readKnown' unless you have a specific reason not to.

Similarly, we inline implementations of 'toTypeAst' just to get tidier Core.

Some 'readKnown' implementations require inserting a call to 'oneShot'. E.g. if 'oneShot' is not
used in 'readKnownConstant' then 'GHC pulls @gshow uniExp@ out of the 'Nothing' branch, thus
allocating a thunk of type 'String' that is completely redundant whenever there's no error,
which is the majority of cases. And putting 'oneShot' as the outermost call results in
worse Core.

Any change to an instance of 'KnownTypeIn', even completely trivial, requires looking into the
generated Core, since compilation of these instances is extremely brittle optimization-wise.

Things to watch out for are unnecessary sharing (for example, a @let@ appearing outside of a @case@
allocates a thunk and if that thunk is not referenced inside of one of the branches, then it's
wasteful, especially when it's not referenced in the most commonly chosen branch) and type class
methods not being extracted from the dictionary and used directly instead (i.e. if you see
multiple @pure@ and @>>=@ in the code, that's not good). Note that neither @let@ nor @>>=@ are bad
in general, we certainly do need to allocate thunks occasionally, it's just that when it comes to
builtins this is rarely the case as most of the time we want aggressive inlining and specialization
and the "just compute the damn thing" behavior.
-}

{- Note [Unlifting values of built-in types]
It's trivial to unlift from a term a value of a monomorphic type like 'Integer': just check that
the term is a constant, extract the type tag and check it for equality with the type tag of
'Integer'.

Things work the same way for a fully monomorphized polymorphic type, i.e. @(Integer, Bool@) is not
any different from just 'Integer' unlifting-wise.

However there's no sensible way of unlifting a value of, say, @[a]@ where @a@ in not a built-in
type. So let's say we instantiated @a@ to an @Opaque val rep@ like we do for polymorphic functions
that don't deal with polymorphic built-in types (e.g. `id`, `ifThenElse` etc). That would mean we'd
need to write a function from a @[a]@ for some arbitrary built-in @a@ to @[Opaque val a]@. Which
is really easy to do: it's just @map makeKnown@. But the problem is, unlifting is supposed to be
cheap and that @map@ is O(n), so for example 'MkCons' would become an O(n) operation making
perfectly linear algorithms quadratic. See https://github.com/input-output-hk/plutus/pull/4215 for
how that would look like.

So the problem is that we can't convert in O(1) time a @[a]@ coming from a constant of
statically-unknown type (that @a@ is existential) to @[a']@ where @a'@ is known statically.
Thus it's impossible to instantiate @a@ in Haskell's

    nullList :: [a] -> Bool

so that there's a 'TypeScheme' for this function.

One non-solution would be to instantiate @a@, then recurse on the type, construct a new function
that defers to the original @nullList@ but wraps its argument in a specific way (more on that below)
making it possible to assign a 'TypeScheme' to the resulting function. Astonishingly enough, that
could actually work and if we ever write a paper on builtins, we should mention that example, but:

1. such a trick requires a generic machinery that knows how to check that the head of the builtin
   application is a particular built-in type. We used to have that, but it was just way too slow
2. that would only work for functions that don't care about @a@ at all. But for example when
   elaborating @cons :: a -> [a] -> [a]@ as a Plutus builtin we need to unlift both the arguments
   and check that their @a@s are equal
   (See Note [Representable built-in functions over polymorphic built-in types])
   and it's either way too complex or even impossible to do that automatically within some generic
   machinery

So what we do is we simply require the user to write

    nullList :: Opaque val [a] -> Bool

and unlift a @[a]@ manually within the definition of the builtin. This works, because the
existential @a@ never escapes the definition of the builtin. I.e. it's fine to unpack an existential
and use it immediately without ever exposing the existential parts to the outside and it's not fine
to try to return a value having an existential inside of it, which is what unlifting of @[a]@ would
amount to.

Could we somehow align the unlifting machinery so that it does not construct values of particular
types, but rather feeds them to a continuation or something, so that the existential parts never
try to escape? Maybe, but see point 2 from the above, we do want to get our hands on the particular
universes sometimes and point 1 prevents us from doing that generically, so it doesn't seem like
we could do that within some automated machinery.

Overall, asking the user to manually unlift from @Opaque val [a]@ is just always going to be
faster than any kind of fancy encoding.
-}

-- See Note [Unlifting values of built-in types].
-- | Convert a constant embedded into a PLC term to the corresponding Haskell value.
readKnownConstant
    :: forall val a err cause. (AsUnliftingError err, KnownBuiltinType val a)
    => Maybe cause -> val -> Either (ErrorWithCause err cause) a
-- See Note [Performance of KnownTypeIn instances].
readKnownConstant :: Maybe cause -> val -> Either (ErrorWithCause err cause) a
readKnownConstant Maybe cause
mayCause val
val = Maybe cause
-> val
-> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf val)))
forall term err cause (m :: * -> *).
(AsConstant term, MonadError (ErrorWithCause err cause) m,
 AsUnliftingError err) =>
Maybe cause -> term -> m (Some (ValueOf (UniOf term)))
asConstant Maybe cause
mayCause val
val Either (ErrorWithCause err cause) (Some (ValueOf (UniOf val)))
-> (Some (ValueOf (UniOf val))
    -> Either (ErrorWithCause err cause) a)
-> Either (ErrorWithCause err cause) a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Some (ValueOf (UniOf val)) -> Either (ErrorWithCause err cause) a)
-> Some (ValueOf (UniOf val))
-> Either (ErrorWithCause err cause) a
oneShot \case
    Some (ValueOf uniAct x) -> do
        let uniExp :: UniOf val (Esc a)
uniExp = Contains (UniOf val) a => UniOf val (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni @_ @(UniOf val) @a
        case UniOf val (Esc a)
uniAct UniOf val (Esc a) -> UniOf val (Esc a) -> Maybe (Esc a :~: Esc a)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` UniOf val (Esc a)
uniExp of
            Just Esc a :~: Esc a
Refl -> a -> Either (ErrorWithCause err cause) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
            Maybe (Esc a :~: Esc a)
Nothing   -> do
                let err :: UnliftingError
err = String -> UnliftingError
forall a. IsString a => String -> a
fromString (String -> UnliftingError) -> String -> UnliftingError
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                        [ String
"Type mismatch: "
                        , String
"expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UniOf val (Esc a) -> String
forall k (t :: k -> *) (a :: k). GShow t => t a -> String
gshow UniOf val (Esc a)
uniExp
                        , String
"; actual: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UniOf val (Esc a) -> String
forall k (t :: k -> *) (a :: k). GShow t => t a -> String
gshow UniOf val (Esc a)
uniAct
                        ]
                AReview err UnliftingError
-> UnliftingError
-> Maybe cause
-> Either (ErrorWithCause err cause) a
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 UnliftingError
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
err Maybe cause
mayCause
{-# INLINE readKnownConstant #-}

-- See Note [Performance of KnownTypeIn instances].
-- We use @default@ for providing instances for built-in types instead of @DerivingVia@, because
-- the latter breaks on @m term@ (and for brevity).
-- | Haskell types known to exist on the PLC side.
-- Both the methods take a @Maybe cause@ argument to report the cause of a potential failure.
-- @cause@ is different to @term@ to support evaluators that distinguish between terms and values
-- (@makeKnown@ normally constructs a value, but it's convenient to report the cause of a failure
-- as a term). Note that an evaluator might require the cause to be computed lazily for best
-- performance on the happy path and @Maybe@ ensures that even if we somehow force the argument,
-- the cause stored in it is not forced due to @Maybe@ being a lazy data type.
-- Note that 'KnownTypeAst' is not a superclass of 'KnownTypeIn'. This is due to the fact that
-- polymorphic built-in types are only liftable/unliftable when they're fully monomorphized, while
-- 'toTypeAst' works for polymorphic built-in types that have type variables in them, and so the
-- constraints are completely different in the two cases and we keep the two classes apart
-- (there doesn't seem to be any cons to that).
class uni ~ UniOf val => KnownTypeIn uni val a where
    -- | Convert a Haskell value to the corresponding PLC val.
    -- The inverse of 'readKnown'.
    makeKnown
        :: ( MonadError (ErrorWithCause err cause) m, AsEvaluationFailure err
           )
        => (Text -> m ()) -> Maybe cause -> a -> m val
    default makeKnown
        :: ( MonadError (ErrorWithCause err cause) m
           , KnownBuiltinType val a
           )
        => (Text -> m ()) -> Maybe cause -> a -> m val
    -- Forcing the value to avoid space leaks. Note that the value is only forced to WHNF,
    -- so care must be taken to ensure that every value of a type from the universe gets forced
    -- to NF whenever it's forced to WHNF.
    makeKnown Text -> m ()
_ Maybe cause
_ a
x = val -> m val
forall (f :: * -> *) a. Applicative f => a -> f a
pure (val -> m val) -> (a -> val) -> a -> m val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> val
forall term.
FromConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant (Some (ValueOf uni) -> val)
-> (a -> Some (ValueOf uni)) -> a -> val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Some (ValueOf uni)
forall a (uni :: * -> *). Includes uni a => a -> Some (ValueOf uni)
someValue (a -> m val) -> a -> m val
forall a b. (a -> b) -> a -> b
$! a
x
    {-# INLINE makeKnown #-}

    -- | Convert a PLC val to the corresponding Haskell value.
    -- The inverse of 'makeKnown'.
    readKnown
        :: ( AsUnliftingError err, AsEvaluationFailure err
           )
        => Maybe cause -> val -> Either (ErrorWithCause err cause) a
    default readKnown
        :: ( AsUnliftingError err
           , KnownBuiltinType val a
           )
        => Maybe cause -> val -> Either (ErrorWithCause err cause) a
    -- If 'inline' is not used, proper inlining does not happen for whatever reason.
    readKnown = (Maybe cause -> val -> Either (ErrorWithCause err cause) a)
-> Maybe cause -> val -> Either (ErrorWithCause err cause) a
forall a. a -> a
inline Maybe cause -> val -> Either (ErrorWithCause err cause) a
forall val a err cause.
(AsUnliftingError err, KnownBuiltinType val a) =>
Maybe cause -> val -> Either (ErrorWithCause err cause) a
readKnownConstant
    {-# INLINE readKnown #-}

-- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'.
type KnownType val a = (KnownTypeAst (UniOf val) a, KnownTypeIn (UniOf val) val a)

-- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
readKnownSelf
    :: ( KnownType val a
       , AsUnliftingError err, AsEvaluationFailure err
       )
    => val -> Either (ErrorWithCause err val) a
readKnownSelf :: val -> Either (ErrorWithCause err val) a
readKnownSelf val
val = Maybe val -> val -> Either (ErrorWithCause err val) a
forall (uni :: * -> *) val a err cause.
(KnownTypeIn uni val a, AsUnliftingError err,
 AsEvaluationFailure err) =>
Maybe cause -> val -> Either (ErrorWithCause err cause) a
readKnown (val -> Maybe val
forall a. a -> Maybe a
Just val
val) val
val

-- | For providing a 'KnownTypeIn' instance for a built-in type it's enough for that type to satisfy
-- 'KnownBuiltinTypeIn', hence the definition.
class    (forall val. KnownBuiltinTypeIn uni val a => KnownTypeIn uni val a) =>
    ImplementedKnownBuiltinTypeIn uni a
instance (forall val. KnownBuiltinTypeIn uni val a => KnownTypeIn uni val a) =>
    ImplementedKnownBuiltinTypeIn uni a

-- | An instance of this class not having any constraints ensures that every type
-- (according to 'Everywhere') from the universe has a 'KnownTypeIn' instance.
class uni `Everywhere` ImplementedKnownBuiltinTypeIn uni => TestTypesFromTheUniverseAreAllKnown uni

-- | A transformer for fitting a monad not carrying the cause of a failure into 'makeKnown'.
newtype NoCauseT (val :: GHC.Type) m a = NoCauseT
    { NoCauseT val m a -> m a
unNoCauseT :: m a
    } deriving newtype (a -> NoCauseT val m b -> NoCauseT val m a
(a -> b) -> NoCauseT val m a -> NoCauseT val m b
(forall a b. (a -> b) -> NoCauseT val m a -> NoCauseT val m b)
-> (forall a b. a -> NoCauseT val m b -> NoCauseT val m a)
-> Functor (NoCauseT val m)
forall a b. a -> NoCauseT val m b -> NoCauseT val m a
forall a b. (a -> b) -> NoCauseT val m a -> NoCauseT val m b
forall val (m :: * -> *) a b.
Functor m =>
a -> NoCauseT val m b -> NoCauseT val m a
forall val (m :: * -> *) a b.
Functor m =>
(a -> b) -> NoCauseT val m a -> NoCauseT val m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> NoCauseT val m b -> NoCauseT val m a
$c<$ :: forall val (m :: * -> *) a b.
Functor m =>
a -> NoCauseT val m b -> NoCauseT val m a
fmap :: (a -> b) -> NoCauseT val m a -> NoCauseT val m b
$cfmap :: forall val (m :: * -> *) a b.
Functor m =>
(a -> b) -> NoCauseT val m a -> NoCauseT val m b
Functor, Functor (NoCauseT val m)
a -> NoCauseT val m a
Functor (NoCauseT val m)
-> (forall a. a -> NoCauseT val m a)
-> (forall a b.
    NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b)
-> (forall a b c.
    (a -> b -> c)
    -> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c)
-> (forall a b.
    NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b)
-> (forall a b.
    NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a)
-> Applicative (NoCauseT val m)
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a
NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b
(a -> b -> c)
-> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c
forall a. a -> NoCauseT val m a
forall a b.
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a
forall a b.
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
forall a b.
NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b
forall a b c.
(a -> b -> c)
-> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c
forall val (m :: * -> *). Applicative m => Functor (NoCauseT val m)
forall val (m :: * -> *) a. Applicative m => a -> NoCauseT val m a
forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a
forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b
forall val (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a
$c<* :: forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m a
*> :: NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
$c*> :: forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
liftA2 :: (a -> b -> c)
-> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c
$cliftA2 :: forall val (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m c
<*> :: NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b
$c<*> :: forall val (m :: * -> *) a b.
Applicative m =>
NoCauseT val m (a -> b) -> NoCauseT val m a -> NoCauseT val m b
pure :: a -> NoCauseT val m a
$cpure :: forall val (m :: * -> *) a. Applicative m => a -> NoCauseT val m a
$cp1Applicative :: forall val (m :: * -> *). Applicative m => Functor (NoCauseT val m)
Applicative, Applicative (NoCauseT val m)
a -> NoCauseT val m a
Applicative (NoCauseT val m)
-> (forall a b.
    NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b)
-> (forall a b.
    NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b)
-> (forall a. a -> NoCauseT val m a)
-> Monad (NoCauseT val m)
NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
forall a. a -> NoCauseT val m a
forall a b.
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
forall a b.
NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b
forall val (m :: * -> *). Monad m => Applicative (NoCauseT val m)
forall val (m :: * -> *) a. Monad m => a -> NoCauseT val m a
forall val (m :: * -> *) a b.
Monad m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
forall val (m :: * -> *) a b.
Monad m =>
NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> NoCauseT val m a
$creturn :: forall val (m :: * -> *) a. Monad m => a -> NoCauseT val m a
>> :: NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
$c>> :: forall val (m :: * -> *) a b.
Monad m =>
NoCauseT val m a -> NoCauseT val m b -> NoCauseT val m b
>>= :: NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b
$c>>= :: forall val (m :: * -> *) a b.
Monad m =>
NoCauseT val m a -> (a -> NoCauseT val m b) -> NoCauseT val m b
$cp1Monad :: forall val (m :: * -> *). Monad m => Applicative (NoCauseT val m)
Monad)

instance (MonadError err m, AsEvaluationFailure err) =>
            MonadError (ErrorWithCause err val) (NoCauseT val m) where
    throwError :: ErrorWithCause err val -> NoCauseT val m a
throwError ErrorWithCause err val
_ = m a -> NoCauseT val m a
forall val (m :: * -> *) a. m a -> NoCauseT val m a
NoCauseT (m a -> NoCauseT val m a) -> m a -> NoCauseT val m a
forall a b. (a -> b) -> a -> b
$ err -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError err
forall err. AsEvaluationFailure err => err
evaluationFailure
    NoCauseT m a
a catchError :: NoCauseT val m a
-> (ErrorWithCause err val -> NoCauseT val m a) -> NoCauseT val m a
`catchError` ErrorWithCause err val -> NoCauseT val m a
h =
        m a -> NoCauseT val m a
forall val (m :: * -> *) a. m a -> NoCauseT val m a
NoCauseT (m a -> NoCauseT val m a) -> m a -> NoCauseT val m a
forall a b. (a -> b) -> a -> b
$ m a
a m a -> (err -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \err
err ->
            NoCauseT val m a -> m a
forall val (m :: * -> *) a. NoCauseT val m a -> m a
unNoCauseT (NoCauseT val m a -> m a)
-> (ErrorWithCause err val -> NoCauseT val m a)
-> ErrorWithCause err val
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorWithCause err val -> NoCauseT val m a
h (ErrorWithCause err val -> m a) -> ErrorWithCause err val -> m a
forall a b. (a -> b) -> a -> b
$ err -> Maybe val -> ErrorWithCause err val
forall err cause. err -> Maybe cause -> ErrorWithCause err cause
ErrorWithCause err
err Maybe val
forall a. Maybe a
Nothing

-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
-- For example the monad can be simply 'EvaluationResult'.
makeKnownOrFail :: (KnownType val a, MonadError err m, AsEvaluationFailure err) => a -> m val
makeKnownOrFail :: a -> m val
makeKnownOrFail = NoCauseT Any m val -> m val
forall val (m :: * -> *) a. NoCauseT val m a -> m a
unNoCauseT (NoCauseT Any m val -> m val)
-> (a -> NoCauseT Any m val) -> a -> m val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> NoCauseT Any m ()) -> Maybe Any -> a -> NoCauseT Any m val
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
_ -> () -> NoCauseT Any m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Maybe Any
forall a. Maybe a
Nothing

instance KnownTypeIn uni val a => KnownTypeIn uni val (EvaluationResult a) where
    makeKnown :: (Text -> m ()) -> Maybe cause -> EvaluationResult a -> m val
makeKnown Text -> m ()
_    Maybe cause
mayCause EvaluationResult a
EvaluationFailure     = AReview err () -> () -> Maybe cause -> m val
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
    makeKnown Text -> m ()
emit Maybe cause
mayCause (EvaluationSuccess a
x) = (Text -> m ()) -> Maybe cause -> a -> m val
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 a
x
    {-# INLINE makeKnown #-}

    -- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
    -- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function
    -- the programmer would be given an explicit 'EvaluationResult' value to handle, which means
    -- that when this value is 'EvaluationFailure', a PLC 'Error' was caught.
    -- I.e. it would essentially allow us to catch errors and handle them in a programmable way.
    -- We forbid this, because it complicates code and isn't supported by evaluation engines anyway.
    readKnown :: Maybe cause
-> val -> Either (ErrorWithCause err cause) (EvaluationResult a)
readKnown Maybe cause
mayCause val
_ =
        AReview err UnliftingError
-> UnliftingError
-> Maybe cause
-> Either (ErrorWithCause err cause) (EvaluationResult a)
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 UnliftingError
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Error catching is not supported" Maybe cause
mayCause
    {-# INLINE readKnown #-}

instance KnownTypeIn uni val a => KnownTypeIn uni val (Emitter a) where
    makeKnown :: (Text -> m ()) -> Maybe cause -> Emitter a -> m val
makeKnown Text -> m ()
emit Maybe cause
mayCause (Emitter forall (m :: * -> *). Monad m => (Text -> m ()) -> m a
k) = (Text -> m ()) -> m a
forall (m :: * -> *). Monad m => (Text -> m ()) -> m a
k Text -> m ()
emit m a -> (a -> m val) -> m val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Text -> m ()) -> Maybe cause -> a -> m val
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
    {-# INLINE makeKnown #-}

    -- TODO: we really should tear 'KnownType' apart into two separate type classes.
    readKnown :: Maybe cause -> val -> Either (ErrorWithCause err cause) (Emitter a)
readKnown Maybe cause
mayCause val
_ = AReview err UnliftingError
-> UnliftingError
-> Maybe cause
-> Either (ErrorWithCause err cause) (Emitter a)
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 UnliftingError
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Can't unlift an 'Emitter'" Maybe cause
mayCause
    {-# INLINE readKnown #-}

instance HasConstantIn uni val => KnownTypeIn uni val (SomeConstant uni rep) where
    makeKnown :: (Text -> m ()) -> Maybe cause -> SomeConstant uni rep -> m val
makeKnown Text -> m ()
_ Maybe cause
_ = (Some (ValueOf uni) -> m val) -> SomeConstant uni rep -> m val
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg ((Some (ValueOf uni) -> m val) -> SomeConstant uni rep -> m val)
-> (Some (ValueOf uni) -> m val) -> SomeConstant uni rep -> m val
forall a b. (a -> b) -> a -> b
$ val -> m val
forall (f :: * -> *) a. Applicative f => a -> f a
pure (val -> m val)
-> (Some (ValueOf uni) -> val) -> Some (ValueOf uni) -> m val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> val
forall term.
FromConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant
    {-# INLINE makeKnown #-}

    readKnown :: Maybe cause
-> val -> Either (ErrorWithCause err cause) (SomeConstant uni rep)
readKnown = ((Maybe cause
  -> val -> Either (ErrorWithCause err cause) (Some (ValueOf uni)))
 -> Maybe cause
 -> val
 -> Either (ErrorWithCause err cause) (SomeConstant uni rep))
-> (Maybe cause
    -> val -> Either (ErrorWithCause err cause) (Some (ValueOf uni)))
-> Maybe cause
-> val
-> Either (ErrorWithCause err cause) (SomeConstant uni rep)
forall a b. Coercible a b => (a -> b) -> a -> b
coerceVia (\Maybe cause
-> val -> Either (ErrorWithCause err cause) (Some (ValueOf uni))
asC Maybe cause
mayCause -> (Some (ValueOf uni) -> SomeConstant uni rep)
-> Either (ErrorWithCause err cause) (Some (ValueOf uni))
-> Either (ErrorWithCause err cause) (SomeConstant uni rep)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Some (ValueOf uni) -> SomeConstant uni rep
forall (uni :: * -> *) rep.
Some (ValueOf uni) -> SomeConstant uni rep
SomeConstant (Either (ErrorWithCause err cause) (Some (ValueOf uni))
 -> Either (ErrorWithCause err cause) (SomeConstant uni rep))
-> (val -> Either (ErrorWithCause err cause) (Some (ValueOf uni)))
-> val
-> Either (ErrorWithCause err cause) (SomeConstant uni rep)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe cause
-> val -> Either (ErrorWithCause err cause) (Some (ValueOf uni))
asC Maybe cause
mayCause) Maybe cause
-> val -> Either (ErrorWithCause err cause) (Some (ValueOf uni))
forall term err cause (m :: * -> *).
(AsConstant term, MonadError (ErrorWithCause err cause) m,
 AsUnliftingError err) =>
Maybe cause -> term -> m (Some (ValueOf (UniOf term)))
asConstant
    {-# INLINE readKnown #-}

instance uni ~ UniOf val => KnownTypeIn uni val (Opaque val rep) where
    makeKnown :: (Text -> m ()) -> Maybe cause -> Opaque val rep -> m val
makeKnown Text -> m ()
_ Maybe cause
_ = (val -> m val) -> Opaque val rep -> m val
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg val -> m val
forall (f :: * -> *) a. Applicative f => a -> f a
pure  -- A faster @pure . Opaque@.
    {-# INLINE makeKnown #-}

    readKnown :: Maybe cause
-> val -> Either (ErrorWithCause err cause) (Opaque val rep)
readKnown Maybe cause
_ = (Opaque val rep
 -> Either (ErrorWithCause err cause) (Opaque val rep))
-> val -> Either (ErrorWithCause err cause) (Opaque val rep)
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg Opaque val rep
-> Either (ErrorWithCause err cause) (Opaque val rep)
forall (f :: * -> *) a. Applicative f => a -> f a
pure  -- A faster @pure . Opaque@.
    {-# INLINE readKnown #-}

-- Utils

-- | Coerce the second argument to the result type of the first one. The motivation for this
-- function is that it's often more annoying to explicitly specify a target type for 'coerce' than
-- to constructor an explicit coercion function, so this combinator can be used in cases like that.
-- Plus the code reads better, as it becomes clear what and where gets wrapped/unwrapped.
coerceVia :: Coercible a b => (a -> b) -> a -> b
coerceVia :: (a -> b) -> a -> b
coerceVia a -> b
_ = a -> b
coerce
{-# INLINE coerceVia #-}

-- | Same as @\f -> f . coerce@, but does not create any closures and so is completely free.
coerceArg :: Coercible a b => (a -> r) -> b -> r
coerceArg :: (a -> r) -> b -> r
coerceArg = (a -> r) -> b -> r
coerce
{-# INLINE coerceArg #-}