@@ -3,8 +3,8 @@
6−To run our 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
7−from the lexer (a list of tokens).
7+from the lexer (which is a list of tokens).
9.. code-block:: idris
9.. code-block:: idris
@@ -18,13 +18,13 @@ If successful this returns 'Right' with a pair of
19otherwise it returns 'Left' with the error message.
19otherwise it returns 'Left' with the error message.
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
22'Grammar' data structure. This is a combinator structure, similar in principle
22'Grammar' data structure. This is a combinator structure, similar in principle
23to the recogniser combinator for the lexer, which was discussed on the
23to the recogniser combinator for the lexer, which was discussed on the
24previous page.
24previous page.
26−As with the Recogniser the Grammar type is dependent on a boolean 'consumes'
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
27+value which allows us to ensure that complicated ``Grammar`` structures will always
28consume input.
28consume input.
30.. code-block:: idris
30.. code-block:: idris
@@ -53,13 +53,13 @@ consume input.
53 Grammar tok c1 ty -> Grammar tok c2 ty ->
53 Grammar tok c1 ty -> Grammar tok c2 ty ->
54 Grammar tok (c1 && c2) ty
54 Grammar tok (c1 && c2) ty
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:
57−'Grammar (TokenData ExpressionToken) True Integer'.
57+``Grammar (TokenData ExpressionToken) True Integer``.
59This is a complicated type name and a given parser will need to use it a lot.
58This is a complicated type name and a given parser will need to use it a lot.
60So to reduce the amount of typing we can use the following type synonym (similar
59So to reduce the amount of typing we can use the following type synonym (similar
61to what is done in Idris 2
60to what is done in Idris 2
62: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
61: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
64.. code-block:: idris
64.. code-block:: idris
@@ -71,12 +71,12 @@ Parser Example
71--------------
71--------------
73On the previous page we implemented a lexer to 'lex' a very simple expression, on
73On 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.
76.. list-table::
76.. list-table::
78− * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
78+ * - The syntax we are aiming at is something
79− like this:
79+ like this (expressed in Backus–Naur form (BNF)):
80 - .. code-block:: idris
80 - .. code-block:: idris
82 <expr> ::= <integer literal>
82 <expr> ::= <integer literal>
@@ -89,8 +89,8 @@ this page we will go on to implement a parser for this running example.
90.. list-table::
90.. list-table::
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
93− sequence of numbers).
93+ sequence of numeric characters).
95 - .. code-block:: idris
95 - .. code-block:: idris
@@ -144,7 +144,7 @@ successful, this is because we are not specifically checking for end-of-file.
145.. list-table::
145.. list-table::
147− * - The 'intLiteral' function above uses the 'terminal' function to
147+ * - The ``intLiteral`` function above uses the ``terminal`` function to
148 construct the grammar
148 construct the grammar
149 - .. code-block:: idris
149 - .. code-block:: idris
@@ -174,10 +174,10 @@ Idris 2 uses a slightly different version which stores an error message like
174 OParen => Just 0
174 OParen => Just 0
175 _ => Nothing)
175 _ => Nothing)
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
178a default value.
178a default value.
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:
182.. code-block:: idris
182.. code-block:: idris
@@ -202,10 +202,10 @@ error for anything else:
202 List (TokenData ExpressionToken))
202 List (TokenData ExpressionToken))
204Now we have two Grammars we can try combining them. The following test looks
204Now 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
205+for ``openParen`` followed by ``intLiteral``, the two Grammars are combined using
206−'<*>'. The 'map const' part uses the integer value from the first.
206+``<*>``. The ``map const`` part uses the integer value from the first.
208−The following test is looking for '(' followed by a number:
208+The following test is looking for ``(`` followed by a number:
210.. code-block:: idris
210.. code-block:: idris
@@ -213,8 +213,8 @@ The following test is looking for '(' followed by a number:
213 (Integer, List (TokenData ExpressionToken))
213 (Integer, List (TokenData ExpressionToken))
214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
216−We can see below that '(' followed by a number is successfully parsed but other
216+We can see below that ``(`` followed by a number is successfully parsed but, as
217−token lists are not:
217+required, other token lists are not:
219.. code-block:: idris
219.. code-block:: idris
@@ -270,21 +270,87 @@ token lists are not:
270 paren : Rule Integer -> Rule Integer
270 paren : Rule Integer -> Rule Integer
271 paren exp = openParen *> exp <* closeParen
271 paren exp = openParen *> exp <* closeParen
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
274value from the inner expression.
274value from the inner expression.
276+So lets try to use this to define a grammar which recognises either:
279+- An integer literal inside parenthesis
280+- An integer literal inside parenthesis inside parenthesis
285+ * - This requires a recursively defined structure like this:
287+ - .. code-block:: idris
291+ expr = intLiteral <|> (paren expr)
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``.
299+So a better method is to use ``do`` notation as described in the following
305+In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is
308+.. code-block:: idris
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)
315+ (>>=) : {c1 : Bool} ->
317+ inf c1 (a -> Grammar tok c2 b) ->
318+ Grammar tok (c1 || c2) b
319+ (>>=) {c1 = False} = SeqEmpty
320+ (>>=) {c1 = True} = SeqEat
324+ * - This allows us to use ``do`` notation for the previous parenthesis example:
326+ - .. code-block:: idris
328+ expr = intLiteral <|> do
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.
337+Implementing the Arithmetic Operators
338+-------------------------------------
276.. list-table::
340.. list-table::
278− * - Now for the operations, in this case: '+', '-' and '*'.
342+ * - Now for the operations, in this case: ``+``, ``-`` and ``*``.
279− The syntax we require is that operators like '+' are infix operators, which
343+ The syntax we require for these infix operators
280− would require a definition like this:
344+ would require recursive grammars like this:
282 - .. code-block:: idris
346 - .. code-block:: idris
284− expr = (add expr (op "+") expr)
348+ expr = expr (op "+") expr
350+As already explained, ``do`` notation can allow us to use recursive
351+definitions but not necessarily left-recursion like this.
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
288(sometimes known as Polish notation) then modify later for infix operators.
354(sometimes known as Polish notation) then modify later for infix operators.
290.. list-table::
356.. list-table::
@@ -295,7 +361,7 @@ In order to work up to this gradually I will start with prefix operators
296 expr = (add (op "+") expr expr)
362 expr = (add (op "+") expr expr)
298−where 'op' is defined like this:
364+where ``op`` is defined like this:
300.. code-block:: idris
366.. code-block:: idris
@@ -308,7 +374,13 @@ where 'op' is defined like this:
309.. list-table::
375.. list-table::
311− * - and 'add' is defined like this:
377+ * - and ``add`` is defined like this:
381+ - x is the add operator.
382+ - y is the first operand.
383+ - z is the second operand.
313 - .. code-block:: idris
385 - .. code-block:: idris
@@ -322,40 +394,37 @@ where 'op' is defined like this:
322 Grammar tok ((c1 || c2) || c3) Integer
394 Grammar tok ((c1 || c2) || c3) Integer
323 add x y z = map addInt (x *> y) <*> z
395 add x y z = map addInt (x *> y) <*> z
327−- x is the add operator.
328−- y is the first operand.
329−- z is the second operand.
331The resulting integer will be the sum of the two operands.
399The resulting integer will be the sum of the two operands.
333−The other operators are defined in a similar way:
401+.. list-table::
335−.. code-block:: idris
403+ * - The other operators are defined in a similar way:
337− subInt : Integer -> Integer -> Integer
405+ - .. code-block:: idris
340− export
407+ subInt : Integer -> Integer -> Integer
341− sub : Grammar tok c1 Integer ->
408+ subInt a b = a-b
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
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
348− multInt : Integer -> Integer -> Integer
417+ multInt : Integer -> Integer -> Integer
349− multInt a b = a*b
418+ multInt a b = a*b
352− mult : Grammar tok c1 Integer ->
421+ mult : Grammar tok c1 Integer ->
353− Grammar tok c2 Integer ->
422+ Grammar tok c2 Integer ->
354− Grammar tok c3 Integer ->
423+ Grammar tok c3 Integer ->
355− Grammar tok ((c1 || c2) || c3) Integer
424+ Grammar tok ((c1 || c2) || c3) Integer
356− mult x y z = map multInt (x *> y) <*> z
425+ mult x y z = map multInt (x *> y) <*> z
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
359partial as it is a potentially infinite structure and so not total.
428partial as it is a potentially infinite structure and so not total.
361.. code-block:: idris
430.. code-block:: idris
@@ -408,7 +477,7 @@ Then an invalid syntax:
408 List (TokenData ExpressionToken))
477 List (TokenData ExpressionToken))
410However if we try something that is invalid, but starts with a valid token,
479However 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)
413.. code-block:: idris
482.. code-block:: idris
@@ -435,8 +504,8 @@ Infix Notation
435--------------
504--------------
437So far we have implemented a prefix notation for operators (like this:
506So 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:
507+``+ 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
508+``expr + expr``). To do this we must be able to deal with potentially
440infinite data structures (see Codata Types here :ref:`sect-typefuns`).
509infinite data structures (see Codata Types here :ref:`sect-typefuns`).
442First alter the grammar to have infix operations:
511First alter the grammar to have infix operations:
@@ -494,10 +563,10 @@ If we have a rule like this:
495 A -> (x<*>y) <|> (x<*>z)
564 A -> (x<*>y) <|> (x<*>z)
497−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has
566+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.
567+already consumed ``x``, so now ``x<*>z`` will fail.
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
501so that, if the first token succeeds but the following tokens fail, then the
570so that, if the first token succeeds but the following tokens fail, then the
502first tokens would not be consumed.
571first tokens would not be consumed.
@@ -524,52 +593,64 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although
524not every context-free grammar can be converted to a LL(1) grammar.
593not every context-free grammar can be converted to a LL(1) grammar.
526This still does not solve the infinite recursion issue and there is another
595This 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.
529−To resolve this we can alter the example like this:
598+.. list-table::
531−.. code-block:: idris
533− paren : Rule Integer -> Rule Integer
600+ * - To resolve this we can alter the example to have a BNF like this:
534− paren exp = openParen *> exp <* closeParen
601+ Where braces ``{ ... }`` mean the contents can occur 1 or more times.
536− addInt : Integer -> Integer -> Integer
603+ - .. code-block:: idris
539− subInt : Integer -> Integer -> Integer
605+ 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}
542− multInt : Integer -> Integer -> Integer
607+ 'term' ::= 'factor' {'*' 'factor'}
545− partial
609+ 'factor' ::=
546− expr : Rule Integer
610+ number
611+ | '(' 'expression' ')'
549− exprAtom : Rule Integer
550− exprAtom = intLiteral <|> (paren expr)
552− partial
614+.. code-block:: idris
553− expr1 : Rule Integer
554− expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)
557− exprMult : Rule Integer
616+ expr : Rule Integer
558− exprMult = expr1 <|> exprAtom
560− partial
618+ factor : Rule Integer
619+ factor = intLiteral <|> do
561− expr2 : Rule Integer
625+ term : Rule Integer
562− expr2 = map addInt exprMult <*> ((op "+") *> exprMult)
626+ term = map multInt factor <*> (
631+ expr = map addInt term <*> (
634+ <|> map subInt term <*> (
639+ calc : String -> Either (ParseError (TokenData ExpressionToken))
640+ (Integer, List (TokenData ExpressionToken))
641+ calc s = parse expr (fst (lex expressionTokens s))
564− partial
643+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()
565− exprAdd : Rule Integer
644+ lft (Error s lst) = putStrLn ("error:"++s)
566− exprAdd = expr2 <|> exprMult
568− partial
646+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
569− expr3 : Rule Integer
647+ rht i = putStrLn ("right " ++ (show i))
570− expr3 = map subInt exprAdd <*> ((op "-") *> expr)
572− expr = expr3 <|> exprAdd
649+ main : IO ()
653+ either lft rht (calc x) -- eliminator for Either
574As the following tests show, this now handles infix operators and precedence.
655As the following tests show, this now handles infix operators and precedence.
@@ -579,44 +660,41 @@ As the following tests show, this now handles infix operators and precedence.
580 - .. code-block:: idris
661 - .. code-block:: idris
582− *parserExInfix> test "2*3"
663+ *algebraREPL> :exec
583− Right (6,
664+ alg>2*3
584− []) : Either (ParseError (TokenData ExpressionToken))
665+ right (6, [])
585− (Integer, List (TokenData ExpressionToken))
587 * - Check that atomic number literals work:
667 * - Check that atomic number literals work:
589 - .. code-block:: idris
669 - .. code-block:: idris
591− *parserExInfix> test "2"
671+ *algebraREPL> :exec
593− []) : Either (ParseError (TokenData ExpressionToken))
673+ right (2, [])
594− (Integer, List (TokenData ExpressionToken))
596 * - Check that '*' has a higher precedence than '+'.
675 * - Check that '*' has a higher precedence than '+'.
598 - .. code-block:: idris
677 - .. code-block:: idris
600− *parserExInfix> test "2+3*4"
679+ *algebraREPL> :exec
601− Right (14,
680+ alg>2+3*4
602− []) : Either (ParseError (TokenData ExpressionToken))
681+ right (14, [])
603− (Integer, List (TokenData ExpressionToken))
605 * - Also '*' has a higher precedence than '+' when the order is reversed.
683 * - Also '*' has a higher precedence than '+' when the order is reversed.
607 - .. code-block:: idris
685 - .. code-block:: idris
609− *parserExInfix> test "3*4+2"
687+ *algebraREPL> :exec
610− Right (14,
688+ alg>3*4+2
611− []) : Either (ParseError (TokenData ExpressionToken))
689+ right (14, [])
612− (Integer, List (TokenData ExpressionToken))
614 * - Also precedence can be overridden by parenthesis.
691 * - Also precedence can be overridden by parenthesis.
616 - .. code-block:: idris
693 - .. code-block:: idris
618− *parserExInfix> test "(2+3)*4"
695+ *algebraREPL> :exec
619− Right (20,
696+ alg>(2+3)*4
620− []) : Either (ParseError (TokenData ExpressionToken))
697+ right (20, [])
621− (Integer, List (TokenData ExpressionToken))
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``.