{-
BuiltinPair and BuiltinList should go into their own module !!
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Plutarch.Builtin.Data (
  PData (PData),
  PAsData (PAsData),
  pchooseData,
  pasConstr,
  pasMap,
  plistData,
  pasList,
  pasInt,
  pasByteStr,
  pserialiseData,
  pconstrBuiltin,
  PBuiltinPair (PBuiltinPair),
  pfstBuiltin,
  psndBuiltin,
  ppairDataBuiltin,
  PBuiltinList (PCons, PNil),
  pheadBuiltin,
  ptailBuiltin,
  pchooseListBuiltin,
  pnullBuiltin,
  pconsBuiltin,
) where

import Data.Kind (Type)

import Plutarch.Builtin.Bool (PBool)
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Integer (PInteger)

import Plutarch.Internal.Term (S, Term, pforce, phoistAcyclic, punsafeBuiltin, (:-->))
import PlutusCore qualified as PLC

newtype PData (s :: S) = PData (Term s PData)
newtype PAsData (a :: S -> Type) (s :: S) = PAsData (Term s a)

pchooseData :: Term s (PData :--> a :--> a :--> a :--> a :--> a :--> a)
pchooseData :: forall (s :: S) (a :: PType).
Term s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
pchooseData = ClosedTerm
  (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
 -> Term
      s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> ClosedTerm
     (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDelayed
     (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term
   s
   (PDelayed
      (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
 -> Term
      s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s
     (PDelayed
        (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term
     s
     (PDelayed
        (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ChooseData

pasConstr :: Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr :: forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr = DefaultFun
-> Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnConstrData

pasMap :: Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap :: forall (s :: S).
Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
pasMap = DefaultFun
-> Term s (PData :--> PBuiltinList (PBuiltinPair PData PData))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnMapData

plistData :: Term s (PBuiltinList PData :--> PData)
plistData :: forall (s :: S). Term s (PBuiltinList PData :--> PData)
plistData = DefaultFun -> Term s (PBuiltinList PData :--> PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ListData

pasList :: Term s (PData :--> PBuiltinList PData)
pasList :: forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList = DefaultFun -> Term s (PData :--> PBuiltinList PData)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnListData

pasInt :: Term s (PData :--> PInteger)
pasInt :: forall (s :: S). Term s (PData :--> PInteger)
pasInt = DefaultFun -> Term s (PData :--> PInteger)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnIData

pasByteStr :: Term s (PData :--> PByteString)
pasByteStr :: forall (s :: S). Term s (PData :--> PByteString)
pasByteStr = DefaultFun -> Term s (PData :--> PByteString)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.UnBData

-- | Serialise any builtin data to its cbor represented by a builtin bytestring
pserialiseData :: Term s (PData :--> PByteString)
pserialiseData :: forall (s :: S). Term s (PData :--> PByteString)
pserialiseData = DefaultFun -> Term s (PData :--> PByteString)
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.SerialiseData

pconstrBuiltin :: Term s (PInteger :--> PBuiltinList PData :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData)))
pconstrBuiltin :: forall (s :: S).
Term
  s
  (PInteger
   :--> (PBuiltinList PData
         :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
pconstrBuiltin = DefaultFun
-> Term
     s
     (PInteger
      :--> (PBuiltinList PData
            :--> PAsData (PBuiltinPair PInteger (PBuiltinList PData))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ConstrData

--------------------------------------------------------------------------------

newtype PBuiltinPair (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PBuiltinPair (Term s (PBuiltinPair a b))

pfstBuiltin :: Term s (PBuiltinPair a b :--> a)
pfstBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin = ClosedTerm (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b :--> a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinPair a b :--> a)
 -> Term s (PBuiltinPair a b :--> a))
-> ClosedTerm (PBuiltinPair a b :--> a)
-> Term s (PBuiltinPair a b :--> a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinPair a b :--> a))
-> Term s (PBuiltinPair a b :--> a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinPair a b :--> a))
 -> Term s (PBuiltinPair a b :--> a))
-> (DefaultFun -> Term s (PDelayed (PBuiltinPair a b :--> a)))
-> DefaultFun
-> Term s (PBuiltinPair a b :--> a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
-> Term s (PDelayed (PBuiltinPair a b :--> a))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
 -> Term s (PDelayed (PBuiltinPair a b :--> a)))
-> (DefaultFun
    -> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a))))
-> DefaultFun
-> Term s (PDelayed (PBuiltinPair a b :--> a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun
-> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> a)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin (DefaultFun -> Term s (PBuiltinPair a b :--> a))
-> DefaultFun -> Term s (PBuiltinPair a b :--> a)
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.FstPair

psndBuiltin :: Term s (PBuiltinPair a b :--> b)
psndBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin = ClosedTerm (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b :--> b)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinPair a b :--> b)
 -> Term s (PBuiltinPair a b :--> b))
-> ClosedTerm (PBuiltinPair a b :--> b)
-> Term s (PBuiltinPair a b :--> b)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinPair a b :--> b))
-> Term s (PBuiltinPair a b :--> b)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinPair a b :--> b))
 -> Term s (PBuiltinPair a b :--> b))
-> (DefaultFun -> Term s (PDelayed (PBuiltinPair a b :--> b)))
-> DefaultFun
-> Term s (PBuiltinPair a b :--> b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
-> Term s (PDelayed (PBuiltinPair a b :--> b))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
 -> Term s (PDelayed (PBuiltinPair a b :--> b)))
-> (DefaultFun
    -> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b))))
-> DefaultFun
-> Term s (PDelayed (PBuiltinPair a b :--> b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun
-> Term s (PDelayed (PDelayed (PBuiltinPair a b :--> b)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin (DefaultFun -> Term s (PBuiltinPair a b :--> b))
-> DefaultFun -> Term s (PBuiltinPair a b :--> b)
forall a b. (a -> b) -> a -> b
$ DefaultFun
PLC.SndPair

{- | Construct a builtin pair of 'PData' elements.

Uses 'PAsData' to preserve more information about the underlying 'PData'.
-}
ppairDataBuiltin :: Term s (PAsData a :--> PAsData b :--> PBuiltinPair (PAsData a) (PAsData b))
ppairDataBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin = DefaultFun
-> Term
     s
     (PAsData a
      :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkPairData

--------------------------------------------------------------------------------

-- | Plutus 'BuiltinList'
data PBuiltinList (a :: S -> Type) (s :: S)
  = PCons (Term s a) (Term s (PBuiltinList a))
  | PNil

pheadBuiltin :: Term s (PBuiltinList a :--> a)
pheadBuiltin :: forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> a)
pheadBuiltin = ClosedTerm (PBuiltinList a :--> a)
-> Term s (PBuiltinList a :--> a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> a)
 -> Term s (PBuiltinList a :--> a))
-> ClosedTerm (PBuiltinList a :--> a)
-> Term s (PBuiltinList a :--> a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> a))
-> Term s (PBuiltinList a :--> a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> a))
 -> Term s (PBuiltinList a :--> a))
-> Term s (PDelayed (PBuiltinList a :--> a))
-> Term s (PBuiltinList a :--> a)
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Term s (PDelayed (PBuiltinList a :--> a))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.HeadList

ptailBuiltin :: Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin :: forall (s :: S) (a :: PType).
Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin = ClosedTerm (PBuiltinList a :--> PBuiltinList a)
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> PBuiltinList a)
 -> Term s (PBuiltinList a :--> PBuiltinList a))
-> ClosedTerm (PBuiltinList a :--> PBuiltinList a)
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
 -> Term s (PBuiltinList a :--> PBuiltinList a))
-> Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term s (PDelayed (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.TailList

pchooseListBuiltin :: Term s (PBuiltinList a :--> b :--> b :--> b)
pchooseListBuiltin :: forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin = ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
 -> Term s (PBuiltinList a :--> (b :--> (b :--> b))))
-> ClosedTerm (PBuiltinList a :--> (b :--> (b :--> b)))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
 -> Term s (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall a b. (a -> b) -> a -> b
$ Term
  s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term
   s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
 -> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term
     s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
-> Term s (PDelayed (PBuiltinList a :--> (b :--> (b :--> b))))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term
     s (PDelayed (PDelayed (PBuiltinList a :--> (b :--> (b :--> b)))))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ChooseList

pnullBuiltin :: Term s (PBuiltinList a :--> PBool)
pnullBuiltin :: forall (s :: S) (a :: PType). Term s (PBuiltinList a :--> PBool)
pnullBuiltin = ClosedTerm (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a :--> PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PBuiltinList a :--> PBool)
 -> Term s (PBuiltinList a :--> PBool))
-> ClosedTerm (PBuiltinList a :--> PBool)
-> Term s (PBuiltinList a :--> PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a :--> PBool)
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (PBuiltinList a :--> PBool))
 -> Term s (PBuiltinList a :--> PBool))
-> Term s (PDelayed (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a :--> PBool)
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Term s (PDelayed (PBuiltinList a :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.NullList

pconsBuiltin :: Term s (a :--> PBuiltinList a :--> PBuiltinList a)
pconsBuiltin :: forall (s :: S) (a :: PType).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin = ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> ClosedTerm (a :--> (PBuiltinList a :--> PBuiltinList a))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (s :: S) (a :: PType). Term s (PDelayed a) -> Term s a
pforce (Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall a b. (a -> b) -> a -> b
$ DefaultFun
-> Term s (PDelayed (a :--> (PBuiltinList a :--> PBuiltinList a)))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkCons