@@ -10,13 +10,16 @@ module:
11 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
11 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
13−This function takes a String and returns a list of tokens. With the tokens we
15+ * - This function takes a String and returns a list of tokens. With the
14−have indexes back to the original string which can be used in error messages:
16+ tokens we have indexes back to the original string which can be used
16−.. image:: ../image/tokenise.png
19+ - .. image:: ../image/tokenise.png
17− :width: 330px
20+ :width: 330px
18− :height: 73px
21+ :height: 73px
19− :alt: diagram illustrating these stages of lexer
22+ :alt: diagram illustrating these stages of lexer
@@ -34,21 +37,24 @@ this information:
34 (Lexer, String -> tokenType)
37 (Lexer, String -> tokenType)
36So for each Lexer in the list, if a substring in the input matches, run
39So for each Lexer in the list, if a substring in the input matches, run
37−the associated function to produce a token of type `tokenType`
40+the associated function to produce a token of type ``tokenType``
39−from Text.Lexer.Core:
42+.. list-table::
41−.. code-block:: idris
44+ * - from Text.Lexer.Core
45+ : https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer/Core.idr
43− TokenMap : (tokenType : Type) -> Type
47+ - .. code-block:: idris
44− TokenMap tokenType = List (Lexer, String -> tokenType)
46−We can create a tokenMap by using a function like this:
49+ TokenMap : (tokenType : Type) -> Type
50+ TokenMap tokenType = List (Lexer, String -> tokenType)
52+ * - We can create a tokenMap by using a function like this:
48−.. code-block:: idris
54+ - .. code-block:: idris
50− myTokenMap : TokenMap Token
56+ myTokenMap : TokenMap Token
51− myTokenMap = [(is 'a',CharLit)]
57+ myTokenMap = [(is 'a',CharLit)]
53Once we have a TokenMap we can use it to lex many strings.
59Once we have a TokenMap we can use it to lex many strings.
@@ -74,7 +80,7 @@ combined, for example,
75.. list-table::
81.. list-table::
77− * - <+> means sequence two recognisers. If either consumes a character,
83+ * - ``<+>`` means sequence two recognisers. If either consumes a character,
78 the sequence is guaranteed to consume a character.
84 the sequence is guaranteed to consume a character.
80 - .. code-block:: idris
86 - .. code-block:: idris
@@ -83,7 +89,7 @@ combined, for example,
83 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
89 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
84 (Delay (is 'b')) : Recognise True
90 (Delay (is 'b')) : Recognise True
86− * - <|> means if both consume, the combination is guaranteed
92+ * - ``<|>`` means if both consume, the combination is guaranteed
87 to consumer a character:
93 to consumer a character:
89 - .. code-block:: idris
95 - .. code-block:: idris
@@ -161,7 +167,7 @@ able to parse simple arithmetic expressions, like this:
161so we need:
167so we need:
163- Numbers (for now integer literals are good enough).
169- Numbers (for now integer literals are good enough).
164−- Some operators (for now '+', '-' and '*' will do.
170+- Some operators (for now ``+``, ``-`` and ``*`` will do.
165- Opening and closing Parentheses.
171- Opening and closing Parentheses.
167We can define these, as tokens, like this:
173We can define these, as tokens, like this:
@@ -178,7 +184,7 @@ We can define these, as tokens, like this:
178 | EndInput
184 | EndInput
180It may help with debugging and to implement error messages to
186It may help with debugging and to implement error messages to
181−implement 'show' for these tokens:
187+implement ``show`` for these tokens:
183.. code-block:: idris
189.. code-block:: idris