module Test.Speculate.Sanity
( instanceErrors
, eqOrdErrors
, eqErrors
, ordErrors
)
where
import Test.Speculate.Expr
import Test.LeanCheck ((==>))
import Data.Maybe (fromMaybe)
import Data.List (intercalate)
import Test.Speculate.Utils
(-==>-) :: Expr -> Expr -> Expr
e1 -==>- e2 = impliesE :$ e1 :$ e2 where impliesE = constant "==>" (==>)
infixr 1 -==>-
(-&&-) :: Expr -> Expr -> Expr
e1 -&&- e2 = andE :$ e1 :$ e2 where andE = constant "&&" (&&)
infixr 3 -&&-
eqErrors :: Instances -> Int -> TypeRep -> [String]
eqErrors is n t =
["not reflexive" | f (x -==- x)]
++ ["not symmetric" | f ((x -==- y) -==- (y -==- x))]
++ ["not transitive" | f (((x -==- y) -&&- (y -==- z)) -==>- (x -==- z))]
where
f = not . true is n
e1 -==- e2 = fromMaybe falseE $ equation is e1 e2
x = Var "x" t
y = Var "y" t
z = Var "z" t
ordErrors :: Instances -> Int -> TypeRep -> [String]
ordErrors is n t =
["not reflexive" | f (x -<=- x)]
++ ["not antisymmetric" | f (((x -<=- y) -&&- (y -<=- x)) -==>- (x -==- y))]
++ ["not transitive" | f (((x -<=- y) -&&- (y -<=- z)) -==>- (x -<=- z))]
where
f = not . true is n
e1 -==- e2 = fromMaybe falseE $ equation is e1 e2
e1 -<=- e2 = fromMaybe falseE $ comparisonLE is e1 e2
x = Var "x" t
y = Var "y" t
z = Var "z" t
eqOrdErrors :: Instances -> Int -> TypeRep -> [String]
eqOrdErrors is n t =
[ "(==) :: " ++ ty ++ " is not an equiavalence (" ++ intercalate ", " es ++ ")"
| let es = eqErrors is n t, isEq is t, not (null es) ]
++ [ "(<=) :: " ++ ty ++ " is not an ordering (" ++ intercalate ", " es ++ ")"
| let es = ordErrors is n t, isOrd is t, not (null es) ]
++ [ "(==) and (<=) :: " ++ ty ++ " are inconsistent: (x == y) /= (x <= y && y <= x)"
| f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x)]
where
f = not . true is n
x = Var "x" t
y = Var "y" t
z = Var "z" t
e1 -==- e2 = fromMaybe falseE $ equation is e1 e2
e1 -<=- e2 = fromMaybe falseE $ comparisonLE is e1 e2
ty = show t ++ " -> " ++ show t ++ " -> Bool"
instanceErrors :: Instances -> Int -> [TypeRep] -> [String]
instanceErrors is n = concatMap $ eqOrdErrors is n