{-# LANGUAGE DeriveDataTypeable #-} -- for GHC <= 7.8
-- |
-- Module      : Test.Extrapolate.Core
-- Copyright   : (c) 2017-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Extrapolate,
-- a library for generalization of counter-examples.
--
-- This is the core of extrapolate.
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)