-- |
-- 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.LeanCheck.Utils (classifyOn)

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 :: forall f. Conjurable f => String -> f -> [Prim] -> IO ()
conjure  =  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  =  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  =  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  =  forall f. Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureWith Args
args
                       {  maxSize :: Int
maxSize = Int
sz
                       ,  maxEquationSize :: Int
maxEquationSize = 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
copyBindings          :: Bool -- ^ copy partial definition bindings in 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
  { 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
  , copyBindings :: Bool
copyBindings           =  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 :: forall f. Conjurable f => Args -> String -> f -> [Prim] -> IO ()
conjureWith Args
args String
nm f
f  =  forall f.
Conjurable f =>
Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With Args
args String
nm f
f (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  =  forall f.
Conjurable f =>
Args -> String -> f -> (f -> Bool) -> [Prim] -> IO ()
conjure0With Args
args String
nm 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
  forall a. Show a => a -> IO ()
print (forall a. Typeable a => String -> a -> Expr
var (forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
nm) f
f)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ts forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- testing " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ts) forall a. [a] -> [a] -> [a]
++ String
" combinations of argument values"
  String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- pruning with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
nRules forall a. [a] -> [a] -> [a]
++ String
"/" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
nREs forall a. [a] -> [a] -> [a]
++ String
" rules"
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showTheory Args
args) forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"{-"
    Thy -> IO ()
printThy Thy
thy
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-}"
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
invalid Thy
thy) forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- reasoning produced "
            forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
invalid Thy
thy)) forall a. [a] -> [a] -> [a]
++ String
" incorrect properties,"
            forall a. [a] -> [a] -> [a]
++ String
" please re-run with more tests for faster results"
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Args -> Bool
showTheory Args
args) forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"{-"
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"invalid:"
      String -> IO ()
putStr   forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Equation -> String
showEq forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
invalid Thy
thy
      String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-}"
  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 (forall a b. (a, b) -> a
fst Equation
eq) forall a. [a] -> [a] -> [a]
++ String
" == " forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr (forall a b. (a, b) -> b
snd Equation
eq)
  pr :: t -> Int -> [([[Equation]], [[Equation]])] -> IO ()
pr t
n Int
t []  =  do String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- tested " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
t forall a. [a] -> [a] -> [a]
++ String
" candidates"
                   String -> IO ()
putStrLn 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  =  forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Equation]]
cs
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- looking through " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
nc forall a. [a] -> [a] -> [a]
++ String
" candidates of size " forall a. [a] -> [a] -> [a]
++ 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
nforall a. Num a => a -> a -> a
+t
1) (Int
tforall a. Num a => a -> a -> a
+Int
nc) [([[Equation]], [[Equation]])]
rs
      ([Equation]
i:[[Equation]]
_)  ->  do let nc' :: Int
nc' = forall a. a -> Maybe a -> a
fromMaybe Int
nc (forall a. (a -> Bool) -> [a] -> Maybe Int
findIndex ([Equation]
iforall a. Eq a => a -> a -> Bool
==) [[Equation]]
cs)
                    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"-- tested " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
tforall a. Num a => a -> a -> a
+Int
nc'forall a. Num a => a -> a -> a
+Int
1) forall a. [a] -> [a] -> [a]
++ String
" candidates"
                    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Equation] -> String
showDefn [Equation]
i
  rs :: [([[Equation]], [[Equation]])]
rs  =  forall a b. [a] -> [b] -> [(a, b)]
zip [[[Equation]]]
iss [[[Equation]]]
css
  ([[[Equation]]]
iss, [[[Equation]]]
css, [Expr]
ts, Thy
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  =  forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
rules Thy
thy)
  nREs :: Int
nREs  =  forall (t :: * -> *) a. Foldable t => t a -> Int
length (Thy -> [Equation]
equations Thy
thy) 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 =  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  =  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 =  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  =  forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args String
nm f
f (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  =  forall f.
Conjurable f =>
Args
-> String
-> f
-> (f -> Bool)
-> [Prim]
-> ([[[Equation]]], [[[Equation]]], [Expr], Thy)
conjpure0With Args
args String
nm 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
uniqueCandidates :: Bool
showTheory :: Bool
copyBindings :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
copyBindings :: 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  =  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 (forall f. Conjurable f => Int -> [Equation] -> f
cevl Int
maxEvalRecursions [Equation]
fx))
  candidatesT :: [[[Equation]]]
candidatesT  =  (if Bool
uniqueCandidates then forall f.
Conjurable f =>
Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
nubCandidates Args
args String
nm f
f else forall a. a -> a
id)
               forall a b. (a -> b) -> a -> b
$  forall a. Int -> [a] -> [a]
take Int
maxSize [[[Equation]]]
candidatesTT
  ([[[Equation]]]
candidatesTT, Thy
thy)  =  forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns Args
args String
nm f
f [Prim]
es
  ffxx :: Expr
ffxx   =  forall f. Conjurable f => String -> f -> Expr
conjureApplication String
nm f
f
  vffxx :: Expr
vffxx  =  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
(-==-)  =  forall f. Conjurable f => f -> Expr -> Expr -> Expr
conjureMkEquation f
f

  isTrueWhenDefined :: [Equation] -> Expr -> Bool
isTrueWhenDefined [Equation]
dfn Expr
e  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
errorToFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Typeable a =>
(Expr -> Expr) -> Int -> [Equation] -> a -> Expr -> a
deval (forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions [Equation]
dfn Bool
False)
                           forall a b. (a -> b) -> a -> b
$  forall a b. (a -> b) -> [a] -> [b]
map (Expr
e Expr -> [Equation] -> Expr
//-) [[Equation]]
dbss

  bss, dbss :: [[(Expr,Expr)]]
  bss :: [[Equation]]
bss  =  forall a. Int -> [a] -> [a]
take Int
maxSearchTests forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [[Equation]]
groundBinds (forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) Expr
ffxx
  dbss :: [[Equation]]
dbss  =  forall a. Int -> [a] -> [a]
take Int
maxTests [[Equation]
bs | [Equation]
bs <- [[Equation]]
bss, Bool -> Bool
errorToFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typeable a => a -> Expr -> a
eval Bool
False 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  =  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 forall a b. (a -> b) -> a -> b
$ String
"theory with " forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
rules Thy
thy) forall a. [a] -> [a] -> [a]
++ String
" rules and "
                            forall a. [a] -> [a] -> [a]
++ (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
equations Thy
thy) forall a. [a] -> [a] -> [a]
++ String
" equations"
  Thy -> IO ()
printThy Thy
thy
  where
  ([[[Equation]]]
_, [[[Equation]]]
_, [Expr]
_, Thy
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 forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefnsC
                      else forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns1


nubCandidates :: Conjurable f => Args -> String -> f -> [[Defn]] -> [[Defn]]
nubCandidates :: forall f.
Conjurable f =>
Args -> String -> f -> [[[Equation]]] -> [[[Equation]]]
nubCandidates Args{Bool
Int
uniqueCandidates :: Bool
showTheory :: Bool
copyBindings :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
copyBindings :: 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  =  forall a. (a -> a -> Bool) -> [[a]] -> [[a]]
discardLaterT [Equation] -> [Equation] -> Bool
(===)
  where
  err :: a
err  =  forall a. HasCallStack => String -> a
error String
"nubCandidates: unexpected evaluation error."
  eq :: Dynamic
eq  =  forall f. Conjurable f => f -> Dynamic
conjureDynamicEq f
f
  [Equation]
d1 === :: [Equation] -> [Equation] -> Bool
=== [Equation]
d2  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
are forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
maxTests forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds (forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) (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
           forall a b. (a -> b) -> a -> b
$  (forall a. Typeable a => Dynamic -> a -> a
`fromDyn` forall {a}. a
err)
           forall a b. (a -> b) -> a -> b
$  Dynamic
eq Dynamic -> Dynamic -> Dynamic
`dynApp` forall a. a -> Maybe a -> a
fromMaybe forall {a}. a
err ((Expr -> Expr) -> Int -> [Equation] -> Expr -> Maybe Dynamic
toDynamicWithDefn (forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions [Equation]
d1 Expr
e)
                 Dynamic -> Dynamic -> Dynamic
`dynApp` forall a. a -> Maybe a -> a
fromMaybe forall {a}. a
err ((Expr -> Expr) -> Int -> [Equation] -> Expr -> Maybe Dynamic
toDynamicWithDefn (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 :: forall f.
Conjurable f =>
Args -> String -> f -> [Prim] -> ([[[Equation]]], Thy)
candidateDefns1 Args
args String
nm f
f [Prim]
ps  =  forall {t} {a} {b}. (t -> a) -> (t, b) -> (a, b)
mapFst (forall a b. (a -> b) -> [[a]] -> [[b]]
mapT forall {b}. b -> [(Expr, b)]
toDefn) forall a b. (a -> b) -> a -> b
$ 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  =  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
uniqueCandidates :: Bool
showTheory :: Bool
copyBindings :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
copyBindings :: 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 forall a. [[a]] -> [[a]] -> [[a]]
\/ forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [[Expr]] -> [[Expr]]
`enumerateFillings` [[Expr]]
recs) [[Expr]]
ts, Thy
thy)
  where
  es :: [Expr]
es  =  forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [Prim]
ps
  ts :: [[Expr]]
ts | Expr -> TypeRep
typ Expr
efxs forall a. Eq a => a -> a -> Bool
== TypeRep
boolTy  =  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
andE [[[Expr]]
cs, [[Expr]]
rs]
                           forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
orE  [[[Expr]]
cs, [[Expr]]
rs]
     | Bool
otherwise           =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepIf
                           forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
as, [[Expr]]
rs]
                           forall a. [[a]] -> [[a]] -> [[a]]
\/ Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts (forall a. Conjurable a => a -> Expr
conjureIf f
f) [[[Expr]]
cs, [[Expr]]
rs, [[Expr]]
as]
  cs :: [[Expr]]
cs  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, forall a. (Typeable a, Show a) => a -> Expr
val Bool
True])
      forall a b. (a -> b) -> a -> b
$  Expr -> [[Expr]]
forN (forall a. Typeable a => a -> Expr
hole (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 forall a b. (a -> b) -> a -> b
$ [Expr]
exs forall a. [a] -> [a] -> [a]
++ [Expr]
es
  forR :: Expr -> [[Expr]]
forR Expr
h  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr
eh forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Expr -> [Expr]
holes Expr
e))
          forall a b. (a -> b) -> a -> b
$  Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep forall a b. (a -> b) -> a -> b
$ [Expr]
exs forall a. [a] -> [a] -> [a]
++ [Expr]
es forall a. [a] -> [a] -> [a]
++ [Expr
eh]
  eh :: Expr
eh  =  Expr -> Expr
holeAsTypeOf Expr
efxs
  efxs :: Expr
efxs  =  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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
fastMostGeneralVariation
  ds :: [Expr]
ds  =  forall a. (a -> Bool) -> [a] -> [a]
filter (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       =  forall a b. a -> b -> a
const Bool
True
    where
    Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e'  =  Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null
                    [  ()
                    |  Expr
d <- [Expr]
deconstructions
                    ,  [Equation]
m <- forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Equation]
`match` Expr
d)
                    ,  forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(/=)) [Equation]
m forall a. Eq a => a -> a -> Bool
== [(Expr -> Expr
holeAsTypeOf Expr
e', Expr
e')]
                    ]
    deconstructions :: [Expr]
    deconstructions :: [Expr]
deconstructions  =  forall a. (a -> Bool) -> [a] -> [a]
filter (forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
                     forall a b. (a -> b) -> a -> b
$  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFrom
                     forall a b. (a -> b) -> a -> b
$  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
                     forall a b. (a -> b) -> a -> b
$  forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT Expr -> [[Expr]]
forN [[Expr]
hs]
      where
      hs :: [Expr]
hs  =  forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f
  recs :: [[Expr]]
recs  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keepR
        forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [[Expr]]
forN Expr
h | Expr
h <- forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
  thy :: Thy
thy  =  (Expr -> Expr -> Bool) -> Thy -> Thy
doubleCheck Expr -> Expr -> Bool
(===)
       forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub
       forall a b. (a -> b) -> a -> b
$  [Prim] -> [Expr]
cjHoles (forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fforall a. a -> [a] -> [a]
:[Prim]
ps) forall a. [a] -> [a] -> [a]
++ [forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, forall a. (Typeable a, Show a) => a -> Expr
val Bool
True] forall a. [a] -> [a] -> [a]
++ [Expr]
es
  === :: Expr -> Expr -> Bool
(===)  =  [Prim] -> Int -> Expr -> Expr -> Bool
cjAreEqual (forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fforall 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
uniqueCandidates :: Bool
showTheory :: Bool
copyBindings :: Bool
usePatterns :: Bool
requireDescent :: Bool
maxDeconstructionSize :: Int
maxSearchTests :: Int
maxEquationSize :: Int
maxEvalRecursions :: Int
maxSize :: Int
maxTests :: Int
uniqueCandidates :: Args -> Bool
showTheory :: Args -> Bool
copyBindings :: 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  =  (forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Equation] -> [[[Equation]]]
fillingsFor [[[Equation]]]
fss,Thy
thy)
  where
  pats :: [[[Expr]]]
pats  =  forall f. Conjurable f => [Expr] -> String -> f -> [[[Expr]]]
conjurePats [Expr]
es String
nm f
f
  fss :: [[[Equation]]]
fss  =  forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT [Expr] -> [[[Equation]]]
ps2fss [[[Expr]]]
pats
  es :: [Expr]
es  =  forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [Prim]
ps

  eh :: Expr
eh  =  Expr -> Expr
holeAsTypeOf Expr
efxs
  efxs :: Expr
efxs  =  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 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 forall a b. (a -> b) -> a -> b
$ [Expr]
vs forall a. [a] -> [a] -> [a]
++ [Expr]
es

  ps2fss :: [Expr] -> [[Defn]]
  ps2fss :: [Expr] -> [[[Equation]]]
ps2fss [Expr]
pats  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT [Equation] -> Bool
isRedundantDefn
               forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT (forall a. Eq a => [a] -> Bool
allEqual forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd)
               forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. [[[a]]] -> [[[a]]]
products
               forall a b. (a -> b) -> a -> b
$  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
&& forall f. Conjurable f => f -> Expr -> Bool
isGroundPat f
f Expr
pat  =  [[(Expr
pat, forall a. Conjurable a => a -> Expr -> Expr
toValPat f
f Expr
pat)]]
    p2eess Expr
pat  =  forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
pat,)
                forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Expr -> [Expr] -> [[Expr]]
appsWith Expr
pat
                forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. [a] -> [a]
tail
                forall a b. (a -> b) -> a -> b
$  Expr -> [Expr]
vars Expr
pat forall a. [a] -> [a] -> [a]
++ [Expr
eh | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {a}. Eq a => [a] -> Expr -> Bool
should) (forall a b. [a] -> [b] -> [(a, b)]
zip [[Expr]]
aess [Expr]
aes)]
      where
      should :: [a] -> Expr -> Bool
should [a]
aes Expr
ae  =  forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub [a]
aes) 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   =                  (forall a. [a] -> [a]
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
rehole) Expr
pat
      aess :: [[Expr]]
aess  =  forall a. [[a]] -> [[a]]
transpose forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. [a] -> [a]
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp 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)  =  forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (\[Expr]
es -> (Expr
ep,Expr -> [Expr] -> Expr
fill Expr
er [Expr]
es))
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. [[[a]]] -> [[[a]]]
products
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
holes Expr
er)
                        forall a b. (a -> b) -> a -> b
$  Expr -> [[Expr]]
recs' Expr
ep

  fillingsFor :: Defn -> [[Defn]]
  fillingsFor :: [Equation] -> [[[Equation]]]
fillingsFor  =  forall a. [[[a]]] -> [[[a]]]
products forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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       =  forall a b. a -> b -> a
const Bool
True
    where
    Expr
e isDecOf :: Expr -> Expr -> Bool
`isDecOf` Expr
e'  =  Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null
                    [  ()
                    |  Expr
d <- [Expr]
deconstructions
                    ,  [Equation]
m <- forall a. Maybe a -> [a]
maybeToList (Expr
e Expr -> Expr -> Maybe [Equation]
`match` Expr
d)
                       -- h (_) is bound to e'
                    ,  forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
h [Equation]
m forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Expr
e'
                       -- other than (h,e') we only accept (var,var)
                    ,  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Expr
e1,Expr
e2) -> Expr
e1 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  =  forall a. (a -> Bool) -> [a] -> [a]
filter (forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests)
                     forall a b. (a -> b) -> a -> b
$  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
candidateDeconstructionsFromHoled
                     forall a b. (a -> b) -> a -> b
$  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
maxDeconstructionSize
                     forall a b. (a -> b) -> a -> b
$  forall a b. (a -> [[b]]) -> [[a]] -> [[b]]
concatMapT (Expr -> [Expr] -> [[Expr]]
`appsWith` [Expr]
hs) [[Expr]
hs]
      where
      hs :: [Expr]
hs  =  forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f
  recs :: Expr -> [[Expr]]
recs Expr
ep  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr -> Expr -> Bool
keepR Expr
ep)
           forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. (a -> Bool) -> [[a]] -> [[a]]
discardT (\Expr
e -> Expr
e forall a. Eq a => a -> a -> Bool
== Expr
ep)
           forall a b. (a -> b) -> a -> b
$  [Expr] -> [[Expr]]
recsV' (forall a. [a] -> [a]
tail (Expr -> [Expr]
vars Expr
ep))
  recsV :: [Expr] -> [[Expr]]
recsV [Expr]
vs  =  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
vs) (Expr -> [Expr]
vars Expr
e))
            forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [Expr] -> [[Expr]]
appsWith Expr
h [Expr]
vs | Expr
h <- forall a. Conjurable a => a -> [Expr]
conjureArgumentHoles f
f]
  -- like recs, but memoized
  recs' :: Expr -> [[Expr]]
recs' Expr
ep  =  forall a. a -> Maybe a -> a
fromMaybe forall {a}. a
errRP forall a b. (a -> b) -> a -> b
$ 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  =  forall a. Ord a => [a] -> [a]
nubSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ [[[Expr]]]
pats
  -- like recsV, but memoized
  recsV' :: [Expr] -> [[Expr]]
recsV' [Expr]
vs  =  forall a. a -> Maybe a -> a
fromMaybe forall {a}. a
errRV forall a b. (a -> b) -> a -> b
$ 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 <- forall a. Ord a => [a] -> [a]
nubSort forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. [a] -> [a]
tail 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
(===)
       forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
maxEquationSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub
       forall a b. (a -> b) -> a -> b
$  [Prim] -> [Expr]
cjHoles (forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fforall a. a -> [a] -> [a]
:[Prim]
ps) forall a. [a] -> [a] -> [a]
++ [forall a. (Typeable a, Show a) => a -> Expr
val Bool
False, forall a. (Typeable a, Show a) => a -> Expr
val Bool
True] forall a. [a] -> [a] -> [a]
++ [Expr]
es
  === :: Expr -> Expr -> Bool
(===)  =  [Prim] -> Int -> Expr -> Expr -> Bool
cjAreEqual (forall a. Conjurable a => String -> a -> Prim
prim String
nm f
fforall a. a -> [a] -> [a]
:[Prim]
ps) Int
maxTests
  isUnbreakable :: Expr -> Bool
isUnbreakable  =  forall f. Conjurable f => f -> Expr -> Bool
conjureIsUnbreakable f
f
  errRP :: a
errRP  =  forall a. HasCallStack => String -> a
error String
"candidateDefnsC: unexpected pattern.  You have found a bug, please report it."
  errRV :: a
errRV  =  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  =  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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
cs) Bool -> Bool -> 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  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {t :: * -> *}. Foldable t => t Equation -> Bool
d1 [[Equation]]
ss
  where
  desc :: [Equation] -> Bool
desc  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall {t :: * -> *}. Foldable t => t Equation -> Bool
d1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Expr] -> [Expr] -> [[Equation]]
useMatches forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip
  d1 :: t Equation -> Bool
d1 t Equation
exys  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Equation -> Bool
isNotConstruction t Equation
exys
           Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Equation -> Bool
isDeconstruction t Equation
exys
  ss :: [[Equation]]
ss  =  forall a. [a] -> [a]
init forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]]
sets [Equation]
exys
  exys :: [Equation]
exys  =  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 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 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 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


-- | 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Typeable a => a -> Expr -> a
eval Bool
False forall a b. (a -> b) -> a -> b
$ Expr
gpat Expr -> Expr -> Expr
-==- Expr
gpat
  where
  gpat :: Expr
gpat  =  forall a. Conjurable a => a -> Expr -> Expr
toGroundPat f
f Expr
pat
  -==- :: 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 (forall a. Typeable a => String -> a -> Expr
value String
"f" f
f forall a. a -> [a] -> [a]
: forall a. [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  =  forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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 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   =  forall a. a -> Maybe a
Just (Expr
e1,Expr
e2)
                                     | Expr -> Bool
isVar Expr
e2   =  forall a. a -> Maybe a
Just (Expr
e2,Expr
e1)
  binding Expr
_                                       =  forall a. Maybe a
Nothing
keepIf Expr
_  =  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  =  forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. Expr -> Triexpr a -> [(Expr, [Equation], a)]
T.lookup Expr
e Triexpr Expr
trie
  where
  trie :: Triexpr Expr
trie  =  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
&&  forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) [Expr
e2 Expr -> [Equation] -> Expr
//- [Equation]
bs | (Expr
_,[Equation]
bs,Expr
e2) <- forall a. Expr -> Triexpr a -> [(Expr, [Equation], a)]
T.lookup Expr
e Triexpr Expr
trie])
  where
  trie :: Triexpr Expr
trie  =  forall a. [(Expr, a)] -> Triexpr a
T.fromList forall a b. (a -> b) -> a -> b
$ Thy -> [Equation]
equations Thy
thy forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map 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 :: forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f  =  forall a b. (a -> b) -> [[a]] -> [[b]]
mapT [a] -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [[[a]]] -> [[[a]]]
products
-- TODO: move to LeanCheck?

delayedProductsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
delayedProductsWith :: forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith [a] -> a
f [[[a]]]
xsss  =  forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f [[[a]]]
xsss forall a. [[a]] -> Int -> [[a]]
`addWeight` 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  =  forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith ([Expr] -> Expr
foldApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
efforall a. a -> [a] -> [a]
:))