@@ -8,8 +8,8 @@ module:
88
99 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
1010
11−This function takes a String and returns a list of tokens. With the tokens we have
12−indexes back to the original string which can be used in error messages:
11+This function takes a String and returns a list of tokens. With the tokens we
12+have indexes back to the original string which can be used in error messages:
1313
1414.. image:: ../image/tokenise.png
1515 :width: 330px
@@ -24,7 +24,8 @@ In order to construct this list of tokens we need:
2424- A way to recognise the tokens in the input string.
2525- A way to construct these individual tokens.
2626
27−This is given by the TokenMap. This is a mapping from lexers to the tokens they produce. This is a list of pairs:
27+This is given by the TokenMap. This is a mapping from lexers to the tokens
28+they produce. This is a list of pairs:
2829
2930.. code-block:: idris
3031
@@ -155,11 +156,11 @@ implement 'show' for these tokens:
155156 Show (TokenData ExpressionToken) where
156157 show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t
157158
158−.. code-block:: idris
159−
160159The following defines the 'TokenMap' for this example:
161160
162− -- integer arithmetic operators plus, minus and multiply.
161+.. code-block:: idris
162+
163+ ||| integer arithmetic operators plus, minus and multiply.
163164 export
164165 opChars : String
165166 opChars = "+-*"
@@ -172,7 +173,7 @@ The following defines the 'TokenMap' for this example:
172173
173174 expressionTokens : TokenMap ExpressionToken
174175 expressionTokens =
175− [(digits, \x => Number (toInt' x)),
176+ [(digits, \x => Number (toInt' x)),
176177 (operator, \x => Operator x),
177178 (is '(' ,\x => OParen),
178179 (is ')' ,\x => CParen)]
@@ -229,7 +230,8 @@ input string as parameters:
229230 Int,
230231 String)
231232
232−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy. In the example the indexes have not been computed but we can pick out the tokens:
233+The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy. In the example the indexes have not been computed but we can
234+pick out the tokens:
233235
234236- (Number 1)
235237- (Operator "+")
@@ -237,4 +239,5 @@ The lexer uses potentially infinite data structures. It has recursive arguments
237239
238240So the code is working.
239241
240−A parser for this example will be constructed on the next page.
242+We can now go ahead and parse this token list. A parser for this example will
243+be constructed on the next page.