{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Test.IOTasks.Internal.SpecificationGenerator (specGen, shrinkSpec, loopBodyGen) where

import Test.IOTasks.Internal.OutputPattern
import Test.IOTasks.Term
import Test.IOTasks.Term.Prelude
import Test.IOTasks.ValueSet
import Test.IOTasks.Var
import {-# SOURCE #-} Test.IOTasks.Internal.Specification

import Test.QuickCheck
import Type.Reflection

instance Show Specification where
  show :: Specification -> String
show = (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n--\n") ShowS -> (Specification -> String) -> Specification -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String)
-> (Specification -> Doc) -> Specification -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Specification -> Doc
pPrintSpecification

specGen :: Gen Specification
specGen :: Gen Specification
specGen = Gen Specification
simpleSpec

shrinkSpec :: Specification -> [Specification]
shrinkSpec :: Specification -> [Specification]
shrinkSpec ReadInput{} = []
shrinkSpec (WriteOutput OptFlag
_ Set (OutputPattern k)
_ Specification
s) = [Specification
s]
shrinkSpec (Branch Term 'Transparent Bool
c Specification
s1 Specification
s2 Specification
s) = [Specification
s1, Specification
s2, Specification
s, Term 'Transparent Bool
-> Specification -> Specification -> Specification -> Specification
Branch Term 'Transparent Bool
c Specification
s1 Specification
s2 Specification
nop]
shrinkSpec Specification
Nop = []
shrinkSpec Specification
E = []
shrinkSpec (TillE Specification
s Specification
s') = [Specification -> Specification
dropE Specification
s, Specification
s']
  where
    dropE :: Specification -> Specification
    dropE :: Specification -> Specification
dropE (ReadInput Var a
x ValueSet a
ty InputMode
m Specification
s') = Var a -> ValueSet a -> InputMode -> Specification -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification -> Specification
ReadInput Var a
x ValueSet a
ty InputMode
m (Specification -> Specification
dropE Specification
s')
    dropE (WriteOutput OptFlag
opt Set (OutputPattern k)
os Specification
s') = OptFlag -> Set (OutputPattern k) -> Specification -> Specification
forall (k :: PatternKind).
OptFlag -> Set (OutputPattern k) -> Specification -> Specification
WriteOutput OptFlag
opt Set (OutputPattern k)
os (Specification -> Specification
dropE Specification
s')
    dropE (Branch Term 'Transparent Bool
c Specification
s1 Specification
s2 Specification
s') = Term 'Transparent Bool
-> Specification -> Specification -> Specification -> Specification
Branch Term 'Transparent Bool
c (Specification -> Specification
dropE Specification
s1) (Specification -> Specification
dropE Specification
s2) (Specification -> Specification
dropE Specification
s')
    dropE Specification
Nop = Specification
Nop
    dropE (TillE Specification
s Specification
s') = Specification -> Specification -> Specification
TillE Specification
s (Specification -> Specification
dropE Specification
s')
    dropE Specification
E = Specification
Nop

-- generator for simple specifications
simpleSpec :: Gen Specification
simpleSpec :: Gen Specification
simpleSpec = do
  Specification
i <- [(Var Integer, ValueSet Integer, InputMode)] -> Gen Specification
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)] -> Gen Specification
input [(String -> Var Integer
intVar String
"n",ValueSet Integer
ints,InputMode
AssumeValid)]
  Specification
l <- [(Var Integer, ValueSet Integer, InputMode)]
-> Gen Condition -> Gen Specification
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
loop [(String -> Var Integer
intVar String
"xs",ValueSet Integer
ints,InputMode
AssumeValid)] ([(Var Integer, ValueSet Integer)] -> [Var Integer] -> Gen Condition
progressCondition [(String -> Var Integer
intVar String
"xs",ValueSet Integer
ints)] [String -> Var Integer
intVar String
"n"])
  Specification
p <- Gen (Term Any Integer) -> Gen Specification
forall a (k :: TermKind).
(Typeable a, Show a) =>
Gen (Term k a) -> Gen Specification
outputOneof ([Var Integer] -> [Var Integer] -> Gen (Term Any Integer)
forall (k :: TermKind).
[Var Integer] -> [Var Integer] -> Gen (Term k Integer)
intTerm [String -> Var Integer
intVar String
"xs", String -> Var Integer
intVar String
"y"] [String -> Var Integer
intVar String
"n"])
  Specification -> Gen Specification
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification -> Gen Specification)
-> Specification -> Gen Specification
forall a b. (a -> b) -> a -> b
$ Specification
i Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
l Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> Specification
p

-- generator for standalone loop bodies
loopBodyGen :: Gen (Specification,Specification)
loopBodyGen :: Gen (Specification, Specification)
loopBodyGen = do
  Specification
s <- [(Var Integer, ValueSet Integer, InputMode)]
-> Gen Condition -> Gen Specification
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
loopBody [(String -> Var Integer
intVar String
"xs",ValueSet Integer
ints,InputMode
AssumeValid)] ([(Var Integer, ValueSet Integer)] -> [Var Integer] -> Gen Condition
progressCondition [(String -> Var Integer
intVar String
"xs",ValueSet Integer
ints)] [String -> Var Integer
intVar String
"n"])
  (Specification, Specification)
-> Gen (Specification, Specification)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Specification
s, Var Integer -> ValueSet Integer -> InputMode -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput (String -> Var Integer
intVar String
"n") ValueSet Integer
nats InputMode
AssumeValid)

-- basic generators
input :: (Typeable a,Read a, Show a) => [(Var a,ValueSet a,InputMode)] -> Gen Specification
input :: forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)] -> Gen Specification
input [(Var a, ValueSet a, InputMode)]
xs = do
  (Var a
x,ValueSet a
vs,InputMode
m) <- [(Var a, ValueSet a, InputMode)]
-> Gen (Var a, ValueSet a, InputMode)
forall a. [a] -> Gen a
elements [(Var a, ValueSet a, InputMode)]
xs
  Specification -> Gen Specification
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification -> Gen Specification)
-> Specification -> Gen Specification
forall a b. (a -> b) -> a -> b
$ Var a -> ValueSet a -> InputMode -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput Var a
x ValueSet a
vs InputMode
m

someInputsWithHole ::  (Typeable a,Read a, Show a) =>  [(Var a,ValueSet a,InputMode)] -> Int -> Gen (Specification -> Specification)
someInputsWithHole :: forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Int -> Gen (Specification -> Specification)
someInputsWithHole [(Var a, ValueSet a, InputMode)]
xs Int
nMax = do
  Int
n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1,Int
nMax)
  Int
p <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
  ([Specification]
is1,[Specification]
is2) <- Int -> [Specification] -> ([Specification], [Specification])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
p ([Specification] -> ([Specification], [Specification]))
-> Gen [Specification] -> Gen ([Specification], [Specification])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Specification -> Gen [Specification]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n ([(Var a, ValueSet a, InputMode)] -> Gen Specification
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)] -> Gen Specification
input [(Var a, ValueSet a, InputMode)]
xs)
  (Specification -> Specification)
-> Gen (Specification -> Specification)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Specification -> Specification)
 -> Gen (Specification -> Specification))
-> (Specification -> Specification)
-> Gen (Specification -> Specification)
forall a b. (a -> b) -> a -> b
$ \Specification
s -> [Specification] -> Specification
forall a. Monoid a => [a] -> a
mconcat ([Specification] -> Specification)
-> [Specification] -> Specification
forall a b. (a -> b) -> a -> b
$ [Specification]
is1 [Specification] -> [Specification] -> [Specification]
forall a. [a] -> [a] -> [a]
++ [Specification
s] [Specification] -> [Specification] -> [Specification]
forall a. [a] -> [a] -> [a]
++ [Specification]
is2

outputOneof :: (Typeable a, Show a) => Gen (Term k a) -> Gen Specification
outputOneof :: forall a (k :: TermKind).
(Typeable a, Show a) =>
Gen (Term k a) -> Gen Specification
outputOneof = Bool -> Gen (Term k a) -> Gen Specification
forall a (k :: TermKind).
(Typeable a, Show a) =>
Bool -> Gen (Term k a) -> Gen Specification
outputOneof' Bool
False

_optionalOutputOneof :: (Typeable a, Show a) => Gen (Term k a) -> Gen Specification
_optionalOutputOneof :: forall a (k :: TermKind).
(Typeable a, Show a) =>
Gen (Term k a) -> Gen Specification
_optionalOutputOneof = Bool -> Gen (Term k a) -> Gen Specification
forall a (k :: TermKind).
(Typeable a, Show a) =>
Bool -> Gen (Term k a) -> Gen Specification
outputOneof' Bool
True

outputOneof' :: (Typeable a, Show a) => Bool -> Gen (Term k a) -> Gen Specification
outputOneof' :: forall a (k :: TermKind).
(Typeable a, Show a) =>
Bool -> Gen (Term k a) -> Gen Specification
outputOneof' Bool
b Gen (Term k a)
ts = do
  Term k a
t <- Gen (Term k a)
ts
  Specification -> Gen Specification
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification -> Gen Specification)
-> Specification -> Gen Specification
forall a b. (a -> b) -> a -> b
$ (if Bool
b then [OutputPattern 'SpecificationP] -> Specification
forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOptionalOutput else [OutputPattern 'SpecificationP] -> Specification
forall (k :: PatternKind). [OutputPattern k] -> Specification
writeOutput) [Term k a -> OutputPattern 'SpecificationP
forall a (tk :: TermKind).
(Typeable a, Show a) =>
Term tk a -> OutputPattern 'SpecificationP
resultOf Term k a
t]

-- branch free sequence of inputs and outputs
_linearSpec ::[(Var Integer,ValueSet Integer,InputMode)] -> [(Var Integer,ValueSet Integer,InputMode)] -> Gen (Specification, [SomeVar])
_linearSpec :: [(Var Integer, ValueSet Integer, InputMode)]
-> [(Var Integer, ValueSet Integer, InputMode)]
-> Gen (Specification, [SomeVar])
_linearSpec [(Var Integer, ValueSet Integer, InputMode)]
lists [(Var Integer, ValueSet Integer, InputMode)]
xs = (Int -> Gen (Specification, [SomeVar]))
-> Gen (Specification, [SomeVar])
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Specification, [SomeVar]))
 -> Gen (Specification, [SomeVar]))
-> (Int -> Gen (Specification, [SomeVar]))
-> Gen (Specification, [SomeVar])
forall a b. (a -> b) -> a -> b
$ \Int
n -> do
  Specification
is <- ((Specification -> Specification) -> Specification -> Specification
forall a b. (a -> b) -> a -> b
$ Specification
nop) ((Specification -> Specification) -> Specification)
-> Gen (Specification -> Specification) -> Gen Specification
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var Integer, ValueSet Integer, InputMode)]
-> Int -> Gen (Specification -> Specification)
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Int -> Gen (Specification -> Specification)
someInputsWithHole ([(Var Integer, ValueSet Integer, InputMode)]
lists [(Var Integer, ValueSet Integer, InputMode)]
-> [(Var Integer, ValueSet Integer, InputMode)]
-> [(Var Integer, ValueSet Integer, InputMode)]
forall a. [a] -> [a] -> [a]
++ [(Var Integer, ValueSet Integer, InputMode)]
xs) (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)
  let vs :: [Var Integer]
vs = forall a. Typeable a => [SomeVar] -> [Var a]
filterType @Integer ([SomeVar] -> [Var Integer]) -> [SomeVar] -> [Var Integer]
forall a b. (a -> b) -> a -> b
$ Specification -> [SomeVar]
readVars Specification
is
  [Specification]
os <- Int -> Gen [Specification] -> Gen [Specification]
forall a. Int -> Gen a -> Gen a
resize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) (Gen [Specification] -> Gen [Specification])
-> Gen [Specification] -> Gen [Specification]
forall a b. (a -> b) -> a -> b
$ Gen Specification -> Gen [Specification]
forall a. Gen a -> Gen [a]
listOf1 (Gen Specification -> Gen [Specification])
-> Gen Specification -> Gen [Specification]
forall a b. (a -> b) -> a -> b
$ Gen (Term Any Integer) -> Gen Specification
forall a (k :: TermKind).
(Typeable a, Show a) =>
Gen (Term k a) -> Gen Specification
outputOneof ([Var Integer] -> [Var Integer] -> Gen (Term Any Integer)
forall (k :: TermKind).
[Var Integer] -> [Var Integer] -> Gen (Term k Integer)
intTerm [Var Integer]
vs [Var Integer]
vs)
  let spec :: Specification
spec = Specification
is Specification -> Specification -> Specification
forall a. Semigroup a => a -> a -> a
<> [Specification] -> Specification
forall a. Monoid a => [a] -> a
mconcat [Specification]
os
  (Specification, [SomeVar]) -> Gen (Specification, [SomeVar])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Specification
spec,Specification -> [SomeVar]
readVars Specification
spec)

-- simple loop
loop :: (Typeable a,Read a, Show a) => [(Var a,ValueSet a,InputMode)] -> Gen Condition -> Gen Specification
loop :: forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
loop [(Var a, ValueSet a, InputMode)]
xs Gen Condition
loopCondition = Specification -> Specification
tillExit (Specification -> Specification)
-> Gen Specification -> Gen Specification
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
loopBody [(Var a, ValueSet a, InputMode)]
xs Gen Condition
loopCondition

loopBody :: (Typeable a,Read a, Show a) => [(Var a,ValueSet a,InputMode)] -> Gen Condition -> Gen Specification
loopBody :: forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Gen Condition -> Gen Specification
loopBody [(Var a, ValueSet a, InputMode)]
xs Gen Condition
loopCondition = do
  Condition
cond <- Gen Condition
loopCondition
  let progress :: Specification
progress = case Condition
cond of  Condition Term 'Transparent Bool
_ (Var a
xp,ValueSet a
vs) -> Var a -> ValueSet a -> InputMode -> Specification
forall a.
(Typeable a, Read a, Show a) =>
Var a -> ValueSet a -> InputMode -> Specification
readInput Var a
xp ValueSet a
vs InputMode
AssumeValid
  Specification -> Specification
s1 <- [(Var a, ValueSet a, InputMode)]
-> Int -> Gen (Specification -> Specification)
forall a.
(Typeable a, Read a, Show a) =>
[(Var a, ValueSet a, InputMode)]
-> Int -> Gen (Specification -> Specification)
someInputsWithHole [(Var a, ValueSet a, InputMode)]
xs Int
2
  let s1' :: Specification
s1' = Specification -> Specification
s1 Specification
progress
  [Gen Specification] -> Gen Specification
forall a. [Gen a] -> Gen a
oneof
    [ Specification -> Gen Specification
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification -> Gen Specification)
-> Specification -> Gen Specification
forall a b. (a -> b) -> a -> b
$ Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch (Condition -> Term 'Transparent Bool
condTerm Condition
cond) Specification
exit Specification
s1'
    , Specification -> Gen Specification
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Specification -> Gen Specification)
-> Specification -> Gen Specification
forall a b. (a -> b) -> a -> b
$ Term 'Transparent Bool
-> Specification -> Specification -> Specification
branch (Term 'Transparent Bool -> Term 'Transparent Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
not' (Term 'Transparent Bool -> Term 'Transparent Bool)
-> Term 'Transparent Bool -> Term 'Transparent Bool
forall a b. (a -> b) -> a -> b
$ Condition -> Term 'Transparent Bool
condTerm Condition
cond) Specification
s1' Specification
exit
    ]

data Condition = forall a. (Typeable a, Read a, Show a) => Condition { Condition -> Term 'Transparent Bool
condTerm :: Term 'Transparent Bool, ()
_progressInfo :: (Var a,ValueSet a) }

-- generates a numeric condition of the form
-- f xs `comp` n
-- that contains every variable at most once
progressCondition :: [(Var Integer,ValueSet Integer)] -> [Var Integer] -> Gen Condition
progressCondition :: [(Var Integer, ValueSet Integer)] -> [Var Integer] -> Gen Condition
progressCondition [(Var Integer, ValueSet Integer)]
lists [Var Integer]
nums = do
  let comp :: Term k Integer -> Term k Integer -> Term k Bool
comp = Term k Integer -> Term k Integer -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
(.>.)
  Term 'Transparent Integer
n <- [Gen (Term 'Transparent Integer)]
-> Gen (Term 'Transparent Integer)
forall a. [Gen a] -> Gen a
oneof [Var Integer -> Term 'Transparent Integer
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k a
currentValue (Var Integer -> Term 'Transparent Integer)
-> Gen (Var Integer) -> Gen (Term 'Transparent Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var Integer] -> Gen (Var Integer)
forall a. [a] -> Gen a
elements [Var Integer]
nums, Integer -> Term 'Transparent Integer
forall (k :: TermKind). Integer -> Term k Integer
intLit (Integer -> Term 'Transparent Integer)
-> Gen Integer -> Gen (Term 'Transparent Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0,Integer
10)]
  (Var Integer
xs,ValueSet Integer
vs) <- [(Var Integer, ValueSet Integer)]
-> Gen (Var Integer, ValueSet Integer)
forall a. [a] -> Gen a
elements [(Var Integer, ValueSet Integer)]
lists
  let f :: Term k [Integer] -> Term k Integer
f = Term k [Integer] -> Term k Integer
forall a (k :: TermKind).
Typeable a =>
Term k [a] -> Term k Integer
length'
  Condition -> Gen Condition
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Condition -> Gen Condition) -> Condition -> Gen Condition
forall a b. (a -> b) -> a -> b
$ Term 'Transparent Bool
-> (Var Integer, ValueSet Integer) -> Condition
forall a.
(Typeable a, Read a, Show a) =>
Term 'Transparent Bool -> (Var a, ValueSet a) -> Condition
Condition (Term 'Transparent [Integer] -> Term 'Transparent Integer
forall {k :: TermKind}. Term k [Integer] -> Term k Integer
f (Var Integer -> Term 'Transparent [Integer]
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k [a]
allValues Var Integer
xs) Term 'Transparent Integer
-> Term 'Transparent Integer -> Term 'Transparent Bool
forall {k :: TermKind}.
Term k Integer -> Term k Integer -> Term k Bool
`comp` Term 'Transparent Integer
n) (Var Integer
xs,ValueSet Integer
vs)

-- simple terms
intTerm :: [Var Integer] -> [Var Integer] -> Gen (Term k Integer)
intTerm :: forall (k :: TermKind).
[Var Integer] -> [Var Integer] -> Gen (Term k Integer)
intTerm [Var Integer]
lists [Var Integer]
xs =
  [Gen (Term k Integer)] -> Gen (Term k Integer)
forall a. [Gen a] -> Gen a
oneof ([Gen (Term k Integer)] -> Gen (Term k Integer))
-> [Gen (Term k Integer)] -> Gen (Term k Integer)
forall a b. (a -> b) -> a -> b
$ [[Gen (Term k Integer)]] -> [Gen (Term k Integer)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [ Gen (Term k Integer)
forall {k :: TermKind}. Gen (Term k Integer)
unary  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Var Integer] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var Integer]
lists ]
    , [ Gen (Term k Integer)
forall {k :: TermKind}. Gen (Term k Integer)
var    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Var Integer] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var Integer]
xs]
    , [ Gen (Term k Integer)
forall {k :: TermKind}. Gen (Term k Integer)
binary | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Var Integer] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var Integer]
xs]
    ]
  where
    var :: Gen (Term k Integer)
var = do
      Var Integer
x <- [Var Integer] -> Gen (Var Integer)
forall a. [a] -> Gen a
elements [Var Integer]
xs
      Term k Integer -> Gen (Term k Integer)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term k Integer -> Gen (Term k Integer))
-> Term k Integer -> Gen (Term k Integer)
forall a b. (a -> b) -> a -> b
$ Var Integer -> Term k Integer
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k a
currentValue Var Integer
x
    unary :: Gen (Term k Integer)
unary = do
      Term k [Integer] -> Term k Integer
f <- [Term k [Integer] -> Term k Integer]
-> Gen (Term k [Integer] -> Term k Integer)
forall a. [a] -> Gen a
elements [Term k [Integer] -> Term k Integer
forall {k :: TermKind}. Term k [Integer] -> Term k Integer
sum', Term k [Integer] -> Term k Integer
forall a (k :: TermKind).
Typeable a =>
Term k [a] -> Term k Integer
length']
      Var Integer
x <- [Var Integer] -> Gen (Var Integer)
forall a. [a] -> Gen a
elements [Var Integer]
lists
      Term k Integer -> Gen (Term k Integer)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term k Integer -> Gen (Term k Integer))
-> Term k Integer -> Gen (Term k Integer)
forall a b. (a -> b) -> a -> b
$ Term k [Integer] -> Term k Integer
f (Term k [Integer] -> Term k Integer)
-> Term k [Integer] -> Term k Integer
forall a b. (a -> b) -> a -> b
$ Var Integer -> Term k [Integer]
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k [a]
allValues Var Integer
x
    binary :: Gen (Term k Integer)
binary = do
      Term k Integer -> Term k Integer -> Term k Integer
f <- [Term k Integer -> Term k Integer -> Term k Integer]
-> Gen (Term k Integer -> Term k Integer -> Term k Integer)
forall a. [a] -> Gen a
elements [Term k Integer -> Term k Integer -> Term k Integer
forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.+.), Term k Integer -> Term k Integer -> Term k Integer
forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.-.), Term k Integer -> Term k Integer -> Term k Integer
forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.*.)]
      Var Integer
x <- [Var Integer] -> Gen (Var Integer)
forall a. [a] -> Gen a
elements [Var Integer]
xs
      Var Integer
y <- [Var Integer] -> Gen (Var Integer)
forall a. [a] -> Gen a
elements [Var Integer]
xs
      Term k Integer -> Gen (Term k Integer)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term k Integer -> Gen (Term k Integer))
-> Term k Integer -> Gen (Term k Integer)
forall a b. (a -> b) -> a -> b
$ Term k Integer -> Term k Integer -> Term k Integer
f (Var Integer -> Term k Integer
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k a
currentValue Var Integer
x) (Var Integer -> Term k Integer
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k a
currentValue Var Integer
y)