{-# LANGUAGE CPP                   #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE OverloadedLists       #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ViewPatterns          #-}
-- This file is part of the Haskell debugger Hoed.
--
-- Copyright (c) Maarten Faddegon, 2014-2017
module Debug.Hoed.Console(debugSession, showGraph) where

import           Control.Monad
import           Control.Arrow (first, second)
import           Data.Char
import           Data.Foldable            as F
import           Data.Graph.Libgraph      as G
import           Data.List                as List (foldl', group, mapAccumL, nub, sort)
import qualified Data.Map.Strict          as Map
import qualified Data.IntMap.Strict       as IntMap
import           Data.Maybe
import           Data.Sequence            (Seq, ViewL (..), viewl, (<|))
import qualified Data.Sequence            as Seq
import qualified Data.Set                 as Set
import           Data.Text (Text, unpack)
import qualified Data.Text                as T
import qualified Data.Text.IO             as T
import qualified Data.Vector              as V
import qualified Data.Vector.Generic      as VG
import           Data.Word
import           Debug.Hoed.Compat
import           Debug.Hoed.CompTree
import           Debug.Hoed.Observe
import           Debug.Hoed.Prop
import           Debug.Hoed.ReadLine
import           Debug.Hoed.Render
import           Debug.Hoed.Serialize
import           Prelude                  hiding (Right)
import           System.Directory
import           System.Exit
import           System.IO
import           System.Process
import           Text.PrettyPrint.FPretty hiding ((<$>))
import           Text.Regex.TDFA
import           Text.Regex.TDFA.Text
import           Web.Browser

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

--------------------------------------------------------------------------------
-- events
type Id = Int
-- | A representation of an event as a span
data Span = Span { spanStart, spanEnd :: Id, polarity :: Bool } deriving (Eq, Ord, Show)
-- | A representation of a trace as a span diagram: a list of columns of spans.
type Spans = [ [Span] ]
-- | The nesting depth of a span
type Depth = Int

-- | Recover the spans from the trace and arrange the columns such that they reflect
--   span containment. A span @b@ is contained in another span @a@ if
--
--   > start b > start a && end b < end a
--
--   The span in column N is contained below N other spans.
--   The renderer should draw the columns left to right.
traceToSpans :: (UID -> EventWithId) -> Trace -> Spans
traceToSpans lookupEvent =
  map sort .
  Map.elems .
  Map.fromListWith (++) .
  map (second (: [])) . snd . VG.ifoldl' (traceToSpans2' lookupEvent) ([], [])

-- This version tries to distinguish between Fun events that terminate a span,
-- and Fun events that signal a second application of a function
traceToSpans2'
  :: (UID -> EventWithId)
  -> (Seq Id, [(Depth, Span)])
  -> UID
  -> Event
  -> (Seq Id, [(Depth, Span)])
traceToSpans2' lookupEv (stack, result) uid e
  | isStart (change e) = (uid <| stack, result)
  | start :< stack' <- viewl stack
  , isEnd lookupEv uid e =
    ( stack'
    , (Seq.length stack', Span start uid (getPolarity e)) : result)
  | otherwise = (stack, result)
  where
    isStart Enter {} = True
    isStart _ = False
    getPolarity Event {change = Observe {}} = True
    getPolarity Event {eventParent = Parent p 0}
      | Event {change = Fun} <- event $ lookupEv p =
        not $ getPolarity (event $ lookupEv p)
    getPolarity Event {eventParent = Parent p _} = getPolarity (event $ lookupEv p)

isEnd lookupEv _ Event {change = Cons {}} = True
isEnd lookupEv uid me@(Event {change = Fun {}}) =
  case prevEv of
    Event{change = Enter{}} -> eventParent prevEv == eventParent me
    _ -> False
  where
    prevEv= event $ lookupEv (uid - 1)
isEnd _ _ _ = False

printTrace :: Trace -> IO ()
printTrace trace =
  putStrLn $
  renderTrace' lookupEvent lookupDescs (traceToSpans lookupEvent trace, trace)
    -- fast lookup via an array
  where
    lookupEvent i = EventWithId i (trace VG.! i)
    lookupDescs =
      (fromMaybe [] .
       (`IntMap.lookup` (IntMap.fromListWith
                           (++)
                           [ (p, [EventWithId uid e])
                           | (uid, e@Event {eventParent = Parent p _}) <-
                               VG.toList (VG.indexed trace)
                           ])))

-- | TODO to be improved
renderTrace :: (Spans, Trace) -> IO ()
renderTrace (spans, trace) = do
  putStrLn "Events"
  putStrLn "------"
  VG.mapM_ print trace
  putStrLn ""
  putStrLn "Spans"
  putStrLn "-----"
  mapM_ print spans

renderTrace' :: (UID -> EventWithId)
             -> (UID -> [EventWithId])
             -> (Spans, Trace)
             -> String
renderTrace' lookupEvent lookupDescs (columns, events) = unlines renderedLines
    -- roll :: State -> (Event, Maybe ColumnEvent) -> (State, String)
  where
    depth = length columns
    ((_, evWidth), renderedLines) =
      mapAccumL roll (replicate (depth + 1) ' ', 0)
      $ align (uncurry EventWithId <$> VG.toList (VG.indexed events)) columnEvents
    -- Merge trace events and column events
    align (ev:evs) (colEv@(rowIx, colIx, pol, isStart):colEvs)
      | eventUID ev == rowIx = (ev, Just (colIx, pol, isStart)) : align evs colEvs
      | otherwise = (ev, Nothing) : align evs (colEv : colEvs)
    align [] [] = []
    align ev [] = map  (\x -> (x, Nothing)) ev
    -- Produce the output in three columns: spans, events, and explains
    -- For spans: keep a state of the open spans
    --   (the state is the rendering in characters)
    -- For events: keep a state of the widest event
    -- For explains: circularly reuse the widest event result
    roll (state, width) (ev, Nothing)
      | (w, s) <- showWithExplains ev = ((state, max width w), state ++ s)
    roll (state, width) (ev, Just (col, pol, True))
      | state' <- update state col '|'
      , state'' <- update state col (if pol then '↑' else '┬')
      , (w, s) <- showWithExplains ev = ((state', max width w), state'' ++ s)
    roll (state, width) (ev, Just (col, pol, False))
      | state' <- update state col ' '
      , state'' <- update state col (if pol then '↓' else '┴')
      , (w, s) <- showWithExplains ev = ((state', max width w), state'' ++ s)
    -- columnEvents :: [(Line,ColIndex,StartOrEnd)]
    -- view the column spans as an event stream
    -- there's an event when a span starts or ends
    columnEvents =
      sortOn
        (\(a, b, c, d) -> a)
        [ (rowIx, colIx, pol, isStart)
        | (colIx, spans) <- zip [0 ..] columns
        , Span {..} <- spans
        , (rowIx, pol, isStart) <- [(spanStart, polarity, True), (spanEnd, polarity, False)]
        ]
    -- update element n of a list with a new value v
    update [] _ _ = []
    update (_:xs) 0 v = v : xs
    update (x:xs) n v = x : update xs (n - 1) v
    -- show the event, add the necessary padding to fill the event col width,
    -- and append the explain.
    showWithExplains ev
      | showEv <- show ev
      , l <- length showEv =
        (l, showEv ++ replicate (evWidth - l) ' ' ++ explain (eventUID ev) (event ev))
    -- Value requests
    explain uid Event {eventParent = Parent p 0, change = Enter}
      | Event {change = Fun, eventParent = Parent p' _} <- event $ lookupEvent p
      , (name,dist) <- findRoot (event $ lookupEvent p') =
        "-- request arg of " ++ unpack name ++ "/" ++ show (dist + 1)
    explain uid Event {eventParent = Parent p 1, change = Enter}
      | Event {change = Fun, eventParent = Parent p' _} <- event $ lookupEvent p
      , (name,dist) <- findRoot (event $ lookupEvent p') =
        "-- request result of " ++ unpack name ++ "/" ++ show (dist+1)
    explain uid Event {eventParent = Parent p 0, change = Enter}
      | Event {change = Observe name} <- event $ lookupEvent p =
        "-- request value of " ++ unpack name
    explain uid Event {eventParent = Parent p i, change = Enter}
      | Event {change = Cons ar name} <- event $ lookupEvent p =
        "-- request value of arg " ++ show i ++ " of constructor " ++ unpack name
    -- Arguments of functions
    explain uid me@Event {eventParent = Parent p 0, change = it@FunOrCons}
      | Event {change = Fun, eventParent = Parent p' _} <- event $ lookupEvent p
      , (name,dist) <- findRoot (event $ lookupEvent p') =
        "-- arg " ++ show (dist+1) ++ " of " ++ unpack name ++ " is " ++ showChange it
    -- Results of functions
    explain uid Event {eventParent = Parent p 1, change = it@Fun}
      | Event {change = Fun, eventParent = Parent p' _} <- event $ lookupEvent p
      , (name,dist) <- findRoot (event $ lookupEvent p') =
        "-- result of " ++ unpack name ++ "/" ++ show (dist+1) ++ " is a function"
    explain uid me@Event {eventParent = Parent p 1, change = Cons{}}
      | Event {change = Fun, eventParent = Parent p' _} <- event $ lookupEvent p
      , (name,dist) <- findRoot (event $ lookupEvent p')
      , arg <- findArg p =
        "-- " ++ unpack name ++ "/" ++ show (dist+1) ++ " " ++ arg ++" = " ++ findValue lookupDescs (EventWithId uid me)
    -- Descendants of Cons events
    explain uid Event {eventParent = Parent p i, change = Cons _ name}
      | Event {change = Cons ar name'} <- event $ lookupEvent p =
        "-- arg " ++ show i ++ " of constructor " ++ unpack name' ++ " is " ++ unpack name
    -- Descendants of root events
    explain uid Event {eventParent = Parent p i, change = Fun}
      | Event {change = Observe name} <- event $ lookupEvent p =
        "-- " ++ unpack name ++ " is a function"
    explain uid me@Event {eventParent = Parent p i, change = Cons{}}
      | Event {change = Observe name} <- event $ lookupEvent p =
        "-- " ++ unpack name ++ " = " ++ findValue lookupDescs (EventWithId uid me)
    explain _ _ = ""

    -- Returns the root observation for this event, together with the distance to it
    findRoot Event{change = Observe name} = (name, 0)
    findRoot Event{eventParent} = succ <$> findRoot (event $ lookupEvent $ parentUID eventParent)

    variableNames = map (:[]) ['a'..'z']

    showChange Fun = "a function"
    showChange (Cons ar name) = "constructor " ++ unpack name

    findArg eventUID =
      case [ e | e@(event -> Event{eventParent = Parent p 0, change = Cons{}}) <- lookupDescs eventUID] of
        [cons] -> findValue lookupDescs cons
        other  -> error $ "Unexpected set of descendants of " ++ show eventUID ++ ": Fun - " ++ show other

findValue :: (UID -> [EventWithId]) -> EventWithId -> String
findValue lookupDescs = go
  where
    go :: EventWithId -> String
    go EventWithId {eventUID = me, event = Event {change = ConsChar c}} = show c
    go EventWithId {eventUID = me, event = Event {change = Cons ar name}}
      | ar == 0 = unpack name
      | isAlpha (T.head name) =
        unpack name ++
        " " ++
        unwords
          (map go $
           sortOn
             (parentPosition . eventParent . event)
             [e | e@EventWithId {event = Event {change = Cons {}}} <- lookupDescs me])
      | ar == 1
      , [a] <- [e | e@EventWithId {event = Event {change = Cons {}}} <- lookupDescs me] = unpack name ++ go a
      | ar == 2
      , [a, b] <- sortOn (parentPosition . eventParent . event) [e | e@(event -> Event {change = Cons {}}) <- lookupDescs me] =
        unwords [go a, unpack name, go b]
    go EventWithId {eventUID, event = Event {change = Enter {}}}
      | [e] <- lookupDescs eventUID = go e
    go other = error $ show other

data RequestDetails = RD Int Explanation

data ReturnDetails
  = ReturnFun
  | ReturnCons { constructor :: Text, arity :: Word8, value :: String}

data Explanation
  = Observation String
  | Request RequestDetails
  | Return RequestDetails ReturnDetails

instance Show Explanation where
  show (Observation obs) = ""
  show (Request r) = "request " ++ showRequest r
  show (Return r val) = showReturn r val

showRequest (RD 0 (Observation name)) = unwords ["value of", name]
showRequest (RD 0 (Return (RD _ (Observation name)) ReturnFun)) = unwords ["arg of", name]
showRequest (RD 1 (Return (RD _ (Observation name)) ReturnFun)) = unwords ["result of", name]
showRequest (RD n (Return _ (ReturnCons name ar _))) = unwords ["arg", show n, "of constructor", unpack name ]

showReturn (RD p (Observation obs)) ReturnFun = unwords ["result of ", obs, "is a function"]
showReturn (RD p req) (ReturnCons name ar val) = unwords [show req, "=", val]

buildExplanation :: (UID -> EventWithId) -> (UID -> [EventWithId]) -> EventWithId -> Explanation
buildExplanation lookupEvent lookupDescs = go . event where
  go Event{eventParent = Parent p pos, change = Enter}
    | par <- go (event $ lookupEvent p)
    = Request (RD 0 par)
  go Event{eventParent = Parent p pos, change = Fun}
    | Request rd <- go (event $ lookupEvent p)
    = Return rd ReturnFun
  go Event{eventParent = Parent p pos, change = Cons ar name}
    | Request rd <- go (event $ lookupEvent p)
    , value <- findValue lookupDescs (lookupEvent p)
    = Return rd (ReturnCons name ar value)


eitherFunOrCons Fun{} = True
eitherFunOrCons Cons {} = True
eitherFunOrCons _ = False

pattern FunOrCons <- (eitherFunOrCons -> True)

--------------------------------------------------------------------------------
-- Debug session

debugSession :: Trace -> CompTree -> [Propositions] -> IO ()
debugSession trace tree ps =
  case filter (not . isRootVertex) vs of
    []    -> putStrLn $ "No functions annotated with 'observe' expressions"
                        ++ " or annotated functions not evaluated"
    (v:_) -> do noBuffering
                mainLoop v trace tree ps
  where
  (Graph _ vs _) = tree

--------------------------------------------------------------------------------
-- Execution loop

type Frame state = state -> IO (Transition state)

data Transition state
  = Down (Frame state)
  | Up   (Maybe state)
  | Next state
  | Same

executionLoop :: [Frame state] -> state -> IO ()
executionLoop [] _ = return ()
executionLoop stack@(runFrame : parents) state = do
  transition <- runFrame state
  case transition of
    Same         -> executionLoop stack state
    Next st      -> executionLoop stack st
    Up Nothing   -> executionLoop parents state
    Up (Just st) -> executionLoop parents st
    Down loop    -> executionLoop (loop : stack) state

--------------------------------------------------------------------------------
-- Commands

type Args = [String]

data Command state = Command
  { name        :: String
  , argsDesc    :: [String]
  , commandDesc :: Doc
  , parse       :: Args -> Maybe (state -> IO (Transition state))
  }

interactiveFrame :: String -> [Command state] -> Frame state
interactiveFrame prompt commands state = do
  input <- readLine (prompt ++ " ") (map name commands)
  let run = fromMaybe (\_ -> Same <$ showHelp commands) $ selectCommand input
  run state
  where
    selectCommand = selectFrom commands

showHelp :: [Command state] -> IO ()
showHelp commands =
  putStrLn (pretty 80 $ vcat $ zipWith compose commandsBlock descriptionsBlock)
  where
    compose c d = text (pad c) <+> align d
    commandsBlock = [unwords (name : argsDesc) | Command {..} <- commands]
    descriptionsBlock = map commandDesc commands
    colWidth = maximum $ map length commandsBlock
    pad x = take (colWidth + 1) $ x ++ spaces
    spaces = repeat ' '

helpCommand :: [Command state1] -> Command state2
helpCommand commands =
  Command "help" [] "Shows this help screen." $ \case
    [] -> Just $ \_ -> Same <$ showHelp commands
    _  -> Nothing

selectFrom :: [Command state] -> String -> Maybe (state -> IO (Transition state))
selectFrom commands =
  \case
    "" -> Nothing
    xx -> do
      let (h:t) = words xx
      c <- Map.lookup h commandsMap
      parse c t
  where
    commandsMap = Map.fromList [(name c, c) | c <- commands]


--------------------------------------------------------------------------------
-- main menu

data State = State
  { cv       :: Vertex
  , trace    :: Trace
  , compTree :: CompTree
  , ps       :: [Propositions]
  }

adbCommand, graphCommand, observeCommand, listCommand, exitCommand :: Command State
adbCommand =
  Command "adb" [] "Start algorithmic debugging." $ \case
    [] -> Just $ \_ -> return $ Down adbFrame
    _  -> Nothing

observeCommand =
  Command
    "observe"
    ["[regexp]"]
    ("Print computation statements that match the regular expression." </>
     "Omitting the expression prints all the statements.") $ \case
    args -> Just $ \State {..} ->
      let regexp = case args of [] -> ".*" ; _ -> unwords args
      in Same <$ printStmts compTree regexp

listCommand =
  Command "list" [] "List all the observables collected." $
    \args -> Just $ \State{..} ->
      let regexp = makeRegex $ case args of [] -> ".*" ; _ -> unwords args
      in Same <$ listStmts compTree regexp

graphCommand =
  Command "graph" ["regexp"]
    ("Show the computation graph of an expression." </>
     "Requires graphviz dotp.") $ \case
        regexp -> Just $ \State{..} -> Same <$ graphStmts (unwords regexp) compTree

eventsCommand =
  Command "events" [] "Print the Event trace (useful only for debugging Hoed)" $ \case
    [] -> Just $ \State{..} -> Same <$ printTrace trace
    _  -> Nothing

exitCommand =
  Command "exit" [] "Leave the debugging session." $ \case
    [] -> Just $ \_ -> return (Up Nothing)
    _  -> Nothing

mainLoopCommands :: [Command State]
mainLoopCommands =
  sortOn name
    [ adbCommand
#ifdef DEBUG
    , eventsCommand
#endif
    , graphCommand
    , listCommand
    , observeCommand
    , exitCommand
    , helpCommand mainLoopCommands
    ]

mainLoop :: Vertex -> Trace -> CompTree -> [Propositions] -> IO ()
mainLoop cv trace compTree ps =
  executionLoop [interactiveFrame "hdb>" mainLoopCommands] $
  State cv trace compTree ps

--------------------------------------------------------------------------------
-- list

listStmts :: CompTree -> Regex -> IO ()
listStmts g regex =
  T.putStrLn $
  T.unlines $
  snub $
  map (stmtLabel . vertexStmt . G.root) $
  selectVertices (\v -> matchLabel v && isRelevantToUser g v) g
  where
    matchLabel RootVertex = False
    matchLabel v          = match regex (unpack $ stmtLabel $ vertexStmt v)
    snub = map head . List.group . sort

-- Restricted to statements for lambda functions or top level constants.
-- Discards nested constant bindings
isRelevantToUser :: Graph Vertex arc -> Vertex -> Bool
isRelevantToUser _ Vertex {vertexStmt = CompStmt {stmtDetails = StmtLam {}}} =
    True
isRelevantToUser g v@Vertex {vertexStmt = CompStmt {stmtDetails = StmtCon {}}} =
    RootVertex `elem` preds g v
isRelevantToUser _ RootVertex = False

-- | Returns the vertices satisfying the predicate. Doesn't alter the graph.
selectVertices :: (Vertex->Bool) -> CompTree -> [CompTree]
selectVertices pred g = [ g{G.root = v} | v <- vertices g, pred v]

matchRegex :: Regex -> Vertex -> Bool
matchRegex regex v = match regex $ noNewlines (vertexRes v)

subGraphFromRoot :: Ord v => Graph v a -> Graph v a
subGraphFromRoot g = subGraphFrom (G.root g) g

subGraphFrom :: Ord v => v -> Graph v a -> Graph v a
subGraphFrom v g = Graph {root = v, vertices = filteredV, arcs = filteredA}
  where
    filteredV = getPreorder $ getDfs g {G.root = v}
    filteredSet = Set.fromList filteredV
    filteredA =
      [ a
      | a <- arcs g
      , Set.member (source a) filteredSet && Set.member (target a) filteredSet
      ]

--------------------------------------------------------------------------------
-- observe


printStmts :: CompTree -> String -> IO ()
printStmts g regexp
    | null vs_filtered  =
      putStrLn $ "There are no computation statements matching \"" ++ regexp ++ "\"."
    | otherwise = forM_ (zip [0..] $ nubOrd $ map printStmt vs_filtered) $ \(n,s) -> do
    putStrLn $ "--- stmt-" ++ show n ++ " ------------------------------------------"
    putStrLn s
  where
  vs_filtered =
    map subGraphFromRoot .
    sortOn (vertexRes . G.root) .
    selectVertices (\v -> matchRegex r v && isRelevantToUser g v) $
    g
  r = makeRegex regexp
  nubOrd = nub -- We want nubOrd from the extra package

printStmt :: CompTree -> String
printStmt g = unlines $
    show(vertexStmt $ G.root g) :
    concat
      [ "  where" :
        map (("    " ++) . unpack) locals
      | not (null locals)]
  where
    locals =
          -- constants
          [ stmtRes c
          | Vertex {vertexStmt = c@CompStmt {stmtDetails = StmtCon{}}} <-
              succs g (G.root g)
          ] ++
          -- function calls
          [ stmtRes c
          | Vertex {vertexStmt = c@CompStmt {stmtDetails = StmtLam{}}} <-
              succs g (G.root g)
          ]

--------------------------------------------------------------------------
-- graph
graphStmts :: String -> CompTree -> IO ()
graphStmts "" g = renderAndOpen g
graphStmts (makeRegex -> r) g = do
          let matches =
                map subGraphFromRoot $
                selectVertices (\v -> matchRegex r v && isRelevantToUser g v) g
          case matches of
            [one] -> renderAndOpen one
            _ ->
              putStrLn "More than one match, please select only one expression."

renderAndOpen g = do
  tempDir <- getTemporaryDirectory
  (tempFile, hTempFile) <- openTempFile tempDir "hoed.svg"
  hClose hTempFile
  cmd "dot" ["-Tsvg", "-o", tempFile] (showGraph g)
  _success <- openBrowser ("file:///" ++ tempFile)
  return ()

showGraph g = showWith g showVertex showArc
  where
    showVertex RootVertex = ("\".\"", "shape=none")
    showVertex v          = ("\"" ++ (escape . showCompStmt) v ++ "\"", "")
    showArc _ = ""
    showCompStmt = show . vertexStmt

cmd line args inp = do
  putStrLn $ unwords (line:args)
  (exit, stdout, stderr) <- readProcessWithExitCode line args inp
  unless (exit == ExitSuccess) $ do
    putStrLn $ "Failed with code: " ++ show exit
    putStrLn stdout
    putStrLn stderr
  return exit

--------------------------------------------------------------------------------
-- algorithmic debugging

adbCommands :: [Command State]
adbCommands = [judgeCommand Right, judgeCommand Wrong]

judgeCommand :: Judgement -> Command State
judgeCommand judgement =
  Command
    verbatim
    []
    ("Judge computation statements" </>
     text verbatim </>
     " according to the intended behaviour/specification of the function.") $ \case
    [] -> Just $ \st -> adb_judge judgement st
    _  -> Nothing
  where
    verbatim | Right <- judgement = "right"
             | Wrong <- judgement = "wrong"

adbFrame :: State -> IO (Transition State)
adbFrame st@State{..} =
  case cv of
    RootVertex -> do
      putStrLn "Out of vertexes"
      return $ Up Nothing
    _ -> do
      adb_stats compTree
      print $ vertexStmt cv
      case lookupPropositions ps cv of
        Nothing   -> interactive st
        Just prop -> do
          judgement <- judge trace prop cv unjudgedCharacterCount compTree
          case judgement of
            (Judge Right)                    -> adb_judge Right st
            (Judge Wrong)                    -> adb_judge Wrong st
            (Judge (Assisted msgs))          -> do
              mapM_ (putStrLn . toString) msgs
              interactive st
            (AlternativeTree newCompTree newTrace) -> do
              putStrLn "Discovered simpler tree!"
              let cv' = next RootVertex newCompTree
              return $ Next $ State cv' newTrace newCompTree ps
  where
    interactive = interactiveFrame "?" adbCommands
    toString (InconclusiveProperty s) = "inconclusive property: " ++ s
    toString (PassingProperty s)      = "passing property: "      ++ s

adb_stats :: CompTree -> IO ()
adb_stats compTree = putStrLn
  $  "======================================================================= ["
  ++ show (length vs_w) ++ "-" ++ show (length vs_r) ++ "/" ++ show (length vs) ++ "]"
  where
  vs   = filter (not . isRootVertex) (vertices compTree)
  vs_r = filter isRight vs
  vs_w = filter isWrong vs

adb_judge :: Judgement -> State -> IO (Transition State)
adb_judge jmt State{..} = case faultyVertices compTree' of
  (v:_) -> do adb_stats compTree'
              putStrLn $ "Fault located! In:\n" ++ vertexRes v
              return $ Up $ Just $ State cv trace compTree' ps
  []    -> return $ Next $ State cv_next trace compTree' ps
  where
  cv_next     = next cv' compTree'
  compTree'   = mapGraph replaceCV compTree
  replaceCV v = if vertexUID v === vertexUID cv' then cv' else v
  cv'         = setJudgement cv jmt

faultyVertices :: CompTree -> [Vertex]
faultyVertices = findFaulty_dag getJudgement

next :: Vertex -> CompTree -> Vertex
next v ct = case getJudgement v of
  Right -> up
  Wrong -> down
  _     -> v
  where
  (up:_)   = preds ct v
  (down:_) = filter unjudged (succs ct v)

unjudged :: Vertex -> Bool
unjudged = unjudged' . getJudgement
  where
  unjudged' Right = False
  unjudged' Wrong = False
  unjudged' _     = True