-- | Scott-encoded lists and ListLike typeclass
module Plutarch.List (
  PList (..),
  PListLike (..),
  PIsListLike,
  pconvertLists,
  pshowList,

  -- * Comparison
  plistEquals,

  -- * Query
  pelem,
  plength,
  ptryIndex,
  pdrop,
  pfind,
  pelemAt,
  (#!!),

  -- * Construction
  psingleton,

  -- * Deconstruction
  puncons,
  ptryUncons,

  -- * Combine
  pconcat,
  pzipWith,
  pzipWith',
  pzip,

  -- * Traversals
  pmap,
  pfilter,

  -- * Catamorphisms
  precList,
  pfoldr,
  pfoldr',
  pfoldrLazy,
  pfoldl,
  pfoldl',

  -- * Special Folds
  pall,
  pany,
) where

import Numeric.Natural (Natural)

import GHC.Generics (Generic)
import Plutarch (
  ClosedTerm,
  DPTStrat,
  DerivePlutusType,
  PDelayed,
  PType,
  PlutusType,
  PlutusTypeScott,
  S,
  Term,
  pcon,
  pdelay,
  perror,
  pfix,
  phoistAcyclic,
  plam,
  plet,
  pmatch,
  (#),
  (#$),
  type (:-->),
 )
import Plutarch.Bool (PBool (PFalse, PTrue), PEq, pif, (#&&), (#<), (#==), (#||))
import Plutarch.Integer (PInteger)
import Plutarch.Lift (pconstant)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Pair (PPair (PPair))
import Plutarch.String (PString)

import Data.Kind
import Plutarch.Show (PShow (pshow'), pshow)
import Plutarch.Trace (ptraceError)

data PList (a :: PType) (s :: S)
  = PSCons (Term s a) (Term s (PList a))
  | PSNil
  deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (a :: PType) (s :: S) x. Rep (PList a s) x -> PList a s
forall (a :: PType) (s :: S) x. PList a s -> Rep (PList a s) x
$cto :: forall (a :: PType) (s :: S) x. Rep (PList a s) x -> PList a s
$cfrom :: forall (a :: PType) (s :: S) x. PList a s -> Rep (PList a s) x
Generic)
  deriving anyclass (forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
forall (a :: PType) (s :: S).
PList a s -> Term s (PInner (PList a))
forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
$cpmatch' :: forall (a :: PType) (s :: S) (b :: PType).
Term s (PInner (PList a)) -> (PList a s -> Term s b) -> Term s b
pcon' :: forall (s :: S). PList a s -> Term s (PInner (PList a))
$cpcon' :: forall (a :: PType) (s :: S).
PList a s -> Term s (PInner (PList a))
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 :: PType -> PType) (a :: PType) (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList @PList @a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
x

pshowList :: forall list a s. (PShow a, PIsListLike list a) => Term s (list a :--> PString)
pshowList :: forall (list :: PType -> PType) (a :: PType) (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a)
list ->
      Term s PString
"[" forall a. Semigroup a => a -> a -> a
<> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList' @list @a forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
list forall a. Semigroup a => a -> a -> a
<> Term s PString
"]"

pshowList' :: forall list a s. (PShow a, PIsListLike list a) => Term s (list a :--> PString)
pshowList' :: forall (list :: PType -> PType) (a :: PType) (s :: S).
(PShow a, PIsListLike list a) =>
Term s (list a :--> PString)
pshowList' =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> PString)
self Term s a
x Term s (list a)
xs ->
          forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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)
_ -> forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow Term s a
x forall a. Semigroup a => a -> a -> a
<> Term s PString
", " forall a. Semigroup a => a -> a -> a
<> Term s (list a :--> PString)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
            (forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow Term s a
x)
            Term s (list a)
xs
      )
      (forall a b. a -> b -> a
const Term s PString
"")

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 = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PList a)
ys

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

-- | 'PIsListLike list a' constraints 'list' be a 'PListLike' with valid element type, 'a'.
type PIsListLike list a = (PListLike list, PElemConstraint list a)

-- | Plutarch types that behave like lists.
class PListLike (list :: PType -> PType) where
  type PElemConstraint list (a :: PType) :: Constraint

  -- | Canonical eliminator for list-likes.
  pelimList ::
    PElemConstraint list a =>
    (Term s a -> Term s (list a) -> Term s r) ->
    Term s r ->
    Term s (list a) ->
    Term s r

  -- | Cons an element onto an existing list.
  pcons :: PElemConstraint list a => Term s (a :--> list a :--> list a)

  -- | The empty list
  pnil :: PElemConstraint list a => Term s (list a)

  -- | Return the first element of a list. Partial, throws an error upon encountering an empty list.
  phead :: PElemConstraint list a => Term s (list a :--> a)
  phead = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 forall a b. a -> b -> a
const forall (s :: S) (a :: PType). Term s a
perror

  -- | Take the tail of a list, meaning drop its head. Partial, throws an error upon encountering an empty list.
  ptail :: PElemConstraint list a => Term s (list a :--> list a)
  ptail = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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)
xs -> Term s (list a)
xs) forall (s :: S) (a :: PType). Term s a
perror

  -- | / O(1) /. Check if a list is empty
  pnull :: PElemConstraint list a => Term s (list a :--> PBool)
  pnull = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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)
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False) forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True

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

-- | / O(n) /. Convert from any ListLike to any ListLike, provided both lists' element constraints are met.
pconvertLists ::
  forall f g a s.
  (PIsListLike f a, PIsListLike g a) =>
  Term s (f a :--> g a)
pconvertLists :: forall (f :: PType -> PType) (g :: PType -> PType) (a :: PType)
       (s :: S).
(PIsListLike f a, PIsListLike g a) =>
Term s (f a :--> g a)
pconvertLists = 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 :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (f a :--> g a)
self ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 (f a)
xs -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (f a :--> g a)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (f a)
xs)
      forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

-- | 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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PPair a (list a))
ptryUncons =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) forall (s :: S) (a :: PType). 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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe (PPair a (list a)))
puncons =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x) (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing)

-- | Like 'pelimList', but with a fixpoint recursion hatch.
precList ::
  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 :: forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> r) -> Term s a -> Term s (list a) -> Term s r
mcons Term s (list a :--> r) -> Term s r
mnil =
  forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> r)
self ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 (list a :--> r) -> Term s a -> Term s (list a) -> Term s r
mcons Term s (list a :--> r)
self)
      (Term s (list a :--> r) -> Term s r
mnil Term s (list a :--> r)
self)

--------------------------------------------------------------------------------
-- Construction

-- | / O(1) /. Create a singleton list from an element
psingleton :: PIsListLike list a => Term s (a :--> list a)
psingleton :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (a :--> list a)
psingleton = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

--------------------------------------------------------------------------------
-- Querying

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

-- | / O(n) /. Count the number of elements in the list
plength :: PIsListLike list a => Term s (list a :--> PInteger)
plength :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger)
plength =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    let go :: PIsListLike list a => Term s (PInteger :--> list a :--> PInteger)
        go :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (PInteger :--> (list a :--> PInteger))
go = forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (list a :--> PInteger))
self Term s PInteger
n -> forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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)
xs -> Term s (PInteger :--> (list a :--> PInteger))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n forall a. Num a => a -> a -> a
+ Term s PInteger
1) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) Term s PInteger
n
     in forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (PInteger :--> (list a :--> PInteger))
go forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
0

-- | Index a BuiltinList, throwing an error if the index is out of bounds.
ptryIndex :: (PIsListLike list a) => Natural -> Term s (list a) -> Term s a
ptryIndex :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s a
ptryIndex Natural
n Term s (list a)
xs = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s (list a)
pdrop Natural
n Term s (list a)
xs

{- |
  Drop the first n fields of a List.

  The term will be statically generated as
  repeated applications of 'ptail', which will be more
  efficient in many circumstances.
-}
pdrop :: (PIsListLike list a) => Natural -> Term s (list a) -> Term s (list a)
pdrop :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Natural -> Term s (list a) -> Term s (list a)
pdrop Natural
n Term s (list a)
xs = forall (list :: PType -> PType) (a :: PType).
PIsListLike list a =>
Natural -> ClosedTerm (list a :--> list a)
pdrop' Natural
n forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs
  where
    pdrop' :: (PIsListLike list a) => Natural -> ClosedTerm (list a :--> list a)
    pdrop' :: forall (list :: PType -> PType) (a :: PType).
PIsListLike list a =>
Natural -> ClosedTerm (list a :--> list a)
pdrop' Natural
0 = forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a. a -> a
id
    pdrop' Natural
1 = forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail
    pdrop' Natural
n' = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a)
x -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType).
PIsListLike list a =>
Natural -> ClosedTerm (list a :--> list a)
pdrop' (Natural
n' forall a. Num a => a -> a -> a
- Natural
1) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
x

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

-- | / O(n) /. Fold on a list left-associatively.
pfoldl :: PIsListLike list a => Term s ((b :--> a :--> b) :--> b :--> list a :--> b)
pfoldl :: forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((b :--> (a :--> b)) :--> (b :--> (list a :--> b)))
pfoldl = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (a :--> b))
f ->
    forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (list a :--> b))
self Term s b
z ->
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 (b :--> (list a :--> b))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (b :--> (a :--> b))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
z forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        Term s b
z

-- | The same as 'pfoldl', but with Haskell-level reduction function.
pfoldl' :: PIsListLike list a => (forall s. Term s b -> Term s a -> Term s b) -> Term s (b :--> list a :--> b)
pfoldl' :: forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
PIsListLike list a =>
(forall (s :: S). Term s b -> Term s a -> Term s b)
-> Term s (b :--> (list a :--> b))
pfoldl' forall (s :: S). Term s b -> Term s a -> Term s b
f = 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 :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (b :--> (list a :--> b))
self Term s b
z ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 (b :--> (list a :--> b))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S). Term s b -> Term s a -> Term s b
f Term s b
z Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
      Term s b
z

-- | / O(n) /. Fold on a list right-associatively.
pfoldr :: PIsListLike list a => Term s ((a :--> b :--> b) :--> b :--> list a :--> b)
pfoldr :: forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
pfoldr = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> b))
f Term s b
z ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> b)
self Term s a
x Term s (list a)
xs -> Term s (a :--> (b :--> b))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> b)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (forall a b. a -> b -> a
const Term s b
z)

-- | The same as 'pfoldr'', but with Haskell-level reduction function.
pfoldr' :: PIsListLike list a => (forall s. Term s a -> Term s b -> Term s b) -> Term s (b :--> list a :--> b)
pfoldr' :: forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
PIsListLike list a =>
(forall (s :: S). Term s a -> Term s b -> Term s b)
-> Term s (b :--> (list a :--> b))
pfoldr' forall (s :: S). Term s a -> Term s b -> Term s b
f = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s b
z ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> b)
self Term s a
x Term s (list a)
xs -> forall (s :: S). Term s a -> Term s b -> Term s b
f Term s a
x (Term s (list a :--> b)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (forall a b. a -> b -> a
const Term s b
z)

{- | / O(n) /. Fold on a list right-associatively, with opportunity for short circuting.

May short circuit when given reducer function is lazy in its second argument.
-}
pfoldrLazy :: PIsListLike list a => Term s ((a :--> PDelayed b :--> b) :--> b :--> list a :--> b)
pfoldrLazy :: forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((a :--> (PDelayed b :--> b)) :--> (b :--> (list a :--> b)))
pfoldrLazy = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (PDelayed b :--> b))
f Term s b
z ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> b)
self Term s a
x Term s (list a)
xs -> Term s (a :--> (PDelayed b :--> b))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall (s :: S) (a :: PType). Term s a -> Term s (PDelayed a)
pdelay (Term s (list a :--> b)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
      (forall a b. a -> b -> a
const Term s b
z)

-- | / O(n) /. Check that predicate holds for all elements in a list.
pall :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
pall :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 (a :--> PBool)
predicate forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s (list a :--> PBool)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
True)

-- | / O(n) /. Check that predicate holds for any element in a list.
pany :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
pany :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pany = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 (a :--> PBool)
predicate forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s (list a :--> PBool)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False)

-- | / O(n) /. Map a function over a list of elements
pmap :: (PListLike list, PElemConstraint list a, PElemConstraint list b) => Term s ((a :--> b) :--> list a :--> list b)
pmap :: forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> b)
f ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> list b)
self Term s a
x Term s (list a)
xs -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> b)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list b)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)) (forall a b. a -> b -> a
const forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)

-- | / O(n) /. Filter elements from a list that don't match the predicate.
pfilter :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> list a)
pfilter :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
pfilter =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
predicate ->
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> list a)
self Term s a
x' Term s (list a)
xs -> forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s a
x' forall a b. (a -> b) -> a -> b
$ \Term s a
x ->
            forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (Term s (a :--> PBool)
predicate forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x)
              (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list a)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs))
              (Term s (list a :--> list a)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        )
        (forall a b. a -> b -> a
const forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)

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

{- | / O(n) /. Concatenate two lists

 Example:
 > pconcat # psingleton x # psingleton y == plistLiteral [x, y]

 pconcat exhibits identities with empty lists such that
 > forall x. pconcat # pnil # x == x
 > forall x. pconcat # x # pnil == x
-}
pconcat :: PIsListLike list a => Term s (list a :--> list a :--> list a)
pconcat :: forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> (list a :--> list a))
pconcat =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a)
xs Term s (list a)
ys ->
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
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 :--> list a)
self Term s a
x Term s (list a)
xs ->
            forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> list a)
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs)
        )
        (forall a b. a -> b -> a
const Term s (list a)
ys)
        # xs

{- | / O(min(n, m)) /. Zip two lists together with a passed function.

If the lists are of differing lengths, cut to the shortest.
-}
pzipWith ::
  ( PListLike list
  , PElemConstraint list a
  , PElemConstraint list b
  , PElemConstraint list c
  ) =>
  Term s ((a :--> b :--> c) :--> list a :--> list b :--> list c)
pzipWith :: forall (list :: PType -> PType) (a :: PType) (b :: PType)
       (c :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b,
 PElemConstraint list c) =>
Term
  s ((a :--> (b :--> c)) :--> (list a :--> (list b :--> list c)))
pzipWith =
  forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> c))
f ->
      forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list b :--> list c))
self Term s (list a)
lx Term s (list b)
ly ->
        forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 ->
              forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 b
y Term s (list b)
ys -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> (b :--> c))
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> (list b :--> list c))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list b)
ys))
                forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
                Term s (list b)
ly
          )
          forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
          Term s (list a)
lx

-- | Like 'pzipWith' but with Haskell-level merge function.
pzipWith' ::
  ( 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' :: forall (list :: PType -> PType) (a :: PType) (b :: PType)
       (c :: PType) (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 c
f =
  forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list a :--> (list b :--> list c))
self Term s (list a)
lx Term s (list b)
ly ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 ->
          forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 b
y Term s (list b)
ys -> forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s b -> Term s c
f Term s a
x Term s b
y forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> (list b :--> list c))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list b)
ys))
            forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
            Term s (list b)
ly
      )
      forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
      Term s (list a)
lx

{- | / 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 :: PType -> PType) (a :: PType) (b :: PType) (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 = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall (list :: PType -> PType) (a :: PType) (b :: PType)
       (c :: PType) (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' forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s b
y -> forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s a
x Term s b
y)

-- | / 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 :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (list a :--> (list a :--> PBool))
plistEquals =
  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 :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam 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 ->
      forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 ->
            forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 -> forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x forall (t :: PType) (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 forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
ys) (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False)) (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False) Term s (list a)
ylist
        )
        (forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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)
_ -> forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False) (forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (l a) -> Term s PInteger -> Term s a
#!! Term s PInteger
i = forall (l :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt = forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n Term s (l a)
xs ->
    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n forall (t :: PType) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
0)
      (forall (s :: S) (a :: PType). Term s PString -> Term s a
ptraceError Term s PString
"pelemAt: negative index")
      (forall (l :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s (PInteger :--> (l a :--> a))
pelemAt' = 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 :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (l a :--> a))
self Term s PInteger
n Term s (l a)
xs ->
    forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
n forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
      (forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)
      (Term s (PInteger :--> (l a :--> a))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
n forall a. Num a => a -> a -> a
- Term s PInteger
1) forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
xs)

-- | / 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 :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind = 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 :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam 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 ->
    forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
(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 ->
          forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s (a :--> PBool)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
y)
            (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: PType) (s :: S). Term s a -> PMaybe a s
PJust Term s a
y)
            (Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
self forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (a :--> PBool)
f forall (s :: S) (a :: PType) (b :: PType).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (l a)
ys)
      )
      (forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: PType) (s :: S). PMaybe a s
PNothing)
      Term s (l a)
xs