-- |
-- Module      : Conjure.Engine
-- Copyright   : (c) 2021 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- An internal module of "Conjure",
-- a library for Conjuring function implementations
-- from tests or partial definitions.
-- (a.k.a.: functional inductive programming)
{-# 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


-- | Conjures an implementation of a partially defined function.
--
-- Takes a 'String' with the name of a function,
-- a partially-defined function from a conjurable type,
-- and a list of building blocks encoded as 'Expr's.
--
-- For example, given:
--
-- > square :: Int -> Int
-- > square 0  =  0
-- > square 1  =  1
-- > square 2  =  4
-- >
-- > primitives :: [Prim]
-- > primitives =
-- >   [ pr (0::Int)
-- >   , pr (1::Int)
-- >   , prim "+" ((+) :: Int -> Int -> Int)
-- >   , prim "*" ((*) :: Int -> Int -> Int)
-- >   ]
--
-- The conjure function does the following:
--
-- > > conjure "square" square primitives
-- > square :: Int -> Int
-- > -- pruning with 14/25 rules
-- > -- testing 3 combinations of argument values
-- > -- looking through 3 candidates of size 1
-- > -- looking through 3 candidates of size 2
-- > -- looking through 5 candidates of size 3
-- > square x  =  x * x
--
-- The primitives list is defined with 'pr' and 'prim'.
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


-- | Conjures an implementation from a function specification.
--
-- This function works like 'conjure' but instead of receiving a partial definition
-- it receives a boolean filter / property about the function.
--
-- For example, given:
--
-- > squareSpec :: (Int -> Int) -> Bool
-- > squareSpec square  =  square 0 == 0
-- >                    && square 1 == 1
-- >                    && square 2 == 4
--
-- Then:
--
-- > > conjureFromSpec "square" squareSpec primitives
-- > square :: Int -> Int
-- > -- pruning with 14/25 rules
-- > -- looking through 3 candidates of size 1
-- > -- looking through 4 candidates of size 2
-- > -- looking through 9 candidates of size 3
-- > square x  =  x * x
--
-- This allows users to specify QuickCheck-style properties,
-- here is an example using LeanCheck:
--
-- > import Test.LeanCheck (holds, exists)
-- >
-- > squarePropertySpec :: (Int -> Int) -> Bool
-- > squarePropertySpec square  =  and
-- >   [ holds n $ \x -> square x >= x
-- >   , holds n $ \x -> square x >= 0
-- >   , exists n $ \x -> square x > x
-- >   ]  where  n = 60
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


-- | Synthesizes an implementation from both a partial definition and a
--   function specification.
--
--   This works like the functions 'conjure' and 'conjureFromSpec' combined.
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


-- | Like 'conjure' but allows setting the maximum size of considered expressions
--   instead of the default value of 12.
--
-- > conjureWithMaxSize 10 "function" function [...]
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)
                       }


-- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.
--   See 'args' for the defaults.
data Args = Args
  { Args -> Int
maxTests              :: Int  -- ^ maximum number of tests to each candidate
  , Args -> Int
maxSize               :: Int  -- ^ maximum size of candidate bodies
  , Args -> Int
maxEvalRecursions     :: Int  -- ^ maximum number of recursive evaluations when testing candidates
  , Args -> Int
maxEquationSize       :: Int  -- ^ maximum size of equation operands
  , Args -> Int
maxSearchTests        :: Int  -- ^ maximum number of tests to search for defined values
  , Args -> Int
maxDeconstructionSize :: Int  -- ^ maximum size of deconstructions (e.g.: @_ - 1@)
  , Args -> Bool
requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments
  , Args -> Bool
usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates
  , Args -> Bool
showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
  , Args -> Bool
uniqueCandidates      :: Bool -- ^ unique-modulo-testing candidates
  }


-- | Default arguments to conjure.
--
-- * 60 tests
-- * functions of up to 12 symbols
-- * maximum of one recursive call allowed in candidate bodies
-- * maximum evaluation of up to 60 recursions
-- * pruning with equations up to size 5
-- * search for defined applications for up to 100000 combinations
-- * require recursive calls to deconstruct arguments
-- * don't show the theory used in pruning
-- * do not make candidates unique module testing
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
  }


-- | Like 'conjure' but allows setting options through 'Args'/'args'.
--
-- > conjureWith args{maxSize = 11} "function" function [...]
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)

-- | Like 'conjureFromSpec' but allows setting options through 'Args'/'args'.
--
-- > conjureFromSpecWith args{maxSize = 11} "function" spec [...]
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

-- | Like 'conjure0' but allows setting options through 'Args'/'args'.
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
    -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs
    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


-- | Like 'conjure' but in the pure world.
--
-- Returns a quadruple with:
--
-- 1. tiers of implementations
-- 2. tiers of candidates
-- 3. a list of tests
-- 4. the underlying theory
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

-- | Like 'conjureFromSpec' but in the pure world.  (cf. 'conjpure')
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

-- | Like 'conjure0' but in the pure world.  (cf. 'conjpure')
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

-- | Like 'conjpure' but allows setting options through 'Args' and '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)

-- | Like 'conjureFromSpecWith' but in the pure world.  (cf. 'conjpure')
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

-- | Like 'conjpure0' but allows setting options through 'Args' and 'args'.
--
-- This is where the actual implementation resides.  The functions
-- 'conjpure', 'conjpureWith', 'conjpureFromSpec', 'conjpureFromSpecWith',
-- 'conjure', 'conjureWith', 'conjureFromSpec', 'conjureFromSpecWith' and
-- 'conjure0' all refer to this.
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


-- | Just prints the underlying theory found by "Test.Speculate"
--   without actually synthesizing a function.
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


-- | Like 'conjureTheory' but allows setting options through '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


-- | Return apparently unique candidate definitions.
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 -- silences errors, ok since this is for optional measuring of optimal pruning
           (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)


-- | Return apparently unique candidate definitions
--   where there is a single body.
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)]


-- | Return apparently unique candidate bodies.
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

-- | Return apparently unique candidate definitions
--   using pattern matching.
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]
  -- like recs, but memoized
  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
  -- like recsV, but memoized
  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."


-- | Returns whether the given recursive call
--   deconstructs one of its arguments.
--
-- > > deconstructs1 ... (factorial' (dec' xx))
-- > True
--
-- > > deconstructs1 ... (factorial' (xx -+- one))
-- > False
--
-- > > deconstructs1 ... (xxs -++- yys)
-- > False
--
-- > > deconstructs1 ... (xxs -++- tail' yys)
-- > True
--
-- > > deconstructs1 ... (zero-:-xxs -++- tail' yys)
-- > True
--
-- 'deconstructs1' implies 'descends'.
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

-- | Returns whether a non-empty subset of arguments
--   descends arguments by deconstruction.
--
-- > > descends isDec (xxs -++- yys) (xxs -++- tail' yys)
-- > True
--
-- > > descends isDec (xxs -++- yys) (xxs -++- yys)
-- > False
--
-- > > descends isDec (xxs -++- yys) (head' xxs -:- tail xxs  -++-  head' yys -:- tail yys)
-- > False

-- > > descends isDec (xxs -\/- yys) (yys -\/- tail' xxs)
-- > True
--
-- The following are not so obvious:
--
-- > > descends isDec (xxs -++- yys) (tail' yys -++- yys)
-- > False
--
-- > > descends isDec (xxs -++- yys) (xx-:-xxs -++- tail' yys)
-- > True
--
-- For all possible sets of arguments (2^n - 1 elements: 1 3 7 15 31),
-- see if any projects the same variables while only using deconstructions
-- and where there is at least a single deconstruction.
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 -- TODO: allow filter and id somehow
-- TODO: improve this function with better isNotConstruction


-- hardcoded filtering rules

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"



--- normality checks ---

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


--- tiers utils ---

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
-- TODO: move to LeanCheck?

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
-- TODO: move to LeanCheck?

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]
:))