{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
-- Note (Koz, 14/11/2025): Needed for the PIsData constraints on the PBuiltinPair
-- instance.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Plutarch.Internal.TryFrom (
  PTryFrom,
  PTryFromExcess,
  ptryFrom',
  ptryFrom,
  PSubtypeRelation (PSubtypeRelation, PNoSubtypeRelation),
  PSubtype,
  PSubtype',
  pupcast,
) where

import Data.Functor.Const (Const)
import Data.Kind (Type)
import Plutarch.Builtin.Bool (PBool, pif, (#||))
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PBuiltinPair (PBuiltinPair),
  PData,
  pasByteStr,
  pasConstr,
  pasInt,
  pasList,
  ppairDataBuiltin,
 )
import Plutarch.Builtin.Integer (
  PInteger,
  pconstantInteger,
  peqInteger,
 )
import Plutarch.Builtin.String (ptraceInfo)
import Plutarch.Internal.IsData (
  PIsData,
  pdata,
  pforgetData,
  pfromData,
 )
import Plutarch.Internal.ListLike (PListLike (pnull), pmap)
import Plutarch.Internal.Numeric (PNatural, PPositive, ptryNatural, ptryPositive)
import Plutarch.Internal.Other (Flip)
import Plutarch.Internal.PLam (PLamN (plam))
import Plutarch.Internal.PlutusType (PInner, pmatch)
import Plutarch.Internal.Subtype (
  PSubtype,
  PSubtype',
  PSubtypeRelation (PNoSubtypeRelation, PSubtypeRelation),
  pupcast,
 )
import Plutarch.Internal.Term (
  S,
  Term,
  perror,
  plet,
  punsafeCoerce,
  (#),
  type (:-->),
 )
import Plutarch.Internal.TermCont (runTermCont, tcont, unTermCont)
import Plutarch.Reducible (Reduce)

{- |
@PTryFrom a b@ represents a subtyping relationship between @a@ and @b@,
and a way to go from @a@ to @b@.
Laws:
- @(punsafeCoerce . fst) <$> tcont (ptryFrom x) ≡ pure x@
-}
class PSubtype a b => PTryFrom (a :: S -> Type) (b :: S -> Type) where
  type PTryFromExcess a b :: S -> Type
  type PTryFromExcess a b = PTryFromExcess a (PInner b)
  ptryFrom' :: forall s r. Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
  default ptryFrom' :: forall s r. (PTryFrom a (PInner b), PTryFromExcess a b ~ PTryFromExcess a (PInner b)) => Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
  ptryFrom' Term s a
opq (Term s b, Reduce (PTryFromExcess a b s)) -> Term s r
f = forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PInner b) @a Term s a
opq \(Term s (PInner b)
inn, Reduce (PTryFromExcess a (PInner b) s)
exc) -> (Term s b, Reduce (PTryFromExcess a b s)) -> Term s r
f (Term s (PInner b) -> Term s b
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s (PInner b)
inn, Reduce (PTryFromExcess a b s)
Reduce (PTryFromExcess a (PInner b) s)
exc)

ptryFrom :: forall b a s r. PTryFrom a b => Term s a -> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r) -> Term s r
ptryFrom :: forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom = Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
forall (s :: S) (r :: S -> Type).
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
forall (a :: S -> Type) (b :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom'

instance PTryFrom PData (PAsData PInteger) where
  type PTryFromExcess PData (PAsData PInteger) = Flip Term PInteger
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PInteger),
   Reduce (PTryFromExcess PData (PAsData PInteger) s))
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PInteger),
    Reduce (PTryFromExcess PData (PAsData PInteger) s))
 -> ((Term s (PAsData PInteger),
      Reduce (PTryFromExcess PData (PAsData PInteger) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PInteger),
      Reduce (PTryFromExcess PData (PAsData PInteger) s))
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PInteger
ver <- ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PInteger -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PInteger))
-> ((Term s PInteger -> Term s r) -> Term s r)
-> TermCont @r s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> (Term s PInteger -> 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 (Term s (PData :--> PInteger)
forall (s :: S). Term s (PData :--> PInteger)
pasInt Term s (PData :--> PInteger) -> Term s PData -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData PInteger), Term s PInteger)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PInteger)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PInteger
ver)

instance PTryFrom PData (PAsData PByteString) where
  type PTryFromExcess PData (PAsData PByteString) = Flip Term PByteString
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PByteString),
   Reduce (PTryFromExcess PData (PAsData PByteString) s))
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PByteString),
    Reduce (PTryFromExcess PData (PAsData PByteString) s))
 -> ((Term s (PAsData PByteString),
      Reduce (PTryFromExcess PData (PAsData PByteString) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PByteString),
      Reduce (PTryFromExcess PData (PAsData PByteString) s))
-> ((Term s (PAsData PByteString),
     Reduce (PTryFromExcess PData (PAsData PByteString) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s PByteString
ver <- ((Term s PByteString -> Term s r) -> Term s r)
-> TermCont @r s (Term s PByteString)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PByteString -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PByteString))
-> ((Term s PByteString -> Term s r) -> Term s r)
-> TermCont @r s (Term s PByteString)
forall a b. (a -> b) -> a -> b
$ Term s PByteString -> (Term s PByteString -> 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 (Term s (PData :--> PByteString)
forall (s :: S). Term s (PData :--> PByteString)
pasByteStr Term s (PData :--> PByteString)
-> Term s PData -> Term s PByteString
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData PByteString), Term s PByteString)
-> TermCont @r s (Term s (PAsData PByteString), Term s PByteString)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PByteString)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PByteString
ver)

{- |
    This verifies a list to be indeed a list but doesn't recover the inner data
    use this instance instead of the one for `PData (PAsData (PBuiltinList (PAsData a)))`
    as this is O(1) instead of O(n)
-}

-- TODO: add the excess inner type list
instance PTryFrom PData (PAsData (PBuiltinList PData)) where
  type PTryFromExcess PData (PAsData (PBuiltinList PData)) = Flip Term (PBuiltinList PData)
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinList PData)),
   Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinList PData)),
    Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
 -> ((Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
-> ((Term s (PAsData (PBuiltinList PData)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinList PData)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinList PData)
ver <- ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList PData)))
-> ((Term s (PBuiltinList PData) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData)
-> (Term s (PBuiltinList PData) -> 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 (Term s (PData :--> PBuiltinList PData)
forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList Term s (PData :--> PBuiltinList PData)
-> Term s PData -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq)
    (Term s (PAsData (PBuiltinList PData)),
 Term s (PBuiltinList PData))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Term s (PBuiltinList PData))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PBuiltinList PData))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinList PData)
ver)

{- |
    Recover a `PBuiltinList (PAsData a)`
-}
instance
  ( PTryFrom PData (PAsData a)
  , PIsData a
  ) =>
  PTryFrom PData (PAsData (PBuiltinList (PAsData a)))
  where
  type PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) = Flip Term (PBuiltinList (PAsData a))
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinList (PAsData a))),
   Reduce
     (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinList (PAsData a))),
    Reduce
      (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
 -> ((Term s (PAsData (PBuiltinList (PAsData a))),
      Reduce
        (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList (PAsData a))),
      Reduce
        (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
-> ((Term s (PAsData (PBuiltinList (PAsData a))),
     Reduce
       (PTryFromExcess PData (PAsData (PBuiltinList (PAsData a))) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    let lst :: Term _ (PBuiltinList PData)
        lst :: Term s (PBuiltinList PData)
lst = Term s (PData :--> PBuiltinList PData)
forall (s :: S). Term s (PData :--> PBuiltinList PData)
pasList Term s (PData :--> PBuiltinList PData)
-> Term s PData -> Term s (PBuiltinList PData)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
        verify :: Term _ (PData :--> PAsData a)
        verify :: Term s (PData :--> PAsData a)
verify = (Term s PData -> Term s (PAsData a))
-> Term s (PData :--> PAsData 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 (PAsData a)) -> Term s (c :--> PAsData a)
plam ((Term s PData -> Term s (PAsData a))
 -> Term s (PData :--> PAsData a))
-> (Term s PData -> Term s (PAsData a))
-> Term s (PData :--> PAsData a)
forall a b. (a -> b) -> a -> b
$ \Term s PData
e ->
          TermCont @(PAsData a) s (Term s (PAsData a)) -> Term s (PAsData a)
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @(PAsData a) s (Term s (PAsData a))
 -> Term s (PAsData a))
-> TermCont @(PAsData a) s (Term s (PAsData a))
-> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ do
            (Term s (PAsData a)
wrapped, GReduce
  (PTryFromExcess PData (PAsData a) s)
  (Rep (PTryFromExcess PData (PAsData a) s))
_) <- (((Term s (PAsData a),
   GReduce
     (PTryFromExcess PData (PAsData a) s)
     (Rep (PTryFromExcess PData (PAsData a) s)))
  -> Term s (PAsData a))
 -> Term s (PAsData a))
-> TermCont
     @(PAsData a)
     s
     (Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData a),
    GReduce
      (PTryFromExcess PData (PAsData a) s)
      (Rep (PTryFromExcess PData (PAsData a) s)))
   -> Term s (PAsData a))
  -> Term s (PAsData a))
 -> TermCont
      @(PAsData a)
      s
      (Term s (PAsData a),
       GReduce
         (PTryFromExcess PData (PAsData a) s)
         (Rep (PTryFromExcess PData (PAsData a) s))))
-> (((Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
     -> Term s (PAsData a))
    -> Term s (PAsData a))
-> TermCont
     @(PAsData a)
     s
     (Term s (PAsData a),
      GReduce
        (PTryFromExcess PData (PAsData a) s)
        (Rep (PTryFromExcess PData (PAsData a) s)))
forall a b. (a -> b) -> a -> b
$ forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData a) (Term s PData
 -> ((Term s (PAsData a),
      Reduce (PTryFromExcess PData (PAsData a) s))
     -> Term s (PAsData a))
 -> Term s (PAsData a))
-> Term s PData
-> ((Term s (PAsData a),
     Reduce (PTryFromExcess PData (PAsData a) s))
    -> Term s (PAsData a))
-> Term s (PAsData a)
forall a b. (a -> b) -> a -> b
$ Term s PData
e
            Term s (PAsData a) -> TermCont @(PAsData a) s (Term s (PAsData a))
forall a. a -> TermCont @(PAsData a) s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Term s (PAsData a)
wrapped
    Term s (PBuiltinList (PAsData a))
ver <- ((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList (PAsData a)))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PBuiltinList (PAsData a))))
-> ((Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PBuiltinList (PAsData a)))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList (PAsData a))
-> (Term s (PBuiltinList (PAsData 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 (Term s (PBuiltinList (PAsData a))
 -> (Term s (PBuiltinList (PAsData a)) -> Term s r) -> Term s r)
-> Term s (PBuiltinList (PAsData a))
-> (Term s (PBuiltinList (PAsData a)) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term
  s
  ((PData :--> PAsData a)
   :--> (PBuiltinList PData :--> PBuiltinList (PAsData a)))
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (b :: S -> Type) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap Term
  s
  ((PData :--> PAsData a)
   :--> (PBuiltinList PData :--> PBuiltinList (PAsData a)))
-> Term s (PData :--> PAsData a)
-> Term s (PBuiltinList PData :--> PBuiltinList (PAsData a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PData :--> PAsData a)
forall {s :: S}. Term s (PData :--> PAsData a)
verify Term s (PBuiltinList PData :--> PBuiltinList (PAsData a))
-> Term s (PBuiltinList PData) -> Term s (PBuiltinList (PAsData a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
lst
    (Term s (PAsData (PBuiltinList (PAsData a))),
 Term s (PBuiltinList (PAsData a)))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList (PAsData a))),
      Term s (PBuiltinList (PAsData a)))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PBuiltinList (PAsData a)))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinList (PAsData a))
ver)

{- |
    Recover a `PAsData (PBuiltinPair a b)`
-}
instance
  ( PTryFrom PData a
  , a ~ PAsData a'
  , PIsData a'
  , PTryFrom PData b
  , b ~ PAsData b'
  , PIsData b'
  ) =>
  PTryFrom PData (PAsData (PBuiltinPair a b))
  where
  type PTryFromExcess PData (PAsData (PBuiltinPair a b)) = Flip Term (PBuiltinPair a b)
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData (PBuiltinPair a b)),
   Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData (PBuiltinPair a b)),
    Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
 -> ((Term s (PAsData (PBuiltinPair a b)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinPair a b)),
      Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
-> ((Term s (PAsData (PBuiltinPair a b)),
     Reduce (PTryFromExcess PData (PAsData (PBuiltinPair a b)) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term
  s
  (PBuiltinPair
     (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
tup <- ((Term
    s
    (PBuiltinPair
       (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term
        s
        (PBuiltinPair
           (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term
         s
         (PBuiltinPair
            (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))))
-> ((Term
       s
       (PBuiltinPair
          (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term
        s
        (PBuiltinPair
           (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair
     (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
-> (Term
      s
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
    -> 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 (Term
  s
  (PAsData
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
-> Term
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
   s
   (PAsData
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
 -> Term
      s
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
-> Term
     s
     (PAsData
        (PBuiltinPair
           (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
-> Term
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
forall a b. (a -> b) -> a -> b
$ Term s PData
-> Term
     s
     (PAsData
        (PBuiltinPair
           (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type)))))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq)
    PBuiltinPair Term s (PAsData (Any @(S -> Type)))
x Term s (PAsData (Any @(S -> Type)))
y <- ((PBuiltinPair
    (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PBuiltinPair
     (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s))
-> (Term
      s
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
    -> (PBuiltinPair
          (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s
        -> Term s r)
    -> Term s r)
-> Term
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
-> TermCont
     @r
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term
  s
  (PBuiltinPair
     (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
-> (PBuiltinPair
      (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) 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
   (PBuiltinPair
      (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
 -> TermCont
      @r
      s
      (PBuiltinPair
         (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s))
-> Term
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
-> TermCont
     @r
     s
     (PBuiltinPair
        (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))) s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair
     (PAsData (Any @(S -> Type))) (PAsData (Any @(S -> Type))))
tup
    let fst' :: Term s a
fst' = TermCont @a s (Term s a) -> Term s a
forall (a :: S -> Type) (s :: S).
TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @a s (Term s a) -> Term s a)
-> TermCont @a s (Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ (Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a
forall a b. (a, b) -> a
fst ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
-> TermCont @a s (Term s a, Reduce (PTryFromExcess PData a s))
-> TermCont @a s (Term s a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
 -> Term s a)
-> TermCont @a s (Term s a, Reduce (PTryFromExcess PData a s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @a (Term s PData
 -> ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
 -> Term s a)
-> Term s PData
-> ((Term s a, Reduce (PTryFromExcess PData a s)) -> Term s a)
-> Term s a
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (Any @(S -> Type))) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData (Any @(S -> Type)))
x)
    let snd' :: Term s b
snd' = 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
$ (Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b
forall a b. (a, b) -> a
fst ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
-> TermCont @b s (Term s b, Reduce (PTryFromExcess PData b s))
-> TermCont @b s (Term s b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
 -> Term s b)
-> TermCont @b s (Term s b, Reduce (PTryFromExcess PData b s))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @b (Term s PData
 -> ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
 -> Term s b)
-> Term s PData
-> ((Term s b, Reduce (PTryFromExcess PData b s)) -> Term s b)
-> Term s b
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (Any @(S -> Type))) -> Term s PData
forall (s :: S) (a :: S -> Type).
Term s (PAsData a) -> Term s PData
pforgetData Term s (PAsData (Any @(S -> Type)))
y)
    Term s (PBuiltinPair (PAsData a') (PAsData b'))
ver <- ((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
 -> Term s r)
-> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
  -> Term s r)
 -> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b'))))
-> ((Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
    -> Term s r)
-> TermCont @r s (Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData a') (PAsData b'))
-> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> 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 (Term s (PBuiltinPair (PAsData a') (PAsData b'))
 -> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
 -> Term s r)
-> Term s (PBuiltinPair (PAsData a') (PAsData b'))
-> (Term s (PBuiltinPair (PAsData a') (PAsData b')) -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PAsData a'
   :--> (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b')))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin Term
  s
  (PAsData a'
   :--> (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b')))
-> Term s (PAsData a')
-> Term s (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b'))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
Term s (PAsData a')
fst' Term s (PAsData b' :--> PBuiltinPair (PAsData a') (PAsData b'))
-> Term s (PAsData b')
-> Term s (PBuiltinPair (PAsData a') (PAsData b'))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
Term s (PAsData b')
snd'
    (Term s (PAsData (PBuiltinPair a b)),
 Term s (PBuiltinPair (PAsData a') (PAsData b')))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinPair a b)),
      Term s (PBuiltinPair (PAsData a') (PAsData b')))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData (PBuiltinPair a b))
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s (PBuiltinPair (PAsData a') (PAsData b'))
ver)

-- | @since 1.7.0
instance PTryFrom PData (PAsData PBool) where
  type PTryFromExcess PData (PAsData PBool) = Const ()
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PBool),
   Reduce (PTryFromExcess PData (PAsData PBool) s))
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PBool),
    Reduce (PTryFromExcess PData (PAsData PBool) s))
 -> ((Term s (PAsData PBool),
      Reduce (PTryFromExcess PData (PAsData PBool) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PBool),
      Reduce (PTryFromExcess PData (PAsData PBool) s))
-> ((Term s (PAsData PBool),
     Reduce (PTryFromExcess PData (PAsData PBool) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr <- ((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
 -> Term s r)
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PBuiltinPair PInteger (PBuiltinList PData)) -> Term s r)
  -> Term s r)
 -> TermCont
      @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
        -> Term s r)
    -> Term s r)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> 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 (Term s (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont
      @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData))))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont
     @r s (Term s (PBuiltinPair PInteger (PBuiltinList PData)))
forall a b. (a -> b) -> a -> b
$ Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S).
Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
pasConstr Term s (PData :--> PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PData
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    PBuiltinPair Term s PInteger
ix Term s (PBuiltinList PData)
dat <- ((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
 -> Term s r)
-> TermCont @r s (PBuiltinPair PInteger (PBuiltinList PData) s)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
  -> Term s r)
 -> TermCont @r s (PBuiltinPair PInteger (PBuiltinList PData) s))
-> (Term s (PBuiltinPair PInteger (PBuiltinList PData))
    -> (PBuiltinPair PInteger (PBuiltinList PData) s -> Term s r)
    -> Term s r)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont @r s (PBuiltinPair PInteger (PBuiltinList PData) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> (PBuiltinPair PInteger (PBuiltinList PData) 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 (PBuiltinPair PInteger (PBuiltinList PData))
 -> TermCont @r s (PBuiltinPair PInteger (PBuiltinList PData) s))
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> TermCont @r s (PBuiltinPair PInteger (PBuiltinList PData) s)
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((() -> Term s r) -> Term s r) -> TermCont @r s ())
-> ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a b. (a -> b) -> a -> b
$ \() -> Term s r
f ->
      Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        ((Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PBool))
peqInteger Term s (PInteger :--> (PInteger :--> PBool))
-> Term s PInteger -> Term s (PInteger :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
ix Term s (PInteger :--> PBool) -> Term s PInteger -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
0) Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| (Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PBool))
peqInteger Term s (PInteger :--> (PInteger :--> PBool))
-> Term s PInteger -> Term s (PInteger :--> PBool)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
ix Term s (PInteger :--> PBool) -> Term s PInteger -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Integer -> Term s PInteger
forall (s :: S). Integer -> Term s PInteger
pconstantInteger Integer
1))
        (() -> Term s r
f ())
        (Term s PString -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"PTryFrom(PAsData PBool): invalid constructor tag" Term s r
forall (s :: S) (a :: S -> Type). Term s a
perror)
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((() -> Term s r) -> Term s r) -> TermCont @r s ())
-> ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a b. (a -> b) -> a -> b
$ \() -> Term s r
f ->
      Term s PBool -> Term s r -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PBuiltinList PData :--> PBool)
forall (a :: S -> Type) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBool)
forall (list :: (S -> Type) -> S -> Type) (a :: S -> Type)
       (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> PBool)
pnull Term s (PBuiltinList PData :--> PBool)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
dat)
        (() -> Term s r
f ())
        (Term s PString -> Term s r -> Term s r
forall (a :: S -> Type) (s :: S).
Term s PString -> Term s a -> Term s a
ptraceInfo Term s PString
"PTryFrom(PAsData PBool): non-empty constructor list" Term s r
forall (s :: S) (a :: S -> Type). Term s a
perror)
    (Term s (PAsData PBool), ())
-> TermCont @r s (Term s (PAsData PBool), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PBool)
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PData
opq, ())

instance PTryFrom PData (PAsData PData) where
  type PTryFromExcess PData (PAsData PData) = Const ()
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PData),
   Reduce (PTryFromExcess PData (PAsData PData) s))
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PData),
    Reduce (PTryFromExcess PData (PAsData PData) s))
 -> ((Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
-> ((Term s (PAsData PData),
     Reduce (PTryFromExcess PData (PAsData PData) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData PData),
 Reduce (PTryFromExcess PData (PAsData PData) s))
-> TermCont
     @r
     s
     (Term s (PAsData PData),
      Reduce (PTryFromExcess PData (PAsData PData) s))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PData)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PData
opq, ())

instance PTryFrom PData PData where
  type PTryFromExcess PData PData = Const ()
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s PData, Reduce (PTryFromExcess PData PData s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq (Term s PData, Reduce (PTryFromExcess PData PData s)) -> Term s r
f = (Term s PData, Reduce (PTryFromExcess PData PData s)) -> Term s r
f (Term s PData
opq, ())

-- | @since 1.10.0
instance PTryFrom PInteger PPositive where
  type PTryFromExcess PInteger PPositive = Const ()
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PInteger
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PInteger
opq = TermCont
  @r
  s
  (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
 -> ((Term s PPositive,
      Reduce (PTryFromExcess PInteger PPositive s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> ((Term s PPositive,
     Reduce (PTryFromExcess PInteger PPositive s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
-> TermCont
     @r
     s
     (Term s PPositive, Reduce (PTryFromExcess PInteger PPositive s))
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PInteger :--> PPositive)
forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive Term s (PInteger :--> PPositive)
-> Term s PInteger -> Term s PPositive
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
opq, ())

-- | @since 1.10.0
instance PTryFrom PData (PAsData PPositive) where
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PPositive),
   Reduce (PTryFromExcess PData (PAsData PPositive) s))
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PPositive),
    Reduce (PTryFromExcess PData (PAsData PPositive) s))
 -> ((Term s (PAsData PPositive),
      Reduce (PTryFromExcess PData (PAsData PPositive) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PPositive),
      Reduce (PTryFromExcess PData (PAsData PPositive) s))
-> ((Term s (PAsData PPositive),
     Reduce (PTryFromExcess PData (PAsData PPositive) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData PInteger)
_, Term s PInteger
i) <- (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
 -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
  -> Term s r)
 -> TermCont @r s (Term s (PAsData PInteger), Term s PInteger))
-> (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
    -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a b. (a -> b) -> a -> b
$ forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PInteger) Term s PData
opq
    let res :: Term s PPositive
res = Term s (PInteger :--> PPositive)
forall (s :: S). Term s (PInteger :--> PPositive)
ptryPositive Term s (PInteger :--> PPositive)
-> Term s PInteger -> Term s PPositive
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 (PAsData PPositive), ())
-> TermCont @r s (Term s (PAsData PPositive), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PPositive -> Term s (PAsData PPositive)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PPositive
res, ())

-- | @since 3.4.0
instance PTryFrom PData (PAsData PNatural) where
  ptryFrom' :: forall (s :: S) (r :: S -> Type).
Term s PData
-> ((Term s (PAsData PNatural),
     Reduce (PTryFromExcess PData (PAsData PNatural) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PNatural),
   Reduce (PTryFromExcess PData (PAsData PNatural) s))
-> ((Term s (PAsData PNatural),
     Reduce (PTryFromExcess PData (PAsData PNatural) s))
    -> Term s r)
-> Term s r
forall (r :: S -> Type) (s :: S) a.
TermCont @r s a -> (a -> Term s r) -> Term s r
runTermCont (TermCont
   @r
   s
   (Term s (PAsData PNatural),
    Reduce (PTryFromExcess PData (PAsData PNatural) s))
 -> ((Term s (PAsData PNatural),
      Reduce (PTryFromExcess PData (PAsData PNatural) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PNatural),
      Reduce (PTryFromExcess PData (PAsData PNatural) s))
-> ((Term s (PAsData PNatural),
     Reduce (PTryFromExcess PData (PAsData PNatural) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData PInteger)
_, Term s PInteger
i) <- (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
 -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a (s :: S) (r :: S -> Type).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
  -> Term s r)
 -> TermCont @r s (Term s (PAsData PInteger), Term s PInteger))
-> (((Term s (PAsData PInteger), Term s PInteger) -> Term s r)
    -> Term s r)
-> TermCont @r s (Term s (PAsData PInteger), Term s PInteger)
forall a b. (a -> b) -> a -> b
$ forall (b :: S -> Type) (a :: S -> Type) (s :: S) (r :: S -> Type).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PInteger) Term s PData
opq
    let res :: Term s PNatural
res = Term s (PInteger :--> PNatural)
forall (s :: S). Term s (PInteger :--> PNatural)
ptryNatural Term s (PInteger :--> PNatural)
-> Term s PInteger -> Term s PNatural
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 (PAsData PNatural), ())
-> TermCont @r s (Term s (PAsData PNatural), ())
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PNatural -> Term s (PAsData PNatural)
forall (a :: S -> Type) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PNatural
res, ())