{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Builtin.KnownType
( KnownTypeError
, throwKnownTypeErrorWithCause
, KnownBuiltinTypeIn
, KnownBuiltinType
, MakeKnownM
, ReadKnownM
, readKnownConstant
, MakeKnownIn (..)
, MakeKnown
, ReadKnownIn (..)
, ReadKnown
, makeKnownRun
, makeKnownOrFail
, readKnownSelf
) where
import PlutusPrelude (reoption)
import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.Polymorphism
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
import PlutusCore.Evaluation.Result
import Control.Lens ((#))
import Control.Lens.TH (makeClassyPrisms)
import Control.Monad.Except
import Data.Coerce
import Data.DList (DList)
import Data.String
import Data.Text (Text)
import GHC.Exts (inline, oneShot)
import GHC.TypeLits
import Universe
type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a)
type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a
data KnownTypeError
= KnownTypeUnliftingError UnliftingError
| KnownTypeEvaluationFailure
deriving stock (KnownTypeError -> KnownTypeError -> Bool
(KnownTypeError -> KnownTypeError -> Bool)
-> (KnownTypeError -> KnownTypeError -> Bool) -> Eq KnownTypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KnownTypeError -> KnownTypeError -> Bool
$c/= :: KnownTypeError -> KnownTypeError -> Bool
== :: KnownTypeError -> KnownTypeError -> Bool
$c== :: KnownTypeError -> KnownTypeError -> Bool
Eq)
makeClassyPrisms ''KnownTypeError
instance AsUnliftingError KnownTypeError where
_UnliftingError :: p UnliftingError (f UnliftingError)
-> p KnownTypeError (f KnownTypeError)
_UnliftingError = p UnliftingError (f UnliftingError)
-> p KnownTypeError (f KnownTypeError)
forall r. AsKnownTypeError r => Prism' r UnliftingError
_KnownTypeUnliftingError
instance AsEvaluationFailure KnownTypeError where
_EvaluationFailure :: p () (f ()) -> p KnownTypeError (f KnownTypeError)
_EvaluationFailure = KnownTypeError -> Prism' KnownTypeError ()
forall err. Eq err => err -> Prism' err ()
_EvaluationFailureVia KnownTypeError
KnownTypeEvaluationFailure
throwKnownTypeErrorWithCause
:: (MonadError (ErrorWithCause err cause) m, AsUnliftingError err, AsEvaluationFailure err)
=> ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause :: ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause (ErrorWithCause KnownTypeError
rkErr Maybe cause
cause) = case KnownTypeError
rkErr of
KnownTypeUnliftingError UnliftingError
unlErr -> AReview err UnliftingError
-> UnliftingError -> Maybe cause -> m void
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
unlErr Maybe cause
cause
KnownTypeError
KnownTypeEvaluationFailure -> AReview err () -> () -> Maybe cause -> m void
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
cause
typeMismatchError
:: GShow uni
=> uni (Esc a)
-> uni (Esc b)
-> UnliftingError
typeMismatchError :: uni (Esc a) -> uni (Esc b) -> UnliftingError
typeMismatchError uni (Esc a)
uniExp uni (Esc b)
uniAct = 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]
++ uni (Esc a) -> String
forall k (t :: k -> *) (a :: k). GShow t => t a -> String
gshow uni (Esc a)
uniExp
, String
"; actual: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ uni (Esc b) -> String
forall k (t :: k -> *) (a :: k). GShow t => t a -> String
gshow uni (Esc b)
uniAct
]
{-# NOINLINE typeMismatchError #-}
type MakeKnownM cause = ExceptT (ErrorWithCause KnownTypeError cause) Emitter
type ReadKnownM cause = Either (ErrorWithCause KnownTypeError cause)
readKnownConstant
:: forall val a cause. KnownBuiltinType val a
=> Maybe cause -> val -> ReadKnownM cause a
readKnownConstant :: Maybe cause -> val -> ReadKnownM cause a
readKnownConstant Maybe cause
mayCause val
val = Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf (UniOf val)))
forall term err cause.
(HasConstant term, AsUnliftingError err) =>
Maybe cause
-> term
-> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf term)))
asConstant Maybe cause
mayCause val
val Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf (UniOf val)))
-> (Some (ValueOf (UniOf val)) -> ReadKnownM cause a)
-> ReadKnownM cause a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Some (ValueOf (UniOf val)) -> ReadKnownM cause a)
-> Some (ValueOf (UniOf val)) -> ReadKnownM 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)
uniExp 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)
uniAct of
Just Esc a :~: Esc a
Refl -> a -> Either (ErrorWithCause KnownTypeError cause) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x
Maybe (Esc a :~: Esc a)
Nothing -> ErrorWithCause KnownTypeError cause -> ReadKnownM cause a
forall a b. a -> Either a b
Left (ErrorWithCause KnownTypeError cause -> ReadKnownM cause a)
-> ErrorWithCause KnownTypeError cause -> ReadKnownM cause a
forall a b. (a -> b) -> a -> b
$
KnownTypeError
-> Maybe cause -> ErrorWithCause KnownTypeError cause
forall err cause. err -> Maybe cause -> ErrorWithCause err cause
ErrorWithCause (Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError)
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError (Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError))
-> UnliftingError -> KnownTypeError
forall t b. AReview t b -> b -> t
# UniOf val (Esc a) -> UniOf val (Esc a) -> UnliftingError
forall (uni :: * -> *) a b.
GShow uni =>
uni (Esc a) -> uni (Esc b) -> UnliftingError
typeMismatchError UniOf val (Esc a)
uniExp UniOf val (Esc a)
uniAct) Maybe cause
mayCause
{-# INLINE readKnownConstant #-}
class uni ~ UniOf val => MakeKnownIn uni val a where
makeKnown :: Maybe cause -> a -> MakeKnownM cause val
default makeKnown :: KnownBuiltinType val a => Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
_ a
x = val -> MakeKnownM cause val
forall (f :: * -> *) a. Applicative f => a -> f a
pure (val -> MakeKnownM cause val)
-> (a -> val) -> a -> MakeKnownM cause val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> val
forall term.
HasConstant 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 -> MakeKnownM cause val) -> a -> MakeKnownM cause val
forall a b. (a -> b) -> a -> b
$! a
x
{-# INLINE makeKnown #-}
type MakeKnown val = MakeKnownIn (UniOf val) val
class uni ~ UniOf val => ReadKnownIn uni val a where
readKnown :: Maybe cause -> val -> ReadKnownM cause a
default readKnown :: KnownBuiltinType val a => Maybe cause -> val -> ReadKnownM cause a
readKnown = (Maybe cause -> val -> ReadKnownM cause a)
-> Maybe cause -> val -> ReadKnownM cause a
forall a. a -> a
inline Maybe cause -> val -> ReadKnownM cause a
forall val a cause.
KnownBuiltinType val a =>
Maybe cause -> val -> ReadKnownM cause a
readKnownConstant
{-# INLINE readKnown #-}
type ReadKnown val = ReadKnownIn (UniOf val) val
makeKnownRun
:: MakeKnownIn uni val a
=> Maybe cause -> a -> (ReadKnownM cause val, DList Text)
makeKnownRun :: Maybe cause -> a -> (ReadKnownM cause val, DList Text)
makeKnownRun Maybe cause
mayCause = Emitter (ReadKnownM cause val)
-> (ReadKnownM cause val, DList Text)
forall a. Emitter a -> (a, DList Text)
runEmitter (Emitter (ReadKnownM cause val)
-> (ReadKnownM cause val, DList Text))
-> (a -> Emitter (ReadKnownM cause val))
-> a
-> (ReadKnownM cause val, DList Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT (ErrorWithCause KnownTypeError cause) Emitter val
-> Emitter (ReadKnownM cause val)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (ErrorWithCause KnownTypeError cause) Emitter val
-> Emitter (ReadKnownM cause val))
-> (a -> ExceptT (ErrorWithCause KnownTypeError cause) Emitter val)
-> a
-> Emitter (ReadKnownM cause val)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe cause
-> a -> ExceptT (ErrorWithCause KnownTypeError cause) Emitter val
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause
{-# INLINE makeKnownRun #-}
makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
makeKnownOrFail :: a -> EvaluationResult val
makeKnownOrFail = Either (ErrorWithCause KnownTypeError Any) val
-> EvaluationResult val
forall (f :: * -> *) (g :: * -> *) a.
(Foldable f, Alternative g) =>
f a -> g a
reoption (Either (ErrorWithCause KnownTypeError Any) val
-> EvaluationResult val)
-> (a -> Either (ErrorWithCause KnownTypeError Any) val)
-> a
-> EvaluationResult val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either (ErrorWithCause KnownTypeError Any) val, DList Text)
-> Either (ErrorWithCause KnownTypeError Any) val
forall a b. (a, b) -> a
fst ((Either (ErrorWithCause KnownTypeError Any) val, DList Text)
-> Either (ErrorWithCause KnownTypeError Any) val)
-> (a
-> (Either (ErrorWithCause KnownTypeError Any) val, DList Text))
-> a
-> Either (ErrorWithCause KnownTypeError Any) val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Any
-> a
-> (Either (ErrorWithCause KnownTypeError Any) val, DList Text)
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> (ReadKnownM cause val, DList Text)
makeKnownRun Maybe Any
forall a. Maybe a
Nothing
{-# INLINE makeKnownOrFail #-}
readKnownSelf
:: ( ReadKnown val a
, AsUnliftingError err, AsEvaluationFailure err
)
=> val -> Either (ErrorWithCause err val) a
readKnownSelf :: val -> Either (ErrorWithCause err val) a
readKnownSelf val
val = (ErrorWithCause KnownTypeError val
-> Either (ErrorWithCause err val) a)
-> (a -> Either (ErrorWithCause err val) a)
-> Either (ErrorWithCause KnownTypeError val) a
-> Either (ErrorWithCause err val) a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ErrorWithCause KnownTypeError val
-> Either (ErrorWithCause err val) a
forall err cause (m :: * -> *) void.
(MonadError (ErrorWithCause err cause) m, AsUnliftingError err,
AsEvaluationFailure err) =>
ErrorWithCause KnownTypeError cause -> m void
throwKnownTypeErrorWithCause a -> Either (ErrorWithCause err val) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (ErrorWithCause KnownTypeError val) a
-> Either (ErrorWithCause err val) a)
-> Either (ErrorWithCause KnownTypeError val) a
-> Either (ErrorWithCause err val) a
forall a b. (a -> b) -> a -> b
$ Maybe val -> val -> Either (ErrorWithCause KnownTypeError val) a
forall (uni :: * -> *) val a cause.
ReadKnownIn uni val a =>
Maybe cause -> val -> ReadKnownM cause a
readKnown (val -> Maybe val
forall a. a -> Maybe a
Just val
val) val
val
{-# INLINE readKnownSelf #-}
instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
makeKnown :: Maybe cause -> EvaluationResult a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause EvaluationResult a
EvaluationFailure = AReview KnownTypeError ()
-> () -> Maybe cause -> MakeKnownM cause 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 KnownTypeError ()
forall err. AsEvaluationFailure err => Prism' err ()
_EvaluationFailure () Maybe cause
mayCause
makeKnown Maybe cause
mayCause (EvaluationSuccess a
x) = Maybe cause -> a -> MakeKnownM cause val
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause a
x
{-# INLINE makeKnown #-}
instance
( TypeError ('Text "‘EvaluationResult’ cannot appear in the type of an argument")
, uni ~ UniOf val
) => ReadKnownIn uni val (EvaluationResult a) where
readKnown :: Maybe cause -> val -> ReadKnownM cause (EvaluationResult a)
readKnown Maybe cause
mayCause val
_ =
(Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError))
-> UnliftingError
-> Maybe cause
-> ReadKnownM 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 Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError)
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Panic: 'TypeError' was bypassed" Maybe cause
mayCause
instance MakeKnownIn uni val a => MakeKnownIn uni val (Emitter a) where
makeKnown :: Maybe cause -> Emitter a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause Emitter a
a = Emitter a
-> ExceptT (ErrorWithCause KnownTypeError cause) Emitter a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Emitter a
a ExceptT (ErrorWithCause KnownTypeError cause) Emitter a
-> (a -> MakeKnownM cause val) -> MakeKnownM cause val
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe cause -> a -> MakeKnownM cause val
forall (uni :: * -> *) val a cause.
MakeKnownIn uni val a =>
Maybe cause -> a -> MakeKnownM cause val
makeKnown Maybe cause
mayCause
{-# INLINE makeKnown #-}
instance
( TypeError ('Text "‘Emitter’ cannot appear in the type of an argument")
, uni ~ UniOf val
) => ReadKnownIn uni val (Emitter a) where
readKnown :: Maybe cause -> val -> ReadKnownM cause (Emitter a)
readKnown Maybe cause
mayCause val
_ =
(Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError))
-> UnliftingError -> Maybe cause -> ReadKnownM 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 Tagged UnliftingError (Identity UnliftingError)
-> Tagged KnownTypeError (Identity KnownTypeError)
forall r. AsUnliftingError r => Prism' r UnliftingError
_UnliftingError UnliftingError
"Panic: 'TypeError' was bypassed" Maybe cause
mayCause
instance HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) where
makeKnown :: Maybe cause -> SomeConstant uni rep -> MakeKnownM cause val
makeKnown Maybe cause
_ = (Some (ValueOf uni) -> MakeKnownM cause val)
-> SomeConstant uni rep -> MakeKnownM cause val
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg ((Some (ValueOf uni) -> MakeKnownM cause val)
-> SomeConstant uni rep -> MakeKnownM cause val)
-> (Some (ValueOf uni) -> MakeKnownM cause val)
-> SomeConstant uni rep
-> MakeKnownM cause val
forall a b. (a -> b) -> a -> b
$ val -> MakeKnownM cause val
forall (f :: * -> *) a. Applicative f => a -> f a
pure (val -> MakeKnownM cause val)
-> (Some (ValueOf uni) -> val)
-> Some (ValueOf uni)
-> MakeKnownM cause val
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf uni) -> val
forall term.
HasConstant term =>
Some (ValueOf (UniOf term)) -> term
fromConstant
{-# INLINE makeKnown #-}
instance HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) where
readKnown :: Maybe cause -> val -> ReadKnownM cause (SomeConstant uni rep)
readKnown = ((Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni)))
-> Maybe cause -> val -> ReadKnownM cause (SomeConstant uni rep))
-> (Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni)))
-> Maybe cause
-> val
-> ReadKnownM cause (SomeConstant uni rep)
forall a b. Coercible a b => (a -> b) -> a -> b
coerceVia (\Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni))
asC Maybe cause
mayCause -> (Some (ValueOf uni) -> SomeConstant uni rep)
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni))
-> ReadKnownM 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 KnownTypeError cause) (Some (ValueOf uni))
-> ReadKnownM cause (SomeConstant uni rep))
-> (val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni)))
-> val
-> ReadKnownM cause (SomeConstant uni rep)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni))
asC Maybe cause
mayCause) Maybe cause
-> val
-> Either
(ErrorWithCause KnownTypeError cause) (Some (ValueOf uni))
forall term err cause.
(HasConstant term, AsUnliftingError err) =>
Maybe cause
-> term
-> Either (ErrorWithCause err cause) (Some (ValueOf (UniOf term)))
asConstant
{-# INLINE readKnown #-}
instance uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) where
makeKnown :: Maybe cause -> Opaque val rep -> MakeKnownM cause val
makeKnown Maybe cause
_ = (val -> MakeKnownM cause val)
-> Opaque val rep -> MakeKnownM cause val
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg val -> MakeKnownM cause val
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE makeKnown #-}
instance uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) where
readKnown :: Maybe cause -> val -> ReadKnownM cause (Opaque val rep)
readKnown Maybe cause
_ = (Opaque val rep -> ReadKnownM cause (Opaque val rep))
-> val -> ReadKnownM cause (Opaque val rep)
forall a b r. Coercible a b => (a -> r) -> b -> r
coerceArg Opaque val rep -> ReadKnownM cause (Opaque val rep)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
{-# INLINE readKnown #-}
coerceVia :: Coercible a b => (a -> b) -> a -> b
coerceVia :: (a -> b) -> a -> b
coerceVia a -> b
_ = a -> b
coerce
{-# INLINE coerceVia #-}
coerceArg :: Coercible a b => (a -> r) -> b -> r
coerceArg :: (a -> r) -> b -> r
coerceArg = (a -> r) -> b -> r
coerce
{-# INLINE coerceArg #-}