{-# language OverloadedStrings #-}

module OBDD.Display where

import OBDD.Data (OBDD, foldM)
import Control.Monad (void)
import Control.Monad.RWS (RWS, evalRWS, tell, get, put)
import Data.Text (Text)
import qualified Data.Text as T
import Data.Monoid
import System.Process.Text

-- | Calls the @dot@ executable (must be in @$PATH@)
-- to draw a diagram in an X11 window.
-- Will block until this window is closed.
-- Window can be closed gracefully
-- by typing  'q'  when it has focus.
display :: (Ord v, Show v) => OBDD v -> IO ()
display :: forall v. (Ord v, Show v) => OBDD v -> IO ()
display OBDD v
d = IO (ExitCode, Text, Text) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
  (IO (ExitCode, Text, Text) -> IO ())
-> IO (ExitCode, Text, Text) -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> Text -> IO (ExitCode, Text, Text)
readProcessWithExitCode FilePath
"dot" [ FilePath
"-Tx11" ]
  (Text -> IO (ExitCode, Text, Text))
-> Text -> IO (ExitCode, Text, Text)
forall a b. (a -> b) -> a -> b
$ Bool -> OBDD v -> Text
forall v. (Ord v, Show v) => Bool -> OBDD v -> Text
toDot Bool
False OBDD v
d

-- | same as @display@, but does not show the @False@ node
-- and the edges pointing to @False@.
display' :: (Ord v, Show v) => OBDD v -> IO ()
display' :: forall v. (Ord v, Show v) => OBDD v -> IO ()
display' OBDD v
d = IO (ExitCode, Text, Text) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
  (IO (ExitCode, Text, Text) -> IO ())
-> IO (ExitCode, Text, Text) -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> Text -> IO (ExitCode, Text, Text)
readProcessWithExitCode FilePath
"dot" [ FilePath
"-Tx11" ]
  (Text -> IO (ExitCode, Text, Text))
-> Text -> IO (ExitCode, Text, Text)
forall a b. (a -> b) -> a -> b
$ Bool -> OBDD v -> Text
forall v. (Ord v, Show v) => Bool -> OBDD v -> Text
toDot Bool
True OBDD v
d

-- | a textual representation of the BDD that is suitable
-- as input to the "dot" program from the graphviz suite.
toDot :: (Ord v, Show v)
  => Bool -- ^ suppress pointers to False
  -> OBDD v -> Text
toDot :: forall v. (Ord v, Show v) => Bool -> OBDD v -> Text
toDot Bool
suppress_false =
    ((), Text) -> Text
forall a b. (a, b) -> b
snd
  (((), Text) -> Text) -> (OBDD v -> ((), Text)) -> OBDD v -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ( \ RWST () Text Int Identity (Maybe Int)
m -> RWS () Text Int () -> () -> Int -> ((), Text)
forall r w s a. RWS r w s a -> r -> s -> (a, w)
evalRWS (do Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell Text
"digraph BDD {"; RWST () Text Int Identity (Maybe Int)
m; Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell Text
"}" ) () Int
0 )
  (RWST () Text Int Identity (Maybe Int) -> ((), Text))
-> (OBDD v -> RWST () Text Int Identity (Maybe Int))
-> OBDD v
-> ((), Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> RWST () Text Int Identity (Maybe Int))
-> (v
    -> Maybe Int -> Maybe Int -> RWST () Text Int Identity (Maybe Int))
-> OBDD v
-> RWST () Text Int Identity (Maybe Int)
forall (m :: * -> *) v a.
(Monad m, Ord v) =>
(Bool -> m a) -> (v -> a -> a -> m a) -> OBDD v -> m a
foldM
  ( \ Bool
b -> if Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& Bool
suppress_false then Maybe Int -> RWST () Text Int Identity (Maybe Int)
forall a. a -> RWST () Text Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing else do
     Int
this <- RWS () Text Int Int
forall b a. Monoid b => RWS a b Int Int
fresh
     Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Text -> RWS () Text Int ()) -> Text -> RWS () Text Int ()
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
T.unlines
       [ Text
"node[shape=rectangle];"
       , Int -> Text
forall {a}. Show a => a -> Text
text Int
this Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
mkLabel (Bool -> Text
forall {a}. Show a => a -> Text
text Bool
b)
       , Text
"node[shape=oval];"
       ]
     Maybe Int -> RWST () Text Int Identity (Maybe Int)
forall a. a -> RWST () Text Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> RWST () Text Int Identity (Maybe Int))
-> Maybe Int -> RWST () Text Int Identity (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
this
  )
  ( \ v
v Maybe Int
ml Maybe Int
mr -> do
     Int
this <- RWS () Text Int Int
forall b a. Monoid b => RWS a b Int Int
fresh
     Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Text -> RWS () Text Int ()) -> Text -> RWS () Text Int ()
forall a b. (a -> b) -> a -> b
$ Int -> Text
forall {a}. Show a => a -> Text
text Int
this Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
mkLabel (v -> Text
forall {a}. Show a => a -> Text
text v
v)
     case Maybe Int
ml of
       Just Int
l -> Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Text -> RWS () Text Int ()) -> Text -> RWS () Text Int ()
forall a b. (a -> b) -> a -> b
$ Int -> Text
forall {a}. Show a => a -> Text
text Int
this Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"->" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall {a}. Show a => a -> Text
text Int
l Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
mkLabel Text
"0"
       Maybe Int
Nothing -> () -> RWS () Text Int ()
forall a. a -> RWST () Text Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     case Maybe Int
mr of
       Just Int
r -> Text -> RWS () Text Int ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Text -> RWS () Text Int ()) -> Text -> RWS () Text Int ()
forall a b. (a -> b) -> a -> b
$ Int -> Text
forall {a}. Show a => a -> Text
text Int
this Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"->" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall {a}. Show a => a -> Text
text Int
r Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
mkLabel Text
"1"
       Maybe Int
Nothing -> () -> RWS () Text Int ()
forall a. a -> RWST () Text Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Maybe Int -> RWST () Text Int Identity (Maybe Int)
forall a. a -> RWST () Text Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> RWST () Text Int Identity (Maybe Int))
-> Maybe Int -> RWST () Text Int Identity (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
this
  )

fresh :: Monoid b => RWS a b Int Int
fresh :: forall b a. Monoid b => RWS a b Int Int
fresh = do Int
this <- RWS a b Int Int
forall s (m :: * -> *). MonadState s m => m s
get ; Int -> RWST a b Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> RWST a b Int Identity ())
-> Int -> RWST a b Int Identity ()
forall a b. (a -> b) -> a -> b
$! Int -> Int
forall a. Enum a => a -> a
succ Int
this ; Int -> RWS a b Int Int
forall a. a -> RWST a b Int Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
this

mkLabel :: Text -> Text
mkLabel Text
lbl = Text
"[label=\"" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
unquote Text
lbl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\"];"

unquote :: Text -> Text
unquote Text
s =
  if Text -> Text -> Bool
T.isPrefixOf Text
"\"" Text
s Bool -> Bool -> Bool
&& Text -> Text -> Bool
T.isSuffixOf Text
"\"" Text
s
  then HasCallStack => Text -> Text
Text -> Text
T.init (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ HasCallStack => Text -> Text
Text -> Text
T.tail Text
s
  else Text
s

text :: a -> Text
text a
x = FilePath -> Text
T.pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ a -> FilePath
forall a. Show a => a -> FilePath
show a
x