{-
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,
  pheadTailBuiltin,
  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.PLam (plam)
import Plutarch.Internal.Term (
  RawTerm (RCase),
  S,
  Term (Term),
  TermResult (TermResult),
  asRawTerm,
  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 :: S -> Type).
Term s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
pchooseData = (forall (s' :: S).
 Term
   s' (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> Term
     s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a))))))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term
    s' (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
 -> Term
      s (PData :--> (a :--> (a :--> (a :--> (a :--> (a :--> a)))))))
-> (forall (s' :: S).
    Term
      s' (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ConstrData

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

{- | A builtin Plutus pair.

@since 1.12.0
-}
data PBuiltinPair (a :: S -> Type) (b :: S -> Type) (s :: S)
  = PBuiltinPair (Term s a) (Term s b)

{-# DEPRECATED pfstBuiltin "Use pmatch instead" #-}
pfstBuiltin :: Term s (PBuiltinPair a b :--> a)
pfstBuiltin :: forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin = (forall (s' :: S). Term s' (PBuiltinPair a b :--> a))
-> Term s (PBuiltinPair a b :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBuiltinPair a b :--> a))
 -> Term s (PBuiltinPair a b :--> a))
-> (forall (s' :: S). Term s' (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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

{-# DEPRECATED psndBuiltin "Use pmatch instead" #-}
psndBuiltin :: Term s (PBuiltinPair a b :--> b)
psndBuiltin :: forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinPair a b :--> b)
psndBuiltin = (forall (s' :: S). Term s' (PBuiltinPair a b :--> b))
-> Term s (PBuiltinPair a b :--> b)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBuiltinPair a b :--> b))
 -> Term s (PBuiltinPair a b :--> b))
-> (forall (s' :: S). Term s' (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type) (b :: S -> Type).
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 :: S -> Type). 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 :: S -> Type). Term s (PBuiltinList a :--> a)
pheadBuiltin = (forall (s' :: S). Term s' (PBuiltinList a :--> a))
-> Term s (PBuiltinList a :--> a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBuiltinList a :--> a))
 -> Term s (PBuiltinList a :--> a))
-> (forall (s' :: S). Term s' (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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.HeadList

ptailBuiltin :: Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin :: forall (s :: S) (a :: S -> Type).
Term s (PBuiltinList a :--> PBuiltinList a)
ptailBuiltin = (forall (s' :: S). Term s' (PBuiltinList a :--> PBuiltinList a))
-> Term s (PBuiltinList a :--> PBuiltinList a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBuiltinList a :--> PBuiltinList a))
 -> Term s (PBuiltinList a :--> PBuiltinList a))
-> (forall (s' :: S). Term s' (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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.TailList

{- | Use this in preference to 'pheadBuiltin' and 'ptailBuiltin' on the same
'PBuiltinList', as this will be faster. This is also faster than a 'pmatch',
as the 'PNil' case is omitted.

@since 1.13.0
-}
pheadTailBuiltin ::
  forall (a :: S -> Type) (b :: S -> Type) (s :: S).
  Term s (PBuiltinList a) ->
  (Term s a -> Term s (PBuiltinList a) -> Term s b) ->
  Term s b
pheadTailBuiltin :: forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s (PBuiltinList a)
-> (Term s a -> Term s (PBuiltinList a) -> Term s b) -> Term s b
pheadTailBuiltin Term s (PBuiltinList a)
ell Term s a -> Term s (PBuiltinList a) -> Term s b
handler = (Word64 -> TermMonad TermResult) -> Term s b
forall (s :: S) (a :: S -> Type).
(Word64 -> TermMonad TermResult) -> Term s a
Term ((Word64 -> TermMonad TermResult) -> Term s b)
-> (Word64 -> TermMonad TermResult) -> Term s b
forall a b. (a -> b) -> a -> b
$ \Word64
level -> do
  TermResult RawTerm
matchRaw [HoistedTerm]
matchDeps <- Term s (a :--> (PBuiltinList a :--> b))
-> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm ((Term s a -> Term s (PBuiltinList a) -> Term s b)
-> Term s (a :--> (PBuiltinList 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 (PBuiltinList a) -> Term s b)
-> Term s (c :--> (PBuiltinList a :--> b))
plam Term s a -> Term s (PBuiltinList a) -> Term s b
handler) Word64
level
  TermResult RawTerm
rawT [HoistedTerm]
depsT <- Term s (PBuiltinList a) -> Word64 -> TermMonad TermResult
forall (s :: S) (a :: S -> Type).
Term s a -> Word64 -> TermMonad TermResult
asRawTerm Term s (PBuiltinList a)
ell Word64
level
  let allDeps :: [HoistedTerm]
allDeps = [HoistedTerm]
matchDeps [HoistedTerm] -> [HoistedTerm] -> [HoistedTerm]
forall a. Semigroup a => a -> a -> a
<> [HoistedTerm]
depsT
  TermResult -> TermMonad TermResult
forall a. a -> TermMonad a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TermResult -> TermMonad TermResult)
-> ([HoistedTerm] -> TermResult)
-> [HoistedTerm]
-> TermMonad TermResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawTerm -> [HoistedTerm] -> TermResult
TermResult (RawTerm -> [RawTerm] -> RawTerm
RCase RawTerm
rawT [Item [RawTerm]
RawTerm
matchRaw]) ([HoistedTerm] -> TermMonad TermResult)
-> [HoistedTerm] -> TermMonad TermResult
forall a b. (a -> b) -> a -> b
$ [HoistedTerm]
allDeps

pchooseListBuiltin :: Term s (PBuiltinList a :--> b :--> b :--> b)
pchooseListBuiltin :: forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (PBuiltinList a :--> (b :--> (b :--> b)))
pchooseListBuiltin = (forall (s' :: S).
 Term s' (PBuiltinList a :--> (b :--> (b :--> b))))
-> Term s (PBuiltinList a :--> (b :--> (b :--> b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term s' (PBuiltinList a :--> (b :--> (b :--> b))))
 -> Term s (PBuiltinList a :--> (b :--> (b :--> b))))
-> (forall (s' :: S).
    Term s' (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 :: S -> Type). 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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.ChooseList

pnullBuiltin :: Term s (PBuiltinList a :--> PBool)
pnullBuiltin :: forall (s :: S) (a :: S -> Type).
Term s (PBuiltinList a :--> PBool)
pnullBuiltin = (forall (s' :: S). Term s' (PBuiltinList a :--> PBool))
-> Term s (PBuiltinList a :--> PBool)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S). Term s' (PBuiltinList a :--> PBool))
 -> Term s (PBuiltinList a :--> PBool))
-> (forall (s' :: S). Term s' (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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.NullList

pconsBuiltin :: Term s (a :--> PBuiltinList a :--> PBuiltinList a)
pconsBuiltin :: forall (s :: S) (a :: S -> Type).
Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
pconsBuiltin = (forall (s' :: S).
 Term s' (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> Term s (a :--> (PBuiltinList a :--> PBuiltinList a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
(forall (s' :: S). Term s' a) -> Term s a
phoistAcyclic ((forall (s' :: S).
  Term s' (a :--> (PBuiltinList a :--> PBuiltinList a)))
 -> Term s (a :--> (PBuiltinList a :--> PBuiltinList a)))
-> (forall (s' :: S).
    Term s' (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 :: S -> Type). 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 :: S -> Type). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.MkCons