module Plutarch.Internal.Fix (pfixHoisted, pfix, pfixInline) where

import Data.Kind (Type)
import Plutarch.Builtin.Opaque (POpaque)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plam',
  punsafeCoerce,
  (#),
  (:-->),
 )

{- | Fixpoint recursion, used to encode recursive functions.

= Note

This fixpoint combinator is /hoisted/, which allows for the smallest code
size. However, in terms of execution units, 'pfixHoisted' is the least
efficient.

'pfixHoisted' used to be the default fixpoint combinator in Plutarch. If you
used 'pfix' before, and want to maintain identical behaviour, use this
function.

= Example

Additional examples can be found in @examples/Recursion.hs@.

> iterateN' ::
>  Term s (PInteger :--> (a :--> a) :--> a :--> a) ->
>  Term s PInteger ->
>  Term s (a :--> a) ->
>  Term s a
> iterateN' self n f x =
>    pif (n #== 0)
>        x
>        (self # n - 1 #$ f x)
>
> iterateN :: Term s (PInteger :--> (a :--> a) :--> a :--> a)
> iterateN = pfixHoisted #$ plam iterateN'

@since 1.12.0
-}
pfixHoisted :: Term s (((a :--> b) :--> a :--> b) :--> a :--> b)
pfixHoisted :: forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfixHoisted = (forall (s' :: S).
 Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
 -> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> (forall (s' :: S).
    Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall a b. (a -> b) -> a -> b
$
  Term
  s'
  (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
   :--> Any @(S -> Type))
-> Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce (Term
   s'
   (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
    :--> Any @(S -> Type))
 -> Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> Term
     s'
     (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
      :--> Any @(S -> Type))
-> Term s' (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall a b. (a -> b) -> a -> b
$
    (Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
 -> Term s' (Any @(S -> Type)))
-> Term
     s'
     (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
      :--> Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' ((Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
  -> Term s' (Any @(S -> Type)))
 -> Term
      s'
      (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
       :--> Any @(S -> Type)))
-> (Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
    -> Term s' (Any @(S -> Type)))
-> Term
     s'
     (((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
      :--> Any @(S -> Type))
forall a b. (a -> b) -> a -> b
$ \Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
f ->
      (Term s' POpaque -> Term s' (Any @(S -> Type)))
-> Term s' (POpaque :--> Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' (\(Term s' POpaque
x :: Term s POpaque) -> Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
f Term s' ((POpaque :--> Any @(S -> Type)) :--> Any @(S -> Type))
-> Term s' (POpaque :--> Any @(S -> Type))
-> Term s' (Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' POpaque -> Term s' (Any @(S -> Type)))
-> Term s' (POpaque :--> Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' (\(Term s' POpaque
v :: Term s POpaque) -> Term s' POpaque
-> Term s' (POpaque :--> (POpaque :--> Any @(S -> Type)))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s' POpaque
x Term s' (POpaque :--> (POpaque :--> Any @(S -> Type)))
-> Term s' POpaque -> Term s' (POpaque :--> Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' POpaque
x Term s' (POpaque :--> Any @(S -> Type))
-> Term s' POpaque -> Term s' (Any @(S -> Type))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' POpaque
v))
        # punsafeCoerce (plam' $ \(x :: Term s POpaque) -> f # plam' (\(v :: Term s POpaque) -> punsafeCoerce x # x # v))

{- | As 'pfixHoisted', but not hoisted. This is more efficient in terms of
execution units, but takes up more script space.

@since 1.12.0
-}
pfix ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  (Term s (a :--> b) -> Term s (a :--> b)) ->
  Term s (a :--> b)
pfix :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix Term s (a :--> b) -> Term s (a :--> b)
f =
  (Term s (Any @(S -> Type) :--> (a :--> b)) -> Term s (a :--> b))
-> Term s ((Any @(S -> Type) :--> (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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (a :--> b)) -> Term s (c :--> (a :--> b))
plam (\Term s (Any @(S -> Type) :--> (a :--> b))
r -> Term s (Any @(S -> Type) :--> (a :--> b))
-> Term s ((Any @(S -> Type) :--> (a :--> b)) :--> (a :--> b))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (Any @(S -> Type) :--> (a :--> b))
r Term s ((Any @(S -> Type) :--> (a :--> b)) :--> (a :--> b))
-> Term s (Any @(S -> Type) :--> (a :--> b)) -> Term s (a :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (Any @(S -> Type) :--> (a :--> b))
r)
    # plam (\r -> f (punsafeCoerce r # r))

{- | As 'pfix', but we perform some additional inlining into the function
argument. This allows for even more speed, but at the cost of larger scripts.

@since 1.12.0
-}
pfixInline ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  (Term s (a :--> b) -> Term s (a :--> b)) ->
  Term s (a :--> b)
pfixInline :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfixInline Term s (a :--> b) -> Term s (a :--> b)
f =
  (Term s (Any @(S -> Type) :--> (a :--> b)) -> Term s (a :--> b))
-> Term s ((Any @(S -> Type) :--> (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)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s (a :--> b)) -> Term s (c :--> (a :--> b))
plam (\Term s (Any @(S -> Type) :--> (a :--> b))
r -> Term s (a :--> b) -> Term s (a :--> b)
f (Term s (Any @(S -> Type) :--> (a :--> b))
-> Term s ((Any @(S -> Type) :--> (a :--> b)) :--> (a :--> b))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (Any @(S -> Type) :--> (a :--> b))
r Term s ((Any @(S -> Type) :--> (a :--> b)) :--> (a :--> b))
-> Term s (Any @(S -> Type) :--> (a :--> b)) -> Term s (a :--> b)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (Any @(S -> Type) :--> (a :--> b))
r))
    # plam (\r -> f (punsafeCoerce r # r))