{-# 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
type TermGen a = Gen (TermOf (Term TyName Name DefaultUni DefaultFun ()) a)
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
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
]
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
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]
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
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
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
]
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
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
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
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
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
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
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
]