{- |
 Module: Plutarch.Extra.List
 Copyright: (C) Liqwid Labs 2022
 License: Apache 2.0
 Maintainer: Koz Ross <[email protected]>
 Portability: GHC only
 Stability: Experimental

 Various helpers for list-like structures. This module is intended to be
 imported qualified.
-}
module Plutarch.Extra.List (
  -- * Construction
  preplicate,
  pfromList,

  -- * Transformation
  pmapMaybe,
  pdeleteFirstBy,
  ptryDeleteFirstBy,
  pdeleteFirst,

  -- * Search
  pfindJust,
  plookupAssoc,

  -- * Elimination
  phandleList,
  precListLookahead,
  ptryElimSingle,

  -- * Comparison
  plistEqualsBy,

  -- * Singleton
  pisSingleton,
  pfromSingleton,
  ptryFromSingleton,
) where

import Plutarch.Extra.Functor (PFunctor (pfmap))
import Plutarch.Extra.Maybe (pjust, pnothing)

{- | 'pelimList' with re-ordered arguments. Useful for cases when the \'nil
 case\' is simple, but the \'cons case\' is complex.

 @since 3.9.0
-}
phandleList ::
  forall (a :: S -> Type) (r :: S -> Type) (ell :: (S -> Type) -> S -> Type) (s :: S).
  (PElemConstraint ell a, PListLike ell) =>
  Term s (ell a) ->
  Term s r ->
  (Term s a -> Term s (ell a) -> Term s r) ->
  Term s r
phandleList :: forall (a :: S -> Type) (r :: S -> Type)
       (ell :: (S -> Type) -> S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
Term s (ell a)
-> Term s r -> (Term s a -> Term s (ell a) -> Term s r) -> Term s r
phandleList Term s (ell a)
xs Term s r
whenNil Term s a -> Term s (ell a) -> Term s r
whenCons = 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 (ell a) -> Term s r
whenCons Term s r
whenNil Term s (ell a)
xs

{- | Similar to 'pelimList', but assumes the argument list-like is a singleton,
 erroring otherwise.

 @since 3.9.0
-}
ptryElimSingle ::
  forall (ell :: (S -> Type) -> S -> Type) (a :: S -> Type) (r :: S -> Type) (s :: S).
  (PElemConstraint ell a, PListLike ell) =>
  (Term s a -> Term s r) ->
  Term s (ell a) ->
  Term s r
ptryElimSingle :: forall (ell :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (r :: S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
(Term s a -> Term s r) -> Term s (ell a) -> Term s r
ptryElimSingle Term s a -> Term s r
f = 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 (ell a) -> Term s r
go (forall (s :: S) (a :: S -> Type). Term s PString -> Term s a
ptraceError Term s PString
emptyErr)
  where
    go ::
      Term s a ->
      Term s (ell a) ->
      Term s r
    go :: Term s a -> Term s (ell a) -> Term s r
go Term s a
h Term s (ell a)
t = forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (ell a)
t) (Term s a -> Term s r
f Term s a
h) (forall (s :: S) (a :: S -> Type). Term s PString -> Term s a
ptraceError Term s PString
nonSingleErr)
    emptyErr :: Term s PString
    emptyErr :: Term s PString
emptyErr = Term s PString
"ptryElimSingle: Found empty list-like."
    nonSingleErr :: Term s PString
    nonSingleErr :: Term s PString
nonSingleErr = Term s PString
"ptryElimSingle: Found non-singleton list-like."

{- | Similar to 'pmap', but allows elements to be thrown out. More precisely,
 for elements where the function argument returns 'PNothing', the
 corresponding element is removed, while for elements where the function
 argument returns `PJust`, the value is used in the result.

     @since 3.14.1
-}
pmapMaybe ::
  forall
    (listO :: (S -> Type) -> (S -> Type))
    (b :: S -> Type)
    (listI :: (S -> Type) -> (S -> Type))
    (a :: S -> Type)
    (s :: S).
  (PIsListLike listI a, PIsListLike listO b) =>
  Term s ((a :--> PMaybe b) :--> listI a :--> listO b)
pmapMaybe :: forall (listO :: (S -> Type) -> S -> Type) (b :: S -> Type)
       (listI :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike listI a, PIsListLike listO b) =>
Term s ((a :--> PMaybe b) :--> (listI a :--> listO b))
pmapMaybe = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PMaybe b)
f -> 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 (forall (s' :: S).
Term s' (a :--> PMaybe b)
-> Term s' (listI a :--> listO b)
-> Term s' a
-> Term s' (listI a)
-> Term s' (listO b)
go Term s (a :--> PMaybe b)
f) (forall a b. a -> b -> a
const forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil)
  where
    go ::
      forall (s' :: S).
      Term s' (a :--> PMaybe b) ->
      Term s' (listI a :--> listO b) ->
      Term s' a ->
      Term s' (listI a) ->
      Term s' (listO b)
    go :: forall (s' :: S).
Term s' (a :--> PMaybe b)
-> Term s' (listI a :--> listO b)
-> Term s' a
-> Term s' (listI a)
-> Term s' (listO b)
go Term s' (a :--> PMaybe b)
f Term s' (listI a :--> listO b)
self Term s' a
x Term s' (listI a)
xs = 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' (a :--> PMaybe b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' a
x) forall a b. (a -> b) -> a -> b
$ \case
      PMaybe b s'
PNothing -> Term s' (listI a :--> listO b)
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (listI a)
xs
      PJust Term s' b
y -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' b
y forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s' (listI a :--> listO b)
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (listI a)
xs

{- | A combination of 'pmap' and 'pfind', but without needing an intermediate
 structure. More precisely, searched for the first element in a list-like
 structure that produces a 'PJust' argument, returning it if found; otherwise,
 produces 'PNothing'.

 @since 3.6.0
-}
pfindJust ::
  forall (b :: S -> Type) (ell :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PElemConstraint ell a, PListLike ell) =>
  Term s ((a :--> PMaybe b) :--> ell a :--> PMaybe b)
pfindJust :: forall (b :: S -> Type) (ell :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
Term s ((a :--> PMaybe b) :--> (ell a :--> PMaybe b))
pfindJust = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PMaybe b)
f -> 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 (forall (s' :: S).
Term s' (a :--> PMaybe b)
-> Term s' (ell a :--> PMaybe b)
-> Term s' a
-> Term s' (ell a)
-> Term s' (PMaybe b)
go Term s (a :--> PMaybe b)
f) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)
  where
    go ::
      forall (s' :: S).
      Term s' (a :--> PMaybe b) ->
      Term s' (ell a :--> PMaybe b) ->
      Term s' a ->
      Term s' (ell a) ->
      Term s' (PMaybe b)
    go :: forall (s' :: S).
Term s' (a :--> PMaybe b)
-> Term s' (ell a :--> PMaybe b)
-> Term s' a
-> Term s' (ell a)
-> Term s' (PMaybe b)
go Term s' (a :--> PMaybe b)
f Term s' (ell a :--> PMaybe b)
self Term s' a
x Term s' (ell a)
xs = 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' (a :--> PMaybe b)
f forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' a
x) forall a b. (a -> b) -> a -> b
$ \case
      PMaybe b s'
PNothing -> Term s' (ell a :--> PMaybe b)
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s' (ell a)
xs
      PJust Term s' b
v -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall a b. (a -> b) -> a -> b
$ forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust Term s' b
v

{- | Treats a list-like structure as an assoc list. More precisely, given a
 list-like structure of key-value pairs, a method of extracting the key and
 the value, and a \'target\' key, returns the corresponding value, or
 'PNothing' if there isn't one.

 = Note

 There may be multiple mappings for a specific key; in such a situation, only
 the /first/ match is returned. In general, this requires time proportional to
 the length of the list-like structure, as we may have to check every entry.

 @since 3.6.0
-}
plookupAssoc ::
  forall (k :: S -> Type) (v :: S -> Type) (kv :: S -> Type) (ell :: (S -> Type) -> S -> Type) (s :: S).
  (PElemConstraint ell kv, PListLike ell, PEq k) =>
  Term s ((kv :--> k) :--> (kv :--> v) :--> k :--> ell kv :--> PMaybe v)
plookupAssoc :: forall (k :: S -> Type) (v :: S -> Type) (kv :: S -> Type)
       (ell :: (S -> Type) -> S -> Type) (s :: S).
(PElemConstraint ell kv, PListLike ell, PEq k) =>
Term
  s
  ((kv :--> k)
   :--> ((kv :--> v) :--> (k :--> (ell kv :--> PMaybe v))))
plookupAssoc = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (kv :--> k)
getKey Term s (kv :--> v)
getVal Term s k
target Term s (ell kv)
kvs ->
    forall (a :: S -> Type) (s :: S) (b :: S -> Type).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (b :: S -> Type) (ell :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
Term s ((a :--> PMaybe b) :--> (ell a :--> PMaybe b))
pfindJust forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (s' :: S).
Term s' ((kv :--> k) :--> (k :--> (kv :--> PMaybe kv)))
go forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (kv :--> k)
getKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s k
target) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (ell kv)
kvs) forall a b. (a -> b) -> a -> b
$ \case
      PMaybe kv s
PNothing -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing
      PJust Term s kv
kv -> forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust forall a b. (a -> b) -> a -> b
$ Term s (kv :--> v)
getVal forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s kv
kv
  where
    go ::
      forall (s' :: S).
      Term s' ((kv :--> k) :--> k :--> kv :--> PMaybe kv)
    go :: forall (s' :: S).
Term s' ((kv :--> k) :--> (k :--> (kv :--> PMaybe kv)))
go = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
      forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (kv :--> k)
getKey Term s k
target Term s kv
kv ->
        forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s k
target forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s (kv :--> k)
getKey forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s kv
kv))
          (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: S -> Type) (s :: S). Term s a -> PMaybe a s
PJust forall a b. (a -> b) -> a -> b
$ Term s kv
kv)
          (forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall (a :: S -> Type) (s :: S). PMaybe a s
PNothing)

{- | Given a count @n@ and a value @x@, produces a list-like structure
 containing @n@ copies of @x@, or an empty structure if @n@ is non-positive.

 = Note

 You will likely need to specify which list-like structure you want; the type
 arguments for this function are optimized for use with `TypeApplications` to
 do exactly this task.

 @since 3.6.0
-}
preplicate ::
  forall (ell :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PElemConstraint ell a, PListLike ell) =>
  Term s (PInteger :--> a :--> ell a)
preplicate :: forall (ell :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
Term s (PInteger :--> (a :--> ell a))
preplicate = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (a :--> ell a))
self Term s PInteger
count Term s a
x ->
    forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
      (Term s PInteger
count forall (t :: S -> Type) (s :: S).
PPartialOrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
      forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil
      (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PInteger :--> (a :--> ell a))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
count forall a. Num a => a -> a -> a
- Term s PInteger
1) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x))

-- Similar to 'precList', but with a \'look-ahead\' in the list-like structure
-- being eliminated. This is more efficient than repeated use of 'pelimList' (or
-- worse, 'puncons'). Furthermore, the \'self argument\' is not passed to the
-- \'nil\' and \'singleton\' cases, as it's pointless there.
--
-- @ since 3.6.0
precListLookahead ::
  forall (a :: S -> Type) (r :: S -> Type) (ell :: (S -> Type) -> S -> Type) (s :: S).
  (PElemConstraint ell a, PListLike ell) =>
  -- | The \'two or more\' case. First @'Term' s a@ is the \'head\', second is
  -- a \'peek-ahead\', while the @'Term' s (ell a)@ is what remains /after/
  -- the \'peek-ahead\'.
  (Term s (a :--> ell a :--> r) -> Term s a -> Term s a -> Term s (ell a) -> Term s r) ->
  -- | The \'singleton\' case, used both for true singletons and also for the
  -- end of a non-empty list-like.
  (Term s a -> Term s r) ->
  -- | The \'nil\' case.
  Term s r ->
  Term s (ell a :--> r)
precListLookahead :: forall (a :: S -> Type) (r :: S -> Type)
       (ell :: (S -> Type) -> S -> Type) (s :: S).
(PElemConstraint ell a, PListLike ell) =>
(Term s (a :--> (ell a :--> r))
 -> Term s a -> Term s a -> Term s (ell a) -> Term s r)
-> (Term s a -> Term s r) -> Term s r -> Term s (ell a :--> r)
precListLookahead Term s (a :--> (ell a :--> r))
-> Term s a -> Term s a -> Term s (ell a) -> Term s r
whenContinuing Term s a -> Term s r
whenOne Term s r
whenDone =
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$
    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 (ell a)
xs -> (forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ Term s (a :--> (ell a :--> r))
-> Term s a -> Term s (ell a) -> Term s r
go) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (ell a)
xs) Term s r
whenDone
  where
    go ::
      Term s (a :--> ell a :--> r) ->
      Term s a ->
      Term s (ell a) ->
      Term s r
    go :: Term s (a :--> (ell a :--> r))
-> Term s a -> Term s (ell a) -> Term s r
go Term s (a :--> (ell a :--> r))
self Term s a
h =
      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 :--> (ell a :--> r))
-> Term s a -> Term s a -> Term s (ell a) -> Term s r
whenContinuing Term s (a :--> (ell a :--> r))
self Term s a
h)
        (Term s a -> Term s r
whenOne Term s a
h)

{- | Turn a Haskell-level list of "Term"s into a "PListLike"
 @since 3.9.0
-}
pfromList ::
  forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
  (PIsListLike list a) =>
  [Term s a] ->
  Term s (list a)
pfromList :: forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
PIsListLike list a =>
[Term s a] -> Term s (list a)
pfromList = forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term s a
x Term s (list a)
xs -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
xs) forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil

{- | Check if two lists are equal. The two list types can be different. The first
     argument is used for equality checks.

     @since 3.14.1
-}
plistEqualsBy ::
  forall
    (list1 :: (S -> Type) -> (S -> Type))
    (list2 :: (S -> Type) -> (S -> Type))
    (a :: S -> Type)
    (b :: S -> Type)
    (s :: S).
  (PIsListLike list1 a, PIsListLike list2 b) =>
  Term s ((a :--> b :--> PBool) :--> list1 a :--> list2 b :--> PBool)
plistEqualsBy :: forall (list1 :: (S -> Type) -> S -> Type)
       (list2 :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PIsListLike list1 a, PIsListLike list2 b) =>
Term
  s
  ((a :--> (b :--> PBool)) :--> (list1 a :--> (list2 b :--> PBool)))
plistEqualsBy = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (b :--> PBool))
eq -> forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (list1 a :--> (list2 b :--> PBool))
self Term s (list1 a)
l1 Term s (list2 b)
l2 ->
    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 (list1 a)
xs ->
          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 b
y Term s (list2 b)
ys ->
                -- Avoid comparison if two lists have different length.
                Term s (list1 a :--> (list2 b :--> PBool))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list1 a)
xs forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list2 b)
ys forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s (a :--> (b :--> PBool))
eq forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
y
            )
            -- l2 is empty, but l1 is not.
            (forall (p :: S -> Type) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False)
            Term s (list2 b)
l2
      )
      -- l1 is empty, so l2 should be empty as well.
      (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list2 b)
l2)
      Term s (list1 a)
l1

{- | / O(n) /. Remove the first occurance of a value that satisfies the
     predicate from the given list. Return nothing if said value is not in
     the list.

     @since 3.14.1
-}
pdeleteFirstBy ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PIsListLike list a) =>
  Term s ((a :--> PBool) :--> list a :--> PMaybe (list a))
pdeleteFirstBy :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PMaybe (list a)))
pdeleteFirstBy = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
p ->
    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 :--> PMaybe (list a))
self Term s a
h Term s (list a)
t ->
          forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s (a :--> PBool)
p forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
h)
            (forall (a :: S -> Type) (s :: S). Term s (a :--> PMaybe a)
pjust forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t)
            (forall (f :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PFunctor f, PSubcategory f a, PSubcategory f b) =>
Term s ((a :--> b) :--> (f a :--> f b))
pfmap forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
h) forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (list a :--> PMaybe (list a))
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t))
      )
      (forall a b. a -> b -> a
const forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing)

{- | Partial version of 'pdeleteBy'.

     @since 3.14.1
-}
ptryDeleteFirstBy ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PIsListLike list a) =>
  Term s ((a :--> PBool) :--> list a :--> list a)
ptryDeleteFirstBy :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
ptryDeleteFirstBy = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
  forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s (a :--> PBool)
p ->
    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 :--> list a)
self Term s a
h Term s (list a)
t ->
          forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s (a :--> PBool)
p forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
h)
            Term s (list a)
t
            (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
h forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (list a :--> list a)
self forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t)
      )
      (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type). Term s PString -> Term s a
ptraceError Term s PString
"Cannot delete element")

{- | Special version of 'pdeleteBy', for types with 'PEq' instance.

     @since 3.14.1
-}
pdeleteFirst ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PEq a, PIsListLike list a) =>
  Term s (a :--> list a :--> PMaybe (list a))
pdeleteFirst :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
(PEq a, PIsListLike list a) =>
Term s (a :--> (list a :--> PMaybe (list a)))
pdeleteFirst = forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$ forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam forall a b. (a -> b) -> a -> b
$ \Term s a
x -> forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PMaybe (list a)))
pdeleteFirstBy forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
plam (forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s a
x)

{- | / O(1) /.Return true if the given list has exactly one element.

     @since 3.14.1
-}
pisSingleton ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PIsListLike list a) =>
  Term s (list a :--> PBool)
pisSingleton :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PBool)
pisSingleton =
  forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    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)
_ Term s a
_ Term s (list a)
t -> forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t)
      (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (p :: S -> Type) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
False)

{- | Extract a singeton value from the given list. Return nothing if the list
     consists of zero or more than one elements.

     @since 3.14.1
-}
pfromSingleton ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PIsListLike list a) =>
  Term s (list a :--> PMaybe a)
pfromSingleton :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> PMaybe a)
pfromSingleton =
  forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    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 :--> PMaybe a)
_ Term s a
h Term s (list a)
t ->
          forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t)
            (forall (a :: S -> Type) (s :: S). Term s (a :--> PMaybe a)
pjust forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
h)
            forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing
      )
      (forall a b. a -> b -> a
const forall (a :: S -> Type) (s :: S). Term s (PMaybe a)
pnothing)

{- | Partial version of `pfromSingleton`.

     @since 3.14.1
-}
ptryFromSingleton ::
  forall
    (a :: S -> Type)
    (list :: (S -> Type) -> (S -> Type))
    (s :: S).
  (PIsListLike list a) =>
  Term s (list a :--> a)
ptryFromSingleton :: forall (a :: S -> Type) (list :: (S -> Type) -> S -> Type)
       (s :: S).
PIsListLike list a =>
Term s (list a :--> a)
ptryFromSingleton =
  forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic forall a b. (a -> b) -> a -> b
$
    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 :--> a)
_ Term s a
h Term s (list a)
t ->
          forall (s :: S) (a :: S -> Type).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (list a)
t)
            Term s a
h
            (forall (s :: S) (a :: S -> Type). Term s PString -> Term s a
ptraceError Term s PString
"More than one element")
      )
      (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (s :: S) (a :: S -> Type). Term s PString -> Term s a
ptraceError Term s PString
"Empty list")