-------------------------------------------------------------------------
--- This module defines the interface of properties that can be checked
--- with the CurryCheck tool, an automatic property-based test tool
--- based on the EasyCheck library.
--- The ideas behind EasyCheck are described in
--- [this paper](http://www-ps.informatik.uni-kiel.de/~sebf/pub/flops08.html).
--- CurryCheck automatically tests properties defined with this library.
--- CurryCheck supports the definition of unit tests
--- (also for I/O operations) and property tests parameterized
--- over some arguments. CurryCheck is described in more detail in
--- [this paper](http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR16.html).
---
--- Basically, this module is a stub clone of the EasyCheck library
--- which contains only the interface of the operations used to specify
--- properties. Hence, this library does not import any other library.
--- This supports the definition of properties in any other module
--- (execept for the prelude).
---
--- @author Sebastian Fischer (with extensions by Michael Hanus)
--- @version January 2019
-------------------------------------------------------------------------

module Test.Prop (

  -- test specification:
  PropIO, returns, sameReturns, toError, toIOError,

  Prop, (==>), for, forAll,

  is, isAlways, isEventually, uniquely, always, eventually,
  failing, successful, deterministic, (-=-), (<~>), (~>), (<~), (<~~>),
  (#), (#<), (#>), (<=>),
  solutionOf,

  -- test annotations
  label, trivial, classify, collect, collectAs,

  -- enumerating values
  valuesOf

  ) where

import Test.Prop.Types

infix  1 `is`, `isAlways`, `isEventually`
infix  1 -=-, <~>, ~>, <~, <~~>, `trivial`, #, #<, #>, <=>
infix  1 `returns`, `sameReturns`
infixr 0 ==>

-------------------------------------------------------------------------
-- Properties involving I/O actions:

--- The property `returns a x` is satisfied if the execution of the
--- I/O action `a` returns the value `x`.
returns :: (Eq a, Show a) => IO a -> a -> PropIO
returns _ _ = propUndefinedError "returns"

--- The property `sameReturns a1 a2` is satisfied if the execution of the
--- I/O actions `a1` and `a2` return identical values.
sameReturns :: (Eq a, Show a) => IO a -> IO a -> PropIO
sameReturns _ _ = propUndefinedError "sameReturns"

--- The property `toError a` is satisfied if the evaluation of the argument
--- to normal form yields an exception.
toError :: a -> PropIO
toError _ = propUndefinedError "toError"

--- The property `toIOError a` is satisfied if the execution of the
--- I/O action `a` causes an exception.
toIOError :: IO a -> PropIO
toIOError _ = propUndefinedError "toIOError"


-------------------------------------------------------------------------
-- Standard properties to be checked:

--- The property `x -=- y` is satisfied if `x` and `y` have deterministic
--- values that are equal.
(-=-) ::(Eq a, Show a) =>  a -> a -> Prop
_ -=- _ = propUndefinedError "-=-"

--- The property `x <~> y` is satisfied if the sets of the values of
--- `x` and `y` are equal.
(<~>) :: (Eq a, Show a) => a -> a -> Prop
_ <~> _ = propUndefinedError "<~>"

--- The property `x ~> y` is satisfied if `x` evaluates to every value of `y`.
--- Thus, the set of values of `y` must be a subset of the set of values of `x`.
(~>) :: (Eq a, Show a) => a -> a -> Prop
_ ~> _ = propUndefinedError "~>"

--- The property `x <~ y` is satisfied if `y` evaluates to every value of `x`.
--- Thus, the set of values of `x` must be a subset of the set of values of `y`.
(<~) :: (Eq a, Show a) => a -> a -> Prop
_ <~ _ = propUndefinedError "<~"

--- The property `x <~~> y` is satisfied if the multisets of the values of
--- `x` and `y` are equal.
(<~~>) :: (Eq a, Show a) => a -> a -> Prop
_ <~~> _ = propUndefinedError "<~~>"

--- A conditional property is tested if the condition evaluates to `True`.
(==>) :: Bool -> Prop -> Prop
_ ==> _ = propUndefinedError "==>"

--- `solutionOf p` returns (non-deterministically) a solution
--- of predicate `p`. This operation is useful to test solutions
--- of predicates.
solutionOf :: (a -> Bool) -> a
solutionOf pred = pred x &> x where x free

--- The property `is x p` is satisfied if `x` has a deterministic value
--- which satisfies `p`.
is :: Show a => a -> (a -> Bool) -> Prop
is _ _ = propUndefinedError "is"

--- The property `isAlways x p` is satisfied if all values of `x` satisfy `p`.
isAlways :: Show a => a -> (a -> Bool) -> Prop
isAlways _ = propUndefinedError "isAlways"

--- The property `isEventually x p` is satisfied if some value of `x`
--- satisfies `p`.
isEventually :: Show a => a -> (a -> Bool) -> Prop
isEventually _ = propUndefinedError "isEventually"

--- The property `uniquely x` is satisfied if `x` has a deterministic value
--- which is true.
uniquely :: Bool -> Prop
uniquely _ = propUndefinedError "uniquely"

--- The property `always x` is satisfied if all values of `x` are true.
always :: Bool -> Prop
always _ = propUndefinedError "always"

--- The property `eventually x` is satisfied if some value of `x` is true.
eventually :: Bool -> Prop
eventually _ = propUndefinedError "eventually"

--- The property `failing x` is satisfied if `x` has no value.
failing :: Show a => a -> Prop
failing _ = propUndefinedError "failing"

--- The property `successful x` is satisfied if `x` has at least one value.
successful :: Show a => a -> Prop
successful _ = propUndefinedError "successful"

--- The property `deterministic x` is satisfied if `x` has exactly one value.
deterministic :: Show a => a -> Prop
deterministic _ = propUndefinedError "deterministic"

--- The property `x # n` is satisfied if `x` has `n` values.
(#) :: (Eq a, Show a) => a -> Int -> Prop
_ # _ =  propUndefinedError "#"

--- The property `x #< n` is satisfied if `x` has less than `n` values.
(#<) :: (Eq a, Show a) => a -> Int -> Prop
_ #< _ = propUndefinedError "#<"

--- The property `x #> n` is satisfied if `x` has more than `n` values.
(#>) :: (Eq a, Show a) => a -> Int -> Prop
_ #> _ = propUndefinedError "#>"

--- The property `for x p` is satisfied if all values `y` of `x`
--- satisfy property `p y`.
for :: Show a => a -> (a -> Prop) -> Prop
for _ _ = propUndefinedError "for"

--- The property `forAll xs p` is satisfied if all values `x` of the list `xs`
--- satisfy property `p x`.
forAll :: Show a => [a] -> (a -> Prop) -> Prop
forAll _ _ = propUndefinedError "forAll"

--- The property `f <=> g` is satisfied if `f` and `g` are equivalent
--- operations, i.e., they can be replaced in any context without changing
--- the computed results.
(<=>) :: a -> a -> Prop
_ <=> _ = propUndefinedError "#"

-------------------------------------------------------------------------
-- Test Annotations

--- Assign a label to a property.
--- All labeled tests are counted and shown at the end.
label :: String -> Prop -> Prop
label _ _ = propUndefinedError "label"

--- Assign a label to a property if the first argument is `True`.
--- All labeled tests are counted and shown at the end.
--- Hence, this combinator can be used to classify tests:
---
---     multIsComm x y = classify (x<0 || y<0) "Negative" $ x*y -=- y*x
---
classify :: Bool -> String -> Prop -> Prop
classify _ _ _ = propUndefinedError "classify"

--- Assign the label "trivial" to a property if the first argument is `True`.
--- All labeled tests are counted and shown at the end.
trivial :: Bool -> Prop -> Prop
trivial _ _ = propUndefinedError "trivial"

--- Assign a label showing the given argument to a property.
--- All labeled tests are counted and shown at the end.
collect :: Show a => a -> Prop -> Prop
collect _ _ = propUndefinedError "collect"

--- Assign a label showing a given name and the given argument to a property.
--- All labeled tests are counted and shown at the end.
collectAs :: Show a => String -> a -> Prop -> Prop
collectAs _ _ _ = propUndefinedError "collectAs"

-------------------------------------------------------------------------
-- Value generation

--- Computes the list of all values of the given argument
--- according to a given strategy (here:
--- randomized diagonalization of levels with flattening).
valuesOf :: a -> [a]
valuesOf =
  error "Test.Prop.valuesOf undefined. Use Test.EasyCheck to actually run it!"

propUndefinedError :: String -> _
propUndefinedError op = error $
  "Test.Prop." ++ op ++ " undefined. Use Test.EasyCheck to actually run it!"

-------------------------------------------------------------------------