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)
]
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]