{-# LANGUAGE CPP, RecordWildCards, TupleSections #-}
module Conjure.Engine
( conjure
, conjureWithMaxSize
, Args(..)
, args
, conjureWith
, conjureFromSpec
, conjureFromSpecWith
, conjure0
, conjure0With
, conjpure
, conjpureWith
, conjpureFromSpec
, conjpureFromSpecWith
, conjpure0
, conjpure0With
, 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 Data.Dynamic (fromDyn, dynApp)
import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
import Test.Speculate.Reason (Thy, rules, equations, invalid, canReduceTo, printThy, closureLimit, doubleCheck)
import Test.Speculate.Engine (theoryFromAtoms, grounds, 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
conjureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> IO ()
conjureFromSpec :: String -> (f -> Bool) -> [Prim] -> IO ()
conjureFromSpec = Args -> String -> (f -> Bool) -> [Prim] -> IO ()
forall f.
Conjurable f =>
Args -> String -> (f -> Bool) -> [Prim] -> IO ()
conjureFromSpecWith Args
args
conjure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0 :: String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0 = Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
forall f.
Conjurable f =>
Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With 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 -> Int
maxDeconstructionSize :: Int
, Args -> Bool
requireDescent :: Bool
, Args -> Bool
usePatterns :: Bool
, Args -> Bool
showTheory :: Bool
, Args -> Bool
uniqueCandidates :: Bool
}
args :: Args
args :: Args
args = Args :: Int
-> Int
-> Int
-> Int
-> Int
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> 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
, maxDeconstructionSize :: Int
maxDeconstructionSize = Int
4
, requireDescent :: Bool
requireDescent = Bool
True
, usePatterns :: Bool
usePatterns = Bool
True
, showTheory :: Bool
showTheory = Bool
False
, uniqueCandidates :: Bool
uniqueCandidates = Bool
False
}
conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureWith :: Args -> String -> f -> [Prim] -> IO ()
conjureWith Args
args String
nm f
f = Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
forall f.
Conjurable f =>
Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With Args
args String
nm f
f (Bool -> f -> Bool
forall a b. a -> b -> a
const Bool
True)
conjureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> IO ()
conjureFromSpecWith :: Args -> String -> (f -> Bool) -> [Prim] -> IO ()
conjureFromSpecWith Args
args String
nm f -> Bool
p = Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
forall f.
Conjurable f =>
Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With Args
args String
nm f
forall a. HasCallStack => a
undefined f -> Bool
p
conjure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With :: Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With Args
args String
nm f
f f -> Bool
p [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)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (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
"-- 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 (Bool -> Bool
not (Bool -> Bool) -> ([Equation] -> Bool) -> [Equation] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Equation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Equation] -> Bool) -> [Equation] -> Bool
forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
invalid 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 "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Equation] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
invalid Thy
thy)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" incorrect properties,"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" please re-run with more tests for faster results"
Integer -> Int -> [([[Equation]], [[Equation]])] -> IO ()
forall t.
(Show t, Num t) =>
t -> Int -> [([[Equation]], [[Equation]])] -> IO ()
pr Integer
1 Int
0 [([[Equation]], [[Equation]])]
rs
where
pr :: t -> Int -> [([[Equation]], [[Equation]])] -> IO ()
pr t
n Int
t [] = do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- tested " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"cannot conjure\n"
pr t
n Int
t (([[Equation]]
is,[[Equation]]
cs):[([[Equation]], [[Equation]])]
rs) = do
let nc :: Int
nc = [[Equation]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Equation]]
cs
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 Int
nc 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 [[Equation]]
is of
[] -> t -> Int -> [([[Equation]], [[Equation]])] -> IO ()
pr (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nc) [([[Equation]], [[Equation]])]
rs
([Equation]
i:[[Equation]]
_) -> do let nc' :: Int
nc' = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
nc (([Equation] -> Bool) -> [[Equation]] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ([Equation]
i[Equation] -> [Equation] -> Bool
forall a. Eq a => a -> a -> Bool
==) [[Equation]]
cs)
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- tested " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nc'Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates"
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [Equation] -> String
showDefn [Equation]
i
rs :: [([[Equation]], [[Equation]])]
rs = [[[Equation]]] -> [[[Equation]]] -> [([[Equation]], [[Equation]])]
forall a b. [a] -> [b] -> [(a, b)]
zip [[[Equation]]]
iss [[[Equation]]]
css
([[[Equation]]]
iss, [[[Equation]]]
css, [Expr]
ts, Thy
thy) = Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args String
nm f
f f -> Bool
p [Prim]
es
nRules :: Int
nRules = [Equation] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
rules Thy
thy)
nREs :: Int
nREs = [Equation] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
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] -> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure = Args
-> String
-> f
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpureWith Args
args
conjpureFromSpec :: Conjurable f => String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureFromSpec :: String
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpureFromSpec = Args
-> String
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpureFromSpecWith Args
args
conjpure0 :: Conjurable f => String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpure0 :: String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0 = Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args
conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureWith :: Args
-> String
-> f
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpureWith Args
args String
nm f
f = Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args String
nm f
f (Bool -> f -> Bool
forall a b. a -> b -> a
const Bool
True)
conjpureFromSpecWith :: Conjurable f => Args -> String -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpureFromSpecWith :: Args
-> String
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpureFromSpecWith Args
args String
nm f -> Bool
p = Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args String
nm f
forall a. HasCallStack => a
undefined f -> Bool
p
conjpure0With :: Conjurable f => Args -> String -> f -> (f -> Bool) -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
conjpure0With :: Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With args :: Args
args@(Args{Bool
Int
uniqueCandidates :: Bool
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxDeconstructionSize :: Args -> Int
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..}) String
nm f
f f -> Bool
p [Prim]
es = ([[[Equation]]]
implementationsT, [[[Equation]]]
candidatesT, [Expr]
tests, Thy
thy)
where
tests :: [Expr]
tests = [Expr
ffxx Expr -> [Equation] -> Expr
//- [Equation]
bs | [Equation]
bs <- [[Equation]]
dbss]
implementationsT :: [[[Equation]]]
implementationsT = ([Equation] -> Bool) -> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT [Equation] -> Bool
implements [[[Equation]]]
candidatesT
implements :: [Equation] -> Bool
implements [Equation]
fx = [Equation] -> Bool
defnApparentlyTerminates [Equation]
fx
Bool -> Bool -> Bool
&& [Equation] -> Expr -> Expr -> Bool
requal [Equation]
fx Expr
ffxx Expr
vffxx
Bool -> Bool -> Bool
&& Bool -> Bool
errorToFalse (f -> Bool
p (Int -> [Equation] -> f
forall f. Conjurable f => Int -> [Equation] -> f
cevl Int
maxEvalRecursions [Equation]
fx))
candidatesT :: [[[Equation]]]
candidatesT = (if Bool
uniqueCandidates then Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
forall f.
Conjurable f =>
Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
nubCandidates Args
args String
nm f
f else [[[Equation]]] -> [[[Equation]]]
forall a. a -> a
id)
([[[Equation]]] -> [[[Equation]]])
-> [[[Equation]]] -> [[[Equation]]]
forall a b. (a -> b) -> a -> b
$ Int -> [[[Equation]]] -> [[[Equation]]]
forall a. Int -> [a] -> [a]
take Int
maxSize [[[Equation]]]
candidatesTT
([[[Equation]]]
candidatesTT, Thy
thy) = Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], 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 :: [Equation] -> Expr -> Expr -> Bool
requal [Equation]
dfn Expr
e1 Expr
e2 = [Equation] -> Expr -> Bool
isTrueWhenDefined [Equation]
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 :: [Equation] -> Expr -> Bool
isTrueWhenDefined [Equation]
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 -> [Equation] -> Bool -> Expr -> Bool
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> [Equation] -> a -> Expr -> a
deval (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions [Equation]
dfn Bool
False)
([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ ([Equation] -> Expr) -> [[Equation]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e Expr -> [Equation] -> Expr
//-) [[Equation]]
dbss
bss, dbss :: [[(Expr,Expr)]]
bss :: [[Equation]]
bss = Int -> [[Equation]] -> [[Equation]]
forall a. Int -> [a] -> [a]
take Int
maxSearchTests ([[Equation]] -> [[Equation]]) -> [[Equation]] -> [[Equation]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [[Equation]]
groundBinds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) Expr
ffxx
dbss :: [[Equation]]
dbss = Int -> [[Equation]] -> [[Equation]]
forall a. Int -> [a] -> [a]
take Int
maxTests [[Equation]
bs | [Equation]
bs <- [[Equation]]
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 -> [Equation] -> Expr
//- [Equation]
bs]
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) -> ([Equation] -> Int) -> [Equation] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Equation] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Equation] -> String) -> [Equation] -> String
forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
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) -> ([Equation] -> Int) -> [Equation] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Equation] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Equation] -> String) -> [Equation] -> String
forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
equations Thy
thy) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" equations"
Thy -> IO ()
printThy Thy
thy
where
([[[Equation]]]
_, [[[Equation]]]
_, [Expr]
_, Thy
thy) = Args
-> String
-> f
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
forall f.
Conjurable f =>
Args
-> String
-> f
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [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] -> ([[[Equation]]], Thy)
candidateDefns Args
args = Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns' Args
args
where
candidateDefns' :: Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns' = if Args -> Bool
usePatterns Args
args
then Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefnsC
else Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns1
nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]
nubCandidates :: Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
nubCandidates Args{Bool
Int
uniqueCandidates :: Bool
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxDeconstructionSize :: Args -> Int
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f = ([Equation] -> [Equation] -> Bool)
-> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> a -> Bool) -> [[a]] -> [[a]]
discardLaterT [Equation] -> [Equation] -> Bool
(===)
where
err :: a
err = String -> a
forall a. HasCallStack => String -> a
error String
"nubCandidates: unexpected evaluation error."
eq :: Dynamic
eq = f -> Dynamic
forall f. Conjurable f => f -> Dynamic
conjureDynamicEq f
f
[Equation]
d1 === :: [Equation] -> [Equation] -> Bool
=== [Equation]
d2 = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
are ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
maxTests ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) (String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f)
where
are :: Expr -> Bool
are :: Expr -> Bool
are Expr
e = Bool -> Bool
errorToFalse
(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Dynamic -> Bool -> Bool
forall a. Typeable a => Dynamic -> a -> a
`fromDyn` Bool
forall a. a
err)
(Dynamic -> Bool) -> Dynamic -> Bool
forall a b. (a -> b) -> a -> b
$ Dynamic
eq Dynamic -> Dynamic -> Dynamic
`dynApp` Dynamic -> Maybe Dynamic -> Dynamic
forall a. a -> Maybe a -> a
fromMaybe Dynamic
forall a. a
err ((Expr -> Expr) -> Int -> [Equation] -> Expr -> Maybe Dynamic
toDynamicWithDefn (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions [Equation]
d1 Expr
e)
Dynamic -> Dynamic -> Dynamic
`dynApp` Dynamic -> Maybe Dynamic -> Dynamic
forall a. a -> Maybe a -> a
fromMaybe Dynamic
forall a. a
err ((Expr -> Expr) -> Int -> [Equation] -> Expr -> Maybe Dynamic
toDynamicWithDefn (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions [Equation]
d2 Expr
e)
candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns1 :: Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns1 Args
args String
nm f
f [Prim]
ps = ([[Expr]] -> [[[Equation]]])
-> ([[Expr]], Thy) -> ([[[Equation]]], Thy)
forall t a b. (t -> a) -> (t, b) -> (a, b)
mapFst ((Expr -> [Equation]) -> [[Expr]] -> [[[Equation]]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT Expr -> [Equation]
forall b. b -> [(Expr, b)]
toDefn) (([[Expr]], Thy) -> ([[[Equation]]], Thy))
-> ([[Expr]], Thy) -> ([[[Equation]]], 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
uniqueCandidates :: Bool
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxDeconstructionSize :: Args -> Int
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 -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
efxs
| Bool
otherwise = Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
where
Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e' = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
[ ()
| Expr
d <- [Expr]
deconstructions
, [Equation]
m <- Maybe [Equation] -> [[Equation]]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Equation]
`match` Expr
d)
, (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> Equation -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) [Equation]
m [Equation] -> [Equation] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Expr -> Expr
holeAsTypeOf Expr
e', Expr
e')]
]
deconstructions :: [Expr]
deconstructions :: [Expr]
deconstructions = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFrom
([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[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
. Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT Expr -> [[Expr]]
forN [[Expr]
hs]
where
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
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
doubleCheck 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] -> ([[[Equation]]], Thy)
candidateDefnsC Args{Bool
Int
uniqueCandidates :: Bool
showTheory :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
requireDescent :: Args -> Bool
maxDeconstructionSize :: Args -> Int
maxSearchTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f [Prim]
ps = (([Equation] -> [[[Equation]]]) -> [[[Equation]]] -> [[[Equation]]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Equation] -> [[[Equation]]]
fillingsFor [[[Equation]]]
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 :: [[[Equation]]]
fss = ([Expr] -> [[[Equation]]]) -> [[[Expr]]] -> [[[Equation]]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Expr] -> [[[Equation]]]
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
isRootNormal 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] -> [[[Equation]]]
ps2fss [Expr]
pats = ([Equation] -> Bool) -> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT ([Expr] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ([Expr] -> Bool) -> ([Equation] -> [Expr]) -> [Equation] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> Expr) -> [Equation] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> Expr
forall a b. (a, b) -> b
snd) ([[[Equation]]] -> [[[Equation]]])
-> ([[[Equation]]] -> [[[Equation]]])
-> [[[Equation]]]
-> [[[Equation]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[Equation]]] -> [[[Equation]]]
forall a. [[[a]]] -> [[[a]]]
products ([[[Equation]]] -> [[[Equation]]])
-> [[[Equation]]] -> [[[Equation]]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Equation]]) -> [Expr] -> [[[Equation]]]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> [[Equation]]
p2eess [Expr]
pats
where
p2eess :: Expr -> [[Bndn]]
p2eess :: Expr -> [[Equation]]
p2eess Expr
pat = (Expr -> Equation) -> [[Expr]] -> [[Equation]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
pat,)
([[Expr]] -> [[Equation]])
-> ([Expr] -> [[Expr]]) -> [Expr] -> [[Equation]]
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] -> [[Equation]]) -> [Expr] -> [[Equation]]
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 :: Equation -> [[Equation]]
fillingsFor1 (Expr
ep,Expr
er) = ([Expr] -> Equation) -> [[[Expr]]] -> [[Equation]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (\[Expr]
es -> (Expr
ep,Expr -> [Expr] -> Expr
fill Expr
er [Expr]
es))
([[[Expr]]] -> [[Equation]])
-> ([[Expr]] -> [[[Expr]]]) -> [[Expr]] -> [[Equation]]
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]] -> [[Equation]]) -> [[Expr]] -> [[Equation]]
forall a b. (a -> b) -> a -> b
$ Expr -> [[Expr]]
recs' Expr
ep
fillingsFor :: Defn -> [[Defn]]
fillingsFor :: [Equation] -> [[[Equation]]]
fillingsFor = [[[Equation]]] -> [[[Equation]]]
forall a. [[[a]]] -> [[[a]]]
products ([[[Equation]]] -> [[[Equation]]])
-> ([Equation] -> [[[Equation]]]) -> [Equation] -> [[[Equation]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Equation -> [[Equation]]) -> [Equation] -> [[[Equation]]]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> [[Equation]]
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 -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
ep
| Bool
otherwise = Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
where
Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e' = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
[ ()
| Expr
d <- [Expr]
deconstructions
, [Equation]
m <- Maybe [Equation] -> [[Equation]]
forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Equation]
`match` Expr
d)
, (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Expr -> Bool) -> Equation -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) [Equation]
m [Equation] -> [Equation] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Expr -> Expr
holeAsTypeOf Expr
e', Expr
e')]
]
deconstructions :: [Expr]
deconstructions :: [Expr]
deconstructions = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (f -> Int -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFrom
([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [[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
. Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
([[Expr]] -> [Expr]) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [Expr] -> [[Expr]]
`appsWith` Expr -> [Expr]
vars Expr
ep) [[Expr]
hs]
where
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
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
doubleCheck 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 -> Expr -> Bool) -> Expr -> Expr -> Bool
descends :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
e' Expr
e = ([Equation] -> Bool) -> [[Equation]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any [Equation] -> Bool
forall (t :: * -> *). Foldable t => t Equation -> Bool
d1 [[Equation]]
ss
where
desc :: [Equation] -> Bool
desc = ([Equation] -> Bool) -> [[Equation]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any [Equation] -> Bool
forall (t :: * -> *). Foldable t => t Equation -> Bool
d1 ([[Equation]] -> Bool)
-> ([Equation] -> [[Equation]]) -> [Equation] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Expr] -> [Expr] -> [[Equation]])
-> ([Expr], [Expr]) -> [[Equation]]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Expr] -> [Expr] -> [[Equation]]
useMatches (([Expr], [Expr]) -> [[Equation]])
-> ([Equation] -> ([Expr], [Expr])) -> [Equation] -> [[Equation]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Equation] -> ([Expr], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip
d1 :: t Equation -> Bool
d1 t Equation
exys = (Equation -> Bool) -> t Equation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Equation -> Bool
isNotConstruction t Equation
exys
Bool -> Bool -> Bool
&& (Equation -> Bool) -> t Equation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Equation -> Bool
isDeconstruction t Equation
exys
ss :: [[Equation]]
ss = [[Equation]] -> [[Equation]]
forall a. [a] -> [a]
init ([[Equation]] -> [[Equation]]) -> [[Equation]] -> [[Equation]]
forall a b. (a -> b) -> a -> b
$ [Equation] -> [[Equation]]
forall a. [a] -> [[a]]
sets [Equation]
exys
exys :: [Equation]
exys = [Expr] -> [Expr] -> [Equation]
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 :: Equation -> Bool
isDeconstruction (Expr
p,Expr
e) | Expr -> Bool
isVar Expr
p = Expr
e Expr -> Expr -> Bool
`isDecOf` Expr
p
| 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 :: Equation -> Bool
isNotConstruction (Expr
p,Expr
e) | Expr -> Bool
isVar Expr
p = Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
p Bool -> Bool -> Bool
|| Expr
e Expr -> Expr -> Bool
`isDecOf` Expr
p
| Bool
otherwise = Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Expr -> Int
size Expr
p
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 Equation
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 Equation
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 Equation
binding (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e1 = Equation -> Maybe Equation
forall a. a -> Maybe a
Just (Expr
e1,Expr
e2)
| Expr -> Bool
isVar Expr
e2 = Equation -> Maybe Equation
forall a. a -> Maybe a
Just (Expr
e2,Expr
e1)
binding Expr
_ = Maybe Equation
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, [Equation], Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Expr, [Equation], Expr)] -> Bool)
-> [(Expr, [Equation], Expr)] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Triexpr Expr -> [(Expr, [Equation], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [Equation], a)]
T.lookup Expr
e Triexpr Expr
trie
where
trie :: Triexpr Expr
trie = [Equation] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList (Thy -> [Equation]
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 -> [Equation] -> Expr
//- [Equation]
bs | (Expr
_,[Equation]
bs,Expr
e2) <- Expr -> Triexpr Expr -> [(Expr, [Equation], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [Equation], a)]
T.lookup Expr
e Triexpr Expr
trie])
where
trie :: Triexpr Expr
trie = [Equation] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList ([Equation] -> Triexpr Expr) -> [Equation] -> Triexpr Expr
forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
equations Thy
thy [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ (Equation -> Equation) -> [Equation] -> [Equation]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> Equation
forall a b. (a, b) -> (b, a)
swap (Thy -> [Equation]
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]
:))