module Plutarch.Internal.Fix (pfix) where

import Plutarch.Builtin.Opaque
import Plutarch.Internal.Term

{- |
  Fixpoint recursion. Used to encode recursive functions.

  Example:

  > 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 = pfix #$ plam iterateN'
  >

  Further examples can be found in examples/Recursion.hs
-}
pfix :: Term s (((a :--> b) :--> a :--> b) :--> a :--> b)
pfix :: forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix = ClosedTerm (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
-> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
 -> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> ClosedTerm (((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 @PType) :--> Any @PType) :--> Any @PType)
-> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term
   s (((POpaque :--> Any @PType) :--> Any @PType) :--> Any @PType)
 -> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b)))
-> Term
     s (((POpaque :--> Any @PType) :--> Any @PType) :--> Any @PType)
-> Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
forall a b. (a -> b) -> a -> b
$
    (Term s ((POpaque :--> Any @PType) :--> Any @PType)
 -> Term s (Any @PType))
-> Term
     s (((POpaque :--> Any @PType) :--> Any @PType) :--> Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' ((Term s ((POpaque :--> Any @PType) :--> Any @PType)
  -> Term s (Any @PType))
 -> Term
      s (((POpaque :--> Any @PType) :--> Any @PType) :--> Any @PType))
-> (Term s ((POpaque :--> Any @PType) :--> Any @PType)
    -> Term s (Any @PType))
-> Term
     s (((POpaque :--> Any @PType) :--> Any @PType) :--> Any @PType)
forall a b. (a -> b) -> a -> b
$ \Term s ((POpaque :--> Any @PType) :--> Any @PType)
f ->
      (Term s POpaque -> Term s (Any @PType))
-> Term s (POpaque :--> Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' (\(Term s POpaque
x :: Term s POpaque) -> Term s ((POpaque :--> Any @PType) :--> Any @PType)
f Term s ((POpaque :--> Any @PType) :--> Any @PType)
-> Term s (POpaque :--> Any @PType) -> Term s (Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s POpaque -> Term s (Any @PType))
-> Term s (POpaque :--> Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
(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 @PType))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s POpaque
x Term s (POpaque :--> (POpaque :--> Any @PType))
-> Term s POpaque -> Term s (POpaque :--> Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s POpaque
x Term s (POpaque :--> Any @PType)
-> Term s POpaque -> Term s (Any @PType)
forall (s :: S) (a :: PType) (b :: PType).
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))