https://github.com/mit-plv/fiat-crypto
Tip revision: e83501253736d8403093203c195457de3f7574f4 authored by Jason Gross on 13 May 2020, 23:08:06 UTC
Try again to auto-bump crate version
Try again to auto-bump crate version
Tip revision: e835012
DepsToDot.hs
#! /usr/bin/env runhaskell
{-# LANGUAGE UnicodeSyntax, ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}
{- Copied and slightly modified from https://github.com/EvgenyMakarov/math-classes/blob/master/tools/DepsToDot.hs -}
import Data.Graph.Inductive
(reachable, delEdge, mkGraph, nmap, Edge, Gr, DynGraph, UEdge, LEdge, efilter, LNode, labNodes, Graph, delNodes)
import Data.GraphViz
(Attributes, toGraphID, color, toLabel, printDotGraph, nonClusteredParams, graphToDot, fmtNode, setID, X11Color(..))
import Data.GraphViz.Attributes.Complete
(Attribute(URL))
import Data.Text.Lazy (Text, pack, unpack)
import Data.List (nub, elemIndex, isSuffixOf, isPrefixOf)
import Control.Monad (liftM2)
import Data.Maybe
import System.Environment
import System.Exit
import System.IO
import System.Console.GetOpt
import Prelude hiding ((.))
(.) :: Functor f ⇒ (a → b) → (f a → f b)
(.) = fmap
dropBack :: Int → [a] → [a]
dropBack n = reverse . drop n . reverse
uedge :: LEdge a → Edge
uedge (x, y, _) = (x, y)
nfilter :: Graph gr ⇒ (LNode a → Bool) → gr a b → gr a b
nfilter p g = delNodes (map fst $ filter (not . p) $ labNodes g) g
untransitive :: DynGraph gr ⇒ gr a b → gr a b
untransitive g = efilter (not . redundant . uedge) g
where redundant e@(from, to) = to `elem` reachable from (delEdge e g)
read_deps :: String → Gr FilePath ()
read_deps input = mkGraph (zip [0..] nodes) edges
where
content :: [(FilePath, FilePath)]
content = do
(left, _ : right) ← break (==':') . lines input
liftM2 (,) (words left) (words right)
nodes :: [FilePath]
nodes = nub $ map fst content ++ map snd content
edges :: [UEdge]
edges = map (\(from, to) →
(fromJust $ elemIndex from nodes, fromJust $ elemIndex to nodes, ())) content
cut_dotvo :: String → String
cut_dotvo = dropBack 3
-- strip to basename
basename :: String → String
basename name = if "src/" `isPrefixOf` name then drop (length "src/") name
else name
cryptoRenameCoqDoc :: String → String
cryptoRenameCoqDoc p = if "src/" `isPrefixOf` p then "Crypto." ++ drop (length "src/") p
else p
coqDocURL :: String → FilePath → String
coqDocURL base p = base
++ map (\c -> if c == '/' then '.' else c) (cryptoRenameCoqDoc (cut_dotvo p))
++ ".html"
label :: Options → FilePath → Attributes
label opts p' =
[ toLabel (basename $ cut_dotvo p)
, color myColor
-- , LabelFontColor (X11Color color)
] ++ maybe [] (\base -> [URL (pack $ coqDocURL base p)]) (optCoqDocBase opts)
where
p = if take 2 p' == "./" then drop 2 p' else p'
myColor :: X11Color
myColor
| "src/Rewriter" `isPrefixOf` p = Red
| "src/Util" `isPrefixOf` p = Blue
| "src/Arithmetic" `isPrefixOf` p = Orange
| "src/Algebra" `isPrefixOf` p = Magenta
| "src/PushButtonSynthesis" `isPrefixOf` p = Green
| otherwise = Black
makeGraph :: Options -> String -> Text
makeGraph opts = printDotGraph .
setID (toGraphID $ optTitle opts) .
graphToDot (nonClusteredParams {fmtNode = snd}) .
nmap (label opts).
untransitive .
nfilter (isSuffixOf ".vo" . snd) .
read_deps
data Options = Options {
optCoqDocBase :: Maybe String,
optTitle :: String,
optInput :: IO String,
optOutput :: String -> IO ()
}
defaultOptions :: Options
defaultOptions = Options {
optCoqDocBase = Nothing,
optTitle = "",
optInput = getContents,
optOutput = putStr
}
options :: [OptDescr (Options -> IO Options)]
options = [
Option [] ["coqdocbase"] (ReqArg (\arg opt ->
return opt { optCoqDocBase = Just arg }) "URL") "coqdoc base path (include trailing slash)",
Option ['i'] ["input"] (ReqArg (\arg opt ->
return opt { optInput = readFile arg }) "FILE") "input file, stdin if omitted",
Option ['o'] ["output"] (ReqArg (\arg opt ->
return opt { optOutput = writeFile arg }) "FILE") "output file, stdout if omitted",
Option ['t'] ["title"] (ReqArg (\arg opt ->
return opt { optTitle = arg }) "TITLE") "title of the graph page",
Option ['h'] ["help"] (NoArg (\_ ->
usage >> exitSuccess)) "display this help page"]
usage :: IO ()
usage = do
prg <- getProgName
hPutStrLn stderr $ usageInfo ("Usage: " ++ prg ++" [OPTION...]") options
hPutStrLn stderr "Use dot -Tsvg deps.dot -o deps.svg to render the graph"
hPutStrLn stderr $ replicate 30 ' ' ++ "This DepsToDot has Super Coq Powers."
main :: IO ()
main = do
argv <- getArgs
case getOpt Permute options argv of
(actions,_,[]) -> do
opts <- foldl (>>=) (return defaultOptions) actions
input <- optInput opts
optOutput opts $ unpack $ makeGraph opts $ input
(_,_,errors) -> do
hPutStrLn stderr $ concat errors
usage
exitFailure