{-# 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)
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)
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)
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)
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)
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, ())
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, ())
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)