@@ -59,8 +59,7 @@ test whether to accept the character. It can be constructed using the 'is' funct
5959
6060.. code-block:: idris
6161
62− Idris> :module Lexer2
63− *Lexer2> is 'a'
62+ *parserEx> is 'a'
6463 Pred (\ARG =>
6564 intToBool (prim__eqChar ARG 'a'))
6665 : Recognise True
@@ -76,39 +75,34 @@ combined, for example,
7675
7776 - .. code-block:: idris
7877
79− *Lexer2> is 'a' <+> is 'b'
78+ *parserEx> is 'a' <+> is 'b'
8079 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
8180 (Delay (is 'b')) : Recognise True
82− *Lexer2>
8381
8482 * - <|> means if both consume, the combination is guaranteed
8583 to consumer a character:
8684
8785 - .. code-block:: idris
8886
89− *Lexer2> is 'a' <|> is 'b'
87+ *parserEx> is 'a' <|> is 'b'
9088 Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
91− (Pred (\ARG => intToBool (prim__eqChar ARG 'b'))) : Recognise True
92− *Lexer2>
89+ (Pred (\ARG => intToBool (prim__eqChar ARG 'b')))
90+ : Recognise True
9391
92+This diagram shows the recogniser combinator with some of its constructors:
9493
9594.. image:: ../image/recogniser.png
9695 :width: 487px
9796 :height: 249px
9897 :alt: recogniser data structure
9998
100−There are constructors and combinators to allow the construction of the lexer definition:
101−
102−
103−So far, this is static code, to define the lexical structure. To lex a given text we need to pass this to the runtime code.
104−
105−However this can only cut up the string into a list of substrings, these must be converted into tokens so we need a way to construct tokens. This will also depend on the lexical structure we require.
106−
10799Simple Expression Example for Lexer
108100-----------------------------------
109101
110−On this page we will implement a lexer to lex a very simple expression, on the
111−next page we will go on to implement a parser for it.
102+On this page we will implement a lexer to lex a very simple expression as
103+a running example, on the next page we will go on to implement a parser for it.
104+
105+First import the lexer and parser code:
112106
113107.. code-block:: idris
114108
@@ -118,54 +112,20 @@ next page we will go on to implement a parser for it.
118112 import public Text.Parser.Core
119113 import public Text.Parser
120114
121−
122−to run:
115+Then decide on the tokens that are needed. For this example the idea is to be
116+able to parse simple arithmetic expressions, like this:
123117
124118.. code-block:: idris
125119
126− cd Idris-dev/libs/contrib
127− idris -p contrib parserEx.idr
128− ____ __ _
129− / _/___/ /____(_)____
130− / // __ / ___/ / ___/ Version 1.3.2
131− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
132− /___/\__,_/_/ /_/____/ Type :? for help
120+ 1+(2*3)
133121
134− Idris is free software with ABSOLUTELY NO WARRANTY.
135− For details type :warranty.
136− Type checking ./Text/Token.idr
137− Type checking ./Text/Quantity.idr
138− Type checking ./Control/Delayed.idr
139− Type checking ./Data/Bool/Extra.idr
140− Type checking ./Text/Lexer/Core.idr
141− Type checking ./Text/Lexer.idr
142− Type checking ./parserEx.idr
122+so we need:
143123
144−.. code-block:: idris
124+- Numbers (for now integer literals are good enough).
125+- Some operators (for now '+', '-' and '*' will do.
126+- Opening and closing Parentheses.
145127
146− *parserEx> lex expressionTokens "1+2"
147− ([MkToken 0 0 (Number 1),
148− MkToken 0
149− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
150− (incol, "") => c + cast (length incol)
151− (incol, b) => cast (length incol))
152− (Operator "+"),
153− MkToken 0
154− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
155− (incol, "") => c + cast (length incol)
156− (incol, b) => cast (length incol))
157− (Number 2)],
158− 0,
159− case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "2" of
160− (incol, "") => c + cast (length incol)
161− (incol, b) => cast (length incol),
162− getString (MkStrLen "" 0)) : (List (TokenData ExpressionToken),
163− Int,
164− Int,
165− String)
166− *parserEx>
167−
168−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy.
128+We can define these, as tokens, like this:
169129
170130.. code-block:: idris
171131
@@ -178,6 +138,9 @@ The lexer uses potentially infinite data structures. It has recursive arguments
178138 | CParen
179139 | EndInput
180140
141+It may help with debugging and to implement error messages to
142+implement 'show' for these tokens:
143+
181144.. code-block:: idris
182145
183146 export
@@ -188,14 +151,14 @@ The lexer uses potentially infinite data structures. It has recursive arguments
188151 show CParen = ")"
189152 show EndInput = "end of input"
190153
191−.. code-block:: idris
192−
193154 export
194155 Show (TokenData ExpressionToken) where
195156 show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t
196157
197158.. code-block:: idris
198159
160+The following defines the 'TokenMap' for this example:
161+
199162 -- integer arithmetic operators plus, minus and multiply.
200163 export
201164 opChars : String
@@ -204,8 +167,6 @@ The lexer uses potentially infinite data structures. It has recursive arguments
204167 operator : Lexer
205168 operator = some (oneOf opChars)
206169
207−.. code-block:: idris
208−
209170 toInt' : String -> Integer
210171 toInt' = cast
211172
@@ -216,3 +177,64 @@ The lexer uses potentially infinite data structures. It has recursive arguments
216177 (is '(' ,\x => OParen),
217178 (is ')' ,\x => CParen)]
218179
180+This specifies the lexer. It gives, for each token, a function to recognise
181+the token type and a function to construct the token.
182+
183+The library module 'Text.Lexer' contains useful functions to help with this.
184+For example, the digits function used above, which reads one or more
185+numeric characters.
186+
187+We can now run the code with various strings to see what output the lexer
188+produces. This is done by calling the 'lex' function with the TokenMap and
189+input string as parameters:
190+
191+.. code-block:: idris
192+
193+ cd Idris-dev/libs/contrib
194+ idris -p contrib parserEx.idr
195+ ____ __ _
196+ / _/___/ /____(_)____
197+ / // __ / ___/ / ___/ Version 1.3.2
198+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
199+ /___/\__,_/_/ /_/____/ Type :? for help
200+
201+ Idris is free software with ABSOLUTELY NO WARRANTY.
202+ For details type :warranty.
203+ Type checking ./Text/Token.idr
204+ Type checking ./Text/Quantity.idr
205+ Type checking ./Control/Delayed.idr
206+ Type checking ./Data/Bool/Extra.idr
207+ Type checking ./Text/Lexer/Core.idr
208+ Type checking ./Text/Lexer.idr
209+ Type checking ./parserEx.idr
210+
211+ *parserEx> lex expressionTokens "1+2"
212+ ([MkToken 0 0 (Number 1),
213+ MkToken 0
214+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
215+ (incol, "") => c + cast (length incol)
216+ (incol, b) => cast (length incol))
217+ (Operator "+"),
218+ MkToken 0
219+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
220+ (incol, "") => c + cast (length incol)
221+ (incol, b) => cast (length incol))
222+ (Number 2)],
223+ 0,
224+ case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "2" of
225+ (incol, "") => c + cast (length incol)
226+ (incol, b) => cast (length incol),
227+ getString (MkStrLen "" 0)) : (List (TokenData ExpressionToken),
228+ Int,
229+ Int,
230+ String)
231+
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+
234+- (Number 1)
235+- (Operator "+")
236+- (Number 2)
237+
238+So the code is working.
239+
240+A parser for this example will be constructed on the next page.