{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Internal.Other (
  printTerm,
  printScript,
  pto,
  pfix,
  POpaque (..),
  popaque,
) where

import Data.Text qualified as T
import GHC.Stack (HasCallStack)
import Plutarch.Internal (ClosedTerm, Config, Term, compile, phoistAcyclic, plam', punsafeCoerce, (#), (:-->))
import Plutarch.Internal.PlutusType (
  PContravariant',
  PCovariant',
  PInner,
  PVariant',
  PlutusType,
  pcon',
  pmatch',
 )
import Plutarch.Script (Script (Script))
import PlutusCore.Pretty (prettyPlcReadableDebug)

-- | Prettyprint a compiled Script via the PLC pretty printer
printScript :: Script -> String
printScript :: Script -> String
printScript = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcReadableDebug forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Script Program DeBruijn DefaultUni DefaultFun ()
s) -> Program DeBruijn DefaultUni DefaultFun ()
s)

{- | Prettyprint a Term via the PLC pretty printer

  TODO: Heavily improve. It's unreadable right now.

  We could convert the de Bruijn indices into names with:

  > show . prettyPlcReadableDef . (\(Right p) -> p) . Scripts.mkTermToEvaluate . compile $ term
-}
printTerm :: HasCallStack => Config -> ClosedTerm a -> String
printTerm :: forall (a :: PType).
HasCallStack =>
Config -> ClosedTerm a -> String
printTerm Config
config ClosedTerm a
term = Script -> String
printScript forall a b. (a -> b) -> a -> b
$ forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. HasCallStack => String -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall (a :: PType). Config -> ClosedTerm a -> Either Text Script
compile Config
config ClosedTerm a
term

{- |
  Safely coerce from a Term to it's 'PInner' representation.
-}
pto :: Term s a -> Term s (PInner a)
pto :: forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

-- | An Arbitrary Term with an unknown type
newtype POpaque s = POpaque (Term s POpaque)

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

-- | Erase the type of a Term
popaque :: Term s a -> Term s POpaque
popaque :: forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque = forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce

{- |
  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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce forall a b. (a -> b) -> a -> b
$
    forall (s :: S) (a :: PType) (b :: PType).
(Term s a -> Term s b) -> Term s (a :--> b)
plam' forall a b. (a -> b) -> a -> b
$ \Term s ((POpaque :--> Any @PType) :--> Any @PType)
f ->
      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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# 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) -> forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s POpaque
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s POpaque
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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))