git.iko.soy/Idris-dev
on master help sign in
improve lexer description
commit3ce4e487e27b202ae0787fc8147414814140dac4 authormartinbaker <git29f185@martinb.com> dateSun 29 Dec 2019, 10:26 (7 years ago) parentbdb7405
3 files changed+583−76
compare with master
unifiedsplit
docs/image/recogniser.png docs/image/recogniser.svg+477 docs/parserLibrary/lexer.rst+106−76
docs/image/recogniser.pngnew file

Binary file not shown.

docs/image/recogniser.svgnew file+477
@@ -0,0 +1,477 @@
1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2+<!-- Created with Inkscape (http://www.inkscape.org/) -->
3+
4+<svg
5+ xmlns:dc="http://purl.org/dc/elements/1.1/"
6+ xmlns:cc="http://creativecommons.org/ns#"
7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
8+ xmlns:svg="http://www.w3.org/2000/svg"
9+ xmlns="http://www.w3.org/2000/svg"
10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
12+ width="210mm"
13+ height="297mm"
14+ viewBox="0 0 210 297"
15+ version="1.1"
16+ id="svg8"
17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18+ sodipodi:docname="recogniser.svg">
19+ <defs
20+ id="defs2" />
21+ <sodipodi:namedview
22+ id="base"
23+ pagecolor="#ffffff"
24+ bordercolor="#666666"
25+ borderopacity="1.0"
26+ inkscape:pageopacity="0.0"
27+ inkscape:pageshadow="2"
28+ inkscape:zoom="1"
29+ inkscape:cx="384.45994"
30+ inkscape:cy="560"
31+ inkscape:document-units="mm"
32+ inkscape:current-layer="layer1"
33+ showgrid="false"
34+ inkscape:window-width="1920"
35+ inkscape:window-height="1015"
36+ inkscape:window-x="0"
37+ inkscape:window-y="0"
38+ inkscape:window-maximized="1" />
39+ <metadata
40+ id="metadata5">
41+ <rdf:RDF>
42+ <cc:Work
43+ rdf:about="">
44+ <dc:format>image/svg+xml</dc:format>
45+ <dc:type
46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
47+ <dc:title />
48+ </cc:Work>
49+ </rdf:RDF>
50+ </metadata>
51+ <g
52+ inkscape:label="Layer 1"
53+ inkscape:groupmode="layer"
54+ id="layer1">
55+ <rect
56+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70599997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
57+ id="rect815"
58+ width="112.44793"
59+ height="77.258354"
60+ x="6.3499999"
61+ y="63.108334"
62+ ry="3.96875"
63+ inkscape:export-xdpi="61.120499"
64+ inkscape:export-ydpi="61.120499" />
65+ <text
66+ xml:space="preserve"
67+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:5.64444447px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
68+ x="11.112496"
69+ y="68.399994"
70+ id="text819"
71+ inkscape:export-xdpi="61.120499"
72+ inkscape:export-ydpi="61.120499"><tspan
73+ sodipodi:role="line"
74+ id="tspan817"
75+ x="11.112496"
76+ y="68.399994"
77+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:5.64444447px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">Text.Lexer.Core</tspan></text>
78+ <text
79+ id="text823"
80+ y="74.749992"
81+ x="8.7312441"
82+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
83+ xml:space="preserve"
84+ inkscape:export-xdpi="61.120499"
85+ inkscape:export-ydpi="61.120499"><tspan
86+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
87+ y="74.749992"
88+ x="8.7312441"
89+ id="tspan821"
90+ sodipodi:role="line">data Recognise : (consumes : Bool) -&gt; Type where</tspan><tspan
91+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
92+ y="80.041656"
93+ x="8.7312441"
94+ sodipodi:role="line"
95+ id="tspan825"> Empty : Recognise False</tspan><tspan
96+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
97+ y="85.333328"
98+ x="8.7312441"
99+ sodipodi:role="line"
100+ id="tspan827"> Fail : Recognise c</tspan><tspan
101+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
102+ y="90.624992"
103+ x="8.7312441"
104+ sodipodi:role="line"
105+ id="tspan829"> Lookahead : (positive : Bool) -&gt; Recognise c -&gt; Recognise False</tspan><tspan
106+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
107+ y="95.916656"
108+ x="8.7312441"
109+ sodipodi:role="line"
110+ id="tspan831"> Pred : (Char -&gt; Bool) -&gt; Recognise True</tspan><tspan
111+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
112+ y="101.20832"
113+ x="8.7312441"
114+ sodipodi:role="line"
115+ id="tspan835"> SeqEat : Recognise True -&gt; Inf (Recognise e) -&gt; Recognise True</tspan><tspan
116+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
117+ y="106.49999"
118+ x="8.7312441"
119+ sodipodi:role="line"
120+ id="tspan837"> SeqEmpty : Recognise e1 -&gt; Recognise e2 -&gt; Recognise (e1 || e2)</tspan><tspan
121+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
122+ y="111.79166"
123+ x="8.7312441"
124+ sodipodi:role="line"
125+ id="tspan839"> Alt : Recognise e1 -&gt; Recognise e2 -&gt; Recognise (e1 &amp;&amp; e2)</tspan><tspan
126+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
127+ y="117.08332"
128+ x="8.7312441"
129+ sodipodi:role="line"
130+ id="tspan841" /><tspan
131+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
132+ y="122.37499"
133+ x="8.7312441"
134+ sodipodi:role="line"
135+ id="tspan843">||| A token recogniser. Guaranteed to consume at least one character.</tspan><tspan
136+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
137+ y="127.66666"
138+ x="8.7312441"
139+ sodipodi:role="line"
140+ id="tspan845">public export</tspan><tspan
141+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
142+ y="132.95833"
143+ x="8.7312441"
144+ sodipodi:role="line"
145+ id="tspan847">Lexer : Type</tspan><tspan
146+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
147+ y="138.24998"
148+ x="8.7312441"
149+ sodipodi:role="line"
150+ id="tspan849">Lexer = Recognise True</tspan><tspan
151+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"
152+ y="143.54166"
153+ x="8.7312441"
154+ sodipodi:role="line"
155+ id="tspan851" /></text>
156+ <rect
157+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
158+ id="rect850"
159+ width="111.65417"
160+ height="10.318749"
161+ x="9.7895756"
162+ y="97.504166"
163+ inkscape:export-xdpi="61.120499"
164+ inkscape:export-ydpi="61.120499" />
165+ <rect
166+ y="97.504166"
167+ x="9.7895756"
168+ height="15.610415"
169+ width="111.38958"
170+ id="rect852"
171+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
172+ inkscape:export-xdpi="61.120499"
173+ inkscape:export-ydpi="61.120499" />
174+ <text
175+ inkscape:export-ydpi="61.120499"
176+ inkscape:export-xdpi="61.120499"
177+ id="text870"
178+ y="98.297905"
179+ x="129.64584"
180+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
181+ xml:space="preserve"><tspan
182+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
183+ y="98.297905"
184+ x="129.64584"
185+ sodipodi:role="line"
186+ id="tspan908">(&lt;+&gt;) : Recognise c1 -&gt; inf c1 (Recognise c2) -&gt; </tspan><tspan
187+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
188+ y="103.58957"
189+ x="129.64584"
190+ sodipodi:role="line"
191+ id="tspan929"> Recognise (c1 || c2)</tspan><tspan
192+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
193+ y="108.88124"
194+ x="129.64584"
195+ sodipodi:role="line"
196+ id="tspan916">Sequence two recognisers. If either consumes a</tspan><tspan
197+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
198+ y="114.1729"
199+ x="129.64584"
200+ sodipodi:role="line"
201+ id="tspan918">character, the sequence is guaranteed to</tspan><tspan
202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
203+ y="119.46457"
204+ x="129.64584"
205+ sodipodi:role="line"
206+ id="tspan935">consume a character</tspan><tspan
207+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
208+ y="124.75623"
209+ x="129.64584"
210+ sodipodi:role="line"
211+ id="tspan912" /><tspan
212+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
213+ y="130.04791"
214+ x="129.64584"
215+ sodipodi:role="line"
216+ id="tspan868" /></text>
217+ <path
218+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
219+ d="m 129.38124,100.41458 -7.9375,-2.910414"
220+ id="path937"
221+ inkscape:connector-curvature="0"
222+ sodipodi:nodetypes="cc"
223+ inkscape:export-xdpi="61.120499"
224+ inkscape:export-ydpi="61.120499" />
225+ <text
226+ xml:space="preserve"
227+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
228+ x="130.175"
229+ y="129.25418"
230+ id="text953"
231+ inkscape:export-xdpi="61.120499"
232+ inkscape:export-ydpi="61.120499"><tspan
233+ sodipodi:role="line"
234+ x="130.175"
235+ y="129.25418"
236+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
237+ id="tspan973">(&lt;|&gt;) : Recognise c1 -&gt; Recognise c2 -&gt;</tspan><tspan
238+ sodipodi:role="line"
239+ x="130.175"
240+ y="134.54584"
241+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
242+ id="tspan975"> Recognise (c1 &amp;&amp; c2)</tspan><tspan
243+ sodipodi:role="line"
244+ x="130.175"
245+ y="139.83751"
246+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
247+ id="tspan983">Alternative recognisers. If both consume, the</tspan><tspan
248+ sodipodi:role="line"
249+ x="130.175"
250+ y="145.12917"
251+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
252+ id="tspan985">combination is guaranteed to consumer a</tspan><tspan
253+ sodipodi:role="line"
254+ x="130.175"
255+ y="150.42084"
256+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
257+ id="tspan992">character.</tspan><tspan
258+ sodipodi:role="line"
259+ x="130.175"
260+ y="155.71251"
261+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
262+ id="tspan977" /><tspan
263+ id="tspan949"
264+ sodipodi:role="line"
265+ x="130.175"
266+ y="161.00417"
267+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan
268+ id="tspan951"
269+ sodipodi:role="line"
270+ x="130.175"
271+ y="166.29584"
272+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>
273+ <path
274+ inkscape:connector-curvature="0"
275+ id="path996"
276+ d="M 128.05833,126.87292 110.33125,110.46875"
277+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
278+ sodipodi:nodetypes="cc"
279+ inkscape:export-xdpi="61.120499"
280+ inkscape:export-ydpi="61.120499" />
281+ <text
282+ xml:space="preserve"
283+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
284+ x="28.045837"
285+ y="51.731236"
286+ id="text1012"
287+ inkscape:export-xdpi="61.120499"
288+ inkscape:export-ydpi="61.120499"><tspan
289+ id="tspan1006"
290+ sodipodi:role="line"
291+ x="28.045837"
292+ y="51.731236"
293+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">empty : Recognise False</tspan><tspan
294+ sodipodi:role="line"
295+ x="28.045837"
296+ y="57.022903"
297+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
298+ id="tspan1087">Recognise no input (doesn't consume any input)</tspan><tspan
299+ id="tspan1008"
300+ sodipodi:role="line"
301+ x="28.045837"
302+ y="62.314568"
303+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan
304+ id="tspan1010"
305+ sodipodi:role="line"
306+ x="28.045837"
307+ y="67.606232"
308+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>
309+ <text
310+ inkscape:export-ydpi="61.120499"
311+ inkscape:export-xdpi="61.120499"
312+ id="text1031"
313+ y="49.614574"
314+ x="114.56458"
315+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
316+ xml:space="preserve"><tspan
317+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
318+ y="49.614574"
319+ x="114.56458"
320+ sodipodi:role="line"
321+ id="tspan1025">fail : Recognise c</tspan><tspan
322+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
323+ y="54.906242"
324+ x="114.56458"
325+ sodipodi:role="line"
326+ id="tspan1089">A recogniser that always fails.</tspan><tspan
327+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
328+ y="60.197906"
329+ x="114.56458"
330+ sodipodi:role="line"
331+ id="tspan1027" /><tspan
332+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
333+ y="65.489571"
334+ x="114.56458"
335+ sodipodi:role="line"
336+ id="tspan1029" /></text>
337+ <text
338+ inkscape:export-ydpi="61.120499"
339+ inkscape:export-xdpi="61.120499"
340+ id="text1039"
341+ y="61.785423"
342+ x="128.32292"
343+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
344+ xml:space="preserve"><tspan
345+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
346+ y="61.785423"
347+ x="128.32292"
348+ sodipodi:role="line"
349+ id="tspan1051">expect : Recognise c -&gt; Recognise False</tspan><tspan
350+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
351+ y="67.077087"
352+ x="128.32292"
353+ sodipodi:role="line"
354+ id="tspan1059">Positive lookahead. Never consumes input.</tspan><tspan
355+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
356+ y="72.368759"
357+ x="128.32292"
358+ sodipodi:role="line"
359+ id="tspan1035" /><tspan
360+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
361+ y="77.660423"
362+ x="128.32292"
363+ sodipodi:role="line"
364+ id="tspan1037" /></text>
365+ <text
366+ xml:space="preserve"
367+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
368+ x="125.14791"
369+ y="86.39167"
370+ id="text1047"
371+ inkscape:export-xdpi="61.120499"
372+ inkscape:export-ydpi="61.120499"><tspan
373+ id="tspan1041"
374+ sodipodi:role="line"
375+ x="125.14791"
376+ y="86.39167"
377+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">pred : (Char -&gt; Bool) -&gt; Lexer</tspan><tspan
378+ sodipodi:role="line"
379+ x="125.14791"
380+ y="91.683334"
381+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
382+ id="tspan1085">Recognise a character that matches a predicate</tspan><tspan
383+ id="tspan1043"
384+ sodipodi:role="line"
385+ x="125.14791"
386+ y="96.975006"
387+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan
388+ id="tspan1045"
389+ sodipodi:role="line"
390+ x="125.14791"
391+ y="102.26667"
392+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>
393+ <rect
394+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
395+ id="rect1053"
396+ width="79.904167"
397+ height="23.283327"
398+ x="121.70833"
399+ y="57.816666"
400+ inkscape:export-xdpi="61.120499"
401+ inkscape:export-ydpi="61.120499" />
402+ <text
403+ xml:space="preserve"
404+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
405+ x="128.32291"
406+ y="72.897926"
407+ id="text1069"
408+ inkscape:export-xdpi="61.120499"
409+ inkscape:export-ydpi="61.120499"><tspan
410+ id="tspan1063"
411+ sodipodi:role="line"
412+ x="128.32291"
413+ y="72.897926"
414+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">reject : Recognise c -&gt; Recognise False</tspan><tspan
415+ sodipodi:role="line"
416+ x="128.32291"
417+ y="78.18959"
418+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
419+ id="tspan1073">Negative lookahead. Never consumes input.</tspan><tspan
420+ sodipodi:role="line"
421+ x="128.32291"
422+ y="83.481262"
423+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"
424+ id="tspan1075" /><tspan
425+ id="tspan1065"
426+ sodipodi:role="line"
427+ x="128.32291"
428+ y="88.772926"
429+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan
430+ id="tspan1067"
431+ sodipodi:role="line"
432+ x="128.32291"
433+ y="94.06459"
434+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>
435+ <path
436+ sodipodi:nodetypes="cc"
437+ inkscape:connector-curvature="0"
438+ id="path1081"
439+ d="M 124.35416,89.83125 76.99375,94.858333"
440+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
441+ inkscape:export-xdpi="61.120499"
442+ inkscape:export-ydpi="61.120499" />
443+ <path
444+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
445+ d="M 123.82499,66.01875 112.97708,86.391666"
446+ id="path1083"
447+ inkscape:connector-curvature="0"
448+ sodipodi:nodetypes="cc"
449+ inkscape:export-xdpi="61.120499"
450+ inkscape:export-ydpi="61.120499" />
451+ <path
452+ sodipodi:nodetypes="cc"
453+ inkscape:connector-curvature="0"
454+ id="path1091"
455+ d="M 33.33749,59.139583 20.90208,76.337499"
456+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
457+ inkscape:export-xdpi="61.120499"
458+ inkscape:export-ydpi="61.120499" />
459+ <path
460+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
461+ d="M 113.77082,51.73125 42.068747,83.481249"
462+ id="path1093"
463+ inkscape:connector-curvature="0"
464+ sodipodi:nodetypes="cc"
465+ inkscape:export-xdpi="61.120499"
466+ inkscape:export-ydpi="61.120499" />
467+ <rect
468+ y="94.064583"
469+ x="129.64583"
470+ height="27.51667"
471+ width="78.316658"
472+ id="rect899"
473+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
474+ inkscape:export-xdpi="61.120499"
475+ inkscape:export-ydpi="61.120499" />
476+ </g>
477+</svg>
docs/parserLibrary/lexer.rst+106−76
@@ -1,6 +1,112 @@
11Lexer
22=====
33
4+The lexer is run by calling the 'lex' function in the Text.Lexer.Core
5+module:
6+
7+.. code-block:: idris
8+
9+ lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
10+
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:
13+
14+.. image:: ../image/tokenise.png
15+ :width: 330px
16+ :height: 73px
17+ :alt: diagram illustrating these stages of lexer
18+
19+TokenMap
20+--------
21+
22+In order to construct this list of tokens we need:
23+
24+- A way to recognise the tokens in the input string.
25+- A way to construct these individual tokens.
26+
27+This is given by the TokenMap. This is a mapping from lexers to the tokens they produce. This is a list of pairs:
28+
29+.. code-block:: idris
30+
31+ (Lexer, String -> tokenType)
32+
33+So for each Lexer in the list, if a substring in the input matches, run
34+the associated function to produce a token of type `tokenType`
35+
36+from Text.Lexer.Core:
37+
38+.. code-block:: idris
39+
40+ TokenMap : (tokenType : Type) -> Type
41+ TokenMap tokenType = List (Lexer, String -> tokenType)
42+
43+We can create a tokenMap by using a function like this:
44+
45+.. code-block:: idris
46+
47+ myTokenMap : TokenMap Token
48+ myTokenMap = [(is 'a',CharLit)]
49+
50+Once we have a TokenMap we can use it to lex many strings.
51+
52+Recognisers
53+-----------
54+
55+The first part of each entry in the TokenMap is the recogniser.
56+
57+A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to
58+test whether to accept the character. It can be constructed using the 'is' function:
59+
60+.. code-block:: idris
61+
62+ Idris> :module Lexer2
63+ *Lexer2> is 'a'
64+ Pred (\ARG =>
65+ intToBool (prim__eqChar ARG 'a'))
66+ : Recognise True
67+
68+More complicated structures can be recognised as tokens, this is done using
69+the combinator structure of recognisers. This allows recognisers to be
70+combined, for example,
71+
72+.. list-table::
73+
74+ * - <+> means sequence two recognisers. If either consumes a character, the sequence
75+ is guaranteed to consume a character.
76+
77+ - .. code-block:: idris
78+
79+ *Lexer2> is 'a' <+> is 'b'
80+ SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
81+ (Delay (is 'b')) : Recognise True
82+ *Lexer2>
83+
84+ * - <|> means if both consume, the combination is guaranteed
85+ to consumer a character:
86+
87+ - .. code-block:: idris
88+
89+ *Lexer2> is 'a' <|> is 'b'
90+ Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
91+ (Pred (\ARG => intToBool (prim__eqChar ARG 'b'))) : Recognise True
92+ *Lexer2>
93+
94+
95+.. image:: ../image/recogniser.png
96+ :width: 487px
97+ :height: 249px
98+ :alt: recogniser data structure
99+
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+
107+Simple Expression Example for Lexer
108+-----------------------------------
109+
4110On this page we will implement a lexer to lex a very simple expression, on the
5111next page we will go on to implement a parser for it.
6112
@@ -110,79 +216,3 @@ The lexer uses potentially infinite data structures. It has recursive arguments
110216 (is '(' ,\x => OParen),
111217 (is ')' ,\x => CParen)]
112218
113−Lexer
114−-----
115−
116−.. image:: ../image/tokenise.png
117− :width: 484px
118− :height: 147px
119− :alt: diagram illustrating these stages of lexer and parser
120−
121−To lex some string to a list of tokens we define the structures using recognisers:
122−
123−img src="recogniser.png" alt="recognisers" width="487" height="249"
124−
125−There are constructors and combinators to allow the construction of the lexer definition:
126−
127−A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to test whether to accept the character. It can be constructed using the 'is' function:
128−
129−.. code-block:: idris
130−
131− Idris> :module Lexer2
132− *Lexer2> is 'a'
133− Pred (\ARG =>
134− intToBool (prim__eqChar ARG 'a'))
135− : Recognise True
136−
137−Recognisers can be combined, for example,
138−
139−.. list-table::
140−
141− * - <+> means sequence two recognisers. If either consumes a character, the sequence
142− is guaranteed to consume a character.
143−
144− .. code-block:: idris
145−
146− *Lexer2> is 'a' <+> is 'b'
147− SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
148− (Delay (is 'b')) : Recognise True
149− *Lexer2>
150−
151− - <|> means if both consume, the combination is guaranteed
152− to consumer a character:
153−
154− .. code-block:: idris
155−
156− *Lexer2> is 'a' <|> is 'b'
157− Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))
158− (Pred (\ARG => intToBool (prim__eqChar ARG 'b'))) : Recognise True
159− *Lexer2>
160−
161−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.
162−
163−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.
164−
165−TokenMap
166−--------
167−
168−We then need to generate a TokenMap. This is a mapping from lexers to the tokens they produce. This is a list of pairs:
169−
170−.. code-block:: idris
171−
172− (Lexer, String -> tokenType)
173−
174−For each Lexer in the list, if a substring in the input matches, run
175−the associated function to produce a token of type `tokenType`
176−
177−from Core:
178−
179−.. code-block:: idris
180−
181− TokenMap : (tokenType : Type) -> Type
182− TokenMap tokenType = List (Lexer, String -> tokenType)
183−
184−Here is the code that generates the TokenMap for Idris2 lexer from
185−
186−_`TokenMap for Idris2 lexer`: https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr">src/Parser/Lexer.idr
187−
188−So, for our code, we can then turn this into a tokenMap by using a function like this:.