{-# 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 = forall k a. Map k a
M.empty
, dsNodeIdSupply :: [Text]
dsNodeIdSupply = forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
L.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'm'forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [Integer
0..]
, dsGraph :: DotGraph
dsGraph = Map Text Text -> Set (Text, Text) -> DotGraph
DotGraph forall a. Monoid a => a
mempty 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{} = forall n. DotState n -> DotGraph
dsGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState forall n. DotState n
initialDotState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall n. Env n -> n -> Text
deLabel forall r (m :: * -> *). MonadReader r m => m r
ask forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
getConnections :: n -> DotM n [n]
getConnections :: forall n. n -> DotM n [n]
getConnections = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall n. Env n -> n -> [n]
deConnections forall r (m :: * -> *). MonadReader r m => m r
ask forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) <- forall s (m :: * -> *). MonadState s m => m s
get
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup n
name Map n Text
nodeIds of
Just Text
nodeId -> 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 <- forall n. n -> DotM n Text
getLabel n
name
forall s (m :: * -> *). MonadState s m => s -> m ()
put DotState n
s
{ dsNodeIds :: Map n Text
dsNodeIds = 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 = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Text
newNodeId Text
label forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Map Text Text
dgNodeLabels forall a b. (a -> b) -> a -> b
$ DotGraph
graph
}
}
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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \DotState n
s -> DotState n
s
{ dsGraph :: DotGraph
dsGraph = (forall n. DotState n -> DotGraph
dsGraph DotState n
s)
{ dgEdges :: Set (Text, Text)
dgEdges = forall a. Ord a => a -> Set a -> Set a
S.insert (Text
m1, Text
m2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. DotGraph -> Set (Text, Text)
dgEdges forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. DotState n -> DotGraph
dsGraph 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 = forall n x. Env n -> DotM n x -> DotGraph
runDotM Env n
env (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) <- forall n. Ord n => n -> DotM n (Text, Bool)
addEntity n
entity
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
continue forall a b. (a -> b) -> a -> b
$ do
[n]
connectedEntities <- forall n. n -> DotM n [n]
getConnections n
entity
[Text]
connectedNodeIds <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall n. Ord n => n -> DotM n Text
dottify' [n]
connectedEntities
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall n. Text -> Text -> DotM n ()
addConnection Text
nodeId) [Text]
connectedNodeIds
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 forall a b. (a -> b) -> a -> b
$ 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) <- 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) <- 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 = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> ByteString -> IO ()
BS.writeFile String
fp forall a b. (a -> b) -> a -> b
$ Text -> ByteString
E.encodeUtf8 forall a b. (a -> b) -> a -> b
$ DotGraph -> Text
renderDot DotGraph
dot