-- editorconfig-checker-disable-file
-- | Sample generators used for tests.

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TypeApplications  #-}

module PlutusCore.Generators.Hedgehog.Interesting
    ( TermGen
    , TermOf(..)
    , genOverapplication
    , factorial
    , genFactorial
    , naiveFib
    , genNaiveFib
    , genNatRoundtrip
    , natSum
    , genScottListSum
    , genIfIntegers
    , fromInterestingTermGens
    ) where

import PlutusCore.Generators.Hedgehog.Denotation
import PlutusCore.Generators.Hedgehog.Entity
import PlutusCore.Generators.Hedgehog.TypedBuiltinGen

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Evaluation.Result
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Quote

import PlutusCore.StdLib.Data.Bool
import PlutusCore.StdLib.Data.Function as Function
import PlutusCore.StdLib.Data.Nat
import PlutusCore.StdLib.Data.ScottList as ScottList
import PlutusCore.StdLib.Data.Unit
import PlutusCore.StdLib.Meta
import PlutusCore.StdLib.Type

import Data.List (genericIndex)
import Hedgehog hiding (Size, Var)
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Type.Reflection

-- | The type of terms-and-their-values generators.
type TermGen a = Gen (TermOf (Term TyName Name DefaultUni DefaultFun ()) a)

-- | Generates application of a builtin that returns a function, immediately saturated afterwards.
--
-- > ifThenElse {integer -> integer -> integer} (lessThanInteger i j) addInteger subtractInteger i j
-- >     == if i < j then i + j else i - j
genOverapplication :: TermGen Integer
genOverapplication :: TermGen Integer
genOverapplication = do
    let typedInteger :: TypeRep Integer
typedInteger = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        integer :: Type TyName DefaultUni ()
integer = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInteger
    TermOf Term TyName Name DefaultUni DefaultFun ()
ti Integer
i <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef TypeRep Integer
typedInteger
    TermOf Term TyName Name DefaultUni DefaultFun ()
tj Integer
j <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef TypeRep Integer
typedInteger
    let term :: Term TyName Name DefaultUni DefaultFun ()
term =
            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
                (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
IfThenElse) (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
integer (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
integer Type TyName DefaultUni ()
integer)
                [ 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
LessThanInteger) [Term TyName Name DefaultUni DefaultFun ()
ti, Term TyName Name DefaultUni DefaultFun ()
tj]
                , () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger
                , () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger
                , Term TyName Name DefaultUni DefaultFun ()
ti
                , Term TyName Name DefaultUni DefaultFun ()
tj
                ]
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> (Integer
    -> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer)
-> Integer
-> TermGen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term (Integer -> TermGen Integer) -> Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
j then Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
j else Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j

-- | @\i -> product [1 :: Integer .. i]@ as a PLC term.
--
-- > \(i : integer) -> product (enumFromTo 1 i)
factorial :: Term TyName Name DefaultUni DefaultFun ()
factorial :: Term TyName Name DefaultUni DefaultFun ()
factorial = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
i <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i"
    let int :: Type tyname DefaultUni ()
int = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
i Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int
        (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Integer) =>
term ()
ScottList.product
        (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ 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 Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Integer, HasTypeAndTermLevel uni (),
 HasTypeAndTermLevel uni Bool) =>
term ()
ScottList.enumFromTo
            [ 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
            , () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i
            ]

-- | The naive exponential fibonacci function as a PLC term.
--
-- > \(i0 : integer) ->
-- >     fix {integer} {integer}
-- >         (\(rec : integer -> integer) (i : integer) ->
-- >                 ifThenElse {integer}
-- >                     (lessThanEqInteger i 1)
-- >                     (\(u : unit) -> i)
-- >                     (\(u : unit) -> addInteger
-- >                         (rec (subtractInteger i 1))
-- >                         (rec (subtractInteger i 2)))
-- >         i0
naiveFib :: Integer -> Term TyName Name DefaultUni DefaultFun ()
naiveFib :: Integer -> Term TyName Name DefaultUni DefaultFun ()
naiveFib Integer
iv = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    Name
i0  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i0"
    Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Name
i   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i"
    Name
u   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"u"
    let
      intS :: Type tyname DefaultUni ()
intS = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
      fib :: Term TyName Name DefaultUni DefaultFun ()
fib = ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
i0 Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS
        (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ 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 (Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS, Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS])
            [   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
rec (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS)
              (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
i Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS
              (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ 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 (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Bool, HasTypeAndTermLevel uni ()) =>
term ()
ifThenElse Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
intS)
                  [ 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
LessThanEqualsInteger)
                      [() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i, 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]
                  , ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
u Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i
                  , ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
u Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger)
                      [ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
rec) (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger)
                          [() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i, 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]
                      , ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
rec) (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
SubtractInteger)
                          [() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i, 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]
                      ]
                  ]
            , () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
i0
            ]
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
fib (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> 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
iv

-- | Generate a term that computes the factorial of an @integer@ and return it
-- along with the factorial of the corresponding 'Integer' computed on the Haskell side.
genFactorial :: TermGen Integer
genFactorial :: TermGen Integer
genFactorial = do
    let m :: Integer
m = Integer
10
    Integer
iv <- Range Integer -> GenT Identity Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> GenT Identity Integer)
-> Range Integer -> GenT Identity Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
1 Integer
m
    let term :: Term TyName Name DefaultUni DefaultFun ()
term = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () Term TyName Name DefaultUni DefaultFun ()
factorial (forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
iv)
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> (Integer
    -> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer)
-> Integer
-> TermGen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term (Integer -> TermGen Integer) -> Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.product [Integer
1..Integer
iv]

-- | Generate a term that computes the ith Fibonacci number and return it
-- along with the corresponding 'Integer' computed on the Haskell side.
genNaiveFib :: TermGen Integer
genNaiveFib :: TermGen Integer
genNaiveFib = do
    let fibs :: [Integer]
fibs = (Integer -> Integer -> Integer)
-> Integer -> [Integer] -> [Integer]
forall b a. (b -> a -> b) -> b -> [a] -> [b]
scanl Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Integer
0 ([Integer] -> [Integer]) -> [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
fibs
        m :: Integer
m = Integer
16
    Integer
iv <- Range Integer -> GenT Identity Integer
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Integer -> GenT Identity Integer)
-> Range Integer -> GenT Identity Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Range Integer
forall a. Integral a => a -> a -> Range a
Range.linear Integer
0 Integer
m
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> (Integer
    -> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer)
-> Integer
-> TermGen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf (Integer -> Term TyName Name DefaultUni DefaultFun ()
naiveFib Integer
iv) (Integer -> TermGen Integer) -> Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ [Integer]
fibs [Integer] -> Integer -> Integer
forall i a. Integral i => [a] -> i -> a
`genericIndex` Integer
iv

-- | Generate an 'Integer', turn it into a Scott-encoded PLC @Nat@ (see 'Nat'),
-- turn that @Nat@ into the corresponding PLC @integer@ using a fold (see 'FoldNat')
-- defined in terms of generic fix (see 'Fix') and return the result
-- along with the original 'Integer'
genNatRoundtrip :: TermGen Integer
genNatRoundtrip :: TermGen Integer
genNatRoundtrip = do
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
    TermOf Term TyName Name DefaultUni DefaultFun ()
_ Integer
iv <- (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> Bool)
-> TermGen Integer -> TermGen Integer
forall (m :: * -> *) a.
(MonadGen m, GenBase m ~ Identity) =>
(a -> Bool) -> m a -> m a
Gen.filter ((Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Integer -> Bool)
-> (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
    -> Integer)
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> Integer
forall term a. TermOf term a -> a
_termOfValue) (TermGen Integer -> TermGen Integer)
-> TermGen Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$
        forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef @(Term TyName Name DefaultUni DefaultFun ()) TypeRep Integer
typedInt
    let term :: Term TyName Name DefaultUni DefaultFun ()
term = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Integer) =>
term ()
natToInteger (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ Integer -> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
iv
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term Integer
iv

-- | @sumNat@ as a PLC term.
natSum :: Term TyName Name DefaultUni DefaultFun ()
natSum :: Term TyName Name DefaultUni DefaultFun ()
natSum = Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name DefaultUni DefaultFun ())
 -> Term TyName Name DefaultUni DefaultFun ())
-> Quote (Term TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ do
    let int :: Type tyname DefaultUni ()
int = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
        nat :: Type TyName uni ()
nat = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
natData
        add :: Term tyname name uni DefaultFun ()
add = () -> DefaultFun -> Term tyname name uni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger
    Name
acc <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"acc"
    Name
n <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"n"
    Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Term TyName Name DefaultUni DefaultFun ()
 -> Quote (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> Quote (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ 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 (Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldList [Type TyName DefaultUni ()
forall {uni :: * -> *}. Type TyName uni ()
nat, Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int])
          [   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
acc Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int
            (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> ([Term TyName Name DefaultUni DefaultFun ()]
    -> Term TyName Name DefaultUni DefaultFun ())
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
n Type TyName DefaultUni ()
forall {uni :: * -> *}. Type TyName uni ()
nat
            (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> ([Term TyName Name DefaultUni DefaultFun ()]
    -> Term TyName Name DefaultUni DefaultFun ())
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Term TyName Name DefaultUni DefaultFun ()
forall {tyname} {name} {uni :: * -> *}.
Term tyname name uni DefaultFun ()
add
            ([Term TyName Name DefaultUni DefaultFun ()]
 -> Term TyName Name DefaultUni DefaultFun ())
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ [ () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
acc
              , 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 Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Integer) =>
term ()
natToInteger [ () -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
n ]
              ]
          , 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
          ]

-- | Generate a list of 'Integer's, turn it into a Scott-encoded PLC @List@ (see 'List'),
-- sum elements of the list (see 'Sum') and return it along with the sum of the original list.
genScottListSum :: TermGen Integer
genScottListSum :: TermGen Integer
genScottListSum = do
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        intS :: Type TyName DefaultUni ()
intS = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInt
    [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
ps <- Range Int
-> TermGen Integer
-> GenT
     Identity
     [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 Int
10) (TermGen Integer
 -> GenT
      Identity
      [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer])
-> TermGen Integer
-> GenT
     Identity
     [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
forall a b. (a -> b) -> a -> b
$ TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall term (m :: * -> *).
(HasConstantIn DefaultUni term, Monad m) =>
TypedBuiltinGenT term m
genTypedBuiltinDef TypeRep Integer
typedInt
    let list :: Term TyName Name DefaultUni DefaultFun ()
list = Type TyName DefaultUni ()
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Type TyName uni () -> [term ()] -> term ()
metaListToScottList Type TyName DefaultUni ()
intS ([Term TyName Name DefaultUni DefaultFun ()]
 -> Term TyName Name DefaultUni DefaultFun ())
-> [Term TyName Name DefaultUni DefaultFun ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> Term TyName Name DefaultUni DefaultFun ())
-> [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
-> [Term TyName Name DefaultUni DefaultFun ()]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> Term TyName Name DefaultUni DefaultFun ()
forall term a. TermOf term a -> term
_termOfTerm [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
ps
        term :: Term TyName Name DefaultUni DefaultFun ()
term = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Integer) =>
term ()
ScottList.sum Term TyName Name DefaultUni DefaultFun ()
list
    let haskSum :: Integer
haskSum = [Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
Prelude.sum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> Integer)
-> [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
-> [Integer]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> Integer
forall term a. TermOf term a -> a
_termOfValue [TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer]
ps
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term Integer
haskSum

-- | Generate a @boolean@ and two @integer@s and check whether @if b then i1 else i2@
-- means the same thing in Haskell and PLC. Terms are generated using 'genTermLoose'.
genIfIntegers :: TermGen Integer
genIfIntegers :: TermGen Integer
genIfIntegers = do
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        int :: Type TyName DefaultUni ()
int = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
b Bool
bv <- TypeRep Bool
-> GenT
     Identity (TermOf (Term TyName Name DefaultUni DefaultFun ()) Bool)
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Bool
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
    TermOf Term TyName Name DefaultUni DefaultFun ()
i Integer
iv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
j Integer
jv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    let instConst :: Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
instConst = ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (Term TyName Name DefaultUni fun ()
 -> Term TyName Name DefaultUni fun ()
 -> Term TyName Name DefaultUni fun ())
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni fun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Function.const [Type TyName DefaultUni ()
int, Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit]
        value :: Integer
value = if Bool
bv then Integer
iv else Integer
jv
        term :: Term TyName Name DefaultUni DefaultFun ()
term =
            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
                (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun,
 HasTypeAndTermLevel uni Bool, HasTypeAndTermLevel uni ()) =>
term ()
ifThenElse Type TyName DefaultUni ()
int)
                [Term TyName Name DefaultUni DefaultFun ()
b, Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall {fun}.
Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
instConst Term TyName Name DefaultUni DefaultFun ()
i, Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall {fun}.
Term TyName Name DefaultUni fun ()
-> Term TyName Name DefaultUni fun ()
instConst Term TyName Name DefaultUni DefaultFun ()
j]
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term Integer
value

-- | Check that builtins can be partially applied.
genApplyAdd1 :: TermGen Integer
genApplyAdd1 :: TermGen Integer
genApplyAdd1 = do
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        int :: Type TyName DefaultUni ()
int = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
i Integer
iv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
j Integer
jv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    let term :: Term TyName Name DefaultUni DefaultFun ()
term =
            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 (Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
applyFun [Type TyName DefaultUni ()
int, Type TyName DefaultUni ()
int])
                [ ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger) Term TyName Name DefaultUni DefaultFun ()
i
                , Term TyName Name DefaultUni DefaultFun ()
j
                ]
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> (Integer
    -> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer)
-> Integer
-> TermGen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term (Integer -> TermGen Integer) -> Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ Integer
iv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
jv

-- | Check that builtins can be partially applied.
genApplyAdd2 :: TermGen Integer
genApplyAdd2 :: TermGen Integer
genApplyAdd2 = do
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        int :: Type TyName DefaultUni ()
int = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
i Integer
iv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
j Integer
jv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    let term :: Term TyName Name DefaultUni DefaultFun ()
term =
            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 (Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
applyFun [Type TyName DefaultUni ()
int, ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
int Type TyName DefaultUni ()
int])
                [ () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
AddInteger
                , Term TyName Name DefaultUni DefaultFun ()
i
                , Term TyName Name DefaultUni DefaultFun ()
j
                ]
    TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
-> TermGen Integer
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
 -> TermGen Integer)
-> (Integer
    -> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer)
-> Integer
-> TermGen Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term TyName Name DefaultUni DefaultFun ()
-> Integer
-> TermOf (Term TyName Name DefaultUni DefaultFun ()) Integer
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term (Integer -> TermGen Integer) -> Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ Integer
iv Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
jv

-- | Check that division by zero results in 'Error'.
genDivideByZero :: TermGen (BuiltinResult Integer)
genDivideByZero :: TermGen (BuiltinResult Integer)
genDivideByZero = do
    DefaultFun
op <- [DefaultFun] -> GenT Identity DefaultFun
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [DefaultFun
DivideInteger, DefaultFun
QuotientInteger, DefaultFun
ModInteger, DefaultFun
RemainderInteger]
    TermOf Term TyName Name DefaultUni DefaultFun ()
i Integer
_ <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose (TypeRep Integer -> TermGen Integer)
-> TypeRep Integer -> TermGen Integer
forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Integer
    let term :: Term TyName Name DefaultUni DefaultFun ()
term = 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
op) [Term TyName Name DefaultUni DefaultFun ()
i, 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]
    TermOf
  (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
-> TermGen (BuiltinResult Integer)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf
   (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
 -> TermGen (BuiltinResult Integer))
-> TermOf
     (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
-> TermGen (BuiltinResult Integer)
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> BuiltinResult Integer
-> TermOf
     (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term BuiltinResult Integer
forall err. AsEvaluationFailure err => err
evaluationFailure

-- | Check that division by zero results in 'Error' even if a function doesn't use that argument.
genDivideByZeroDrop :: TermGen (BuiltinResult Integer)
genDivideByZeroDrop :: TermGen (BuiltinResult Integer)
genDivideByZeroDrop = do
    DefaultFun
op <- [DefaultFun] -> GenT Identity DefaultFun
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element [DefaultFun
DivideInteger, DefaultFun
QuotientInteger, DefaultFun
ModInteger, DefaultFun
RemainderInteger]
    let typedInt :: TypeRep Integer
typedInt = TypeRep Integer
forall {k} (a :: k). Typeable a => TypeRep a
typeRep
        int :: Type TyName DefaultUni ()
int = TypeRep Integer -> Type TyName DefaultUni ()
forall a tyname (uni :: * -> *) (x :: a) (proxy :: a -> *).
KnownTypeAst tyname uni x =>
proxy x -> Type tyname uni ()
toTypeAst TypeRep Integer
typedInt
    TermOf Term TyName Name DefaultUni DefaultFun ()
i Integer
iv <- TypeRep Integer -> TermGen Integer
TypedBuiltinGenT
  (Term TyName Name DefaultUni DefaultFun ()) Identity
forall (m :: * -> *).
Monad m =>
TypedBuiltinGenT (Term TyName Name DefaultUni DefaultFun ()) m
genTermLoose TypeRep Integer
typedInt
    let term :: Term TyName Name DefaultUni DefaultFun ()
term =
            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 (Term TyName Name DefaultUni DefaultFun ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Function.const [Type TyName DefaultUni ()
int, Type TyName DefaultUni ()
int])
                [ forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
iv
                , 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 tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
op) [Term TyName Name DefaultUni DefaultFun ()
i, 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]
                ]
    TermOf
  (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
-> TermGen (BuiltinResult Integer)
forall a. a -> GenT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TermOf
   (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
 -> TermGen (BuiltinResult Integer))
-> TermOf
     (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
-> TermGen (BuiltinResult Integer)
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun ()
-> BuiltinResult Integer
-> TermOf
     (Term TyName Name DefaultUni DefaultFun ()) (BuiltinResult Integer)
forall term a. term -> a -> TermOf term a
TermOf Term TyName Name DefaultUni DefaultFun ()
term BuiltinResult Integer
forall err. AsEvaluationFailure err => err
evaluationFailure

-- | Apply a function to all interesting generators and collect the results.
fromInterestingTermGens
    :: (forall a. KnownType (Term TyName Name DefaultUni DefaultFun ()) a => String -> TermGen a -> c)
    -> [c]
fromInterestingTermGens :: forall c.
(forall a.
 KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
 String -> TermGen a -> c)
-> [c]
fromInterestingTermGens forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f =
    [ String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"overapplication"  TermGen Integer
genOverapplication
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"factorial"        TermGen Integer
genFactorial
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"fibonacci"        TermGen Integer
genNaiveFib
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"NatRoundTrip"     TermGen Integer
genNatRoundtrip
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"ScottListSum"     TermGen Integer
genScottListSum
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"IfIntegers"       TermGen Integer
genIfIntegers
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"ApplyAdd1"        TermGen Integer
genApplyAdd1
    , String -> TermGen Integer -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"ApplyAdd2"        TermGen Integer
genApplyAdd2
    , String -> TermGen (BuiltinResult Integer) -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"DivideByZero"     TermGen (BuiltinResult Integer)
genDivideByZero
    , String -> TermGen (BuiltinResult Integer) -> c
forall a.
KnownType (Term TyName Name DefaultUni DefaultFun ()) a =>
String -> TermGen a -> c
f String
"DivideByZeroDrop" TermGen (BuiltinResult Integer)
genDivideByZeroDrop
    ]