-- |
-- 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
  , conjpure
  , conjpureWith
  , candidateExprs
  , module Data.Express
  , module Data.Express.Fixtures
  , module Test.Speculate.Engine
  , module Test.Speculate.Reason
  )
where

import Control.Monad (when)

import Data.Express
import Data.Express.Fixtures hiding ((-==-))
import qualified Data.Express.Triexpr as T

import Test.LeanCheck
import Test.LeanCheck.Tiers
import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)

import Test.Speculate.Reason (Thy, rules, equations, canReduceTo, printThy)
import Test.Speculate.Engine (theoryFromAtoms, groundBinds)

import Conjure.Expr
import Conjure.Conjurable


-- | 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 :: [Expr]
-- > primitives =
-- >   [ val (0::Int)
-- >   , val (1::Int)
-- >   , value "+" ((+) :: Int -> Int -> Int)
-- >   , value "*" ((*) :: Int -> Int -> Int)
-- > ]
--
-- The conjure function does the following:
--
-- > > conjure "square" square primitives
-- > square :: Int -> Int
-- > -- 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 'val' and 'value'.
conjure :: Conjurable f => String -> f -> [Expr] -> IO ()
conjure :: String -> f -> [Expr] -> IO ()
conjure  =  Args -> String -> f -> [Expr] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith 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 -> [Expr] -> IO ()
conjureWithMaxSize :: Int -> String -> f -> [Expr] -> IO ()
conjureWithMaxSize Int
sz  =  Args -> String -> f -> [Expr] -> IO ()
forall f. Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith Args
args
                       {  maxSize :: Int
maxSize = Int
sz
                       ,  maxEquationSize :: Int
maxEquationSize = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
sz (Args -> Int
maxEquationSize Args
args)
                       }


-- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.
--   See 'args' for the defaults.
data Args = Args
  { Args -> Int
maxTests          :: Int  -- ^ maximum number of tests to each candidate
  , Args -> Int
maxSize           :: Int  -- ^ maximum size of candidate bodies
  , Args -> Int
maxRecursiveCalls :: Int  -- ^ maximum number of allowed recursive calls
  , Args -> Int
maxEquationSize   :: Int  -- ^ maximum size of equation operands
  , Args -> Int
maxRecursionSize  :: Int  -- ^ maximum size of a recursive expression expansion
  , Args -> Int
maxSearchTests    :: Int  -- ^ maximum number of tests to search for defined values
  , Args -> [[Expr]]
forceTests :: [[Expr]]  -- ^ force tests
  }


-- | Default arguments to conjure.
--
-- * 60 tests
-- * functions of up to 12 symbols
-- * maximum of 1 recursive call
-- * pruning with equations up to size 5
-- * recursion up to 60 symbols
-- * search for defined applications for up to 100000 combinations
args :: Args
args :: Args
args = Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args
Args
  { maxTests :: Int
maxTests           =  Int
60
  , maxSize :: Int
maxSize            =  Int
12
  , maxRecursiveCalls :: Int
maxRecursiveCalls  =   Int
1
  , maxEquationSize :: Int
maxEquationSize    =   Int
5
  , maxRecursionSize :: Int
maxRecursionSize   =  Int
60
  , maxSearchTests :: Int
maxSearchTests     =  Int
100000
  , forceTests :: [[Expr]]
forceTests         =  []
  }


-- | Like 'conjure' but allows setting options through 'Args'/'args'.
--
-- > conjureWith args{maxSize = 11} "function" function [...]
conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()
conjureWith :: Args -> String -> f -> [Expr] -> IO ()
conjureWith Args
args String
nm f
f [Expr]
es  =  do
  Expr -> IO ()
forall a. Show a => a -> IO ()
print (String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
var ([String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
nm) f
f)
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- testing " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" combinations of argument values"
  Integer -> [([Expr], [Expr], [Expr])] -> IO ()
forall (t :: * -> *) t a c.
(Foldable t, Show t, Num t) =>
t -> [([Expr], t a, c)] -> IO ()
pr Integer
1 [([Expr], [Expr], [Expr])]
rs
  where
  pr :: t -> [([Expr], t a, c)] -> IO ()
pr t
n []  =  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"cannot conjure"
  pr t
n (([Expr]
is,t a
cs,c
es):[([Expr], t a, c)]
rs)  =  do
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"-- looking through "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
cs)
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates of size " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
n
    -- when (n<=6) $ putStrLn $ unlines $ map show es
    case [Expr]
is of
      []     ->  t -> [([Expr], t a, c)] -> IO ()
pr (t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1) [([Expr], t a, c)]
rs
      (Expr
i:[Expr]
_)  ->  do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Expr -> String
showEq Expr
i
                    String -> IO ()
putStrLn String
""
  rs :: [([Expr], [Expr], [Expr])]
rs  =  [[Expr]] -> [[Expr]] -> [[Expr]] -> [([Expr], [Expr], [Expr])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [[Expr]]
iss [[Expr]]
css [[Expr]]
ess
  ([[Expr]]
iss, [[Expr]]
css, [[Expr]]
ess, [Expr]
ts)  =  Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
forall f.
Conjurable f =>
Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args
args String
nm f
f [Expr]
es


-- | Like 'conjure' but in the pure world.
--
-- Returns a triple with:
--
-- 1. tiers of implementations
-- 2. tiers of candidate bodies (right type)
-- 3. tiers of candidate expressions (any type)
-- 4. a list of tests
conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpure :: String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpure =  Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
forall f.
Conjurable f =>
Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args
args


-- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith :: Args
-> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
conjpureWith Args{Int
[[Expr]]
forceTests :: [[Expr]]
maxSearchTests :: Int
maxRecursionSize :: Int
maxEquationSize :: Int
maxRecursiveCalls :: Int
maxSize :: Int
maxTests :: Int
forceTests :: Args -> [[Expr]]
maxSearchTests :: Args -> Int
maxRecursionSize :: Args -> Int
maxRecursiveCalls :: Args -> Int
maxTests :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
..} String
nm f
f [Expr]
es  =  ([[Expr]]
implementationsT, [[Expr]]
candidatesT, [[Expr]]
allCandidatesT, [Expr]
tests)
  where
  tests :: [Expr]
tests  =  [Expr
ffxx Expr -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs | [(Expr, Expr)]
bs <- [[(Expr, Expr)]]
dbss]
  implementationsT :: [[Expr]]
implementationsT  =  (Expr -> Expr) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr
vffxx Expr -> Expr -> Expr
-==-) ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
implements [[Expr]]
candidatesT
  implements :: Expr -> Bool
implements Expr
e  =  Expr -> Expr -> Bool
apparentlyTerminates Expr
rrff Expr
e
                Bool -> Bool -> Bool
&& (Expr, Expr) -> Expr -> Expr -> Bool
requal (Expr
vffxx,Expr
e) Expr
ffxx Expr
e
  candidatesT :: [[Expr]]
candidatesT  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
ffxx) [[Expr]]
allCandidatesT
  allCandidatesT :: [[Expr]]
allCandidatesT  =  Int -> [[Expr]] -> [[Expr]]
forall a. Int -> [a] -> [a]
take Int
maxSize
                  ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
forall f.
Conjurable f =>
String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
candidateExprs String
nm f
f Int
maxEquationSize Int
maxRecursiveCalls Expr -> Expr -> Bool
(===) [Expr]
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

  === :: Expr -> Expr -> Bool
(===)  =  f -> Int -> Expr -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Expr -> Bool
conjureAreEqual f
f Int
maxTests
  requal :: (Expr, Expr) -> Expr -> Expr -> Bool
requal (Expr, Expr)
dfn Expr
e1 Expr
e2  =  (Expr, Expr) -> Expr -> Bool
isTrueWhenDefined (Expr, Expr)
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 :: (Expr, Expr) -> Expr -> Bool
isTrueWhenDefined (Expr, Expr)
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 -> Bool -> Expr -> Bool
forall a. Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a
reval (Expr, Expr)
dfn Int
maxRecursionSize Bool
False) ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ ([(Expr, Expr)] -> Expr) -> [[(Expr, Expr)]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e Expr -> [(Expr, Expr)] -> Expr
//-) [[(Expr, Expr)]]
dbss

  bss, dbss :: [[(Expr,Expr)]]
  bss :: [[(Expr, Expr)]]
bss  =  Int -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Int -> [a] -> [a]
take Int
maxSearchTests ([[(Expr, Expr)]] -> [[(Expr, Expr)]])
-> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ (Expr -> [[Expr]]) -> Expr -> [[(Expr, Expr)]]
groundBinds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
conjureTiersFor f
f) Expr
ffxx
  fbss :: [[(Expr, Expr)]]
fbss  =  [[Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
xxs [Expr]
vs | [Expr]
vs <- [[Expr]]
forceTests, Expr -> Bool
isWellTyped (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
foldApp (Expr
rrffExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
vs)]
  dbss :: [[(Expr, Expr)]]
dbss  =  Int -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Int -> [a] -> [a]
take Int
maxTests
        ([[(Expr, Expr)]] -> [[(Expr, Expr)]])
-> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$  ([[(Expr, Expr)]
bs | [(Expr, Expr)]
bs <- [[(Expr, Expr)]]
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 -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs] [[(Expr, Expr)]] -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. Eq a => [a] -> [a] -> [a]
\\ [[(Expr, Expr)]]
fbss)
        [[(Expr, Expr)]] -> [[(Expr, Expr)]] -> [[(Expr, Expr)]]
forall a. [a] -> [a] -> [a]
++ [[(Expr, Expr)]]
fbss
    where
    e :: Expr
e  =  Expr
ffxx Expr -> Expr -> Expr
-==- Expr
ffxx


candidateExprs :: Conjurable f
               => String -> f
               -> Int
               -> Int
               -> (Expr -> Expr -> Bool)
               -> [Expr]
               -> [[Expr]]
candidateExprs :: String
-> f -> Int -> Int -> (Expr -> Expr -> Bool) -> [Expr] -> [[Expr]]
candidateExprs String
nm f
f Int
sz Int
mc Expr -> Expr -> Bool
(===) [Expr]
es  =  [[Expr]]
as [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]]
ts
  where
  ts :: [[Expr]]
ts  =  (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]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es]
  forD :: Expr -> [[Expr]]
forD Expr
h  =  Expr -> (Expr -> Bool) -> [[Expr]] -> [[Expr]]
enumerateAppsFor Expr
h (Bool -> Expr -> Bool
forall a b. a -> b -> a
const Bool
True) [[Expr]
exs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
ds]
  forR :: Expr -> [[Expr]]
forR Expr
h  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (Expr
ef Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) (Expr -> [Expr]
vars 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]]
recs
  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 Expr
e  =  Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e
          Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Int
forall a. (a -> Bool) -> [a] -> Int
count (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ef) (Expr -> [Expr]
vars Expr
e) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
mc
  thy :: Thy
thy  =  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
sz ([[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
$  f -> [Expr]
forall f. Conjurable f => f -> [Expr]
conjureHoles f
f [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
  ds :: [Expr]
ds  =  ((Expr, Expr) -> Expr) -> [(Expr, Expr)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd ([(Expr, Expr)] -> [Expr]) -> [(Expr, Expr)] -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> Int -> [Expr] -> [(Expr, Expr)]
forall f. Conjurable f => f -> Int -> [Expr] -> [(Expr, Expr)]
deconstructors f
f Int
60 [Expr]
es
  recs :: [[Expr]]
recs  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Expr
efxs Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/=)
        ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef [Expr -> [[Expr]]
forD Expr
h | Expr
h <- f -> [Expr]
forall f. Conjurable f => f -> [Expr]
conjureArgumentHoles f
f]

-- | Example:
--
-- > > deconstructors and 60
-- > >   [ val False
-- > >   , val True
-- > >   , value "null" (null::[Bool]->Bool)
-- > >   , value "head" (head :: [Bool] -> Bool)
-- > >   , value "tail" (tail :: [Bool] -> [Bool])
-- > >   , value "drop1" (drop 1 :: [Bool] -> [Bool])
-- > >   ]
-- > [tail :: [Bool] -> [Bool]]
--
-- In this case, inc is a deconstructor as it converges for more than half the
-- values:
--
-- > > deconstructors (negate :: Int -> Int) 60
-- > >   [ value "eq0" ((==0) :: Int -> Bool)
-- > >   , val (0 :: Int)
-- > >   , value "==" ((==) :: Int -> Int -> Bool)
-- > >   , value "dec" (subtract 1 :: Int -> Int)
-- > >   , value "inc" ((+1) :: Int -> Int)
-- > >   ]
-- > [ ((0 ==) :: Int -> Bool,dec :: Int -> Int)
-- > , ((0 ==) :: Int -> Bool,inc :: Int -> Int)
-- > ]
deconstructors :: Conjurable f => f -> Int -> [Expr] -> [(Expr, Expr)]
deconstructors :: f -> Int -> [Expr] -> [(Expr, Expr)]
deconstructors f
f Int
maxTests [Expr]
es  =
  [ (Expr
z, Expr
d)
  | Expr
d <- [Expr]
es
  , Expr
h <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 [Expr
h | Expr
h <- [Expr]
hs, Expr -> Maybe TypeRep
mtyp (Expr
d Expr -> Expr -> Expr
:$ Expr
h) Maybe TypeRep -> Maybe TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe TypeRep
mtyp Expr
h]
  , Expr
z <- Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
1 [Expr
z | Expr
z <- [Expr]
es2, Expr -> Maybe TypeRep
mtyp (Expr
z Expr -> Expr -> Expr
:$ Expr
h) Maybe TypeRep -> Maybe TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe TypeRep
mtyp Expr
b Bool -> Bool -> Bool
&& Expr -> Expr -> Expr -> Bool
isDeconstructor Expr
h Expr
z Expr
d]
  ]
  where
  b :: Expr
b  =  Bool -> Expr
forall a. Typeable a => a -> Expr
hole (Bool
forall a. HasCallStack => a
undefined :: Bool)
  hs :: [Expr]
hs  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ f -> [Expr]
forall f. Conjurable f => f -> [Expr]
conjureArgumentHoles f
f
  isDeconstructor :: Expr -> Expr -> Expr -> Bool
isDeconstructor  =  f -> Int -> Expr -> Expr -> Expr -> Bool
forall f. Conjurable f => f -> Int -> Expr -> Expr -> Expr -> Bool
conjureIsDeconstructor f
f Int
maxTests
  es2 :: [Expr]
es2  =  [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2 | Expr
e1 <- [Expr]
es, Expr
e2 <- [Expr]
es, Expr -> Bool
isWellTyped (Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2)]


candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]
candidatesTD Expr -> Bool
keep Expr
h [Expr]
primitives  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
hasHole)
                                ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  [[Expr]] -> [[Expr]]
town [[Expr
h]]
  where
  most :: Expr -> Expr
most = Expr -> Expr
mostGeneralCanonicalVariation

  town :: [[Expr]] -> [[Expr]]
  town :: [[Expr]] -> [[Expr]]
town ((Expr
e:[Expr]
es):[[Expr]]
ess) | Expr -> Bool
keep (Expr -> Expr
most Expr
e)  =  [[Expr
e]] [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]] -> [[Expr]]
town (Expr -> [[Expr]]
expand Expr
e [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ ([Expr]
es[Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]]
ess))
                    | Bool
otherwise      =  [[Expr]] -> [[Expr]]
town ([Expr]
es[Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]]
ess)
  town ([]:[[Expr]]
ess)  =  [][Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
:[[Expr]] -> [[Expr]]
town [[Expr]]
ess
  town []  =  []

  expand :: Expr -> [[Expr]]
  expand :: Expr -> [[Expr]]
expand Expr
e  =  case Expr -> [Expr]
holesBFS Expr
e of
    [] -> []
    (Expr
h:[Expr]
_) -> (Expr -> Expr) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr -> Expr -> Expr
fillBFS Expr
e) (Expr -> [[Expr]]
replacementsFor Expr
h)

  replacementsFor :: Expr -> [[Expr]]
  replacementsFor :: Expr -> [[Expr]]
replacementsFor Expr
h  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
h)
                     ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  [Expr] -> [[Expr]]
primitiveApplications [Expr]
primitives


-- 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 (Expr, Expr)
binding Expr
ep of
                  Just (Expr
v,Expr
e) -> Expr
v Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expr -> [Expr]
values Expr
ex
                  Maybe (Expr, Expr)
Nothing -> Bool
True
  where
  anormal :: Expr -> Bool
anormal (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e2 Bool -> Bool -> Bool
|| Expr -> Bool
isConst Expr
e1  =  Bool
True
  anormal Expr
_                                                    =  Bool
False
  binding :: Expr -> Maybe (Expr,Expr)
  binding :: Expr -> Maybe (Expr, Expr)
binding (Value String
"==" Dynamic
_ :$ Expr
e1 :$ Expr
e2) | Expr -> Bool
isVar Expr
e1   =  (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
e1,Expr
e2)
                                     | Expr -> Bool
isVar Expr
e2   =  (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
e2,Expr
e1)
  binding Expr
_                                       =  Maybe (Expr, Expr)
forall a. Maybe a
Nothing
keepIf Expr
_  =  String -> Bool
forall a. HasCallStack => String -> a
error String
"Conjure.Engine.keepIf: not an if"



--- normality checks ---

isRootNormal :: Thy -> Expr -> Bool
isRootNormal :: Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e  =  [(Expr, [(Expr, Expr)], Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Expr, [(Expr, Expr)], Expr)] -> Bool)
-> [(Expr, [(Expr, Expr)], Expr)] -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Triexpr Expr -> [(Expr, [(Expr, Expr)], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [(Expr, Expr)], a)]
T.lookup Expr
e Triexpr Expr
trie
  where
  trie :: Triexpr Expr
trie  =  [(Expr, Expr)] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList (Thy -> [(Expr, Expr)]
rules Thy
thy)

isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE :: Thy -> Expr -> Bool
isRootNormalE Thy
thy Expr
e  =  Thy -> Expr -> Bool
isRootNormal Thy
thy Expr
e
                    Bool -> Bool -> Bool
&&  [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr
e Expr -> Expr -> Bool
->-) [Expr
e2 Expr -> [(Expr, Expr)] -> Expr
//- [(Expr, Expr)]
bs | (Expr
_,[(Expr, Expr)]
bs,Expr
e2) <- Expr -> Triexpr Expr -> [(Expr, [(Expr, Expr)], Expr)]
forall a. Expr -> Triexpr a -> [(Expr, [(Expr, Expr)], a)]
T.lookup Expr
e Triexpr Expr
trie])
  where
  trie :: Triexpr Expr
trie  =  [(Expr, Expr)] -> Triexpr Expr
forall a. [(Expr, a)] -> Triexpr a
T.fromList ([(Expr, Expr)] -> Triexpr Expr) -> [(Expr, Expr)] -> Triexpr Expr
forall a b. (a -> b) -> a -> b
$ Thy -> [(Expr, Expr)]
equations Thy
thy [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ ((Expr, Expr) -> (Expr, Expr)) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> (Expr, Expr)
forall a b. (a, b) -> (b, a)
swap (Thy -> [(Expr, Expr)]
equations Thy
thy)
  ->- :: Expr -> Expr -> Bool
(->-)  =  Thy -> Expr -> Expr -> Bool
canReduceTo Thy
thy


--- tiers utils ---

productsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
productsWith :: ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f  =  ([a] -> a) -> [[[a]]] -> [[a]]
forall a b. (a -> b) -> [[a]] -> [[b]]
mapT [a] -> a
f ([[[a]]] -> [[a]]) -> ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[a]]] -> [[[a]]]
forall a. [[[a]]] -> [[[a]]]
products
-- TODO: move to LeanCheck?

delayedProductsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]]
delayedProductsWith :: ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith [a] -> a
f [[[a]]]
xsss  =  ([a] -> a) -> [[[a]]] -> [[a]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
productsWith [a] -> a
f [[[a]]]
xsss [[a]] -> Int -> [[a]]
forall a. [[a]] -> Int -> [[a]]
`addWeight` [[[a]]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[[a]]]
xsss
-- TODO: move to LeanCheck?

foldAppProducts :: Expr -> [ [[Expr]] ] -> [[Expr]]
foldAppProducts :: Expr -> [[[Expr]]] -> [[Expr]]
foldAppProducts Expr
ef  =  ([Expr] -> Expr) -> [[[Expr]]] -> [[Expr]]
forall a. ([a] -> a) -> [[[a]]] -> [[a]]
delayedProductsWith ([Expr] -> Expr
foldApp ([Expr] -> Expr) -> ([Expr] -> [Expr]) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:))