@@ -59,8 +59,7 @@ test whether to accept the character. It can be constructed using the 'is' funct
60.. code-block:: idris
60.. code-block:: idris
62− Idris> :module Lexer2
62+ *parserEx> is 'a'
64 Pred (\ARG =>
63 Pred (\ARG =>
65 intToBool (prim__eqChar ARG 'a'))
64 intToBool (prim__eqChar ARG 'a'))
66 : Recognise True
65 : Recognise True
@@ -76,39 +75,34 @@ combined, for example,
77 - .. code-block:: idris
76 - .. code-block:: idris
79− *Lexer2> is 'a' <+> is 'b'
78+ *parserEx> is 'a' <+> is 'b'
80 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
79 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
81 (Delay (is 'b')) : Recognise True
80 (Delay (is 'b')) : Recognise True
84 * - <|> means if both consume, the combination is guaranteed
82 * - <|> means if both consume, the combination is guaranteed
85 to consumer a character:
83 to consumer a character:
87 - .. code-block:: idris
85 - .. code-block:: idris
89− *Lexer2> is 'a' <|> is 'b'
87+ *parserEx> is 'a' <|> is 'b'
90 Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
88 Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
91− (Pred (\ARG => intToBool (prim__eqChar ARG 'b'))) : Recognise True
89+ (Pred (\ARG => intToBool (prim__eqChar ARG 'b')))
92− *Lexer2>
90+ : Recognise True
92+This diagram shows the recogniser combinator with some of its constructors:
95.. image:: ../image/recogniser.png
94.. image:: ../image/recogniser.png
96 :width: 487px
95 :width: 487px
97 :height: 249px
96 :height: 249px
98 :alt: recogniser data structure
97 :alt: recogniser data structure
100−There are constructors and combinators to allow the construction of the lexer definition:
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.
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.
107Simple Expression Example for Lexer
99Simple Expression Example for Lexer
108-----------------------------------
100-----------------------------------
110−On this page we will implement a lexer to lex a very simple expression, on the
102+On this page we will implement a lexer to lex a very simple expression as
111−next page we will go on to implement a parser for it.
103+a running example, on the next page we will go on to implement a parser for it.
105+First import the lexer and parser code:
113.. code-block:: idris
107.. code-block:: idris
@@ -118,54 +112,20 @@ next page we will go on to implement a parser for it.
118 import public Text.Parser.Core
112 import public Text.Parser.Core
119 import public Text.Parser
113 import public Text.Parser
121−
115+Then decide on the tokens that are needed. For this example the idea is to be
122−to run:
116+able to parse simple arithmetic expressions, like this:
124.. code-block:: idris
118.. code-block:: idris
126− cd Idris-dev/libs/contrib
120+ 1+(2*3)
127− idris -p contrib parserEx.idr
129− / _/___/ /____(_)____
130− / // __ / ___/ / ___/ Version 1.3.2
131− _/ // /_/ / / / (__ ) http://www.idris-lang.org/
132− /___/\__,_/_/ /_/____/ Type :? for help
134− Idris is free software with ABSOLUTELY NO WARRANTY.
122+so we need:
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
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.
146− *parserEx> lex expressionTokens "1+2"
128+We can define these, as tokens, like this:
147− ([MkToken 0 0 (Number 1),
149− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
150− (incol, "") => c + cast (length incol)
151− (incol, b) => cast (length incol))
154− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
155− (incol, "") => c + cast (length incol)
156− (incol, b) => cast (length incol))
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),
168−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy.
170.. code-block:: idris
130.. code-block:: idris
@@ -178,6 +138,9 @@ The lexer uses potentially infinite data structures. It has recursive arguments
179 | EndInput
139 | EndInput
141+It may help with debugging and to implement error messages to
142+implement 'show' for these tokens:
181.. code-block:: idris
144.. code-block:: idris
@@ -188,14 +151,14 @@ The lexer uses potentially infinite data structures. It has recursive arguments
188 show CParen = ")"
151 show CParen = ")"
189 show EndInput = "end of input"
152 show EndInput = "end of input"
191−.. code-block:: idris
194 Show (TokenData ExpressionToken) where
155 Show (TokenData ExpressionToken) where
195 show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t
156 show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t
197.. code-block:: idris
158.. code-block:: idris
160+The following defines the 'TokenMap' for this example:
199 -- integer arithmetic operators plus, minus and multiply.
162 -- integer arithmetic operators plus, minus and multiply.
201 opChars : String
164 opChars : String
@@ -204,8 +167,6 @@ The lexer uses potentially infinite data structures. It has recursive arguments
204 operator : Lexer
167 operator : Lexer
205 operator = some (oneOf opChars)
168 operator = some (oneOf opChars)
207−.. code-block:: idris
209 toInt' : String -> Integer
170 toInt' : String -> Integer
210 toInt' = cast
171 toInt' = cast
@@ -216,3 +177,64 @@ The lexer uses potentially infinite data structures. It has recursive arguments
216 (is '(' ,\x => OParen),
177 (is '(' ,\x => OParen),
217 (is ')' ,\x => CParen)]
178 (is ')' ,\x => CParen)]
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.
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
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:
191+.. code-block:: idris
193+ cd Idris-dev/libs/contrib
194+ idris -p contrib parserEx.idr
196+ / _/___/ /____(_)____
197+ / // __ / ___/ / ___/ Version 1.3.2
198+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/
199+ /___/\__,_/_/ /_/____/ Type :? for help
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
211+ *parserEx> lex expressionTokens "1+2"
212+ ([MkToken 0 0 (Number 1),
214+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
215+ (incol, "") => c + cast (length incol)
216+ (incol, b) => cast (length incol))
219+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
220+ (incol, "") => c + cast (length incol)
221+ (incol, b) => cast (length incol))
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),
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:
238+So the code is working.
240+A parser for this example will be constructed on the next page.