{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

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

import Data.Functor.Const (Const)
import GHC.Generics (Generic)
import Plutarch.Builtin.Bool (PBool, pif, (#||))
import Plutarch.Builtin.ByteString (PByteString)
import Plutarch.Builtin.Data (
  PAsData,
  PBuiltinList,
  PBuiltinPair,
  PData,
  pasByteStr,
  pasConstr,
  pasInt,
  pasList,
  pfstBuiltin,
  ppairDataBuiltin,
  psndBuiltin,
 )
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 (PPositive, ptryPositive)
import Plutarch.Internal.PLam (PLamN (plam))
import Plutarch.Internal.PlutusType (PInner)
import Plutarch.Internal.Subtype (
  PSubtype,
  PSubtype',
  PSubtypeRelation (PNoSubtypeRelation, PSubtypeRelation),
  pdowncastF,
  pupcast,
  pupcastF,
 )
import Plutarch.Internal.Term (
  PType,
  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 :: PType) (b :: PType) where
  type PTryFromExcess a b :: PType
  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 :: PType) (a :: PType) (s :: S) (r :: PType).
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 :: PType) (a :: PType) (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 :: PType) (a :: PType) (s :: S) (r :: PType).
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 :: PType).
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
forall (a :: PType) (b :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom'

newtype Flip f a b = Flip (f b a) deriving stock ((forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x)
-> (forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b)
-> Generic (Flip @k @k f a b)
forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cfrom :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Flip @k @k f a b -> Rep (Flip @k @k f a b) x
from :: forall x. Flip @k @k f a b -> Rep (Flip @k @k f a b) x
$cto :: forall k k (f :: k -> k -> Type) (a :: k) (b :: k) x.
Rep (Flip @k @k f a b) x -> Flip @k @k f a b
to :: forall x. Rep (Flip @k @k f a b) x -> Flip @k @k f a b
Generic)

instance PTryFrom PData (PAsData PInteger) where
  type PTryFromExcess PData (PAsData PInteger) = Flip Term PInteger
  ptryFrom' :: forall (s :: S) (r :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 :: PType) (b :: PType).
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 :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (a :: PType) (s :: S) (r :: PType).
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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap 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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 @PType)) (PAsData (Any @PType)))
tup <- ((Term
    s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term
        s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term
         s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))))
-> ((Term
       s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term
        s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> (Term
      s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
    -> Term s r)
-> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term
  s
  (PAsData
     (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
   s
   (PAsData
      (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
 -> Term
      s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s
     (PAsData
        (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
forall a b. (a -> b) -> a -> b
$ Term s PData
-> Term
     s
     (PAsData
        (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))))
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s PData
opq)
    let fst' :: Term _ a
        fst' :: Term s a
fst' = TermCont @a s (Term s a) -> Term s a
forall (a :: PType) (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 :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
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 @PType)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (Any @PType)) -> Term s PData)
-> Term s (PAsData (Any @PType)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> Term s (PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup)
        snd' :: Term _ b
        snd' :: Term s b
snd' = TermCont @b s (Term s b) -> Term s b
forall (a :: PType) (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 :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
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 @PType)) -> Term s PData
forall (s :: S) (a :: PType). Term s (PAsData a) -> Term s PData
pforgetData (Term s (PAsData (Any @PType)) -> Term s PData)
-> Term s (PAsData (Any @PType)) -> Term s PData
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType))
   :--> PAsData (Any @PType))
-> Term
     s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
-> Term s (PAsData (Any @PType))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData (Any @PType)) (PAsData (Any @PType)))
tup)
    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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
Term s (PAsData b')
snd'
    (Term s (PAsData (PBuiltinPair (PAsData a') (PAsData b'))),
 Term s (PBuiltinPair (PAsData a') (PAsData b')))
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinPair (PAsData a') (PAsData 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 (PAsData a') (PAsData b')))
forall (b :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PData
opq
    let ix :: Term s PInteger
ix = Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term s (PBuiltinPair PInteger (PBuiltinList PData) :--> PInteger)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: PType).
((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 :: PType) (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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (b :: PType).
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 :: PType) (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 :: PType). Term s a
perror)
    let dat :: Term s (PBuiltinList PData)
dat = Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair PInteger (PBuiltinList PData)
   :--> PBuiltinList PData)
-> Term s (PBuiltinPair PInteger (PBuiltinList PData))
-> Term s (PBuiltinList PData)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair PInteger (PBuiltinList PData))
asConstr
    ((() -> Term s r) -> Term s r) -> TermCont @r s ()
forall a (s :: S) (r :: PType).
((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 :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s (PBuiltinList PData :--> PBool)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBool)
forall (list :: PType -> PType) (a :: PType) (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 :: PType) (b :: PType).
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 :: PType) (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 :: PType). 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 :: PType) (a :: PType) (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 :: PType).
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 :: PType) (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 :: PType) (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 :: PType).
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 WIP
instance PTryFrom PInteger PPositive where
  type PTryFromExcess PInteger PPositive = Const ()
  ptryFrom' :: forall (s :: S) (r :: PType).
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 :: PType) (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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
opq, ())

-- | @since WIP
instance PTryFrom PData (PAsData PPositive) where
  type PTryFromExcess PData (PAsData PPositive) = Flip Term PPositive
  ptryFrom' :: forall (s :: S) (r :: PType).
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 :: PType) (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 :: PType).
((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 :: PType) (a :: PType) (s :: S) (r :: PType).
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
    Term s PPositive
res <- ((Term s PPositive -> Term s r) -> Term s r)
-> TermCont @r s (Term s PPositive)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s PPositive -> Term s r) -> Term s r)
 -> TermCont @r s (Term s PPositive))
-> (Term s PPositive -> (Term s PPositive -> Term s r) -> Term s r)
-> Term s PPositive
-> TermCont @r s (Term s PPositive)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PPositive -> (Term s PPositive -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PPositive -> TermCont @r s (Term s PPositive))
-> Term s PPositive -> TermCont @r s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ 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 :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
i
    Term s (PAsData PPositive)
resData <- ((Term s (PAsData PPositive) -> Term s r) -> Term s r)
-> TermCont @r s (Term s (PAsData PPositive))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((Term s (PAsData PPositive) -> Term s r) -> Term s r)
 -> TermCont @r s (Term s (PAsData PPositive)))
-> (Term s (PAsData PPositive)
    -> (Term s (PAsData PPositive) -> Term s r) -> Term s r)
-> Term s (PAsData PPositive)
-> TermCont @r s (Term s (PAsData PPositive))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData PPositive)
-> (Term s (PAsData PPositive) -> Term s r) -> Term s r
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PAsData PPositive)
 -> TermCont @r s (Term s (PAsData PPositive)))
-> Term s (PAsData PPositive)
-> TermCont @r s (Term s (PAsData PPositive))
forall a b. (a -> b) -> a -> b
$ Term s PPositive -> Term s (PAsData PPositive)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PPositive
res
    (Term s (PAsData PPositive), Term s PPositive)
-> TermCont @r s (Term s (PAsData PPositive), Term s PPositive)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s (PAsData PPositive)
resData, Term s PPositive
res)