module Plutarch.Extra.State (
  PState,
  pstate,
  prunState,
  pevalState,
  pexecState,
  pget,
  pput,
  pmodify,
) where

import Plutarch.Extra.Applicative (PApplicative (ppure), PApply (pliftA2))
import Plutarch.Extra.Bind (PBind ((#>>=)))
import Plutarch.Extra.Functor (PFunctor (PSubcategory, pfmap), Plut)
import Plutarch.Extra.TermCont (pmatchC)

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

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

-- | @since 3.1.0
instance PFunctor (PState s) where
  type PSubcategory (PState s) = Plut
  pfmap :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PState s) a, PSubcategory (PState s) b) =>
Term s ((a :--> b) :--> (PState s a :--> PState s b))
pfmap = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(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)
f Term s (PState s a)
state -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PState Term s (s :--> PPair s a)
g <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PState s a)
state
      forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
s -> forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (s :--> PPair s a)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s)

-- | @since 1.0.0
instance PApply (PState s) where
  pliftA2 :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type) (s :: S).
(PSubcategory (PState s) a, PSubcategory (PState s) b,
 PSubcategory (PState s) c) =>
Term
  s
  ((a :--> (b :--> c))
   :--> (PState s a :--> (PState s b :--> PState s c)))
pliftA2 = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(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))
f Term s (PState s a)
xs Term s (PState s b)
ys -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
      PState Term s (s :--> PPair s a)
g <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PState s a)
xs
      PState Term s (s :--> PPair s b)
h <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PState s 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 :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$
        forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
s -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
          PPair Term s s
s' Term s a
x <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (Term s (s :--> PPair s a)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s)
          PPair Term s s
s'' Term s b
y <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (Term s (s :--> PPair s b)
h forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s')
          forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s s
s'' forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y

-- | @since 1.0.0
instance PApplicative (PState s) where
  ppure :: forall (a :: S -> Type) (s :: S).
PSubcategory (PState s) a =>
Term s (a :--> PState s a)
ppure =
    forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
s -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s s
s forall a b. (a -> b) -> a -> b
$ Term s a
x

-- | @since 3.0.1
instance PBind (PState s) where
  {-# INLINEABLE (#>>=) #-}
  Term s (PState s a)
xs #>>= :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(PSubcategory (PState s) a, PSubcategory (PState s) b) =>
Term s (PState s a)
-> Term s (a :--> PState s b) -> Term s (PState s b)
#>>= Term s (a :--> PState s b)
f = forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PState s a)
xs forall a b. (a -> b) -> a -> b
$ \case
    PState Term s (s :--> PPair s a)
g -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
s -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (s :--> PPair s a)
g forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s) forall a b. (a -> b) -> a -> b
$ \case
      PPair Term s s
s' Term s a
res -> forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (a :--> PState s b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
res) forall a b. (a -> b) -> a -> b
$ \case
        PState Term s (s :--> PPair s b)
h -> Term s (s :--> PPair s b)
h forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s'

{- | Lift a Plutarch lambda into 'PState'.

 @since 1.0.0
-}
pstate ::
  forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
  Term s' ((s :--> PPair s a) :--> PState s a)
pstate :: forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' ((s :--> PPair s a) :--> PState s a)
pstate = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState

-- | @since 1.0.0
prunState ::
  forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
  Term s' (PState s a :--> s :--> PPair s a)
prunState :: forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (PState s a :--> (s :--> PPair s a))
prunState = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PState s a)
comp Term s s
state -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PState Term s (s :--> PPair s a)
f <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC Term s (PState s a)
comp
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Term s (s :--> PPair s a)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
state

-- | @since 1.0.0
pevalState ::
  forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
  Term s' (PState s a :--> s :--> a)
pevalState :: forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (PState s a :--> (s :--> a))
pevalState = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PState s a)
comp Term s s
state -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PPair Term s s
_ Term s a
x <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (PState s a :--> (s :--> PPair s a))
prunState forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PState s a)
comp forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
state)
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s a
x

-- | @since 1.0.0
pexecState ::
  forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
  Term s' (PState s a :--> s :--> s)
pexecState :: forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (PState s a :--> (s :--> s))
pexecState = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PState s a)
comp Term s s
state -> forall (a :: S -> Type) (s :: S). TermCont s (Term s a) -> Term s a
unTermCont forall a b. (a -> b) -> a -> b
$ do
    PPair Term s s
state' Term s a
_ <- forall {r :: S -> Type} (a :: S -> Type) (s :: S).
PlutusType a =>
Term s a -> TermCont s (a s)
pmatchC (forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (PState s a :--> (s :--> PPair s a))
prunState forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PState s a)
comp forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
state)
    forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s s
state'

-- | @since 1.0.0
pget ::
  forall (s :: S -> Type) (s' :: S).
  Term s' (PState s s)
pget :: forall (s :: S -> Type) (s' :: S). Term s' (PState s s)
pget = forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s' s
s -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s' s
s forall a b. (a -> b) -> a -> b
$ Term s' s
s

-- | @since 1.0.0
pput ::
  forall (s :: S -> Type) (s' :: S).
  Term s' (s :--> PState s PUnit)
pput :: forall (s :: S -> Type) (s' :: S). Term s' (s :--> PState s PUnit)
pput = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
x -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
_ -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s s
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k). PUnit s
PUnit

-- | @since 1.0.0
pmodify ::
  forall (s :: S -> Type) (s' :: S).
  Term s' ((s :--> s) :--> PState s PUnit)
pmodify :: forall (s :: S -> Type) (s' :: S).
Term s' ((s :--> s) :--> PState s PUnit)
pmodify = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (s :--> s)
f -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: S -> Type) (a :: S -> Type) (s' :: S).
Term s' (s :--> PPair s a) -> PState s a s'
PState forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s s
s -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair (Term s (s :--> s)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s s
s) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall {k} (s :: k). PUnit s
PUnit