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

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

import Data.Maybe (fromJust)
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 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 forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"digraph g { Bot [label=\"0\",shape=\"box\"]; }"
  | Bdd
myb forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"digraph g { Top [label=\"1\",shape=\"box\"]; }"
  | Bool
otherwise = String
"strict digraph g {\n" forall a. [a] -> [a] -> [a]
++ String
links forall a. [a] -> [a] -> [a]
++ String
sinks forall a. [a] -> [a] -> [a]
++ String
rankings 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Bdd
top,Bdd
bot] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Bdd, Int)]
done then (String
"",[(Bdd, Int)]
done) else
            let
              thisn :: Int
thisn = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bdd, Int)]
done then Int
0 else forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bdd, Int)]
done) forall a. Num a => a -> a -> a
+ Int
1
              thisnstr :: String
thisnstr = forall a. Show a => a -> String
show Int
thisn
              thisvar :: Int
thisvar = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ Bdd -> Maybe Int
firstVarOf Bdd
curB
              out1 :: String
out1  = String
"n" forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++ String
" [label=\"" forall a. [a] -> [a] -> [a]
++ Int -> String
myShow Int
thisvar 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)forall a. a -> [a] -> [a]
:[(Bdd, Int)]
done) Bdd
lhs
              leftn :: Int
leftn = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Bdd
lhs [(Bdd, Int)]
lhsdone
              out2 :: String
out2
                | Bdd
lhs forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> Top;\n"
                | Bdd
lhs forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> Bot;\n"
                | Bool
otherwise  = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
leftn forall a. [a] -> [a] -> [a]
++String
";\n" forall a. [a] -> [a] -> [a]
++ String
lhsoutput
              (String
rhsoutput,[(Bdd, Int)]
rhsdone) = [(Bdd, Int)] -> Bdd -> (String, [(Bdd, Int)])
genGraphStep [(Bdd, Int)]
lhsdone Bdd
rhs
              rightn :: Int
rightn = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Bdd
rhs [(Bdd, Int)]
rhsdone
              out3 :: String
out3
                | Bdd
rhs forall a. Eq a => a -> a -> Bool
== Bdd
top = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> Top [style=dashed];\n"
                | Bdd
rhs forall a. Eq a => a -> a -> Bool
== Bdd
bot = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> Bot [style=dashed];\n"
                | Bool
otherwise  = String
"n"forall a. [a] -> [a] -> [a]
++ String
thisnstr forall a. [a] -> [a] -> [a]
++String
" -> n"forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
rightn forall a. [a] -> [a] -> [a]
++String
" [style=dashed];\n" forall a. [a] -> [a] -> [a]
++ String
rhsoutput
            in (String
out1 forall a. [a] -> [a] -> [a]
++ String
out2 forall a. [a] -> [a] -> [a]
++ String
out3, [(Bdd, Int)]
rhsdone)
      sinks :: String
sinks = String
"Bot [label=\"0\",shape=\"box\"];\n" forall a. [a] -> [a] -> [a]
++ String
"Top [label=\"1\",shape=\"box\"];\n"
      rankings :: String
rankings = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"{ rank=same; "forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (Int -> [String]
nodesOf Int
v) forall a. [a] -> [a] -> [a]
++ String
" }\n" | Int
v <- Bdd -> [Int]
allVarsOf Bdd
myb ]
      nodesOf :: Int -> [String]
nodesOf Int
v = forall a b. (a -> b) -> [a] -> [b]
map ((String
"n"forall a. [a] -> [a] -> [a]
++)forall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a. Show a => a -> String
showforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter ( \(Bdd
b,Int
_) -> Bdd -> Maybe Int
firstVarOf Bdd
b forall a. Eq a => a -> a -> Bool
== 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"] forall a. Maybe a
Nothing 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
  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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([String] -> String
unlinesforall b c a. (b -> c) -> (a -> b) -> a -> c
.forall a. [a] -> [a]
tailforall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> [String]
lines) String
out
    ExitFailure Int
n -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"dot -Tsvg failed with exit code " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" and error: " forall a. [a] -> [a] -> [a]
++ String
err