{-# LANGUAGE NoPartialTypeSignatures #-}

module Plutarch.Test.Methods (
  -- * POrd
  pmaxDefaultBetter,
  pminDefaultBetter,

  -- * PCountable
  psuccessorNBetter,

  -- * PEnumerable
  ppredecessorNBetter,

  -- * Additive
  pscalePositiveBetter,
  pscaleNaturalBetter,
  pscaleIntegerBetter,

  -- * Multiplicative
  ppowPositiveBetter,
  ppowNaturalBetter,
) where

import Data.Bifunctor (first)
import Data.ByteString.Short qualified as Short
import Data.Kind (Type)
import Data.SatInt (fromSatInt)
import Data.Tagged (Tagged (Tagged))
import Data.Text (Text)
import Data.Text qualified as Text
import Plutarch.Evaluate (evalScriptUnlimited)
import Plutarch.Internal.Numeric (pbySquaringDefault)
import Plutarch.Internal.Term (compileOptimized, punsafeCoerce)
import Plutarch.Prelude (
  PAdditiveGroup (pnegate, pscaleInteger),
  PAdditiveMonoid (pscaleNatural, pzero),
  PAdditiveSemigroup (pscalePositive, (#+)),
  PCountable (psuccessor, psuccessorN),
  PEnumerable (ppredecessor, ppredecessorN),
  PInteger,
  PMultiplicativeMonoid (ppowNatural),
  PMultiplicativeSemigroup (ppowPositive, (#*)),
  PNatural,
  POrd (pmax, pmin, (#<=)),
  PPositive,
  S,
  Term,
  pfix,
  pif,
  plam,
  plet,
  pone,
  (#),
  (#==),
  (:-->),
 )
import Plutarch.Script (Script (unScript))
import Plutarch.Test.Utils (typeName)
import Plutarch.Unsafe (punsafeDowncast)
import PlutusCore.Evaluation.Machine.ExBudget (ExBudget (ExBudget))
import PlutusCore.Evaluation.Machine.ExMemory (ExCPU (ExCPU), ExMemory (ExMemory))
import PlutusLedgerApi.Common (serialiseUPLC)
import Test.Tasty (TestTree)
import Test.Tasty.Providers (
  IsTest (run, testOptions),
  Result,
  singleTest,
  testFailed,
  testPassed,
 )
import Type.Reflection (Typeable)

{- | Given two arguments to test with, compares the default implementation of
'pmax' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
pmaxDefaultBetter ::
  forall (a :: S -> Type).
  (POrd a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s a) ->
  TestTree
pmaxDefaultBetter :: forall (a :: S -> Type).
(POrd a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> TestTree
pmaxDefaultBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s a
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> DefaultBetter
forall (a :: S -> Type).
POrd a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> DefaultBetter
PMax Term s a
forall (s :: S). Term s a
arg1 Term s a
forall (s :: S). Term s a
arg2
  where
    testName :: String
    testName :: String
testName = String
"pmax versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'pmin' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
pminDefaultBetter ::
  forall (a :: S -> Type).
  (POrd a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s a) ->
  TestTree
pminDefaultBetter :: forall (a :: S -> Type).
(POrd a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> TestTree
pminDefaultBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s a
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> DefaultBetter
forall (a :: S -> Type).
POrd a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s a) -> DefaultBetter
PMin Term s a
forall (s :: S). Term s a
arg1 Term s a
forall (s :: S). Term s a
arg2
  where
    testName :: String
    testName :: String
testName = String
"pmin versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'psuccessorN' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
psuccessorNBetter ::
  forall (a :: S -> Type).
  (PCountable a, Typeable a) =>
  (forall (s :: S). Term s PPositive) ->
  (forall (s :: S). Term s a) ->
  TestTree
psuccessorNBetter :: forall (a :: S -> Type).
(PCountable a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> TestTree
psuccessorNBetter forall (s :: S). Term s PPositive
arg1 forall (s :: S). Term s a
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> DefaultBetter
forall (a :: S -> Type).
PCountable a =>
(forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> DefaultBetter
PSuccessorN Term s PPositive
forall (s :: S). Term s PPositive
arg1 Term s a
forall (s :: S). Term s a
arg2
  where
    testName :: String
    testName :: String
testName = String
"psuccessorN versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'ppredecessorN' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
ppredecessorNBetter ::
  forall (a :: S -> Type).
  (PEnumerable a, Typeable a) =>
  (forall (s :: S). Term s PPositive) ->
  (forall (s :: S). Term s a) ->
  TestTree
ppredecessorNBetter :: forall (a :: S -> Type).
(PEnumerable a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> TestTree
ppredecessorNBetter forall (s :: S). Term s PPositive
arg1 forall (s :: S). Term s a
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> DefaultBetter
forall (a :: S -> Type).
PEnumerable a =>
(forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a) -> DefaultBetter
PPredecessorN Term s PPositive
forall (s :: S). Term s PPositive
arg1 Term s a
forall (s :: S). Term s a
arg2
  where
    testName :: String
    testName :: String
testName = String
"ppredecessorN versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'pscalePositive' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
pscalePositiveBetter ::
  forall (a :: S -> Type).
  (PAdditiveSemigroup a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s PPositive) ->
  TestTree
pscalePositiveBetter :: forall (a :: S -> Type).
(PAdditiveSemigroup a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> TestTree
pscalePositiveBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s PPositive
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> DefaultBetter
forall (a :: S -> Type).
PAdditiveSemigroup a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> DefaultBetter
PScalePositive Term s a
forall (s :: S). Term s a
arg1 Term s PPositive
forall (s :: S). Term s PPositive
arg2
  where
    testName :: String
    testName :: String
testName = String
"pscalePositive versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'pscaleNatural' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
pscaleNaturalBetter ::
  forall (a :: S -> Type).
  (PAdditiveMonoid a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s PNatural) ->
  TestTree
pscaleNaturalBetter :: forall (a :: S -> Type).
(PAdditiveMonoid a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> TestTree
pscaleNaturalBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s PNatural
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> DefaultBetter
forall (a :: S -> Type).
PAdditiveMonoid a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> DefaultBetter
PScaleNatural Term s a
forall (s :: S). Term s a
arg1 Term s PNatural
forall (s :: S). Term s PNatural
arg2
  where
    testName :: String
    testName :: String
testName = String
"pscaleNatural versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'pscaleInteger' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
pscaleIntegerBetter ::
  forall (a :: S -> Type).
  (PAdditiveGroup a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s PInteger) ->
  TestTree
pscaleIntegerBetter :: forall (a :: S -> Type).
(PAdditiveGroup a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PInteger) -> TestTree
pscaleIntegerBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s PInteger
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PInteger) -> DefaultBetter
forall (a :: S -> Type).
PAdditiveGroup a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PInteger) -> DefaultBetter
PScaleInteger Term s a
forall (s :: S). Term s a
arg1 Term s PInteger
forall (s :: S). Term s PInteger
arg2
  where
    testName :: String
    testName :: String
testName = String
"pscaleInteger versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'ppowPositive' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
ppowPositiveBetter ::
  forall (a :: S -> Type).
  (PMultiplicativeSemigroup a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s PPositive) ->
  TestTree
ppowPositiveBetter :: forall (a :: S -> Type).
(PMultiplicativeSemigroup a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> TestTree
ppowPositiveBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s PPositive
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> DefaultBetter
forall (a :: S -> Type).
PMultiplicativeSemigroup a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive) -> DefaultBetter
PPowPositive Term s a
forall (s :: S). Term s a
arg1 Term s PPositive
forall (s :: S). Term s PPositive
arg2
  where
    testName :: String
    testName :: String
testName = String
"ppowPositive versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

{- | Given two arguments to test with, compares the default implementation of
'ppowNatural' to the one defined for the given type. If the defined implementation
is worse than the default in any capacity, the test fails, indicating both
what metric (out of exunits, memory use or script size) was worse, and by how
much; otherwise, the test passes, indicating how much better (if at all) the
defined implementation is compared to the default.

@since 1.0.3
-}
ppowNaturalBetter ::
  forall (a :: S -> Type).
  (PMultiplicativeMonoid a, Typeable a) =>
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s PNatural) ->
  TestTree
ppowNaturalBetter :: forall (a :: S -> Type).
(PMultiplicativeMonoid a, Typeable @(S -> Type) a) =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> TestTree
ppowNaturalBetter forall (s :: S). Term s a
arg1 forall (s :: S). Term s PNatural
arg2 = String -> DefaultBetter -> TestTree
forall t. IsTest t => String -> t -> TestTree
singleTest String
testName (DefaultBetter -> TestTree) -> DefaultBetter -> TestTree
forall a b. (a -> b) -> a -> b
$ (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> DefaultBetter
forall (a :: S -> Type).
PMultiplicativeMonoid a =>
(forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural) -> DefaultBetter
PPowNatural Term s a
forall (s :: S). Term s a
arg1 Term s PNatural
forall (s :: S). Term s PNatural
arg2
  where
    testName :: String
    testName :: String
testName = String
"ppowNatural versus default for " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> forall k (a :: k). Typeable @k a => String
typeName @(S -> Type) @a

-- Helpers

data DefaultBetter where
  PMax ::
    forall (a :: S -> Type).
    POrd a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s a) ->
    DefaultBetter
  PMin ::
    forall (a :: S -> Type).
    POrd a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s a) ->
    DefaultBetter
  PSuccessorN ::
    forall (a :: S -> Type).
    PCountable a =>
    (forall (s :: S). Term s PPositive) ->
    (forall (s :: S). Term s a) ->
    DefaultBetter
  PPredecessorN ::
    forall (a :: S -> Type).
    PEnumerable a =>
    (forall (s :: S). Term s PPositive) ->
    (forall (s :: S). Term s a) ->
    DefaultBetter
  PScalePositive ::
    forall (a :: S -> Type).
    PAdditiveSemigroup a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s PPositive) ->
    DefaultBetter
  PScaleNatural ::
    forall (a :: S -> Type).
    PAdditiveMonoid a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s PNatural) ->
    DefaultBetter
  PScaleInteger ::
    forall (a :: S -> Type).
    PAdditiveGroup a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s PInteger) ->
    DefaultBetter
  PPowPositive ::
    forall (a :: S -> Type).
    PMultiplicativeSemigroup a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s PPositive) ->
    DefaultBetter
  PPowNatural ::
    forall (a :: S -> Type).
    PMultiplicativeMonoid a =>
    (forall (s :: S). Term s a) ->
    (forall (s :: S). Term s PNatural) ->
    DefaultBetter

instance IsTest DefaultBetter where
  testOptions :: Tagged @Type DefaultBetter [OptionDescription]
testOptions = [OptionDescription]
-> Tagged @Type DefaultBetter [OptionDescription]
forall {k} (s :: k) b. b -> Tagged @k s b
Tagged []
  run :: OptionSet -> DefaultBetter -> (Progress -> IO ()) -> IO Result
run OptionSet
_ DefaultBetter
t Progress -> IO ()
_ = Result -> IO Result
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Result -> IO Result)
-> (Either String (Integer, Integer, Integer) -> Result)
-> Either String (Integer, Integer, Integer)
-> IO Result
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Result)
-> ((Integer, Integer, Integer) -> Result)
-> Either String (Integer, Integer, Integer)
-> Result
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Result
testFailed (Integer, Integer, Integer) -> Result
handleDeltas (Either String (Integer, Integer, Integer) -> IO Result)
-> Either String (Integer, Integer, Integer) -> IO Result
forall a b. (a -> b) -> a -> b
$ case DefaultBetter
t of
    PMax forall (s :: S). Term s a
x forall (s :: S). Term s a
y -> String
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s a)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"pmax" Term s (a :--> (a :--> a))
forall (s :: S). Term s (a :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s (a :--> (a :--> a))
pmaxDefault ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a)))
-> (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x' Term s a
y' -> Term s a -> Term s a -> Term s a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s t
pmax Term s a
x' Term s a
y') Term s a
forall (s :: S). Term s a
x Term s a
forall (s :: S). Term s a
y
    PMin forall (s :: S). Term s a
x forall (s :: S). Term s a
y -> String
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s (a :--> (a :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s a)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"pmin" Term s (a :--> (a :--> a))
forall (s :: S). Term s (a :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
POrd a =>
Term s (a :--> (a :--> a))
pminDefault ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a)))
-> (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x' Term s a
y' -> Term s a -> Term s a -> Term s a
forall (s :: S). Term s a -> Term s a -> Term s a
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s t
pmin Term s a
x' Term s a
y') Term s a
forall (s :: S). Term s a
x Term s a
forall (s :: S). Term s a
y
    PSuccessorN forall (s :: S). Term s PPositive
p forall (s :: S). Term s a
x -> String
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"psuccessorN" Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorNDefault Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorN Term s PPositive
forall (s :: S). Term s PPositive
p Term s a
forall (s :: S). Term s a
x
    PPredecessorN forall (s :: S). Term s PPositive
p forall (s :: S). Term s a
x -> String
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s (PPositive :--> (a :--> a)))
-> (forall (s :: S). Term s PPositive)
-> (forall (s :: S). Term s a)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"ppredecessorN" Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorNDefault Term s (PPositive :--> (a :--> a))
forall (s :: S). Term s (PPositive :--> (a :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorN Term s PPositive
forall (s :: S). Term s PPositive
p Term s a
forall (s :: S). Term s a
x
    PScalePositive forall (s :: S). Term s a
x forall (s :: S). Term s PPositive
p -> String
-> (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"pscalePositive" ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ (forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
pbySquaringDefault Term s' a -> Term s' a -> Term s' a
forall (s' :: S). Term s' a -> Term s' a -> Term s' a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
(#+)) ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive) Term s a
forall (s :: S). Term s a
x Term s PPositive
forall (s :: S). Term s PPositive
p
    PScaleNatural forall (s :: S). Term s a
x forall (s :: S). Term s PNatural
n -> String
-> (forall (s :: S). Term s (a :--> (PNatural :--> a)))
-> (forall (s :: S). Term s (a :--> (PNatural :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"pscaleNatural" Term s (a :--> (PNatural :--> a))
forall (s :: S). Term s (a :--> (PNatural :--> a))
forall (a :: S -> Type) (s :: S).
PAdditiveMonoid a =>
Term s (a :--> (PNatural :--> a))
pscaleNaturalDefault ((Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural -> Term s a)
-> Term s (c :--> (PNatural :--> a))
plam Term s a -> Term s PNatural -> Term s a
forall (s :: S). Term s a -> Term s PNatural -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveMonoid a =>
Term s a -> Term s PNatural -> Term s a
pscaleNatural) Term s a
forall (s :: S). Term s a
x Term s PNatural
forall (s :: S). Term s PNatural
n
    PScaleInteger forall (s :: S). Term s a
x forall (s :: S). Term s PInteger
i -> String
-> (forall (s :: S). Term s (a :--> (PInteger :--> a)))
-> (forall (s :: S). Term s (a :--> (PInteger :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PInteger)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"pscaleInteger" Term s (a :--> (PInteger :--> a))
forall (s :: S). Term s (a :--> (PInteger :--> a))
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> (PInteger :--> a))
pscaleIntegerDefault ((Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s a)
-> Term s (c :--> (PInteger :--> a))
plam Term s a -> Term s PInteger -> Term s a
forall (s :: S). Term s a -> Term s PInteger -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s a -> Term s PInteger -> Term s a
pscaleInteger) Term s a
forall (s :: S). Term s a
x Term s PInteger
forall (s :: S). Term s PInteger
i
    PPowPositive forall (s :: S). Term s a
x forall (s :: S). Term s PPositive
p -> String
-> (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> (forall (s :: S). Term s (a :--> (PPositive :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PPositive)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"ppowPositive" ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ (forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
(forall (s' :: S). Term s' a -> Term s' a -> Term s' a)
-> Term s a -> Term s PPositive -> Term s a
pbySquaringDefault Term s' a -> Term s' a -> Term s' a
forall (s' :: S). Term s' a -> Term s' a -> Term s' a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s a -> Term s a
(#*)) ((Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s PPositive -> Term s a
ppowPositive) Term s a
forall (s :: S). Term s a
x Term s PPositive
forall (s :: S). Term s PPositive
p
    PPowNatural forall (s :: S). Term s a
x forall (s :: S). Term s PNatural
n -> String
-> (forall (s :: S). Term s (a :--> (PNatural :--> a)))
-> (forall (s :: S). Term s (a :--> (PNatural :--> a)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s PNatural)
-> Either String (Integer, Integer, Integer)
forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
"ppowNatural" Term s (a :--> (PNatural :--> a))
forall (s :: S). Term s (a :--> (PNatural :--> a))
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s (a :--> (PNatural :--> a))
ppowNaturalDefault ((Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural -> Term s a)
-> Term s (c :--> (PNatural :--> a))
plam Term s a -> Term s PNatural -> Term s a
forall (s :: S). Term s a -> Term s PNatural -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a -> Term s PNatural -> Term s a
ppowNatural) Term s a
forall (s :: S). Term s a
x Term s PNatural
forall (s :: S). Term s PNatural
n
    where
      pmaxDefault :: forall (a :: S -> Type) (s :: S). POrd a => Term s (a :--> a :--> a)
      pmaxDefault :: forall (a :: S -> Type) (s :: S).
POrd a =>
Term s (a :--> (a :--> a))
pmaxDefault = (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a)))
-> (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s a
y -> Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
y) Term s a
y Term s a
x
      pminDefault :: forall (a :: S -> Type) (s :: S). POrd a => Term s (a :--> a :--> a)
      pminDefault :: forall (a :: S -> Type) (s :: S).
POrd a =>
Term s (a :--> (a :--> a))
pminDefault = (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a)))
-> (Term s a -> Term s a -> Term s a) -> Term s (a :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s a
y -> Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s a
x Term s a -> Term s a -> Term s PBool
forall (s :: S). Term s a -> Term s a -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s a
y) Term s a
x Term s a
y
      psuccessorNDefault ::
        forall (a :: S -> Type) (s :: S).
        PCountable a => Term s (PPositive :--> a :--> a)
      psuccessorNDefault :: forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s (PPositive :--> (a :--> a))
psuccessorNDefault = (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s PPositive -> Term s a -> Term s a)
 -> Term s (PPositive :--> (a :--> a)))
-> (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
p Term s a
x -> Term s PPositive -> Term s (a :--> (PPositive :--> a))
forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s PPositive -> Term s (a :--> (PPositive :--> a))
goSucc Term s PPositive
p Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
      goSucc ::
        forall (a :: S -> Type) (s :: S).
        PCountable a => Term s PPositive -> Term s (a :--> PPositive :--> a)
      goSucc :: forall (a :: S -> Type) (s :: S).
PCountable a =>
Term s PPositive -> Term s (a :--> (PPositive :--> a))
goSucc Term s PPositive
limit = (Term s (a :--> (PPositive :--> a))
 -> Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s (a :--> (PPositive :--> a))
  -> Term s (a :--> (PPositive :--> a)))
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s (a :--> (PPositive :--> a))
    -> Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (PPositive :--> a))
self -> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
acc Term s PPositive
count ->
        Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PPositive
count Term s PPositive -> Term s PPositive -> Term s PBool
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PPositive
limit) Term s a
acc (Term s (a :--> (PPositive :--> a))
self Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S). PCountable a => Term s (a :--> a)
psuccessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
acc) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PPositive
count Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone))
      ppredecessorNDefault ::
        forall (a :: S -> Type) (s :: S).
        PEnumerable a => Term s (PPositive :--> a :--> a)
      ppredecessorNDefault :: forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (PPositive :--> (a :--> a))
ppredecessorNDefault = (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s a -> Term s a) -> Term s (c :--> (a :--> a))
plam ((Term s PPositive -> Term s a -> Term s a)
 -> Term s (PPositive :--> (a :--> a)))
-> (Term s PPositive -> Term s a -> Term s a)
-> Term s (PPositive :--> (a :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s PPositive
n Term s a
x -> Term s PPositive -> Term s (a :--> (PPositive :--> a))
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s PPositive -> Term s (a :--> (PPositive :--> a))
goPred Term s PPositive
n Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
x) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
      goPred ::
        forall (a :: S -> Type) (s :: S).
        PEnumerable a => Term s PPositive -> Term s (a :--> PPositive :--> a)
      goPred :: forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s PPositive -> Term s (a :--> (PPositive :--> a))
goPred Term s PPositive
limit = (Term s (a :--> (PPositive :--> a))
 -> Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall (a :: S -> Type) (b :: S -> Type) (s :: S).
(Term s (a :--> b) -> Term s (a :--> b)) -> Term s (a :--> b)
pfix ((Term s (a :--> (PPositive :--> a))
  -> Term s (a :--> (PPositive :--> a)))
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s (a :--> (PPositive :--> a))
    -> Term s (a :--> (PPositive :--> a)))
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s (a :--> (PPositive :--> a))
self -> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PPositive -> Term s a)
-> Term s (c :--> (PPositive :--> a))
plam ((Term s a -> Term s PPositive -> Term s a)
 -> Term s (a :--> (PPositive :--> a)))
-> (Term s a -> Term s PPositive -> Term s a)
-> Term s (a :--> (PPositive :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
acc Term s PPositive
count ->
        Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PPositive
count Term s PPositive -> Term s PPositive -> Term s PBool
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PPositive
limit) Term s a
acc (Term s (a :--> (PPositive :--> a))
self Term s (a :--> (PPositive :--> a))
-> Term s a -> Term s (PPositive :--> a)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PEnumerable a =>
Term s (a :--> a)
ppredecessor Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
acc) Term s (PPositive :--> a) -> Term s PPositive -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s PPositive
count Term s PPositive -> Term s PPositive -> Term s PPositive
forall (s :: S).
Term s PPositive -> Term s PPositive -> Term s PPositive
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s a -> Term s a
#+ Term s PPositive
forall (s :: S). Term s PPositive
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone))
      pscaleNaturalDefault ::
        forall (a :: S -> Type) (s :: S).
        PAdditiveMonoid a => Term s (a :--> PNatural :--> a)
      pscaleNaturalDefault :: forall (a :: S -> Type) (s :: S).
PAdditiveMonoid a =>
Term s (a :--> (PNatural :--> a))
pscaleNaturalDefault = (Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural -> Term s a)
-> Term s (c :--> (PNatural :--> a))
plam ((Term s a -> Term s PNatural -> Term s a)
 -> Term s (a :--> (PNatural :--> a)))
-> (Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s PNatural
n -> Term s PNatural -> (Term s PNatural -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s a) -> Term s a)
-> (Term s PNatural -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
n' ->
        Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s PNatural
n' Term s PNatural -> Term s PNatural -> Term s PBool
forall (s :: S). Term s PNatural -> Term s PNatural -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PNatural
forall (s :: S). Term s PNatural
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero) Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
x (Term s PNatural -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PNatural
n'))
      pscaleIntegerDefault ::
        forall (a :: S -> Type) (s :: S).
        PAdditiveGroup a => Term s (a :--> PInteger :--> a)
      pscaleIntegerDefault :: forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> (PInteger :--> a))
pscaleIntegerDefault = (Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PInteger -> Term s a)
-> Term s (c :--> (PInteger :--> a))
plam ((Term s a -> Term s PInteger -> Term s a)
 -> Term s (a :--> (PInteger :--> a)))
-> (Term s a -> Term s PInteger -> Term s a)
-> Term s (a :--> (PInteger :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
b Term s PInteger
e ->
        Term s PInteger -> (Term s PInteger -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PInteger
e ((Term s PInteger -> Term s a) -> Term s a)
-> (Term s PInteger -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PInteger
e' ->
          Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
            (Term s PInteger
e' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
            Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero
            ( Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                (Term s PInteger
e' Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: S -> Type) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s PInteger
forall (s :: S). Term s PInteger
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
                (Term s (a :--> a)
forall (s :: S). Term s (a :--> a)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (a :--> a) -> Term s a -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
b (Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner (PInner PPositive)) -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInteger :--> PInteger)
forall (s :: S). Term s (PInteger :--> PInteger)
forall (a :: S -> Type) (s :: S).
PAdditiveGroup a =>
Term s (a :--> a)
pnegate Term s (PInteger :--> PInteger)
-> Term s PInteger -> Term s PInteger
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PInteger
e'))))
                (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PAdditiveSemigroup a =>
Term s a -> Term s PPositive -> Term s a
pscalePositive Term s a
b (Term s (PInner PPositive) -> Term s PPositive
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast (Term s (PInner (PInner PPositive)) -> Term s (PInner PPositive)
forall (s :: S) (a :: S -> Type). Term s (PInner a) -> Term s a
punsafeDowncast Term s PInteger
Term s (PInner (PInner PPositive))
e')))
            )
      ppowNaturalDefault ::
        forall (a :: S -> Type) (s :: S).
        PMultiplicativeMonoid a => Term s (a :--> PNatural :--> a)
      ppowNaturalDefault :: forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s (a :--> (PNatural :--> a))
ppowNaturalDefault = (Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a (b :: S -> Type) (s :: S) (c :: S -> Type).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: S -> Type).
HasCallStack =>
(Term s c -> Term s PNatural -> Term s a)
-> Term s (c :--> (PNatural :--> a))
plam ((Term s a -> Term s PNatural -> Term s a)
 -> Term s (a :--> (PNatural :--> a)))
-> (Term s a -> Term s PNatural -> Term s a)
-> Term s (a :--> (PNatural :--> a))
forall a b. (a -> b) -> a -> b
$ \Term s a
x Term s PNatural
n -> Term s PNatural -> (Term s PNatural -> Term s a) -> Term s a
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s a -> (Term s a -> Term s b) -> Term s b
plet Term s PNatural
n ((Term s PNatural -> Term s a) -> Term s a)
-> (Term s PNatural -> Term s a) -> Term s a
forall a b. (a -> b) -> a -> b
$ \Term s PNatural
n' ->
        Term s PBool -> Term s a -> Term s a -> Term s a
forall (a :: S -> Type) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s PNatural
n' Term s PNatural -> Term s PNatural -> Term s PBool
forall (s :: S). Term s PNatural -> Term s PNatural -> Term s PBool
forall (t :: S -> Type) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PNatural
forall (s :: S). Term s PNatural
forall (a :: S -> Type) (s :: S). PAdditiveMonoid a => Term s a
pzero)
          Term s a
forall (s :: S). Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeMonoid a =>
Term s a
pone
          (Term s a -> Term s PPositive -> Term s a
forall (s :: S). Term s a -> Term s PPositive -> Term s a
forall (a :: S -> Type) (s :: S).
PMultiplicativeSemigroup a =>
Term s a -> Term s PPositive -> Term s a
ppowPositive Term s a
x (Term s PNatural -> Term s PPositive
forall (b :: S -> Type) (a :: S -> Type) (s :: S).
Term s a -> Term s b
punsafeCoerce Term s PNatural
n'))

scriptSize :: Script -> Integer
scriptSize :: Script -> Integer
scriptSize = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> (Script -> Int) -> Script -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortByteString -> Int
Short.length (ShortByteString -> Int)
-> (Script -> ShortByteString) -> Script -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program DeBruijn DefaultUni DefaultFun () -> ShortByteString
serialiseUPLC (Program DeBruijn DefaultUni DefaultFun () -> ShortByteString)
-> (Script -> Program DeBruijn DefaultUni DefaultFun ())
-> Script
-> ShortByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Script -> Program DeBruijn DefaultUni DefaultFun ()
unScript

tryAndApply ::
  forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
  String ->
  (forall (s :: S). Term s (a :--> b :--> c)) ->
  (forall (s :: S). Term s (a :--> b :--> c)) ->
  (forall (s :: S). Term s a) ->
  (forall (s :: S). Term s b) ->
  Either String (Integer, Integer, Integer)
tryAndApply :: forall (a :: S -> Type) (b :: S -> Type) (c :: S -> Type).
String
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s (a :--> (b :--> c)))
-> (forall (s :: S). Term s a)
-> (forall (s :: S). Term s b)
-> Either String (Integer, Integer, Integer)
tryAndApply String
op forall (s :: S). Term s (a :--> (b :--> c))
defaultImpl forall (s :: S). Term s (a :--> (b :--> c))
definedImpl forall (s :: S). Term s a
x forall (s :: S). Term s b
y = do
  Script
usingDefault <- (Text -> String) -> Either Text Script -> Either String Script
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Text -> String
formatCompileErr String
"default") (Either Text Script -> Either String Script)
-> ((forall (s :: S). Term s c) -> Either Text Script)
-> (forall (s :: S). Term s c)
-> Either String Script
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (s :: S). Term s c) -> Either Text Script
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> Either Text Script
compileOptimized ((forall (s :: S). Term s c) -> Either String Script)
-> (forall (s :: S). Term s c) -> Either String Script
forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
forall (s :: S). Term s (a :--> (b :--> c))
defaultImpl Term s (a :--> (b :--> c)) -> Term s a -> Term s (b :--> c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
forall (s :: S). Term s a
x Term s (b :--> c) -> Term s b -> Term s c
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
forall (s :: S). Term s b
y
  Script
usingImpl <- (Text -> String) -> Either Text Script -> Either String Script
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> Text -> String
formatCompileErr String
"defined") (Either Text Script -> Either String Script)
-> ((forall (s :: S). Term s c) -> Either Text Script)
-> (forall (s :: S). Term s c)
-> Either String Script
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (s :: S). Term s c) -> Either Text Script
forall (a :: S -> Type).
(forall (s :: S). Term s a) -> Either Text Script
compileOptimized ((forall (s :: S). Term s c) -> Either String Script)
-> (forall (s :: S). Term s c) -> Either String Script
forall a b. (a -> b) -> a -> b
$ Term s (a :--> (b :--> c))
forall (s :: S). Term s (a :--> (b :--> c))
definedImpl Term s (a :--> (b :--> c)) -> Term s a -> Term s (b :--> c)
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s a
forall (s :: S). Term s a
x Term s (b :--> c) -> Term s b -> Term s c
forall (s :: S) (a :: S -> Type) (b :: S -> Type).
Term s (a :--> b) -> Term s a -> Term s b
# Term s b
forall (s :: S). Term s b
y
  (Integer
cpuDefault, Integer
memDefault) <- String -> Script -> Either String (Integer, Integer)
tryEval String
"Default" Script
usingDefault
  (Integer
cpuImpl, Integer
memImpl) <- String -> Script -> Either String (Integer, Integer)
tryEval String
"Defined" Script
usingImpl
  let sizeDelta :: Integer
sizeDelta = Script -> Integer
scriptSize Script
usingDefault Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Script -> Integer
scriptSize Script
usingImpl
  let exunitDelta :: Integer
exunitDelta = Integer
cpuDefault Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
cpuImpl
  let memDelta :: Integer
memDelta = Integer
memDefault Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
memImpl
  (Integer, Integer, Integer)
-> Either String (Integer, Integer, Integer)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer
sizeDelta, Integer
exunitDelta, Integer
memDelta)
  where
    formatCompileErr :: String -> Text -> String
    formatCompileErr :: String -> Text -> String
formatCompileErr String
which Text
err =
      String
"Failed to compile "
        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
which
        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"implementation of "
        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
op
        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": "
        String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
err
    tryEval :: String -> Script -> Either String (Integer, Integer)
    tryEval :: String -> Script -> Either String (Integer, Integer)
tryEval String
which Script
s = case Script
-> (Either
      (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
      Script,
    ExBudget, [Text])
evalScriptUnlimited Script
s of
      (Left CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
err, ExBudget
_, [Text]
_) -> String -> Either String (Integer, Integer)
forall a b. a -> Either a b
Left (String -> Either String (Integer, Integer))
-> String -> Either String (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ String
which String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" implementation of " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
op String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" did not evaluate: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
-> String
forall a. Show a => a -> String
show CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
err
      (Right Script
_, ExBudget (ExCPU CostingInteger
cpu) (ExMemory CostingInteger
mem), [Text]
_) -> (Integer, Integer) -> Either String (Integer, Integer)
forall a. a -> Either String a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall a. Num a => CostingInteger -> a
fromSatInt @Integer CostingInteger
cpu, forall a. Num a => CostingInteger -> a
fromSatInt @Integer CostingInteger
mem)

handleDeltas :: (Integer, Integer, Integer) -> Result
handleDeltas :: (Integer, Integer, Integer) -> Result
handleDeltas deltas :: (Integer, Integer, Integer)
deltas@(Integer
sizeDelta, Integer
exUnitDelta, Integer
memDelta) =
  let formatted :: String
formatted = (Integer, Integer, Integer) -> String
formatDelta (Integer, Integer, Integer)
deltas
   in if (Integer
sizeDelta Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) Bool -> Bool -> Bool
&& (Integer
exUnitDelta Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) Bool -> Bool -> Bool
&& (Integer
memDelta Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0)
        then String -> Result
testPassed String
formatted
        else String -> Result
testFailed String
formatted

formatDelta :: (Integer, Integer, Integer) -> String
formatDelta :: (Integer, Integer, Integer) -> String
formatDelta (Integer
sizeDelta, Integer
exUnitDelta, Integer
memDelta) =
  String
"Difference from default implementation (negative means worse):\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Script size: "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
sizeDelta
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Exunits: "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
exUnitDelta
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Memory: "
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
memDelta
    String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n"