{-# LANGUAGE QuantifiedConstraints #-}
-- Needed to connect PConst to Const
{-# OPTIONS_GHC -Wno-orphans #-}

module Plutarch.Extra.Const (
  -- * Type
  PConst (..),

  -- * Helper functions
  preconst,
) where

import Plutarch.Extra.Applicative (PApplicative (ppure), PApply (pliftA2))
import Plutarch.Extra.Boring (PBoring (pboring))
import Plutarch.Extra.Functor (
  PBifunctor (PSubcategoryLeft, PSubcategoryRight, pbimap, psecond),
  PFunctor (PSubcategory, pfmap),
  Plut,
 )
import Plutarch.Extra.TermCont (pmatchC)
import Plutarch.Num (PNum)
import Plutarch.Unsafe (punsafeCoerce)

{- | A value of type @a@ pretending to a be a value of type @b@.

 @since 1.0.0
-}
newtype PConst (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PConst (Term s a)
  deriving stock
    ( -- | @since 1.0.0
      forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PConst a b s) x -> PConst a b s
forall (a :: PType) (b :: PType) (s :: S) x.
PConst a b s -> Rep (PConst a b s) x
$cto :: forall (a :: PType) (b :: PType) (s :: S) x.
Rep (PConst a b s) x -> PConst a b s
$cfrom :: forall (a :: PType) (b :: PType) (s :: S) x.
PConst a b s -> Rep (PConst a b s) x
Generic
    )
  deriving anyclass
    ( -- | @since 1.0.0
      forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: PType) (b :: PType) (s :: S).
PConst a b s -> Term s (PInner (PConst a b))
forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PConst a b))
-> (PConst a b s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PConst a b))
-> (PConst a b s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (b :: PType) (s :: S) (b :: PType).
Term s (PInner (PConst a b))
-> (PConst a b s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PConst a b s -> Term s (PInner (PConst a b))
$cpcon' :: forall (a :: PType) (b :: PType) (s :: S).
PConst a b s -> Term s (PInner (PConst a b))
PlutusType
    )

-- | @since 1.4.0
instance DerivePlutusType (PConst a b) where
  type DPTStrat _ = PlutusTypeNewtype

-- | @since 1.0.0
deriving anyclass instance (PIsData a) => (PIsData (PConst a b))

-- | @since 1.0.0
deriving anyclass instance (PEq a) => PEq (PConst a b)

-- | @since 1.4.0
deriving anyclass instance (POrd a) => PPartialOrd (PConst a b)

-- | @since 1.0.0
deriving anyclass instance (POrd a) => POrd (PConst a b)

-- | @since 1.0.0
deriving anyclass instance (PIntegral a) => PIntegral (PConst a b)

-- | @since 1.4.0
deriving anyclass instance (PNum a) => PNum (PConst a b)

-- | @since 1.0.0
deriving anyclass instance (PShow a) => PShow (PConst a b)

-- | @since 3.1.0
instance PFunctor (PConst a) where
  type PSubcategory (PConst a) = Plut
  pfmap :: forall (a :: PType) (b :: PType) (s :: S).
(PSubcategory (PConst a) a, PSubcategory (PConst a) b) =>
Term s ((a :--> b) :--> (PConst a a :--> PConst a b))
pfmap = forall (f :: PType -> PType -> PType) (a :: PType) (b :: PType)
       (d :: PType) (s :: S).
(PBifunctor f, PSubcategoryLeft f a, PSubcategoryRight f b,
 PSubcategoryRight f d) =>
Term s ((b :--> d) :--> (f a b :--> f a d))
psecond

-- | @since 3.1.0
instance PBifunctor PConst where
  type PSubcategoryLeft PConst = Plut
  type PSubcategoryRight PConst = Plut
  pbimap :: forall (a :: PType) (b :: PType) (c :: PType) (d :: PType)
       (s :: S).
(PSubcategoryLeft PConst a, PSubcategoryLeft PConst c,
 PSubcategoryRight PConst b, PSubcategoryRight PConst d) =>
Term
  s ((a :--> c) :--> ((b :--> d) :--> (PConst a b :--> PConst c d)))
pbimap = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> c)
f Term s (b :--> d)
_ Term s (PConst a b)
t -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PConst Term s a
tx <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PConst a b)
t
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S). Term s a -> PConst a b s
PConst forall a b. (a -> b) -> a -> b
$ Term s (a :--> c)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
tx

-- | @since 1.0.0
instance
  (forall (s :: S). Semigroup (Term s a)) =>
  PApply (PConst a)
  where
  pliftA2 :: forall (a :: PType) (b :: PType) (c :: PType) (s :: S).
(PSubcategory (PConst a) a, PSubcategory (PConst a) b,
 PSubcategory (PConst a) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PConst a a :--> (PConst a b :--> PConst a c)))
pliftA2 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
_ Term s (PConst a a)
xs Term s (PConst a b)
ys -> forall (a :: PType) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PConst Term s a
tx <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PConst a a)
xs
      PConst Term s a
ty <- forall {r :: PType} (a :: PType) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PConst a b)
ys
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S). Term s a -> PConst a b s
PConst forall a b. (a -> b) -> a -> b
$ Term s a
tx forall a. Semigroup a => a -> a -> a
<> Term s a
ty

-- | @since 1.0.0
instance
  (forall (s :: S). Monoid (Term s a)) =>
  PApplicative (PConst a)
  where
  ppure :: forall (a :: PType) (s :: S).
PSubcategory (PConst a) a =>
Term s (a :--> PConst a a)
ppure = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
_ -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S). Term s a -> PConst a b s
PConst forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
mempty

-- | @since 1.2.0
instance (PBoring a) => PBoring (PConst a b) where
  pboring :: forall (s :: S). Term s (PConst a b)
pboring = forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S). Term s a -> PConst a b s
PConst forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). PBoring a => Term s a
pboring

{- | Since 'PConst' is only /pretending/ to be a value of another type, we can
 change what we \'pretend to be\' without having to rebuild. Essentially, this
 is 'punsafeCoerce', but because we're only changing a tag, we're not worried.

 @since 1.2.0
-}
preconst ::
  forall (c :: S -> Type) (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (PConst a b) ->
  Term s (PConst a c)
preconst :: forall (c :: PType) (a :: PType) (b :: PType) (s :: S).
Term s (PConst a b) -> Term s (PConst a c)
preconst = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce