-- |
-- Module      : Test.Extrapolate.ConditionalGeneralization
-- 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 conditional generalization.
--
-- You are probably better off importing "Test.Extrapolate".
module Test.Extrapolate.ConditionalGeneralization
  ( conditionalCounterExampleGeneralizations
  , validConditions
  , candidateConditions
  )
where

import Data.Ratio

import Test.LeanCheck.Error (errorToFalse)

import Test.Extrapolate.Speculation
import Test.Extrapolate.Generalization
import Test.Extrapolate.Utils

conditionalCounterExampleGeneralizations
  :: Int -> [[Expr]] -> (Expr -> [Expr]) -> (Expr -> Expr -> Expr)
  -> Expr -> [Expr]
conditionalCounterExampleGeneralizations :: Int
-> [[Expr]]
-> (Expr -> [Expr])
-> (Expr -> Expr -> Expr)
-> Expr
-> [Expr]
conditionalCounterExampleGeneralizations Int
maxConditionSize [[Expr]]
atoms Expr -> [Expr]
grounds Expr -> Expr -> Expr
(-==-) Expr
e  =
  [ Expr -> Expr
canonicalize (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
g Expr -> Expr -> Expr
-&&- Expr
wc
  | Expr
g <- (Expr -> Bool) -> Expr -> [Expr]
fastCandidateGeneralizations Expr -> Bool
isListable Expr
e
  , let wc :: Expr
wc = Expr -> Expr
weakestCondition' Expr
g
  , Expr
wc Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Bool -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"False" Bool
False
  , Expr
wc Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Bool -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"True"  Bool
True
  ]
  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
  weakestCondition' :: Expr -> Expr
weakestCondition' = (Thy, [Expr]) -> (Expr -> [Expr]) -> Expr -> Expr
weakestCondition
    ((Expr -> Expr -> Bool) -> Int -> [[Expr]] -> (Thy, [Expr])
theoryAndReprConds Expr -> Expr -> Bool
(===) Int
maxConditionSize [[Expr]]
atoms)
    Expr -> [Expr]
grounds
  Expr
e1 === :: Expr -> Expr -> Bool
=== Expr
e2 = (Expr -> [Expr]) -> Expr -> Bool
isTrue Expr -> [Expr]
grounds (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2

candidateConditions :: (Expr -> [Expr]) -> (Thy,[Expr]) -> Expr -> [Expr]
candidateConditions :: (Expr -> [Expr]) -> (Thy, [Expr]) -> Expr -> [Expr]
candidateConditions Expr -> [Expr]
grounds (Thy
thy,[Expr]
cs) Expr
e = Bool -> Expr
forall a. Express a => a -> Expr
expr Bool
True Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:
  [ Expr
c | (Expr
c,[Expr]
_) <- Thy -> [Expr] -> [Expr] -> [(Expr, [Expr])]
classesFromSchemasAndVariables Thy
thy (Expr -> [Expr]
nubVars Expr
e) [Expr]
cs
      , Expr -> Bool
hasVar Expr
c
      , Bool -> Bool
not (Expr -> Bool
isAssignment Expr
c)
      , Bool -> Bool
not ((Expr -> [Expr]) -> Expr -> Bool
isAssignmentTest Expr -> [Expr]
grounds Expr
c)
      ]
-- 'expr True' is expected by the functions that call candidateConditions.  It
-- is always useful to check if a generalization without any conditions still
-- passes (that means we should skip as there is an already reported
-- unconditional generalization).

validConditions :: (Thy,[Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
validConditions :: (Thy, [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
validConditions (Thy, [Expr])
thyes Expr -> [Expr]
grounds Expr
e =
  [ Expr
c | Expr
c <- (Expr -> [Expr]) -> (Thy, [Expr]) -> Expr -> [Expr]
candidateConditions Expr -> [Expr]
grounds (Thy, [Expr])
thyes Expr
e
      , Expr -> Bool
isCounterExample (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
e Expr -> Expr -> Expr
-&&- Expr
c ] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Bool -> Expr
forall a. Express a => a -> Expr
expr Bool
False]
  where
  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

weakestCondition :: (Thy,[Expr]) -> (Expr -> [Expr]) -> Expr -> Expr
weakestCondition :: (Thy, [Expr]) -> (Expr -> [Expr]) -> Expr -> Expr
weakestCondition (Thy, [Expr])
thyes Expr -> [Expr]
grounds Expr
e  =
  (Expr -> Ratio Int) -> [Expr] -> Expr
forall b a. Ord b => (a -> b) -> [a] -> a
maximumOn ((Expr -> [Expr]) -> Expr -> Ratio Int
ratioFailures Expr -> [Expr]
grounds (Expr -> Ratio Int) -> (Expr -> Expr) -> Expr -> Ratio Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
e Expr -> Expr -> Expr
-&&-)) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ (Thy, [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
validConditions (Thy, [Expr])
thyes Expr -> [Expr]
grounds Expr
e

ratioFailures :: (Expr -> [Expr]) -> Expr -> Ratio Int
ratioFailures :: (Expr -> [Expr]) -> Expr -> Ratio Int
ratioFailures Expr -> [Expr]
grounds Expr
e  =  [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ps Int -> Int -> Ratio Int
forall a. Integral a => a -> a -> Ratio a
% [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
gs
  where
  gs :: [Expr]
gs = Expr -> [Expr]
grounds Expr
e
  ps :: [Expr]
ps = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (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) -> Expr
forall a b. (a, b) -> b
snd ((Expr, Expr) -> Expr) -> (Expr -> (Expr, Expr)) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> (Expr, Expr)
unand) [Expr]
gs

isAssignmentTest :: (Expr -> [Expr]) -> Expr -> Bool
isAssignmentTest :: (Expr -> [Expr]) -> Expr -> Bool
isAssignmentTest Expr -> [Expr]
grounds Expr
e | Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr -> TypeRep
typ Expr
false = Bool
False
isAssignmentTest Expr -> [Expr]
grounds Expr
e = [Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
rs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& [Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id [Bool]
rs) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
  where
  rs :: [Bool]
rs = [Bool -> Bool
errorToFalse (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False Expr
e' | Expr
e' <- Expr -> [Expr]
grounds Expr
e]