-- |
-- Module      : Test.Extrapolate.Generalization
-- 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 defines utilities for unconditional generalization.
--
-- You are probably better off importing "Test.Extrapolate".
module Test.Extrapolate.Generalization
  ( counterExampleGeneralizations

  , candidateGeneralizations
  , fastCandidateGeneralizations
  , candidateHoleGeneralizations

  , module Test.Extrapolate.Expr
  )
where

import Test.LeanCheck.Error (errorToFalse)

import Test.Extrapolate.Expr

-- |
-- Given boolean expression representing a counter-example,
-- returns all possible unconditional generalizations.
--
-- If more than one generalization is returned,
-- they are _not_ instances of one another.
-- (cf. 'isInstanceOf')
-- All according to a given function that lists ground expressions.
--
-- > > counterExampleGeneralizations (groundsFor not) false
-- > []
--
-- > > counterExampleGeneralizations (groundsFor not) (false -&&- true)
-- > [False && p :: Bool]
--
-- > > counterExampleGeneralizations (groundsFor not) (false -||- true)
-- > []
--
-- > > counterExampleGeneralizations (groundsFor not) (false -/=- false)
-- > [p /= p :: Bool]
--
-- > > counterExampleGeneralizations (groundsFor not) (false -&&- true -&&- false)
-- > [ (False && _) && _ :: Bool
-- > , p && False :: Bool
-- > ]
counterExampleGeneralizations :: (Expr -> [Expr]) -> Expr -> [Expr]
counterExampleGeneralizations :: (Expr -> [Expr]) -> Expr -> [Expr]
counterExampleGeneralizations Expr -> [Expr]
grounds  =
  (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
canonicalize ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
filterRelevant ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> Expr -> [Expr]
fastCandidateGeneralizations Expr -> Bool
isListable
  where
  isListable :: Expr -> Bool
isListable = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
grounds (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
holeAsTypeOf
  isCounterExample :: Expr -> Bool
isCounterExample  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
errorToFalse (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False) ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
grounds
  filterRelevant :: [Expr] -> [Expr]
filterRelevant []  =  []
  filterRelevant (Expr
g:[Expr]
gs)
    | Expr -> Bool
isCounterExample Expr
g  =  Expr
g Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr] -> [Expr]
filterRelevant [Expr
g' | Expr
g' <- [Expr]
gs, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
g' Expr -> Expr -> Bool
`isInstanceOf` Expr
g]
    | Bool
otherwise           =  [Expr] -> [Expr]
filterRelevant [Expr]
gs

-- |
-- Returns candidate generalizations for an expression.
-- (cf. 'candidateHoleGeneralizations')
--
-- This takes a function that returns whether to generalize a given
-- subexpression.
--
-- > > import Data.Express.Fixtures
--
-- > > candidateGeneralizations (\e -> typ e == typ one) (one -+- two)
-- > [ _ :: Int
-- > , _ + _ :: Int
-- > , x + x :: Int
-- > , _ + 2 :: Int
-- > , 1 + _ :: Int
-- > ]
--
-- > > candidateGeneralizations (const True) (one -+- two)
-- > [ _ :: Int
-- > , _ _ :: Int
-- > , _ _ _ :: Int
-- > , _ x x :: Int
-- > , _ 1 _ :: Int
-- > , _ + _ :: Int
-- > , x + x :: Int
-- > , _ 2 :: Int
-- > , _ _ 2 :: Int
-- > , _ 1 2 :: Int
-- > , _ + 2 :: Int
-- > , 1 + _ :: Int
-- > ]
candidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
candidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
candidateGeneralizations Expr -> Bool
should  =  (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
canonicalize
                                 ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Bool) -> Expr -> [Expr]
fastCandidateGeneralizations Expr -> Bool
should

-- |
-- Like 'candidateGeneralizations' but faster because result is not
-- canonicalized.  Variable names will be repeated across different types.
fastCandidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
fastCandidateGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
fastCandidateGeneralizations Expr -> Bool
should  =  (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
fastCanonicalVariations
                                     ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Bool) -> Expr -> [Expr]
candidateHoleGeneralizations Expr -> Bool
should

-- |
-- Returns candidate generalizations for an expression by replacing values with
-- holes. (cf. 'candidateGeneralizations')
--
-- > > import Data.Express.Fixtures
--
-- > > candidateHoleGeneralizations (\e -> typ e == typ one) (one -+- two)
-- > [ _ :: Int
-- > , _ + _ :: Int
-- > , _ + 2 :: Int
-- > , 1 + _ :: Int
-- > ]
--
-- > > candidateHoleGeneralizations (const True) (one -+- two)
-- > [ _ :: Int
-- > , _ _ :: Int
-- > , _ _ _ :: Int
-- > , _ 1 _ :: Int
-- > , _ + _ :: Int
-- > , _ 2 :: Int
-- > , _ _ 2 :: Int
-- > , _ 1 2 :: Int
-- > , _ + 2 :: Int
-- > , 1 + _ :: Int
-- > ]
candidateHoleGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
candidateHoleGeneralizations :: (Expr -> Bool) -> Expr -> [Expr]
candidateHoleGeneralizations Expr -> Bool
shouldGeneralize  =  Expr -> [Expr]
gen
  where
  gen :: Expr -> [Expr]
gen e :: Expr
e@(Expr
e1 :$ Expr
e2)  =
    [Expr -> Expr
holeAsTypeOf Expr
e | Expr -> Bool
shouldGeneralize Expr
e]
    [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> Expr -> Expr) -> [Expr] -> [Expr] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
productWith Expr -> Expr -> Expr
(:$) (Expr -> [Expr]
gen Expr
e1) (Expr -> [Expr]
gen Expr
e2)
    [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Expr -> Expr
:$ Expr
e2) (Expr -> [Expr]
gen Expr
e1)
    [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e1 Expr -> Expr -> Expr
:$) (Expr -> [Expr]
gen Expr
e2)
  gen Expr
e
    | Expr -> Bool
isVar Expr
e    =  []
    | Bool
otherwise  =  [Expr -> Expr
holeAsTypeOf Expr
e | Expr -> Bool
shouldGeneralize Expr
e]

productWith :: (a -> b -> c) -> [a] -> [b] -> [c]
productWith :: (a -> b -> c) -> [a] -> [b] -> [c]
productWith a -> b -> c
f [a]
xs [b]
ys = [a -> b -> c
f a
x b
y | a
x <- [a]
xs, b
y <- [b]
ys]