module Plutarch.Enum (
PCountable (..),
PEnumerable (..),
) where
import Data.Kind (Type)
import Plutarch.Builtin.Bool (pif)
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Internal.Eq ((#==))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.Numeric (PPositive, pone, (#+))
import Plutarch.Internal.Ord (POrd)
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.Term (
S,
Term,
phoistAcyclic,
(#),
(#$),
(:-->),
)
class POrd a => PCountable (a :: S -> Type) where
psuccessor :: forall (s :: S). Term s (a :--> a)
{-# INLINEABLE psuccessorN #-}
psuccessorN :: forall (s :: S). Term s (PPositive :--> a :--> a)
psuccessorN = (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a)))
-> (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
n Term s a
x -> Term s PPositive -> Term s (a :--> (PPositive :--> a))
forall (s' :: S).
Term s' PPositive -> Term s' (a :--> (PPositive :--> a))
go Term s PPositive
n Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
where
go ::
forall (s' :: S).
Term s' PPositive ->
Term s' (a :--> PPositive :--> a)
go :: forall (s' :: S).
Term s' PPositive -> Term s' (a :--> (PPositive :--> a))
go Term s' PPositive
limit = Term
s'
(((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
:--> (a :--> (PPositive :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s'
(((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
:--> (a :--> (PPositive :--> a)))
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (c :--> (a :--> (PPositive :--> a)))
plam ((Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a))))
-> (Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> (PPositive :--> a))
self Term s' a
acc Term s' PPositive
count ->
Term s' PBool -> Term s' a -> Term s' a -> Term s' a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s' PPositive
count Term s' PPositive -> Term s' PPositive -> Term s' PBool
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s' PPositive
limit)
Term s' a
acc
(Term s' (a :--> (PPositive :--> a))
self Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s' (a :--> a) -> Term s' a -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' a
acc) Term s' (PPositive :--> a) -> Term s' PPositive -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PPositive
count Term s' PPositive -> Term s' PPositive -> Term s' PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s' PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone))
instance PCountable PInteger where
{-# INLINEABLE psuccessor #-}
psuccessor :: forall (s :: S). Term s (PInteger :--> PInteger)
psuccessor = (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger))
-> (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> PInteger)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger) -> Term s (c :--> PInteger)
plam (Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
+ Term s PInteger
1)
{-# INLINEABLE psuccessorN #-}
psuccessorN :: forall (s :: S). Term s (PPositive :--> (PInteger :--> PInteger))
psuccessorN = (forall (s :: S). Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger)))
-> (forall (s :: S).
Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s PInteger)
-> Term s (c :--> (PInteger :--> PInteger))
plam ((Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger)))
-> (Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
p Term s PInteger
i -> Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
p Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
+ Term s PInteger
i
instance PCountable PPositive where
{-# INLINEABLE psuccessor #-}
psuccessor :: forall (s :: S). Term s (PPositive :--> PPositive)
psuccessor = (forall (s :: S). Term s (PPositive :--> PPositive))
-> Term s (PPositive :--> PPositive)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PPositive :--> PPositive))
-> Term s (PPositive :--> PPositive))
-> (forall (s :: S). Term s (PPositive :--> PPositive))
-> Term s (PPositive :--> PPositive)
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s PPositive)
-> Term s (PPositive :--> PPositive)
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 PPositive) -> Term s (c :--> PPositive)
plam (Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone)
{-# INLINEABLE psuccessorN #-}
psuccessorN :: forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
psuccessorN = (forall (s :: S).
Term s (PPositive :--> (PPositive :--> PPositive)))
-> Term s (PPositive :--> (PPositive :--> PPositive))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term s (PPositive :--> (PPositive :--> PPositive)))
-> Term s (PPositive :--> (PPositive :--> PPositive)))
-> (forall (s :: S).
Term s (PPositive :--> (PPositive :--> PPositive)))
-> Term s (PPositive :--> (PPositive :--> PPositive))
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s PPositive -> Term s PPositive)
-> Term s (PPositive :--> (PPositive :--> PPositive))
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 PPositive -> Term s PPositive)
-> Term s (c :--> (PPositive :--> PPositive))
plam Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)
class PCountable a => PEnumerable (a :: S -> Type) where
ppredecessor :: forall (s :: S). Term s (a :--> a)
{-# INLINEABLE ppredecessorN #-}
ppredecessorN :: forall (s :: S). Term s (PPositive :--> a :--> a)
ppredecessorN = (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a)))
-> (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
n Term s a
x -> Term s PPositive -> Term s (a :--> (PPositive :--> a))
forall (s' :: S).
Term s' PPositive -> Term s' (a :--> (PPositive :--> a))
go Term s PPositive
n Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
where
go ::
forall (s' :: S).
Term s' PPositive ->
Term s' (a :--> PPositive :--> a)
go :: forall (s' :: S).
Term s' PPositive -> Term s' (a :--> (PPositive :--> a))
go Term s' PPositive
limit = Term
s'
(((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
:--> (a :--> (PPositive :--> a)))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
s'
(((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
:--> (a :--> (PPositive :--> a)))
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s' c -> Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (c :--> (a :--> (PPositive :--> a)))
plam ((Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a))))
-> (Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' PPositive -> Term s' a)
-> Term
s' ((a :--> (PPositive :--> a)) :--> (a :--> (PPositive :--> a)))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> (PPositive :--> a))
self Term s' a
acc Term s' PPositive
count ->
Term s' PBool -> Term s' a -> Term s' a -> Term s' a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
(Term s' PPositive
count Term s' PPositive -> Term s' PPositive -> Term s' PBool
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s' PPositive
limit)
Term s' a
acc
(Term s' (a :--> (PPositive :--> a))
self Term s' (a :--> (PPositive :--> a))
-> Term s' a -> Term s' (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s' (a :--> a) -> Term s' a -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s' a
acc) Term s' (PPositive :--> a) -> Term s' PPositive -> Term s' a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s' PPositive
count Term s' PPositive -> Term s' PPositive -> Term s' PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s' PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone))
instance PEnumerable PInteger where
{-# INLINEABLE ppredecessor #-}
ppredecessor :: forall (s :: S). Term s (PInteger :--> PInteger)
ppredecessor = (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger))
-> (forall (s :: S). Term s (PInteger :--> PInteger))
-> Term s (PInteger :--> PInteger)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> PInteger)
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger) -> Term s (c :--> PInteger)
plam (Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
1)
{-# INLINEABLE ppredecessorN #-}
ppredecessorN :: forall (s :: S). Term s (PPositive :--> (PInteger :--> PInteger))
ppredecessorN = (forall (s :: S). Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall (a :: S -> Type) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger)))
-> (forall (s :: S).
Term s (PPositive :--> (PInteger :--> PInteger)))
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ (Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s PInteger)
-> Term s (c :--> (PInteger :--> PInteger))
plam ((Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger)))
-> (Term s PPositive -> Term s PInteger -> Term s PInteger)
-> Term s (PPositive :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
p Term s PInteger
i -> Term s PInteger
i Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s a -> Term s (PInner a)
pto Term s PPositive
p