-- |
-- Module      : Test.Speculate.Sanity
-- Copyright   : (c) 2016-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Speculate.
--
-- Sanity checks for before running the Speculate algorithm.
module Test.Speculate.Sanity
  ( instanceErrors
  , eqOrdErrors
  , eqErrors
  , ordErrors
  )
where

import Test.Speculate.Expr
import Test.LeanCheck ((==>))
import Data.List (intercalate)

(-==>-) :: Expr -> Expr -> Expr
Expr
e1 -==>- :: Expr -> Expr -> Expr
-==>- Expr
e2 = Expr
impliesE Expr -> Expr -> Expr
:$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2 where impliesE :: Expr
impliesE = String -> (Bool -> Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"==>" Bool -> Bool -> Bool
(==>)
infixr 1 -==>-

(-&&-) :: Expr -> Expr -> Expr
Expr
e1 -&&- :: Expr -> Expr -> Expr
-&&- Expr
e2 = Expr
andE Expr -> Expr -> Expr
:$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2 where andE :: Expr
andE = String -> (Bool -> Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"&&" Bool -> Bool -> Bool
(&&)
infixr 3 -&&-

-- returns a list of errors on the Eq instances (if any)
-- returns an empty list when ok
eqErrors :: Instances -> Int -> TypeRep -> [String]
eqErrors :: Instances -> Int -> TypeRep -> [String]
eqErrors Instances
is Int
n TypeRep
t = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> String -> Bool
forall a b. a -> b -> a
const (Bool -> String -> Bool) -> Bool -> String -> Bool
forall a b. (a -> b) -> a -> b
$ Instances -> TypeRep -> Bool
isListableT Instances
is TypeRep
t) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
     [String
"not reflexive"  | Expr -> Bool
f   (Expr
x Expr -> Expr -> Expr
-==- Expr
x)]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"not symmetric"  | Expr -> Bool
f  ((Expr
x Expr -> Expr -> Expr
-==- Expr
y) Expr -> Expr -> Expr
-==- (Expr
y Expr -> Expr -> Expr
-==- Expr
x))]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"not transitive" | Expr -> Bool
f (((Expr
x Expr -> Expr -> Expr
-==- Expr
y) Expr -> Expr -> Expr
-&&- (Expr
y Expr -> Expr -> Expr
-==- Expr
z)) Expr -> Expr -> Expr
-==>- (Expr
x Expr -> Expr -> Expr
-==- Expr
z))]
  where
  f :: Expr -> Bool
f = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Instances) -> Expr -> Bool
isTrue (Int -> Instances -> Instances
forall a. Int -> [a] -> [a]
take Int
n (Instances -> Instances)
-> (Expr -> Instances) -> Expr -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Instances]) -> Expr -> Instances
grounds (Instances -> Expr -> [Instances]
lookupTiers Instances
is))
  Expr
e1 -==- :: Expr -> Expr -> Expr
-==- Expr
e2 = Instances -> Expr -> Expr -> Expr
mkEquation Instances
is Expr
e1 Expr
e2
  e :: Expr
e = Instances -> TypeRep -> Expr
holeOfTy Instances
is TypeRep
t
  x :: Expr
x = String
"x" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  y :: Expr
y = String
"y" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  z :: Expr
z = String
"z" String -> Expr -> Expr
`varAsTypeOf` Expr
e

-- returns a list of errors on the Ord instance (if any)
ordErrors :: Instances -> Int -> TypeRep -> [String]
ordErrors :: Instances -> Int -> TypeRep -> [String]
ordErrors Instances
is Int
n TypeRep
t = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> String -> Bool
forall a b. a -> b -> a
const (Bool -> String -> Bool) -> Bool -> String -> Bool
forall a b. (a -> b) -> a -> b
$ Instances -> TypeRep -> Bool
isListableT Instances
is TypeRep
t) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
     [String
"not reflexive"     | Expr -> Bool
f   (Expr
x Expr -> Expr -> Expr
-<=- Expr
x)]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"not antisymmetric" | Expr -> Bool
f (((Expr
x Expr -> Expr -> Expr
-<=- Expr
y) Expr -> Expr -> Expr
-&&- (Expr
y Expr -> Expr -> Expr
-<=- Expr
x)) Expr -> Expr -> Expr
-==>- (Expr
x Expr -> Expr -> Expr
-==- Expr
y))]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"not transitive"    | Expr -> Bool
f (((Expr
x Expr -> Expr -> Expr
-<=- Expr
y) Expr -> Expr -> Expr
-&&- (Expr
y Expr -> Expr -> Expr
-<=- Expr
z)) Expr -> Expr -> Expr
-==>- (Expr
x Expr -> Expr -> Expr
-<=- Expr
z))]
  where
  f :: Expr -> Bool
f = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Instances) -> Expr -> Bool
isTrue (Int -> Instances -> Instances
forall a. Int -> [a] -> [a]
take Int
n (Instances -> Instances)
-> (Expr -> Instances) -> Expr -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Instances]) -> Expr -> Instances
grounds (Instances -> Expr -> [Instances]
lookupTiers Instances
is))
  Expr
e1 -==- :: Expr -> Expr -> Expr
-==- Expr
e2 = Instances -> Expr -> Expr -> Expr
mkEquation     Instances
is Expr
e1 Expr
e2
  Expr
e1 -<=- :: Expr -> Expr -> Expr
-<=- Expr
e2 = Instances -> Expr -> Expr -> Expr
mkComparisonLE Instances
is Expr
e1 Expr
e2
  e :: Expr
e = Instances -> TypeRep -> Expr
holeOfTy Instances
is TypeRep
t
  x :: Expr
x = String
"x" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  y :: Expr
y = String
"y" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  z :: Expr
z = String
"z" String -> Expr -> Expr
`varAsTypeOf` Expr
e

eqOrdErrors :: Instances -> Int -> TypeRep -> [String]
eqOrdErrors :: Instances -> Int -> TypeRep -> [String]
eqOrdErrors Instances
is Int
n TypeRep
t =
     [ String
"(==) :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  is not an equiavalence (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
     | Bool
listable, Bool
eq,  let es :: [String]
es = Instances -> Int -> TypeRep -> [String]
eqErrors  Instances
is Int
n TypeRep
t, Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
es) ]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"(<=) :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  is not an ordering ("     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
     | Bool
listable, Bool
ord, let es :: [String]
es = Instances -> Int -> TypeRep -> [String]
ordErrors Instances
is Int
n TypeRep
t, Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
es) ]
  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"(==) and (<=) :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" are inconsistent: (x == y) /= (x <= y && y <= x)"
     | Bool
listable, Bool
eq, Bool
ord, Expr -> Bool
f (Expr -> Bool) -> Expr -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr
x Expr -> Expr -> Expr
-==- Expr
y) Expr -> Expr -> Expr
-==- (Expr
x Expr -> Expr -> Expr
-<=- Expr
y Expr -> Expr -> Expr
-&&- Expr
y Expr -> Expr -> Expr
-<=- Expr
x) ]
  where
  listable :: Bool
listable = Instances -> TypeRep -> Bool
isListableT Instances
is TypeRep
t
  eq :: Bool
eq       = Instances -> TypeRep -> Bool
isEqT       Instances
is TypeRep
t
  ord :: Bool
ord      = Instances -> TypeRep -> Bool
isOrdT      Instances
is TypeRep
t
  f :: Expr -> Bool
f = Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Instances) -> Expr -> Bool
isTrue (Int -> Instances -> Instances
forall a. Int -> [a] -> [a]
take Int
n (Instances -> Instances)
-> (Expr -> Instances) -> Expr -> Instances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [Instances]) -> Expr -> Instances
grounds (Instances -> Expr -> [Instances]
lookupTiers Instances
is))
  e :: Expr
e = Instances -> TypeRep -> Expr
holeOfTy Instances
is TypeRep
t
  x :: Expr
x = String
"x" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  y :: Expr
y = String
"y" String -> Expr -> Expr
`varAsTypeOf` Expr
e
  Expr
e1 -==- :: Expr -> Expr -> Expr
-==- Expr
e2 = Instances -> Expr -> Expr -> Expr
mkEquation Instances
is Expr
e1 Expr
e2
  Expr
e1 -<=- :: Expr -> Expr -> Expr
-<=- Expr
e2 = Instances -> Expr -> Expr -> Expr
mkComparisonLE Instances
is Expr
e1 Expr
e2
  ty :: String
ty = TypeRep -> String
forall a. Show a => a -> String
show TypeRep
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show TypeRep
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> Bool"

instanceErrors :: Instances -> Int -> [TypeRep] -> [String]
instanceErrors :: Instances -> Int -> [TypeRep] -> [String]
instanceErrors Instances
is Int
n = (TypeRep -> [String]) -> [TypeRep] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((TypeRep -> [String]) -> [TypeRep] -> [String])
-> (TypeRep -> [String]) -> [TypeRep] -> [String]
forall a b. (a -> b) -> a -> b
$ Instances -> Int -> TypeRep -> [String]
eqOrdErrors Instances
is Int
n