1.. _parserLibraryParser:
6To run the parser we call ``parse``. This requires a grammar and the output
7from the lexer (which is a list of tokens).
11 parse : (act : Grammar tok c ty) -> (xs : List tok) ->
12 Either (ParseError tok) (ty, List tok)
14If successful this returns 'Right' with a pair of
17- the unparsed tokens (the remaining input).
19otherwise it returns 'Left' with the error message.
21So 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
23to the recogniser combinator for the lexer, which was discussed on the
26As with the Recogniser the ``Grammar`` type is dependent on a boolean 'consumes'
27value which allows us to ensure that complicated ``Grammar`` structures will always
32 ||| Description of a language's grammar. The `tok` parameter is the type
33 ||| of tokens, and the `consumes` flag is True if the language is guaranteed
34 ||| to be non-empty - that is, successfully parsing the language is guaranteed
35 ||| to consume some input.
37 data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
38 Empty : (val : ty) -> Grammar tok False ty
39 Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
40 NextIs : String -> (tok -> Bool) -> Grammar tok False tok
41 EOF : Grammar tok False ()
43 Fail : Bool -> String -> Grammar tok c ty
44 Commit : Grammar tok False ()
45 MustWork : Grammar tok c a -> Grammar tok c a
47 SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
49 SeqEmpty : {c1, c2 : Bool} ->
50 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
51 Grammar tok (c1 || c2) b
52 Alt : {c1, c2 : Bool} ->
53 Grammar tok c1 ty -> Grammar tok c2 ty ->
54 Grammar tok (c1 && c2) ty
56So an example of a grammer type may look something like this:
57``Grammar (TokenData ExpressionToken) True Integer``.
58This 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
60to what is done in Idris 2
61: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
68 Rule ty = Grammar (TokenData ExpressionToken) True ty
73On the previous page we implemented a lexer to 'lex' a very simple expression, on
74this page we will go on to add a parser for this running example.
78 * - The syntax we are aiming at is something
79 like this (expressed in Backus–Naur form (BNF)):
80 - .. code-block:: idris
82 <expr> ::= <integer literal>
88 <integer literal> ::= <digit>|<integer literal><digit>
92 * - To start, here is a grammar to parse an integer literal (that is, a
93 sequence of numeric characters).
95 - .. code-block:: idris
98 intLiteral : Rule Integer
100 = terminal (\x => case tok x of
104In order to try this out, here is a temporary function, this calls
105parse which takes two parameters:
107- The grammar (in this case intLiteral)
108- The token list from the lexer.
112 test1 : String -> Either (ParseError (TokenData ExpressionToken))
113 (Integer, List (TokenData ExpressionToken))
114 test1 s = parse intLiteral (fst (lex expressionTokens s))
116As required, if we pass it a string which is a number literal then it will
117return the number in the 'Right' option.
121 *parserEx> test1 "123"
122 Right (123, []) : Either (ParseError (TokenData ExpressionToken))
123 (Integer, List (TokenData ExpressionToken))
125If we pass it a string which is not a number literal then it will return an
131 Left (Error "End of input"
132 []) : Either (ParseError (TokenData ExpressionToken))
133 (Integer, List (TokenData ExpressionToken))
135If we pass it a number followed by something else, then it will still be
136successful, this is because we are not specifically checking for end-of-file.
140 *parserEx> test1 "123a"
141 Right (123, []) : Either (ParseError (TokenData ExpressionToken))
142 (Integer, List (TokenData ExpressionToken))
147 * - The ``intLiteral`` function above uses the ``terminal`` function to
148 construct the grammar
149 - .. code-block:: idris
151 ||| Succeeds if running the predicate on the
152 ||| next token returns Just x, returning x.
155 terminal : (tok -> Maybe a) -> Grammar tok True a
159: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Parser/Core.idr
160Idris 2 uses a slightly different version which stores an error message like
161"Expected integer literal" which can be output if the rule fails
162: https://github.com/edwinb/Idris2/blob/master/src/Text/Parser/Core.idr
166 * - The 'terminal' function is also used to construct the other
167 elements of the grammar that we require, for instance,
170 - .. code-block:: idris
172 openParen : Rule Integer
173 openParen = terminal (\x => case tok x of
177Integer value is not really relevant for parenthesis so ``0`` (zero) is used as
180As before, this can be tested with a function like this:
184 test2 : String -> Either (ParseError (TokenData ExpressionToken))
185 (Integer, List (TokenData ExpressionToken))
186 test2 s = parse openParen (fst (lex expressionTokens s))
188We can see below that it correctly parses an open parenthesis and gives an
189error for anything else:
194 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
195 (Integer, List (TokenData ExpressionToken))
196 *parserEx> test2 "123"
197 Left (Error "Unrecognised token"
200 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
202 List (TokenData ExpressionToken))
204Now we have two Grammars we can try combining them. The following test looks
205for ``openParen`` followed by ``intLiteral``, the two Grammars are combined using
206``<*>``. The ``map const`` part uses the integer value from the first.
208The following test is looking for ``(`` followed by a number:
212 test3 : String -> Either (ParseError (TokenData ExpressionToken))
213 (Integer, List (TokenData ExpressionToken))
214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
216We can see below that ``(`` followed by a number is successfully parsed but, as
217required, other token lists are not:
221 *parserEx> test3 "(123"
222 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
223 (Integer, List (TokenData ExpressionToken))
224 *parserEx> test3 "(("
225 Left (Error "Unrecognised token"
227 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
229 (incol, "") => c + cast (length incol)
230 (incol, b) => cast (length incol))
231 OParen]) : Either (ParseError (TokenData ExpressionToken))
232 (Integer, List (TokenData ExpressionToken))
234 *parserEx> test3 "123"
235 Left (Error "Unrecognised token"
238 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
240 List (TokenData ExpressionToken))
241 *parserEx> test3 "123("
242 Left (Error "Unrecognised token"
243 [MkToken 0 0 (Number 123),
245 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
247 (incol, "") => c + cast (length incol)
248 (incol, b) => cast (length incol))
249 OParen]) : Either (ParseError (TokenData ExpressionToken))
250 (Integer, List (TokenData ExpressionToken))
254 * - The closing parenthesis is constructed in the same way.
256 - .. code-block:: idris
258 closeParen : Rule Integer
259 closeParen = terminal (\x => case tok x of
265 * - Now we can generate a Grammar for an expression inside parenthesis
268 - .. code-block:: idris
270 paren : Rule Integer -> Rule Integer
271 paren exp = openParen *> exp <* closeParen
273The use of ``*>`` and ``<*`` instead of ``<*>`` is an easy way to use the integer
274value from the inner expression.
276So 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)
293This is a valid grammar because every time it is called it is guaranteed to
294consume a token. However, as an Idris structure, it is problematic due to
295the recursion. Defining it as partial allows it to compile but at runtime
296we are likely to get a crash with an (unhelpful) error message like
297``killed by signal 11``.
299So a better method is to use ``do`` notation as described in the following
305In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is
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
334This can be more flexible than using the ``<*>`` operator. Also it is defined
335using ``Inf`` so we can implement recursively defined grammars as above.
337Implementing the Arithmetic Operators
338-------------------------------------
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:
346 - .. code-block:: idris
348 expr = expr (op "+") expr
350As already explained, ``do`` notation can allow us to use recursive
351definitions but not necessarily left-recursion like this.
353In order to work up to this gradually lets start with prefix operators
354(sometimes known as Polish notation) then modify later for infix operators.
358 * - So prefix operators would have this sort of form:
360 - .. code-block:: idris
362 expr = (add (op "+") expr expr)
364where ``op`` is defined like this:
368 ||| Matches if this is an operator token and string matches, that is,
369 ||| it is the required type of operator.
370 op : String -> Rule Integer
371 op s = terminal (\x => case tok x of
372 (Operator s1) => if s==s1 then Just 0 else Nothing
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.
385 - .. code-block:: idris
387 addInt : Integer -> Integer -> Integer
391 add : Grammar tok c1 Integer ->
392 Grammar tok c2 Integer ->
393 Grammar tok c3 Integer ->
394 Grammar tok ((c1 || c2) || c3) Integer
395 add x y z = map addInt (x *> y) <*> z
399The resulting integer will be the sum of the two operands.
403 * - The other operators are defined in a similar way:
405 - .. code-block:: idris
407 subInt : Integer -> Integer -> Integer
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
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
427So 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.
434 expr = (add (op "+") expr expr)
435 <|> (sub (op "-") expr expr)
436 <|> (mult (op "*") expr expr)
437 <|> intLiteral <|> (paren expr)
441 * - To make the testing easier we can use this function:
443 - .. code-block:: idris
446 test : String -> Either (ParseError (TokenData ExpressionToken))
447 (Integer, List (TokenData ExpressionToken))
448 test s = parse expr (fst (lex expressionTokens s))
452 * - First test a valid (prefix) expression:
454 - .. code-block:: idris
456 *parserEx> test "+1*6(4)"
458 []) : Either (ParseError (TokenData ExpressionToken))
459 (Integer, List (TokenData ExpressionToken))
461Then an invalid syntax:
466 Left (Error "Unrecognised token"
470 not (intToBool (prim__eqChar ARG
473 (incol, "") => c + cast (length incol)
474 (incol, b) => cast (length incol))
475 CParen]) : Either (ParseError (TokenData ExpressionToken))
477 List (TokenData ExpressionToken))
479However if we try something that is invalid, but starts with a valid token,
480then it will return ``Right`` (to indicate success)
484 *parserEx> test "1))"
488 not (intToBool (prim__eqChar ARG '\n')))
490 (incol, "") => c + cast (length incol)
491 (incol, b) => cast (length incol))
495 not (intToBool (prim__eqChar ARG '\n')))
497 (incol, "") => c + cast (length incol)
498 (incol, b) => cast (length incol))
499 CParen]) : Either (ParseError (TokenData ExpressionToken))
501 List (TokenData ExpressionToken))
506So 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
509infinite data structures (see Codata Types here :ref:`sect-typefuns`).
511First alter the grammar to have infix operations:
515 addInt : Integer -> Integer -> Integer
519 add : Grammar tok c1 Integer ->
520 Grammar tok c2 Integer ->
521 Grammar tok c3 Integer ->
522 Grammar tok ((c1 || c2) || c3) Integer
523 add x y z = map addInt (x <* y) <*> z
525 subInt : Integer -> Integer -> Integer
529 sub : Grammar tok c1 Integer ->
530 Grammar tok c2 Integer ->
531 Grammar tok c3 Integer ->
532 Grammar tok ((c1 || c2) || c3) Integer
533 sub x y z = map subInt (x <* y) <*> z
536 multInt : Integer -> Integer -> Integer
540 mult : Grammar tok c1 Integer ->
541 Grammar tok c2 Integer ->
542 Grammar tok c3 Integer ->
543 Grammar tok ((c1 || c2) || c3) Integer
544 mult x y z = map multInt (x <* y) <*> z
548 expr = (add expr (op "+") expr)
549 <|> (sub expr (op "-") expr)
550 <|> (mult expr (op "*") expr)
551 <|> intLiteral <|> (paren expr)
553However, if this was run, the code would not terminate.
555Implement Left Recursion Elimination
556------------------------------------
558Left factoring, like this, is a general problem.
560If we have a rule like this:
564 A -> (x<*>y) <|> (x<*>z)
566If ``x<*>y`` fails but ``x<*>z`` would succeed a problem is that, ``x<*>y`` has
567already consumed ``x``, so now ``x<*>z`` will fail.
569so 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
571first tokens would not be consumed.
573Another approach is left factoring:
578Replace the rule with two rules (that is we add a non-terminal symbol) so
579for example, instead of:
583 A -> (x<*>y) <|> (x<*>z)
585we add an extra rule to give:
592That 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.
595This still does not solve the infinite recursion issue and there is another
596problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.
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.
603 - .. code-block:: idris
605 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}
607 'term' ::= 'factor' {'*' 'factor'}
611 | '(' 'expression' ')'
618 factor : Rule Integer
619 factor = intLiteral <|> do
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))
643 lft : (ParseError (TokenData ExpressionToken)) -> IO ()
644 lft (Error s lst) = putStrLn ("error:"++s)
646 rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
647 rht i = putStrLn ("right " ++ (show i))
653 either lft rht (calc x) -- eliminator for Either
655As the following tests show, this now handles infix operators and precedence.
659 * - For example '*' is an infix operator:
661 - .. code-block:: idris
667 * - Check that atomic number literals work:
669 - .. code-block:: idris
675 * - Check that '*' has a higher precedence than '+'.
677 - .. code-block:: idris
683 * - Also '*' has a higher precedence than '+' when the order is reversed.
685 - .. code-block:: idris
691 * - Also precedence can be overridden by parenthesis.
693 - .. code-block:: idris
699This is still not correct because it does not correctly parse multiple sums or terms
700like ``1+2+3`` or ``1*2*3``.
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list