-- |
-- Module      : Conjure.Defn.Test
-- Copyright   : (c) 2021-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of "Conjure".
--
-- This module exports functions that test 'Defn's using ground values.
--
-- You are probably better off importing "Conjure".
module Conjure.Defn.Test
  ( equalModuloTesting
  , erroneousCandidate
  , findDefnError
  )
where

import Conjure.Defn
import Conjure.Conjurable

import Test.LeanCheck.Error (errorToFalse, errorToNothing)

import Data.Dynamic (fromDyn, dynApp)


equalModuloTesting :: Conjurable f => Int -> Int -> String -> f -> Defn -> Defn -> Bool
equalModuloTesting :: forall f.
Conjurable f =>
Int -> Int -> String -> f -> Defn -> Defn -> Bool
equalModuloTesting Int
maxTests Int
maxEvalRecursions String
nm f
f  =  Defn -> Defn -> Bool
(===)
  where
  testGrounds :: [Expr]
testGrounds  =  Int -> Int -> String -> f -> [Expr]
forall f. Conjurable f => Int -> Int -> String -> f -> [Expr]
nonNegativeAppGrounds Int
maxTests Int
maxEvalRecursions String
nm f
f
  Defn
d1 === :: Defn -> Defn -> Bool
=== Defn
d2  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
are ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr]
testGrounds
    where
    -- silences errors, ok since this is for optional measuring of optimal pruning
    are :: Expr -> Bool
    are :: Expr -> Bool
are Expr
e  =  Bool -> Bool
forall a. a -> Bool
isError (Defn -> Defn -> Expr -> Bool
ee Defn
d1 Defn
d1 Expr
e)
           Bool -> Bool -> Bool
&& Bool -> Bool
forall a. a -> Bool
isError (Defn -> Defn -> Expr -> Bool
ee Defn
d2 Defn
d2 Expr
e)
           Bool -> Bool -> Bool
|| Bool -> Bool
errorToFalse (Defn -> Defn -> Expr -> Bool
ee Defn
d1 Defn
d2 Expr
e)
           where  ee :: Defn -> Defn -> Expr -> Bool
ee  =  Int -> f -> Defn -> Defn -> Expr -> Bool
forall f. Conjurable f => Int -> f -> Defn -> Defn -> Expr -> Bool
devlEqual Int
maxEvalRecursions f
f


-- | For debugging purposes.
--
-- This may be taken out of the API at any moment.
erroneousCandidate :: Conjurable f => Int -> Int -> String -> f -> Defn -> Bool
erroneousCandidate :: forall f. Conjurable f => Int -> Int -> String -> f -> Defn -> Bool
erroneousCandidate Int
maxTests Int
maxEvalRecursions String
nm f
f  =
  Maybe Expr -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Expr -> Bool) -> (Defn -> Maybe Expr) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> String -> f -> Defn -> Maybe Expr
forall f.
Conjurable f =>
Int -> Int -> String -> f -> Defn -> Maybe Expr
findDefnError Int
maxTests Int
maxEvalRecursions String
nm f
f


-- | For debugging purposes,
--   finds a set of arguments that triggers an error in the candidate 'Defn'.
--
-- Warning: this is an experimental function
-- which may be taken out of the API at any moment.
findDefnError :: Conjurable f => Int -> Int -> String -> f -> Defn -> Maybe Expr
findDefnError :: forall f.
Conjurable f =>
Int -> Int -> String -> f -> Defn -> Maybe Expr
findDefnError Int
maxTests Int
maxEvalRecursions String
nm f
f Defn
d  =
  (Expr -> Bool) -> [Expr] -> Maybe Expr
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Expr -> Bool
is [Expr]
testGrounds
  where
  testGrounds :: [Expr]
testGrounds  =  Int -> Int -> String -> f -> [Expr]
forall f. Conjurable f => Int -> Int -> String -> f -> [Expr]
nonNegativeAppGrounds Int
maxTests Int
maxEvalRecursions String
nm f
f
  is :: Expr -> Bool
  is :: Expr -> Bool
is Expr
e  =  Bool -> Bool
forall a. a -> Bool
isError (Int -> f -> Defn -> Defn -> Expr -> Bool
forall f. Conjurable f => Int -> f -> Defn -> Defn -> Expr -> Bool
devlEqual Int
maxEvalRecursions f
f Defn
d Defn
d Expr
e)


nonNegativeAppGrounds :: Conjurable f => Int -> Int -> String -> f -> [Expr]
nonNegativeAppGrounds :: forall f. Conjurable f => Int -> Int -> String -> f -> [Expr]
nonNegativeAppGrounds Int
maxTests Int
maxEvalRecursions String
nm f
f
  =  (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr -> Bool) -> [Expr] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
none Expr -> Bool
isNegative ([Expr] -> Bool) -> (Expr -> [Expr]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp)
  ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
maxTests
  ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  f -> Expr -> [Expr]
forall f. Conjurable f => f -> Expr -> [Expr]
conjureGrounds f
f (String -> f -> Expr
forall f. Conjurable f => String -> f -> Expr
conjureVarApplication String
nm f
f)


devlEqual :: Conjurable f => Int -> f -> Defn -> Defn -> Expr -> Bool
devlEqual :: forall f. Conjurable f => Int -> f -> Defn -> Defn -> Expr -> Bool
devlEqual Int
maxEvalRecursions f
f Defn
d1 Defn
d2 Expr
e  =
  Dynamic
eq Dynamic -> Dynamic -> Dynamic
`dynApp` Defn -> Expr -> Dynamic
evalDyn Defn
d1 Expr
e
     Dynamic -> Dynamic -> Dynamic
`dynApp` Defn -> Expr -> Dynamic
evalDyn Defn
d2 Expr
e Dynamic -> Bool -> Bool
forall a. Typeable a => Dynamic -> a -> a
`fromDyn` Bool
forall {a}. a
err
  where
  evalDyn :: Defn -> Expr -> Dynamic
evalDyn Defn
d Expr
e  =  Dynamic -> Maybe Dynamic -> Dynamic
forall a. a -> Maybe a -> a
fromMaybe Dynamic
forall {a}. a
err ((Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn (f -> Expr -> Expr
forall a. Conjurable a => a -> Expr -> Expr
conjureExpress f
f) Int
maxEvalRecursions Defn
d Expr
e)
  eq :: Dynamic
eq  =  f -> Dynamic
forall f. Conjurable f => f -> Dynamic
conjureDynamicEq f
f
  err :: a
err  =  String -> a
forall a. HasCallStack => String -> a
error String
"Conjure.devlEqual: evaluation error"
  -- We cannot use conjureMkEquation here because
  -- we need different Defns at each side of the equation
  -- so they have to be evaluated independently.

-- | Is the argument value an error value?
isError :: a -> Bool
isError :: forall a. a -> Bool
isError  =  Maybe a -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe a -> Bool) -> (a -> Maybe a) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
errorToNothing
-- There should not be a problem if this ever appears in LeanCheck:
-- imports are qualfied in this module.