-- |
-- 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
  ( module Data.Express
  , module Data.Express.Fixtures
  , module Test.Speculate.Engine
  , module Test.Speculate.Reason
  , Args(..)
  , args
  , conjure
  , conjureWith
  , conjpure
  , conjpureWith
  , candidateExprs
  , ifFor
  )
where

import Data.Express
import Data.Express.Fixtures hiding ((-==-))
import qualified Data.Ratio
import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)
import Test.Speculate hiding ((===), Args(..), args)
import Test.Speculate.Reason
import Test.Speculate.Engine
import Test.Speculate.Expr
import System.IO

import Conjure.Expr
import Conjure.Conjurable

-- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.
--   See 'args' for the defaults.
data Args = Args
  { Args -> Int
maxTests         :: Int  -- ^ defaults to 60
  , Args -> Int
maxSize          :: Int  -- ^ defaults to 9, keep greater than maxEquationSize
  , Args -> Int
maxEquationSize  :: Int  -- ^ defaults to 5, keep smaller than maxSize
  , Args -> Int
maxRecursionSize :: Int  -- ^ defaults to 60
  }

-- | Default arguments to conjure.
--
-- * 60 tests
-- * functions of up to 9 symbols
-- * pruning with equations up to size 5
-- * recursion up to 60 symbols.
args :: Args
args :: Args
args = Args :: Int -> Int -> Int -> Int -> Args
Args
  { maxTests :: Int
maxTests          =  Int
60
  , maxSize :: Int
maxSize           =   Int
9
  , maxEquationSize :: Int
maxEquationSize   =   Int
5
  , maxRecursionSize :: Int
maxRecursionSize  =  Int
60
  }

-- | Like 'conjure' but in the pure world.
--
-- Returns a triple whose:
--
-- 1. first element is the number of candidates considered
--
-- 2. second element is the number of defined points in the given function
--
-- 3. third element is a list of implementations encoded as 'Expr's
--    paired with the number of matching points.
conjpure :: Conjurable f => String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])
conjpure :: String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
conjpure =  Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
forall f.
Conjurable f =>
Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
conjpureWith Args
args

-- | Like 'conjpure' but allows setting options through 'Args' and 'args'.
conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])
conjpureWith :: Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
conjpureWith Args{Int
maxRecursionSize :: Int
maxEquationSize :: Int
maxSize :: Int
maxTests :: Int
maxRecursionSize :: Args -> Int
maxEquationSize :: Args -> Int
maxSize :: Args -> Int
maxTests :: Args -> Int
..} String
nm f
f [Expr]
es  =  ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
candidates,Int
totalDefined,) ([(Int, Expr)] -> (Int, Int, [(Int, Expr)]))
-> [(Int, Expr)] -> (Int, Int, [(Int, Expr)])
forall a b. (a -> b) -> a -> b
$ ((Int, Expr) -> (Int, Expr) -> Ordering)
-> [(Int, Expr)] -> [(Int, Expr)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int, Expr) -> (Int, Expr) -> Ordering
compareResult
  [ (Expr
ffxx Expr -> Expr -> Int
.=. Expr
re, Expr
ffxx Expr -> Expr -> Expr
-==- Expr
e)
  | Expr
e <- [Expr]
candidates
  , Expr -> Expr -> Bool
apparentlyTerminates Expr
rrff Expr
e
  , let re :: Expr
re = Int -> Expr -> Expr -> Expr
recursexpr Int
maxRecursionSize Expr
vffxx Expr
e
  , Expr
ffxx Expr -> Expr -> Bool
?=? Expr
re
  ]
  where
  totalDefined :: Int
totalDefined  =  Expr
ffxx Expr -> Expr -> Int
.=. Expr
ffxx
  candidates :: [Expr]
candidates  =  (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Expr
e -> Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
ffxx)
              ([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
.  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 -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall f.
Conjurable f =>
String
-> f -> Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]
candidateExprs String
nm f
f Int
maxEquationSize Expr -> Expr -> Bool
(===) [[Expr]
es]
  ffxx :: Expr
ffxx   =  String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
canonicalApplication String
nm f
f
  vffxx :: Expr
vffxx  =  String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
canonicalVarApplication String
nm f
f
  rrff :: Expr
rrff   =  String -> f -> Expr
forall a. Typeable a => String -> a -> Expr
var String
nm f
f

  (===), (?=?) :: Expr -> Expr -> Bool
  Expr
e1 === :: Expr -> Expr -> Bool
=== Expr
e2  =  Expr -> Bool
isReallyTrue      (Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2)
  Expr
e1 ?=? :: Expr -> Expr -> Bool
?=? Expr
e2  =  Expr -> Bool
isTrueWhenDefined (Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2)

  Expr
e1 .=. :: Expr -> Expr -> Int
.=. Expr
e2  =  Expr -> Int
countTrue         (Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2)
  -==- :: Expr -> Expr -> Expr
(-==-)  =  [Expr] -> Expr -> Expr -> Expr
mkEquation  [Expr]
eqs
    where
    eqs :: [Expr]
eqs  =  String -> (Bool -> Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"==" (Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Bool -> Bool -> Bool)
         Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:  [Expr]
es

  isTrueWhenDefined :: Expr -> Bool
isTrueWhenDefined  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
errorToTrue  (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 -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
gs
  isReallyTrue :: Expr -> Bool
isReallyTrue       =  (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
. Bool -> Expr -> Bool
forall a. Typeable a => a -> Expr -> a
eval Bool
False) ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
gs
  countTrue :: Expr -> Int
countTrue        =  (Expr -> Bool) -> [Expr] -> Int
forall a. (a -> Bool) -> [a] -> Int
count (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] -> Int) -> (Expr -> [Expr]) -> Expr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
gs

  gs :: Expr -> [Expr]
  gs :: Expr -> [Expr]
gs  =  Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
maxTests ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds (f -> Expr -> [[Expr]]
forall f. Conjurable f => f -> Expr -> [[Expr]]
tiersFor f
f)

-- | 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
-- >
-- > background :: [Expr]
-- > background =
-- >   [ val (0::Int)
-- >   , val (1::Int)
-- >   , value "+" ((+) :: Int -> Int -> Int)
-- >   , value "*" ((*) :: Int -> Int -> Int)
-- >   , value "==" ((==) :: Int -> Int -> Bool)
-- > ]
--
-- The conjure function does the following:
--
-- > > conjure "square" square background
-- > square :: Int -> Int
-- > -- looking through 815 candidates, 100% match, 3/3 assignments
-- > square x  =  x * x
--
-- The background is defined with 'val', 'value' and 'ifFor'.
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 options through 'Args' and 'args'.
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
nm f
f)
  String -> IO ()
putStr (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
ncs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" candidates"
  Handle -> IO ()
hFlush Handle
stdout
  case [(Int, Expr)]
rs of
    []    -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\ncannot conjure"
    ((Int
n,Expr
e):[(Int, Expr)]
_) -> do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
showMatch Int
n
                    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Expr -> String
showEq Expr
e
--  nes -> putStrLn . unlines $ "":[showEq e ++ "  -- " ++ show n | (n,e) <- nes]
  String -> IO ()
putStrLn String
""
  where
  (Int
ncs,Int
t,[(Int, Expr)]
rs)  =  Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
forall f.
Conjurable f =>
Args -> String -> f -> [Expr] -> (Int, Int, [(Int, Expr)])
conjpureWith Args
args String
nm f
f [Expr]
es
  showMatch :: Int -> String
showMatch Int
n  =  Int -> String
forall a. Show a => a -> String
show (Int
n Int -> Int -> Int
% Int
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"% match, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n 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
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" assignments"
  showEq :: Expr -> String
showEq Expr
eq  =  Expr -> String
showExpr (Expr -> Expr
lhs Expr
eq) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr (Expr -> Expr
rhs Expr
eq)

candidateExprs :: Conjurable f
               => String -> f
               -> Int
               -> (Expr -> Expr -> Bool)
               -> [[Expr]]
               -> [[Expr]]
candidateExprs :: String
-> f -> Int -> (Expr -> Expr -> Bool) -> [[Expr]] -> [[Expr]]
candidateExprs String
nm f
f Int
sz Expr -> Expr -> Bool
(===) [[Expr]]
ess  =  [[Expr]] -> [[Expr]]
expressionsT ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ [Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
exs] [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]]
ess
  where
  (Expr
ef:[Expr]
exs)  =  Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
canonicalVarApplication String
nm f
f
  thy :: Thy
thy  =  (Expr -> Expr -> Bool) -> Int -> [[Expr]] -> Thy
theoryFromAtoms Expr -> Expr -> Bool
(===) Int
sz ([[Expr]] -> Thy) -> [[Expr]] -> Thy
forall a b. (a -> b) -> a -> b
$ [[Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub (Expr
b_Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:(Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
holeAsTypeOf [Expr]
exs)] [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ [[Expr]]
ess
  expressionsT :: [[Expr]] -> [[Expr]]
expressionsT [[Expr]]
ds  =  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (\Expr
e -> (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
1)
                   ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  (Expr -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT (Thy -> Expr -> Bool
isRootNormalE Thy
thy)
                   ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  [[Expr]]
ds [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
\/ ([[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]]
delay ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Maybe Expr) -> [[Expr]] -> [[Expr]] -> [[Expr]]
forall a b c. (a -> b -> Maybe c) -> [[a]] -> [[b]] -> [[c]]
productMaybeWith Expr -> Expr -> Maybe Expr
($$) [[Expr]]
es [[Expr]]
es)
    where
    es :: [[Expr]]
es = [[Expr]] -> [[Expr]]
expressionsT [[Expr]]
ds

lhs, rhs :: Expr -> Expr
lhs :: Expr -> Expr
lhs (((Value String
"==" Dynamic
_) :$ Expr
e) :$ Expr
_)  =  Expr
e
rhs :: Expr -> Expr
rhs (((Value String
"==" Dynamic
_) :$ Expr
_) :$ Expr
e)  =  Expr
e

compareResult :: (Int,Expr) -> (Int,Expr) -> Ordering
compareResult :: (Int, Expr) -> (Int, Expr) -> Ordering
compareResult (Int
n1,Expr
e1) (Int
n2,Expr
e2)  =  Int
n2 Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
n1
                               Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Expr
e1 Expr -> Expr -> Ordering
`compareSimplicity` Expr
e2

(%) :: Int -> Int -> Int
Int
x % :: Int -> Int -> Int
% Int
y  =  Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
y