{-# 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.PlutusType (
  PContravariant',
  PCovariant',
  PInner,
  PVariant',
  PlutusType,
  pcon',
  pmatch',
 )
import Plutarch.Internal.Term (
  ClosedTerm,
  Config,
  Term,
  compile,
  phoistAcyclic,
  plam',
  punsafeCoerce,
  (#),
  (:-->),
 )
import Plutarch.Script (Script (Script))
import PlutusCore.Pretty (prettyPlcReadable)

-- | Prettyprint a compiled Script via the PLC pretty printer
printScript :: Script -> String
printScript :: Script -> String
printScript = Doc (Any @Type) -> String
forall a. Show a => a -> String
show (Doc (Any @Type) -> String)
-> (Script -> Doc (Any @Type)) -> Script -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program DeBruijn DefaultUni DefaultFun () -> Doc (Any @Type)
forall a ann. PrettyPlc a => a -> Doc ann
prettyPlcReadable (Program DeBruijn DefaultUni DefaultFun () -> Doc (Any @Type))
-> (Script -> Program DeBruijn DefaultUni DefaultFun ())
-> Script
-> Doc (Any @Type)
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 (Script -> String) -> Script -> String
forall a b. (a -> b) -> a -> b
$ (Text -> Script)
-> (Script -> Script) -> Either Text Script -> Script
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Script
forall a. HasCallStack => String -> a
error (String -> Script) -> (Text -> String) -> Text -> Script
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack) Script -> Script
forall a. a -> a
id (Either Text Script -> Script) -> Either Text Script -> Script
forall a b. (a -> b) -> a -> b
$ Config -> ClosedTerm a -> Either Text Script
forall (a :: PType). Config -> ClosedTerm a -> Either Text Script
compile Config
config Term s a
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 = Term s a -> Term s (PInner a)
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 (PInner POpaque)
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 (Term s POpaque -> POpaque s
forall (s :: S). Term s POpaque -> POpaque s
POpaque Term s (PInner POpaque)
Term s 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 = Term s a -> Term s 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 = 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 (s :: S) (a :: PType) (b :: PType). 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 (s :: S) (a :: PType) (b :: PType). 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))