module Language.Fixpoint.Types.Graphs (
CVertex (..)
, CEdge
, KVGraph
, Comps
, KVComps
, writeGraph
)
where
import GHC.Generics (Generic)
import Data.Hashable
import Text.PrettyPrint.HughesPJ
import Language.Fixpoint.Misc
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Refinements
data CVertex = KVar KVar
| DKVar KVar
| Cstr Integer
deriving (Eq, Ord, Show, Generic)
instance PPrint CVertex where
pprintTidy _ (KVar k) = doubleQuotes $ pprint $ kv k
pprintTidy _ (Cstr i) = text "id_" <> pprint i
pprintTidy _ (DKVar k) = pprint k <> text "*"
instance Hashable CVertex
type CEdge = (CVertex, CVertex)
type KVGraph = [(CVertex, CVertex, [CVertex])]
type Comps a = [[a]]
type KVComps = Comps CVertex
writeGraph :: FilePath -> KVGraph -> IO ()
writeGraph f = writeFile f . render . ppGraph
ppGraph :: KVGraph -> Doc
ppGraph g = ppEdges [ (v, v') | (v,_,vs) <- g, v' <- vs]
ppEdges :: [CEdge] -> Doc
ppEdges = vcat . wrap ["digraph Deps {"] ["}"]
. map ppE
. filter (not . isJunkEdge)
where
ppE (v, v') = pprint v <+> "->" <+> pprint v'
isJunkEdge :: CEdge -> Bool
isJunkEdge (DKVar _, _) = True
isJunkEdge (_, DKVar _) = True
isJunkEdge (Cstr _, Cstr _) = True
isJunkEdge _ = False