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

module Plutarch.Rational (
  PRational (PRational),
  preduce,
  pnumerator,
  pdenominator,
  Plutarch.Rational.pfromInteger,
  pround,
  ptruncate,
  pproperFraction,
) where

import GHC.Generics (Generic)
import Generics.SOP qualified as SOP
import Plutarch.Builtin.Bool (PBool, pcond, pif)
import Plutarch.Builtin.Data (PAsData, PBuiltinList, PData, ppairDataBuiltin)
import Plutarch.Builtin.Integer (PInteger)
import Plutarch.Internal.Eq (PEq ((#==)))
import Plutarch.Internal.Fix (pfix)
import Plutarch.Internal.IsData (pdata)
import Plutarch.Internal.Lift (
  PLiftable (
    AsHaskell,
    PlutusRepr,
    fromPlutarch,
    fromPlutarchRepr,
    toPlutarch,
    toPlutarchRepr
  ),
  PLiftedClosed,
  fromPlutarchReprClosed,
  getPLifted,
  mkPLifted,
  pconstant,
  toPlutarchReprClosed,
 )
import Plutarch.Internal.ListLike (phead, pnil, ptail)
import Plutarch.Internal.Numeric (
  PAdditiveGroup (pnegate, pscaleInteger, (#-)),
  PAdditiveMonoid (pzero),
  PAdditiveSemigroup (pscalePositive, (#+)),
  PIntegralDomain (pabs, psignum),
  PMultiplicativeMonoid (pone),
  PMultiplicativeSemigroup (ppowPositive, (#*)),
  PPositive,
  PRing (pfromInteger),
  pdiv,
  pmod,
  pquot,
  ptryPositive,
 )
import Plutarch.Internal.Ord (
  POrd ((#<), (#<=)),
 )
import Plutarch.Internal.Other (pto)
import Plutarch.Internal.PLam (plam)
import Plutarch.Internal.PlutusType (PlutusType, pcon, pmatch)
import Plutarch.Internal.Show (PShow, pshow, pshow')
import Plutarch.Internal.Term (
  S,
  Term,
  phoistAcyclic,
  plet,
  punsafeBuiltin,
  (#),
  (#$),
  (:-->),
 )
import Plutarch.Internal.TermCont (
  runTermCont,
  tcont,
  unTermCont,
 )
import Plutarch.Internal.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'), ptryFrom)
import Plutarch.Pair (PPair (PPair))
import Plutarch.Repr.SOP (DeriveAsSOPRec (DeriveAsSOPRec))
import Plutarch.Trace (ptraceInfoError)
import Plutarch.Unsafe (punsafeCoerce, punsafeDowncast)
import PlutusCore qualified as PLC
import PlutusTx.Ratio qualified as PlutusTx

{- | A Scott-encoded rational number, with a guaranteed positive denominator
(and thus, a canonical form).

= Note

This is not the Plutarch equivalent of a Plutus @Rational@; for this, you
want @PRationalData@ from @plutarch-ledger-api@. 'PRational' is designed to
optimize for computation: if you want to do any serious work with rational
numbers that isn't just passing them around, you want to use (or convert to)
'PRational'.
-}
data PRational s
  = PRational (Term s PInteger) (Term s PPositive)
  deriving stock ((forall x. PRational s -> Rep (PRational s) x)
-> (forall x. Rep (PRational s) x -> PRational s)
-> Generic (PRational s)
forall x. Rep (PRational s) x -> PRational s
forall x. PRational s -> Rep (PRational s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PRational s) x -> PRational s
forall (s :: S) x. PRational s -> Rep (PRational s) x
$cfrom :: forall (s :: S) x. PRational s -> Rep (PRational s) x
from :: forall x. PRational s -> Rep (PRational s) x
$cto :: forall (s :: S) x. Rep (PRational s) x -> PRational s
to :: forall x. Rep (PRational s) x -> PRational s
Generic)
  deriving anyclass (All @[Type] (SListI @Type) (Code (PRational s))
All @[Type] (SListI @Type) (Code (PRational s)) =>
(PRational s -> Rep (PRational s))
-> (Rep (PRational s) -> PRational s) -> Generic (PRational s)
Rep (PRational s) -> PRational s
PRational s -> Rep (PRational s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (s :: S). All @[Type] (SListI @Type) (Code (PRational s))
forall (s :: S). Rep (PRational s) -> PRational s
forall (s :: S). PRational s -> Rep (PRational s)
$cfrom :: forall (s :: S). PRational s -> Rep (PRational s)
from :: PRational s -> Rep (PRational s)
$cto :: forall (s :: S). Rep (PRational s) -> PRational s
to :: Rep (PRational s) -> PRational s
SOP.Generic)

deriving via (DeriveAsSOPRec PRational) instance PlutusType PRational

-- | @since WIP
instance PLiftable PRational where
  type AsHaskell PRational = PlutusTx.Rational
  type PlutusRepr PRational = PLiftedClosed PRational
  {-# INLINEABLE toPlutarchRepr #-}
  toPlutarchRepr :: AsHaskell PRational -> PlutusRepr PRational
toPlutarchRepr = AsHaskell PRational -> PlutusRepr PRational
forall (a :: PType).
(PLiftable a,
 (PlutusRepr a :: Type) ~ (PLiftedClosed a :: Type)) =>
AsHaskell a -> PlutusRepr a
toPlutarchReprClosed
  {-# INLINEABLE toPlutarch #-}
  toPlutarch :: forall (s :: S). AsHaskell PRational -> PLifted s PRational
toPlutarch AsHaskell PRational
r =
    let n :: Integer
n = Rational -> Integer
PlutusTx.numerator Rational
AsHaskell PRational
r
        d :: Integer
d = Rational -> Integer
PlutusTx.denominator Rational
AsHaskell PRational
r
     in Term s PRational -> PLifted s PRational
forall (s :: S) (a :: PType). Term s a -> PLifted s a
mkPLifted (Term s PRational -> PLifted s PRational)
-> (PRational s -> Term s PRational)
-> PRational s
-> PLifted s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> PLifted s PRational)
-> PRational s -> PLifted s PRational
forall a b. (a -> b) -> a -> b
$
          if
            | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 -> Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone
            | Integer
d Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (AsHaskell PInteger -> Term s PInteger)
-> (AsHaskell PInteger -> AsHaskell PInteger)
-> AsHaskell PInteger
-> Term s PInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsHaskell PInteger -> AsHaskell PInteger
forall a. Num a => a -> a
negate (AsHaskell PInteger -> Term s PInteger)
-> AsHaskell PInteger -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ Integer
AsHaskell PInteger
n) (Term s PPositive -> PRational s)
-> (AsHaskell PInteger -> Term s PPositive)
-> AsHaskell PInteger
-> PRational s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> (AsHaskell PInteger -> Term s PInteger)
-> AsHaskell PInteger
-> Term s PPositive
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PInteger (AsHaskell PInteger -> Term s PInteger)
-> (AsHaskell PInteger -> AsHaskell PInteger)
-> AsHaskell PInteger
-> Term s PInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AsHaskell PInteger -> AsHaskell PInteger
forall a. Num a => a -> a
negate (AsHaskell PInteger -> PRational s)
-> AsHaskell PInteger -> PRational s
forall a b. (a -> b) -> a -> b
$ Integer
AsHaskell PInteger
d
            | Bool
otherwise -> Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Integer
AsHaskell PInteger
n) (Term s PPositive -> PRational s)
-> (AsHaskell PInteger -> Term s PPositive)
-> AsHaskell PInteger
-> PRational s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> (AsHaskell PInteger -> Term s PInteger)
-> AsHaskell PInteger
-> Term s PPositive
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @PInteger (AsHaskell PInteger -> PRational s)
-> AsHaskell PInteger -> PRational s
forall a b. (a -> b) -> a -> b
$ Integer
AsHaskell PInteger
d
  {-# INLINEABLE fromPlutarchRepr #-}
  fromPlutarchRepr :: PlutusRepr PRational -> Maybe (AsHaskell PRational)
fromPlutarchRepr = PlutusRepr PRational -> Maybe (AsHaskell PRational)
forall (a :: PType).
(PLiftable a,
 (PlutusRepr a :: Type) ~ (PLiftedClosed a :: Type)) =>
PlutusRepr a -> Maybe (AsHaskell a)
fromPlutarchReprClosed
  {-# INLINEABLE fromPlutarch #-}
  fromPlutarch :: (forall (s :: S). PLifted s PRational)
-> Either LiftError (AsHaskell PRational)
fromPlutarch forall (s :: S). PLifted s PRational
t = do
    (Integer
n, Integer
d) <- (forall (s :: S).
 PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> Either
     LiftError
     (AsHaskell (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
forall (a :: PType).
PLiftable a =>
(forall (s :: S). PLifted s a) -> Either LiftError (AsHaskell a)
fromPlutarch ((forall (s :: S).
  PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
 -> Either
      LiftError
      (AsHaskell (PBuiltinPair (PAsData PInteger) (PAsData PInteger))))
-> (forall (s :: S).
    PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> Either
     LiftError
     (AsHaskell (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
-> PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
forall (s :: S) (a :: PType). Term s a -> PLifted s a
mkPLifted (Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
 -> PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
-> PLifted s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s
    -> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (PLifted s PRational -> Term s PRational
forall (s :: S) (a :: PType). PLifted s a -> Term s a
getPLifted PLifted s PRational
forall (s :: S). PLifted s PRational
t) ((PRational s
  -> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
 -> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> (PRational s
    -> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger)))
-> Term s (PBuiltinPair (PAsData PInteger) (PAsData PInteger))
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
n' Term s PPositive
d') ->
      Term
  s
  (PAsData PInteger
   :--> (PAsData (PInner PPositive)
         :--> PBuiltinPair (PAsData PInteger) (PAsData (PInner PPositive))))
forall (s :: S) (a :: PType) (b :: PType).
Term
  s
  (PAsData a
   :--> (PAsData b :--> PBuiltinPair (PAsData a) (PAsData b)))
ppairDataBuiltin Term
  s
  (PAsData PInteger
   :--> (PAsData (PInner PPositive)
         :--> PBuiltinPair (PAsData PInteger) (PAsData (PInner PPositive))))
-> Term s (PAsData PInteger)
-> Term
     s
     (PAsData (PInner PPositive)
      :--> PBuiltinPair (PAsData PInteger) (PAsData (PInner PPositive)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger -> Term s (PAsData PInteger)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PInteger
n' Term
  s
  (PAsData (PInner PPositive)
   :--> PBuiltinPair (PAsData PInteger) (PAsData (PInner PPositive)))
-> Term s (PAsData (PInner PPositive))
-> Term
     s (PBuiltinPair (PAsData PInteger) (PAsData (PInner PPositive)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInner PPositive) -> Term s (PAsData (PInner PPositive))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
d')
    Rational -> Either LiftError Rational
forall a. a -> Either LiftError a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rational -> Either LiftError Rational)
-> (Integer -> Rational) -> Integer -> Either LiftError Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Rational
PlutusTx.unsafeRatio Integer
n (Integer -> Either LiftError Rational)
-> Integer -> Either LiftError Rational
forall a b. (a -> b) -> a -> b
$ Integer
d

instance PEq PRational where
  {-# INLINEABLE (#==) #-}
  Term s PRational
l' #== :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PBool
#== Term s PRational
r' = Term s (PRational :--> (PRational :--> PBool))
forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l' Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r'
    where
      inner :: forall (s :: S). Term s (PRational :--> PRational :--> PBool)
      inner :: forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner = (forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (forall (s :: S).
    Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
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 PRational -> Term s PBool)
-> Term s (c :--> (PRational :--> PBool))
plam ((Term s PRational -> Term s PRational -> Term s PBool)
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
l Term s PRational
r ->
        Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
forall (s :: S).
Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
cmpHelper Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
-> Term s (PInteger :--> (PInteger :--> PBool))
-> Term s (PRational :--> (PRational :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# DefaultFun -> Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.EqualsInteger Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r

instance POrd PRational where
  {-# INLINEABLE (#<=) #-}
  Term s PRational
l' #<= :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PBool
#<= Term s PRational
r' = Term s (PRational :--> (PRational :--> PBool))
forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l' Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r'
    where
      inner :: forall (s :: S). Term s (PRational :--> PRational :--> PBool)
      inner :: forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner = (forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (forall (s :: S).
    Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
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 PRational -> Term s PBool)
-> Term s (c :--> (PRational :--> PBool))
plam ((Term s PRational -> Term s PRational -> Term s PBool)
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
l Term s PRational
r ->
        Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
forall (s :: S).
Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
cmpHelper Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
-> Term s (PInteger :--> (PInteger :--> PBool))
-> Term s (PRational :--> (PRational :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# DefaultFun -> Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanEqualsInteger Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r
  {-# INLINEABLE (#<) #-}
  Term s PRational
l' #< :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PBool
#< Term s PRational
r' = Term s (PRational :--> (PRational :--> PBool))
forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l' Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r'
    where
      inner :: forall (s :: S). Term s (PRational :--> PRational :--> PBool)
      inner :: forall (s :: S). Term s (PRational :--> (PRational :--> PBool))
inner = (forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> (PRational :--> PBool)))
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (forall (s :: S).
    Term s (PRational :--> (PRational :--> PBool)))
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
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 PRational -> Term s PBool)
-> Term s (c :--> (PRational :--> PBool))
plam ((Term s PRational -> Term s PRational -> Term s PBool)
 -> Term s (PRational :--> (PRational :--> PBool)))
-> (Term s PRational -> Term s PRational -> Term s PBool)
-> Term s (PRational :--> (PRational :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
l Term s PRational
r ->
        Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
forall (s :: S).
Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
cmpHelper Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
-> Term s (PInteger :--> (PInteger :--> PBool))
-> Term s (PRational :--> (PRational :--> PBool))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# DefaultFun -> Term s (PInteger :--> (PInteger :--> PBool))
forall (s :: S) (a :: PType). DefaultFun -> Term s a
punsafeBuiltin DefaultFun
PLC.LessThanInteger Term s (PRational :--> (PRational :--> PBool))
-> Term s PRational -> Term s (PRational :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
l Term s (PRational :--> PBool) -> Term s PRational -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
r

-- | @since WIP
instance PAdditiveSemigroup PRational where
  {-# INLINEABLE (#+) #-}
  Term s PRational
x' #+ :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PRational
#+ Term s PRational
y' =
    ClosedTerm (PRational :--> (PRational :--> PRational))
-> Term s (PRational :--> (PRational :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
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 PRational -> Term s PRational)
-> Term s (c :--> (PRational :--> PRational))
plam ((Term s PRational -> Term s PRational -> Term s PRational)
 -> Term s (PRational :--> (PRational :--> PRational)))
-> (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PRational
y -> TermCont @PRational s (Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PRational s (Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ do
          PRational Term s PInteger
xn Term s PPositive
xd' <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x
          PRational Term s PInteger
yn Term s PPositive
yd' <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
y
          Term s PPositive
xd <- ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational 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 PRational) -> Term s PRational)
 -> TermCont @PRational s (Term s PPositive))
-> ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PPositive
-> (Term s PPositive -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
xd'
          Term s PPositive
yd <- ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational 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 PRational) -> Term s PRational)
 -> TermCont @PRational s (Term s PPositive))
-> ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PPositive
-> (Term s PPositive -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
yd'
          Term s PRational -> TermCont @PRational s (Term s PRational)
forall a. a -> TermCont @PRational s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PRational -> TermCont @PRational s (Term s PRational))
-> Term s PRational -> TermCont @PRational s (Term s PRational)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
yd Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
+ Term s PInteger
yn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s PPositive
xd Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive
yd)
      )
      # x'
      # y'
  {-# INLINEABLE pscalePositive #-}
  pscalePositive :: forall (s :: S). Term s (PRational :--> (PPositive :--> PRational))
pscalePositive = (forall (s :: S).
 Term s (PRational :--> (PPositive :--> PRational)))
-> Term s (PRational :--> (PPositive :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PRational :--> (PPositive :--> PRational)))
 -> Term s (PRational :--> (PPositive :--> PRational)))
-> (forall (s :: S).
    Term s (PRational :--> (PPositive :--> PRational)))
-> Term s (PRational :--> (PPositive :--> PRational))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PPositive -> Term s PRational)
-> Term s (PRational :--> (PPositive :--> PRational))
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 PPositive -> Term s PRational)
-> Term s (c :--> (PPositive :--> PRational))
plam ((Term s PRational -> Term s PPositive -> Term s PRational)
 -> Term s (PRational :--> (PPositive :--> PRational)))
-> (Term s PRational -> Term s PPositive -> Term s PRational)
-> Term s (PRational :--> (PPositive :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PPositive
p ->
    Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
      Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
p) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd

-- | @since WIP
instance PAdditiveMonoid PRational where
  {-# INLINEABLE pzero #-}
  pzero :: forall (s :: S). Term s PRational
pzero = PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> (Term s PPositive -> PRational s)
-> Term s PPositive
-> Term s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero (Term s PPositive -> Term s PRational)
-> Term s PPositive -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone

-- | @since WIP
instance PAdditiveGroup PRational where
  {-# INLINEABLE pnegate #-}
  pnegate :: forall (s :: S). Term s (PRational :--> PRational)
pnegate =
    (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PRational))
 -> Term s (PRational :--> PRational))
-> (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$
      (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRational -> Term s PRational)
 -> Term s (PRational :--> PRational))
-> (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
        Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
          PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
xn) Term s PPositive
xd
  {-# INLINEABLE (#-) #-}
  Term s PRational
x' #- :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PRational
#- Term s PRational
y' =
    ClosedTerm (PRational :--> (PRational :--> PRational))
-> Term s (PRational :--> (PRational :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
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 PRational -> Term s PRational)
-> Term s (c :--> (PRational :--> PRational))
plam ((Term s PRational -> Term s PRational -> Term s PRational)
 -> Term s (PRational :--> (PRational :--> PRational)))
-> (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PRational
y -> TermCont @PRational s (Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PRational s (Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ do
          PRational Term s PInteger
xn Term s PPositive
xd' <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x
          PRational Term s PInteger
yn Term s PPositive
yd' <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
y
          Term s PPositive
xd <- ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational 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 PRational) -> Term s PRational)
 -> TermCont @PRational s (Term s PPositive))
-> ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PPositive
-> (Term s PPositive -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
xd'
          Term s PPositive
yd <- ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational 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 PRational) -> Term s PRational)
 -> TermCont @PRational s (Term s PPositive))
-> ((Term s PPositive -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PPositive
-> (Term s PPositive -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
yd'
          Term s PRational -> TermCont @PRational s (Term s PRational)
forall a. a -> TermCont @PRational s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PRational -> TermCont @PRational s (Term s PRational))
-> Term s PRational -> TermCont @PRational s (Term s PRational)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
yd Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
- Term s PInteger
yn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s PPositive
xd Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive
yd)
      )
      # x'
      # y'
  {-# INLINEABLE pscaleInteger #-}
  pscaleInteger :: forall (s :: S). Term s (PRational :--> (PInteger :--> PRational))
pscaleInteger = (forall (s :: S).
 Term s (PRational :--> (PInteger :--> PRational)))
-> Term s (PRational :--> (PInteger :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PRational :--> (PInteger :--> PRational)))
 -> Term s (PRational :--> (PInteger :--> PRational)))
-> (forall (s :: S).
    Term s (PRational :--> (PInteger :--> PRational)))
-> Term s (PRational :--> (PInteger :--> PRational))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PInteger -> Term s PRational)
-> Term s (PRational :--> (PInteger :--> PRational))
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 PInteger -> Term s PRational)
-> Term s (c :--> (PInteger :--> PRational))
plam ((Term s PRational -> Term s PInteger -> Term s PRational)
 -> Term s (PRational :--> (PInteger :--> PRational)))
-> (Term s PRational -> Term s PInteger -> Term s PRational)
-> Term s (PRational :--> (PInteger :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PInteger
e ->
    Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
      Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn Term s PInteger -> Term s PInteger -> Term s PInteger
forall (s :: S).
Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PInteger
e) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd

{-
-- | @since WIP
instance PAbs PRational where
  {-# INLINEABLE pabs #-}
-}

-- | @since WIP
instance PMultiplicativeSemigroup PRational where
  {-# INLINEABLE (#*) #-}
  Term s PRational
x' #* :: forall (s :: S).
Term s PRational -> Term s PRational -> Term s PRational
#* Term s PRational
y' =
    ClosedTerm (PRational :--> (PRational :--> PRational))
-> Term s (PRational :--> (PRational :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic
      ( (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
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 PRational -> Term s PRational)
-> Term s (c :--> (PRational :--> PRational))
plam ((Term s PRational -> Term s PRational -> Term s PRational)
 -> Term s (PRational :--> (PRational :--> PRational)))
-> (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PRational
y -> TermCont @PRational s (Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PRational s (Term s PRational) -> Term s PRational)
-> TermCont @PRational s (Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ do
          PRational Term s PInteger
xn Term s PPositive
xd <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x
          PRational Term s PInteger
yn Term s PPositive
yd <- ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PRational) -> Term s PRational)
 -> TermCont @PRational s (PRational s))
-> ((PRational s -> Term s PRational) -> Term s PRational)
-> TermCont @PRational s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
y
          Term s PRational -> TermCont @PRational s (Term s PRational)
forall a. a -> TermCont @PRational s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PRational -> TermCont @PRational s (Term s PRational))
-> Term s PRational -> TermCont @PRational s (Term s PRational)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
* Term s PInteger
yn) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto (Term s PPositive
xd Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
#* Term s PPositive
yd)
      )
      # x'
      # y'
  {-# INLINEABLE ppowPositive #-}
  ppowPositive :: forall (s :: S). Term s (PRational :--> (PPositive :--> PRational))
ppowPositive = (forall (s :: S).
 Term s (PRational :--> (PPositive :--> PRational)))
-> Term s (PRational :--> (PPositive :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PRational :--> (PPositive :--> PRational)))
 -> Term s (PRational :--> (PPositive :--> PRational)))
-> (forall (s :: S).
    Term s (PRational :--> (PPositive :--> PRational)))
-> Term s (PRational :--> (PPositive :--> PRational))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PPositive -> Term s PRational)
-> Term s (PRational :--> (PPositive :--> PRational))
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 PPositive -> Term s PRational)
-> Term s (c :--> (PPositive :--> PRational))
plam ((Term s PRational -> Term s PPositive -> Term s PRational)
 -> Term s (PRational :--> (PPositive :--> PRational)))
-> (Term s PRational -> Term s PPositive -> Term s PRational)
-> Term s (PRational :--> (PPositive :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PPositive
p ->
    Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
      PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> (Term s PPositive -> PRational s)
-> Term s PPositive
-> Term s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInteger :--> (PPositive :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PPositive :--> PInteger))
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s (a :--> (PPositive :--> a))
ppowPositive Term s (PInteger :--> (PPositive :--> PInteger))
-> Term s PInteger -> Term s (PPositive :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
xn Term s (PPositive :--> PInteger)
-> Term s PPositive -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
p) (Term s PPositive -> Term s PRational)
-> Term s PPositive -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s (PPositive :--> (PPositive :--> PPositive))
forall (s :: S). Term s (PPositive :--> (PPositive :--> PPositive))
forall (a :: PType) (s :: S).
PMultiplicativeSemigroup a =>
Term s (a :--> (PPositive :--> a))
ppowPositive Term s (PPositive :--> (PPositive :--> PPositive))
-> Term s PPositive -> Term s (PPositive :--> PPositive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
xd Term s (PPositive :--> PPositive)
-> Term s PPositive -> Term s PPositive
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
p

-- | @since WIP
instance PMultiplicativeMonoid PRational where
  {-# INLINEABLE pone #-}
  pone :: forall (s :: S). Term s PRational
pone = PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> (Term s PPositive -> PRational s)
-> Term s PPositive
-> Term s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone (Term s PPositive -> Term s PRational)
-> Term s PPositive -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone

-- | @since WIP
instance PRing PRational where
  {-# INLINEABLE pfromInteger #-}
  pfromInteger :: forall (s :: S). Integer -> Term s PRational
pfromInteger Integer
n = PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Integer -> Term s PInteger
forall a. Num a => Integer -> a
fromInteger Integer
n) Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone

-- | @since WIP
instance PIntegralDomain PRational where
  {-# INLINEABLE pabs #-}
  pabs :: forall (s :: S). Term s (PRational :--> PRational)
pabs =
    (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PRational))
 -> Term s (PRational :--> PRational))
-> (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$
      (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRational -> Term s PRational)
 -> Term s (PRational :--> PRational))
-> (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
        Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
          PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
xn) Term s PPositive
xd
  {-# INLINEABLE psignum #-}
  psignum :: forall (s :: S). Term s (PRational :--> PRational)
psignum = (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PRational))
 -> Term s (PRational :--> PRational))
-> (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRational -> Term s PRational)
 -> Term s (PRational :--> PRational))
-> (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
    Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
n Term s PPositive
_) ->
      [(Term s PBool, Term s PRational)]
-> Term s PRational -> Term s PRational
forall (a :: PType) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond
        [ (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0, Term s PRational
forall (s :: S). Term s PRational
forall (a :: PType) (s :: S). PAdditiveMonoid a => Term s a
pzero)
        , (Term s PInteger
n Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0, PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> (Term s PPositive -> PRational s)
-> Term s PPositive
-> Term s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (Integer
-1)) (Term s PPositive -> Term s PRational)
-> Term s PPositive -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone)
        ]
        Term s PRational
forall (s :: S). Term s PRational
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone

-- | @since WIP
instance Fractional (Term s PRational) where
  {-# INLINEABLE (/) #-}
  Term s PRational
x / :: Term s PRational -> Term s PRational -> Term s PRational
/ Term s PRational
y = Term s (PRational :--> (PRational :--> PRational))
ClosedTerm (PRational :--> (PRational :--> PRational))
inner Term s (PRational :--> (PRational :--> PRational))
-> Term s PRational -> Term s (PRational :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
x Term s (PRational :--> PRational)
-> Term s PRational -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
y
    where
      inner :: forall (s :: S). Term s (PRational :--> PRational :--> PRational)
      inner :: ClosedTerm (PRational :--> (PRational :--> PRational))
inner = ClosedTerm (PRational :--> (PRational :--> PRational))
-> Term s (PRational :--> (PRational :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PRational :--> (PRational :--> PRational))
 -> Term s (PRational :--> (PRational :--> PRational)))
-> ClosedTerm (PRational :--> (PRational :--> PRational))
-> Term s (PRational :--> (PRational :--> PRational))
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
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 PRational -> Term s PRational)
-> Term s (c :--> (PRational :--> PRational))
plam ((Term s PRational -> Term s PRational -> Term s PRational)
 -> Term s (PRational :--> (PRational :--> PRational)))
-> (Term s PRational -> Term s PRational -> Term s PRational)
-> Term s (PRational :--> (PRational :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x Term s PRational
y -> Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
        Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
y ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
yn Term s PPositive
yd) ->
          Term s PInteger
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
* Term s PInteger
yn) ((Term s PInteger -> Term s PRational) -> Term s PRational)
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
denm ->
            Term s PBool
-> Term s PRational -> Term s PRational -> Term s PRational
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (Term s PInteger
denm Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
              (Term s PString -> Term s PRational
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"Cannot divide by zero")
              (Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PInteger
xn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
yd) Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
denm)
  {-# INLINEABLE recip #-}
  recip :: Term s PRational -> Term s PRational
recip Term s PRational
x = Term s (PRational :--> PRational)
forall (s :: S). Term s (PRational :--> PRational)
inner Term s (PRational :--> PRational)
-> Term s PRational -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
x
    where
      inner :: forall (s :: S). Term s (PRational :--> PRational)
      inner :: forall (s :: S). Term s (PRational :--> PRational)
inner = (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PRational))
 -> Term s (PRational :--> PRational))
-> (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRational -> Term s PRational)
 -> Term s (PRational :--> PRational))
-> (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x -> Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
xn Term s PPositive
xd) ->
        [(Term s PBool, Term s PRational)]
-> Term s PRational -> Term s PRational
forall (a :: PType) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond
          [ (Term s PInteger
xn Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0, Term s PString -> Term s PRational
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"attempted to construct the reciprocal of zero")
          , (Term s PInteger
xn Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0, PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInner PPositive :--> PInner PPositive)
forall (s :: S). Term s (PInner PPositive :--> PInner PPositive)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInner PPositive :--> PInner PPositive)
-> Term s (PInner PPositive) -> Term s (PInner PPositive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd) (Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce (Term s PInteger -> Term s PPositive)
-> Term s PInteger -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
xn))
          ]
          (PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
xd) (Term s PInteger -> Term s PPositive
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s PInteger
xn))
  {-# INLINEABLE fromRational #-}
  fromRational :: Rational -> Term s PRational
fromRational = AsHaskell PRational -> Term s PRational
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (AsHaskell PRational -> Term s PRational)
-> (Rational -> AsHaskell PRational)
-> Rational
-> Term s PRational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Rational
Rational -> AsHaskell PRational
PlutusTx.fromGHC

instance PShow PRational where
  pshow' :: forall (s :: S). Bool -> Term s PRational -> Term s PString
pshow' Bool
_ Term s PRational
x =
    Term s (PRational :--> PString)
forall {s :: S}. Term s (PRational :--> PString)
pshowRat Term s (PRational :--> PString)
-> Term s PRational -> Term s PString
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
x
    where
      pshowRat :: Term s (PRational :--> PString)
pshowRat = (forall {s :: S}. Term s (PRational :--> PString))
-> Term s (PRational :--> PString)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall {s :: S}. Term s (PRational :--> PString))
 -> Term s (PRational :--> PString))
-> (forall {s :: S}. Term s (PRational :--> PString))
-> Term s (PRational :--> PString)
forall a b. (a -> b) -> a -> b
$
        (Term s PRational -> Term s PString)
-> Term s (PRational :--> PString)
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 PString) -> Term s (c :--> PString)
plam ((Term s PRational -> Term s PString)
 -> Term s (PRational :--> PString))
-> (Term s PRational -> Term s PString)
-> Term s (PRational :--> PString)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
n -> Term s PRational
-> (PRational s -> Term s PString) -> Term s PString
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
n ((PRational s -> Term s PString) -> Term s PString)
-> (PRational s -> Term s PString) -> Term s PString
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
x Term s PPositive
y) ->
          Term s PInteger -> Term s PString
forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow Term s PInteger
x Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s PString
"/" Term s PString -> Term s PString -> Term s PString
forall a. Semigroup a => a -> a -> a
<> Term s (PInner PPositive) -> Term s PString
forall (a :: PType) (s :: S). PShow a => Term s a -> Term s PString
pshow (Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
y)

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)

-- | NOTE: This instance produces a verified 'PPositive' as the excess output.
instance PTryFrom PData (PAsData PRational) where
  type PTryFromExcess PData (PAsData PRational) = Flip Term PPositive
  ptryFrom' :: forall (s :: S) (r :: PType).
Term s PData
-> ((Term s (PAsData PRational),
     Reduce (PTryFromExcess PData (PAsData PRational) s))
    -> Term s r)
-> Term s r
ptryFrom' Term s PData
opq = TermCont
  @r
  s
  (Term s (PAsData PRational),
   Reduce (PTryFromExcess PData (PAsData PRational) s))
-> ((Term s (PAsData PRational),
     Reduce (PTryFromExcess PData (PAsData PRational) 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 PRational),
    Reduce (PTryFromExcess PData (PAsData PRational) s))
 -> ((Term s (PAsData PRational),
      Reduce (PTryFromExcess PData (PAsData PRational) s))
     -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData PRational),
      Reduce (PTryFromExcess PData (PAsData PRational) s))
-> ((Term s (PAsData PRational),
     Reduce (PTryFromExcess PData (PAsData PRational) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData (PBuiltinList PData))
_, Term s (PBuiltinList PData)
ld) <- (((Term s (PAsData (PBuiltinList PData)),
   Term s (PBuiltinList PData))
  -> Term s r)
 -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Term s (PBuiltinList PData))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData (PBuiltinList PData)),
    Term s (PBuiltinList PData))
   -> Term s r)
  -> Term s r)
 -> TermCont
      @r
      s
      (Term s (PAsData (PBuiltinList PData)),
       Term s (PBuiltinList PData)))
-> (((Term s (PAsData (PBuiltinList PData)),
      Term s (PBuiltinList PData))
     -> Term s r)
    -> Term s r)
-> TermCont
     @r
     s
     (Term s (PAsData (PBuiltinList PData)),
      Term s (PBuiltinList PData))
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 (PBuiltinList PData)) Term s PData
opq
    Term s (PBuiltinList PData)
ratTail <- ((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 (PBuiltinList PData) -> Term s r) -> Term s r)
-> Term s (PBuiltinList PData)
-> TermCont @r s (Term s (PBuiltinList PData))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (PBuiltinList PData)
 -> TermCont @r s (Term s (PBuiltinList PData)))
-> Term s (PBuiltinList PData)
-> TermCont @r s (Term s (PBuiltinList PData))
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (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 (PBuiltinList PData)
ld
    ((() -> 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 :--> PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> list a)
ptail Term s (PBuiltinList PData :--> PBuiltinList PData)
-> Term s (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 (PBuiltinList PData)
ratTail Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (s :: S).
Term s (PBuiltinList PData)
-> Term s (PBuiltinList PData) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PBuiltinList PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a)
pnil) (() -> Term s r
f ()) (Term s r -> Term s r) -> Term s r -> Term s r
forall a b. (a -> b) -> a -> b
$ Term s PString -> Term s r
forall (a :: PType) (s :: S). Term s PString -> Term s a
ptraceInfoError Term s PString
"ptryFrom(PRational): data list length should be 2"
    (Term s (PAsData PInteger)
_, Term s PInteger
denm) <- (((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
 -> ((Term s (PAsData PInteger),
      Reduce (PTryFromExcess PData (PAsData PInteger) s))
     -> Term s r)
 -> Term s r)
-> Term s PData
-> ((Term s (PAsData PInteger),
     Reduce (PTryFromExcess PData (PAsData PInteger) s))
    -> Term s r)
-> Term s r
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList PData :--> PData)
forall (a :: PType) (s :: S).
PElemConstraint PBuiltinList a =>
Term s (PBuiltinList a :--> a)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList PData :--> PData)
-> Term s (PBuiltinList PData) -> Term s PData
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList PData)
ratTail
    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
denm
    (Term s (PAsData PRational), Term s PPositive)
-> TermCont @r s (Term s (PAsData PRational), Term s PPositive)
forall a. a -> TermCont @r s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PData -> Term s (PAsData PRational)
forall (b :: PType) (a :: PType) (s :: S). Term s a -> Term s b
punsafeCoerce Term s PData
opq, Term s PPositive
res)

preduce :: Term s (PRational :--> PRational)
preduce :: forall (s :: S). Term s (PRational :--> PRational)
preduce = (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PRational))
 -> Term s (PRational :--> PRational))
-> (forall (s :: S). Term s (PRational :--> PRational))
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PRational -> Term s PRational)
 -> Term s (PRational :--> PRational))
-> (Term s PRational -> Term s PRational)
-> Term s (PRational :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
  Term s PRational
-> (PRational s -> Term s PRational) -> Term s PRational
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PRational) -> Term s PRational)
-> (PRational s -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
n Term s PPositive
d) -> Term s (PInteger :--> (PInteger :--> PRational))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' Term s (PInteger :--> (PInteger :--> PRational))
-> Term s PInteger -> Term s (PInteger :--> PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
d

pgcd :: Term s (PInteger :--> PInteger :--> PInteger)
pgcd :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pgcd = (forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger)))
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger)))
 -> Term s (PInteger :--> (PInteger :--> PInteger)))
-> (forall (s :: S).
    Term s (PInteger :--> (PInteger :--> PInteger)))
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$
  (Term s PInteger -> Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> (PInteger :--> PInteger))
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 PInteger -> Term s PInteger)
-> Term s (c :--> (PInteger :--> PInteger))
plam ((Term s PInteger -> Term s PInteger -> Term s PInteger)
 -> Term s (PInteger :--> (PInteger :--> PInteger)))
-> (Term s PInteger -> Term s PInteger -> Term s PInteger)
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
x' Term s PInteger
y' -> TermCont @PInteger s (Term s PInteger) -> Term s PInteger
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PInteger s (Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (Term s PInteger) -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ do
    Term s PInteger
x <- ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PInteger))
-> (Term s PInteger
    -> (Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> Term s PInteger
-> TermCont @PInteger s (Term s PInteger)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger
-> (Term s PInteger -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x'
    Term s PInteger
y <- ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PInteger))
-> (Term s PInteger
    -> (Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> Term s PInteger
-> TermCont @PInteger s (Term s PInteger)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger
-> (Term s PInteger -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S).
PIntegralDomain a =>
Term s (a :--> a)
pabs Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y'
    Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a. a -> TermCont @PInteger s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$
      Term s PBool
-> Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PInteger
x Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
y)
        (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pgcd' Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x)
        (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pgcd' Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
x Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
y)

-- assumes inputs are non negative and a >= b
pgcd' :: Term s (PInteger :--> PInteger :--> PInteger)
pgcd' :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pgcd' = (forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger)))
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger)))
 -> Term s (PInteger :--> (PInteger :--> PInteger)))
-> (forall (s :: S).
    Term s (PInteger :--> (PInteger :--> PInteger)))
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (((PInteger :--> (PInteger :--> PInteger))
    :--> (PInteger :--> (PInteger :--> PInteger)))
   :--> (PInteger :--> (PInteger :--> PInteger)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (((a :--> b) :--> (a :--> b)) :--> (a :--> b))
pfix Term
  s
  (((PInteger :--> (PInteger :--> PInteger))
    :--> (PInteger :--> (PInteger :--> PInteger)))
   :--> (PInteger :--> (PInteger :--> PInteger)))
-> Term
     s
     ((PInteger :--> (PInteger :--> PInteger))
      :--> (PInteger :--> (PInteger :--> PInteger)))
-> Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ (Term s (PInteger :--> (PInteger :--> PInteger))
 -> Term s PInteger -> Term s PInteger -> Term s PInteger)
-> Term
     s
     ((PInteger :--> (PInteger :--> PInteger))
      :--> (PInteger :--> (PInteger :--> PInteger)))
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 PInteger -> Term s PInteger -> Term s PInteger)
-> Term s (c :--> (PInteger :--> (PInteger :--> PInteger)))
plam Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s PInteger -> Term s PInteger
forall {s :: S}.
Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s PInteger -> Term s PInteger
f
  where
    f :: Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s PInteger -> Term s PInteger
f Term s (PInteger :--> (PInteger :--> PInteger))
self Term s PInteger
a Term s PInteger
b =
      Term s PBool
-> Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PInteger
b Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
0)
        Term s PInteger
a
        (Term s PInteger -> Term s PInteger)
-> Term s PInteger -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
self Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
b Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmod Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
a Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
b

pnumerator :: Term s (PRational :--> PInteger)
pnumerator :: forall (s :: S). Term s (PRational :--> PInteger)
pnumerator = (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PInteger))
 -> Term s (PRational :--> PInteger))
-> (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
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 PInteger) -> Term s (c :--> PInteger)
plam ((Term s PRational -> Term s PInteger)
 -> Term s (PRational :--> PInteger))
-> (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x -> Term s PRational
-> (PRational s -> Term s PInteger) -> Term s PInteger
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PInteger) -> Term s PInteger)
-> (PRational s -> Term s PInteger) -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
n Term s PPositive
_) -> Term s PInteger
n

pdenominator :: Term s (PRational :--> PPositive)
pdenominator :: forall (s :: S). Term s (PRational :--> PPositive)
pdenominator = (forall (s :: S). Term s (PRational :--> PPositive))
-> Term s (PRational :--> PPositive)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PPositive))
 -> Term s (PRational :--> PPositive))
-> (forall (s :: S). Term s (PRational :--> PPositive))
-> Term s (PRational :--> PPositive)
forall a b. (a -> b) -> a -> b
$ (Term s PRational -> Term s PPositive)
-> Term s (PRational :--> PPositive)
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 PPositive) -> Term s (c :--> PPositive)
plam ((Term s PRational -> Term s PPositive)
 -> Term s (PRational :--> PPositive))
-> (Term s PRational -> Term s PPositive)
-> Term s (PRational :--> PPositive)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x -> Term s PRational
-> (PRational s -> Term s PPositive) -> Term s PPositive
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PPositive) -> Term s PPositive)
-> (PRational s -> Term s PPositive) -> Term s PPositive
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
_ Term s PPositive
d) -> Term s PPositive
d

pfromInteger :: Term s (PInteger :--> PRational)
pfromInteger :: forall (s :: S). Term s (PInteger :--> PRational)
pfromInteger = (forall (s :: S). Term s (PInteger :--> PRational))
-> Term s (PInteger :--> PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PInteger :--> PRational))
 -> Term s (PInteger :--> PRational))
-> (forall (s :: S). Term s (PInteger :--> PRational))
-> Term s (PInteger :--> PRational)
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PRational)
-> Term s (PInteger :--> PRational)
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 PRational) -> Term s (c :--> PRational)
plam ((Term s PInteger -> Term s PRational)
 -> Term s (PInteger :--> PRational))
-> (Term s PInteger -> Term s PRational)
-> Term s (PInteger :--> PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n -> PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational Term s PInteger
n Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: PType) (s :: S). PMultiplicativeMonoid a => Term s a
pone

pround :: Term s (PRational :--> PInteger)
pround :: forall (s :: S). Term s (PRational :--> PInteger)
pround = (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PInteger))
 -> Term s (PRational :--> PInteger))
-> (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$
  (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
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 PInteger) -> Term s (c :--> PInteger)
plam ((Term s PRational -> Term s PInteger)
 -> Term s (PRational :--> PInteger))
-> (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x -> TermCont @PInteger s (Term s PInteger) -> Term s PInteger
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PInteger s (Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (Term s PInteger) -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ do
    PRational Term s PInteger
a' Term s PPositive
b' <- ((PRational s -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (PRational s)
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((PRational s -> Term s PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (PRational s))
-> ((PRational s -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (PRational s)
forall a b. (a -> b) -> a -> b
$ Term s PRational
-> (PRational s -> Term s PInteger) -> Term s PInteger
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x
    Term s PInteger
a <- ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PInteger))
-> ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s PInteger
-> (Term s PInteger -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PInteger
a'
    Term s PPositive
b <- ((Term s PPositive -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PPositive))
-> ((Term s PPositive -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger s (Term s PPositive)
forall a b. (a -> b) -> a -> b
$ Term s PPositive
-> (Term s PPositive -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PPositive
b'
    Term s PInteger
base <- ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PInteger))
-> (Term s PInteger
    -> (Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> Term s PInteger
-> TermCont @PInteger s (Term s PInteger)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger
-> (Term s PInteger -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
a Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b
    Term s PInteger
rem <- ((Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> TermCont @PInteger 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 PInteger) -> Term s PInteger)
 -> TermCont @PInteger s (Term s PInteger))
-> (Term s PInteger
    -> (Term s PInteger -> Term s PInteger) -> Term s PInteger)
-> Term s PInteger
-> TermCont @PInteger s (Term s PInteger)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s PInteger
-> (Term s PInteger -> Term s PInteger) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmod Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
a Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b
    let result :: Term s PInteger
result =
          [(Term s PBool, Term s PInteger)]
-> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
[(Term s PBool, Term s a)] -> Term s a -> Term s a
pcond
            [ (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmod Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2 Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1, Term s PBool
-> Term s PInteger -> Term s PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2 Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s PInteger
rem) Term s PInteger
1 Term s PInteger
0)
            , (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2 Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
rem, Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pmod Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
base Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2)
            , (Term s PInteger
rem Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
2, Term s PInteger
0)
            ]
            Term s PInteger
1
    Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a. a -> TermCont @PInteger s a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PInteger -> TermCont @PInteger s (Term s PInteger))
-> Term s PInteger -> TermCont @PInteger s (Term s PInteger)
forall a b. (a -> b) -> a -> b
$ Term s PInteger
base Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
+ Term s PInteger
result

ptruncate :: Term s (PRational :--> PInteger)
ptruncate :: forall (s :: S). Term s (PRational :--> PInteger)
ptruncate = (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PRational :--> PInteger))
 -> Term s (PRational :--> PInteger))
-> (forall (s :: S). Term s (PRational :--> PInteger))
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$
  (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
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 PInteger) -> Term s (c :--> PInteger)
plam ((Term s PRational -> Term s PInteger)
 -> Term s (PRational :--> PInteger))
-> (Term s PRational -> Term s PInteger)
-> Term s (PRational :--> PInteger)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
    Term s PRational
-> (PRational s -> Term s PInteger) -> Term s PInteger
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
x ((PRational s -> Term s PInteger) -> Term s PInteger)
-> (PRational s -> Term s PInteger) -> Term s PInteger
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
a Term s PPositive
b) ->
      Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pquot Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
a Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
b

pproperFraction :: Term s (PRational :--> PPair PInteger PRational)
pproperFraction :: forall (s :: S). Term s (PRational :--> PPair PInteger PRational)
pproperFraction = (forall (s :: S). Term s (PRational :--> PPair PInteger PRational))
-> Term s (PRational :--> PPair PInteger PRational)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PRational :--> PPair PInteger PRational))
 -> Term s (PRational :--> PPair PInteger PRational))
-> (forall (s :: S).
    Term s (PRational :--> PPair PInteger PRational))
-> Term s (PRational :--> PPair PInteger PRational)
forall a b. (a -> b) -> a -> b
$
  (Term s PRational -> Term s (PPair PInteger PRational))
-> Term s (PRational :--> PPair PInteger PRational)
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 (PPair PInteger PRational))
-> Term s (c :--> PPair PInteger PRational)
plam ((Term s PRational -> Term s (PPair PInteger PRational))
 -> Term s (PRational :--> PPair PInteger PRational))
-> (Term s PRational -> Term s (PPair PInteger PRational))
-> Term s (PRational :--> PPair PInteger PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PRational
x ->
    Term s PInteger
-> (Term s PInteger -> Term s (PPair PInteger PRational))
-> Term s (PPair PInteger PRational)
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PRational :--> PInteger)
forall (s :: S). Term s (PRational :--> PInteger)
ptruncate Term s (PRational :--> PInteger)
-> Term s PRational -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PRational
x) ((Term s PInteger -> Term s (PPair PInteger PRational))
 -> Term s (PPair PInteger PRational))
-> (Term s PInteger -> Term s (PPair PInteger PRational))
-> Term s (PPair PInteger PRational)
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
q ->
      PPair PInteger PRational s -> Term s (PPair PInteger PRational)
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PPair PInteger PRational s -> Term s (PPair PInteger PRational))
-> PPair PInteger PRational s -> Term s (PPair PInteger PRational)
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PRational -> PPair PInteger PRational s
forall (a :: PType) (b :: PType) (s :: S).
Term s a -> Term s b -> PPair a b s
PPair Term s PInteger
q (Term s PRational
x Term s PRational -> Term s PRational -> Term s PRational
forall a. Num a => a -> a -> a
- Term s (PInteger :--> PRational)
forall (s :: S). Term s (PInteger :--> PRational)
Plutarch.Rational.pfromInteger Term s (PInteger :--> PRational)
-> Term s PInteger -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
q)

-- Helpers

cmpHelper ::
  forall (s :: S).
  Term s ((PInteger :--> PInteger :--> PBool) :--> PRational :--> PRational :--> PBool)
cmpHelper :: forall (s :: S).
Term
  s
  ((PInteger :--> (PInteger :--> PBool))
   :--> (PRational :--> (PRational :--> PBool)))
cmpHelper = (forall (s :: S).
 Term
   s
   ((PInteger :--> (PInteger :--> PBool))
    :--> (PRational :--> (PRational :--> PBool))))
-> Term
     s
     ((PInteger :--> (PInteger :--> PBool))
      :--> (PRational :--> (PRational :--> PBool)))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term
    s
    ((PInteger :--> (PInteger :--> PBool))
     :--> (PRational :--> (PRational :--> PBool))))
 -> Term
      s
      ((PInteger :--> (PInteger :--> PBool))
       :--> (PRational :--> (PRational :--> PBool))))
-> (forall (s :: S).
    Term
      s
      ((PInteger :--> (PInteger :--> PBool))
       :--> (PRational :--> (PRational :--> PBool))))
-> Term
     s
     ((PInteger :--> (PInteger :--> PBool))
      :--> (PRational :--> (PRational :--> PBool)))
forall a b. (a -> b) -> a -> b
$ (Term s (PInteger :--> (PInteger :--> PBool))
 -> Term s PRational -> Term s PRational -> Term s PBool)
-> Term
     s
     ((PInteger :--> (PInteger :--> PBool))
      :--> (PRational :--> (PRational :--> PBool)))
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 PRational -> Term s PRational -> Term s PBool)
-> Term s (c :--> (PRational :--> (PRational :--> PBool)))
plam ((Term s (PInteger :--> (PInteger :--> PBool))
  -> Term s PRational -> Term s PRational -> Term s PBool)
 -> Term
      s
      ((PInteger :--> (PInteger :--> PBool))
       :--> (PRational :--> (PRational :--> PBool))))
-> (Term s (PInteger :--> (PInteger :--> PBool))
    -> Term s PRational -> Term s PRational -> Term s PBool)
-> Term
     s
     ((PInteger :--> (PInteger :--> PBool))
      :--> (PRational :--> (PRational :--> PBool)))
forall a b. (a -> b) -> a -> b
$ \Term s (PInteger :--> (PInteger :--> PBool))
f Term s PRational
l Term s PRational
r ->
  Term s PRational -> (PRational s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
l ((PRational s -> Term s PBool) -> Term s PBool)
-> (PRational s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
ln Term s PPositive
ld) ->
    Term s PRational -> (PRational s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PRational
r ((PRational s -> Term s PBool) -> Term s PBool)
-> (PRational s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \(PRational Term s PInteger
rn Term s PPositive
rd) ->
      Term s (PInteger :--> (PInteger :--> PBool))
f 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 PPositive -> Term s (PInner PPositive)
forall (s :: S) (a :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
rd Term s PInteger -> Term s PInteger -> Term s PInteger
forall a. Num a => a -> a -> a
* Term s PInteger
ln) 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
# (Term s PInteger
rn 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 :: PType). Term s a -> Term s (PInner a)
pto Term s PPositive
ld)

-- Assumes d is not zero
preduce' :: forall (s :: S). Term s (PInteger :--> PInteger :--> PRational)
preduce' :: forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational))
preduce' = (forall (s :: S). Term s (PInteger :--> (PInteger :--> PRational)))
-> Term s (PInteger :--> (PInteger :--> PRational))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PInteger :--> (PInteger :--> PRational)))
 -> Term s (PInteger :--> (PInteger :--> PRational)))
-> (forall (s :: S).
    Term s (PInteger :--> (PInteger :--> PRational)))
-> Term s (PInteger :--> (PInteger :--> PRational))
forall a b. (a -> b) -> a -> b
$ (Term s PInteger -> Term s PInteger -> Term s PRational)
-> Term s (PInteger :--> (PInteger :--> PRational))
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 PInteger -> Term s PRational)
-> Term s (c :--> (PInteger :--> PRational))
plam ((Term s PInteger -> Term s PInteger -> Term s PRational)
 -> Term s (PInteger :--> (PInteger :--> PRational)))
-> (Term s PInteger -> Term s PInteger -> Term s PRational)
-> Term s (PInteger :--> (PInteger :--> PRational))
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
n Term s PInteger
d' ->
  Term s PInteger
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PInteger
d' ((Term s PInteger -> Term s PRational) -> Term s PRational)
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
d ->
    Term s PInteger
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall (s :: S) (a :: PType) (b :: PType).
Term s a -> (Term s a -> Term s b) -> Term s b
plet (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pgcd Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
d) ((Term s PInteger -> Term s PRational) -> Term s PRational)
-> (Term s PInteger -> Term s PRational) -> Term s PRational
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
r ->
      Term s PBool
-> Term s PRational -> Term s PRational -> Term s PRational
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
        (Term s PInteger
d Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
0)
        (PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
r)) (Term s PPositive -> PRational s)
-> Term s PPositive -> PRational s
forall a b. (a -> b) -> a -> b
$ Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: PType) (s :: S). PAdditiveGroup a => Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
d Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
r)))
        (PRational s -> Term s PRational
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PRational s -> Term s PRational)
-> PRational s -> Term s PRational
forall a b. (a -> b) -> a -> b
$ Term s PInteger -> Term s PPositive -> PRational s
forall (s :: S). Term s PInteger -> Term s PPositive -> PRational s
PRational (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
n Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
r) (Term s PPositive -> PRational s)
-> Term s PPositive -> PRational s
forall a b. (a -> b) -> a -> b
$ Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: PType). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInteger :--> (PInteger :--> PInteger))
forall (s :: S). Term s (PInteger :--> (PInteger :--> PInteger))
pdiv Term s (PInteger :--> (PInteger :--> PInteger))
-> Term s PInteger -> Term s (PInteger :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
d Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
r))