
   0 | module Graphics.DOT.Interfaces
   1 | 
   2 | import Graphics.DOT.AST
   3 | 
   4 | import Data.Vect
   5 | import Data.List1
   6 | import Data.String
   7 | 
   8 | %default total
   9 | 
  10 | 
  11 | --------------------------------------------------------------------------------
  12 | -- INTERFACES FOR CONVERTING TO DOT
  13 | --------------------------------------------------------------------------------
  14 | 
  15 | ||| The type `t` can be converted to a `CompassPoint`.
  16 | public export
  17 | interface DOTCompassPoint t where
  18 |   toCompassPoint : t -> CompassPoint
  19 | 
  20 | ||| The type `t` can be converted to a `Keyword`.
  21 | public export
  22 | interface DOTKeyword t where
  23 |   toKeyword : t -> Keyword
  24 | 
  25 | ||| The type `t` can be converted to a `DOTID`.
  26 | public export
  27 | interface DOTDOTID t where
  28 |   toDOTID : t -> DOTID
  29 | 
  30 | ||| The type `t` can be converted to a `Port`.
  31 | public export
  32 | interface DOTPort t where
  33 |   toPort : t -> Port
  34 | 
  35 | ||| The type `t` can be converted to a `NodeID`.
  36 | public export
  37 | interface DOTNodeID t where
  38 |   toNodeID : t -> NodeID
  39 | 
  40 | ||| The type `t` can be converted to an `Assign`.
  41 | public export
  42 | interface DOTAssign t where
  43 |   toAssign : t -> Assign
  44 | 
  45 | ||| The type `t` can be converted to an `EdgeOp`.
  46 | public export
  47 | interface DOTEdgeOp t where
  48 |   toEdgeOp : t -> EdgeOp
  49 | 
  50 | ||| The type `t` can be converted to an `EdgeRHS`.
  51 | public export
  52 | interface DOTEdgeRHS t where
  53 |   toEdgeRHS : t -> EdgeRHS
  54 | 
  55 | ||| The type `t` can be converted to a `Subgraph`.
  56 | public export
  57 | interface DOTSubgraph t where
  58 |   toSubgraph : t -> Subgraph
  59 | 
  60 | ||| The type `t` can be converted to a `Stmt`.
  61 | public export
  62 | interface DOTStmt t where
  63 |   toStmt : t -> Stmt
  64 | 
  65 | ||| The type `t` can be converted to a `Graph`.
  66 | public export
  67 | interface DOTGraph t where
  68 |   toGraph : t -> Graph
  69 | 
  70 | 
  71 | --------------------------------------------------------------------------------
  72 | -- GENERAL IMPLEMENTATIONS
  73 | --------------------------------------------------------------------------------
  74 | 
  75 | ----------
  76 | -- SHOW --
  77 | ----------
  78 | 
  79 | export
  80 | Show CompassPoint where
  81 |   show N = "n"
  82 |   show NE = "ne"
  83 |   show E = "e"
  84 |   show SE = "se"
  85 |   show S = "s"
  86 |   show SW = "sw"
  87 |   show W = "w"
  88 |   show NW = "nw"
  89 |   show Center = "c"
  90 |   show Underscore = "_"
  91 | 
  92 | export
  93 | Show Keyword where
  94 |   show StrictKW = "strict"
  95 |   show GraphKW = "graph"
  96 |   show DigraphKW = "digraph"
  97 |   show NodeKW = "node"
  98 |   show EdgeKW = "edge"
  99 |   show SubgraphKW = "subgraph"
 100 | 
 101 | export
 102 | Show DOTID where
 103 |   show (StringID id_) = show id_    -- `show` puts " around id_
 104 |   show (NameID name) = name
 105 |   show (Numeral num) = num
 106 |   show (HTML htmlStr) = htmlStr
 107 | 
 108 | export
 109 | Show Port where
 110 |   show (IDPort id_ Nothing) = ":" ++ show id_
 111 |   show (IDPort id_ (Just cpt)) = ":" ++ show id_ ++ ":" ++ show cpt
 112 |   show (PlainPort cpt) = ":" ++ show cpt
 113 | 
 114 | export
 115 | Show NodeID where
 116 |   show (MkNodeID id_ Nothing) = show id_
 117 |   show (MkNodeID id_ (Just port)) = show id_ ++ show port
 118 | 
 119 | export
 120 | Show Assign where
 121 |   show (MkAssign lhs rhs) = show lhs ++ "=" ++ show rhs
 122 | 
 123 | export
 124 | Show EdgeOp where
 125 |   show Arrow = "->"
 126 |   show Dash  = "--"
 127 | 
 128 | mutual
 129 |   -- stmtLists should be shown as
 130 |   -- elem1; elem2; ...; elemN
 131 |   covering
 132 |   showStmtList : List Stmt -> String
 133 |   showStmtList stmtList = joinBy "; " (map show stmtList)
 134 | 
 135 |   -- attrLists should be shown as
 136 |   -- "[ elems1 ]"
 137 |   -- "[ elems1 ][ elems2 ]"
 138 |   -- etc...
 139 |   covering
 140 |   showAttrList : List (List Assign) -> String
 141 |   showAttrList = concatMap show
 142 | 
 143 |   export
 144 |   covering
 145 |   Show EdgeRHS where
 146 |     show (MkEdgeRHS op (Left id_)) = show op ++ " " ++ show id_
 147 |     show (MkEdgeRHS op (Right subGr)) = show op ++ " " ++ show subGr
 148 | 
 149 |   export
 150 |   covering
 151 |   Show Subgraph where
 152 |     show (MkSubgraph Nothing stmtList) =
 153 |       "{ " ++ showStmtList stmtList ++ " }"
 154 | 
 155 |     show (MkSubgraph (Just (kw, Nothing)) stmtList) =
 156 |       show kw ++ " { " ++ showStmtList stmtList ++ " }"
 157 | 
 158 |     show (MkSubgraph (Just (kw, (Just id_))) stmtList) =
 159 |       show kw ++ " " ++ show id_ ++ " { " ++ showStmtList stmtList ++ " }"
 160 | 
 161 |   export
 162 |   covering
 163 |   Show Stmt where
 164 |     show (NodeStmt nodeID attrList) =
 165 |       show nodeID ++ " " ++ concatMap show attrList
 166 | 
 167 |     show (EdgeStmt (Left nodeID) rhs attrList) =
 168 |       show nodeID ++ " " ++ concatMap show rhs ++ " " ++ showAttrList attrList
 169 |     show (EdgeStmt (Right subGr) rhs attrList) =
 170 |       show subGr ++ " " ++ concatMap show rhs ++ " " ++ showAttrList attrList
 171 | 
 172 |     show (AttrStmt kw attrList) =
 173 |       show kw ++ " " ++ showAttrList attrList
 174 | 
 175 |     show (AssignStmt a) =
 176 |       show a
 177 | 
 178 |     show (SubgraphStmt subGr) =
 179 |       show subGr
 180 | 
 181 | export
 182 | covering
 183 | Show Graph where
 184 |   show (MkGraph Nothing graphTy Nothing stmtList) =
 185 |     show graphTy ++ " {\n" ++ showStmtList stmtList ++ "\n}"
 186 | 
 187 |   show (MkGraph Nothing graphTy (Just id_) stmtList) =
 188 |     show graphTy ++ " " ++ show id_ ++ " {\n" ++ showStmtList stmtList ++ "\n}"
 189 | 
 190 |   show (MkGraph (Just strict) graphTy Nothing stmtList) =
 191 |     show strict ++ " " ++ show graphTy
 192 |     ++ " {\n"
 193 |     ++ showStmtList stmtList
 194 |     ++ "\n}"
 195 | 
 196 |   show (MkGraph (Just strict) graphTy (Just id_) stmtList) =
 197 |     show strict ++ " " ++ show graphTy ++ " " ++ show id_
 198 |     ++ " {\n"
 199 |     ++ showStmtList stmtList
 200 |     ++ "\n}"
 201 | 
 202 | --------
 203 | -- EQ --
 204 | --------
 205 | 
 206 | export
 207 | Eq CompassPoint where
 208 |   (==) N  N  = True
 209 |   (==) NE NE = True
 210 |   (==) E  E  = True
 211 |   (==) SE SE = True
 212 |   (==) S  S  = True
 213 |   (==) SW SW = True
 214 |   (==) W  W  = True
 215 |   (==) NW NW = True
 216 |   (==) Center Center = True
 217 |   (==) Underscore Underscore = True
 218 |   (==) _  _  = False
 219 | 
 220 | export
 221 | Eq Keyword where
 222 |   (==) StrictKW   StrictKW   = True
 223 |   (==) GraphKW    GraphKW    = True
 224 |   (==) DigraphKW  DigraphKW  = True
 225 |   (==) NodeKW     NodeKW     = True
 226 |   (==) EdgeKW     EdgeKW     = True
 227 |   (==) SubgraphKW SubgraphKW = True
 228 |   (==) _          _          = False
 229 | 
 230 | export
 231 | Eq DOTID where
 232 |   (==) (StringID id1) (StringID id2) = id1 == id2
 233 |   (==) (NameID n1)    (NameID n2)    = n1 == n2
 234 |   (==) (Numeral num1) (Numeral num2) = num1 == num2
 235 |   (==) (HTML html1)   (HTML html2)   = html1 == html2
 236 |   (==) _              _              = False
 237 | 
 238 | export
 239 | Eq Port where
 240 |   (==) (IDPort id1 mCPT1) (IDPort id2 mCPT2) = mCPT1 == mCPT2 && id1 == id2 
 241 |   (==) (PlainPort cpt1)   (PlainPort cpt2)   = cpt1 == cpt2
 242 |   (==) _                  _                  = False
 243 | 
 244 | export
 245 | Eq NodeID where
 246 |   (==) (MkNodeID id1 mPort1) (MkNodeID id2 mPort2) = mPort1 == mPort2 && id1 == id2 
 247 | 
 248 | export
 249 | Eq Assign where
 250 |   (==) (MkAssign lhs1 rhs1) (MkAssign lhs2 rhs2) = lhs1 == lhs2 && rhs1 == rhs2
 251 | 
 252 | export
 253 | Eq EdgeOp where
 254 |   (==) Arrow Arrow = True
 255 |   (==) Dash  Dash  = True
 256 |   (==) _     _     = False
 257 | 
 258 | mutual
 259 |   export
 260 |   covering
 261 |   Eq EdgeRHS where
 262 |     (==) (MkEdgeRHS op1 s1) (MkEdgeRHS op2 s2) = op1 == op2 && s1 == s2
 263 | 
 264 |   export
 265 |   covering
 266 |   Eq Subgraph where
 267 |     (==) (MkSubgraph mSubGrID1 stmtList1) (MkSubgraph mSubGrID2 stmtList2) =
 268 |       mSubGrID1 == mSubGrID2 && stmtList1 == stmtList2
 269 | 
 270 |   export
 271 |   covering
 272 |   Eq Stmt where
 273 |     (==) (NodeStmt nodeID1 attrList1) (NodeStmt nodeID2 attrList2) =
 274 |       nodeID1 == nodeID2 && attrList1 == attrList2
 275 | 
 276 |     (==) (EdgeStmt e1 rhs1 attrList1) (EdgeStmt e2 rhs2 attrList2) =
 277 |       e1 == e2 && rhs1 == rhs2 && attrList1 == attrList2
 278 | 
 279 |     (==) (AttrStmt kw1 attrList1) (AttrStmt kw2 attrList2) =
 280 |       kw1 == kw2 && attrList1 == attrList2
 281 | 
 282 |     (==) (AssignStmt a1) (AssignStmt a2) =
 283 |       a1 == a2
 284 | 
 285 |     (==) (SubgraphStmt subGr1) (SubgraphStmt subGr2) =
 286 |       subGr1 == subGr2
 287 | 
 288 |     (==) _ _ =
 289 |       False
 290 | 
 291 | export
 292 | covering
 293 | Eq Graph where
 294 |   (==) (MkGraph s1 grTy1 mID1 stmtList1) (MkGraph s2 grTy2 mID2 stmtList2) =
 295 |     s1 == s2 && grTy1 == grTy2 && mID1 == mID2 && stmtList1 == stmtList2
 296 | 
 297 |