{-# 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)
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 -> [[Expr]]
forceTests :: [[Expr]]
}
args :: Args
args :: Args
args = Args :: Int -> Int -> Int -> Int -> Int -> Bool -> [[Expr]] -> Args
Args
{ maxTests :: Int
maxTests = Int
60
, 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
, 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"
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]]
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
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 -> 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]]
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
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, Expr) -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd (Defn -> [Expr]) -> Defn -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> Int -> [Expr] -> Defn
forall f. Conjurable f => f -> Int -> [Expr] -> Defn
deconstructors 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) -> 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]]
requireDescent :: Bool
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
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
fss :: [[Defn]]
fss = ([Expr] -> [[Defn]]) -> [[[Expr]]] -> [[Defn]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Expr] -> [[Defn]]
ps2fss ([Expr] -> String -> f -> [[[Expr]]]
forall f. Conjurable f => [Expr] -> String -> f -> [[[Expr]]]
conjurePats [Expr]
es String
nm f
f)
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] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
pats Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1, (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr -> Bool
should [Expr]
aes]
where
should :: Expr -> Bool
should Expr
ae = Expr -> Bool
hasVar Expr
ae Bool -> Bool -> Bool
&& (Expr -> Bool
isApp Expr
ae Bool -> Bool -> Bool
|| Expr -> Bool
isUnbreakable Expr
ae)
(Expr
_:[Expr]
aes) = Expr -> [Expr]
unfoldApp Expr
pat
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] -> [[Expr]]
recs Expr
ep [Expr]
es
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
recs :: Expr -> [Expr] -> [[Expr]]
recs Expr
ep [Expr]
es = (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 -> 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] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es) | Expr
h <- f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
where
vs :: [Expr]
vs = [Expr] -> [Expr]
forall a. [a] -> [a]
tail (Expr -> [Expr]
vars Expr
ep)
thy :: Thy
thy = (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
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
d1 [Defn]
ss
where
d1 :: Defn -> Bool
d1 Defn
exys = Expr -> [Expr]
nubVars ([Expr] -> Expr
foldApp [Expr]
exs) [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> [Expr]
nubVars ([Expr] -> Expr
foldApp [Expr]
eys)
Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isNotConstruction [Expr]
eys
Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr -> Bool
isDeconstruction [Expr]
eys
where
exs :: [Expr]
exs = ((Expr, Expr) -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst Defn
exys
eys :: [Expr]
eys = ((Expr, Expr) -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd Defn
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 -> 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
isNotConstruction :: Expr -> Bool
isNotConstruction Expr
e = (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
deconstructors :: Conjurable f => f -> Int -> [Expr] -> [(Expr, Expr)]
deconstructors :: f -> Int -> [Expr] -> Defn
deconstructors f
f Int
maxTests [Expr]
es =
[ (Expr
z, Expr
d)
| Expr
d <- [Expr]
es
, Expr
h <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 [Expr
h | Expr
h <- [Expr]
hs, Expr -> Maybe TypeRep
mtyp (Expr
d Expr -> Expr -> Expr
:$ Expr
h) Maybe TypeRep -> Maybe TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe TypeRep
mtyp Expr
h]
, Expr
z <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 [Expr
z | Expr
z <- [Expr]
es2, Expr -> Maybe TypeRep
mtyp (Expr
z Expr -> Expr -> Expr
:$ Expr
h) Maybe TypeRep -> Maybe TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe TypeRep
mtyp Expr
b Bool -> Bool -> Bool
&& Expr -> Expr -> Expr -> Bool
isDeconstructor Expr
h Expr
z Expr
d]
]
where
b :: Expr
b = Bool -> Expr
forall a. Typeable a => a -> Expr
hole (Bool
forall a. HasCallStack => a
undefined :: Bool)
hs :: [Expr]
hs = [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> [Expr]
forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f
isDeconstructor :: Expr -> Expr -> Expr -> Bool
isDeconstructor = f -> Int -> Expr -> Expr -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Expr -> Expr -> Bool
conjureIsDeconstructor f
f Int
maxTests
es2 :: [Expr]
es2 = [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2 | Expr
e1 <- [Expr]
es, Expr
e2 <- [Expr]
es, Expr -> Bool
isWellTyped (Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2)]
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
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]
:))