{-# LANGUAGE CPP, RecordWildCards, TupleSections #-}
module Conjure.Engine
( conjure
, conjureWithMaxSize
, Args(..)
, args
, conjureWith
, conjpure
, conjpureWith
, candidateExprs
, module Data.Express
, module Data.Express.Fixtures
, module Test.Speculate.Engine
, module Test.Speculate.Reason
)
where
import Data.Express
import Data.Express.Fixtures hiding ((-==-))
import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
import Test.Speculate.Reason (isRootNormalE)
import Test.Speculate.Engine (theoryFromAtoms, groundBinds)
import Conjure.Expr
import Conjure.Conjurable
conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
conjure :: String -> f -> [Expr] -> IO ()
conjure = Args -> String -> f -> [Expr] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith Args
args
conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()
conjureWithMaxSize :: Int -> String -> f -> [Expr] -> IO ()
conjureWithMaxSize Int
sz = Args -> String -> f -> [Expr] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith Args
args
{ maxSize :: Int
maxSize = Int
sz
, maxEquationSize :: Int
maxEquationSize = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
sz (Args -> Int
maxEquationSize Args
args)
}
data Args = Args
{ Args -> Int
maxTests :: Int
, Args -> Int
maxSize :: Int
, Args -> Int
maxRecursiveCalls :: Int
, Args -> Int
maxEquationSize :: Int
, Args -> Int
maxRecursionSize :: Int
, Args -> Int
maxSearchTests :: Int
, Args -> [[Expr]]
forceTests :: [[Expr]]
}
args :: Args
args :: Args
args = Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args
Args
{ maxTests :: Int
maxTests = Int
60
, maxSize :: Int
maxSize = Int
12
, maxRecursiveCalls :: Int
maxRecursiveCalls = Int
1
, maxEquationSize :: Int
maxEquationSize = Int
5
, maxRecursionSize :: Int
maxRecursionSize = Int
60
, maxSearchTests :: Int
maxSearchTests = Int
100000
, forceTests :: [[Expr]]
forceTests = []
}
conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith :: Args -> String -> f -> [Expr] -> IO ()
conjureWith Args
args String
nm f
f [Expr]
es = do
Expr -> IO ()
forall a. Show a => a -> IO ()
print (String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
var ([String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
nm) f
f)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- testing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" combinations of argument values"
Integer -> [([Expr], [Expr], [Expr])] -> IO ()
forall (t :: * -> *) (t :: * -> *) t a a.
(Foldable t, Foldable t, Show t, Num t) =>
t -> [([Expr], t a, t a)] -> IO ()
pr Integer
1 [([Expr], [Expr], [Expr])]
rs
where
pr :: t -> [([Expr], t a, t a)] -> IO ()
pr t
n [] = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"cannot conjure"
pr t
n (([Expr]
is,t a
cs,t a
es):[([Expr], t a, t a)]
rs) = do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- looking through "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
cs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
es)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
n
case [Expr]
is of
[] -> t -> [([Expr], t a, t a)] -> IO ()
pr (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) [([Expr], t a, t a)]
rs
(Expr
i:[Expr]
_) -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Expr -> String
showEq Expr
i
String -> IO ()
putStrLn String
""
rs :: [([Expr], [Expr], [Expr])]
rs = [[Expr]] -> [[Expr]] -> [[Expr]] -> [([Expr], [Expr], [Expr])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [[Expr]]
iss [[Expr]]
css [[Expr]]
ess
([[Expr]]
iss, [[Expr]]
css, [[Expr]]
ess, [Expr]
ts) = Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
forall f.
Conjurable f =>
Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args
args String
nm f
f [Expr]
es
conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpure :: String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpure = Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
forall f.
Conjurable f =>
Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args
args
conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith :: Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args{Int
[[Expr]]
forceTests :: [[Expr]]
maxSearchTests :: Int
maxRecursionSize :: Int
maxEquationSize :: Int
maxRecursiveCalls :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
maxSearchTests :: Args -> Int
maxRecursionSize :: Args -> Int
maxRecursiveCalls :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f [Expr]
es = ([[Expr]]
implementationsT, [[Expr]]
candidatesT, [[Expr]]
allCandidatesT, [Expr]
tests)
where
tests :: [Expr]
tests = [Expr
ffxx Expr -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs | [(Expr, Expr)]
bs <- [[(Expr, Expr)]]
dbss]
implementationsT :: [[Expr]]
implementationsT = (Expr -> Expr) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
vffxx Expr -> Expr -> Expr
-==-) ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
implements [[Expr]]
candidatesT
implements :: Expr -> Bool
implements Expr
e = Expr -> Expr -> Bool
apparentlyTerminates Expr
rrff Expr
e
Bool -> Bool -> Bool
&& Expr
ffxx Expr -> Expr -> Bool
?=? Int -> Expr -> Expr -> Expr
recursexpr Int
maxRecursionSize Expr
vffxx Expr
e
candidatesT :: [[Expr]]
candidatesT = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
ffxx) [[Expr]]
allCandidatesT
allCandidatesT :: [[Expr]]
allCandidatesT = Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxSize
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
forall f.
Conjurable f =>
String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
candidateExprs String
nm f
f Int
maxEquationSize Int
maxRecursiveCalls Expr -> Expr -> Bool
(===) [Expr]
es
ffxx :: Expr
ffxx = String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureApplication String
nm f
f
vffxx :: Expr
vffxx = String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
(Expr
rrff:[Expr]
xxs) = Expr -> [Expr]
unfoldApp Expr
vffxx
=== :: Expr -> Expr -> Bool
(===) = f -> Int -> Expr -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Expr -> Bool
conjureAreEqual f
f Int
maxTests
Expr
e1 ?=? :: Expr -> Expr -> Bool
?=? Expr
e2 = Expr -> Bool
isTrueWhenDefined (Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2)
-==- :: Expr -> Expr -> Expr
(-==-) = f -> Expr -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f
isTrueWhenDefined :: Expr -> Bool
isTrueWhenDefined Expr
e = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (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] -> Bool
forall a b. (a -> b) -> a -> b
$ ([(Expr, Expr)] -> Expr) -> [[(Expr, Expr)]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e Expr -> [(Expr, Expr)] -> Expr
//-) [[(Expr, Expr)]]
dbss
bss, dbss :: [[(Expr,Expr)]]
bss :: [[(Expr, Expr)]]
bss = Int -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Int -> [a] -> [a]
take Int
maxSearchTests ([[(Expr, Expr)]] -> [[(Expr, Expr)]])
-> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [[(Expr, Expr)]]
groundBinds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) Expr
ffxx
fbss :: [[(Expr, Expr)]]
fbss = [[Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
xxs [Expr]
vs | [Expr]
vs <- [[Expr]]
forceTests, Expr -> Bool
isWellTyped (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
foldApp (Expr
rrffExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
vs)]
dbss :: [[(Expr, Expr)]]
dbss = Int -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Int -> [a] -> [a]
take Int
maxTests
([[(Expr, Expr)]] -> [[(Expr, Expr)]])
-> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ ([[(Expr, Expr)]
bs | [(Expr, Expr)]
bs <- [[(Expr, Expr)]]
bss, 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 -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
e Expr -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs] [[(Expr, Expr)]] -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[(Expr, Expr)]]
fbss)
[[(Expr, Expr)]] -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. [a] -> [a] -> [a]
++ [[(Expr, Expr)]]
fbss
where
e :: Expr
e = Expr
ffxx Expr -> Expr -> Expr
-==- Expr
ffxx
candidateExprs :: Conjurable f
=> String -> f
-> Int
-> Int
-> (Expr -> Expr -> Bool)
-> [Expr]
-> [[Expr]]
candidateExprs :: String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
candidateExprs String
nm f
f Int
sz Int
mc Expr -> Expr -> Bool
(===) [Expr]
es =
String
-> f
-> Int
-> Int
-> (Expr -> Expr -> Bool)
-> [[Expr]]
-> [[Expr]]
forall f.
Conjurable f =>
String
-> f
-> Int
-> Int
-> (Expr -> Expr -> Bool)
-> [[Expr]]
-> [[Expr]]
candidateExprsT String
nm f
f Int
sz Int
mc Expr -> Expr -> Bool
(===) [[Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ f -> [Expr]
forall f. Conjurable f => f -> [Expr]
conjureIfs f
f]
candidateExprsT :: Conjurable f
=> String -> f
-> Int
-> Int
-> (Expr -> Expr -> Bool)
-> [[Expr]]
-> [[Expr]]
candidateExprsT :: String
-> f
-> Int
-> Int
-> (Expr -> Expr -> Bool)
-> [[Expr]]
-> [[Expr]]
candidateExprsT String
nm f
f Int
sz Int
mc Expr -> Expr -> Bool
(===) [[Expr]]
ess =
(Expr -> Bool) -> [[Expr]] -> [[Expr]]
candidateExprsTT Expr -> Bool
keep ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
exs] [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]]
ess
where
(Expr
ef:[Expr]
exs) = Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
keep :: Expr -> Bool
keep Expr
e = Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Int
forall a. (a -> Bool) -> [a] -> Int
count (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ef) (Expr -> [Expr]
vars Expr
e) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
mc
thy :: Thy
thy = (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
sz ([[Expr]] -> Thy) -> [[Expr]] -> Thy
forall a b. (a -> b) -> a -> b
$ [f -> [Expr]
forall f. Conjurable f => f -> [Expr]
conjureHoles f
f [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
falseAndTrue]
[[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Expr]
falseAndTrue) [[Expr]]
ess
falseAndTrue :: [Expr]
falseAndTrue = [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True]
candidateExprsTT :: (Expr -> Bool) -> [[Expr]] -> [[Expr]]
candidateExprsTT :: (Expr -> Bool) -> [[Expr]] -> [[Expr]]
candidateExprsTT Expr -> Bool
keep = [[Expr]] -> [[Expr]]
exprT
where
exprT :: [[Expr]] -> [[Expr]]
exprT [[Expr]]
ess = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keep
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [[Expr]]
ess [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ ([[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]]
delay ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Maybe Expr) -> [[Expr]] -> [[Expr]] -> [[Expr]]
forall a b c. (a -> b -> Maybe c) -> [[a]] -> [[b]] -> [[c]]
productMaybeWith Expr -> Expr -> Maybe Expr
($$) [[Expr]]
rss [[Expr]]
rss)
where
rss :: [[Expr]]
rss = [[Expr]] -> [[Expr]]
exprT [[Expr]]
ess
candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
candidatesTD Expr -> Bool
keep Expr
h [Expr]
primitives = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
hasHole)
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [[Expr]]
town [[Expr
h]]
where
most :: Expr -> Expr
most = Expr -> Expr
mostGeneralCanonicalVariation
town :: [[Expr]] -> [[Expr]]
town :: [[Expr]] -> [[Expr]]
town ((Expr
e:[Expr]
es):[[Expr]]
ess) | Expr -> Bool
keep (Expr -> Expr
most Expr
e) = [[Expr
e]] [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]] -> [[Expr]]
town (Expr -> [[Expr]]
expand Expr
e [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ ([Expr]
es[Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]]
ess))
| Bool
otherwise = [[Expr]] -> [[Expr]]
town ([Expr]
es[Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]]
ess)
town ([]:[[Expr]]
ess) = [][Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]] -> [[Expr]]
town [[Expr]]
ess
town [] = []
expand :: Expr -> [[Expr]]
expand :: Expr -> [[Expr]]
expand Expr
e = case Expr -> [Expr]
holesBFS Expr
e of
[] -> []
(Expr
h:[Expr]
_) -> (Expr -> Expr) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr -> Expr -> Expr
fillBFS Expr
e) (Expr -> [[Expr]]
replacementsFor Expr
h)
replacementsFor :: Expr -> [[Expr]]
replacementsFor :: Expr -> [[Expr]]
replacementsFor Expr
h = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
h)
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [[Expr]]
primitiveApplications [Expr]
primitives