@@ -3,8 +3,8 @@
33Parser
44======
55
6−To run our parser we call 'parse'. This requires a Grammar and the output
7−from the lexer (a list of tokens).
6+To run the parser we call ``parse``. This requires a Grammar and the output
7+from the lexer (which is a list of tokens).
88
99.. code-block:: idris
1010
@@ -54,12 +54,12 @@ consume input.
5454 Grammar tok (c1 && c2) ty
5555
5656So an example of a Grammer type may look something like this:
57−'Grammar (TokenData ExpressionToken) True Integer'.
58−
57+``Grammar (TokenData ExpressionToken) True Integer``.
5958This is a complicated type name and a given parser will need to use it a lot.
6059So to reduce the amount of typing we can use the following type synonym (similar
6160to what is done in Idris 2
6261: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
62+)
6363
6464.. code-block:: idris
6565
@@ -71,12 +71,12 @@ Parser Example
7171--------------
7272
7373On the previous page we implemented a lexer to 'lex' a very simple expression, on
74−this page we will go on to implement a parser for this running example.
74+this page we will go on to add a parser for this running example.
7575
7676.. list-table::
7777
78− * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
79− like this:
78+ * - The syntax we are aiming at is something
79+ like this (expressed in Backus–Naur form (BNF)):
8080 - .. code-block:: idris
8181
8282 <expr> ::= <integer literal>
@@ -90,7 +90,7 @@ this page we will go on to implement a parser for this running example.
9090.. list-table::
9191
9292 * - To start, here is a Grammar to parse an integer literal (that is, a
93− sequence of numbers).
93+ sequence of numeric characters).
9494
9595 - .. code-block:: idris
9696
@@ -144,7 +144,7 @@ successful, this is because we are not specifically checking for end-of-file.
144144
145145.. list-table::
146146
147− * - The 'intLiteral' function above uses the 'terminal' function to
147+ * - The ``intLiteral`` function above uses the ``terminal`` function to
148148 construct the grammar
149149 - .. code-block:: idris
150150
@@ -174,10 +174,10 @@ Idris 2 uses a slightly different version which stores an error message like
174174 OParen => Just 0
175175 _ => Nothing)
176176
177−Integer value is not really relevant for parenthesis so '0' is used as
177+Integer value is not really relevant for parenthesis so ``0`` (zero) is used as
178178a default value.
179179
180−As before, we can test this out with a function like this:
180+As before, this can be tested with a function like this:
181181
182182.. code-block:: idris
183183
@@ -202,10 +202,10 @@ error for anything else:
202202 List (TokenData ExpressionToken))
203203
204204Now we have two Grammars we can try combining them. The following test looks
205−for 'openParen' followed by 'intLiteral', the two Grammars are combined using
206−'<*>'. The 'map const' part uses the integer value from the first.
205+for ``openParen`` followed by ``intLiteral``, the two Grammars are combined using
206+``<*>``. The ``map const`` part uses the integer value from the first.
207207
208−The following test is looking for '(' followed by a number:
208+The following test is looking for ``(`` followed by a number:
209209
210210.. code-block:: idris
211211
@@ -213,8 +213,8 @@ The following test is looking for '(' followed by a number:
213213 (Integer, List (TokenData ExpressionToken))
214214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
215215
216−We can see below that '(' followed by a number is successfully parsed but other
217−token lists are not:
216+We can see below that ``(`` followed by a number is successfully parsed but, as
217+required, other token lists are not:
218218
219219.. code-block:: idris
220220
@@ -270,21 +270,85 @@ token lists are not:
270270 paren : Rule Integer -> Rule Integer
271271 paren exp = openParen *> exp <* closeParen
272272
273−The use of '*>' and '<*' instead of '<*>' is an easy way to use the integer
273+The use of ``*>`` and ``<*`` instead of ``<*>`` is an easy way to use the integer
274274value from the inner expression.
275275
276+So lets try to use this to define a grammar which recognises either:
277+
278+- An integer literal
279+- An integer literal inside parenthesis
280+- An integer literal inside parenthesis inside parenthesis
281+- ... and so on.
282+
283+This requires a recursively defined structure like this:
284+
285+.. code-block:: idris
286+
287+ partial
288+ expr : Rule Integer
289+ expr = intLiteral <|> (paren expr)
290+
291+This is a valid grammar because every time it is called it is guaranteed to
292+consume a token. However, as an Idris structure, it is problematic due to
293+the recursion. Defining it as partial allows it to compile but at runtime
294+we are likely to get a crash with an (unhelpful) error message like
295+``killed by signal 11``.
296+
297+So a better method is to use ``do`` notation as described in the following
298+section.
299+
300+Monadic Combinator
301+------------------
302+
303+In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is
304+defined like this:
305+
306+.. code-block:: idris
307+
308+ ||| Sequence two grammars. If either consumes some input, the sequence is
309+ ||| guaranteed to consume some input. If the first one consumes input, the
310+ ||| second is allowed to be recursive (because it means some input has been
311+ ||| consumed and therefore the input is smaller)
312+ export %inline
313+ (>>=) : {c1 : Bool} ->
314+ Grammar tok c1 a ->
315+ inf c1 (a -> Grammar tok c2 b) ->
316+ Grammar tok (c1 || c2) b
317+ (>>=) {c1 = False} = SeqEmpty
318+ (>>=) {c1 = True} = SeqEat
319+
276320.. list-table::
277321
278− * - Now for the operations, in this case: '+', '-' and '*'.
279− The syntax we require is that operators like '+' are infix operators, which
280− would require a definition like this:
322+ * - This allows us to use ``do`` notation for the previous parenthesis example:
281323
282324 - .. code-block:: idris
283325
284− expr = (add expr (op "+") expr)
326+ expr = intLiteral <|> do
327+ openParen
328+ r <- expr
329+ closeParen
330+ pure r
331+
332+This can be more flexible than using the ``<*>`` operator. Also it is defined
333+using ``Inf`` so we can implement recursively defined grammars like the above.
334+
335+Implementing the Arithmetic Operators
336+-------------------------------------
337+
338+.. list-table::
339+
340+ * - Now for the operations, in this case: ``+``, ``-`` and ``*``.
341+ The syntax we require for these infix operators
342+ would require recursive grammars like this:
343+
344+ - .. code-block:: idris
285345
286−This is a potentially infinite structure which is not total.
287−In order to work up to this gradually I will start with prefix operators
346+ expr = expr (op "+") expr
347+
348+As already explained, ``do`` notation can allow us to use recursive
349+definitions but not necessarily left-recursion like this.
350+
351+In order to work up to this gradually lets start with prefix operators
288352(sometimes known as Polish notation) then modify later for infix operators.
289353
290354.. list-table::
@@ -295,7 +359,7 @@ In order to work up to this gradually I will start with prefix operators
295359
296360 expr = (add (op "+") expr expr)
297361
298−where 'op' is defined like this:
362+where `op` is defined like this:
299363
300364.. code-block:: idris
301365
@@ -308,7 +372,7 @@ where 'op' is defined like this:
308372
309373.. list-table::
310374
311− * - and 'add' is defined like this:
375+ * - and ``add`` is defined like this:
312376
313377 - .. code-block:: idris
314378
@@ -439,6 +503,17 @@ So far we have implemented a prefix notation for operators (like this:
439503'expr + expr'). To do this we must be able to deal with potentially
440504infinite data structures (see Codata Types here :ref:`sect-typefuns`).
441505
506+.. code-block:: idris
507+
508+ expression = ["+"|"-"] term {("+"|"-") term} .
509+
510+ term = factor {("*"|"/") factor} .
511+
512+ factor =
513+ ident
514+ | number
515+ | "(" expression ")"
516+
442517First alter the grammar to have infix operations:
443518
444519.. code-block:: idris