-- |
-- Module      : Conjure.Ingredient
-- Copyright   : (c) 2021-2025 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of "Conjure".
--
-- The 'Ingredient' type and utilities involving it.
--
-- You are probably better off importing "Conjure".
module Conjure.Ingredient
  ( Ingredient
  , con
  , fun
  , iif
  , ordcase
  , guard
  , cjHoles
  , cjTiersFor
  , cjAreEqual
  , cjMkEquation
  , Prim
  , pr
  , prim
  , prif
  , primOrdCaseFor
  )
where

import Conjure.Conjurable
import Conjure.Expr
import Test.LeanCheck.Error (errorToFalse)
import Test.LeanCheck.Utils


-- | A single functional ingredient in conjuring.
-- Specify conjure ingredients with 'con' and 'fun':
--
-- > conjure "foo" foo [ con False
-- >                   , con True
-- >                   , con (0 :: Int)
-- >                   , con (1 :: Int)
-- >                   , ...
-- >                   , fun "&&" (&&)
-- >                   , fun "||" (||)
-- >                   , fun "+" ((+) :: Int -> Int -> Int)
-- >                   , fun "*" ((*) :: Int -> Int -> Int)
-- >                   , fun "-" ((-) :: Int -> Int -> Int)
-- >                   , ...
-- >                   ]
--
-- Ingredients may include arbitrary
-- constants ('con'),
-- constructors ('con')
-- or functions ('fun').
-- These may be built-in or user defined.
-- Use 'con' on 'Show' instances
-- and 'fun' otherwise.
--
-- This is internally
-- an arbitrary atomic 'Expr'ession
-- paired with
-- a 'Reification' of type information.
type Ingredient  =  (Expr, Reification)


-- | Provides a constant or constructor as an ingredient to Conjure.
--   To be used on 'Show' instances.
--   (cf. 'fun')
--
-- > conjure "foo" foo [ con False
-- >                   , con True
-- >                   , con (0 :: Int)
-- >                   , con (1 :: Int)
-- >                   , ...
-- >                   ]
--
-- Argument types have to be monomorphized,
-- so use type bindings when applicable.
con :: (Conjurable a, Show a) => a -> Ingredient
con :: forall a. (Conjurable a, Show a) => a -> Ingredient
con a
x  =  (a -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val a
x, a -> Reification
forall a. Conjurable a => a -> Reification
conjureType a
x)


-- | Provides a functional value as an ingredient to Conjure.
--   To be used on values that are not 'Show' instances
--   such as functions.
--   (cf. 'con')
--
-- > conjure "foo" foo [ ...
-- >                   , fun "&&" (&&)
-- >                   , fun "||" (||)
-- >                   , fun "+" ((+) :: Int -> Int -> Int)
-- >                   , fun "*" ((*) :: Int -> Int -> Int)
-- >                   , fun "-" ((-) :: Int -> Int -> Int)
-- >                   , ...
-- >                   ]
--
-- Argument types have to be monomorphized,
-- so use type bindings when applicable.
fun :: Conjurable a => String -> a -> Ingredient
fun :: forall a. Conjurable a => String -> a -> Ingredient
fun String
s a
x  =  (String -> a -> Expr
forall a. Typeable a => String -> a -> Expr
value String
s a
x, a -> Reification
forall a. Conjurable a => a -> Reification
conjureType a
x)


-- | Provides an if condition bound to the given return type
--   as a Conjure ingredient.
--
-- This should be used when one wants Conjure to consider
-- if-expressions at all:
--
-- > last' :: [Int] -> Int
-- > last' [x]  =  x
-- > last' [x,y]  =  y
-- > last' [x,y,z]  =  z
--
-- > > conjure "last" last' [ con ([] :: [Int])
-- > >                      , fun ":" ((:) :: Int -> [Int] -> [Int])
-- > >                      , fun "null" (null :: [Int] -> Bool)
-- > >                      , iif (undefined :: Int)
-- > >                      , fun "undefined" (undefined :: Int)
-- > >                      ]
-- > last :: [Int] -> Int
-- > -- 0.0s, testing 360 combinations of argument values
-- > -- 0.0s, pruning with 5/5 rules
-- > -- ...   ...   ...   ...   ...
-- > -- 0.0s, 4 candidates of size 7
-- > -- 0.0s, tested 2 candidates
-- > last []  =  undefined
-- > last (x:xs)  =  if null xs
-- >                 then x
-- >                 else last xs
iif :: Conjurable a => a -> Ingredient
iif :: forall a. Conjurable a => a -> Ingredient
iif a
x  =  (a -> Expr
forall a. Typeable a => a -> Expr
ifFor a
x, a -> Reification
forall a. Conjurable a => a -> Reification
conjureType a
x)


-- | Provides a guard bound to the conjured function's return type.
--
-- Guards are only alllowed at the root fo the RHS.
--
-- > last' :: [Int] -> Int
-- > last' [x]  =  x
-- > last' [x,y]  =  y
-- > last' [x,y,z]  =  z
--
-- > > conjure "last" last'
-- > >   [ con ([] :: [Int])
-- > >   , fun ":" ((:) :: Int -> [Int] -> [Int])
-- > >   , fun "null" (null :: [Int] -> Bool)
-- > >   , guard
-- > >   , fun "undefined" (undefined :: Int)
-- > >   ]
-- > last :: [Int] -> Int
-- > -- 0.0s, testing 360 combinations of argument values
-- > -- 0.0s, pruning with 5/5 rules
-- > -- 0.0s, 1 candidates of size 1
-- > -- 0.0s, 0 candidates of size 2
-- > -- 0.0s, 0 candidates of size 3
-- > -- 0.0s, 0 candidates of size 4
-- > -- 0.0s, 0 candidates of size 5
-- > -- 0.0s, 0 candidates of size 6
-- > -- 0.0s, 4 candidates of size 7
-- > -- 0.0s, tested 2 candidates
-- > last []  =  undefined
-- > last (x:xs)
-- >   | null xs  =  x
-- >   | otherwise  =  last xs
guard :: Ingredient
guard :: Ingredient
guard  =  (Bool -> Expr
forall a. Typeable a => a -> Expr
guardFor (Bool
forall a. HasCallStack => a
undefined :: Bool), Bool -> Reification
forall a. Conjurable a => a -> Reification
conjureType (Bool
forall a. HasCallStack => a
undefined :: Bool))
-- internally we always return a guard of the Bool return type,
-- this is replaced by Conjure when enumerating candidates


-- | Provides a case condition bound to the given return type.
--
-- This should be used when one wants Conjure to consider ord-case expressions:
--
-- > > conjure "mem" mem
-- > >   [ con False
-- > >   , con True
-- > >   , fun "`compare`" (compare :: Int -> Int -> Ordering)
-- > >   , ordcase (undefined :: Bool)
-- > >   ]
-- > mem :: Int -> Tree -> Bool
-- > -- ...   ...   ...   ...   ...
-- > -- 0.0s, 384 candidates of size 12
-- > -- 0.0s, tested 346 candidates
-- > mem x Leaf  =  False
-- > mem x (Node t1 y t2)  =  case x `compare` y of
-- >                          LT -> mem x t1
-- >                          EQ -> True
-- >                          GT -> mem x t2
ordcase :: Conjurable a => a -> Ingredient
ordcase :: forall a. Conjurable a => a -> Ingredient
ordcase a
x  =  (a -> Expr
forall a. Typeable a => a -> Expr
caseForOrd a
x, a -> Reification
forall a. Conjurable a => a -> Reification
conjureType a
x)


-- the following functions mirror their "conjure" counterparts from
-- Conjure.Conjurable but need a list of Ingredients instead of a Conjurable
-- representative.

-- | Computes a list of 'Reification1's from a list of 'Ingredient's.
--
-- This function mirrors functionality of 'conjureReification'.
cjReification :: [Ingredient] -> [Reification1]
cjReification :: [Ingredient] -> [Reification1]
cjReification [Ingredient]
ps  =  (Reification1 -> Expr) -> Reification
forall b a. Eq b => (a -> b) -> [a] -> [a]
nubOn (\(Expr
eh,Maybe Expr
_,Maybe [[Expr]]
_,[String]
_,[Expr]
_,Expr
_) -> Expr
eh)
                  Reification -> Reification
forall a b. (a -> b) -> a -> b
$  (Reification -> Reification -> Reification)
-> Reification -> [Reification] -> Reification
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Reification -> Reification -> Reification
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Reification
forall a. a -> a
id ((Ingredient -> Reification) -> [Ingredient] -> [Reification]
forall a b. (a -> b) -> [a] -> [b]
map Ingredient -> Reification
forall a b. (a, b) -> b
snd [Ingredient]
ps) [Bool -> Reification1
forall a. Conjurable a => a -> Reification1
conjureReification1 Bool
bool]

-- | Computes a list of holes encoded as 'Expr's from a list of 'Ingredient's.
--
-- This function mirrors functionality from 'conjureHoles'.
cjHoles :: [Ingredient] -> [Expr]
cjHoles :: [Ingredient] -> [Expr]
cjHoles [Ingredient]
ps  =  [Expr
eh | (Expr
eh,Maybe Expr
_,Just [[Expr]]
_,[String]
_,[Expr]
_,Expr
_) <- [Ingredient] -> [Reification1]
cjReification [Ingredient]
ps]

-- | Computes a function that equates two 'Expr's from a list of 'Ingredient's.
--
-- This function mirrors functionality from 'conjureMkEquation'.
cjMkEquation :: [Ingredient] -> Expr -> Expr -> Expr
cjMkEquation :: [Ingredient] -> Expr -> Expr -> Expr
cjMkEquation [Ingredient]
ps  =  [Expr] -> Expr -> Expr -> Expr
mkEquation [Expr
eq | (Expr
_,Just Expr
eq,Maybe [[Expr]]
_,[String]
_,[Expr]
_,Expr
_) <- [Ingredient] -> [Reification1]
cjReification [Ingredient]
ps]

-- | Given a list of 'Ingredient's,
--   computes a function that checks whether two 'Expr's are equal
--   up to a given number of tests.
cjAreEqual :: [Ingredient] -> Int -> Expr -> Expr -> Bool
cjAreEqual :: [Ingredient] -> Int -> Expr -> Expr -> Bool
cjAreEqual [Ingredient]
ps Int
maxTests  =  Expr -> Expr -> Bool
(===)
  where
  -==- :: Expr -> Expr -> Expr
(-==-)  =  [Ingredient] -> Expr -> Expr -> Expr
cjMkEquation [Ingredient]
ps
  Expr
e1 === :: Expr -> Expr -> Bool
=== Expr
e2  =  Expr -> Bool
isTrue (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
-==- Expr
e2
  isTrue :: Expr -> Bool
isTrue  =  (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
  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
. [Ingredient] -> Expr -> [Expr]
cjGrounds [Ingredient]
ps

-- | Given a list of 'Ingredient's,
--   computes a grounds function that lists
--   ground expressions of an 'Expr'.
cjGrounds :: [Ingredient] -> Expr -> [Expr]
cjGrounds :: [Ingredient] -> Expr -> [Expr]
cjGrounds  =  (Expr -> [[Expr]]) -> Expr -> [Expr]
grounds ((Expr -> [[Expr]]) -> Expr -> [Expr])
-> ([Ingredient] -> Expr -> [[Expr]])
-> [Ingredient]
-> Expr
-> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ingredient] -> Expr -> [[Expr]]
cjTiersFor

-- | Given a list of 'Ingredient's,
--   returns a function that given an 'Expr'
--   will return tiers of test 'Expr' values.
--
-- This is used in 'cjAreEqual'.
cjTiersFor :: [Ingredient] -> Expr -> [[Expr]]
cjTiersFor :: [Ingredient] -> Expr -> [[Expr]]
cjTiersFor [Ingredient]
ps Expr
e  =  [[[Expr]]] -> [[Expr]]
tf [[[Expr]]]
allTiers
  where
  allTiers :: [ [[Expr]] ]
  allTiers :: [[[Expr]]]
allTiers  =  [[[Expr]]
etiers | (Expr
_,Maybe Expr
_,Just [[Expr]]
etiers,[String]
_,[Expr]
_,Expr
_) <- [Ingredient] -> [Reification1]
cjReification [Ingredient]
ps]
  tf :: [[[Expr]]] -> [[Expr]]
tf []  =  [[Expr
e]] -- no tiers found, keep variable
  tf ([[Expr]]
etiers:[[[Expr]]]
etc)  =  case [[Expr]]
etiers of
                      ((Expr
e':[Expr]
_):[[Expr]]
_) | Expr -> TypeRep
typ Expr
e' TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e -> [[Expr]]
etiers
                      [[Expr]]
_                            -> [[[Expr]]] -> [[Expr]]
tf [[[Expr]]]
etc




-- | __DEPRACATED__.  Please use 'Ingredient' instead
type Prim  =  Ingredient
{-# DEPRECATED Prim "'Prim' is deprecated, please use 'Ingredient' instead" #-}


-- | __DEPRECATED__.  Please use 'con' instead.
pr :: (Conjurable a, Show a) => a -> Ingredient
pr :: forall a. (Conjurable a, Show a) => a -> Ingredient
pr  =  a -> Ingredient
forall a. (Conjurable a, Show a) => a -> Ingredient
con
{-# DEPRECATED pr "'pr' is deprecated, please use 'con' instead" #-}

-- | __DEPRECATED__.  Please use 'fun' instead.
prim :: Conjurable a => String -> a -> Ingredient
prim :: forall a. Conjurable a => String -> a -> Ingredient
prim  =  String -> a -> Ingredient
forall a. Conjurable a => String -> a -> Ingredient
fun
{-# DEPRECATED prim "'prim' is deprecated, please use 'fun' instead" #-}

prif :: Conjurable a => a -> Ingredient
prif :: forall a. Conjurable a => a -> Ingredient
prif  =  a -> Ingredient
forall a. Conjurable a => a -> Ingredient
iif
{-# DEPRECATED prif "'prif' is deprecated, please use 'iif' instead" #-}

primOrdCaseFor :: Conjurable a => a -> Ingredient
primOrdCaseFor :: forall a. Conjurable a => a -> Ingredient
primOrdCaseFor  =  a -> Ingredient
forall a. Conjurable a => a -> Ingredient
ordcase
{-# DEPRECATED primOrdCaseFor "'primOrdCaseFor' is deprecated, please use 'ordcase' instead" #-}