0a8b421 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

add page about whitespace and comments

0a8b421martinbaker7 years ago

docs/parserLibrary/index.rst+1

compare with master

unifiedsplit

@@ -21,3 +21,4 @@ A tutorial on the lexer and parser library in Idris.

21 introduction

22 lexer

23 parser

24+ whitespace

docs/parserLibrary/introduction.rst+23−11

@@ -5,16 +5,19 @@ Parser Library Introduction

5***************************

7The parser library can be used to build Idris structures from text. It involves a

8−certain amount of complexity and so it would typically be used for big projects. An

8+certain amount of complexity and so it would typically be used for big projects.

9−example might be a compiler for another language, written in Idris.

9+An example might be a compiler for another language, written in Idris.

11−Of course the parser library can also be used to compile to Idris, this is what is

11+Of course the parser library can also be used to compile to Idris, this is what

12−done in Idris 2 and that is what the this library appears to have been written for.

12+is done in Idris 2 and that is what the this library appears to have been

13+written for.

14So a secondary use for this tutorial would be to help understanding the internal

15So a secondary use for this tutorial would be to help understanding the internal

15workings of Idris 2.

16workings of Idris 2.

18+The parser library is used in a similar way to Parsec which is a library for

17−The parser library is used in a similar way to Parsec which is a library for writing parsers in Haskell. It is based on higher-order parser combinators, so a complicated parser can be made out of many smaller ones.

19+writing parsers in Haskell. It is based on higher-order parser combinators, so a

20+complicated parser can be made out of many smaller ones.

19.. list-table::

22.. list-table::

@@ -27,22 +30,31 @@ The parser library is used in a similar way to Parsec which is a library for wri

27 :height: 76px

30 :height: 76px

28 :alt: diagram illustrating these stages of lexer and parser

31 :alt: diagram illustrating these stages of lexer and parser

30−The advantage of using two stages, like this, is that things like whitespace and comments don't need to be considered in every parser rule.

33+The advantage of using two stages, like this, is that things like whitespace and

34+comments don't need to be considered in every parser rule.

36+The Idris parser library differs from Parsec in that you need to say in the

32−The Idris parser library differs from Parsec in that you need to say in the Recogniser whether a rule is guaranteed to consume input. This means that the Idris type system prevents the construction of recognisers/rules that can't consume the input.

37+Recogniser whether a rule is guaranteed to consume input. This means that the

38+Idris type system prevents the construction of recognisers/rules that can't

39+consume the input.

41+The Lexer is similar but works at the level of characters rather than tokens, and

34−The Lexer is similar but works at the level of characters rather than tokens, and you need to provide a TokenMap which says how to build a token representation from a string when a rule is matched.

42+you need to provide a TokenMap which says how to build a token representation from

43+a string when a rule is matched.

36−The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a tutorial for the :ref:`parserLibraryParser`. These tutorials have a running

45+The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a

46+tutorial for the :ref:`parserLibraryParser`. These tutorials have a running

37example of a parser for integer expressions. This is a very simple example, there

47example of a parser for integer expressions. This is a very simple example, there

38−may be easier ways to do something so simple, but it illustrates some of the principles.

48+may be easier ways to do something so simple, but it illustrates some of the

49+principles.

40Parser Library and Idris 2

51Parser Library and Idris 2

41--------------------------

52--------------------------

43The parser library, in Idris 1, is almost the same as the code that the Idris 2

54The parser library, in Idris 1, is almost the same as the code that the Idris 2

44parser is built on. Even if you only want to use the Idris 1 parser library it

55parser is built on. Even if you only want to use the Idris 1 parser library it

45−is useful to look at the code in the Idris 2 compilers to see how the library can be used.

56+is useful to look at the code in the Idris 2 compilers to see how the library

57+can be used.

47Idris 2 has at least 3 compilers:

59Idris 2 has at least 3 compilers:

docs/parserLibrary/lexer.rst+11−9

@@ -26,7 +26,8 @@ In order to construct this list of tokens we need:

26- A way to recognise the tokens in the input string.

27- A way to construct these individual tokens.

29−This is given by the TokenMap which is a list of pairs containing this information:

29+This is given by the TokenMap which is a list of pairs containing

30+this information:

31.. code-block:: idris

32.. code-block:: idris

@@ -57,7 +58,8 @@ Recognisers

57The first part of each entry in the TokenMap is the recogniser.

58The first part of each entry in the TokenMap is the recogniser.

59A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to

60A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to

60−test whether to accept the character. It can be constructed using the 'is' function:

61+test whether to accept the character. It can be constructed using the

62+'is' function:

62.. code-block:: idris

64.. code-block:: idris

@@ -72,8 +74,8 @@ combined, for example,

73.. list-table::

75.. list-table::

75− * - <+> means sequence two recognisers. If either consumes a character, the sequence

77+ * - <+> means sequence two recognisers. If either consumes a character,

76− is guaranteed to consume a character.

78+ the sequence is guaranteed to consume a character.

78 - .. code-block:: idris

80 - .. code-block:: idris

@@ -130,9 +132,8 @@ is important to indicate blocks. In this case we might want to output a

130start-of-block token when the indent increases and an end-of-block token

132start-of-block token when the indent increases and an end-of-block token

131when the indent decreases.

133when the indent decreases.

132

134

133−This topic needs to be more fully expanded here. Until someone does that, a

135+This topic will be discussed more fully on this page

134−possible way to get more information is to see how it is done in Idris 2

136+:ref:`parserLibraryWhitespace`.

135−: https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr

136

137

137Simple Expression Example for Lexer

138Simple Expression Example for Lexer

138-----------------------------------

139-----------------------------------

@@ -267,8 +268,9 @@ input string as parameters:

267 Int,

268 Int,

268 String)

269 String)

269

270

270−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy. In the output above the indexes have not been computed but we can

271+The lexer uses potentially infinite data structures. It has recursive

272+arguments (codata type) so code is lazy. In the output above the indexes

271−pick out the tokens:

273+have not been computed but we can pick out the tokens:

272

274

273- (Number 1)

275- (Number 1)

274- (Operator "+")

276- (Operator "+")

docs/parserLibrary/parser.rst+22−12

@@ -3,7 +3,8 @@

3Parser

4======

6−To run our parser we call 'parse'. This requires a Grammar and the output from the lexer (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).

8.. code-block:: idris

9.. code-block:: idris

@@ -18,8 +19,9 @@ If successful this returns 'Right' with a pair of

18otherwise it returns 'Left' with the error message.

19otherwise it returns 'Left' with the error message.

20So we need to define the Grammar for our parser, this is done using the following

21So we need to define the Grammar for our parser, this is done using the following

21−'Grammar' data structure. This is a combinator structure, similar in principle to the

22+'Grammar' data structure. This is a combinator structure, similar in principle

22−recogniser combinator for the lexer, which was discussed on the previous page.

23+to the recogniser combinator for the lexer, which was discussed on the

24+previous page.

24As with the Recogniser the Grammar type is dependent on a boolean 'consumes'

26As with the Recogniser the Grammar type is dependent on a boolean 'consumes'

25value which allows us to ensure that complicated Grammar structures will always

27value which allows us to ensure that complicated Grammar structures will always

@@ -111,8 +113,8 @@ parse which takes two parameters:

111 (Integer, List (TokenData ExpressionToken))

113 (Integer, List (TokenData ExpressionToken))

112 test1 s = parse intLiteral (fst (lex expressionTokens s))

114 test1 s = parse intLiteral (fst (lex expressionTokens s))

113

115

114−As required, if we pass it a string which is a number literal then it will return the

116+As required, if we pass it a string which is a number literal then it will

115−number in the 'Right' option.

117+return the number in the 'Right' option.

116

118

117.. code-block:: idris

119.. code-block:: idris

118

120

@@ -260,7 +262,8 @@ token lists are not:

260

262

261.. list-table::

263.. list-table::

262

264

263− * - Now we can generate a Grammar for an expression inside parenthesis like this.

265+ * - Now we can generate a Grammar for an expression inside parenthesis

266+ like this.

264

267

265 - .. code-block:: idris

268 - .. code-block:: idris

266

269

@@ -281,7 +284,8 @@ value from the inner expression.

281 expr = (add expr (op "+") expr)

284 expr = (add expr (op "+") expr)

282

285

283This is a potentially infinite structure which is not total.

286This is a potentially infinite structure which is not total.

287+In order to work up to this gradually I will start with prefix operators

284−In order to work up to this gradually I will start with prefix operators (sometimes known as Polish notation) then modify later for infix operators.

288+(sometimes known as Polish notation) then modify later for infix operators.

285

289

286.. list-table::

290.. list-table::

287

291

@@ -490,16 +494,20 @@ If we have a rule like this:

490

494

491 A -> (x<*>y) <|> (x<*>z)

495 A -> (x<*>y) <|> (x<*>z)

492

496

493−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has 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.

494

499

500+so we could write code to backtrack. That is 'try' 'x<*>y' without consuming

495−so we could write code to backtrack. That is 'try' 'x<*>y' without consuming so that, if the first token succeeds but the following tokens fail, then the first tokens would not be consumed.

501+so that, if the first token succeeds but the following tokens fail, then the

502+first tokens would not be consumed.

496

503

497Another approach is left factoring:

504Another approach is left factoring:

498

505

499Left Factoring

506Left Factoring

500--------------

507--------------

501

508

502−Replace the rule with two rules (that is we add a non-terminal symbol) so for example, instead of:

509+Replace the rule with two rules (that is we add a non-terminal symbol) so

510+for example, instead of:

503

511

504.. code-block:: idris

512.. code-block:: idris

505

513

@@ -512,9 +520,11 @@ we add an extra rule to give:

512 A -> x<*>N

520 A -> x<*>N

513 N -> y <|> z

521 N -> y <|> z

514

522

515−That is we convert a general context-free grammar to a LL(1) grammar. Although not every context-free grammar can be converted to a LL(1) grammar.

523+That is we convert a general context-free grammar to a LL(1) grammar. Although

524+not every context-free grammar can be converted to a LL(1) grammar.

516

525

517−This still does not solve the infinite recursion issue and there is another problem: the precedence of the operators +, - and * is not explicit.

526+This still does not solve the infinite recursion issue and there is another

527+problem: the precedence of the operators +, - and * is not explicit.

518

528

519To resolve this we can alter the example like this:

529To resolve this we can alter the example like this:

520

530

docs/parserLibrary/whitespace.rstnew file+136

@@ -0,0 +1,136 @@

1+.. _parserLibraryWhitespace:

3+Whitespace and Comments

4+=======================

6+The previous two pages introduced the lexer and parser but have not yet

7+discussed how to handle whitespace and comments.

9+In some grammars whitespace and comments would not be considered significant and

10+so we might be tempted not to generate any tokens for them. However, in the

11+running example, we may want to make spaces significant. For example, we might

12+want to implement function application expressed by juxtaposition as in

13+Haskell and Idris like this: ``f x``.

14+

15+Also, I'm not sure if it is an problem for error messages and so on if some

16+text does not have corresponding tokens.

17+

18+So, on this page, we will add a token for whitespace and comments.

19+

20+Whitespace and Comments in Lexer

21+--------------------------------

22+

23+To start with we can use the same token for both whitespace and comments. Here

24+it is called ``Comment`` and added to the ``ExpressionToken`` data structure

25+like this:

26+

27+.. code-block:: idris

28+

29+ public export

30+ data ExpressionToken = Number Integer

31+ | Operator String

32+ | OParen

33+ | CParen

34+ | Comment String

35+ | EndInput

36+

37+This is added to the ``TokenMap`` like this:

38+

39+.. code-block:: idris

40+

41+ ||| from https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr

42+ comment : Lexer

43+ comment = is '-' <+> is '-' <+> many (isNot '\n')

44+

45+ expressionTokens : TokenMap ExpressionToken

46+ expressionTokens =

47+ [(digits, \x => Number (toInt' x)),

48+ (operator, \x => Operator x),

49+ (is '(' ,\x => OParen),

50+ (is ')' ,\x => CParen),

51+ (space, Comment),

52+ (comment, Comment)]

53+

54+As you can see, the comment is defined like a single line Idris comment,

55+it starts with ``--`` and continues for the remainder of the line.

56+

57+We don't need to define ``space`` because it is already defined in

58+: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr

59+like this:

60+

61+.. code-block:: idris

62+

63+ ||| Recognise a single whitespace character

64+ ||| /\\s/

65+ space : Lexer

66+ space = pred isSpace

67+

68+ ||| Recognise one or more whitespace characters

69+ ||| /\\s+/

70+ spaces : Lexer

71+ spaces = some space

72+

73+Whitespace and Comments in Parser

74+---------------------------------

75+

76+Now that there are ``Comment`` tokens the parser needs to be able to handle them.

77+

78+So far we don't have any syntax that requires spaces to be significant so we

79+need to define the grammar so that it will parse with, or without, spaces.

80+This needs to be done in a systematic way, here I have defined the grammar so

81+that there is an optional space to the right of every atom or operator:

82+

83+.. code-block:: idris

84+

85+ commentSpace : Rule Integer

86+ commentSpace = terminal (\x => case tok x of

87+ Comment s => Just 0

88+ _ => Nothing)

89+

90+.. code-block:: idris

91+

92+ partial

93+ exprAtom : Rule Integer

94+ exprAtom = (intLiteral <* commentSpace)

95+ <|> intLiteral <|> (paren expr)

96+

97+ partial

98+ expr1 : Rule Integer

99+ expr1 = map multInt exprAtom <*> (

100+ (((op "*") <* commentSpace) <|> (op "*"))

101+ *> exprAtom)

102+

103+ partial

104+ exprMult : Rule Integer

105+ exprMult = expr1 <|> exprAtom

106+

107+ partial

108+ expr2 : Rule Integer

109+ expr2 = map addInt exprMult <*> (

110+ (((op "+") <* commentSpace) <|> (op "+"))

111+ *> exprMult)

112+

113+ partial

114+ exprAdd : Rule Integer

115+ exprAdd = expr2 <|> exprMult

116+

117+ partial

118+ expr3 : Rule Integer

119+ expr3 = map subInt exprAdd <*> (

120+ (((op "-") <* commentSpace) <|> (op "-"))

121+ *> expr)

122+

123+ expr = expr3 <|> exprAdd

124+

125+

126+

127+

128+

129+

130+

131+

132+

133+

134+

135+

136+