@@ -3,8 +3,8 @@
33Parser
44======
55
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).
6+To run our parser we call 'parse'. This requires a Grammar and the output
7+from the lexer (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``.
56+So an example of a Grammer type may look something like this:
57+'Grammar (TokenData ExpressionToken) True Integer'.
58+
5859This is a complicated type name and a given parser will need to use it a lot.
5960So to reduce the amount of typing we can use the following type synonym (similar
6061to what is done in Idris 2
6162: 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 add a parser for this running example.
74+this page we will go on to implement a parser for this running example.
7575
7676.. list-table::
7777
78− * - The syntax we are aiming at is something
79− like this (expressed in Backus–Naur form (BNF)):
78+ * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
79+ like this:
8080 - .. code-block:: idris
8181
8282 <expr> ::= <integer literal>
@@ -89,8 +89,8 @@ 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
93− sequence of numeric characters).
92+ * - To start, here is a Grammar to parse an integer literal (that is, a
93+ sequence of numbers).
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`` (zero) is used as
177+Integer value is not really relevant for parenthesis so '0' is used as
178178a default value.
179179
180−As before, this can be tested with a function like this:
180+As before, we can test this out 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, as
217−required, other token lists are not:
216+We can see below that '(' followed by a number is successfully parsed but other
217+token lists are not:
218218
219219.. code-block:: idris
220220
@@ -270,87 +270,21 @@ required, other 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−
340276.. list-table::
341277
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:
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:
345281
346282 - .. code-block:: idris
347283
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.
284+ expr = (add expr (op "+") expr)
352285
353−In order to work up to this gradually lets start with prefix operators
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
354288(sometimes known as Polish notation) then modify later for infix operators.
355289
356290.. list-table::
@@ -361,7 +295,7 @@ In order to work up to this gradually lets start with prefix operators
361295
362296 expr = (add (op "+") expr expr)
363297
364−where ``op`` is defined like this:
298+where 'op' is defined like this:
365299
366300.. code-block:: idris
367301
@@ -374,13 +308,7 @@ where ``op`` is defined like this:
374308
375309.. list-table::
376310
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.
311+ * - and 'add' is defined like this:
384312
385313 - .. code-block:: idris
386314
@@ -394,37 +322,40 @@ where ``op`` is defined like this:
394322 Grammar tok ((c1 || c2) || c3) Integer
395323 add x y z = map addInt (x *> y) <*> z
396324
325+Where:
397326
327+- x is the add operator.
328+- y is the first operand.
329+- z is the second operand.
398330
399331The resulting integer will be the sum of the two operands.
400332
401−.. list-table::
333+The other operators are defined in a similar way:
402334
403− * - The other operators are defined in a similar way:
335+.. code-block:: idris
404336
405− - .. code-block:: idris
337+ subInt : Integer -> Integer -> Integer
338+ subInt a b = a-b
406339
407− subInt : Integer -> Integer -> Integer
408− subInt a b = a-b
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
409346
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
416347
417− multInt : Integer -> Integer -> Integer
418− multInt a b = a*b
348+ multInt : Integer -> Integer -> Integer
349+ multInt a b = a*b
419350
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
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
426357
427−So the top level ``Grammar`` can now be defined as follows. Note that this is
358+So the top level Grammar can now be defined as follows. Note that this is
428359partial as it is a potentially infinite structure and so not total.
429360
430361.. code-block:: idris
@@ -477,7 +408,7 @@ Then an invalid syntax:
477408 List (TokenData ExpressionToken))
478409
479410However if we try something that is invalid, but starts with a valid token,
480−then it will return ``Right`` (to indicate success)
411+then it will return 'Right' (to indicate success)
481412
482413.. code-block:: idris
483414
@@ -504,8 +435,8 @@ Infix Notation
504435--------------
505436
506437So far we have implemented a prefix notation for operators (like this:
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
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
509440infinite data structures (see Codata Types here :ref:`sect-typefuns`).
510441
511442First alter the grammar to have infix operations:
@@ -563,10 +494,10 @@ If we have a rule like this:
563494
564495 A -> (x<*>y) <|> (x<*>z)
565496
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.
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.
568499
569−so we could write code to backtrack. That is ``try`` ``x<*>y`` without consuming
500+so we could write code to backtrack. That is 'try' 'x<*>y' without consuming
570501so that, if the first token succeeds but the following tokens fail, then the
571502first tokens would not be consumed.
572503
@@ -593,64 +524,52 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although
593524not every context-free grammar can be converted to a LL(1) grammar.
594525
595526This still does not solve the infinite recursion issue and there is another
596−problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.
527+problem: the precedence of the operators +, - and * is not explicit.
597528
598−.. list-table::
529+To resolve this we can alter the example like this:
599530
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.
531+.. code-block:: idris
602532
603− - .. code-block:: idris
533+ paren : Rule Integer -> Rule Integer
534+ paren exp = openParen *> exp <* closeParen
535+
536+ addInt : Integer -> Integer -> Integer
537+ addInt a b = a+b
604538
605− 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}
539+ subInt : Integer -> Integer -> Integer
540+ subInt a b = a-b
606541
607− 'term' ::= 'factor' {'*' 'factor'}
542+ multInt : Integer -> Integer -> Integer
543+ multInt a b = a*b
608544
609− 'factor' ::=
610− number
611− | '(' 'expression' ')'
545+ partial
546+ expr : Rule Integer
612547
548+ partial
549+ exprAtom : Rule Integer
550+ exprAtom = intLiteral <|> (paren expr)
613551
614−.. code-block:: idris
552+ partial
553+ expr1 : Rule Integer
554+ expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)
615555
616− expr : Rule Integer
556+ partial
557+ exprMult : Rule Integer
558+ exprMult = expr1 <|> exprAtom
617559
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))
560+ partial
561+ expr2 : Rule Integer
562+ expr2 = map addInt exprMult <*> ((op "+") *> exprMult)
642563
643− lft : (ParseError (TokenData ExpressionToken)) -> IO ()
644− lft (Error s lst) = putStrLn ("error:"++s)
564+ partial
565+ exprAdd : Rule Integer
566+ exprAdd = expr2 <|> exprMult
645567
646− rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
647− rht i = putStrLn ("right " ++ (show i))
568+ partial
569+ expr3 : Rule Integer
570+ expr3 = map subInt exprAdd <*> ((op "-") *> expr)
648571
649− main : IO ()
650− main = do
651− putStr "alg>"
652− x <- getLine
653− either lft rht (calc x) -- eliminator for Either
572+ expr = expr3 <|> exprAdd
654573
655574As the following tests show, this now handles infix operators and precedence.
656575
@@ -660,41 +579,44 @@ As the following tests show, this now handles infix operators and precedence.
660579
661580 - .. code-block:: idris
662581
663− *algebraREPL> :exec
664− alg>2*3
665− right (6, [])
582+ *parserExInfix> test "2*3"
583+ Right (6,
584+ []) : Either (ParseError (TokenData ExpressionToken))
585+ (Integer, List (TokenData ExpressionToken))
666586
667587 * - Check that atomic number literals work:
668588
669589 - .. code-block:: idris
670590
671− *algebraREPL> :exec
672− alg>2
673− right (2, [])
591+ *parserExInfix> test "2"
592+ Right (2,
593+ []) : Either (ParseError (TokenData ExpressionToken))
594+ (Integer, List (TokenData ExpressionToken))
674595
675596 * - Check that '*' has a higher precedence than '+'.
676597
677598 - .. code-block:: idris
678599
679− *algebraREPL> :exec
680− alg>2+3*4
681− right (14, [])
600+ *parserExInfix> test "2+3*4"
601+ Right (14,
602+ []) : Either (ParseError (TokenData ExpressionToken))
603+ (Integer, List (TokenData ExpressionToken))
682604
683605 * - Also '*' has a higher precedence than '+' when the order is reversed.
684606
685607 - .. code-block:: idris
686608
687− *algebraREPL> :exec
688− alg>3*4+2
689− right (14, [])
609+ *parserExInfix> test "3*4+2"
610+ Right (14,
611+ []) : Either (ParseError (TokenData ExpressionToken))
612+ (Integer, List (TokenData ExpressionToken))
690613
691614 * - Also precedence can be overridden by parenthesis.
692615
693616 - .. code-block:: idris
694617
695− *algebraREPL> :exec
696− alg>(2+3)*4
697− right (20, [])
618+ *parserExInfix> test "(2+3)*4"
619+ Right (20,
620+ []) : Either (ParseError (TokenData ExpressionToken))
621+ (Integer, List (TokenData ExpressionToken))
698622
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``.