{-# LANGUAGE CPP, FlexibleContexts #-}

{- |
   Module      : Data.Graph.Inductive.Query.Properties
   Description : Properties for Query modules
   Copyright   : (c) Ivan Lazar Miljenovic
   License     : BSD3
   Maintainer  : Ivan.Miljenovic@gmail.com

Rather than having an individual module of properties for each
`Data.Graph.Inductive.Query.*` module, this combines all such
properties and tests into one module.

 -}
module Data.Graph.Inductive.Query.Properties where

import Data.Graph.Inductive.Arbitrary
import Data.Graph.Inductive.Example      (clr595, vor)
import Data.Graph.Inductive.Graph
import Data.Graph.Inductive.PatriciaTree (Gr)
import Data.Graph.Inductive.Proxy
import Data.Graph.Inductive.Query

import Test.Hspec      (Spec, describe, it, shouldBe, shouldMatchList,
                        shouldSatisfy)
import Test.QuickCheck

import           Control.Arrow (second)
import           Data.List     (delete, sort, unfoldr, group, (\\))
import           Data.Maybe    (fromJust, isJust, isNothing)
import qualified Data.Set      as S

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative ((<*>))
#endif

{-# ANN module "HLint: ignore Use camelCase" #-}

-- -----------------------------------------------------------------------------
-- Articulation Points

-- | Deleting the articulation points should increase the number of
--   components.
test_ap :: (ArbGraph gr) => Proxy (gr a b) -> Undirected gr a b -> Property
test_ap _ ug = not (isEmpty g) ==>
                 null points || noComponents (delNodes points g) > noComponents g
  where
    g = toBaseGraph ug

    points = ap g

-- -----------------------------------------------------------------------------
-- BCC

-- | Test that the bi-connected components are indeed composed solely
--   from the original graph (and comprise the entire original graph).
test_bcc :: (ArbGraph gr, Ord b) => Proxy (gr a b) -> UConnected gr a b -> Bool
test_bcc _ cg = sort (concatMap labEdges bgs) == sort (labEdges g)
                                    -- Don't test labNodes as a node
                                    -- may be repeated in multiple
                                    -- bi-connected components.
  where
    g = connGraph cg

    bgs = bcc g

-- -----------------------------------------------------------------------------
-- BFS

test_bfs :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr a b -> Bool
test_bfs _ cg = sort (bfs (connNode cg) g) == sort (nodes g)
  where
    g = connGraph cg

test_level :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr a b -> Bool
test_level _ cg = sort expect == sort (level cn g)
  where
    g = connGraph cg

    cn = connNode cg

    vs = delete cn (nodes g)

    expect = (cn,0) : map (flip (,) 1) vs

-- esp tested as part of test_sp

-- -----------------------------------------------------------------------------
-- DFS

-- TODO: flesh out

-- | The 'components' function should never return an empty list, and
--   none of its sub-lists should be empty (unless the graph is
--   empty).  All nodes in the graph should be in precisely one of the
--   components.
test_components :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr a b -> Bool
test_components _ cg = all (not . null) cs && sort (concat cs) == sort (nodes g)
  where
    g = connGraph cg

    cs = components g

-- | The strongly connected components should be a partitioning of the
--   nodes of a graph.
test_scc :: (Graph gr) => Proxy (gr a b) -> gr a b -> Bool
test_scc _ g = sort (concat (scc g)) == sort (nodes g)

-- | Every node in an undirected connected graph should be reachable.
test_reachable :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr a b -> Property
test_reachable _ cg = not (isEmpty g) ==> sort (reachable v g) == sort (nodes g)
  where
    g = connGraph cg

    v = node' . fst . matchAny $ g

-- | The nodes of the condensation should be exactly the connected
-- components, and the edges of the condensation should correspond
-- exactly to the edges between the connected components.
test_condensation :: (Graph gr) => Proxy (gr a b) -> gr a b -> Bool
test_condensation _ g = sort sccs == sort (map snd $ labNodes cdg)
                        && and [ or [ hasEdge g (v,w) == hasEdge cdg (cv,cw)
                                    | v <- sccv, w <- sccw ]
                               | (cv,sccv) <- labNodes cdg
                               , (cw,sccw) <- labNodes cdg
                               , cv /= cw
                               ]
  where
    sccs = scc g
    cdg = condensation g

-- -----------------------------------------------------------------------------
-- Dominators

test_dom :: Spec
test_dom = describe "dom" $ do
  it "regular dom" $
    sortIt (dom domGraph 1) `shouldMatchList` [ (1, [1])
                                              , (2, [1,2])
                                              , (3, [1,2,3])
                                              , (4, [1,2,4])
                                              , (5, [1,2,5])
                                              , (6, [1,2,6])
                                              ]
  it "multiple components dom" $
    sortIt (dom domGraph1 1) `shouldMatchList` [ (1, [1])
                                               , (2, [1, 2])
                                               ]
  it "directed reachable components dom" $
    sortIt (dom domGraph2 1) `shouldMatchList` [ (1, [1]) ]

  it "unreachable nodes dom" $
    sortIt (dom domGraph3 1) `shouldMatchList` [(1,[1]), (2,[1,2])]

  where
    sortIt = map (second sort)

test_iDom :: Spec
test_iDom = it "iDom" $
  iDom domGraph 1 `shouldMatchList` [(2,1),(3,2),(4,2),(5,2),(6,2)]

-- Taken from <https://en.wikipedia.org/wiki/Dominator_%28graph_theory%29>
domGraph :: Gr () ()
domGraph = mkUGraph [1..6]
                    [ (1,2)
                    , (2,3)
                    , (2,4)
                    , (2,6)
                    , (3,5)
                    , (4,5)
                    , (5,2)
                    ]

-- This graph has two components (independent subgraphs)
domGraph1 :: Gr () ()
domGraph1 = mkUGraph [1..3]
                     [ (1,2)
                     ]

-- This graph has no reachables from 1 (but 1 is reachable)
domGraph2 :: Gr () ()
domGraph2 = mkUGraph [1..3]
                     [ (2,1)
                     , (2,2)
                     ]

-- From #109: 1 -> 2 <- 3
domGraph3 :: Gr () ()
domGraph3 = mkUGraph [1..3] [(1,2), (3,2)]

-- -----------------------------------------------------------------------------
-- GVD

test_voronoiSet :: Spec
test_voronoiSet = describe "voronoiSet" $ do
  describe "inwards" $ do
    it "with root node" (voronoiSet 4 vd `shouldMatchList` [1,2,4])
    it "other node"     (voronoiSet 1 vd `shouldSatisfy`   null)
  describe "outwards" $ do
    it "with root node" (voronoiSet 4 vd0 `shouldMatchList` [2,4,6,7])
    it "other node"     (voronoiSet 1 vd0 `shouldSatisfy`   null)

test_nearestNode :: Spec
test_nearestNode = describe "nearestNode" $ do
  describe "inwards" $ do
    it "reachable"   (nearestNode 6 vd `shouldBe` Just 5)
    it "unreachable" (nearestNode 7 vd `shouldBe` Nothing)
  describe "outwards" $ do
    it "reachable"   (nearestNode 6 vd0 `shouldBe` Just 4)
    it "unreachable" (nearestNode 1 vd0 `shouldBe` Nothing)

test_nearestDist :: Spec
test_nearestDist = describe "nearestDist" $ do
  describe "inwards" $ do
    it "root"        (nearestDist 4 vd `shouldBe` Just 0)
    it "reachable"   (nearestDist 1 vd `shouldBe` Just 3)
    it "unreachable" (nearestDist 7 vd `shouldBe` Nothing)
  describe "outwards" $ do
    it "root"        (nearestDist 5 vd0 `shouldBe` Just 0)
    it "reachable"   (nearestDist 7 vd0 `shouldBe` Just 4)
    it "unreachable" (nearestDist 1 vd0 `shouldBe` Nothing)

test_nearestPath :: Spec
test_nearestPath = describe "nearestPath" $ do
  describe "inwards" $ do
    it "reachable"   (nearestPath 1 vd `shouldBe` Just [1,4])
    it "unreachable" (nearestPath 7 vd `shouldBe` Nothing)
  describe "outwards" $ do
    it "reachable"   (nearestPath 7 vd0 `shouldBe` Just [7,6,4])
    it "unreachable" (nearestPath 1 vd0 `shouldBe` Nothing)

vd :: Voronoi Int
vd = gvdIn [4,5] vor

vd0 :: Voronoi Int
vd0 = gvdOut [4,5] vor

-- -----------------------------------------------------------------------------
-- Indep

-- TODO: how to prove that the found independent set is /maximal/?

-- | Make sure the size of independent sets is indeed accurate.
test_indepSize :: (ArbGraph gr) => Proxy (gr a b) -> gr a b -> Bool
test_indepSize _ ag = uncurry ((==) . length) (indepSize g)
  where
    g = toBaseGraph ag

-- | Is this really an independent set?
test_indep :: (ArbGraph gr) => Proxy (gr a b) -> gr a b -> Bool
test_indep _ ag = and . unfoldr checkSet . S.fromList $ indep g
  where
    g = toBaseGraph ag

    checkSet = fmap checkVal . S.minView

    checkVal (v,ws) = (S.null (S.fromList (neighbors g v) `S.intersection` ws), ws)

-- -----------------------------------------------------------------------------
-- MaxFlow2

-- As it is difficult to generate a suitable arbitrary graph for which
-- there /is/ a valid flow, we instead use unit tests based upon the
-- examples in the source code.

-- | Maximum flow of 2000
exampleNetwork1 :: Network
exampleNetwork1 = emap (flip (,) 0 . fromIntegral) exampleFlowGraph1

-- | Taken from "Introduction to Algorithms" (Cormen, Leiserson, Rivest).
--   This network has a maximum flow of 23
exampleNetwork2 :: Network
-- Names of nodes in "Introduction to Algorithms":
-- 1: s
-- 2: v1
-- 3: v2
-- 4: v3
-- 5: v4
-- 6: t
exampleNetwork2 = nemap (const ()) (flip (,) 0 . fromIntegral) clr595

clr595_network :: Network
clr595_network = maxFlowgraph clr595' 1 6
  where
    clr595' = nemap (const ()) fromIntegral clr595

test_maxFlow2_with :: String -> (Network -> Node -> Node -> (Network,Double)) -> Spec
test_maxFlow2_with nm f = it nm $ do
  snd (f exampleNetwork1 1 4) `shouldBe` 2000
  snd (f exampleNetwork2 1 6) `shouldBe` 23

test_maxFlow2 :: Spec
test_maxFlow2 = describe "MaxFlow2" $ do
  test_maxFlow2_with "ekSimple" ekSimple
  test_maxFlow2_with "ekFused"  ekFused
  test_maxFlow2_with "ekList"   ekList

-- -----------------------------------------------------------------------------
-- MaxFlow

-- TODO: test other exported functions.

exampleFlowGraph1 :: Gr () Int
exampleFlowGraph1 = mkGraph [ (1,()), (2,()), (3,()), (4,()) ]
                            [ (1,2,1000), (1,3,1000)
                            , (2,3,1), (2,4,1000), (3,4,1000)
                            ]

test_maxFlow :: Spec
test_maxFlow = it "maxFlow" $ do
  maxFlow exampleFlowGraph1 1 4 `shouldBe` 2000
  maxFlow clr595            1 6 `shouldBe` 23

-- -----------------------------------------------------------------------------
-- MST

-- | A minimum spanning tree of a connected, undirected graph should
--   cover all nodes, and all edges in the tree should be present in
--   the original graph.
test_msTree :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr () Int -> Bool
test_msTree _ cg = ns == mstNs && S.isSubsetOf mstEs es
  where
    g = connGraph cg -- a Connected graph is always non-empty

    mst = map unLPath (msTree g)

    ns = S.fromList (nodes g)
    es = S.fromList (labEdges g)

    mstNs = S.unions (map (S.fromList . map fst) mst)
    mstEs = S.unions (map (S.fromList . (zipWith toE <*> tail)) mst)

    toE (w,l) (v,_) = (v,w,l)

-- -----------------------------------------------------------------------------
-- SP

test_sp :: (ArbGraph gr) => Proxy (gr a b) -> UConnected gr () (Positive Int) -> Bool
test_sp _ cg = all test_p (map unLPath (msTree g))
  where
    -- Use Positive to avoid problems with distances containing
    -- negative lengths. The shortest path algorithm is Dijkstra's,
    -- which doesn't support negative weights.
    g = emap getPositive (connGraph cg)

    gCon = emap (const 1) g `asTypeOf` g

               -- Length-based test
    test_p p = length p >= len_gCon
               && length (esp v w gCon) == len_gCon
               -- Weighting-based test
               && sum (map snd p) >= fromJust (spLength v w g)
      where
        v = fst (head p)
        w = fst (last p)

        len_gCon = length (fromJust $ sp v w gCon)

-- | Test that 'spLength' and 'sp' return a length and an connecting
--   path when destination is reachable from source.
test_sp_Just :: (ArbGraph gr, Graph gr, Real b) =>
  Proxy (gr a b) -> gr a b -> Property
test_sp_Just _ g =
  case nodes g of
    u:v:_ ->
      v `elem` bfs u g ==>
      isJust (spLength u v g) &&
      case sp u v g of
        Nothing -> False
        Just path ->
          not (null path) &&
          head path == u &&
          last path == v
    _ -> property True

-- | Test that 'spLength' and 'sp' return 'Nothing' when destination
--   is not reachable from source.
test_sp_Nothing :: (ArbGraph gr, Graph gr, Real b) =>
  Proxy (gr a b) -> gr a b -> Property
test_sp_Nothing _ g =
  case nodes g of
    u:v:_ ->
      not (v `elem` bfs u g) ==>
        isNothing (spLength u v g) &&
        isNothing (sp u v g)
    _ -> property True

-- -----------------------------------------------------------------------------
-- TransClos

-- | The transitive, reflexive closure of a graph means that every
-- node is a successor of itself, and also that if (a, b) is an edge,
-- and (b, c) is an edge, then (a, c) must also be an edge.
test_trc :: DynGraph gr => Proxy (gr a b) -> (NoMultipleEdges gr) a b -> Bool
test_trc _ nme = all valid $ nodes gTrans
  where
    g       = emap (const ()) (nmeGraph nme)
    gTrans  = trc g
    valid n =
      -- For each node n, check that:
      --   the successors for n in gTrans are a superset of the successors for n in g.
      null (suc g n \\ suc gTrans n) &&
      --   the successors for n in gTrans are exactly equal to the reachable nodes for n in g, plus n.
      sort (suc gTrans n) == map head (group (sort (n:[ v | u <- suc g n, v <- reachable u g ])))

-- | The transitive closure of a graph means that if (a, b) is an
-- edge, and (b, c) is an edge, then (a, c) must also be an edge.
test_tc :: DynGraph gr => Proxy (gr a b) -> (NoMultipleEdges gr) a b -> Bool
test_tc _ nme = all valid $ nodes gTrans
  where
    g       = nmeGraph nme
    gTrans  = tc g
    valid n =
      -- For each node n, check that:
      --   the successors for n in gTrans are a superset of the successors for n in g.
      null (suc g n \\ suc gTrans n) &&
      --   the successors for n in gTrans are exactly equal to the reachable nodes for n in g.
      sort (suc gTrans n) == map head (group (sort [ v | u <- suc g n, v <- reachable u g ]))

-- | The reflexive closure of a graph means that all nodes are a
-- successor of themselves.
test_rc :: DynGraph gr => Proxy (gr a b) -> gr a b -> Bool
test_rc _ g = and [ n `elem` suc gRefl n | n <- nodes gRefl ]
  where
    gRefl = rc g

-- -----------------------------------------------------------------------------
-- Utility functions

type UConnected gr a b = Connected (Undirected gr) a b