content: -- This program applies FitSpec to the Digraph library.
  --
  -- Usage:
  -- analyse properties about membership functions:
  --   ./digraphs [options] m
  --
  -- analyse properties about ispath and subgraph functions:
  --   ./digraphs [options] ps <refinement-id>
  --
  --
  -- This program is more complicated than it should, as it:
  --   * allows switching between two function-tuples/property-sets -- 'digraphs m' or 'digraphs ps';
  --   * allows switching between refinements -- 'digraphs ps 0', 'digraphs ps 1', ...;
  --   * uses polymorphism where it could use monomorphism.
  import Digraph as D
  import Test.FitSpec
  import Data.List ((\\))
  import qualified Data.List as L (delete)
  import Control.Monad
  
  instance (Ord a, Listable a) => Listable (Digraph a) where
    tiers = concatMapT graphs $ setsOf tiers
      where
      graphs ns = mapT (D . zip ns)
                $ listsOfLength (length ns) (setsOf $ toTiers ns)
  
  -- Our digraph instance above is too complicated.
  -- Simple reference implementation:
  listDigraphsInneficient :: (Ord a, Listable a) => [Digraph a]
  listDigraphsInneficient = concat tiers'
    where
    tiers' = cons1 D  `suchThat` okDigraph  `ofWeight` 0
  
  -- Tests Listable Digraph listable instance
  -- by comparing to an equivalent inneficient implementation:
  --
  -- > tiers === tiersDigraphsInneficient
  listableOK :: Bool
  listableOK = and
    [ holds 10000 $ \d -> okDigraph (d :: Digraph A)                  -- sound
    , take 100 list `subset` (listDigraphsInneficient :: [Digraph A]) -- sound
    , take 100 (listDigraphsInneficient :: [Digraph A]) `subset` list -- complete
    ]
    where xs `subset` ys = all (`elem` ys) xs
  
  -- For debugging the digraphs instance
  putDigraphs :: Int -> IO ()
  putDigraphs n = putStrLn . unlines . map (unlines . map show)
                $ take n (tiers :: [[Digraph A]])
  
  
  instance (Ord a, Listable a) => Mutable (Digraph a) where mutiers = mutiersEq
  
  instance (Ord a, Show a, Listable a) => ShowMutable (Digraph a) where
    mutantS = mutantSEq
  
  
  
  type Preds a = a -> Digraph a -> [a]
  type Succs a = a -> Digraph a -> [a]
  type IsNode a = a -> Digraph a -> Bool
  type IsEdge a = a -> a -> Digraph a -> Bool
  
  type TyM a = (Preds a, Succs a, IsNode a, IsEdge a)
  
  -- | properties about membership in a digraph
  propertiesM :: (Ord a, Eq a, Show a, Listable a) => TyM a -> [Property]
  propertiesM (preds, succs, isNode, isEdge) =
    [ property $ \d t   -> D.strictOrder (preds t d)
    , property $ \d s   -> D.strictOrder (succs s d)
    , property $ \d s t -> (s `elem` preds t d) == (t `elem` succs s d)
    , property $ \d s t -> (t `elem` succs s d) == isEdge s t d
    , property $ \d s t -> isEdge s t d ==> (isNode s d && isNode t d)
    , property $ \d s   -> isNode s d == (s `elem` D.nodes d)
    ]
  
  functionsM :: Ord a => TyM a
  functionsM = (preds,succs,isNode,isEdge)
  
  
  type IsPath a = a -> a -> Digraph a -> Bool
  type Subgraph a = [a] -> Digraph a -> Digraph a
  
  type TyPS a = (IsPath a, Subgraph a)
  
  -- | properties abouth path and subgraph
  propertiesPS :: (Ord a, Eq a, Show a, Listable a) => TyPS a -> [Property]
  propertiesPS (isPath, subgraph) =
    [ property $ \n d     -> isPath n n d == isNode n d
    , property $ \n1 n2 n3 d -> isPath n1 n2 d && isPath n2 n3 d ==> isPath n1 n3 d
    , property $ \d -> subgraph (D.nodes d) d == d
    , property $ \ns1 ns2 d -> subgraph ns1 (subgraph ns2 d) == subgraph ns2 (subgraph ns1 d)
    , property $ \n1 n2 ns d -> isPath n1 n2 (subgraph ns d) ==> isPath n1 n2 d
  
    -- 5-7
    , property $ \n1 n2 d -> isPath n1 n2 d ==> isNode n1 d && isNode n2 d
    , property $ \n1 n2 d -> isPath n1 n2 d && n1 /= n2 ==>
                                any (\n1' -> n1' /= n1 && isPath n1' n2 d) (succs n1 d)
    , property $ \n1 n2 d -> n1 /= n2 ==>
                   isPath n1 n2 d ==
                   let d' = subgraph (nodes d \\ [n1]) d in
                   any (\n1' -> isPath n1' n2 d')
                       (succs n1 d)
  
    -- 8-9
    , property $ \n ns d -> isNode n (subgraph ns d) == (isNode n d && n `elem` ns)
    , property $ \n1 n2 ns d -> isEdge n1 n2 (subgraph ns d)
              == (isEdge n1 n2 d && n1 `elem` ns && n2 `elem` ns)
    ]
  
  functionsPS :: Ord a => TyPS a
  functionsPS = (isPath, subgraph)
  
  
  
  extraMutantsM :: Ord a => [TyM a]
  extraMutantsM = []
  
  extraMutantsPS :: Ord a => [TyPS a]
  extraMutantsPS = drop 1
    [ (isPath, subgraph)
    , (\n1 n2 d -> isNode n1 d && isNode n2 d, subgraph)
    , (isPath, \ns d -> D [])
    ]
  
  main :: IO ()
  main = do
    unless listableOK
      $ putStrLn "WARNING: Listable Digraph is broken!  (read my source.)"
  
    as <- getArgsWith args { names = [ "isPath n1 n2 d"
                                     , "subgraph ns d" ] }
  
    let (pset,step) = case extra as of
                        (p:s:_) -> (p  ,read s)
                        [p]     -> (p  ,0)
                        []      -> ("m",0)
  
    case pset of
      "m" ->
        mainWith as { names = [ "preds n d"
                              , "succs n d"
                              , "isNode n d"
                              , "isEdge s t d" ] }
                    (functionsM :: TyM A)
                    propertiesM
  
      "ps" ->
        let is = case step of
                   0 -> [                   ]
                   1 -> [0,1,2,3,4          ]
                   2 -> [0,1,2,3,4,5,6      ]
                   3 -> [0,1,2,3,4,5,6,  8,9]
                   4 -> [0,1,2,3,4,5,  7,8,9]
                   5 -> [0,            7,8,9]
                   _ -> [0,1,2,3,4,5,6,7,8,9] -- not an actual step
        in
        mainWith as { names = [ "isPath n1 n2 d"
                              , "subgraph ns d" ] }
                    (functionsPS :: TyPS A)
                    ((!!! is) . propertiesPS)
  
  (!!!) :: [a] -> [Int] -> [a]
  xs !!! is = map (xs !!) is
  