@@ -3,7 +3,7 @@
33Parser
44======
55
6−To run the parser we call ``parse``. This requires a Grammar and the output
6+To run the parser we call ``parse``. This requires a grammar and the output
77from the lexer (which is a list of tokens).
88
99.. code-block:: idris
@@ -18,13 +18,13 @@ If successful this returns 'Right' with a pair of
1818
1919otherwise it returns 'Left' with the error message.
2020
21−So we need to define the Grammar for our parser, this is done using the following
21+So we need to define the grammar for our parser, this is done using the following
2222'Grammar' data structure. This is a combinator structure, similar in principle
2323to the recogniser combinator for the lexer, which was discussed on the
2424previous page.
2525
26−As with the Recogniser the Grammar type is dependent on a boolean 'consumes'
27−value which allows us to ensure that complicated Grammar structures will always
26+As with the Recogniser the ``Grammar`` type is dependent on a boolean 'consumes'
27+value which allows us to ensure that complicated ``Grammar`` structures will always
2828consume input.
2929
3030.. code-block:: idris
@@ -53,7 +53,7 @@ consume input.
5353 Grammar tok c1 ty -> Grammar tok c2 ty ->
5454 Grammar tok (c1 && c2) ty
5555
56−So an example of a Grammer type may look something like this:
56+So an example of a grammer type may look something like this:
5757``Grammar (TokenData ExpressionToken) True Integer``.
5858This is a complicated type name and a given parser will need to use it a lot.
5959So to reduce the amount of typing we can use the following type synonym (similar
@@ -89,7 +89,7 @@ this page we will go on to add a parser for this running example.
8989
9090.. list-table::
9191
92− * - To start, here is a Grammar to parse an integer literal (that is, a
92+ * - To start, here is a grammar to parse an integer literal (that is, a
9393 sequence of numeric characters).
9494
9595 - .. code-block:: idris
@@ -280,13 +280,15 @@ So lets try to use this to define a grammar which recognises either:
280280- An integer literal inside parenthesis inside parenthesis
281281- ... and so on.
282282
283−This requires a recursively defined structure like this:
283+.. list-table::
284284
285−.. code-block:: idris
285+ * - This requires a recursively defined structure like this:
286286
287− partial
288− expr : Rule Integer
289− expr = intLiteral <|> (paren expr)
287+ - .. code-block:: idris
288+
289+ partial
290+ expr : Rule Integer
291+ expr = intLiteral <|> (paren expr)
290292
291293This is a valid grammar because every time it is called it is guaranteed to
292294consume a token. However, as an Idris structure, it is problematic due to
@@ -330,7 +332,7 @@ defined like this:
330332 pure r
331333
332334This 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.
335+using ``Inf`` so we can implement recursively defined grammars as above.
334336
335337Implementing the Arithmetic Operators
336338-------------------------------------
@@ -359,7 +361,7 @@ In order to work up to this gradually lets start with prefix operators
359361
360362 expr = (add (op "+") expr expr)
361363
362−where `op` is defined like this:
364+where ``op`` is defined like this:
363365
364366.. code-block:: idris
365367
@@ -374,6 +376,12 @@ where `op` is defined like this:
374376
375377 * - and ``add`` is defined like this:
376378
379+ Where:
380+
381+ - x is the add operator.
382+ - y is the first operand.
383+ - z is the second operand.
384+
377385 - .. code-block:: idris
378386
379387 addInt : Integer -> Integer -> Integer
@@ -386,40 +394,37 @@ where `op` is defined like this:
386394 Grammar tok ((c1 || c2) || c3) Integer
387395 add x y z = map addInt (x *> y) <*> z
388396
389−Where:
390397
391−- x is the add operator.
392−- y is the first operand.
393−- z is the second operand.
394398
395399The resulting integer will be the sum of the two operands.
396400
397−The other operators are defined in a similar way:
401+.. list-table::
398402
399−.. code-block:: idris
403+ * - The other operators are defined in a similar way:
400404
401− subInt : Integer -> Integer -> Integer
402− subInt a b = a-b
405+ - .. code-block:: idris
403406
404− export
405− sub : Grammar tok c1 Integer ->
406− Grammar tok c2 Integer ->
407− Grammar tok c3 Integer ->
408− Grammar tok ((c1 || c2) || c3) Integer
409− sub x y z = map subInt (x *> y) <*> z
407+ subInt : Integer -> Integer -> Integer
408+ subInt a b = a-b
410409
410+ export
411+ sub : Grammar tok c1 Integer ->
412+ Grammar tok c2 Integer ->
413+ Grammar tok c3 Integer ->
414+ Grammar tok ((c1 || c2) || c3) Integer
415+ sub x y z = map subInt (x *> y) <*> z
411416
412− multInt : Integer -> Integer -> Integer
413− multInt a b = a*b
417+ multInt : Integer -> Integer -> Integer
418+ multInt a b = a*b
414419
415− export
416− mult : Grammar tok c1 Integer ->
417− Grammar tok c2 Integer ->
418− Grammar tok c3 Integer ->
419− Grammar tok ((c1 || c2) || c3) Integer
420− mult x y z = map multInt (x *> y) <*> z
420+ export
421+ mult : Grammar tok c1 Integer ->
422+ Grammar tok c2 Integer ->
423+ Grammar tok c3 Integer ->
424+ Grammar tok ((c1 || c2) || c3) Integer
425+ mult x y z = map multInt (x *> y) <*> z
421426
422−So the top level Grammar can now be defined as follows. Note that this is
427+So the top level ``Grammar`` can now be defined as follows. Note that this is
423428partial as it is a potentially infinite structure and so not total.
424429
425430.. code-block:: idris
@@ -472,7 +477,7 @@ Then an invalid syntax:
472477 List (TokenData ExpressionToken))
473478
474479However if we try something that is invalid, but starts with a valid token,
475−then it will return 'Right' (to indicate success)
480+then it will return ``Right`` (to indicate success)
476481
477482.. code-block:: idris
478483
@@ -499,21 +504,10 @@ Infix Notation
499504--------------
500505
501506So far we have implemented a prefix notation for operators (like this:
502−'+ expr expr') but the aim is to implemented an infix notation (like this:
503−'expr + expr'). To do this we must be able to deal with potentially
507+``+ expr expr``) but the aim is to implemented an infix notation (like this:
508+``expr + expr``). To do this we must be able to deal with potentially
504509infinite data structures (see Codata Types here :ref:`sect-typefuns`).
505510
506−.. code-block:: idris
507−
508− expression = ["+"|"-"] term {("+"|"-") term} .
509−
510− term = factor {("*"|"/") factor} .
511−
512− factor =
513− ident
514− | number
515− | "(" expression ")"
516−
517511First alter the grammar to have infix operations:
518512
519513.. code-block:: idris
@@ -569,10 +563,10 @@ If we have a rule like this:
569563
570564 A -> (x<*>y) <|> (x<*>z)
571565
572−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has
573−already consumed 'x', so now 'x<*>z' will fail.
566+If ``x<*>y`` fails but ``x<*>z`` would succeed a problem is that, ``x<*>y`` has
567+already consumed ``x``, so now ``x<*>z`` will fail.
574568
575−so we could write code to backtrack. That is 'try' 'x<*>y' without consuming
569+so we could write code to backtrack. That is ``try`` ``x<*>y`` without consuming
576570so that, if the first token succeeds but the following tokens fail, then the
577571first tokens would not be consumed.
578572
@@ -599,9 +593,22 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although
599593not every context-free grammar can be converted to a LL(1) grammar.
600594
601595This still does not solve the infinite recursion issue and there is another
602−problem: the precedence of the operators +, - and * is not explicit.
596+problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.
597+
598+.. list-table::
599+
600+ * - To resolve this we can alter the example to have a BNF like this:
601+
602+ - .. code-block:: idris
603+
604+ 'expression' ::= ['+'|'-'] 'term' {('+'|'-') 'term'}
605+
606+ 'term' ::= 'factor' {'*' 'factor'}
607+
608+ 'factor' ::=
609+ number
610+ | '(' 'expression' ')'
603611
604−To resolve this we can alter the example like this:
605612
606613.. code-block:: idris
607614