{-# LANGUAGE CPP, RecordWildCards, TupleSections #-}
module Conjure.Engine
( conjure
, conjureWithMaxSize
, Args(..)
, args
, conjureWith
, conjpure
, conjpureWith
, candidateExprs
, candidateDefns
, candidateDefns1
, candidateDefnsC
, conjureTheory
, conjureTheoryWith
, module Data.Express
, module Data.Express.Fixtures
, module Test.Speculate.Engine
, module Test.Speculate.Reason
)
where
import Control.Monad (when)
import Data.Express
import Data.Express.Fixtures hiding ((-==-))
import qualified Data.Express.Triexpr as T
import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
import Test.Speculate.Reason (Thy, rules, equations, canReduceTo, printThy, closureLimit)
import Test.Speculate.Engine (theoryFromAtoms, groundBinds, boolTy)
import Conjure.Expr
import Conjure.Conjurable
import Conjure.Prim
import Conjure.Defn
conjure :: Conjurable f => String -> f -> [Prim] -> IO ()
conjure :: String -> f -> [Prim] -> IO ()
conjure = Args -> String -> f -> [Prim] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureWith Args
args
conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
conjureWithMaxSize :: Int -> String -> f -> [Prim] -> IO ()
conjureWithMaxSize Int
sz = Args -> String -> f -> [Prim] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Prim] -> 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
maxEvalRecursions :: Int
, Args -> Int
maxEquationSize :: Int
, Args -> Int
maxSearchTests :: Int
, Args -> Bool
requireDescent :: Bool
, Args -> Bool
usePatterns :: Bool
, Args -> Bool
showTheory :: Bool
, Args -> [[Expr]]
forceTests :: [[Expr]]
}
args :: Args
args :: Args
args = Args :: Int
-> Int
-> Int
-> Int
-> Int
-> Bool
-> Bool
-> Bool
-> [[Expr]]
-> Args
Args
{ maxTests :: Int
maxTests = Int
360
, maxSize :: Int
maxSize = Int
12
, maxEvalRecursions :: Int
maxEvalRecursions = Int
60
, maxEquationSize :: Int
maxEquationSize = Int
5
, maxSearchTests :: Int
maxSearchTests = Int
100000
, requireDescent :: Bool
requireDescent = Bool
True
, usePatterns :: Bool
usePatterns = Bool
True
, showTheory :: Bool
showTheory = Bool
False
, forceTests :: [[Expr]]
forceTests = []
}
conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureWith :: Args -> String -> f -> [Prim] -> IO ()
conjureWith Args
args String
nm f
f [Prim]
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"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- pruning with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nRules 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 Int
nREs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" rules"
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showTheory Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"{-"
Thy -> IO ()
printThy Thy
thy
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Thy -> Bool
filtered Thy
thy) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- reasoning produced incorrect properties,"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" please re-run with more tests for faster results"
Integer -> [([Defn], [Defn])] -> IO ()
forall (t :: * -> *) t a.
(Foldable t, Show t, Num t) =>
t -> [([Defn], t a)] -> IO ()
pr Integer
1 [([Defn], [Defn])]
rs
where
pr :: t -> [([Defn], t a)] -> IO ()
pr t
n [] = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"cannot conjure\n"
pr t
n (([Defn]
is,t a
cs):[([Defn], 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
" candidates of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
n
case [Defn]
is of
[] -> t -> [([Defn], t a)] -> IO ()
pr (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) [([Defn], t a)]
rs
(Defn
i:[Defn]
_) -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Defn -> String
showDefn Defn
i
rs :: [([Defn], [Defn])]
rs = [[Defn]] -> [[Defn]] -> [([Defn], [Defn])]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Defn]]
iss [[Defn]]
css
([[Defn]]
iss, [[Defn]]
css, [Expr]
ts, Thy
thy) = Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith Args
args String
nm f
f [Prim]
es
nRules :: Int
nRules = Defn -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> Defn
rules Thy
thy)
nREs :: Int
nREs = Defn -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> Defn
equations Thy
thy) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nRules
conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpure :: String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpure = Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith Args
args
conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith :: Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith args :: Args
args@(Args{Bool
Int
[[Expr]]
forceTests :: [[Expr]]
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..}) String
nm f
f [Prim]
es = ([[Defn]]
implementationsT, [[Defn]]
candidatesT, [Expr]
tests, Thy
thy)
where
tests :: [Expr]
tests = [Expr
ffxx Expr -> Defn -> Expr
//- Defn
bs | Defn
bs <- [Defn]
dbss]
implementationsT :: [[Defn]]
implementationsT = (Defn -> Bool) -> [[Defn]] -> [[Defn]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Defn -> Bool
implements [[Defn]]
candidatesT
implements :: Defn -> Bool
implements Defn
fx = Defn -> Bool
defnApparentlyTerminates Defn
fx
Bool -> Bool -> Bool
&& Defn -> Expr -> Expr -> Bool
requal Defn
fx Expr
ffxx Expr
vffxx
candidatesT :: [[Defn]]
candidatesT = Int -> [[Defn]] -> [[Defn]]
forall a. Int -> [a] -> [a]
take Int
maxSize [[Defn]]
candidatesTT
([[Defn]]
candidatesTT, Thy
thy) = Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns Args
args String
nm f
f [Prim]
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
requal :: Defn -> Expr -> Expr -> Bool
requal Defn
dfn Expr
e1 Expr
e2 = Defn -> Expr -> Bool
isTrueWhenDefined Defn
dfn (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 :: Defn -> Expr -> Bool
isTrueWhenDefined Defn
dfn 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
. (Expr -> Expr) -> Int -> Defn -> Bool -> Expr -> Bool
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions Defn
dfn Bool
False)
([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ (Defn -> Expr) -> [Defn] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e Expr -> Defn -> Expr
//-) [Defn]
dbss
bss, dbss :: [[(Expr,Expr)]]
bss :: [Defn]
bss = Int -> [Defn] -> [Defn]
forall a. Int -> [a] -> [a]
take Int
maxSearchTests ([Defn] -> [Defn]) -> [Defn] -> [Defn]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [Defn]
groundBinds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) Expr
ffxx
fbss :: [Defn]
fbss = [[Expr] -> [Expr] -> Defn
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 :: [Defn]
dbss = Int -> [Defn] -> [Defn]
forall a. Int -> [a] -> [a]
take Int
maxTests
([Defn] -> [Defn]) -> [Defn] -> [Defn]
forall a b. (a -> b) -> a -> b
$ ([Defn
bs | Defn
bs <- [Defn]
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 -> Defn -> Expr
//- Defn
bs] [Defn] -> [Defn] -> [Defn]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Defn]
fbss)
[Defn] -> [Defn] -> [Defn]
forall a. [a] -> [a] -> [a]
++ [Defn]
fbss
where
e :: Expr
e = Expr
ffxx Expr -> Expr -> Expr
-==- Expr
ffxx
conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO ()
conjureTheory :: String -> f -> [Prim] -> IO ()
conjureTheory = Args -> String -> f -> [Prim] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureTheoryWith Args
args
conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureTheoryWith :: Args -> String -> f -> [Prim] -> IO ()
conjureTheoryWith Args
args String
nm f
f [Prim]
es = do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"theory with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Defn -> Int) -> Defn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Defn -> String) -> Defn -> String
forall a b. (a -> b) -> a -> b
$ Thy -> Defn
rules Thy
thy) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" rules and "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Defn -> Int) -> Defn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Defn -> String) -> Defn -> String
forall a b. (a -> b) -> a -> b
$ Thy -> Defn
equations Thy
thy) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" equations"
Thy -> IO ()
printThy Thy
thy
where
([[Defn]]
_, [[Defn]]
_, [Expr]
_, Thy
thy) = Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith Args
args String
nm f
f [Prim]
es
candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns :: Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns Args
args = Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
cds Args
args
where
cds :: Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
cds = if Args -> Bool
usePatterns Args
args
then Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefnsC
else Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns1
candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns1 :: Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns1 Args
args String
nm f
f [Prim]
ps = ([[Expr]] -> [[Defn]]) -> ([[Expr]], Thy) -> ([[Defn]], Thy)
forall t a b. (t -> a) -> (t, b) -> (a, b)
mapFst ((Expr -> Defn) -> [[Expr]] -> [[Defn]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT Expr -> Defn
forall b. b -> [(Expr, b)]
toDefn) (([[Expr]], Thy) -> ([[Defn]], Thy))
-> ([[Expr]], Thy) -> ([[Defn]], Thy)
forall a b. (a -> b) -> a -> b
$ Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
candidateExprs Args
args String
nm f
f [Prim]
ps
where
mapFst :: (t -> a) -> (t, b) -> (a, b)
mapFst t -> a
f (t
x,b
y) = (t -> a
f t
x, b
y)
efxs :: Expr
efxs = String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
toDefn :: b -> [(Expr, b)]
toDefn b
e = [(Expr
efxs, b
e)]
candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
candidateExprs :: Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
candidateExprs Args{Bool
Int
[[Expr]]
forceTests :: [[Expr]]
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f [Prim]
ps = ([[Expr]]
as [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [[Expr]] -> [[Expr]]
`enumerateFillings` [[Expr]]
recs) [[Expr]]
ts, Thy
thy)
where
es :: [Expr]
es = (Prim -> Expr) -> [Prim] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Prim -> Expr
forall a b. (a, b) -> a
fst [Prim]
ps
ts :: [[Expr]]
ts | Expr -> TypeRep
typ Expr
efxs TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy = Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
andE [[[Expr]]
cs, [[Expr]]
rs]
[[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
orE [[[Expr]]
cs, [[Expr]]
rs]
| Bool
otherwise = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepIf
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (f -> Expr
forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
as, [[Expr]]
rs]
[[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (f -> Expr
forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
rs, [[Expr]]
as]
cs :: [[Expr]]
cs = (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` [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])
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [[Expr]]
forN (Bool -> Expr
forall a. Typeable a => a -> Expr
hole (Bool
forall a. HasCallStack => a
undefined :: Bool))
as :: [[Expr]]
as = Expr -> [[Expr]]
forN Expr
efxs
rs :: [[Expr]]
rs = Expr -> [[Expr]]
forR Expr
efxs
forN :: Expr -> [[Expr]]
forN Expr
h = Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
forR :: Expr -> [[Expr]]
forR Expr
h = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr
eh Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Expr -> [Expr]
holes Expr
e))
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
eh]
eh :: Expr
eh = Expr -> Expr
holeAsTypeOf Expr
efxs
efxs :: Expr
efxs = String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
(Expr
ef:[Expr]
exs) = Expr -> [Expr]
unfoldApp Expr
efxs
keep :: Expr -> Bool
keep = Thy -> Expr -> Bool
isRootNormalE Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
ds :: [Expr]
ds = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstructor f
f Int
maxTests) [Expr]
es
keepR :: Expr -> Bool
keepR | Bool
requireDescent = (Expr -> Bool) -> Expr -> Expr -> Bool
descends (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
ds) Expr
efxs
| Bool
otherwise = Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
recs :: [[Expr]]
recs = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepR
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [[Expr]]
forN Expr
h | Expr
h <- f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
thy :: Thy
thy = (Expr -> Expr -> Bool) -> Thy -> Thy
filterTheory Expr -> Expr -> Bool
(===)
(Thy -> Thy) -> ([Expr] -> Thy) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize ([[Expr]] -> Thy) -> ([Expr] -> [[Expr]]) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[]) ([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub
([Expr] -> Thy) -> [Expr] -> Thy
forall a b. (a -> b) -> a -> b
$ [Prim] -> [Expr]
cjHoles (String -> f -> Prim
forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fPrim -> [Prim] -> [Prim]
forall a. a -> [a] -> [a]
:[Prim]
ps) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [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] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
=== :: Expr -> Expr -> Bool
(===) = [Prim] -> Int -> Expr -> Expr -> Bool
cjAreEqual (String -> f -> Prim
forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fPrim -> [Prim] -> [Prim]
forall a. a -> [a] -> [a]
:[Prim]
ps) Int
maxTests
candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefnsC :: Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefnsC Args{Bool
Int
[[Expr]]
forceTests :: [[Expr]]
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f [Prim]
ps = ((Defn -> [[Defn]]) -> [[Defn]] -> [[Defn]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT Defn -> [[Defn]]
fillingsFor [[Defn]]
fss,Thy
thy)
where
pats :: [[[Expr]]]
pats = [Expr] -> String -> f -> [[[Expr]]]
forall f. Conjurable f => [Expr] -> String -> f -> [[[Expr]]]
conjurePats [Expr]
es String
nm f
f
fss :: [[Defn]]
fss = ([Expr] -> [[Defn]]) -> [[[Expr]]] -> [[Defn]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Expr] -> [[Defn]]
ps2fss [[[Expr]]]
pats
es :: [Expr]
es = (Prim -> Expr) -> [Prim] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Prim -> Expr
forall a b. (a, b) -> a
fst [Prim]
ps
eh :: Expr
eh = Expr -> Expr
holeAsTypeOf Expr
efxs
efxs :: Expr
efxs = String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f
(Expr
ef:[Expr]
exs) = Expr -> [Expr]
unfoldApp Expr
efxs
keep :: Expr -> Bool
keep = Thy -> Expr -> Bool
isRootNormalE Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
appsWith :: Expr -> [Expr] -> [[Expr]]
appsWith :: Expr -> [Expr] -> [[Expr]]
appsWith Expr
eh [Expr]
vs = Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
eh Expr -> Bool
keep ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
vs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
ps2fss :: [Expr] -> [[Defn]]
ps2fss :: [Expr] -> [[Defn]]
ps2fss [Expr]
pats = (Defn -> Bool) -> [[Defn]] -> [[Defn]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT ([Expr] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ([Expr] -> Bool) -> (Defn -> [Expr]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr) -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd) ([[Defn]] -> [[Defn]])
-> ([[Defn]] -> [[Defn]]) -> [[Defn]] -> [[Defn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Defn]] -> [[Defn]]
forall a. [[[a]]] -> [[[a]]]
products ([[Defn]] -> [[Defn]]) -> [[Defn]] -> [[Defn]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Defn]) -> [Expr] -> [[Defn]]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> [Defn]
p2eess [Expr]
pats
where
p2eess :: Expr -> [[Bndn]]
p2eess :: Expr -> [Defn]
p2eess Expr
pat = (Expr -> (Expr, Expr)) -> [[Expr]] -> [Defn]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
pat,)
([[Expr]] -> [Defn]) -> ([Expr] -> [[Expr]]) -> [Expr] -> [Defn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr] -> [[Expr]]
appsWith Expr
pat
([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. [a] -> [a]
tail
([Expr] -> [Defn]) -> [Expr] -> [Defn]
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
vars Expr
pat [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
eh | (([Expr], Expr) -> Bool) -> [([Expr], Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (([Expr] -> Expr -> Bool) -> ([Expr], Expr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Expr] -> Expr -> Bool
forall a. Eq a => [a] -> Expr -> Bool
should) ([[Expr]] -> [Expr] -> [([Expr], Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [[Expr]]
aess [Expr]
aes)]
where
should :: [a] -> Expr -> Bool
should [a]
aes Expr
ae = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
aes) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& Expr -> Bool
hasVar Expr
ae Bool -> Bool -> Bool
&& (Expr -> Bool
isApp Expr
ae Bool -> Bool -> Bool
|| Expr -> Bool
isUnbreakable Expr
ae)
aes :: [Expr]
aes = ([Expr] -> [Expr]
forall a. [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
rehole) Expr
pat
aess :: [[Expr]]
aess = [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]]
transpose ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map ([Expr] -> [Expr]
forall a. [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Expr -> Expr) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
rehole) [Expr]
pats
fillingsFor1 :: Bndn -> [[Bndn]]
fillingsFor1 :: (Expr, Expr) -> [Defn]
fillingsFor1 (Expr
ep,Expr
er) = ([Expr] -> (Expr, Expr)) -> [[[Expr]]] -> [Defn]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (\[Expr]
es -> (Expr
ep,Expr -> [Expr] -> Expr
fill Expr
er [Expr]
es))
([[[Expr]]] -> [Defn])
-> ([[Expr]] -> [[[Expr]]]) -> [[Expr]] -> [Defn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[Expr]]] -> [[[Expr]]]
forall a. [[[a]]] -> [[[a]]]
products
([[[Expr]]] -> [[[Expr]]])
-> ([[Expr]] -> [[[Expr]]]) -> [[Expr]] -> [[[Expr]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [[Expr]] -> [[[Expr]]]
forall a. Int -> a -> [a]
replicate ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> [Expr] -> Int
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
holes Expr
er)
([[Expr]] -> [Defn]) -> [[Expr]] -> [Defn]
forall a b. (a -> b) -> a -> b
$ Expr -> [[Expr]]
recs' Expr
ep
fillingsFor :: Defn -> [[Defn]]
fillingsFor :: Defn -> [[Defn]]
fillingsFor = [[Defn]] -> [[Defn]]
forall a. [[[a]]] -> [[[a]]]
products ([[Defn]] -> [[Defn]]) -> (Defn -> [[Defn]]) -> Defn -> [[Defn]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr) -> [Defn]) -> Defn -> [[Defn]]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> [Defn]
fillingsFor1
ds :: [Expr]
ds = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstructor f
f Int
maxTests) [Expr]
es
keepR :: Expr -> Expr -> Bool
keepR Expr
ep | Bool
requireDescent = (Expr -> Bool) -> Expr -> Expr -> Bool
descends (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
ds) Expr
ep
| Bool
otherwise = Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
recs :: Expr -> [[Expr]]
recs Expr
ep = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr -> Expr -> Bool
keepR Expr
ep)
([[Expr]] -> [[Expr]])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT (\Expr
e -> Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ep)
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [[Expr]]
recsV' ([Expr] -> [Expr]
forall a. [a] -> [a]
tail (Expr -> [Expr]
vars Expr
ep))
recsV :: [Expr] -> [[Expr]]
recsV [Expr]
vs = (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
vs) (Expr -> [Expr]
vars Expr
e))
([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [Expr] -> [[Expr]]
appsWith Expr
h [Expr]
vs | Expr
h <- f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
recs' :: Expr -> [[Expr]]
recs' Expr
ep = [[Expr]] -> Maybe [[Expr]] -> [[Expr]]
forall a. a -> Maybe a -> a
fromMaybe [[Expr]]
forall a. a
errRP (Maybe [[Expr]] -> [[Expr]]) -> Maybe [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ Expr -> [(Expr, [[Expr]])] -> Maybe [[Expr]]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
ep [(Expr, [[Expr]])]
eprs
where
eprs :: [(Expr, [[Expr]])]
eprs = [(Expr
ep, Expr -> [[Expr]]
recs Expr
ep) | Expr
ep <- [Expr]
possiblePats]
possiblePats :: [Expr]
possiblePats = [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort ([Expr] -> [Expr])
-> ([[[Expr]]] -> [Expr]) -> [[[Expr]]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Expr]] -> [Expr])
-> ([[[Expr]]] -> [[Expr]]) -> [[[Expr]]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[Expr]]] -> [[Expr]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[Expr]]] -> [Expr]) -> [[[Expr]]] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[[Expr]]]
pats
recsV' :: [Expr] -> [[Expr]]
recsV' [Expr]
vs = [[Expr]] -> Maybe [[Expr]] -> [[Expr]]
forall a. a -> Maybe a -> a
fromMaybe [[Expr]]
forall a. a
errRV (Maybe [[Expr]] -> [[Expr]]) -> Maybe [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [([Expr], [[Expr]])] -> Maybe [[Expr]]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Expr]
vs [([Expr], [[Expr]])]
evrs
where
evrs :: [([Expr], [[Expr]])]
evrs = [([Expr]
vs, [Expr] -> [[Expr]]
recsV [Expr]
vs) | [Expr]
vs <- [[Expr]] -> [[Expr]]
forall a. Ord a => [a] -> [a]
nubSort ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map ([Expr] -> [Expr]
forall a. [a] -> [a]
tail ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
vars) [Expr]
possiblePats]
thy :: Thy
thy = (Expr -> Expr -> Bool) -> Thy -> Thy
filterTheory Expr -> Expr -> Bool
(===)
(Thy -> Thy) -> ([Expr] -> Thy) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize ([[Expr]] -> Thy) -> ([Expr] -> [[Expr]]) -> [Expr] -> Thy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[]) ([Expr] -> [[Expr]]) -> ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub
([Expr] -> Thy) -> [Expr] -> Thy
forall a b. (a -> b) -> a -> b
$ [Prim] -> [Expr]
cjHoles (String -> f -> Prim
forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fPrim -> [Prim] -> [Prim]
forall a. a -> [a] -> [a]
:[Prim]
ps) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [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] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
=== :: Expr -> Expr -> Bool
(===) = [Prim] -> Int -> Expr -> Expr -> Bool
cjAreEqual (String -> f -> Prim
forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fPrim -> [Prim] -> [Prim]
forall a. a -> [a] -> [a]
:[Prim]
ps) Int
maxTests
isUnbreakable :: Expr -> Bool
isUnbreakable = f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
conjureIsUnbreakable f
f
errRP :: a
errRP = String -> a
forall a. HasCallStack => String -> a
error String
"candidateDefnsC: unexpected pattern. You have found a bug, please report it."
errRV :: a
errRV = String -> a
forall a. HasCallStack => String -> a
error String
"candidateDefnsC: unexpected variables. You have found a bug, please report it."
deconstructs1 :: (Expr -> Bool) -> Expr -> Expr -> Bool
deconstructs1 :: (Expr -> Bool) -> Expr -> Expr -> Bool
deconstructs1 Expr -> Bool
isDec Expr
_ Expr
e = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr -> Bool
isDeconstruction [Expr]
exs
where
(Expr
ef:[Expr]
exs) = Expr -> [Expr]
unfoldApp Expr
e
isDeconstruction :: Expr -> Bool
isDeconstruction Expr
e = Bool -> Bool
not ([Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
cs) Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isDec [Expr]
cs
where
cs :: [Expr]
cs = Expr -> [Expr]
consts Expr
e
descends :: (Expr -> Bool) -> Expr -> Expr -> Bool
descends :: (Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Bool
isDec Expr
e' Expr
e = (Defn -> Bool) -> [Defn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Defn -> Bool
forall (t :: * -> *). Foldable t => t (Expr, Expr) -> Bool
d1 [Defn]
ss
where
desc :: Defn -> Bool
desc = (Defn -> Bool) -> [Defn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Defn -> Bool
forall (t :: * -> *). Foldable t => t (Expr, Expr) -> Bool
d1 ([Defn] -> Bool) -> (Defn -> [Defn]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [Expr] -> [Defn]) -> ([Expr], [Expr]) -> [Defn]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Expr] -> [Expr] -> [Defn]
useMatches (([Expr], [Expr]) -> [Defn])
-> (Defn -> ([Expr], [Expr])) -> Defn -> [Defn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> ([Expr], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip
d1 :: t (Expr, Expr) -> Bool
d1 t (Expr, Expr)
exys = ((Expr, Expr) -> Bool) -> t (Expr, Expr) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr, Expr) -> Bool
isNotConstruction t (Expr, Expr)
exys
Bool -> Bool -> Bool
&& ((Expr, Expr) -> Bool) -> t (Expr, Expr) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr, Expr) -> Bool
isDeconstruction t (Expr, Expr)
exys
ss :: [Defn]
ss = [Defn] -> [Defn]
forall a. [a] -> [a]
init ([Defn] -> [Defn]) -> [Defn] -> [Defn]
forall a b. (a -> b) -> a -> b
$ Defn -> [Defn]
forall a. [a] -> [[a]]
sets Defn
exys
exys :: Defn
exys = [Expr] -> [Expr] -> Defn
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
exs [Expr]
eys
(Expr
_:[Expr]
exs) = Expr -> [Expr]
unfoldApp Expr
e'
(Expr
_:[Expr]
eys) = Expr -> [Expr]
unfoldApp Expr
e
isDeconstruction :: (Expr, Expr) -> Bool
isDeconstruction (Expr
p,Expr
e) | Expr -> Bool
isVar Expr
p = Bool -> Bool
not ([Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
cs) Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isDec [Expr]
cs
| Bool
otherwise = Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> Int
size Expr
p
where
cs :: [Expr]
cs = Expr -> [Expr]
consts Expr
e
isNotConstruction :: (Expr, Expr) -> Bool
isNotConstruction (Expr
p,Expr
e) | Expr -> Bool
isVar Expr
p = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isDec (Expr -> [Expr]
consts Expr
e)
| Bool
otherwise = Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr -> Int
size Expr
p
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
keepIf :: Expr -> Bool
keepIf :: Expr -> Bool
keepIf (Value String
"if" Dynamic
_ :$ Expr
ep :$ Expr
ex :$ Expr
ey)
| Expr
ex Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ey = Bool
False
| Expr -> Bool
anormal Expr
ep = Bool
False
| Bool
otherwise = case Expr -> Maybe (Expr, Expr)
binding Expr
ep of
Just (Expr
v,Expr
e) -> Expr
v Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expr -> [Expr]
values Expr
ex
Maybe (Expr, Expr)
Nothing -> Bool
True
where
anormal :: Expr -> Bool
anormal (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e2 Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e1 = Bool
True
anormal Expr
_ = Bool
False
binding :: Expr -> Maybe (Expr,Expr)
binding :: Expr -> Maybe (Expr, Expr)
binding (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e1 = (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
e1,Expr
e2)
| Expr -> Bool
isVar Expr
e2 = (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
e2,Expr
e1)
binding Expr
_ = Maybe (Expr, Expr)
forall a. Maybe a
Nothing
keepIf Expr
_ = String -> Bool
forall a. HasCallStack => String -> a
error String
"Conjure.Engine.keepIf: not an if"
isRootNormal :: Thy -> Expr -> Bool
isRootNormal :: Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e = [(Expr, Defn, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Expr, Defn, Expr)] -> Bool) -> [(Expr, Defn, Expr)] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Triexpr Expr -> [(Expr, Defn, Expr)]
forall a. Expr -> Triexpr a -> [(Expr, Defn, a)]
T.lookup Expr
e Triexpr Expr
trie
where
trie :: Triexpr Expr
trie = Defn -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList (Thy -> Defn
rules Thy
thy)
isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e = Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e
Bool -> Bool -> Bool
&& [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) [Expr
e2 Expr -> Defn -> Expr
//- Defn
bs | (Expr
_,Defn
bs,Expr
e2) <- Expr -> Triexpr Expr -> [(Expr, Defn, Expr)]
forall a. Expr -> Triexpr a -> [(Expr, Defn, a)]
T.lookup Expr
e Triexpr Expr
trie])
where
trie :: Triexpr Expr
trie = Defn -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList (Defn -> Triexpr Expr) -> Defn -> Triexpr Expr
forall a b. (a -> b) -> a -> b
$ Thy -> Defn
equations Thy
thy Defn -> Defn -> Defn
forall a. [a] -> [a] -> [a]
++ ((Expr, Expr) -> (Expr, Expr)) -> Defn -> Defn
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> (Expr, Expr)
forall a b. (a, b) -> (b, a)
swap (Thy -> Defn
equations Thy
thy)
->- :: Expr -> Expr -> Bool
(->-) = Thy -> Expr -> Expr -> Bool
canReduceTo Thy
thy
filtered :: Thy -> Bool
filtered :: Thy -> Bool
filtered = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0) (Int -> Bool) -> (Thy -> Int) -> Thy -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thy -> Int
closureLimit
filterTheory :: (Expr -> Expr -> Bool) -> Thy -> Thy
filterTheory :: (Expr -> Expr -> Bool) -> Thy -> Thy
filterTheory Expr -> Expr -> Bool
(===) Thy
thy = Thy
thy
{ rules :: Defn
rules = Defn
rs
, equations :: Defn
equations = Defn
es
, closureLimit :: Int
closureLimit = if Bool
r' Bool -> Bool -> Bool
&& Bool
e'
then Thy -> Int
closureLimit Thy
thy
else -Int
1
}
where
correct :: (Expr, Expr) -> Bool
correct = (Expr -> Expr -> Bool) -> (Expr, Expr) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
(===)
(Defn
rs,Bool
r') = ((Expr, Expr) -> Bool) -> Defn -> (Defn, Bool)
forall a. (a -> Bool) -> [a] -> ([a], Bool)
filterAnd (Expr, Expr) -> Bool
correct (Thy -> Defn
rules Thy
thy)
(Defn
es,Bool
e') = ((Expr, Expr) -> Bool) -> Defn -> (Defn, Bool)
forall a. (a -> Bool) -> [a] -> ([a], Bool)
filterAnd (Expr, Expr) -> Bool
correct (Thy -> Defn
equations Thy
thy)
productsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
productsWith :: ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f = ([a] -> a) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT [a] -> a
f ([[[a]]] -> [[a]]) -> ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[a]]] -> [[[a]]]
forall a. [[[a]]] -> [[[a]]]
products
delayedProductsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
delayedProductsWith :: ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith [a] -> a
f [[[a]]]
xsss = ([a] -> a) -> [[[a]]] -> [[a]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f [[[a]]]
xsss [[a]] -> Int -> [[a]]
forall a. [[a]] -> Int -> [[a]]
`addWeight` [[[a]]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
xsss
foldAppProducts :: Expr -> [ [[Expr]] ] -> [[Expr]]
foldAppProducts :: Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef = ([Expr] -> Expr) -> [[[Expr]]] -> [[Expr]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith ([Expr] -> Expr
foldApp ([Expr] -> Expr) -> ([Expr] -> [Expr]) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:))