Test.hs

-----------------------------------------------------------------------------
-- |
-- Module     : Algebra.Graph.Test
-- Copyright  : (c) Andrey Mokhov 2016-2022
-- License    : MIT (see the file LICENSE)
-- Maintainer : andrey.mokhov@gmail.com
-- Stability  : experimental
--
-- Basic testsuite infrastructure.
-----------------------------------------------------------------------------
module Algebra.Graph.Test (
    module Data.List,
    module Data.List.Extra,
    module Test.QuickCheck,
    module Test.QuickCheck.Function,

    GraphTestsuite, (//), axioms, theorems, undirectedAxioms, reflexiveAxioms,
    transitiveAxioms, preorderAxioms, size10, test
    ) where

import Data.List (sort)
import Data.List.Extra (nubOrd)
import Prelude hiding ((+), (*))
import System.Exit (exitFailure)
import Test.QuickCheck hiding ((===))
import Test.QuickCheck.Function

import Algebra.Graph.Class
import Algebra.Graph.Test.Arbitrary ()

-- | Test a property only on small (at most size 10) inputs.
size10 :: Testable prop => prop -> Property
size10 = mapSize (min 10)

test :: Testable a => String -> a -> IO ()
test str p = do
    result <- quickCheckWithResult (stdArgs { chatty = False }) p
    if isSuccess result
        then putStrLn $ "OK: " ++ str
        else do
            putStrLn $ "\nTest failure:\n    " ++ str ++ "\n"
            putStrLn $ output result
            exitFailure

(+) :: Graph g => g -> g -> g
(+) = overlay

(*) :: Graph g => g -> g -> g
(*) = connect

(//) :: Testable prop => prop -> String -> Property
p // s = label s $ counterexample ("Failed when checking '" ++ s ++ "'") p

infixl 1 //
infixl 6 +
infixl 7 *

type GraphTestsuite g = (Ord g, Graph g) => g -> g -> g -> Property

axioms :: GraphTestsuite g
axioms x y z = conjoin
    [       x + y == y + x                 // "Overlay commutativity"
    , x + (y + z) == (x + y) + z           // "Overlay associativity"
    ,   empty * x == x                     // "Left connect identity"
    ,   x * empty == x                     // "Right connect identity"
    , x * (y * z) == (x * y) * z           // "Connect associativity"
    , x * (y + z) == x * y + x * z         // "Left distributivity"
    , (x + y) * z == x * z + y * z         // "Right distributivity"
    ,   x * y * z == x * y + x * z + y * z // "Decomposition" ]

theorems :: GraphTestsuite g
theorems x y z = conjoin
    [     x + empty == x                     // "Overlay identity"
    ,         x + x == x                     // "Overlay idempotence"
    , x + y + x * y == x * y                 // "Absorption"
    ,     x * y * z == x * y + x * z + y * z
                     + x + y + z + empty     // "Full decomposition"
    ,         x * x == x * x * x             // "Connect saturation"
    ,         empty <= x                     // "Lower bound"
    ,             x <= x + y                 // "Overlay order"
    ,         x + y <= x * y                 // "Overlay-connect order" ]

undirectedAxioms :: GraphTestsuite g
undirectedAxioms x y z = conjoin
    [ axioms x y z
    , x * y == y * x // "Connect commutativity" ]

reflexiveAxioms :: forall g. (Arbitrary (Vertex g), Show (Vertex g)) => GraphTestsuite g
reflexiveAxioms x y z = conjoin
    [ axioms x y z
    , forAll arbitrary (\v -> vertex @g v == vertex v * vertex v) // "Vertex self-loop" ]

transitiveAxioms :: GraphTestsuite g
transitiveAxioms x y z = conjoin
    [ axioms x y z
    , y == empty || x * y * z == x * y + y * z // "Closure" ]

preorderAxioms :: forall g. (Arbitrary (Vertex g), Show (Vertex g)) => GraphTestsuite g
preorderAxioms x y z = conjoin
    [ axioms x y z
    , forAll arbitrary (\v -> vertex @g v == vertex v * vertex v) // "Vertex self-loop"
    , y == empty || x * y * z == x * y + y * z                    // "Closure" ]