-- editorconfig-checker-disable-file

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}

module Evaluation.Builtins.Conversion (
  i2bProperty1,
  i2bProperty2,
  i2bProperty3,
  i2bProperty4,
  i2bProperty5,
  i2bProperty6,
  i2bProperty7,
  b2iProperty1,
  b2iProperty2,
  b2iProperty3,
  i2bCipExamples,
  i2bLimitTests,
  b2iCipExamples
  ) where

import Evaluation.Builtins.Common (typecheckEvaluateCek)
import PlutusCore qualified as PLC
import PlutusCore.Bitwise qualified as Bitwise (maximumOutputLength)
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultBuiltinCostModelForTesting)
import PlutusCore.MkPlc (builtin, mkConstant, mkIterAppNoAnn)
import PlutusPrelude (Word8, def)
import UntypedPlutusCore qualified as UPLC

import Data.ByteString (ByteString)
import GHC.Exts (fromList)
import Hedgehog (Gen, PropertyT, annotateShow, failure, forAllWith, (===))
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Test.Tasty (TestTree)
import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)
import Text.Show.Pretty (ppShow)

-- Properties and examples directly from CIP-121:
--
-- - https://github.com/cardano-foundation/CIPs/tree/master/CIP-0121#builtinintegertobytestring
-- - https://github.com/cardano-foundation/CIPs/tree/master/CIP-01211#builtinbytestringtointeger

-- lengthOfByteString (integerToByteString e d 0) = d
i2bProperty1 :: PropertyT IO ()
i2bProperty1 :: PropertyT IO ()
i2bProperty1 = do
  Bool
e <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  -- We limit this temporarily due to the limit imposed on lengths for the
  -- conversion primitive.
  Integer
d <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow (Gen Integer -> PropertyT IO Integer)
-> Gen Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 Integer
Bitwise.maximumOutputLength)
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
e,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
d,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
        ]
  let lenExp :: Term TyName Name DefaultUni DefaultFun ()
lenExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LengthOfByteString) [
        Term TyName Name DefaultUni DefaultFun ()
actualExp
        ]
  let compareExp :: Term TyName Name DefaultUni DefaultFun ()
compareExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.EqualsInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
d,
        Term TyName Name DefaultUni DefaultFun ()
lenExp
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True) Term TyName Name DefaultUni DefaultFun ()
compareExp

-- indexByteString (integerToByteString e k 0) j = 0
i2bProperty2 :: PropertyT IO ()
i2bProperty2 :: PropertyT IO ()
i2bProperty2 = do
  Bool
e <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  -- We limit this temporarily due to the limit imposed on lengths for the
  -- conversion primitive.
  Integer
k <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow (Gen Integer -> PropertyT IO Integer)
-> Gen Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
1 Integer
Bitwise.maximumOutputLength)
  Integer
j <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow (Gen Integer -> PropertyT IO Integer)
-> Gen Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 (Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
e,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
k,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
        ]
  let indexExp :: Term TyName Name DefaultUni DefaultFun ()
indexExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IndexByteString) [
        Term TyName Name DefaultUni DefaultFun ()
actualExp,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
j
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0) Term TyName Name DefaultUni DefaultFun ()
indexExp

-- lengthOfByteString (integerToByteString e 0 p) > 0
i2bProperty3 :: PropertyT IO ()
i2bProperty3 :: PropertyT IO ()
i2bProperty3 = do
  Bool
e <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  Integer
p <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genP
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
e,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
p
        ]
  let lengthExp :: Term TyName Name DefaultUni DefaultFun ()
lengthExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LengthOfByteString) [
        Term TyName Name DefaultUni DefaultFun ()
actualExp
        ]
  let compareExp :: Term TyName Name DefaultUni DefaultFun ()
compareExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LessThanInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
        Term TyName Name DefaultUni DefaultFun ()
lengthExp
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True) Term TyName Name DefaultUni DefaultFun ()
compareExp

-- integerToByteString False 0 (multiplyInteger p 256) = consByteString
-- 0 (integerToByteString False 0 p)
i2bProperty4 :: PropertyT IO ()
i2bProperty4 :: PropertyT IO ()
i2bProperty4 = do
  Integer
p <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genP
  let pExp :: Term TyName Name DefaultUni DefaultFun ()
pExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
p
                ]
  let pTimesExp :: Term TyName Name DefaultUni DefaultFun ()
pTimesExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.MultiplyInteger) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
p,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
256
                    ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                    Term TyName Name DefaultUni DefaultFun ()
pTimesExp
                    ]
  let expectedExp :: Term TyName Name DefaultUni DefaultFun ()
expectedExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ConsByteString) [
                      forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                      Term TyName Name DefaultUni DefaultFun ()
pExp
                      ]
  Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify2 Term TyName Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp

-- integerToByteString True 0 (multiplyInteger p 256) = appendByteString
-- (integerToByteString True 0 p) (singleton 0)
i2bProperty5 :: PropertyT IO ()
i2bProperty5 :: PropertyT IO ()
i2bProperty5 = do
  Integer
p <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genP
  let pExp :: Term TyName Name DefaultUni DefaultFun ()
pExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
p
                ]
  let pTimesExp :: Term TyName Name DefaultUni DefaultFun ()
pTimesExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.MultiplyInteger) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
p,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
256
                    ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                    Term TyName Name DefaultUni DefaultFun ()
pTimesExp
                    ]
  let expectedExp :: Term TyName Name DefaultUni DefaultFun ()
expectedExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AppendByteString) [
                      Term TyName Name DefaultUni DefaultFun ()
pExp,
                      forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
"\NUL"
                      ]
  Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify2 Term TyName Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp

-- integerToByteString False 0 (plusInteger (multiplyInteger q 256) r) =
-- appendByteString (integerToByteString False 0 r) (integerToByteString False 0 q)
i2bProperty6 :: PropertyT IO ()
i2bProperty6 :: PropertyT IO ()
i2bProperty6 = do
  Integer
q <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genQ
  Integer
r <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genR
  let qTimesExp :: Term TyName Name DefaultUni DefaultFun ()
qTimesExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.MultiplyInteger) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
256
                    ]
  let largeNumberExp :: Term TyName Name DefaultUni DefaultFun ()
largeNumberExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AddInteger) [
                          Term TyName Name DefaultUni DefaultFun ()
qTimesExp,
                          forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
r
                          ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                    Term TyName Name DefaultUni DefaultFun ()
largeNumberExp
                    ]
  let rBSExp :: Term TyName Name DefaultUni DefaultFun ()
rBSExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
r
                  ]
  let qBSExp :: Term TyName Name DefaultUni DefaultFun ()
qBSExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q
                  ]
  let expectedExp :: Term TyName Name DefaultUni DefaultFun ()
expectedExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AppendByteString) [
                      Term TyName Name DefaultUni DefaultFun ()
rBSExp,
                      Term TyName Name DefaultUni DefaultFun ()
qBSExp
                      ]
  Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify2 Term TyName Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp

-- integerToByteString True 0 (plusInteger (multiplyInteger q 256) r) =
-- appendByteString (integerToByteString False 0 q)
-- (integerToByteString False 0 r)
i2bProperty7 :: PropertyT IO ()
i2bProperty7 :: PropertyT IO ()
i2bProperty7 = do
  Integer
q <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genQ
  Integer
r <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genR
  let qTimesExp :: Term TyName Name DefaultUni DefaultFun ()
qTimesExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.MultiplyInteger) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
256
                    ]
  let largeNumberExp :: Term TyName Name DefaultUni DefaultFun ()
largeNumberExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AddInteger) [
                          Term TyName Name DefaultUni DefaultFun ()
qTimesExp,
                          forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
r
                          ]
  let rBSExp :: Term TyName Name DefaultUni DefaultFun ()
rBSExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
r
                  ]
  let qBSExp :: Term TyName Name DefaultUni DefaultFun ()
qBSExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q
                  ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                    forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                    Term TyName Name DefaultUni DefaultFun ()
largeNumberExp
                    ]
  let expectedExp :: Term TyName Name DefaultUni DefaultFun ()
expectedExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.AppendByteString) [
                      Term TyName Name DefaultUni DefaultFun ()
qBSExp,
                      Term TyName Name DefaultUni DefaultFun ()
rBSExp
                      ]
  Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify2 Term TyName Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp

-- byteStringToInteger b (integerToByteString b 0 q) = q
b2iProperty1 :: PropertyT IO ()
b2iProperty1 :: PropertyT IO ()
b2iProperty1 = do
  Bool
b <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  Integer
q <- (Integer -> String) -> Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Integer -> String
forall a. Show a => a -> String
ppShow Gen Integer
genQ
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q
        ]
  let convertedExp :: Term TyName Name DefaultUni DefaultFun ()
convertedExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b,
        Term TyName Name DefaultUni DefaultFun ()
actualExp
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
q) Term TyName Name DefaultUni DefaultFun ()
convertedExp

-- byteStringToInteger b (consByteString w8 emptyByteString) = w8
b2iProperty2 :: PropertyT IO ()
b2iProperty2 :: PropertyT IO ()
b2iProperty2 = do
  Integer
w8 :: Integer <- Word8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word8 -> Integer) -> PropertyT IO Word8 -> PropertyT IO Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word8 -> String) -> Gen Word8 -> PropertyT IO Word8
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Word8 -> String
forall a. Show a => a -> String
ppShow (forall (m :: * -> *) a. (MonadGen m, Enum a, Bounded a) => m a
Gen.enumBounded @_ @Word8)
  Bool
b <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  let consed :: Term TyName Name DefaultUni DefaultFun ()
consed = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ConsByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
w8,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
""
        ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b,
        Term TyName Name DefaultUni DefaultFun ()
consed
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
w8) Term TyName Name DefaultUni DefaultFun ()
actualExp

-- integerToByteString b (lengthOfByteString bs) (byteStringToInteger b bs) = bs
b2iProperty3 :: PropertyT IO ()
b2iProperty3 :: PropertyT IO ()
b2iProperty3 = do
  Bool
b <- (Bool -> String) -> Gen Bool -> PropertyT IO Bool
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith Bool -> String
forall a. Show a => a -> String
ppShow Gen Bool
forall (m :: * -> *). MonadGen m => m Bool
Gen.bool
  ByteString
bs <- (ByteString -> String) -> Gen ByteString -> PropertyT IO ByteString
forall (m :: * -> *) a.
(Monad m, HasCallStack) =>
(a -> String) -> Gen a -> PropertyT m a
forAllWith ByteString -> String
forall a. Show a => a -> String
ppShow (Gen ByteString -> PropertyT IO ByteString)
-> Gen ByteString -> PropertyT IO ByteString
forall a b. (a -> b) -> a -> b
$ Range Int -> Gen ByteString
forall (m :: * -> *). MonadGen m => Range Int -> m ByteString
Gen.bytes (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
17)
  let sized :: Term TyName Name DefaultUni DefaultFun ()
sized = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.LengthOfByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
        ]
  let converted :: Term TyName Name DefaultUni DefaultFun ()
converted = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b,
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs
        ]
  let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
b,
        Term TyName Name DefaultUni DefaultFun ()
sized,
        Term TyName Name DefaultUni DefaultFun ()
converted
        ]
  Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
bs) Term TyName Name DefaultUni DefaultFun ()
actualExp

i2bCipExamples :: [TestTree]
i2bCipExamples :: [TestTree]
i2bCipExamples = [
  -- integerToByteString False 0 (-1) => failure
  String -> Assertion -> TestTree
testCase String
"example 1" (let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (-Integer
1)
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp),
  -- integerToByteString True 0 (-1) => failure
  String -> Assertion -> TestTree
testCase String
"example 2" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (-Integer
1)
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 100 (-1) => failure
  String -> Assertion -> TestTree
testCase String
"example 3" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
100,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () (-Integer
1)
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 0 0 => [ ]
  String -> Assertion -> TestTree
testCase String
"example 4" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                                ]
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
"") Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 0 0 => [ ]
  String -> Assertion -> TestTree
testCase String
"example 5" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                                ]
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
"") Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 5 0 => [ 0x00, 0x00, 0x00, 0x00, 0x00]
  String -> Assertion -> TestTree
testCase String
"example 6" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
5,
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                              ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
"\NUL\NUL\NUL\NUL\NUL"
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 5 0 => [ 0x00, 0x00, 0x00, 0x00, 0x00]
  String -> Assertion -> TestTree
testCase String
"example 7" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
5,
                              forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                              ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
"\NUL\NUL\NUL\NUL\NUL"
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 536870912 0 => failure
  String -> Assertion -> TestTree
testCase String
"example 8" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
536870912,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 536870912 0 => failure
  String -> Assertion -> TestTree
testCase String
"example 9"  (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
536870912,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 1 404 => failure
  String -> Assertion -> TestTree
testCase String
"example 10" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 1 404 => failure
  String -> Assertion -> TestTree
testCase String
"example 11" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                            in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 2 404 => [ 0x94, 0x01 ]
  String -> Assertion -> TestTree
testCase String
"example 12" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x94, Word8
Item ByteString
0x01])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 0 404 => [ 0x94, 0x01 ]
  String -> Assertion -> TestTree
testCase String
"example 13" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x94, Word8
Item ByteString
0x01])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 2 404 => [ 0x01, 0x94 ]
  String -> Assertion -> TestTree
testCase String
"example 14" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
2,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x94])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 0 404 => [ 0x01, 0x94 ]
  String -> Assertion -> TestTree
testCase String
"example 15" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x94])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString False 5 404 => [ 0x94, 0x01, 0x00, 0x00, 0x00 ]
  String -> Assertion -> TestTree
testCase String
"example 16" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
5,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x94, Word8
Item ByteString
0x01, Word8
Item ByteString
0x00, Word8
Item ByteString
0x00, Word8
Item ByteString
0x00])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- integerToByteString True 5 404 => [ 0x00, 0x00, 0x00, 0x01, 0x94 ]
  String -> Assertion -> TestTree
testCase String
"example 17" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
5,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
404
                                ]
                              expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x00, Word8
Item ByteString
0x00, Word8
Item ByteString
0x00, Word8
Item ByteString
0x01, Word8
Item ByteString
0x94])
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp
  ]

-- Unit tests to make sure that `integerToByteString` behaves as expected for
-- inputs close to the maximum size.
i2bLimitTests ::[TestTree]
i2bLimitTests :: [TestTree]
i2bLimitTests =
    let maxAcceptableInput :: Integer
maxAcceptableInput = Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
8Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
Bitwise.maximumOutputLength) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        maxOutput :: ByteString
maxOutput = [Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList (Int -> [Item ByteString] -> [Item ByteString]
forall a. Int -> [a] -> [a]
take (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
Bitwise.maximumOutputLength) ([Item ByteString] -> [Item ByteString])
-> [Item ByteString] -> [Item ByteString]
forall a b. (a -> b) -> a -> b
$ Item ByteString -> [Item ByteString]
forall a. a -> [a]
repeat Item ByteString
0xFF)
        makeTests :: Bool -> [TestTree]
makeTests Bool
endianness =
            let prefix :: String
prefix = if Bool
endianness
                         then String
"Big-endian, "
                         else String
"Little-endian, "
                mkIntegerToByteStringApp :: Integer -> Integer -> term ()
mkIntegerToByteStringApp Integer
width Integer
input =
                    term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.IntegerToByteString) [
                                        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
endianness,
                                        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
width,
                                        forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
input
                                       ]
            in [
             -- integerToByteString 0 maxInput = 0xFF...FF
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"maximum acceptable input, no length specified") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp Integer
0 Integer
maxAcceptableInput
                          expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
maxOutput
                      in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
             -- integerToByteString maxLen maxInput = 0xFF...FF
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"maximum acceptable input, maximum acceptable length argument") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp Integer
Bitwise.maximumOutputLength Integer
maxAcceptableInput
                          expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
maxOutput
                      in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
             -- integerToByteString 0 (maxInput+1) fails
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"input too big, no length specified") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp Integer
0 (Integer
maxAcceptableInput Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
                      in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
             -- integerToByteString maxLen (maxInput+1) fails
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"input too big, maximum acceptable length argument") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp Integer
Bitwise.maximumOutputLength (Integer
maxAcceptableInput Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
                      in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
             -- integerToByteString (maxLen-1) maxInput fails
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"maximum acceptable input, length argument not big enough") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp (Integer
Bitwise.maximumOutputLength Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer
maxAcceptableInput
                      in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp,
             -- integerToByteString _ (maxLen+1) 0 fails, just to make sure that
             -- we can't go beyond the supposed limit
             String -> Assertion -> TestTree
testCase (String
prefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"input zero, length argument over limit") (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
                      let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Integer -> Integer -> Term TyName Name DefaultUni DefaultFun ()
forall {uni :: * -> *} {term :: * -> *} {tyname} {name}.
(Contains uni Bool, Contains uni Integer,
 TermLike term tyname name uni DefaultFun) =>
Integer -> Integer -> term ()
mkIntegerToByteStringApp (Integer
Bitwise.maximumOutputLength Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Integer
0
                      in Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
actualExp
            ]
        in Bool -> [TestTree]
makeTests Bool
True [TestTree] -> [TestTree] -> [TestTree]
forall a. [a] -> [a] -> [a]
++ Bool -> [TestTree]
makeTests Bool
False

b2iCipExamples :: [TestTree]
b2iCipExamples :: [TestTree]
b2iCipExamples = [
  -- byteStringToInteger False emptyByteString => 0
  String -> Assertion -> TestTree
testCase String
"example 1" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
""
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger True emptyByteString => 0
  String -> Assertion -> TestTree
testCase String
"example 2" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                  forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ByteString
""
                                  ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger False (consByteString 0x01 (consByteString 0x01 emptyByteString)) =>
  -- 257
  String -> Assertion -> TestTree
testCase String
"example 3" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x01])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
257
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger True (consByteString 0x01 (consByteString 0x01 emptyByteString)) =>
  -- 257
  String -> Assertion -> TestTree
testCase String
"example 4" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x01])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
257
                            in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger True (consByteString 0x00 (consByteString 0x01 (consByteString 0x01
  -- emptyByteString))) => 257
  String -> Assertion -> TestTree
testCase String
"example 5" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x00, Word8
Item ByteString
0x01, Word8
Item ByteString
0x01])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
257
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger False (consByteString 0x00 (consByteString 0x01 (consByteString 0x01
  -- emptyByteString))) => 65792
  String -> Assertion -> TestTree
testCase String
"example 6" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x00, Word8
Item ByteString
0x01, Word8
Item ByteString
0x01])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
65792
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger False (consByteString 0x01 (consByteString 0x01 (consByteString 0x00
  -- emptyByteString))) => 257
  String -> Assertion -> TestTree
testCase String
"example 7" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x01, Word8
Item ByteString
0x00])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
257
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp,
  -- byteStringToInteger True (consByteString 0x01 (consByteString 0x01 (consByteString 0x00
  -- emptyByteString))) => 65792
  String -> Assertion -> TestTree
testCase String
"example 8" (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$ let actualExp :: Term TyName Name DefaultUni DefaultFun ()
actualExp = Term TyName Name DefaultUni DefaultFun ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ByteStringToInteger) [
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True,
                                forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @ByteString () ([Item ByteString] -> ByteString
forall l. IsList l => [Item l] -> l
fromList [Word8
Item ByteString
0x01, Word8
Item ByteString
0x01, Word8
Item ByteString
0x00])
                                ]
                             expectedExp :: Term Name DefaultUni DefaultFun ()
expectedExp = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
65792
                          in Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expectedExp Term TyName Name DefaultUni DefaultFun ()
actualExp
  ]

-- Generators

-- As per the CIP, p must be positive, and needs to be large enough to reasonably exercise our
-- tests. We choose a maximum size of 17 bytes: this is enough to give meaningful coverage, but not
-- so large as to slow the tests down excessively.
genP :: Gen Integer
genP :: Gen Integer
genP = Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
1 (Integer
256 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
17 :: Int) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

-- Same as above, except 0 is allowed.
genQ :: Gen Integer
genQ :: Gen Integer
genQ = Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
0 (Integer
256 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
17 :: Int) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

genR :: Gen Integer
genR :: Gen Integer
genR = Range Integer -> Gen Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Integer -> Integer -> Range Integer
forall a. a -> a -> Range a
Range.constant Integer
1 Integer
255)

-- Helpers

evaluateAndVerify ::
  UPLC.Term UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  PLC.Term UPLC.TyName UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  PropertyT IO ()
evaluateAndVerify :: Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify Term Name DefaultUni DefaultFun ()
expected Term TyName Name DefaultUni DefaultFun ()
actual =
  case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
actual of
    Left Error DefaultUni DefaultFun ()
x -> Error DefaultUni DefaultFun () -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Error DefaultUni DefaultFun ()
x PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
    Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
res, [Text]
logs) -> case EvaluationResult (Term Name DefaultUni DefaultFun ())
res of
      EvaluationResult (Term Name DefaultUni DefaultFun ())
PLC.EvaluationFailure   -> [Text] -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow [Text]
logs PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
      PLC.EvaluationSuccess Term Name DefaultUni DefaultFun ()
r -> Term Name DefaultUni DefaultFun ()
r Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun () -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Term Name DefaultUni DefaultFun ()
expected

evaluateAndVerify2 ::
  PLC.Term UPLC.TyName UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  PLC.Term UPLC.TyName UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  PropertyT IO ()
evaluateAndVerify2 :: Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> PropertyT IO ()
evaluateAndVerify2 Term TyName Name DefaultUni DefaultFun ()
expected Term TyName Name DefaultUni DefaultFun ()
actual =
  let expectedResult :: Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
expectedResult = BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
expected
      actualResult :: Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
actualResult = BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
actual
    in case (Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
expectedResult, Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
actualResult) of
      (Left Error DefaultUni DefaultFun ()
err, Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
_) -> Error DefaultUni DefaultFun () -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Error DefaultUni DefaultFun ()
err PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
      (Either
  (Error DefaultUni DefaultFun ())
  (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
_, Left Error DefaultUni DefaultFun ()
err) -> Error DefaultUni DefaultFun () -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow Error DefaultUni DefaultFun ()
err PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
      (Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
eRes, [Text]
eLogs), Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
aRes, [Text]
aLogs)) -> case (EvaluationResult (Term Name DefaultUni DefaultFun ())
eRes, EvaluationResult (Term Name DefaultUni DefaultFun ())
aRes) of
        (EvaluationResult (Term Name DefaultUni DefaultFun ())
PLC.EvaluationFailure, EvaluationResult (Term Name DefaultUni DefaultFun ())
_) -> [Text] -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow [Text]
eLogs PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        (EvaluationResult (Term Name DefaultUni DefaultFun ())
_, EvaluationResult (Term Name DefaultUni DefaultFun ())
PLC.EvaluationFailure) -> [Text] -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Show a, HasCallStack) =>
a -> m ()
annotateShow [Text]
aLogs PropertyT IO () -> PropertyT IO () -> PropertyT IO ()
forall a b. PropertyT IO a -> PropertyT IO b -> PropertyT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropertyT IO ()
forall (m :: * -> *) a. (MonadTest m, HasCallStack) => m a
failure
        (PLC.EvaluationSuccess Term Name DefaultUni DefaultFun ()
eResult, PLC.EvaluationSuccess Term Name DefaultUni DefaultFun ()
aResult) -> Term Name DefaultUni DefaultFun ()
eResult Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun () -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Term Name DefaultUni DefaultFun ()
aResult

evaluateShouldFail ::
  PLC.Term UPLC.TyName UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  IO ()
evaluateShouldFail :: Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateShouldFail Term TyName Name DefaultUni DefaultFun ()
expr = case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
expr of
  Left Error DefaultUni DefaultFun ()
_ -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure String
"unexpectedly failed to typecheck"
  Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
result, [Text]
_) -> case EvaluationResult (Term Name DefaultUni DefaultFun ())
result of
    EvaluationResult (Term Name DefaultUni DefaultFun ())
PLC.EvaluationFailure   -> () -> Assertion
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    PLC.EvaluationSuccess Term Name DefaultUni DefaultFun ()
_ -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure String
"should have failed, but didn't"

evaluateAssertEqual ::
  UPLC.Term UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  PLC.Term UPLC.TyName UPLC.Name UPLC.DefaultUni UPLC.DefaultFun () ->
  IO ()
evaluateAssertEqual :: Term Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun () -> Assertion
evaluateAssertEqual Term Name DefaultUni DefaultFun ()
expected Term TyName Name DefaultUni DefaultFun ()
actual =
  case BuiltinSemanticsVariant DefaultFun
-> CostingPart DefaultUni DefaultFun
-> Term TyName Name DefaultUni DefaultFun ()
-> Either
     (Error DefaultUni DefaultFun ())
     (EvaluationResult (Term Name DefaultUni DefaultFun ()), [Text])
forall (uni :: * -> *) fun (m :: * -> *).
(MonadError (Error uni fun ()) m, Typecheckable uni fun, GEq uni,
 Everywhere uni ExMemoryUsage, PrettyUni uni, Pretty fun) =>
BuiltinSemanticsVariant fun
-> CostingPart uni fun
-> Term TyName Name uni fun ()
-> m (EvaluationResult (Term Name uni fun ()), [Text])
typecheckEvaluateCek BuiltinSemanticsVariant DefaultFun
forall a. Default a => a
def BuiltinCostModel
CostingPart DefaultUni DefaultFun
defaultBuiltinCostModelForTesting Term TyName Name DefaultUni DefaultFun ()
actual of
    Left Error DefaultUni DefaultFun ()
_ -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure String
"unexpectedly failed to typecheck"
    Right (EvaluationResult (Term Name DefaultUni DefaultFun ())
result, [Text]
_) -> case EvaluationResult (Term Name DefaultUni DefaultFun ())
result of
      EvaluationResult (Term Name DefaultUni DefaultFun ())
PLC.EvaluationFailure   -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure String
"unexpectedly failed to evaluate"
      PLC.EvaluationSuccess Term Name DefaultUni DefaultFun ()
x -> String
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Assertion
forall a.
(Eq a, Show a, HasCallStack) =>
String -> a -> a -> Assertion
assertEqual String
"" Term Name DefaultUni DefaultFun ()
x Term Name DefaultUni DefaultFun ()
expected