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

module Plutarch.Internal.PlutusType (
  PlutusType,
  PlutusTypeStratConstraint,
  PCon,
  PMatch,
  pcon',
  pmatch',
  pmatch,
  pcon,
  PInner,
  PlutusTypeStrat,
  DerivePlutusType,
  DPTStrat,
  DerivedPInner,
  derivedPCon,
  derivedPMatch,
  PVariant,
  PCovariant,
  PContravariant,
  PVariant',
  PCovariant',
  PContravariant',
) where

import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (ErrorMessage (ShowType, Text, (:<>:)), TypeError)
import Generics.SOP (All2)
import Plutarch.Internal.Generic (PCode)
import Plutarch.Internal.Quantification (PFix (PFix), PForall (PForall), PSome (PSome))
import Plutarch.Internal.Term (PType, Term, plam', plet, punsafeCoerce, (#), (:-->) (PLam))
import Plutarch.Internal.Witness (witness)

class PlutusTypeStrat (strategy :: Type) where
  type PlutusTypeStratConstraint strategy :: PType -> Constraint
  type DerivedPInner strategy (a :: PType) :: PType
  derivedPCon :: forall a s. (DerivePlutusType a, DPTStrat a ~ strategy) => a s -> Term s (DerivedPInner strategy a)
  derivedPMatch :: forall a s b. (DerivePlutusType a, DPTStrat a ~ strategy) => Term s (DerivedPInner strategy a) -> (a s -> Term s b) -> Term s b

class
  ( PInner a ~ DerivedPInner (DPTStrat a) a
  , PlutusTypeStrat (DPTStrat a)
  , PlutusTypeStratConstraint (DPTStrat a) a
  , PlutusType a
  ) =>
  DerivePlutusType (a :: PType)
  where
  type DPTStrat a :: Type
  type DPTStrat a = TypeError ('Text "Please specify a strategy for deriving PlutusType for type " ':<>: 'ShowType a)

class PlutusType (a :: PType) where
  type PInner a :: PType
  type PInner a = DerivedPInner (DPTStrat a) a
  type PCovariant' a :: Constraint
  type PCovariant' a = All2 PCovariant'' (PCode a)
  type PContravariant' a :: Constraint
  type PContravariant' a = All2 PContravariant'' (PCode a)
  type PVariant' a :: Constraint
  type PVariant' a = All2 PVariant'' (PCode a)
  pcon' :: forall s. a s -> Term s (PInner a)
  default pcon' :: DerivePlutusType a => forall s. a s -> Term s (PInner a)
  pcon' = let ()
_ = Proxy @Constraint (PlutusType a) -> ()
forall (c :: Constraint). c => Proxy @Constraint c -> ()
witness (forall {k} (t :: k). Proxy @k t
forall (t :: Constraint). Proxy @Constraint t
Proxy @(PlutusType a)) in a s -> Term s (PInner a)
a s -> Term s (DerivedPInner (DPTStrat a) a)
forall strategy (a :: PType) (s :: S).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
a s -> Term s (DerivedPInner strategy a)
forall (a :: PType) (s :: S).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (DPTStrat a :: Type)) =>
a s -> Term s (DerivedPInner (DPTStrat a) a)
derivedPCon

  pmatch' :: forall s b. Term s (PInner a) -> (a s -> Term s b) -> Term s b
  -- FIXME buggy GHC, needs AllowAmbiguousTypes
  default pmatch' :: DerivePlutusType a => forall s b. Term s (PInner a) -> (a s -> Term s b) -> Term s b
  pmatch' = Term s (PInner a) -> (a s -> Term s b) -> Term s b
Term s (DerivedPInner (DPTStrat a) a)
-> (a s -> Term s b) -> Term s b
forall strategy (a :: PType) (s :: S) (b :: PType).
(PlutusTypeStrat strategy, DerivePlutusType a,
 (DPTStrat a :: Type) ~ (strategy :: Type)) =>
Term s (DerivedPInner strategy a) -> (a s -> Term s b) -> Term s b
forall (a :: PType) (s :: S) (b :: PType).
(DerivePlutusType a,
 (DPTStrat a :: Type) ~ (DPTStrat a :: Type)) =>
Term s (DerivedPInner (DPTStrat a) a)
-> (a s -> Term s b) -> Term s b
derivedPMatch

{-# DEPRECATED PCon "Use PlutusType" #-}
type PCon = PlutusType
{-# DEPRECATED PMatch "Use PlutusType" #-}
type PMatch = PlutusType

-- | Construct a Plutarch Term via a Haskell datatype
pcon :: PlutusType a => a s -> Term s a
pcon :: forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon a s
x = Term s (PInner a) -> Term s a
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce (a s -> Term s (PInner a)
forall (s :: S). a s -> Term s (PInner a)
forall (a :: PType) (s :: S).
PlutusType a =>
a s -> Term s (PInner a)
pcon' a s
x)

-- | Pattern match over Plutarch Terms via a Haskell datatype
pmatch :: PlutusType a => Term s a -> (a s -> Term s b) -> Term s b
pmatch :: forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s a
x = Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (s :: S) (b :: PType).
Term s (PInner a) -> (a s -> Term s b) -> Term s b
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s (PInner a) -> (a s -> Term s b) -> Term s b
pmatch' (Term s a -> Term s (PInner a)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s a
x)

class PCovariant' a => PCovariant'' a
instance PCovariant' a => PCovariant'' a

class PContravariant' a => PContravariant'' a
instance PContravariant' a => PContravariant'' a

class PVariant' a => PVariant'' a
instance PVariant' a => PVariant'' a

class (forall t. PCovariant'' t => PCovariant'' (a t)) => PCovariant a
instance (forall t. PCovariant'' t => PCovariant'' (a t)) => PCovariant a

class (forall t. PCovariant'' t => PContravariant'' (a t)) => PContravariant a
instance (forall t. PCovariant'' t => PContravariant'' (a t)) => PContravariant a

class (forall t. PVariant'' t => PVariant'' (a t)) => PVariant a
instance (forall t. PVariant'' t => PVariant'' (a t)) => PVariant a

instance PlutusType (a :--> b) where
  type PInner (a :--> b) = a :--> b
  type PCovariant' (a :--> b) = (PContravariant' a, PCovariant' b)
  type PContravariant' (a :--> b) = (PCovariant' a, PContravariant' b)
  type PVariant' (a :--> b) = (PVariant' a, PVariant' b)
  pcon' :: forall (s :: S). (:-->) a b s -> Term s (PInner (a :--> b))
pcon' (PLam Term s a -> Term s b
f) = (Term s a -> Term s b) -> Term s (a :--> b)
forall (s :: S) (a :: PType) (b :: PType).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' Term s a -> Term s b
f
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (a :--> b))
-> ((:-->) a b s -> Term s b) -> Term s b
pmatch' Term s (PInner (a :--> b))
f (:-->) a b s -> Term s b
g = Term s (PInner (a :--> b))
-> (Term s (PInner (a :--> b)) -> Term s b) -> Term s b
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s (PInner (a :--> b))
f \Term s (PInner (a :--> b))
f' -> (:-->) a b s -> Term s b
g ((Term s a -> Term s b) -> (:-->) a b s
forall (a :: PType) (b :: PType) (s :: S).
(Term s a -> Term s b) -> (:-->) a b s
PLam (Term s (a :--> b)
Term s (PInner (a :--> b))
f' #))

instance PlutusType (PForall f) where
  type PInner (PForall f) = PForall f
  pcon' :: forall (s :: S). PForall @a f s -> Term s (PInner (PForall @a f))
pcon' (PForall forall (x :: a). Term s (f x)
x) = Term s (f (Any @a)) -> Term s (PInner (PForall @a f))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (f (Any @a))
forall (x :: a). Term s (f x)
x
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PForall @a f))
-> (PForall @a f s -> Term s b) -> Term s b
pmatch' Term s (PInner (PForall @a f))
x PForall @a f s -> Term s b
f = PForall @a f s -> Term s b
f ((forall (x :: a). Term s (f x)) -> PForall @a f s
forall a (b :: a -> PType) (s :: S).
(forall (x :: a). Term s (b x)) -> PForall @a b s
PForall ((forall (x :: a). Term s (f x)) -> PForall @a f s)
-> (forall (x :: a). Term s (f x)) -> PForall @a f s
forall a b. (a -> b) -> a -> b
$ Term s (PInner (PForall @a f)) -> Term s (f x)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PForall @a f))
x)

instance PlutusType (PSome f) where
  type PInner (PSome f) = PSome f
  pcon' :: forall (s :: S). PSome @a f s -> Term s (PInner (PSome @a f))
pcon' (PSome Term s (f x)
x) = Term s (f x) -> Term s (PInner (PSome @a f))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (f x)
x
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PSome @a f))
-> (PSome @a f s -> Term s b) -> Term s b
pmatch' Term s (PInner (PSome @a f))
x PSome @a f s -> Term s b
f = PSome @a f s -> Term s b
f (Term s (f (Any @a)) -> PSome @a f s
forall a (b :: a -> PType) (s :: S) (x :: a).
Term s (b x) -> PSome @a b s
PSome (Term s (f (Any @a)) -> PSome @a f s)
-> Term s (f (Any @a)) -> PSome @a f s
forall a b. (a -> b) -> a -> b
$ Term s (PInner (PSome @a f)) -> Term s (f (Any @a))
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s (PInner (PSome @a f))
x)

instance PlutusType (PFix f) where
  type PInner (PFix f) = f (PFix f)
  pcon' :: forall (s :: S). PFix f s -> Term s (PInner (PFix f))
pcon' (PFix Term s (f (PFix f))
x) = Term s (f (PFix f))
Term s (PInner (PFix f))
x
  pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PFix f)) -> (PFix f s -> Term s b) -> Term s b
pmatch' Term s (PInner (PFix f))
x PFix f s -> Term s b
f = PFix f s -> Term s b
f (Term s (f (PFix f)) -> PFix f s
forall (f :: PType -> PType) (s :: S).
Term s (f (PFix f)) -> PFix f s
PFix Term s (f (PFix f))
Term s (PInner (PFix f))
x)