0 | module Graphics.DOT.Parser
  1 |
  2 | import Libraries.Text.Parser
  3 |
  4 | import Data.Vect
  5 | import Data.List1
  6 | import Data.String
  7 |
  8 | import Graphics.DOT.Lexer
  9 | import Graphics.DOT.AST
 10 |
 11 | %default total
 12 |
 13 |
 14 | ------------------------------------------------------------------------
 15 | -- Interfaces
 16 |
 17 | export
 18 | Show (ParsingError DOTToken) where
 19 |   show (Error errStr Nothing) = errStr
 20 |   show (Error errStr (Just (MkBounds startLine startCol endLine endCol)))
 21 |     = "\{errStr}@L\{show startLine}:\{show startCol}-L\{show endLine}:\{show endCol}"
 22 |
 23 |
 24 | ------------------------------------------------------------------------
 25 | -- Terminals --
 26 |
 27 | lBrace : Grammar _ DOTToken True ()
 28 | lBrace = terminal "Expected '{'"
 29 |             (\case LBrace => Just ()
 30 |                    _ => Nothing)
 31 |
 32 | rBrace : Grammar _ DOTToken True ()
 33 | rBrace = terminal "Expected '}' (might not be properly closed?)"
 34 |             (\case RBrace => Just ()
 35 |                    _ => Nothing)
 36 |
 37 | lBracket : Grammar _ DOTToken True ()
 38 | lBracket = terminal "Expected '['"
 39 |               (\case LBracket => Just ()
 40 |                      _ => Nothing)
 41 |
 42 | rBracket : Grammar _ DOTToken True ()
 43 | rBracket = terminal "Expected ']' (might not be properly closed?)"
 44 |               (\case RBracket => Just ()
 45 |                      _ => Nothing)
 46 |
 47 | colon : Grammar _ DOTToken True ()
 48 | colon = terminal "Expected ':'"
 49 |           (\case Colon => Just ()
 50 |                  _ => Nothing)
 51 |
 52 | semicolon : Grammar _ DOTToken True ()
 53 | semicolon = terminal "Expected ';' (shouldn't get this message)"
 54 |               (\case Semicolon => Just ()
 55 |                      _ => Nothing)
 56 |
 57 | comma : Grammar _ DOTToken True ()
 58 | comma = terminal "Expected ','"
 59 |           (\case Comma => Just ()
 60 |                  _ => Nothing)
 61 |
 62 | equals : Grammar _ DOTToken True ()
 63 | equals = terminal "Expected '='"
 64 |           (\case Equal => Just ()
 65 |                  _ => Nothing)
 66 |
 67 | nameID : Grammar _ DOTToken True DOTID
 68 | nameID = terminal "Not a name"
 69 |           (\case (NameID name) => Just (NameID name)
 70 |                  _ => Nothing)
 71 |
 72 | numeralID : Grammar _ DOTToken True DOTID
 73 | numeralID = terminal "Not a numeral"
 74 |               (\case (NumeralID num) => Just (Numeral num)
 75 |                      _ => Nothing)
 76 |
 77 | stringID : Grammar _ DOTToken True DOTID
 78 | stringID = terminal "Not a string"
 79 |             (\case (StringID str) => Just (StringID str)
 80 |                    _ => Nothing)
 81 |
 82 | htmlID : Grammar _ DOTToken True DOTID
 83 | htmlID = terminal "Not an HTML string"
 84 |           (\case (HTML_ID html) => Just (HTML html)
 85 |                  _ => Nothing)
 86 |
 87 | nodeKW : Grammar _ DOTToken True Keyword
 88 | nodeKW = terminal "Expected 'node' keyword"
 89 |           (\case Keyword "node" => Just NodeKW
 90 |                  _ => Nothing)
 91 |
 92 | edgeKW : Grammar _ DOTToken True Keyword
 93 | edgeKW = terminal "Expecetd 'edge' keyword"
 94 |           (\case Keyword "edge" => Just EdgeKW
 95 |                  _ => Nothing)
 96 |
 97 | graphKW : Grammar _ DOTToken True Keyword
 98 | graphKW = terminal "Expected 'graph' keyword"
 99 |            (\case Keyword "graph" => Just GraphKW
100 |                   _ => Nothing)
101 |
102 | digraphKW : Grammar _ DOTToken True Keyword
103 | digraphKW = terminal "Expected 'digraph' keyword"
104 |               (\case Keyword "digraph" => Just DigraphKW
105 |                      _ => Nothing)
106 |
107 | subgraphKW : Grammar _ DOTToken True Keyword
108 | subgraphKW = terminal "Expected 'subgraph' keyword"
109 |               (\case Keyword "subgraph" => Just SubgraphKW
110 |                      _ => Nothing)
111 |
112 | strictKW : Grammar _ DOTToken True Keyword
113 | strictKW = terminal "Expected 'strict' keyword"
114 |             (\case Keyword "strict" => Just StrictKW
115 |                    _ => Nothing)
116 |
117 | ||| Compass points (n, ne, e, se, s, sw, w, nw, c, _).
118 | compassPt : Grammar _ DOTToken True CompassPoint
119 | compassPt = terminal "Unknown compass-point"
120 |               (\case CompassPt pt =>
121 |                         case pt of
122 |                              "n"  => Just N
123 |                              "ne" => Just NE
124 |                              "e"  => Just E
125 |                              "se" => Just SE
126 |                              "s"  => Just S
127 |                              "sw" => Just SW
128 |                              "w"  => Just W
129 |                              "nw" => Just NW
130 |                              "c"  => Just Center
131 |                              "_"  => Just Underscore
132 |                              _    => Nothing
133 |                      _ => Nothing)
134 |
135 | ||| --
136 | grEdgeOp : Grammar _ DOTToken True EdgeOp
137 | grEdgeOp = terminal "Expected '--'"
138 |             (\case GrEdgeOp => Just Dash
139 |                    _ => Nothing)
140 |
141 | ||| ->
142 | diGrEdgeOp : Grammar _ DOTToken True EdgeOp
143 | diGrEdgeOp = terminal "Exepected '->'"
144 |               (\case DiGrEdgeOp => Just Arrow
145 |                      _ => Nothing)
146 |
147 |
148 | -- Non-terminals --
149 |
150 | ||| Keywords ('node', 'edge', 'graph', 'digraph', 'subgraph', 'strict').
151 | keyword : Grammar _ DOTToken True Keyword
152 | keyword =  nodeKW
153 |        <|> edgeKW
154 |        <|> graphKW
155 |        <|> digraphKW
156 |        <|> subgraphKW
157 |        <|> strictKW
158 |
159 | ||| An identifier is either:
160 | ||| - a name
161 | ||| - a numeral
162 | ||| - a quoted string
163 | ||| - an HTML string
164 | identifier : Grammar _ DOTToken True DOTID
165 | identifier =  nameID
166 |           <|> numeralID
167 |           <|> stringID
168 |           <|> htmlID
169 |
170 | ||| Assignment, i.e.
171 | ||| ID '=' ID
172 | assign_ : Grammar _ DOTToken True Assign
173 | assign_ = do idLHS <- identifier
174 |              equals
175 |              idRHS <- identifier
176 |              pure (MkAssign idLHS idRHS)
177 |
178 | ||| Separators are semicolons and commas, but they are purely aesthetic.
179 | sepChoice : Grammar _ DOTToken False ()
180 | sepChoice = ignore $ optional (choose semicolon comma)
181 |
182 | ||| An 'a_list' is an assignment, optionally followed by a separator, optionally
183 | ||| followed by more of an 'a_list'.
184 | a_list : Grammar _ DOTToken True (List Assign)
185 | a_list = do head <- assign_
186 |             sepChoice
187 |             rest <- (a_list <|> pure [])
188 |             pure (head :: rest)
189 |
190 | -- helper for `attr_list`
191 | attr_list : Grammar _ DOTToken True (List (List Assign))
192 | attr_list = do lBracket
193 |                mAList <- optional a_list
194 |                rBracket
195 |                rest <- (attr_list <|> pure [])
196 |                the (Grammar _ _ False _) $   -- case can confuse the type-checker
197 |                  case mAList of
198 |                       Nothing      => pure rest
199 |                       (Just aList) => pure (aList :: rest)
200 |
201 | ||| An attr_stmt is one of the keywords 'graph', 'node', or 'edge', followed by
202 | ||| an attr_list.
203 | attr_stmt : Grammar _ DOTToken True Stmt
204 | attr_stmt =
205 |   do kw <- gne    -- (graph|node|edge)
206 |      attrList <- attr_list
207 |      pure (AttrStmt kw attrList)
208 |   where
209 |     gne : Grammar _ DOTToken True Keyword
210 |     gne =  graphKW
211 |        <|> nodeKW
212 |        <|> edgeKW
213 |
214 | ||| A colon followed by an ID, optionally followed by more colon+compass_pt
215 | ||| pairs.
216 | idPort : Grammar _ DOTToken True Port
217 | idPort = do colon
218 |             id_ <- identifier
219 |             maybeCPT <- optional compassPt
220 |             pure (IDPort id_ maybeCPT)
221 |
222 | ||| A colon followed by a compass_pt.
223 | cptPort : Grammar _ DOTToken True Port
224 | cptPort = do colon
225 |              cpt <- compassPt
226 |              pure (PlainPort cpt)
227 |
228 | ||| A port is either:
229 | ||| - A colon followed by an ID, optionally followed by more colon+compass_pt
230 | |||   pairs.
231 | ||| - A colon followed by a compass_pt.
232 | port : Grammar _ DOTToken True Port
233 | port =  idPort
234 |     <|> cptPort
235 |
236 | ||| A 'node_id' is an identifier optionally followed by a port.
237 | node_id : Grammar _ DOTToken True NodeID
238 | node_id = do id_ <- identifier
239 |              mPort <- optional port
240 |              pure (MkNodeID id_ mPort)
241 |
242 | ||| A 'node_stmt' is a 'node_id' optionally followed by an 'attr_list'.
243 | node_stmt : Grammar _ DOTToken True Stmt
244 | node_stmt = do nID <- node_id
245 |                attrList <- (attr_list <|> pure [])
246 |                pure (NodeStmt nID attrList)
247 |
248 | ||| An edgeop is either '->' in directed graphs, or '--' in undirected graphs.
249 | edgeop : Grammar _ DOTToken True EdgeOp
250 | edgeop =  diGrEdgeOp
251 |       <|> grEdgeOp
252 |
253 | ||| A subgraph start is the keyword 'subgraph' optionally followed by an
254 | ||| identifier.
255 | subgraphStart : Grammar _ DOTToken True (Keyword, Maybe DOTID)
256 | subgraphStart = do kw <- subgraphKW
257 |                    mID <- optional identifier
258 |                    pure (kw, mID)
259 |
260 | mutual
261 |   ||| A subgraph is optionally a `subgraphStart` (a helper function), followed
262 |   ||| by a '{', followed by a 'stmt_list', followed by a '}'.
263 |   subgraph : Grammar _ DOTToken True Subgraph
264 |   subgraph = do start <- optional subgraphStart
265 |                 lBrace
266 |                 stmtList <- stmt_list
267 |                 rBrace
268 |                 pure (MkSubgraph start stmtList)
269 |
270 |   -- helper for `edgeRHS` and 'edge_stmt'
271 |   nidORsubgr : Grammar _ DOTToken True (Either NodeID Subgraph)
272 |   nidORsubgr =  (do subgr <- subgraph; pure (Right subgr))
273 |             <|> (do nID <- node_id; pure (Left nID))
274 |
275 |   -- helper for `edgeRHS`, not requiring the list to be non-empty
276 |   edgeRHS' : Grammar _ DOTToken True (List EdgeRHS)
277 |   edgeRHS' = do edgeOp <- edgeop
278 |                 nORs <- nidORsubgr
279 |                 rest <- (edgeRHS' <|> pure [])
280 |                 pure ((MkEdgeRHS edgeOp nORs) :: rest)
281 |
282 |   ||| The RHS of an edge is an 'edgeop', followed by either a 'node_id' or a
283 |   ||| 'subgraph', optionally followed by more 'edgeRHS'.
284 |   edgeRHS : Grammar _ DOTToken True (List1 EdgeRHS)
285 |   edgeRHS = do edgeOp <- edgeop
286 |                nORs <- nidORsubgr
287 |                rest <- (edgeRHS' <|> pure [])
288 |                pure ((MkEdgeRHS edgeOp nORs) ::: rest)
289 |
290 |   ||| An 'edge_stmt' is either a 'node_id' or a 'subgraph', followed by an
291 |   ||| 'edgeRHS', optionally followed by an 'attr_list'.
292 |   edge_stmt : Grammar _ DOTToken True Stmt
293 |   edge_stmt = do nORs <- nidORsubgr
294 |                  rhs <- edgeRHS
295 |                  attrList <- (attr_list <|> pure [])
296 |                  pure (EdgeStmt nORs rhs attrList)
297 |
298 |   subgr_stmt : Grammar _ DOTToken True Stmt
299 |   subgr_stmt = do subgr <- subgraph
300 |                   pure $ SubgraphStmt subgr
301 |
302 |   assign_stmt : Grammar _ DOTToken True Stmt
303 |   assign_stmt = do a <- assign_
304 |                    pure $ AssignStmt a
305 |
306 |   ||| A 'stmt' is either a 'node_stmt', 'edge_stmt', 'attr_stmt', an assignment,
307 |   ||| or a subgraph.
308 |   stmt : Grammar _ DOTToken True Stmt
309 |   stmt =  subgr_stmt
310 |       <|> edge_stmt
311 |       <|> attr_stmt
312 |       <|> assign_stmt
313 |       <|> node_stmt
314 |
315 |   ||| A 'stmt_list' is optionally: a 'stmt', followed by an optional semicolon,
316 |   ||| followed by more of a 'stmt_list'.
317 |   stmt_list : Grammar _ DOTToken True (List Stmt)
318 |   stmt_list = do aStmt <- stmt
319 |                  ignore $ optional semicolon   -- we don't store the ';'
320 |                  rest <- (stmt_list <|> pure [])
321 |                  pure (aStmt :: rest)
322 |
323 |   -- Is the graph strict? Helper for 'graph'.
324 |   isStrict : Grammar _ DOTToken False Bool
325 |   isStrict = do (Just _) <- optional strictKW
326 |                   | Nothing => pure False
327 |                 pure True
328 |
329 |   -- Directed or undirected graph? Helper for 'graph'.
330 |   graphType : Grammar _ DOTToken True Keyword
331 |   graphType =  graphKW
332 |            <|> digraphKW
333 |
334 |   ||| A 'graph' is optionally the keyword "strict", followed by either the
335 |   ||| keywords "graph" or "digraph", optionally followed by an identifier,
336 |   ||| followed by a 'stmt_list' in braces.
337 |   graph : Grammar _ DOTToken True Graph
338 |   graph = do strict <- isStrict
339 |              gType <- graphType
340 |              mID <- optional identifier
341 |              lBrace
342 |              stmtList <- stmt_list
343 |              rBrace
344 |              pure (MkGraph (if strict then Just StrictKW else Nothing) gType mID stmtList)
345 |
346 | export
347 | parse :  (xs : List (WithBounds DOTToken))
348 |       -> Either (List1 (ParsingError DOTToken))
349 |                 (ParsingWarnings, Graph, List (WithBounds DOTToken))
350 | parse xs = parse graph xs
351 |
352 |