{-# LANGUAGE DeriveDataTypeable #-}
module Test.Extrapolate.Core
( module Test.LeanCheck
, module Test.Extrapolate.Expr
, module Test.Extrapolate.Speculation
, module Test.Extrapolate.Generalizable
, module Test.Extrapolate.Generalization
, module Test.Extrapolate.ConditionalGeneralization
, module Test.Extrapolate.Testable
, counterExampleWithGeneralizations
)
where
import Data.Typeable
import Test.LeanCheck hiding
( Testable
, results
, counterExamples
, counterExample
, productWith
, check
, checkFor
, checkResult
, checkResultFor
)
import Test.Speculate.Reason (Thy)
import Test.Speculate.Engine (classesFromSchemasAndVariables)
import Test.Extrapolate.Expr
import Test.Extrapolate.Speculation
import Test.Extrapolate.Generalizable
import Test.Extrapolate.Generalization
import Test.Extrapolate.ConditionalGeneralization
import Test.Extrapolate.Testable
counterExampleWithGeneralizations :: Testable a => a -> Maybe (Expr,[Expr])
counterExampleWithGeneralizations :: a -> Maybe (Expr, [Expr])
counterExampleWithGeneralizations a
p = case a -> Maybe Expr
forall a. Testable a => a -> Maybe Expr
counterExample a
p of
Maybe Expr
Nothing -> Maybe (Expr, [Expr])
forall a. Maybe a
Nothing
Just Expr
e -> (Expr, [Expr]) -> Maybe (Expr, [Expr])
forall a. a -> Maybe a
Just (Expr
e,Expr -> [Expr]
gens Expr
e [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 (Expr -> [Expr]
cgens Expr
e))
where
grounds :: Expr -> [Expr]
grounds = a -> Expr -> [Expr]
forall a. Testable a => a -> Expr -> [Expr]
testableGrounds a
p
gens :: Expr -> [Expr]
gens = (Expr -> [Expr]) -> Expr -> [Expr]
counterExampleGeneralizations Expr -> [Expr]
grounds
cgens :: Expr -> [Expr]
cgens = Int
-> [[Expr]]
-> (Expr -> [Expr])
-> (Expr -> Expr -> Expr)
-> Expr
-> [Expr]
conditionalCounterExampleGeneralizations
(a -> Int
forall a. Testable a => a -> Int
testableMaxConditionSize a
p)
(a -> [[Expr]]
forall a. Testable a => a -> [[Expr]]
testableAtoms a
p)
Expr -> [Expr]
grounds
(a -> Expr -> Expr -> Expr
forall a. Testable a => a -> Expr -> Expr -> Expr
testableMkEquation a
p)