{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

{- |
Module: Plutarch.Lift
Description: Conversion to and from Plutarch terms and Haskell types

This module defines functions, associated type families, and newtypes for use with
[@DerivingVia@](https://ryanglscott.github.io/papers/deriving-via.pdf) to allow
Plutarch to convert to and from PTypes and Haskell types.
-}
module Plutarch.Lift (
  -- * Converstion between Plutarch terms and Haskell types
  pconstant,
  plift,
  plift',
  LiftError (..),

  -- * Define your own conversion
  PConstantDecl (..),
  PLift,
  PConstant,
  DerivePConstantDirect (..),
  DerivePConstantViaNewtype (..),
  DerivePConstantViaBuiltin (..),

  -- * Internal use
  PUnsafeLiftDecl (..),
) where

import Control.Lens ((^?))
import Data.Coerce (Coercible, coerce)
import Data.Kind (Constraint, Type)
import Data.Text (Text)
import GHC.Stack (HasCallStack)
import Plutarch.Internal (ClosedTerm, Config (Config, tracingMode), PType, Term, compile, punsafeConstantInternal, pattern DoTracing)
import Plutarch.Internal.Evaluate (EvalError, evalScriptHuge)
import Plutarch.Script (unScript)
import PlutusCore qualified as PLC
import PlutusCore.Builtin (KnownTypeError, readKnownConstant)
import PlutusCore.Evaluation.Machine.Exception (_UnliftingErrorE)
import PlutusTx (BuiltinData, Data, builtinDataToData, dataToBuiltinData)
import PlutusTx.Builtins.Class (FromBuiltin, ToBuiltin, fromBuiltin, toBuiltin)
import UntypedPlutusCore qualified as UPLC

{- |
Laws:
 - It must be that @PConstantRepr (PLifted p)@ when encoded as a constant
   in UPLC (via the 'UntypedPlutusCore.Constant' constructor) is a valid @p@.
-}
class (PConstantDecl (PLifted p), PConstanted (PLifted p) ~ p) => PUnsafeLiftDecl (p :: PType) where
  type PLifted p = (r :: Type) | r -> p

{- | Class of Haskell types `h` that can be represented as a Plutus core builtin
and converted to a Plutarch type.

The Plutarch type is determined by `PConstanted h`. Its Plutus Core representation is given by `PConstantRepr h`.

This typeclass is closely tied with 'PLift'.

Laws:
 - @pconstantFromRepr . pconstantToRepr ≡ Just@
 - @(pconstantToRepr <$>) . pconstantFromRepr ≡ Just@
 - @plift . pfromData . flip ptryFrom fst . pconstant . PlutusTx.toData ≡ id@
 - @PlutusTx.fromData . plift . pforgetData . pdata . pconstant ≡ Just@

These laws must be upheld for the sake of soundness of the type system.
-}
class
  ( PUnsafeLiftDecl (PConstanted h)
  , PLC.DefaultUni `PLC.Includes` PConstantRepr h
  ) =>
  PConstantDecl (h :: Type)
  where
  type PConstantRepr h :: Type
  type PConstanted h :: PType
  pconstantToRepr :: h -> PConstantRepr h
  pconstantFromRepr :: PConstantRepr h -> Maybe h

{- | Class of Plutarch types `p` that can be converted to/from a Haskell type.

The Haskell type is determined by `PLifted p`.

This typeclass is closely tied with 'PConstant'.
-}
type PLift :: PType -> Constraint
type PLift = PUnsafeLiftDecl

{- | Create a Plutarch-level constant, from a Haskell value.
Example:
> pconstant @PInteger 42
-}
pconstant :: forall p s. PLift p => PLifted p -> Term s p
pconstant :: forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted p
x = forall (s :: S) (a :: PType).
Some @Type (ValueOf DefaultUni) -> Term s a
punsafeConstantInternal forall a b. (a -> b) -> a -> b
$ forall a (uni :: Type -> Type).
Includes @Type uni a =>
a -> Some @Type (ValueOf uni)
PLC.someValue @(PConstantRepr (PLifted p)) @PLC.DefaultUni forall a b. (a -> b) -> a -> b
$ forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr PLifted p
x

{-# HLINT ignore LiftError "Use camelCase" #-}

{- | Error during script evaluation.

 @since 1.2.1
-}
data LiftError
  = LiftError_EvalError EvalError
  | LiftError_KnownTypeError KnownTypeError
  | LiftError_FromRepr
  | LiftError_CompilationError Text
  deriving stock (LiftError -> LiftError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LiftError -> LiftError -> Bool
$c/= :: LiftError -> LiftError -> Bool
== :: LiftError -> LiftError -> Bool
$c== :: LiftError -> LiftError -> Bool
Eq)

{- | Convert a Plutarch term to the associated Haskell value. Fail otherwise.
This will fully evaluate the arbitrary closed expression, and convert the resulting value.
-}
plift' :: forall p. PUnsafeLiftDecl p => Config -> ClosedTerm p -> Either LiftError (PLifted p)
plift' :: forall (p :: PType).
PUnsafeLiftDecl p =>
Config -> ClosedTerm p -> Either LiftError (PLifted p)
plift' Config
config ClosedTerm p
prog = case forall (a :: PType). Config -> ClosedTerm a -> Either Text Script
compile Config
config ClosedTerm p
prog of
  Left Text
msg -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Text -> LiftError
LiftError_CompilationError Text
msg
  Right Script
script -> case Script -> (Either EvalError Script, ExBudget, [Text])
evalScriptHuge Script
script of
    (Right (Script -> Program DeBruijn DefaultUni DefaultFun ()
unScript -> UPLC.Program ()
_ Version ()
_ Term DeBruijn DefaultUni DefaultFun ()
term), ExBudget
_, [Text]
_) ->
      case forall val a. KnownBuiltinType val a => val -> ReadKnownM a
readKnownConstant Term DeBruijn DefaultUni DefaultFun ()
term of
        Right PConstantRepr (PLifted p)
r -> case forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr PConstantRepr (PLifted p)
r of
          Just PLifted p
h -> forall a b. b -> Either a b
Right PLifted p
h
          Maybe (PLifted p)
Nothing -> forall a b. a -> Either a b
Left LiftError
LiftError_FromRepr
        Left KnownTypeError
e -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ KnownTypeError -> LiftError
LiftError_KnownTypeError KnownTypeError
e
    (Left EvalError
e, ExBudget
_, [Text]
_) -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ EvalError -> LiftError
LiftError_EvalError EvalError
e

-- | Like `plift'` but throws on failure.
plift :: forall p. (HasCallStack, PLift p) => ClosedTerm p -> PLifted p
plift :: forall (p :: PType).
(HasCallStack, PLift p) =>
ClosedTerm p -> PLifted p
plift ClosedTerm p
prog = case forall (p :: PType).
PUnsafeLiftDecl p =>
Config -> ClosedTerm p -> Either LiftError (PLifted p)
plift' (Config {$sel:tracingMode:Config :: TracingMode
tracingMode = TracingMode
DoTracing}) ClosedTerm p
prog of
  Right PLifted p
x -> PLifted p
x
  Left LiftError
LiftError_FromRepr -> forall a. HasCallStack => [Char] -> a
error [Char]
"plift failed: pconstantFromRepr returned 'Nothing'"
  Left (LiftError_KnownTypeError KnownTypeError
e) ->
    let unliftErrMaybe :: Maybe Text
unliftErrMaybe = KnownTypeError
e forall s a. s -> Getting (First a) s a -> Maybe a
^? forall r. AsUnliftingError r => Prism' r Text
_UnliftingErrorE
     in forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
          [Char]
"plift failed: incorrect type: "
            forall a. Semigroup a => a -> a -> a
<> forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"absurd evaluation failure" forall a. Show a => a -> [Char]
show Maybe Text
unliftErrMaybe
  Left (LiftError_EvalError EvalError
e) -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"plift failed: erring term: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show EvalError
e
  Left (LiftError_CompilationError Text
msg) -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"plift failed: compilation failed: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Text
msg

{- | Newtype wrapper for deriving @PConstant@ when the wrapped type is directly
represented by a builtin UPLC type that is /not/ @Data@.

  Ex: @PInteger@ is directly represented as a builtin integer.
-}
newtype DerivePConstantDirect (h :: Type) (p :: PType) = DerivePConstantDirect h

instance
  (PLift p, PLC.DefaultUni `PLC.Includes` h) =>
  PConstantDecl (DerivePConstantDirect h p)
  where
  type PConstantRepr (DerivePConstantDirect h p) = h
  type PConstanted (DerivePConstantDirect h p) = p
  pconstantToRepr :: DerivePConstantDirect h p
-> PConstantRepr (DerivePConstantDirect h p)
pconstantToRepr = coerce :: forall a b. Coercible @Type a b => a -> b
coerce
  pconstantFromRepr :: PConstantRepr (DerivePConstantDirect h p)
-> Maybe (DerivePConstantDirect h p)
pconstantFromRepr = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible @Type a b => a -> b
coerce

{- | Newtype wrapper for deriving @PConstant@ when the wrapped type is represented
indirectly by a builtin UPLC type that is /not/ @Data@.

  Ex: @PPubKeyHash@ is a newtype to a @PByteString@ and @PByteString@ is directly
  represented as a builtin bytestring.

Polymorphic types can be derived as follows:

>newtype Foo a = Foo a
>
>newtype PFoo a s = PFoo (Term s a)
>
>instance forall a. PLift a => PUnsafeLiftDecl (PFoo a) where
>  type PLifted (PFoo a) = Foo (PLifted a)
>
>deriving via
>  ( DerivePConstantViaNewtype
>      (Foo a)
>      (PFoo (PConstanted a))
>      (PConstanted a)
>  )
>  instance
>    PConstant a =>
>    PConstantDecl (Foo a)
-}
newtype
  DerivePConstantViaNewtype
    (h :: Type)
    (p :: PType) -- PType to associate with the newtype
    (p' :: PType) -- Underlying UPLC representation type
  = -- | The Haskell newtype we are deriving a @PConstant@ instance for
    DerivePConstantViaNewtype h

{- | Type synonym to simplify deriving of @PConstant@ via @DerivePConstantViaNewtype@.

A newtype @Foo a@ is considered "Constantable" if:

- The wrapped type @a@ has a @PConstant@ instance.
- The lifted type of @a@ has a @PUnsafeLiftDecl@ instance.
- There is type equality between @a@ and @PLifted (PConstanted a)@.

These constraints are sufficient to derive a @PConstant@ instance for the newtype.

For deriving @PConstant@ for a wrapped type represented in UPLC as @Data@, see
@DerivePConstantViaData@.
-}
type PConstant :: Type -> Constraint
type PConstant a = (a ~ PLifted (PConstanted a), PConstantDecl a)

instance (PLift p, PLift p', Coercible h (PLifted p')) => PConstantDecl (DerivePConstantViaNewtype h p p') where
  type PConstantRepr (DerivePConstantViaNewtype h p p') = PConstantRepr (PLifted p')
  type PConstanted (DerivePConstantViaNewtype h p p') = p
  pconstantToRepr :: DerivePConstantViaNewtype h p p'
-> PConstantRepr (DerivePConstantViaNewtype h p p')
pconstantToRepr DerivePConstantViaNewtype h p p'
x = forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr @(PLifted p') forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible @Type a b => a -> b
coerce DerivePConstantViaNewtype h p p'
x
  pconstantFromRepr :: PConstantRepr (DerivePConstantViaNewtype h p p')
-> Maybe (DerivePConstantViaNewtype h p p')
pconstantFromRepr PConstantRepr (DerivePConstantViaNewtype h p p')
x = coerce :: forall a b. Coercible @Type a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr @(PLifted p') PConstantRepr (DerivePConstantViaNewtype h p p')
x

class ToBuiltin' a arep | a -> arep where
  toBuiltin' :: a -> arep

class FromBuiltin' arep a | arep -> a where
  fromBuiltin' :: arep -> a

-- FIXME this overlappable instance is nonsense and disregards the fundep
instance {-# OVERLAPPABLE #-} ToBuiltin a arep => ToBuiltin' a arep where
  toBuiltin' :: a -> arep
toBuiltin' = forall a arep. ToBuiltin a arep => a -> arep
toBuiltin

instance {-# OVERLAPPABLE #-} FromBuiltin arep a => FromBuiltin' arep a where
  fromBuiltin' :: arep -> a
fromBuiltin' = forall arep a. FromBuiltin arep a => arep -> a
fromBuiltin

instance ToBuiltin' Data BuiltinData where
  toBuiltin' :: Data -> BuiltinData
toBuiltin' = Data -> BuiltinData
dataToBuiltinData

instance FromBuiltin' BuiltinData Data where
  fromBuiltin' :: BuiltinData -> Data
fromBuiltin' = BuiltinData -> Data
builtinDataToData

newtype DerivePConstantViaBuiltin (h :: Type) (p :: PType) (p' :: PType) = DerivePConstantViaBuiltin h

instance
  ( PLift p
  , PLift p'
  , Coercible h h'
  , ToBuiltin' (PLifted p') h'
  , FromBuiltin' h' (PLifted p')
  ) =>
  PConstantDecl (DerivePConstantViaBuiltin h p p')
  where
  type PConstantRepr (DerivePConstantViaBuiltin h p p') = PConstantRepr (PLifted p')
  type PConstanted (DerivePConstantViaBuiltin h p p') = p
  pconstantToRepr :: DerivePConstantViaBuiltin h p p'
-> PConstantRepr (DerivePConstantViaBuiltin h p p')
pconstantToRepr DerivePConstantViaBuiltin h p p'
x = forall h. PConstantDecl h => h -> PConstantRepr h
pconstantToRepr @(PLifted p') forall a b. (a -> b) -> a -> b
$ forall arep a. FromBuiltin' arep a => arep -> a
fromBuiltin' (coerce :: forall a b. Coercible @Type a b => a -> b
coerce DerivePConstantViaBuiltin h p p'
x :: h')
  pconstantFromRepr :: PConstantRepr (DerivePConstantViaBuiltin h p p')
-> Maybe (DerivePConstantViaBuiltin h p p')
pconstantFromRepr PConstantRepr (DerivePConstantViaBuiltin h p p')
x = coerce :: forall a b. Coercible @Type a b => a -> b
coerce (forall a arep. ToBuiltin' a arep => a -> arep
toBuiltin' forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall h. PConstantDecl h => PConstantRepr h -> Maybe h
pconstantFromRepr @(PLifted p') PConstantRepr (DerivePConstantViaBuiltin h p p')
x :: Maybe h')