module Test.Speculate.Sanity
( instanceErrors
, eqOrdErrors
, eqErrors
, ordErrors
)
where
import Test.Speculate.Expr
import Test.LeanCheck ((==>))
import Data.List (intercalate)
(-==>-) :: Expr -> Expr -> Expr
e1 -==>- e2 = impliesE :$ e1 :$ e2 where impliesE = value "==>" (==>)
infixr 1 -==>-
(-&&-) :: Expr -> Expr -> Expr
e1 -&&- e2 = andE :$ e1 :$ e2 where andE = value "&&" (&&)
infixr 3 -&&-
eqErrors :: Instances -> Int -> TypeRep -> [String]
eqErrors is n t = takeWhile (const $ isListableT is 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 . isTrue (take n . grounds (lookupTiers is))
e1 -==- e2 = mkEquation is e1 e2
e = holeOfTy is t
x = "x" `varAsTypeOf` e
y = "y" `varAsTypeOf` e
z = "z" `varAsTypeOf` e
ordErrors :: Instances -> Int -> TypeRep -> [String]
ordErrors is n t = takeWhile (const $ isListableT is 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 . isTrue (take n . grounds (lookupTiers is))
e1 -==- e2 = mkEquation is e1 e2
e1 -<=- e2 = mkComparisonLE is e1 e2
e = holeOfTy is t
x = "x" `varAsTypeOf` e
y = "y" `varAsTypeOf` e
z = "z" `varAsTypeOf` e
eqOrdErrors :: Instances -> Int -> TypeRep -> [String]
eqOrdErrors is n t =
[ "(==) :: " ++ ty ++ " is not an equiavalence (" ++ intercalate ", " es ++ ")"
| listable, eq, let es = eqErrors is n t, not (null es) ]
++ [ "(<=) :: " ++ ty ++ " is not an ordering (" ++ intercalate ", " es ++ ")"
| listable, ord, let es = ordErrors is n t, not (null es) ]
++ [ "(==) and (<=) :: " ++ ty ++ " are inconsistent: (x == y) /= (x <= y && y <= x)"
| listable, eq, ord, f $ (x -==- y) -==- (x -<=- y -&&- y -<=- x) ]
where
listable = isListableT is t
eq = isEqT is t
ord = isOrdT is t
f = not . isTrue (take n . grounds (lookupTiers is))
e = holeOfTy is t
x = "x" `varAsTypeOf` e
y = "y" `varAsTypeOf` e
e1 -==- e2 = mkEquation is e1 e2
e1 -<=- e2 = mkComparisonLE is e1 e2
ty = show t ++ " -> " ++ show t ++ " -> Bool"
instanceErrors :: Instances -> Int -> [TypeRep] -> [String]
instanceErrors is n = concatMap $ eqOrdErrors is n