0 | module Graphics.DOT.AST
  1 |
  2 | import Data.List1
  3 |
  4 | %default total
  5 |
  6 | ||| The various compass points that can be used in DOT
  7 | public export
  8 | data CompassPoint
  9 |   = N
 10 |   | NE
 11 |   | E
 12 |   | SE
 13 |   | S
 14 |   | SW
 15 |   | W
 16 |   | NW
 17 |   | Center
 18 |   | Underscore
 19 |
 20 | ||| The various DOT keywords
 21 | public export
 22 | data Keyword
 23 |   = StrictKW
 24 |   | GraphKW
 25 |   | DigraphKW
 26 |   | NodeKW
 27 |   | EdgeKW
 28 |   | SubgraphKW
 29 |
 30 | ||| A DOT identifier
 31 | public export
 32 | data DOTID : Type where
 33 |   StringID : (id_ : String) -> DOTID
 34 |   NameID   : (name : String) -> DOTID
 35 |   Numeral  : (num : String) -> DOTID
 36 |   HTML     : (htmlStr : String) -> DOTID
 37 |
 38 | ||| A DOT port
 39 | public export
 40 | data Port : Type where
 41 |   ||| A port with an id
 42 |   |||   port :=  ':' ID [ ':' compass_pt ]
 43 |   IDPort :  (id_ : DOTID) -> Maybe CompassPoint -> Port
 44 |
 45 |   ||| A port without an id
 46 |   |||   port |=  ':' compass_pt
 47 |   PlainPort : CompassPoint -> Port
 48 |
 49 | ||| A node identifier (separate from regular identifiers, for some reason)
 50 | public export
 51 | data NodeID : Type where
 52 |   MkNodeID : (id_ : DOTID) -> (mPort : Maybe Port) -> NodeID
 53 |
 54 | ||| Assignment
 55 | |||   id '=' id
 56 | public export
 57 | data Assign : Type where
 58 |   MkAssign :  (lhs : DOTID)
 59 |            -> (rhs : DOTID)
 60 |            -> Assign
 61 |
 62 | ||| An edge op
 63 | public export
 64 | data EdgeOp : Type where
 65 |   -- TODO: Could be dependent on whether the graph is `strict`?
 66 |   Arrow : EdgeOp
 67 |   Dash  : EdgeOp
 68 |
 69 | mutual
 70 |   ||| The right hand side (RHS) of an edge op
 71 |   public export
 72 |   data EdgeRHS : Type where
 73 |     MkEdgeRHS :  (op : EdgeOp)
 74 |               -> Either NodeID Subgraph
 75 |               -> EdgeRHS
 76 |
 77 |   ||| A subgraph
 78 |   public export
 79 |   data Subgraph : Type where
 80 |     MkSubgraph :  Maybe (Keyword, Maybe DOTID)
 81 |                -> (stmtList : List Stmt)
 82 |                -> Subgraph
 83 |
 84 |   ||| A DOT statement
 85 |   public export
 86 |   data Stmt : Type where
 87 |
 88 |     NodeStmt : (nodeID : NodeID) -> (attrList : List (List Assign)) -> Stmt
 89 |
 90 |     EdgeStmt :  Either NodeID Subgraph
 91 |              -> (rhs : List1 EdgeRHS)
 92 |              -> (attrList : List (List Assign))
 93 |              -> Stmt
 94 |
 95 |     ||| An attribute statement
 96 |     ||| `attr_stmt : (graph | node | edge) '[' [ a_list ] ']' [ attr_list ]`
 97 |     AttrStmt :  (kw : Keyword)
 98 |              -> (attrList : List (List Assign))
 99 |              -> Stmt
100 |
101 |     AssignStmt : (a : Assign) -> Stmt
102 |
103 |     SubgraphStmt : (subGr : Subgraph) -> Stmt
104 |
105 | ||| A DOT graph. This is the top-level IR node
106 | public export
107 | data Graph : Type where
108 |   -- TODO: this could possibly be turned into multiple constructors
109 |   --       (e.g. Graph, Digraph, StrictGraph, etc.)?
110 |   MkGraph :  (strict : Maybe Keyword)
111 |           -> (graphTy : Keyword)
112 |           -> (mID_ : Maybe DOTID)
113 |           -> (stmtList : List Stmt)
114 |           -> Graph
115 |
116 |