{-# LANGUAGE GADTs #-}
module Agda.Interaction.Highlighting.Dot.Base
( dottify
, renderDotToFile
, renderDot
, DotGraph (..)
, Env(..)
) where
import Control.Monad (liftM2, when)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader (ReaderT, runReaderT, ask)
import Control.Monad.State (State, execState, get, modify, put)
import qualified Data.Map as M
import Data.Map(Map)
import qualified Data.Set as S
import Data.Set (Set)
import qualified Data.Text.Lazy as L
import qualified Data.Text.Lazy.Encoding as E
import qualified Data.ByteString.Lazy as BS
type NodeId = L.Text
data DotGraph = DotGraph
{ DotGraph -> Map Text Text
dgNodeLabels :: Map NodeId L.Text
, DotGraph -> Set (Text, Text)
dgEdges :: Set (NodeId, NodeId)
}
data Env n where
Env :: Ord n =>
{ forall n. Env n -> n -> [n]
deConnections :: n -> [n]
, forall n. Env n -> n -> Text
deLabel :: n -> L.Text
} -> Env n
data DotState n = DotState
{ forall n. DotState n -> Map n Text
dsNodeIds :: Map n NodeId
, forall n. DotState n -> [Text]
dsNodeIdSupply :: [NodeId]
, forall n. DotState n -> DotGraph
dsGraph :: DotGraph
}
initialDotState :: DotState n
initialDotState :: forall n. DotState n
initialDotState = DotState
{ dsNodeIds :: Map n Text
dsNodeIds = Map n Text
forall k a. Map k a
M.empty
, dsNodeIdSupply :: [Text]
dsNodeIdSupply = (Integer -> Text) -> [Integer] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
L.pack (String -> Text) -> (Integer -> String) -> Integer -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'm'Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Integer -> String) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show) [Integer
0..]
, dsGraph :: DotGraph
dsGraph = Map Text Text -> Set (Text, Text) -> DotGraph
DotGraph Map Text Text
forall a. Monoid a => a
mempty Set (Text, Text)
forall a. Monoid a => a
mempty
}
type DotM n a = ReaderT (Env n) (State (DotState n)) a
runDotM :: Env n -> DotM n x -> DotGraph
runDotM :: forall n x. Env n -> DotM n x -> DotGraph
runDotM env :: Env n
env@Env{} = DotState n -> DotGraph
forall n. DotState n -> DotGraph
dsGraph (DotState n -> DotGraph)
-> (DotM n x -> DotState n) -> DotM n x -> DotGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State (DotState n) x -> DotState n -> DotState n)
-> DotState n -> State (DotState n) x -> DotState n
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (DotState n) x -> DotState n -> DotState n
forall s a. State s a -> s -> s
execState DotState n
forall n. DotState n
initialDotState (State (DotState n) x -> DotState n)
-> (DotM n x -> State (DotState n) x) -> DotM n x -> DotState n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DotM n x -> Env n -> State (DotState n) x)
-> Env n -> DotM n x -> State (DotState n) x
forall a b c. (a -> b -> c) -> b -> a -> c
flip DotM n x -> Env n -> State (DotState n) x
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Env n
env
getLabel :: n -> DotM n L.Text
getLabel :: forall n. n -> DotM n Text
getLabel = (Env n -> n -> Text)
-> ReaderT (Env n) (State (DotState n)) (Env n)
-> ReaderT (Env n) (State (DotState n)) n
-> ReaderT (Env n) (State (DotState n)) Text
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Env n -> n -> Text
forall n. Env n -> n -> Text
deLabel ReaderT (Env n) (State (DotState n)) (Env n)
forall r (m :: * -> *). MonadReader r m => m r
ask (ReaderT (Env n) (State (DotState n)) n
-> ReaderT (Env n) (State (DotState n)) Text)
-> (n -> ReaderT (Env n) (State (DotState n)) n)
-> n
-> ReaderT (Env n) (State (DotState n)) Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> ReaderT (Env n) (State (DotState n)) n
forall (f :: * -> *) a. Applicative f => a -> f a
pure
getConnections :: n -> DotM n [n]
getConnections :: forall n. n -> DotM n [n]
getConnections = (Env n -> n -> [n])
-> ReaderT (Env n) (State (DotState n)) (Env n)
-> ReaderT (Env n) (State (DotState n)) n
-> ReaderT (Env n) (State (DotState n)) [n]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Env n -> n -> [n]
forall n. Env n -> n -> [n]
deConnections ReaderT (Env n) (State (DotState n)) (Env n)
forall r (m :: * -> *). MonadReader r m => m r
ask (ReaderT (Env n) (State (DotState n)) n
-> ReaderT (Env n) (State (DotState n)) [n])
-> (n -> ReaderT (Env n) (State (DotState n)) n)
-> n
-> ReaderT (Env n) (State (DotState n)) [n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> ReaderT (Env n) (State (DotState n)) n
forall (f :: * -> *) a. Applicative f => a -> f a
pure
addEntity :: Ord n => n -> DotM n (NodeId, Bool)
addEntity :: forall n. Ord n => n -> DotM n (Text, Bool)
addEntity n
name = do
s :: DotState n
s@(DotState Map n Text
nodeIds [Text]
nodeIdSupply DotGraph
graph) <- ReaderT (Env n) (State (DotState n)) (DotState n)
forall s (m :: * -> *). MonadState s m => m s
get
case n -> Map n Text -> Maybe Text
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup n
name Map n Text
nodeIds of
Just Text
nodeId -> (Text, Bool) -> DotM n (Text, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
nodeId, Bool
False)
Maybe Text
Nothing -> do
let Text
newNodeId:[Text]
remainingNodeIdSupply = [Text]
nodeIdSupply
Text
label <- n -> DotM n Text
forall n. n -> DotM n Text
getLabel n
name
DotState n -> ReaderT (Env n) (State (DotState n)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put DotState n
s
{ dsNodeIds :: Map n Text
dsNodeIds = n -> Text -> Map n Text -> Map n Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert n
name Text
newNodeId Map n Text
nodeIds
, dsNodeIdSupply :: [Text]
dsNodeIdSupply = [Text]
remainingNodeIdSupply
, dsGraph :: DotGraph
dsGraph = DotGraph
graph
{ dgNodeLabels :: Map Text Text
dgNodeLabels = Text -> Text -> Map Text Text -> Map Text Text
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Text
newNodeId Text
label (Map Text Text -> Map Text Text)
-> (DotGraph -> Map Text Text) -> DotGraph -> Map Text Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Map Text Text
dgNodeLabels (DotGraph -> Map Text Text) -> DotGraph -> Map Text Text
forall a b. (a -> b) -> a -> b
$ DotGraph
graph
}
}
(Text, Bool) -> DotM n (Text, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
newNodeId, Bool
True)
addConnection :: NodeId -> NodeId -> DotM n ()
addConnection :: forall n. Text -> Text -> DotM n ()
addConnection Text
m1 Text
m2 = (DotState n -> DotState n)
-> ReaderT (Env n) (State (DotState n)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DotState n -> DotState n)
-> ReaderT (Env n) (State (DotState n)) ())
-> (DotState n -> DotState n)
-> ReaderT (Env n) (State (DotState n)) ()
forall a b. (a -> b) -> a -> b
$ \DotState n
s -> DotState n
s
{ dsGraph :: DotGraph
dsGraph = (DotState n -> DotGraph
forall n. DotState n -> DotGraph
dsGraph DotState n
s)
{ dgEdges :: Set (Text, Text)
dgEdges = (Text, Text) -> Set (Text, Text) -> Set (Text, Text)
forall a. Ord a => a -> Set a -> Set a
S.insert (Text
m1, Text
m2) (Set (Text, Text) -> Set (Text, Text))
-> (DotState n -> Set (Text, Text))
-> DotState n
-> Set (Text, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Set (Text, Text)
dgEdges (DotGraph -> Set (Text, Text))
-> (DotState n -> DotGraph) -> DotState n -> Set (Text, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotState n -> DotGraph
forall n. DotState n -> DotGraph
dsGraph (DotState n -> Set (Text, Text)) -> DotState n -> Set (Text, Text)
forall a b. (a -> b) -> a -> b
$ DotState n
s
}
}
dottify :: Ord n => Env n -> n -> DotGraph
dottify :: forall n. Ord n => Env n -> n -> DotGraph
dottify Env n
env n
root = Env n -> DotM n Text -> DotGraph
forall n x. Env n -> DotM n x -> DotGraph
runDotM Env n
env (n -> DotM n Text
forall n. Ord n => n -> DotM n Text
dottify' n
root)
dottify' :: Ord n => n -> DotM n NodeId
dottify' :: forall n. Ord n => n -> DotM n Text
dottify' n
entity = do
(Text
nodeId, Bool
continue) <- n -> DotM n (Text, Bool)
forall n. Ord n => n -> DotM n (Text, Bool)
addEntity n
entity
Bool
-> ReaderT (Env n) (State (DotState n)) ()
-> ReaderT (Env n) (State (DotState n)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
continue (ReaderT (Env n) (State (DotState n)) ()
-> ReaderT (Env n) (State (DotState n)) ())
-> ReaderT (Env n) (State (DotState n)) ()
-> ReaderT (Env n) (State (DotState n)) ()
forall a b. (a -> b) -> a -> b
$ do
[n]
connectedEntities <- n -> DotM n [n]
forall n. n -> DotM n [n]
getConnections n
entity
[Text]
connectedNodeIds <- (n -> DotM n Text)
-> [n] -> ReaderT (Env n) (State (DotState n)) [Text]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM n -> DotM n Text
forall n. Ord n => n -> DotM n Text
dottify' [n]
connectedEntities
(Text -> ReaderT (Env n) (State (DotState n)) ())
-> [Text] -> ReaderT (Env n) (State (DotState n)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Text -> Text -> ReaderT (Env n) (State (DotState n)) ()
forall n. Text -> Text -> DotM n ()
addConnection Text
nodeId) [Text]
connectedNodeIds
Text -> DotM n Text
forall (m :: * -> *) a. Monad m => a -> m a
return Text
nodeId
renderDot :: DotGraph -> L.Text
renderDot :: DotGraph -> Text
renderDot DotGraph
g = [Text] -> Text
L.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [ Text
"digraph dependencies {" ]
, [ [Text] -> Text
L.concat [Text
" ", Text
nodeId, Text
"[label=\"", Text
label, Text
"\"];"]
| (Text
nodeId, Text
label) <- Map Text Text -> [(Text, Text)]
forall k a. Map k a -> [(k, a)]
M.toList (DotGraph -> Map Text Text
dgNodeLabels DotGraph
g) ]
, [ [Text] -> Text
L.concat [Text
" ", Text
r1, Text
" -> ", Text
r2, Text
";"]
| (Text
r1 , Text
r2) <- Set (Text, Text) -> [(Text, Text)]
forall a. Set a -> [a]
S.toList (DotGraph -> Set (Text, Text)
dgEdges DotGraph
g) ]
, [Text
"}"]
]
renderDotToFile :: MonadIO m => DotGraph -> FilePath -> m ()
renderDotToFile :: forall (m :: * -> *). MonadIO m => DotGraph -> String -> m ()
renderDotToFile DotGraph
dot String
fp = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
BS.writeFile String
fp (ByteString -> IO ()) -> ByteString -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> ByteString
E.encodeUtf8 (Text -> ByteString) -> Text -> ByteString
forall a b. (a -> b) -> a -> b
$ DotGraph -> Text
renderDot DotGraph
dot