@@ -3,8 +3,8 @@
6−To run the parser we call ``parse``. This requires a grammar and the output
6+To run our parser we call 'parse'. This requires a Grammar and the output
7−from the lexer (which is a list of tokens).
7+from the lexer (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'.
58This is a complicated type name and a given parser will need to use it a lot.
59This is a complicated type name and a given parser will need to use it a lot.
59So to reduce the amount of typing we can use the following type synonym (similar
60So to reduce the amount of typing we can use the following type synonym (similar
60to what is done in Idris 2
61to what is done in Idris 2
61: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
62: 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 add a parser for this running example.
74+this page we will go on to implement a parser for this running example.
76.. list-table::
76.. list-table::
78− * - The syntax we are aiming at is something
78+ * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
79− like this (expressed in Backus–Naur form (BNF)):
79+ like this:
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 add 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 numeric characters).
93+ sequence of numbers).
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`` (zero) is used as
177+Integer value is not really relevant for parenthesis so '0' is used as
178a default value.
178a default value.
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:
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, as
216+We can see below that '(' followed by a number is successfully parsed but other
217−required, other token lists are not:
217+token lists are not:
219.. code-block:: idris
219.. code-block:: idris
@@ -270,87 +270,21 @@ required, other 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−-------------------------------------
340.. list-table::
276.. list-table::
342− * - Now for the operations, in this case: ``+``, ``-`` and ``*``.
278+ * - Now for the operations, in this case: '+', '-' and '*'.
343− The syntax we require for these infix operators
279+ The syntax we require is that operators like '+' are infix operators, which
344− would require recursive grammars like this:
280+ would require a definition like this:
346 - .. code-block:: idris
282 - .. code-block:: idris
348− expr = expr (op "+") expr
284+ expr = (add 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.
353−In order to work up to this gradually lets start with prefix operators
287+In order to work up to this gradually I will start with prefix operators
354(sometimes known as Polish notation) then modify later for infix operators.
288(sometimes known as Polish notation) then modify later for infix operators.
356.. list-table::
290.. list-table::
@@ -361,7 +295,7 @@ In order to work up to this gradually lets start with prefix operators
362 expr = (add (op "+") expr expr)
296 expr = (add (op "+") expr expr)
364−where ``op`` is defined like this:
298+where 'op' is defined like this:
366.. code-block:: idris
300.. code-block:: idris
@@ -374,13 +308,7 @@ where ``op`` is defined like this:
375.. list-table::
309.. list-table::
377− * - and ``add`` is defined like this:
311+ * - and 'add' is defined like this:
381− - x is the add operator.
382− - y is the first operand.
383− - z is the second operand.
385 - .. code-block:: idris
313 - .. code-block:: idris
@@ -394,37 +322,40 @@ where ``op`` is defined like this:
394 Grammar tok ((c1 || c2) || c3) Integer
322 Grammar tok ((c1 || c2) || c3) Integer
395 add x y z = map addInt (x *> y) <*> z
323 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.
399The resulting integer will be the sum of the two operands.
331The resulting integer will be the sum of the two operands.
401−.. list-table::
333+The other operators are defined in a similar way:
403− * - The other operators are defined in a similar way:
335+.. code-block:: idris
405− - .. code-block:: idris
337+ subInt : Integer -> Integer -> Integer
407− subInt : Integer -> Integer -> Integer
340+ export
408− subInt a b = a-b
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
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
417− multInt : Integer -> Integer -> Integer
348+ multInt : Integer -> Integer -> Integer
418− multInt a b = a*b
349+ multInt a b = a*b
421− mult : Grammar tok c1 Integer ->
352+ mult : Grammar tok c1 Integer ->
422− Grammar tok c2 Integer ->
353+ Grammar tok c2 Integer ->
423− Grammar tok c3 Integer ->
354+ Grammar tok c3 Integer ->
424− Grammar tok ((c1 || c2) || c3) Integer
355+ Grammar tok ((c1 || c2) || c3) Integer
425− mult x y z = map multInt (x *> y) <*> z
356+ mult x y z = map multInt (x *> y) <*> z
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
428partial as it is a potentially infinite structure and so not total.
359partial as it is a potentially infinite structure and so not total.
430.. code-block:: idris
361.. code-block:: idris
@@ -477,7 +408,7 @@ Then an invalid syntax:
477 List (TokenData ExpressionToken))
408 List (TokenData ExpressionToken))
479However if we try something that is invalid, but starts with a valid token,
410However 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)
482.. code-block:: idris
413.. code-block:: idris
@@ -504,8 +435,8 @@ Infix Notation
504--------------
435--------------
506So far we have implemented a prefix notation for operators (like this:
437So 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:
438+'+ 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
439+'expr + expr'). To do this we must be able to deal with potentially
509infinite data structures (see Codata Types here :ref:`sect-typefuns`).
440infinite data structures (see Codata Types here :ref:`sect-typefuns`).
511First alter the grammar to have infix operations:
442First alter the grammar to have infix operations:
@@ -563,10 +494,10 @@ If we have a rule like this:
564 A -> (x<*>y) <|> (x<*>z)
495 A -> (x<*>y) <|> (x<*>z)
566−If ``x<*>y`` fails but ``x<*>z`` would succeed a problem is that, ``x<*>y`` has
497+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.
498+already consumed 'x', so now 'x<*>z' will fail.
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
570so that, if the first token succeeds but the following tokens fail, then the
501so that, if the first token succeeds but the following tokens fail, then the
571first tokens would not be consumed.
502first tokens would not be consumed.
@@ -593,64 +524,52 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although
593not every context-free grammar can be converted to a LL(1) grammar.
524not every context-free grammar can be converted to a LL(1) grammar.
595This still does not solve the infinite recursion issue and there is another
526This 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.
598−.. list-table::
529+To resolve this we can alter the example like this:
600− * - To resolve this we can alter the example to have a BNF like this:
531+.. code-block:: idris
601− Where braces ``{ ... }`` mean the contents can occur 1 or more times.
603− - .. code-block:: idris
533+ paren : Rule Integer -> Rule Integer
534+ paren exp = openParen *> exp <* closeParen
536+ addInt : Integer -> Integer -> Integer
605− 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}
539+ subInt : Integer -> Integer -> Integer
607− 'term' ::= 'factor' {'*' 'factor'}
542+ multInt : Integer -> Integer -> Integer
609− 'factor' ::=
545+ partial
610− number
546+ expr : Rule Integer
611− | '(' 'expression' ')'
549+ exprAtom : Rule Integer
550+ exprAtom = intLiteral <|> (paren expr)
614−.. code-block:: idris
552+ partial
553+ expr1 : Rule Integer
554+ expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)
616− expr : Rule Integer
557+ exprMult : Rule Integer
558+ exprMult = expr1 <|> exprAtom
618− factor : Rule Integer
560+ partial
619− factor = intLiteral <|> do
625− term : Rule Integer
561+ expr2 : Rule Integer
626− term = map multInt factor <*> (
562+ expr2 = map addInt exprMult <*> ((op "+") *> exprMult)
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))
643− lft : (ParseError (TokenData ExpressionToken)) -> IO ()
564+ partial
644− lft (Error s lst) = putStrLn ("error:"++s)
565+ exprAdd : Rule Integer
566+ exprAdd = expr2 <|> exprMult
646− rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
568+ partial
647− rht i = putStrLn ("right " ++ (show i))
569+ expr3 : Rule Integer
570+ expr3 = map subInt exprAdd <*> ((op "-") *> expr)
649− main : IO ()
572+ expr = expr3 <|> exprAdd
653− either lft rht (calc x) -- eliminator for Either
655As the following tests show, this now handles infix operators and precedence.
574As the following tests show, this now handles infix operators and precedence.
@@ -660,41 +579,44 @@ As the following tests show, this now handles infix operators and precedence.
661 - .. code-block:: idris
580 - .. code-block:: idris
663− *algebraREPL> :exec
582+ *parserExInfix> test "2*3"
664− alg>2*3
583+ Right (6,
665− right (6, [])
584+ []) : Either (ParseError (TokenData ExpressionToken))
585+ (Integer, List (TokenData ExpressionToken))
667 * - Check that atomic number literals work:
587 * - Check that atomic number literals work:
669 - .. code-block:: idris
589 - .. code-block:: idris
671− *algebraREPL> :exec
591+ *parserExInfix> test "2"
673− right (2, [])
593+ []) : Either (ParseError (TokenData ExpressionToken))
594+ (Integer, List (TokenData ExpressionToken))
675 * - Check that '*' has a higher precedence than '+'.
596 * - Check that '*' has a higher precedence than '+'.
677 - .. code-block:: idris
598 - .. code-block:: idris
679− *algebraREPL> :exec
600+ *parserExInfix> test "2+3*4"
680− alg>2+3*4
601+ Right (14,
681− right (14, [])
602+ []) : Either (ParseError (TokenData ExpressionToken))
603+ (Integer, List (TokenData ExpressionToken))
683 * - Also '*' has a higher precedence than '+' when the order is reversed.
605 * - Also '*' has a higher precedence than '+' when the order is reversed.
685 - .. code-block:: idris
607 - .. code-block:: idris
687− *algebraREPL> :exec
609+ *parserExInfix> test "3*4+2"
688− alg>3*4+2
610+ Right (14,
689− right (14, [])
611+ []) : Either (ParseError (TokenData ExpressionToken))
612+ (Integer, List (TokenData ExpressionToken))
691 * - Also precedence can be overridden by parenthesis.
614 * - Also precedence can be overridden by parenthesis.
693 - .. code-block:: idris
616 - .. code-block:: idris
695− *algebraREPL> :exec
618+ *parserExInfix> test "(2+3)*4"
696− alg>(2+3)*4
619+ Right (20,
697− right (20, [])
620+ []) : Either (ParseError (TokenData ExpressionToken))
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``.