-- | Very simple visualisation of BDDs using /dot/.

module Data.HasCacBDD.Visuals (
  genGraph,
  genGraphWith,
  showGraph,
  svgGraph
) where

import System.Exit
import System.IO
import System.Process

import Data.HasCacBDD

-- | Generate a string which describes the BDD in the dot language.
genGraph :: Bdd -> String
genGraph :: Bdd -> String
genGraph = (Int -> String) -> Bdd -> String
genGraphWith Int -> String
forall a. Show a => a -> String
show

-- | Given a function to show variables, generate a string which describes the BDD in the dot language.
genGraphWith :: (Int -> String) -> Bdd -> String
genGraphWith :: (Int -> String) -> Bdd -> String
genGraphWith Int -> String
myShow Bdd
myb
  | Bdd
myb Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"digraph g { Bot [label=\"0\",shape=\"box\"]; }"
  | Bdd
myb Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"digraph g { Top [label=\"1\",shape=\"box\"]; }"
  | Bool
otherwise = String
"strict digraph g {\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
links String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sinks String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rankings String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}" where
      (String
links,[(Bdd, Int)]
topdone) = [(Bdd, Int)] -> Bdd -> (String, [(Bdd, Int)])
genGraphStep [] Bdd
myb
      genGraphStep :: [(Bdd,Int)] -> Bdd -> (String,[(Bdd,Int)])
      genGraphStep :: [(Bdd, Int)] -> Bdd -> (String, [(Bdd, Int)])
genGraphStep [(Bdd, Int)]
done Bdd
curB =
        if Bdd
curB Bdd -> [Bdd] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Bdd
top,Bdd
bot] [Bdd] -> [Bdd] -> [Bdd]
forall a. [a] -> [a] -> [a]
++ ((Bdd, Int) -> Bdd) -> [(Bdd, Int)] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map (Bdd, Int) -> Bdd
forall a b. (a, b) -> a
fst [(Bdd, Int)]
done then (String
"",[(Bdd, Int)]
done) else
            let
              thisn :: Int
thisn = if [(Bdd, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bdd, Int)]
done then Int
0 else [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (((Bdd, Int) -> Int) -> [(Bdd, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Bdd, Int) -> Int
forall a b. (a, b) -> b
snd [(Bdd, Int)]
done) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
              thisnstr :: String
thisnstr = Int -> String
forall a. Show a => a -> String
show Int
thisn
              (Just Int
thisvar) = Bdd -> Maybe Int
firstVarOf Bdd
curB
              out1 :: String
out1  = String
"n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" [label=\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
myShow Int
thisvar String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\",shape=\"circle\"];\n"
              (Bdd
lhs, Bdd
rhs) = (Bdd -> Bdd
thenOf Bdd
curB, Bdd -> Bdd
elseOf Bdd
curB)
              (String
lhsoutput,[(Bdd, Int)]
lhsdone) = [(Bdd, Int)] -> Bdd -> (String, [(Bdd, Int)])
genGraphStep ((Bdd
curB,Int
thisn)(Bdd, Int) -> [(Bdd, Int)] -> [(Bdd, Int)]
forall a. a -> [a] -> [a]
:[(Bdd, Int)]
done) Bdd
lhs
              (Just Int
leftn) = Bdd -> [(Bdd, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Bdd
lhs [(Bdd, Int)]
lhsdone
              out2 :: String
out2
                | Bdd
lhs Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> Top;\n"
                | Bdd
lhs Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> Bot;\n"
                | Bool
otherwise  = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
leftn String -> String -> String
forall a. [a] -> [a] -> [a]
++String
";\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lhsoutput
              (String
rhsoutput,[(Bdd, Int)]
rhsdone) = [(Bdd, Int)] -> Bdd -> (String, [(Bdd, Int)])
genGraphStep [(Bdd, Int)]
lhsdone Bdd
rhs
              (Just Int
rightn) = Bdd -> [(Bdd, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Bdd
rhs [(Bdd, Int)]
rhsdone
              out3 :: String
out3
                | Bdd
rhs Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> Top [style=dashed];\n"
                | Bdd
rhs Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> Bot [style=dashed];\n"
                | Bool
otherwise  = String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thisnstr String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" -> n"String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
rightn String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" [style=dashed];\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rhsoutput
            in (String
out1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
out2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
out3, [(Bdd, Int)]
rhsdone)
      sinks :: String
sinks = String
"Bot [label=\"0\",shape=\"box\"];\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Top [label=\"1\",shape=\"box\"];\n"
      rankings :: String
rankings = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"{ rank=same; "String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (Int -> [String]
nodesOf Int
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }\n" | Int
v <- Bdd -> [Int]
allVarsOf Bdd
myb ]
      nodesOf :: Int -> [String]
nodesOf Int
v = ((Bdd, Int) -> String) -> [(Bdd, Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"n"String -> String -> String
forall a. [a] -> [a] -> [a]
++)(String -> String)
-> ((Bdd, Int) -> String) -> (Bdd, Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Int -> String
forall a. Show a => a -> String
show(Int -> String) -> ((Bdd, Int) -> Int) -> (Bdd, Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Bdd, Int) -> Int
forall a b. (a, b) -> b
snd) ([(Bdd, Int)] -> [String]) -> [(Bdd, Int)] -> [String]
forall a b. (a -> b) -> a -> b
$ ((Bdd, Int) -> Bool) -> [(Bdd, Int)] -> [(Bdd, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \(Bdd
b,Int
_) -> Bdd -> Maybe Int
firstVarOf Bdd
b Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
v ) [(Bdd, Int)]
topdone

-- | Display the graph of a BDD with dot.
showGraph :: Bdd -> IO ()
showGraph :: Bdd -> IO ()
showGraph Bdd
b = do
  (Handle
inp,Handle
_,Handle
_,ProcessHandle
pid) <- String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess String
"/usr/bin/dot" [String
"-Tx11"] Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing
  Handle -> String -> IO ()
hPutStr Handle
inp (Bdd -> String
genGraph Bdd
b)
  Handle -> IO ()
hFlush Handle
inp
  Handle -> IO ()
hClose Handle
inp
  ExitCode
_ <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Generate SVG of a BDD with dot.
svgGraph :: Bdd -> IO String
svgGraph :: Bdd -> IO String
svgGraph Bdd
b = do
  (ExitCode
exitCode,String
out,String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
"/usr/bin/dot" [String
"-Tsvg" ] (Bdd -> String
genGraph Bdd
b)
  case ExitCode
exitCode of
    ExitCode
ExitSuccess -> String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ ([String] -> String
unlines([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[String] -> [String]
forall a. [a] -> [a]
tail([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> [String]
lines) String
out
    ExitFailure Int
n -> String -> IO String
forall a. HasCallStack => String -> a
error (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ String
"dot -Tsvg failed with exit code " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err