module Test.Extrapolate.Generalization
( counterExampleGeneralizations
, candidateGeneralizations
, fastCandidateGeneralizations
, candidateHoleGeneralizations
, module Test.Extrapolate.Expr
)
where
import Test.LeanCheck.Error (errorToFalse)
import Test.Extrapolate.Expr
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
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
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
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]