@@ -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
@@ -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,13 +53,13 @@ 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:
57−'Grammar (TokenData ExpressionToken) True Integer'.
58−
56+So an example of a grammer type may look something like this:
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>
@@ -89,8 +89,8 @@ this page we will go on to implement 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
93− sequence of numbers).
92+ * - To start, here is a grammar to parse an integer literal (that is, a
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,87 @@ 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+.. list-table::
284+
285+ * - This requires a recursively defined structure like this:
286+
287+ - .. code-block:: idris
288+
289+ partial
290+ expr : Rule Integer
291+ expr = intLiteral <|> (paren expr)
292+
293+This is a valid grammar because every time it is called it is guaranteed to
294+consume a token. However, as an Idris structure, it is problematic due to
295+the recursion. Defining it as partial allows it to compile but at runtime
296+we are likely to get a crash with an (unhelpful) error message like
297+``killed by signal 11``.
298+
299+So a better method is to use ``do`` notation as described in the following
300+section.
301+
302+Monadic Combinator
303+------------------
304+
305+In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is
306+defined like this:
307+
308+.. code-block:: idris
309+
310+ ||| Sequence two grammars. If either consumes some input, the sequence is
311+ ||| guaranteed to consume some input. If the first one consumes input, the
312+ ||| second is allowed to be recursive (because it means some input has been
313+ ||| consumed and therefore the input is smaller)
314+ export %inline
315+ (>>=) : {c1 : Bool} ->
316+ Grammar tok c1 a ->
317+ inf c1 (a -> Grammar tok c2 b) ->
318+ Grammar tok (c1 || c2) b
319+ (>>=) {c1 = False} = SeqEmpty
320+ (>>=) {c1 = True} = SeqEat
321+
322+.. list-table::
323+
324+ * - This allows us to use ``do`` notation for the previous parenthesis example:
325+
326+ - .. code-block:: idris
327+
328+ expr = intLiteral <|> do
329+ openParen
330+ r <- expr
331+ closeParen
332+ pure r
333+
334+This can be more flexible than using the ``<*>`` operator. Also it is defined
335+using ``Inf`` so we can implement recursively defined grammars as above.
336+
337+Implementing the Arithmetic Operators
338+-------------------------------------
339+
276340.. list-table::
277341
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:
342+ * - Now for the operations, in this case: ``+``, ``-`` and ``*``.
343+ The syntax we require for these infix operators
344+ would require recursive grammars like this:
281345
282346 - .. code-block:: idris
283347
284− expr = (add expr (op "+") expr)
348+ expr = expr (op "+") expr
349+
350+As already explained, ``do`` notation can allow us to use recursive
351+definitions but not necessarily left-recursion like this.
285352
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
353+In order to work up to this gradually lets start with prefix operators
288354(sometimes known as Polish notation) then modify later for infix operators.
289355
290356.. list-table::
@@ -295,7 +361,7 @@ In order to work up to this gradually I will start with prefix operators
295361
296362 expr = (add (op "+") expr expr)
297363
298−where 'op' is defined like this:
364+where ``op`` is defined like this:
299365
300366.. code-block:: idris
301367
@@ -308,7 +374,13 @@ where 'op' is defined like this:
308374
309375.. list-table::
310376
311− * - and 'add' is defined like this:
377+ * - and ``add`` is defined like this:
378+
379+ Where:
380+
381+ - x is the add operator.
382+ - y is the first operand.
383+ - z is the second operand.
312384
313385 - .. code-block:: idris
314386
@@ -322,40 +394,37 @@ where 'op' is defined like this:
322394 Grammar tok ((c1 || c2) || c3) Integer
323395 add x y z = map addInt (x *> y) <*> z
324396
325−Where:
326397
327−- x is the add operator.
328−- y is the first operand.
329−- z is the second operand.
330398
331399The resulting integer will be the sum of the two operands.
332400
333−The other operators are defined in a similar way:
401+.. list-table::
334402
335−.. code-block:: idris
403+ * - The other operators are defined in a similar way:
336404
337− subInt : Integer -> Integer -> Integer
338− subInt a b = a-b
405+ - .. code-block:: idris
339406
340− export
341− sub : Grammar tok c1 Integer ->
342− Grammar tok c2 Integer ->
343− Grammar tok c3 Integer ->
344− Grammar tok ((c1 || c2) || c3) Integer
345− sub x y z = map subInt (x *> y) <*> z
407+ subInt : Integer -> Integer -> Integer
408+ subInt a b = a-b
346409
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
347416
348− multInt : Integer -> Integer -> Integer
349− multInt a b = a*b
417+ multInt : Integer -> Integer -> Integer
418+ multInt a b = a*b
350419
351− export
352− mult : Grammar tok c1 Integer ->
353− Grammar tok c2 Integer ->
354− Grammar tok c3 Integer ->
355− Grammar tok ((c1 || c2) || c3) Integer
356− 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
357426
358−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
359428partial as it is a potentially infinite structure and so not total.
360429
361430.. code-block:: idris
@@ -408,7 +477,7 @@ Then an invalid syntax:
408477 List (TokenData ExpressionToken))
409478
410479However if we try something that is invalid, but starts with a valid token,
411−then it will return 'Right' (to indicate success)
480+then it will return ``Right`` (to indicate success)
412481
413482.. code-block:: idris
414483
@@ -435,8 +504,8 @@ Infix Notation
435504--------------
436505
437506So far we have implemented a prefix notation for operators (like this:
438−'+ expr expr') but the aim is to implemented an infix notation (like this:
439−'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
440509infinite data structures (see Codata Types here :ref:`sect-typefuns`).
441510
442511First alter the grammar to have infix operations:
@@ -494,10 +563,10 @@ If we have a rule like this:
494563
495564 A -> (x<*>y) <|> (x<*>z)
496565
497−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has
498−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.
499568
500−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
501570so that, if the first token succeeds but the following tokens fail, then the
502571first tokens would not be consumed.
503572
@@ -524,52 +593,64 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although
524593not every context-free grammar can be converted to a LL(1) grammar.
525594
526595This still does not solve the infinite recursion issue and there is another
527−problem: the precedence of the operators +, - and * is not explicit.
596+problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.
528597
529−To resolve this we can alter the example like this:
530−
531−.. code-block:: idris
598+.. list-table::
532599
533− paren : Rule Integer -> Rule Integer
534− paren exp = openParen *> exp <* closeParen
600+ * - To resolve this we can alter the example to have a BNF like this:
601+ Where braces ``{ ... }`` mean the contents can occur 1 or more times.
535602
536− addInt : Integer -> Integer -> Integer
537− addInt a b = a+b
603+ - .. code-block:: idris
538604
539− subInt : Integer -> Integer -> Integer
540− subInt a b = a-b
605+ 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}
541606
542− multInt : Integer -> Integer -> Integer
543− multInt a b = a*b
607+ 'term' ::= 'factor' {'*' 'factor'}
544608
545− partial
546− expr : Rule Integer
609+ 'factor' ::=
610+ number
611+ | '(' 'expression' ')'
547612
548− partial
549− exprAtom : Rule Integer
550− exprAtom = intLiteral <|> (paren expr)
551613
552− partial
553− expr1 : Rule Integer
554− expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)
614+.. code-block:: idris
555615
556− partial
557− exprMult : Rule Integer
558− exprMult = expr1 <|> exprAtom
616+ expr : Rule Integer
559617
560− partial
561− expr2 : Rule Integer
562− expr2 = map addInt exprMult <*> ((op "+") *> exprMult)
618+ factor : Rule Integer
619+ factor = intLiteral <|> do
620+ openParen
621+ r <- expr
622+ closeParen
623+ pure r
624+
625+ term : Rule Integer
626+ term = map multInt factor <*> (
627+ (op "*")
628+ *> factor)
629+ <|> factor
630+
631+ expr = map addInt term <*> (
632+ (op "+")
633+ *> term)
634+ <|> map subInt term <*> (
635+ (op "-")
636+ *> term)
637+ <|> term
638+
639+ calc : String -> Either (ParseError (TokenData ExpressionToken))
640+ (Integer, List (TokenData ExpressionToken))
641+ calc s = parse expr (fst (lex expressionTokens s))
563642
564− partial
565− exprAdd : Rule Integer
566− exprAdd = expr2 <|> exprMult
643+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()
644+ lft (Error s lst) = putStrLn ("error:"++s)
567645
568− partial
569− expr3 : Rule Integer
570− expr3 = map subInt exprAdd <*> ((op "-") *> expr)
646+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
647+ rht i = putStrLn ("right " ++ (show i))
571648
572− expr = expr3 <|> exprAdd
649+ main : IO ()
650+ main = do
651+ putStr "alg>"
652+ x <- getLine
653+ either lft rht (calc x) -- eliminator for Either
573654
574655As the following tests show, this now handles infix operators and precedence.
575656
@@ -579,44 +660,41 @@ As the following tests show, this now handles infix operators and precedence.
579660
580661 - .. code-block:: idris
581662
582− *parserExInfix> test "2*3"
583− Right (6,
584− []) : Either (ParseError (TokenData ExpressionToken))
585− (Integer, List (TokenData ExpressionToken))
663+ *algebraREPL> :exec
664+ alg>2*3
665+ right (6, [])
586666
587667 * - Check that atomic number literals work:
588668
589669 - .. code-block:: idris
590670
591− *parserExInfix> test "2"
592− Right (2,
593− []) : Either (ParseError (TokenData ExpressionToken))
594− (Integer, List (TokenData ExpressionToken))
671+ *algebraREPL> :exec
672+ alg>2
673+ right (2, [])
595674
596675 * - Check that '*' has a higher precedence than '+'.
597676
598677 - .. code-block:: idris
599678
600− *parserExInfix> test "2+3*4"
601− Right (14,
602− []) : Either (ParseError (TokenData ExpressionToken))
603− (Integer, List (TokenData ExpressionToken))
679+ *algebraREPL> :exec
680+ alg>2+3*4
681+ right (14, [])
604682
605683 * - Also '*' has a higher precedence than '+' when the order is reversed.
606684
607685 - .. code-block:: idris
608686
609− *parserExInfix> test "3*4+2"
610− Right (14,
611− []) : Either (ParseError (TokenData ExpressionToken))
612− (Integer, List (TokenData ExpressionToken))
687+ *algebraREPL> :exec
688+ alg>3*4+2
689+ right (14, [])
613690
614691 * - Also precedence can be overridden by parenthesis.
615692
616693 - .. code-block:: idris
617694
618− *parserExInfix> test "(2+3)*4"
619− Right (20,
620− []) : Either (ParseError (TokenData ExpressionToken))
621− (Integer, List (TokenData ExpressionToken))
695+ *algebraREPL> :exec
696+ alg>(2+3)*4
697+ right (20, [])
622698
699+This is still not correct because it does not correctly parse multiple sums or terms
700+like ``1+2+3`` or ``1*2*3``.