module Plutarch.Enum (
  -- * Type classes
  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.PLam (plam)
import Plutarch.Internal.Subtype (pupcast)
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  (#),
  (:-->),
 )

{- | A notion of \'next\' value. More formally, instances of this type class are
discrete linear orders with no maximal element.

= Laws

1. @x /= psuccessor x@
2. @y < x@ @=@ @psuccessor y <= x@
3. @x < psuccessor y@ @=@ @x <= y@

If you define 'psuccessorN', you must also ensure the following hold; the
default implementation ensures this.

4. @psuccessorN 1@ @=@ @psuccessor@
5. @psuccessorN n . psuccessorN m@ @=@ @psuccessorN (n + m)@

Law 1 ensures no value is its own successor. Laws 2 and 3 ensure that there
are no \'gaps\': every value is \'reachable\' from any lower value by a
finite number of applications of 'successor'.

@since 1.10.0
-}
class POrd a => PCountable (a :: S -> Type) where
  -- | @since 1.10.0
  psuccessor :: forall (s :: S). Term s (a :--> a)

  {- | The default implementation of this function is inefficient: if at all
  possible, give instances an optimized version that doesn't require
  recursion.

  @since 1.10.0
  -}
  {-# 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 =>
(forall (s' :: S). Term s' 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))
 -> Term s' (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s' (a :--> (PPositive :--> a))
  -> Term s' (a :--> (PPositive :--> a)))
 -> Term s' (a :--> (PPositive :--> a)))
-> (Term s' (a :--> (PPositive :--> a))
    -> Term s' (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> (PPositive :--> a))
self -> (Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (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' PPositive -> Term s' a)
-> Term s' (c :--> (PPositive :--> a))
plam ((Term s' a -> Term s' PPositive -> Term s' a)
 -> Term s' (a :--> (PPositive :--> a)))
-> (Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \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))

-- | @since 1.10.0
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 =>
(forall (s' :: S). Term s' 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 =>
(forall (s' :: S). Term s' 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' PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s' PPositive
p Term s' PInteger -> Term s' PInteger -> Term s' PInteger
forall a. Num a => a -> a -> a
+ Term s' PInteger
i

-- | @since 1.10.0
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 =>
(forall (s' :: S). Term s' 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 =>
(forall (s' :: S). Term s' 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
(#+)

{- | Similar to 'PCountable', but has the ability to get a \'previous\' value as
well. More formally, instances of this type class are discrete linear orders
with no maximal or minimal element.

= Laws

1. @ppredecessor . psuccessor@ @=@ @psuccessor . ppredecessor@ @=@ @id@

If you define 'ppredecessorN', you must also ensure the following hold; the
default implementation ensures this.

2. @ppredecessorN 1@ @=@ @ppredecessor@
3. @ppredecessorN n . ppredecessorN m@ @=@ @ppredecessorN (n + m)@

From Law 1, we obtain the following theorem:

* @x /= predecessor x@

@since 1.10.0
-}
class PCountable a => PEnumerable (a :: S -> Type) where
  -- | @since 1.10.0
  ppredecessor :: forall (s :: S). Term s (a :--> a)

  {- | The default implementation of this function is inefficient: if at all
  possible, give instances an optimized version that doesn't require
  recursion.

  @since 1.10.0
  -}
  {-# 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 =>
(forall (s' :: S). Term s' 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))
 -> Term s' (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s' (a :--> (PPositive :--> a))
  -> Term s' (a :--> (PPositive :--> a)))
 -> Term s' (a :--> (PPositive :--> a)))
-> (Term s' (a :--> (PPositive :--> a))
    -> Term s' (a :--> (PPositive :--> a)))
-> Term s' (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s' (a :--> (PPositive :--> a))
self -> (Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (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' PPositive -> Term s' a)
-> Term s' (c :--> (PPositive :--> a))
plam ((Term s' a -> Term s' PPositive -> Term s' a)
 -> Term s' (a :--> (PPositive :--> a)))
-> (Term s' a -> Term s' PPositive -> Term s' a)
-> Term s' (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \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))

-- | @since 1.10.0
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 =>
(forall (s' :: S). Term s' 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 =>
(forall (s' :: S). Term s' 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' PInteger
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
PSubtype a b =>
Term s b -> Term s a
pupcast Term s' PPositive
p