-- spec.hs: conjuring a function from a specification
--
-- Adapted from Colin Runciman's example "ListFuns"
import Conjure
import Test.LeanCheck (holds, exists)
import Prelude hiding (sum)


squareSpec :: (Int -> Int) -> Bool
squareSpec square  =  square 0 == 0
                   && square 1 == 1
                   && square 2 == 4

squareIngredients :: [Ingredient]
squareIngredients  =
  [ con (0::Int)
  , con (1::Int)
  , fun "+" ((+) :: Int -> Int -> Int)
  , fun "*" ((*) :: Int -> Int -> Int)
  ]

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


sumSpec :: ([Int] -> Int) -> Bool
sumSpec sum  =  sum []      == 0
             && sum [1,2]   == 3
             && sum [3,4,5] == 12

sumIngredients :: [Ingredient]
sumIngredients  =
  [ fun "null" (null :: [Int] -> Bool)
  , con (0::Int)
  , fun "+"    ((+) :: Int -> Int -> Int)
  , fun "head" (head :: [Int] -> Int)
  , fun "tail" (tail :: [Int] -> [Int])
  ]


appSpec :: ([Int] -> [Int] -> [Int]) -> Bool
appSpec (++)  =  []      ++ [0,1]   == [0,1]
              && [2,3]   ++ []      == [2,3]
              && [4,5,6] ++ [7,8,9] == [4,5,6,7,8,9]

appIngredients :: [Ingredient]
appIngredients =
  [ fun "null" (null :: [Int] -> Bool)
  , fun ":"    ((:) :: Int -> [Int] -> [Int])
  , fun "head" (head :: [Int] -> Int)
  , fun "tail" (tail :: [Int] -> [Int])
  ]


main :: IO ()
main = do
  conjureFromSpec "square" squareSpec squareIngredients
  conjureFromSpec "square" squarePropertySpec squareIngredients
  conjureFromSpec "sum" sumSpec sumIngredients
  conjureFromSpec "++"  appSpec appIngredients