git.iko.soy/Idris-dev
on d689c19 help sign in
Idris-dev/docs/parserLibrary/parser.rst
622 lines 19 kB history raw
1.. _parserLibraryParser:
3Parser
4======
6To run our parser we call 'parse'. This requires a Grammar and the output
7from the lexer (a list of tokens).
9.. code-block:: idris
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
16- the parse result.
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
24previous page.
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
28consume input.
30.. code-block:: idris
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.
36 public export
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) ->
48 Grammar tok True 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'.
59This 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
61to what is done in Idris 2
62: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
64.. code-block:: idris
66 public export
67 Rule : Type -> Type
68 Rule ty = Grammar (TokenData ExpressionToken) True ty
70Parser Example
71--------------
73On the previous page we implemented a lexer to 'lex' a very simple expression, on
74this page we will go on to implement a parser for this running example.
76.. list-table::
78 * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
79 like this:
80 - .. code-block:: idris
82 <expr> ::= <integer literal>
83 | <expr>'+'<expr>
84 | <expr>'-'<expr>
85 | <expr>'*'<expr>
86 | '('<expr>')'
88 <integer literal> ::= <digit>|<integer literal><digit>
90.. list-table::
92 * - To start, here is a Grammar to parse an integer literal (that is, a
93 sequence of numbers).
95 - .. code-block:: idris
97 export
98 intLiteral : Rule Integer
99 intLiteral
100 = terminal (\x => case tok x of
101 Number i => Just i
102 _ => Nothing)
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.
110.. code-block:: idris
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.
119.. code-block:: idris
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
126error message.
128.. code-block:: idris
130 *parserEx> test1 "a"
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.
138.. code-block:: idris
140 *parserEx> test1 "123a"
141 Right (123, []) : Either (ParseError (TokenData ExpressionToken))
142 (Integer, List (TokenData ExpressionToken))
143 *parserEx>
145.. list-table::
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.
153 ||| Otherwise fails.
154 export
155 terminal : (tok -> Maybe a) -> Grammar tok True a
156 terminal = Terminal
158This is defined here
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
164.. list-table::
166 * - The 'terminal' function is also used to construct the other
167 elements of the grammar that we require, for instance,
168 opening parenthesis:
170 - .. code-block:: idris
172 openParen : Rule Integer
173 openParen = terminal (\x => case tok x of
174 OParen => Just 0
175 _ => Nothing)
177Integer value is not really relevant for parenthesis so '0' is used as
178a default value.
180As before, we can test this out with a function like this:
182.. code-block:: idris
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:
191.. code-block:: idris
193 *parserEx> test2 "("
194 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
195 (Integer, List (TokenData ExpressionToken))
196 *parserEx> test2 "123"
197 Left (Error "Unrecognised token"
198 [MkToken 0
199 0
200 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
201 (Integer,
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:
210.. code-block:: idris
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 other
217token lists are not:
219.. code-block:: idris
221 *parserEx> test3 "(123"
222 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
223 (Integer, List (TokenData ExpressionToken))
224 *parserEx> test3 "(("
225 Left (Error "Unrecognised token"
226 [MkToken 0
227 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
228 "(" of
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"
236 [MkToken 0
237 0
238 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
239 (Integer,
240 List (TokenData ExpressionToken))
241 *parserEx> test3 "123("
242 Left (Error "Unrecognised token"
243 [MkToken 0 0 (Number 123),
244 MkToken 0
245 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
246 "321" of
247 (incol, "") => c + cast (length incol)
248 (incol, b) => cast (length incol))
249 OParen]) : Either (ParseError (TokenData ExpressionToken))
250 (Integer, List (TokenData ExpressionToken))
252.. list-table::
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
260 CParen => Just 0
261 _ => Nothing)
263.. list-table::
265 * - Now we can generate a Grammar for an expression inside parenthesis
266 like this.
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.
276.. list-table::
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:
282 - .. code-block:: idris
284 expr = (add expr (op "+") expr)
286This is a potentially infinite structure which is not total.
287In order to work up to this gradually I will start with prefix operators
288(sometimes known as Polish notation) then modify later for infix operators.
290.. list-table::
292 * - So prefix operators would have this sort of form:
294 - .. code-block:: idris
296 expr = (add (op "+") expr expr)
298where 'op' is defined like this:
300.. code-block:: idris
302 ||| Matches if this is an operator token and string matches, that is,
303 ||| it is the required type of operator.
304 op : String -> Rule Integer
305 op s = terminal (\x => case tok x of
306 (Operator s1) => if s==s1 then Just 0 else Nothing
307 _ => Nothing)
309.. list-table::
311 * - and 'add' is defined like this:
313 - .. code-block:: idris
315 addInt : Integer -> Integer -> Integer
316 addInt a b = a+b
318 export
319 add : Grammar tok c1 Integer ->
320 Grammar tok c2 Integer ->
321 Grammar tok c3 Integer ->
322 Grammar tok ((c1 || c2) || c3) Integer
323 add x y z = map addInt (x *> y) <*> z
325Where:
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.
333The other operators are defined in a similar way:
335.. code-block:: idris
337 subInt : Integer -> Integer -> Integer
338 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
348 multInt : Integer -> Integer -> Integer
349 multInt a b = a*b
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
358So 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.
361.. code-block:: idris
363 partial
364 expr : Rule Integer
365 expr = (add (op "+") expr expr)
366 <|> (sub (op "-") expr expr)
367 <|> (mult (op "*") expr expr)
368 <|> intLiteral <|> (paren expr)
370.. list-table::
372 * - To make the testing easier we can use this function:
374 - .. code-block:: idris
376 partial
377 test : String -> Either (ParseError (TokenData ExpressionToken))
378 (Integer, List (TokenData ExpressionToken))
379 test s = parse expr (fst (lex expressionTokens s))
381.. list-table::
383 * - First test a valid (prefix) expression:
385 - .. code-block:: idris
387 *parserEx> test "+1*6(4)"
388 Right (25,
389 []) : Either (ParseError (TokenData ExpressionToken))
390 (Integer, List (TokenData ExpressionToken))
392Then an invalid syntax:
394.. code-block:: idris
396 *parserEx> test "))"
397 Left (Error "Unrecognised token"
398 [MkToken 0 0 CParen,
399 MkToken 0
400 (case fspan (\ARG =>
401 not (intToBool (prim__eqChar ARG
402 '\n')))
403 ")" of
404 (incol, "") => c + cast (length incol)
405 (incol, b) => cast (length incol))
406 CParen]) : Either (ParseError (TokenData ExpressionToken))
407 (Integer,
408 List (TokenData ExpressionToken))
410However if we try something that is invalid, but starts with a valid token,
411then it will return 'Right' (to indicate success)
413.. code-block:: idris
415 *parserEx> test "1))"
416 Right (1,
417 [MkToken 0
418 (case fspan (\ARG =>
419 not (intToBool (prim__eqChar ARG '\n')))
420 "1" of
421 (incol, "") => c + cast (length incol)
422 (incol, b) => cast (length incol))
423 CParen,
424 MkToken 0
425 (case fspan (\ARG =>
426 not (intToBool (prim__eqChar ARG '\n')))
427 ")" of
428 (incol, "") => c + cast (length incol)
429 (incol, b) => cast (length incol))
430 CParen]) : Either (ParseError (TokenData ExpressionToken))
431 (Integer,
432 List (TokenData ExpressionToken))
434Infix Notation
435--------------
437So 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
440infinite data structures (see Codata Types here :ref:`sect-typefuns`).
442First alter the grammar to have infix operations:
444.. code-block:: idris
446 addInt : Integer -> Integer -> Integer
447 addInt a b = a+b
449 export
450 add : Grammar tok c1 Integer ->
451 Grammar tok c2 Integer ->
452 Grammar tok c3 Integer ->
453 Grammar tok ((c1 || c2) || c3) Integer
454 add x y z = map addInt (x <* y) <*> z
456 subInt : Integer -> Integer -> Integer
457 subInt a b = a-b
459 export
460 sub : Grammar tok c1 Integer ->
461 Grammar tok c2 Integer ->
462 Grammar tok c3 Integer ->
463 Grammar tok ((c1 || c2) || c3) Integer
464 sub x y z = map subInt (x <* y) <*> z
467 multInt : Integer -> Integer -> Integer
468 multInt a b = a*b
470 export
471 mult : Grammar tok c1 Integer ->
472 Grammar tok c2 Integer ->
473 Grammar tok c3 Integer ->
474 Grammar tok ((c1 || c2) || c3) Integer
475 mult x y z = map multInt (x <* y) <*> z
477 partial
478 expr : Rule Integer
479 expr = (add expr (op "+") expr)
480 <|> (sub expr (op "-") expr)
481 <|> (mult expr (op "*") expr)
482 <|> intLiteral <|> (paren expr)
484However, if this was run, the code would not terminate.
486Implement Left Recursion Elimination
487------------------------------------
489Left factoring, like this, is a general problem.
491If we have a rule like this:
493.. code-block:: idris
495 A -> (x<*>y) <|> (x<*>z)
497If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has
498already consumed 'x', so now 'x<*>z' will fail.
500so 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
502first tokens would not be consumed.
504Another approach is left factoring:
506Left Factoring
507--------------
509Replace the rule with two rules (that is we add a non-terminal symbol) so
510for example, instead of:
512.. code-block:: idris
514 A -> (x<*>y) <|> (x<*>z)
516we add an extra rule to give:
518.. code-block:: idris
520 A -> x<*>N
521 N -> y <|> z
523That 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.
526This still does not solve the infinite recursion issue and there is another
527problem: the precedence of the operators +, - and * is not explicit.
529To resolve this we can alter the example like this:
531.. code-block:: idris
533 paren : Rule Integer -> Rule Integer
534 paren exp = openParen *> exp <* closeParen
536 addInt : Integer -> Integer -> Integer
537 addInt a b = a+b
539 subInt : Integer -> Integer -> Integer
540 subInt a b = a-b
542 multInt : Integer -> Integer -> Integer
543 multInt a b = a*b
545 partial
546 expr : Rule Integer
548 partial
549 exprAtom : Rule Integer
550 exprAtom = intLiteral <|> (paren expr)
552 partial
553 expr1 : Rule Integer
554 expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)
556 partial
557 exprMult : Rule Integer
558 exprMult = expr1 <|> exprAtom
560 partial
561 expr2 : Rule Integer
562 expr2 = map addInt exprMult <*> ((op "+") *> exprMult)
564 partial
565 exprAdd : Rule Integer
566 exprAdd = expr2 <|> exprMult
568 partial
569 expr3 : Rule Integer
570 expr3 = map subInt exprAdd <*> ((op "-") *> expr)
572 expr = expr3 <|> exprAdd
574As the following tests show, this now handles infix operators and precedence.
576.. list-table::
578 * - For example '*' is an infix operator:
580 - .. code-block:: idris
582 *parserExInfix> test "2*3"
583 Right (6,
584 []) : Either (ParseError (TokenData ExpressionToken))
585 (Integer, List (TokenData ExpressionToken))
587 * - Check that atomic number literals work:
589 - .. code-block:: idris
591 *parserExInfix> test "2"
592 Right (2,
593 []) : Either (ParseError (TokenData ExpressionToken))
594 (Integer, List (TokenData ExpressionToken))
596 * - Check that '*' has a higher precedence than '+'.
598 - .. code-block:: idris
600 *parserExInfix> test "2+3*4"
601 Right (14,
602 []) : Either (ParseError (TokenData ExpressionToken))
603 (Integer, List (TokenData ExpressionToken))
605 * - Also '*' has a higher precedence than '+' when the order is reversed.
607 - .. code-block:: idris
609 *parserExInfix> test "3*4+2"
610 Right (14,
611 []) : Either (ParseError (TokenData ExpressionToken))
612 (Integer, List (TokenData ExpressionToken))
614 * - Also precedence can be overridden by parenthesis.
616 - .. code-block:: idris
618 *parserExInfix> test "(2+3)*4"
619 Right (20,
620 []) : Either (ParseError (TokenData ExpressionToken))
621 (Integer, List (TokenData ExpressionToken))