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

git.iko.soy/Idris-dev

add page about whitespace and comments

commit0a8b421d385dae959d07831598ffad82b318ab9c authormartinbaker <git29f185@martinb.com> dateThu 9 Jan 2020, 08:34 (7 years ago) parenteb780f7

5 files changed+193−32

compare with master

unifiedsplit

docs/parserLibrary/index.rst+1 docs/parserLibrary/introduction.rst+23−11 docs/parserLibrary/lexer.rst+11−9 docs/parserLibrary/parser.rst+22−12 docs/parserLibrary/whitespace.rst+136

docs/parserLibrary/index.rst+1

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

2121 introduction

2222 lexer

2323 parser

24+ whitespace

docs/parserLibrary/introduction.rst+23−11

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

55***************************

77The 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

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

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

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

1010

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

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

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

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

13+written for.

1314

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

1516workings of Idris 2.

1617

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.

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

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.

1821

1922.. list-table::

2023

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

2730 :height: 76px

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

2932

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.

3135

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.

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

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.

3340

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.

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

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

43+a string when a rule is matched.

3544

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

3747example 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.

3950

4051Parser Library and Idris 2

4152--------------------------

4253

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

4455parser 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.

4658

4759Idris 2 has at least 3 compilers:

4860

docs/parserLibrary/lexer.rst+11−9

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

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

2727- A way to construct these individual tokens.

2828

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:

3031

3132.. code-block:: idris

3233

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

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

5859

5960A 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:

6163

6264.. code-block:: idris

6365

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

7274

7375.. list-table::

7476

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

76− is guaranteed to consume a character.

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

78+ the sequence is guaranteed to consume a character.

7779

7880 - .. code-block:: idris

7981

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

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

131133when the indent decreases.

132134

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

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

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

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

136+:ref:`parserLibraryWhitespace`.

136137

137138Simple Expression Example for Lexer

138139-----------------------------------

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

267268 Int,

268269 String)

269270

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−pick out the tokens:

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

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

272274

273275- (Number 1)

274276- (Operator "+")

docs/parserLibrary/parser.rst+22−12

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

33Parser

44======

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).

89.. code-block:: idris

910

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

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

1920

2021So 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−recogniser combinator for the lexer, which was discussed on the previous page.

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

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

24+previous page.

2325

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

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

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

111113 (Integer, List (TokenData ExpressionToken))

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

113115

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

115−number in the 'Right' option.

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

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

116118

117119.. code-block:: idris

118120

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

260262

261263.. list-table::

262264

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.

264267

265268 - .. code-block:: idris

266269

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

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

282285

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

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.

287+In 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.

285289

286290.. list-table::

287291

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

490494

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

492496

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.

494499

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.

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

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

502+first tokens would not be consumed.

496503

497504Another approach is left factoring:

498505

499506Left Factoring

500507--------------

501508

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:

503511

504512.. code-block:: idris

505513

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

512520 A -> x<*>N

513521 N -> y <|> z

514522

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.

516525

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.

518528

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

520530

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+