-- |
-- Module      : Conjure.Engine
-- Copyright   : (c) 2021-2024 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 Conjure.Reason
  )
where

import Control.Monad (when)

import Data.Express
import Data.Express.Fixtures hiding ((-==-))

import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToFalse)
import Test.LeanCheck.Utils (classifyOn)

import Conjure.Expr
import Conjure.Conjurable
import Conjure.Prim
import Conjure.Defn
import Conjure.Defn.Redundancy
import Conjure.Defn.Test
import Conjure.Red
import Conjure.Reason


-- | 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 :: forall f. Conjurable f => 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 :: forall f. Conjurable f => 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 :: forall f.
Conjurable f =>
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 :: forall f. Conjurable f => 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 = sz
                       ,  maxEquationSize = min sz (maxEquationSize 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@)

  -- advanced options --
  , Args -> Bool
carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate
  , Args -> Bool
showTheory            :: Bool -- ^ show theory discovered by Speculate used in pruning
  , Args -> Bool
usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates

  -- pruning options --
  , Args -> Bool
rewriting             :: Bool -- ^ unique-modulo-rewriting candidates
  , Args -> Bool
requireDescent        :: Bool -- ^ require recursive calls to deconstruct arguments
  , Args -> Bool
adHocRedundancy       :: Bool -- ^ ad-hoc redundancy checks
  , Args -> Bool
copyBindings          :: Bool -- ^ copy partial definition bindings in candidates
  , Args -> Bool
atomicNumbers         :: Bool -- ^ restrict constant/ground numeric expressions to atoms
  , 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
  { 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

  -- advanced options --
  , carryOn :: Bool
carryOn                =  Bool
False
  , showTheory :: Bool
showTheory             =  Bool
False
  , usePatterns :: Bool
usePatterns            =  Bool
True

  -- pruning options --
  , rewriting :: Bool
rewriting              =  Bool
True
  , requireDescent :: Bool
requireDescent         =  Bool
True
  , adHocRedundancy :: Bool
adHocRedundancy        =  Bool
True
  , copyBindings :: Bool
copyBindings           =  Bool
True
  , atomicNumbers :: Bool
atomicNumbers          =  Bool
True
  , 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 :: forall f. Conjurable f => 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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
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. HasCallStack => [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 a. [a] -> 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 a. [a] -> 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 a. [a] -> 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
$ do
    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 a. [a] -> 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"
    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
"{-"
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"invalid:"
      String -> IO ()
putStr   (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Equation -> String) -> [Equation] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Equation -> String
showEq ([Equation] -> [String]) -> [Equation] -> [String]
forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
invalid Thy
thy
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-}"
  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
  showEq :: Equation -> String
showEq Equation
eq  =  Expr -> String
showExpr (Equation -> Expr
forall a b. (a, b) -> a
fst Equation
eq) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" == " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr (Equation -> Expr
forall a b. (a, b) -> b
snd Equation
eq)
  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 a. [a] -> 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]
_:[[Equation]]
_)  ->  do Int -> [[Equation]] -> [[Equation]] -> IO ()
pr1 Int
t [[Equation]]
is [[Equation]]
cs
                    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
carryOn Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ 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
  pr1 :: Int -> [[Equation]] -> [[Equation]] -> IO ()
pr1 Int
t [] [[Equation]]
cs  =  () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  pr1 Int
t ([Equation]
i:[[Equation]]
is) [[Equation]]
cs  =  do
    let ([[Equation]]
cs',[[Equation]]
cs'') = ([Equation] -> Bool)
-> [[Equation]] -> ([[Equation]], [[Equation]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ([Equation]
i[Equation] -> [Equation] -> Bool
forall a. Eq a => a -> a -> Bool
==) [[Equation]]
cs
    let t' :: Int
t' = Int
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Equation]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Equation]]
cs' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    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
$ [Equation] -> String
showDefn [Equation]
i
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
carryOn Args
args) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> [[Equation]] -> [[Equation]] -> IO ()
pr1 Int
t' [[Equation]]
is (Int -> [[Equation]] -> [[Equation]]
forall a. Int -> [a] -> [a]
drop Int
1 [[Equation]]
cs'')
  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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
rules Thy
thy)
  nREs :: Int
nREs  =  [Equation] -> Int
forall a. [a] -> 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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
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 :: forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With args :: Args
args@(Args{Bool
Int
maxSize :: Args -> Int
maxEquationSize :: Args -> Int
maxTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxSearchTests :: Args -> Int
maxDeconstructionSize :: Args -> Int
carryOn :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
rewriting :: Args -> Bool
requireDescent :: Args -> Bool
adHocRedundancy :: Args -> Bool
copyBindings :: Args -> Bool
atomicNumbers :: Args -> Bool
uniqueCandidates :: Args -> Bool
maxTests :: Int
maxSize :: Int
maxEvalRecursions :: Int
maxEquationSize :: Int
maxSearchTests :: Int
maxDeconstructionSize :: Int
carryOn :: Bool
showTheory :: Bool
usePatterns :: Bool
rewriting :: Bool
requireDescent :: Bool
adHocRedundancy :: Bool
copyBindings :: Bool
atomicNumbers :: Bool
uniqueCandidates :: Bool
..}) 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 :: forall f. Conjurable f => 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 :: forall f. Conjurable f => 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 a. [a] -> 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 a. [a] -> 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 :: forall f.
Conjurable f =>
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


-- | Return apparently unique candidate definitions
--   where there is a single body.
candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)
candidateDefns1 :: forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns1 Args
args String
nm f
f [Prim]
ps  =  ([[Expr]] -> [[[Equation]]])
-> ([[Expr]], Thy) -> ([[[Equation]]], Thy)
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first ((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
  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 :: forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[Expr]], Thy)
candidateExprs Args{Bool
Int
maxSize :: Args -> Int
maxEquationSize :: Args -> Int
maxTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxSearchTests :: Args -> Int
maxDeconstructionSize :: Args -> Int
carryOn :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
rewriting :: Args -> Bool
requireDescent :: Args -> Bool
adHocRedundancy :: Args -> Bool
copyBindings :: Args -> Bool
atomicNumbers :: Args -> Bool
uniqueCandidates :: Args -> Bool
maxTests :: Int
maxSize :: Int
maxEvalRecursions :: Int
maxEquationSize :: Int
maxSearchTests :: Int
maxDeconstructionSize :: Int
carryOn :: Bool
showTheory :: Bool
usePatterns :: Bool
rewriting :: Bool
requireDescent :: Bool
adHocRedundancy :: Bool
copyBindings :: Bool
atomicNumbers :: Bool
uniqueCandidates :: Bool
..} 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 a. Eq a => a -> [a] -> 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 | Bool
rewriting  =  Thy -> Expr -> Bool
isRootNormalC Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
       | Bool
otherwise  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True
  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 a. [a] -> 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 :: forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefnsC Args{Bool
Int
maxSize :: Args -> Int
maxEquationSize :: Args -> Int
maxTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxSearchTests :: Args -> Int
maxDeconstructionSize :: Args -> Int
carryOn :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
rewriting :: Args -> Bool
requireDescent :: Args -> Bool
adHocRedundancy :: Args -> Bool
copyBindings :: Args -> Bool
atomicNumbers :: Args -> Bool
uniqueCandidates :: Args -> Bool
maxTests :: Int
maxSize :: Int
maxEvalRecursions :: Int
maxEquationSize :: Int
maxSearchTests :: Int
maxDeconstructionSize :: Int
carryOn :: Bool
showTheory :: Bool
usePatterns :: Bool
rewriting :: Bool
requireDescent :: Bool
adHocRedundancy :: Bool
copyBindings :: Bool
atomicNumbers :: Bool
uniqueCandidates :: Bool
..} String
nm f
f [Prim]
ps  =  (([Equation] -> Bool) -> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT [Equation] -> Bool
hasRedundant ([[[Equation]]] -> [[[Equation]]])
-> [[[Equation]]] -> [[[Equation]]]
forall a b. (a -> b) -> a -> b
$ ([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 | Bool
rewriting  =  Thy -> Expr -> Bool
isRootNormalC Thy
thy (Expr -> Bool) -> (Expr -> Expr) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
       | Bool
otherwise  =  Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True

  appsWith :: Expr -> [Expr] -> [[Expr]]
  appsWith :: Expr -> [Expr] -> [[Expr]]
appsWith Expr
eh [Expr]
vs  =  Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
eh Expr -> Bool
k ([Expr] -> [[Expr]]) -> [Expr] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr]
vs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es
    where
    k :: Expr -> Bool
k | Bool
atomicNumbers Bool -> Bool -> Bool
&& f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
conjureIsNumeric f
f Expr
eh  =  \Expr
e -> Expr -> Bool
keepNumeric Expr
e Bool -> Bool -> Bool
&& Expr -> Bool
keep Expr
e
      | Bool
otherwise                               =  Expr -> Bool
keep
    -- discards non-atomic numeric ground expressions such as 1 + 1
    keepNumeric :: Expr -> Bool
keepNumeric Expr
e  =  Expr -> Bool
isFun Expr
e Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e Bool -> Bool -> Bool
|| Bool -> Bool
not (Expr -> Bool
isGround Expr
e)

  isRedundant :: [Equation] -> Bool
isRedundant | Bool
adHocRedundancy  =  \[Equation]
e -> [Equation] -> Bool
isRedundantDefn [Equation]
e Bool -> Bool -> Bool
|| (Expr -> Expr) -> [Equation] -> Bool
isRedundantModuloRewriting (Thy -> Expr -> Expr
normalize Thy
thy) [Equation]
e
              | Bool
otherwise        =  Bool -> [Equation] -> Bool
forall a b. a -> b -> a
const Bool
False

  hasRedundant :: [Equation] -> Bool
hasRedundant | Bool
adHocRedundancy  =  [Equation] -> Bool
hasRedundantRecursion
               | Bool
otherwise        =  Bool -> [Equation] -> Bool
forall a b. a -> b -> a
const Bool
False

  ps2fss :: [Expr] -> [[Defn]]
  ps2fss :: [Expr] -> [[[Equation]]]
ps2fss [Expr]
pats  =  ([Equation] -> Bool) -> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT [Equation] -> Bool
isRedundant
               ([[[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]]
    -- the following guarded line is an optional optimization
    -- if the function is defined for the given pattern,
    -- simply use its return value as the only possible result
    p2eess :: Expr -> [[Equation]]
p2eess Expr
pat | Bool
copyBindings Bool -> Bool -> Bool
&& f -> Expr -> Bool
forall f. Conjurable f => f -> Expr -> Bool
isGroundPat f
f Expr
pat  =  [[(Expr
pat, f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toValPat f
f Expr
pat)]]
    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. HasCallStack => [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 a. [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. HasCallStack => [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. HasCallStack => [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 a. [a] -> 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

  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 a. [a] -> 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)
                       -- h (_) is bound to e'
                    ,  Expr -> [Equation] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
h [Equation]
m Maybe Expr -> Maybe Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e'
                       -- other than (h,e') we only accept (var,var)
                    ,  (Equation -> Bool) -> [Equation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Expr
e1,Expr
e2) -> Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
h Bool -> Bool -> Bool
|| Expr -> Bool
isVar Expr
e2) [Equation]
m
                    ]
      where
      h :: Expr
h = Expr -> Expr
holeAsTypeOf 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]
candidateDeconstructionsFromHoled
                     ([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]
hs) [[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. HasCallStack => [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 a. Eq a => a -> [a] -> 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. HasCallStack => [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."


-- | Checks if the given pattern is a ground pattern.
--
-- A pattern is a ground pattern when its arguments are fully defined
-- and evaluating the function returns a defined value.
--
-- This is to be used on values returned by conjurePats.
--
-- For now, this is only used on 'candidateDefnsC'.
isGroundPat :: Conjurable f => f -> Expr -> Bool
isGroundPat :: forall f. Conjurable f => f -> Expr -> Bool
isGroundPat f
f Expr
pat  =  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
gpat Expr -> Expr -> Expr
-==- Expr
gpat
  where
  gpat :: Expr
gpat  =  f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f Expr
pat
  -==- :: Expr -> Expr -> Expr
(-==-)  =  f -> Expr -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f


-- | Given a complete "pattern", i.e. application encoded as expr,
--   converts it from using a "variable" function,
--   to an actual "value" function.
--
-- This function is used on 'isGroundPat' and 'toValPat'
toGroundPat :: Conjurable f => f -> Expr -> Expr
toGroundPat :: forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f Expr
pat  =  [Expr] -> Expr
foldApp (String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"f" f
f Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail (Expr -> [Expr]
unfoldApp Expr
pat))

-- | Evaluates a pattern to its final value.
--
-- Only to be used when the function is defined for the given set of arguments.
--
-- For now, this is only used on 'candidateDefnsC'.
toValPat :: Conjurable f => f -> Expr -> Expr
toValPat :: forall a. Conjurable a => a -> Expr -> Expr
toValPat f
f  =  f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f
-- NOTE: the use of conjureExpress above is a hack.
--       Here, one could have used a conjureVal function,
--       that lifts 'val' over 'Expr's.
--       However this function does not exist.


-- 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"


-- equality between candidates

nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]
nubCandidates :: forall f.
Conjurable f =>
Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
nubCandidates Args{Bool
Int
maxSize :: Args -> Int
maxEquationSize :: Args -> Int
maxTests :: Args -> Int
maxEvalRecursions :: Args -> Int
maxSearchTests :: Args -> Int
maxDeconstructionSize :: Args -> Int
carryOn :: Args -> Bool
showTheory :: Args -> Bool
usePatterns :: Args -> Bool
rewriting :: Args -> Bool
requireDescent :: Args -> Bool
adHocRedundancy :: Args -> Bool
copyBindings :: Args -> Bool
atomicNumbers :: Args -> Bool
uniqueCandidates :: Args -> Bool
maxTests :: Int
maxSize :: Int
maxEvalRecursions :: Int
maxEquationSize :: Int
maxSearchTests :: Int
maxDeconstructionSize :: Int
carryOn :: Bool
showTheory :: Bool
usePatterns :: Bool
rewriting :: Bool
requireDescent :: Bool
adHocRedundancy :: Bool
copyBindings :: Bool
atomicNumbers :: Bool
uniqueCandidates :: Bool
..} String
nm f
f  =
  ([Equation] -> [Equation] -> Bool)
-> [[[Equation]]] -> [[[Equation]]]
forall a. (a -> a -> Bool) -> [[a]] -> [[a]]
discardLaterT (([Equation] -> [Equation] -> Bool)
 -> [[[Equation]]] -> [[[Equation]]])
-> ([Equation] -> [Equation] -> Bool)
-> [[[Equation]]]
-> [[[Equation]]]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> String -> f -> [Equation] -> [Equation] -> Bool
forall f.
Conjurable f =>
Int -> Int -> String -> f -> [Equation] -> [Equation] -> Bool
equalModuloTesting Int
maxTests Int
maxEvalRecursions String
nm f
f


--- tiers utils ---

productsThat :: (a -> [a] -> Bool) -> [ [[a]] ] -> [[ [a] ]]
productsThat :: forall a. (a -> [a] -> Bool) -> [[[a]]] -> [[[a]]]
productsThat a -> [a] -> Bool
p  =  ([[a]] -> [[[a]]] -> [[[a]]]) -> [[[a]]] -> [[[a]]] -> [[[a]]]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((a -> [a] -> [a])
-> (a -> [a] -> Bool) -> [[a]] -> [[[a]]] -> [[[a]]]
forall a b c.
(a -> b -> c) -> (a -> b -> Bool) -> [[a]] -> [[b]] -> [[c]]
productWithThat (:) a -> [a] -> Bool
p) [[[]]]

productWithThat :: (a->b->c) -> (a->b->Bool) -> [[a]] -> [[b]] -> [[c]]
productWithThat :: forall a b c.
(a -> b -> c) -> (a -> b -> Bool) -> [[a]] -> [[b]] -> [[c]]
productWithThat a -> b -> c
f a -> b -> Bool
p [[a]]
xss [[b]]
yss  =  ((a, b) -> c) -> [[(a, b)]] -> [[c]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c
f)
                             ([[(a, b)]] -> [[c]])
-> ([[(a, b)]] -> [[(a, b)]]) -> [[(a, b)]] -> [[c]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  ((a, b) -> Bool) -> [[(a, b)]] -> [[(a, b)]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT ((a -> b -> Bool) -> (a, b) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> Bool
p)
                             ([[(a, b)]] -> [[c]]) -> [[(a, b)]] -> [[c]]
forall a b. (a -> b) -> a -> b
$  [[a]]
xss [[a]] -> [[b]] -> [[(a, b)]]
forall a b. [[a]] -> [[b]] -> [[(a, b)]]
>< [[b]]
yss

productsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
productsWith :: forall a. ([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 productsWith to LeanCheck?

delayedProductsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
delayedProductsWith :: forall a. ([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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
xsss
-- TODO: move delayedProductsWith 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]
:))

boolTy :: TypeRep
boolTy :: TypeRep
boolTy  =  Expr -> TypeRep
typ Expr
b_