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 maxCondSize atoms grounds (-==-) e =
[ canonicalize $ g -&&- wc
| g <- fastCandidateGeneralizations isListable e
, let wc = weakestCondition' g
, wc /= value "False" False
, wc /= value "True" True
]
where
isListable = not . null . grounds . holeAsTypeOf
weakestCondition' = weakestCondition
(theoryAndReprConds maxCondSize (===) atoms)
grounds
e1 === e2 = isTrue grounds $ e1 -==- e2
candidateConditions :: (Expr -> [Expr]) -> (Thy,[Expr]) -> Expr -> [Expr]
candidateConditions grounds (thy,cs) e = expr True :
[ c | (c,_) <- classesFromSchemasAndVariables thy (nubVars e) cs
, hasVar c
, not (isAssignment c)
, not (isAssignmentTest grounds c)
]
validConditions :: (Thy,[Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
validConditions thyes grounds e =
[ c | c <- candidateConditions grounds thyes e
, isCounterExample $ e -&&- c ] ++ [expr False]
where
isCounterExample = all (not . errorToFalse . eval False) . grounds
weakestCondition :: (Thy,[Expr]) -> (Expr -> [Expr]) -> Expr -> Expr
weakestCondition thyes grounds e =
maximumOn (ratioFailures grounds . (e -&&-)) $ validConditions thyes grounds e
ratioFailures :: (Expr -> [Expr]) -> Expr -> Ratio Int
ratioFailures grounds e = length ps % length gs
where
gs = grounds e
ps = filter (errorToFalse . eval False . snd . unand) gs
isAssignmentTest :: (Expr -> [Expr]) -> Expr -> Bool
isAssignmentTest grounds e | typ e /= typ false = False
isAssignmentTest grounds e = length rs > 1 && length (filter id rs) == 1
where
rs = [errorToFalse $ eval False e' | e' <- grounds e]