-- | Scott-encoded lists and ListLike typeclass
module Plutarch.List (
  PList (PSCons, PSNil),
  ptryUncons,
  puncons,
  pzip,
  pfind,
  preverse,
  pcheckSorted,
  pelem,
  (#!!),
  pelemAt,
  pelemAt',
  plistEquals,
) where

import Data.Kind (Type)
import GHC.Generics (Generic)
import Plutarch.Builtin.Bool (PBool (PFalse, PTrue), pif, ptrue, (#&&))
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.Lift (pconstant)
import Plutarch.Internal.ListLike (
  PElemConstraint,
  PIsListLike,
  PListLike,
  pcons,
  pelimList,
  pfoldl,
  phead,
  pnil,
  precList,
  ptail,
  pzipWith',
 )
import Plutarch.Internal.Ord (POrd ((#<), (#<=)))
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (
  DerivePlutusType (DPTStrat),
  PlutusType,
  pcon,
  pmatch,
 )
import Plutarch.Internal.ScottEncoding (
  PlutusTypeScott,
 )
import Plutarch.Internal.Show (PShow (pshow'), pshowList)
import Plutarch.Internal.Term (
  S,
  Term,
  perror,
  phoistAcyclic,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.Trace (ptraceInfo)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Pair (PPair (PPair))

data PList (a :: S -> Type) (s :: S)
  = PSCons (Term s a) (Term s (PList a))
  | PSNil
  deriving stock ((forall x. PList a s -> Rep (PList a s) x)
-> (forall x. Rep (PList a s) x -> PList a s)
-> Generic (PList a s)
forall x. Rep (PList a s) x -> PList a s
forall x. PList a s -> Rep (PList a s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
$cfrom :: forall (a :: S -> Type) (s :: S) x. PList a s -> Rep (PList a s) x
from :: forall x. PList a s -> Rep (PList a s) x
$cto :: forall (a :: S -> Type) (s :: S) x. Rep (PList a s) x -> PList a s
to :: forall x. Rep (PList a s) x -> PList a s
Generic)
  deriving anyclass ((forall (s :: S). PList a s -> Term s (PInner (PList a)))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b)
-> PlutusType (PList a)
forall (s :: S). PList a s -> Term s (PInner (PList a))
forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
forall (a :: S -> Type).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: S -> Type).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
$cpcon' :: forall (a :: S -> Type) (s :: S).
PList a s -> Term s (PInner (PList a))
pcon' :: forall (s :: S). PList a s -> Term s (PInner (PList a))
$cpmatch' :: forall (a :: S -> Type) (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: S -> Type).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
PlutusType)

instance DerivePlutusType (PList a) where
  type DPTStrat _ = PlutusTypeScott

instance PShow a => PShow (PList a) where
  pshow' :: forall (s :: S). Bool -> Term s (PList a) -> Term s PString
pshow' Bool
_ Term s (PList a)
x = forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList @PList @a Term s (PList a :--> PString) -> Term s (PList a) -> Term s PString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
x

instance PEq a => PEq (PList a) where
  #== :: forall (s :: S).
Term s (PList a) -> Term s (PList a) -> Term s PBool
(#==) Term s (PList a)
xs Term s (PList a)
ys = Term s (PList a :--> (PList a :--> PBool))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals Term s (PList a :--> (PList a :--> PBool))
-> Term s (PList a) -> Term s (PList a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs Term s (PList a :--> PBool) -> Term s (PList a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
ys

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

instance PListLike PList where
  type PElemConstraint PList _ = ()
  pelimList :: forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint PList a =>
(Term s a -> Term s (PList a) -> Term s r)
-> Term s r -> Term s (PList a) -> Term s r
pelimList Term s a -> Term s (PList a) -> Term s r
match_cons Term s r
match_nil Term s (PList a)
ls = Term s (PList a) -> (PList a s -> Term s r) -> Term s r
forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PList a)
ls ((PList a s -> Term s r) -> Term s r)
-> (PList a s -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \case
    PSCons Term s a
x Term s (PList a)
xs -> Term s a -> Term s (PList a) -> Term s r
match_cons Term s a
x Term s (PList a)
xs
    PList a s
PSNil -> Term s r
match_nil
  pcons :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (a :--> (PList a :--> PList a))
pcons = ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (PList a :--> PList a))
 -> Term s (a :--> (PList a :--> PList a)))
-> ClosedTerm (a :--> (PList a :--> PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
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 (PList a) -> Term s (PList a))
-> Term s (c :--> (PList a :--> PList a))
plam ((Term s a -> Term s (PList a) -> Term s (PList a))
 -> Term s (a :--> (PList a :--> PList a)))
-> (Term s a -> Term s (PList a) -> Term s (PList a))
-> Term s (a :--> (PList a :--> PList a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s (PList a)
xs -> PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s (PList a) -> PList a s
forall (a :: S -> Type) (s :: S).
Term s a -> Term s (PList a) -> PList a s
PSCons Term s a
x Term s (PList a)
xs)
  pnil :: forall (a :: S -> Type) (s :: S).
PElemConstraint PList a =>
Term s (PList a)
pnil = PList a s -> Term s (PList a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PList a s
forall (a :: S -> Type) (s :: S). PList a s
PSNil

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

-- | Extract head and tail of the list, throws error if list is empty.
ptryUncons ::
  PIsListLike list a =>
  Term s (list a :--> PPair a (list a))
ptryUncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PPair a (list a))
ptryUncons =
  ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PPair a (list a))
 -> Term s (list a :--> PPair a (list a)))
-> ClosedTerm (list a :--> PPair a (list a))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
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 (PPair a (list a)))
-> Term s (c :--> PPair a (list a))
plam ((Term s (list a) -> Term s (PPair a (list a)))
 -> Term s (list a :--> PPair a (list a)))
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a :--> PPair a (list a))
forall a b. (a -> b) -> a -> b
$
      (Term s a -> Term s (list a) -> Term s (PPair a (list a)))
-> Term s (PPair a (list a))
-> Term s (list a)
-> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
x -> PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) Term s (PPair a (list a))
forall (s :: S) (a :: S -> Type). Term s a
perror

-- | Extract head and tail of the list, if list is not empty.
puncons ::
  PIsListLike list a =>
  Term s (list a :--> PMaybe (PPair a (list a)))
puncons :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons =
  ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> PMaybe (PPair a (list a)))
 -> Term s (list a :--> PMaybe (PPair a (list a))))
-> ClosedTerm (list a :--> PMaybe (PPair a (list a)))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
    (Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
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 (PMaybe (PPair a (list a))))
-> Term s (c :--> PMaybe (PPair a (list a)))
plam ((Term s (list a) -> Term s (PMaybe (PPair a (list a))))
 -> Term s (list a :--> PMaybe (PPair a (list a))))
-> (Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (list a :--> PMaybe (PPair a (list a)))
forall a b. (a -> b) -> a -> b
$
      (Term s a -> Term s (list a) -> Term s (PMaybe (PPair a (list a))))
-> Term s (PMaybe (PPair a (list a)))
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
x -> PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a))))
-> (Term s (list a) -> PMaybe (PPair a (list a)) s)
-> Term s (list a)
-> Term s (PMaybe (PPair a (list a)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust (Term s (PPair a (list a)) -> PMaybe (PPair a (list a)) s)
-> (Term s (list a) -> Term s (PPair a (list a)))
-> Term s (list a)
-> PMaybe (PPair a (list a)) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PPair a (list a) s -> Term s (PPair a (list a))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair a (list a) s -> Term s (PPair a (list a)))
-> (Term s (list a) -> PPair a (list a) s)
-> Term s (list a)
-> Term s (PPair a (list a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s a -> Term s (list a) -> PPair a (list a) s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) (PMaybe (PPair a (list a)) s -> Term s (PMaybe (PPair a (list a)))
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe (PPair a (list a)) s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)

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

{- | / O(min(n, m)) /. Zip two lists together, creating pairs of the elements.

If the lists are of differing lengths, cut to the shortest.
-}
pzip ::
  ( PListLike list
  , PElemConstraint list a
  , PElemConstraint list b
  , PElemConstraint list (PPair a b)
  ) =>
  Term s (list a :--> list b :--> list (PPair a b))
pzip :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list (PPair a b)) =>
Term s (list a :--> (list b :--> list (PPair a b)))
pzip = ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list b :--> list (PPair a b)))
 -> Term s (list a :--> (list b :--> list (PPair a b))))
-> ClosedTerm (list a :--> (list b :--> list (PPair a b)))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (c :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list c) =>
(Term s a -> Term s b -> Term s c)
-> Term s (list a :--> (list b :--> list c))
pzipWith' ((Term s a -> Term s b -> Term s (PPair a b))
 -> Term s (list a :--> (list b :--> list (PPair a b))))
-> (Term s a -> Term s b -> Term s (PPair a b))
-> Term s (list a :--> (list b :--> list (PPair a b)))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> PPair a b s -> Term s (PPair a b)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (Term s a -> Term s b -> PPair a b s
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x Term s b
y)

-- | / O(n) /. like haskell level `find` but on plutarch level
pfind :: PIsListLike l a => Term s ((a :--> PBool) :--> l a :--> PMaybe a)
pfind :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind = ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
 -> Term s ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> ClosedTerm ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall a b. (a -> b) -> a -> b
$
  Term
  s
  ((((a :--> PBool) :--> (l a :--> PMaybe a))
    :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
   :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  ((((a :--> PBool) :--> (l a :--> PMaybe a))
    :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
   :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
-> Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
 -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
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 (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term s (c :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
plam ((Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
  -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
 -> Term
      s
      (((a :--> PBool) :--> (l a :--> PMaybe a))
       :--> ((a :--> PBool) :--> (l a :--> PMaybe a))))
-> (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
    -> Term s (a :--> PBool) -> Term s (l a) -> Term s (PMaybe a))
-> Term
     s
     (((a :--> PBool) :--> (l a :--> PMaybe a))
      :--> ((a :--> PBool) :--> (l a :--> PMaybe a)))
forall a b. (a -> b) -> a -> b
$ \Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s (a :--> PBool)
f Term s (l a)
xs ->
    (Term s a -> Term s (l a) -> Term s (PMaybe a))
-> Term s (PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
      ( \Term s a
y Term s (l a)
ys ->
          Term s PBool
-> Term s (PMaybe a) -> Term s (PMaybe a) -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s (a :--> PBool)
f Term s (a :--> PBool) -> Term s a -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
            (PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon (PMaybe a s -> Term s (PMaybe a))
-> PMaybe a s -> Term s (PMaybe a)
forall a b. (a -> b) -> a -> b
$ Term s a -> PMaybe a s
forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust Term s a
y)
            (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
-> Term s (a :--> PBool) -> Term s (l a :--> PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> PBool)
f Term s (l a :--> PMaybe a) -> Term s (l a) -> Term s (PMaybe a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
ys)
      )
      (PMaybe a s -> Term s (PMaybe a)
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PMaybe a s
forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
      Term s (l a)
xs

{- | / O(n) /. Reverse a list-like structure.

@since WIP
-}
preverse ::
  forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  PIsListLike l a =>
  Term s (l a :--> l a)
preverse :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a :--> l a)
preverse = ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (l a :--> l a) -> Term s (l a :--> l a))
-> ClosedTerm (l a :--> l a) -> Term s (l a :--> l a)
forall a b. (a -> b) -> a -> b
$ Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (b :: S -> Type).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl Term s ((l a :--> (a :--> l a)) :--> (l a :--> (l a :--> l a)))
-> Term s (l a :--> (a :--> l a))
-> Term s (l a :--> (l a :--> l a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (l a) -> Term s a -> Term s (l a))
-> Term s (l a :--> (a :--> l a))
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 a -> Term s (l a))
-> Term s (c :--> (a :--> l a))
plam (\Term s (l a)
xs Term s a
x -> Term s (a :--> (l a :--> l a))
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (a :--> (l a :--> l a))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term s (a :--> (l a :--> l a)) -> Term s a -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs) Term s (l a :--> (l a :--> l a))
-> Term s (l a) -> Term s (l a :--> l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

{- | / O(n) /. Checks if a list-list structure is sorted.

@since WIP
-}
pcheckSorted ::
  forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PIsListLike l a, POrd a) =>
  Term s (l a :--> PBool)
pcheckSorted :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike l a, POrd a) =>
Term s (l a :--> PBool)
pcheckSorted =
  Term
  s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s (((l a :--> PBool) :--> (l a :--> PBool)) :--> (l a :--> PBool))
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
-> Term s (l a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
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 (l a) -> Term s PBool)
-> Term s (c :--> (l a :--> PBool))
plam ((Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
 -> Term s ((l a :--> PBool) :--> (l a :--> PBool)))
-> (Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool)
-> Term s ((l a :--> PBool) :--> (l a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s (l a :--> PBool)
self Term s (l a)
xs ->
    (Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
      ( \Term s a
x1 Term s (l a)
xs ->
          (Term s a -> Term s (l a) -> Term s PBool)
-> Term s PBool -> Term s (l a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint l a =>
(Term s a -> Term s (l a) -> Term s r)
-> Term s r -> Term s (l a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
            (\Term s a
x2 Term s (l a)
_ -> Term s a
x1 Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
x2 Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& (Term s (l a :--> PBool)
self Term s (l a :--> PBool) -> Term s (l a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs))
            Term s PBool
forall (s :: S). Term s PBool
ptrue
            Term s (l a)
xs
      )
      Term s PBool
forall (s :: S). Term s PBool
ptrue
      Term s (l a)
xs

-- | / O(n) /. Check if element is in the list
pelem :: (PIsListLike list a, PEq a) => Term s (a :--> list a :--> PBool)
pelem :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (a :--> (list a :--> PBool))
pelem =
  ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (a :--> (list a :--> PBool))
 -> Term s (a :--> (list a :--> PBool)))
-> ClosedTerm (a :--> (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
    (Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
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 (list a :--> PBool))
-> Term s (c :--> (list a :--> PBool))
plam ((Term s a -> Term s (list a :--> PBool))
 -> Term s (a :--> (list a :--> PBool)))
-> (Term s a -> Term s (list a :--> PBool))
-> Term s (a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s a
needle ->
      (Term s (list a :--> PBool)
 -> Term s a -> Term s (list a) -> Term s PBool)
-> (Term s (list a :--> PBool) -> Term s PBool)
-> Term s (list a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
        (\Term s (list a :--> PBool)
self Term s a
x Term s (list a)
xs -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
needle) (PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PTrue) (Term s (list a :--> PBool)
self Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
        (\Term s (list a :--> PBool)
_self -> PBool s -> Term s PBool
forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse)

-- | / O(min(n, m)) /. Check if two lists are equal.
plistEquals :: (PIsListLike list a, PEq a) => Term s (list a :--> list a :--> PBool)
plistEquals :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals =
  ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (list a :--> (list a :--> PBool))
 -> Term s (list a :--> (list a :--> PBool)))
-> ClosedTerm (list a :--> (list a :--> PBool))
-> Term s (list a :--> (list a :--> PBool))
forall a b. (a -> b) -> a -> b
$
    Term
  s
  (((list a :--> (list a :--> PBool))
    :--> (list a :--> (list a :--> PBool)))
   :--> (list a :--> (list a :--> PBool)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((list a :--> (list a :--> PBool))
    :--> (list a :--> (list a :--> PBool)))
   :--> (list a :--> (list a :--> PBool)))
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
-> Term s (list a :--> (list a :--> PBool))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (list a :--> (list a :--> PBool))
 -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
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 (list a) -> Term s (list a) -> Term s PBool)
-> Term s (c :--> (list a :--> (list a :--> PBool)))
plam ((Term s (list a :--> (list a :--> PBool))
  -> Term s (list a) -> Term s (list a) -> Term s PBool)
 -> Term
      s
      ((list a :--> (list a :--> PBool))
       :--> (list a :--> (list a :--> PBool))))
-> (Term s (list a :--> (list a :--> PBool))
    -> Term s (list a) -> Term s (list a) -> Term s PBool)
-> Term
     s
     ((list a :--> (list a :--> PBool))
      :--> (list a :--> (list a :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list a :--> PBool))
self Term s (list a)
xlist Term s (list a)
ylist ->
      (Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList
        ( \Term s a
x Term s (list a)
xs ->
            (Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
y Term s (list a)
ys -> Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
y) (Term s (list a :--> (list a :--> PBool))
self Term s (list a :--> (list a :--> PBool))
-> Term s (list a) -> Term s (list a :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs Term s (list a :--> PBool) -> Term s (list a) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
ys) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False)) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) Term s (list a)
ylist
        )
        ((Term s a -> Term s (list a) -> Term s PBool)
-> Term s PBool -> Term s (list a) -> Term s PBool
forall (a :: S -> Type) (s :: S) (r :: S -> Type).
PElemConstraint list a =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S)
       (r :: S -> Type).
(PListLike list, PElemConstraint list a) =>
(Term s a -> Term s (list a) -> Term s r)
-> Term s r -> Term s (list a) -> Term s r
pelimList (\Term s a
_ Term s (list a)
_ -> AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False) (AsHaskell PBool -> Term s PBool
forall (a :: S -> Type) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
True) Term s (list a)
ylist)
        Term s (list a)
xlist

-- | / O(n) /. Like Haskell level `(!!)` but on the plutarch level
(#!!) :: PIsListLike l a => Term s (l a) -> Term s PInteger -> Term s a
Term s (l a)
l #!! :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (l a) -> Term s PInteger -> Term s a
#!! Term s PInteger
i = Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
l

{- | / O(n) /. Like Haskell level `(!!)` but on the Plutarch level, not infix and
    with arguments reversed, errors if the specified index is greater than or equal
    to the lists length
-}
pelemAt :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
 -> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
  (Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
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 (l a) -> Term s a)
-> Term s (c :--> (l a :--> a))
plam ((Term s PInteger -> Term s (l a) -> Term s a)
 -> Term s (PInteger :--> (l a :--> a)))
-> (Term s PInteger -> Term s (l a) -> Term s a)
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n Term s (l a)
xs ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
0)
      (Term s PString -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"pelemAt: negative index" Term s a
forall (s :: S) (a :: S -> Type). Term s a
perror)
      (Term s (PInteger :--> (l a :--> a))
forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)

-- | / O(n) /. like `pelemAt` but doesn't fail on negative indexes
pelemAt' :: PIsListLike l a => Term s (PInteger :--> l a :--> a)
pelemAt' :: forall (l :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' = ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PInteger :--> (l a :--> a))
 -> Term s (PInteger :--> (l a :--> a)))
-> ClosedTerm (PInteger :--> (l a :--> a))
-> Term s (PInteger :--> (l a :--> a))
forall a b. (a -> b) -> a -> b
$
  Term
  s
  (((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
   :--> (PInteger :--> (l a :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
   :--> (PInteger :--> (l a :--> a)))
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
-> Term s (PInteger :--> (l a :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PInteger :--> (l a :--> a))
 -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
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 PInteger -> Term s (l a) -> Term s a)
-> Term s (c :--> (PInteger :--> (l a :--> a)))
plam ((Term s (PInteger :--> (l a :--> a))
  -> Term s PInteger -> Term s (l a) -> Term s a)
 -> Term
      s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a))))
-> (Term s (PInteger :--> (l a :--> a))
    -> Term s PInteger -> Term s (l a) -> Term s a)
-> Term
     s ((PInteger :--> (l a :--> a)) :--> (PInteger :--> (l a :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (l a :--> a))
self Term s PInteger
n Term s (l a)
xs ->
    Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
      (Term s (l a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)
      (Term s (PInteger :--> (l a :--> a))
self Term s (PInteger :--> (l a :--> a))
-> Term s PInteger -> Term s (l a :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1) Term s (l a :--> a) -> Term s (l a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (l a :--> l a)
forall (a :: S -> Type) (s :: S).
PElemConstraint l a =>
Term s (l a :--> l a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (l a :--> l a) -> Term s (l a) -> Term s (l a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)