{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

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

import Data.Bifunctor (bimap)
import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Generics (Generic)
import GHC.TypeLits (KnownNat, natVal, type (+), type (-))
import Generics.SOP (NP (..))
import Generics.SOP qualified as SOP
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 (
  PlutusType,
  pcon,
  pmatch,
 )
import Plutarch.Internal.Show (PShow (pshow'), pshowList)
import Plutarch.Internal.Term (
  InternalConfig (..),
  S,
  Term,
  perror,
  pgetInternalConfig,
  phoistAcyclic,
  plet,
  pplaceholder,
  punsafeCoerce,
  pwithInternalConfig,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.TermCont (pfindAllPlaceholders, unTermCont)
import Plutarch.Internal.Trace (ptraceInfo)
import Plutarch.Maybe (PMaybe (PJust, PNothing))
import Plutarch.Pair (PPair (PPair))
import Plutarch.Repr.SOP (DeriveAsSOPStruct (DeriveAsSOPStruct))

{- | SOP-encoded list.

@since 1.10.0
-}
data PList (a :: S -> Type) (s :: S)
  = PSCons (Term s a) (Term s (PList a))
  | PSNil
  deriving stock
    ( -- | @since 1.10.0
      (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
    ( -- | @since 1.10.0
      All @[Type] (SListI @Type) (Code (PList a s))
All @[Type] (SListI @Type) (Code (PList a s)) =>
(PList a s -> Rep (PList a s))
-> (Rep (PList a s) -> PList a s) -> Generic (PList a s)
Rep (PList a s) -> PList a s
PList a s -> Rep (PList a s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (a :: S -> Type) (s :: S).
All @[Type] (SListI @Type) (Code (PList a s))
forall (a :: S -> Type) (s :: S). Rep (PList a s) -> PList a s
forall (a :: S -> Type) (s :: S). PList a s -> Rep (PList a s)
$cfrom :: forall (a :: S -> Type) (s :: S). PList a s -> Rep (PList a s)
from :: PList a s -> Rep (PList a s)
$cto :: forall (a :: S -> Type) (s :: S). Rep (PList a s) -> PList a s
to :: Rep (PList a s) -> PList a s
SOP.Generic
    )

-- | @since 1.10.0
deriving via
  DeriveAsSOPStruct (PList a)
  instance
    PlutusType (PList a)

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 1.10.0
-}
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 1.10.0
-}
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)

{- | Match first N elements from the list. It's is better to use @pmatchList@ if number of elements that needs to be
match does not need to be dynamically determined. It is important to understand each element given in Haskell
list is "computation" to get nth element. If those need to be referenced multiple times, it needs to be pletted to
prevent duplication of computation.

@since WIP
-}
pmatchListN ::
  forall b li a s.
  PIsListLike li a =>
  Integer ->
  Term s (li a) ->
  ([Term s a] -> Term s (li a) -> Term s b) ->
  Term s b
pmatchListN :: forall (b :: S -> Type) (li :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
PIsListLike li a =>
Integer
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s b)
-> Term s b
pmatchListN Integer
n Term s (li a)
xs [Term s a] -> Term s (li a) -> Term s b
f = (InternalConfig -> Term s b) -> Term s b
forall (s :: S) (a :: S -> Type).
(InternalConfig -> Term s a) -> Term s a
pgetInternalConfig ((InternalConfig -> Term s b) -> Term s b)
-> (InternalConfig -> Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ \InternalConfig
cfg -> TermCont @b s (Term s b) -> Term s b
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ do
  let
    -- placeholders are from 0 to n - 1, n is the "rest" part
    placeholders :: [Term s a]
placeholders = Integer -> Term s a
forall (s :: S) (a :: S -> Type). Integer -> Term s a
pplaceholder (Integer -> Term s a) -> [Integer] -> [Term s a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
Item [Integer]
0 .. (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)]
    placeholderApplied :: Term s b
placeholderApplied = InternalConfig -> Term s b -> Term s b
forall (s :: S) (a :: S -> Type).
InternalConfig -> Term s a -> Term s a
pwithInternalConfig (Bool -> InternalConfig
InternalConfig Bool
False) (Term s b -> Term s b) -> Term s b -> Term s b
forall a b. (a -> b) -> a -> b
$ [Term s a] -> Term s (li a) -> Term s b
f [Term s a]
placeholders (Integer -> Term s (li a)
forall (s :: S) (a :: S -> Type). Integer -> Term s a
pplaceholder Integer
n)

  [Integer]
usedFields <-
    if InternalConfig -> Bool
internalConfig'dataRecPMatchOptimization InternalConfig
cfg
      then Term s b -> TermCont @b s [Integer]
forall {r :: S -> Type} (s :: S) (a :: S -> Type).
Term s a -> TermCont @r s [Integer]
pfindAllPlaceholders Term s b
placeholderApplied
      else [Integer] -> TermCont @b s [Integer]
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [Integer
Item [Integer]
0 .. Integer
Item [Integer]
n]

  Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s b -> TermCont @b s (Term s b))
-> Term s b -> TermCont @b s (Term s b)
forall a b. (a -> b) -> a -> b
$ Integer
-> [Integer]
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s b)
-> Term s b
forall (b :: S -> Type) (li :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
PIsListLike li a =>
Integer
-> [Integer]
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s b)
-> Term s b
pmatchList' Integer
n [Integer]
usedFields Term s (li a)
xs [Term s a] -> Term s (li a) -> Term s b
f

{- | Same functionality to @pmatchListN@ but each matched value will be given in @NP@ for better typing. Same performance
implications as @pmatchListN@.

@since WIP
-}
pmatchList ::
  forall n r li a s.
  ( PIsListLike li a
  , KnownNat (Length (Replicate n a))
  , UnsafeConstrNP (Replicate n a)
  ) =>
  Term s (li a) ->
  (NP (Term s) (Replicate n a) -> Term s (li a) -> Term s r) ->
  Term s r
pmatchList :: forall (n :: Natural) (r :: S -> Type)
       (li :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike li a,
 KnownNat (Length @(S -> Type) (Replicate @(S -> Type) n a)),
 UnsafeConstrNP (Replicate @(S -> Type) n a)) =>
Term s (li a)
-> (NP @(S -> Type) (Term s) (Replicate @(S -> Type) n a)
    -> Term s (li a) -> Term s r)
-> Term s r
pmatchList = forall (struct :: [S -> Type]) (r :: S -> Type)
       (li :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike li a, KnownNat (Length @(S -> Type) struct),
 UnsafeConstrNP struct) =>
Term s (li a)
-> (NP @(S -> Type) (Term s) struct -> Term s (li a) -> Term s r)
-> Term s r
pmatchListUnsafe @(Replicate n a)

{- | Same as @pmatchList@ but allows matching each element to arbitrary type. Essentially, this is @pmatchList@ combined
with @punsafeCoerce@; therefore, this is unsafe and will require careful attention when using this.

This function is especially helpful when matching on @PBuiltinList (PData)@ when user knows the type of each elements.
If first two elements are Data Integers, one can use @pmatchListUnsafe @'[PAsData PInteger, PAsData PInteger] li@ and
have everything already coerced when it's being matched.

@since WIP
-}
pmatchListUnsafe ::
  forall (struct :: [S -> Type]) r li a s.
  (PIsListLike li a, KnownNat (Length struct), UnsafeConstrNP struct) =>
  Term s (li a) ->
  (NP (Term s) struct -> Term s (li a) -> Term s r) ->
  Term s r
pmatchListUnsafe :: forall (struct :: [S -> Type]) (r :: S -> Type)
       (li :: (S -> Type) -> S -> Type) (a :: S -> Type) (s :: S).
(PIsListLike li a, KnownNat (Length @(S -> Type) struct),
 UnsafeConstrNP struct) =>
Term s (li a)
-> (NP @(S -> Type) (Term s) struct -> Term s (li a) -> Term s r)
-> Term s r
pmatchListUnsafe Term s (li a)
xs NP @(S -> Type) (Term s) struct -> Term s (li a) -> Term s r
f =
  let
    go :: [Term s a] -> Term s (li a) -> Term s r
go [Term s a]
xs' Term s (li a)
rest =
      case forall (xs :: [S -> Type]) (a :: S -> Type) (s :: S).
UnsafeConstrNP xs =>
[Term s a] -> Maybe (NP @(S -> Type) (Term s) xs)
constrNP @struct [Term s a]
xs' of
        Maybe (NP @(S -> Type) (Term s) struct)
Nothing -> [Char] -> Term s r
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
        Just NP @(S -> Type) (Term s) struct
xs'' -> NP @(S -> Type) (Term s) struct -> Term s (li a) -> Term s r
f NP @(S -> Type) (Term s) struct
xs'' Term s (li a)
rest
   in
    Integer
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s r)
-> Term s r
forall (b :: S -> Type) (li :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
PIsListLike li a =>
Integer
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s b)
-> Term s b
pmatchListN (Proxy @Natural (Length @(S -> Type) struct) -> Integer
forall (n :: Natural) (proxy :: Natural -> Type).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Natural). Proxy @Natural t
forall {k} (t :: k). Proxy @k t
Proxy @(Length struct))) Term s (li a)
xs [Term s a] -> Term s (li a) -> Term s r
go

-- TODO: make pmatchDataRec use this
-- NOTE: Maybe not, it could require some more coercing, less safer when messing with internal code.
pmatchList' ::
  forall b li a s.
  PIsListLike li a =>
  Integer ->
  [Integer] ->
  Term s (li a) ->
  ([Term s a] -> Term s (li a) -> Term s b) ->
  Term s b
pmatchList' :: forall (b :: S -> Type) (li :: (S -> Type) -> S -> Type)
       (a :: S -> Type) (s :: S).
PIsListLike li a =>
Integer
-> [Integer]
-> Term s (li a)
-> ([Term s a] -> Term s (li a) -> Term s b)
-> Term s b
pmatchList' Integer
n [Integer]
usedFields Term s (li a)
xs [Term s a] -> Term s (li a) -> Term s b
f = TermCont @b s (Term s b) -> Term s b
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @b s (Term s b) -> Term s b)
-> TermCont @b s (Term s b) -> Term s b
forall a b. (a -> b) -> a -> b
$ do
  let
    mkMatches ::
      Integer ->
      Term s (li a) ->
      (Integer, Term s (li a)) ->
      ([(Term s a, Term s (li a))] -> Term s r) ->
      Term s r
    mkMatches :: forall (r :: S -> Type).
Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
mkMatches Integer
idx Term s (li a)
running lastBind :: (Integer, Term s (li a))
lastBind@(Integer
lastBindIdx, Term s (li a)
lastBindT) [(Term s a, Term s (li a))] -> Term s r
cps
      | Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n = [(Term s a, Term s (li a))] -> Term s r
cps [] -- >= is not correct, we want to compute one more for the "rest" part.
      | Integer
idx Integer -> [Integer] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [Integer]
usedFields =
          let
            isLastBind :: Bool
isLastBind = (Integer -> Bool) -> [Integer] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
idx) [Integer]
usedFields
            dropAmount :: Int
dropAmount = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
lastBindIdx
            dropToCurrent' :: forall s'. Term s' (li a) -> Term s' (li a)
            dropToCurrent' :: forall (s' :: S). Term s' (li a) -> Term s' (li a)
dropToCurrent' = ((Term s' (li a) -> Term s' (li a))
 -> (Term s' (li a) -> Term s' (li a))
 -> Term s' (li a)
 -> Term s' (li a))
-> (Term s' (li a) -> Term s' (li a))
-> [Term s' (li a) -> Term s' (li a)]
-> Term s' (li a)
-> Term s' (li a)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term s' (li a) -> Term s' (li a))
-> (Term s' (li a) -> Term s' (li a))
-> Term s' (li a)
-> Term s' (li a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Term s' (li a) -> Term s' (li a)
forall a. a -> a
id ([Term s' (li a) -> Term s' (li a)]
 -> Term s' (li a) -> Term s' (li a))
-> [Term s' (li a) -> Term s' (li a)]
-> Term s' (li a)
-> Term s' (li a)
forall a b. (a -> b) -> a -> b
$ Int
-> (Term s' (li a) -> Term s' (li a))
-> [Term s' (li a) -> Term s' (li a)]
forall a. Int -> a -> [a]
replicate Int
dropAmount (Term s' (li a :--> li a)
forall (a :: S -> Type) (s :: S).
PElemConstraint li a =>
Term s (li a :--> li a)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail #)

            -- If this is last term, or amount of @ptail@ we need is less than 3, we don't hoist.
            currentTerm :: Term s (li a)
currentTerm
              | Bool
isLastBind Bool -> Bool -> Bool
|| Int
dropAmount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
3 = Term s (li a) -> Term s (li a)
forall (s' :: S). Term s' (li a) -> Term s' (li a)
dropToCurrent' Term s (li a)
lastBindT
              | Bool
otherwise = ClosedTerm (li a :--> li a) -> Term s (li a :--> li a)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((Term s (li a) -> Term s (li a)) -> Term s (li a :--> li 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 (li a)) -> Term s (c :--> li a)
plam Term s (li a) -> Term s (li a)
forall (s' :: S). Term s' (li a) -> Term s' (li a)
dropToCurrent') Term s (li a :--> li a) -> Term s (li a) -> Term s (li a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (li a)
lastBindT

            bindIfNeeded :: Term s (li a) -> (Term s (li a) -> Term s r) -> Term s r
bindIfNeeded = if Bool
isLastBind then (\Term s (li a)
a Term s (li a) -> Term s r
h -> Term s (li a) -> Term s r
h Term s (li a)
a) else Term s (li a) -> (Term s (li a) -> Term s r) -> Term s r
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet
           in
            Term s (li a) -> (Term s (li a) -> Term s r) -> Term s r
bindIfNeeded Term s (li a)
currentTerm ((Term s (li a) -> Term s r) -> Term s r)
-> (Term s (li a) -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \Term s (li a)
newBind ->
              Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
forall (r :: S -> Type).
Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
mkMatches (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Term s (li a :--> li a)
forall (a :: S -> Type) (s :: S).
PElemConstraint li a =>
Term s (li a :--> li 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 (li a :--> li a) -> Term s (li a) -> Term s (li a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (li a)
running) (Integer
idx, Term s (li a)
newBind) (([(Term s a, Term s (li a))] -> Term s r) -> Term s r)
-> ([(Term s a, Term s (li a))] -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$ \[(Term s a, Term s (li a))]
rest ->
                [(Term s a, Term s (li a))] -> Term s r
cps ([(Term s a, Term s (li a))] -> Term s r)
-> [(Term s a, Term s (li a))] -> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s (li a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint li a =>
Term s (li 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 (li a :--> a) -> Term s (li 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 (li a)
newBind, Term s (li a)
newBind) (Term s a, Term s (li a))
-> [(Term s a, Term s (li a))] -> [(Term s a, Term s (li a))]
forall a. a -> [a] -> [a]
: [(Term s a, Term s (li a))]
rest
      | Bool
otherwise =
          Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
forall (r :: S -> Type).
Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
mkMatches (Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) (Term s (li a :--> li a)
forall (a :: S -> Type) (s :: S).
PElemConstraint li a =>
Term s (li a :--> li 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 (li a :--> li a) -> Term s (li a) -> Term s (li a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (li a)
running) (Integer, Term s (li a))
lastBind (([(Term s a, Term s (li a))] -> Term s r) -> Term s r)
-> ([(Term s a, Term s (li a))] -> Term s r) -> Term s r
forall a b. (a -> b) -> a -> b
$
            \[(Term s a, Term s (li a))]
rest ->
              [(Term s a, Term s (li a))] -> Term s r
cps ([(Term s a, Term s (li a))] -> Term s r)
-> [(Term s a, Term s (li a))] -> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s (li a :--> a)
forall (a :: S -> Type) (s :: S).
PElemConstraint li a =>
Term s (li 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 (li a :--> a) -> Term s (li 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 (li a)
running, Term s (li a)
running) (Term s a, Term s (li a))
-> [(Term s a, Term s (li a))] -> [(Term s a, Term s (li a))]
forall a. a -> [a] -> [a]
: [(Term s a, Term s (li a))]
rest

  Term s b -> TermCont @b s (Term s b)
forall a. a -> TermCont @b s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s b -> TermCont @b s (Term s b))
-> Term s b -> TermCont @b s (Term s b)
forall a b. (a -> b) -> a -> b
$ Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s b)
-> Term s b
forall (r :: S -> Type).
Integer
-> Term s (li a)
-> (Integer, Term s (li a))
-> ([(Term s a, Term s (li a))] -> Term s r)
-> Term s r
mkMatches Integer
0 Term s (li a)
xs (Integer
0, Term s (li a)
xs) (([Term s a] -> Term s (li a) -> Term s b)
-> ([Term s a], Term s (li a)) -> Term s b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Term s a] -> Term s (li a) -> Term s b
f (([Term s a], Term s (li a)) -> Term s b)
-> ([(Term s a, Term s (li a))] -> ([Term s a], Term s (li a)))
-> [(Term s a, Term s (li a))]
-> Term s b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Term s a] -> [Term s a])
-> ([Term s (li a)] -> Term s (li a))
-> ([Term s a], [Term s (li a)])
-> ([Term s a], Term s (li a))
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Int -> [Term s a] -> [Term s a]
forall a. Int -> [a] -> [a]
take (Int -> [Term s a] -> [Term s a])
-> Int -> [Term s a] -> [Term s a]
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) [Term s (li a)] -> Term s (li a)
forall a. HasCallStack => [a] -> a
last (([Term s a], [Term s (li a)]) -> ([Term s a], Term s (li a)))
-> ([(Term s a, Term s (li a))] -> ([Term s a], [Term s (li a)]))
-> [(Term s a, Term s (li a))]
-> ([Term s a], Term s (li a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Term s a, Term s (li a))] -> ([Term s a], [Term s (li a)])
forall a b. [(a, b)] -> ([a], [b])
unzip)

type family Length xs where
  Length '[] = 0
  Length (_ ': xs) = 1 + Length xs

type family Replicate n a where
  Replicate 0 _ = '[]
  Replicate x a = a ': Replicate (x - 1) a

-- This is very dangerous, be extra careful when using it
-- Essentially, this will construct NP of specified structure from the given list of term
-- There is no type assurances whatsoever and each term will be coerced.
class UnsafeConstrNP xs where
  constrNP :: forall a s. [Term s a] -> Maybe (NP (Term s) xs)

instance UnsafeConstrNP xs => UnsafeConstrNP (x ': xs) where
  constrNP :: forall (a :: S -> Type) (s :: S).
[Term s a]
-> Maybe (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs))
constrNP [] = Maybe (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs))
forall a. Maybe a
Nothing
  constrNP (Term s a
x : [Term s a]
xs) = do
    NP @(S -> Type) (Term s) xs
rest <- forall (xs :: [S -> Type]) (a :: S -> Type) (s :: S).
UnsafeConstrNP xs =>
[Term s a] -> Maybe (NP @(S -> Type) (Term s) xs)
constrNP @xs [Term s a]
xs
    NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs)
-> Maybe (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs))
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs)
 -> Maybe (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs)))
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs)
-> Maybe (NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs))
forall a b. (a -> b) -> a -> b
$ Term s a -> Term s x
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s a
x Term s x
-> NP @(S -> Type) (Term s) xs
-> NP @(S -> Type) (Term s) ((':) @(S -> Type) x xs)
forall {k} (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NP @k a xs -> NP @k a ((':) @k x xs)
:* NP @(S -> Type) (Term s) xs
rest

instance UnsafeConstrNP '[] where
  constrNP :: forall (a :: S -> Type) (s :: S).
[Term s a] -> Maybe (NP @(S -> Type) (Term s) ('[] @(S -> Type)))
constrNP [Term s a]
_ = NP @(S -> Type) (Term s) ('[] @(S -> Type))
-> Maybe (NP @(S -> Type) (Term s) ('[] @(S -> Type)))
forall a. a -> Maybe a
Just NP @(S -> Type) (Term s) ('[] @(S -> Type))
forall {k} (a :: k -> Type). NP @k a ('[] @k)
Nil