git.iko.soy/Idris-dev
on master help sign in
add parser library documentation
d86f82emartinbaker
docs/image/parserModules.pngnew file
compare with master
unifiedsplit

Binary file not shown.

docs/image/parserModules.svgnew file+1154
@@ -0,0 +1,1154 @@
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="modules.svg">
19+ <defs
20+ id="defs2">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker1000"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow1Mend">
29+ <path
30+ transform="scale(0.4) rotate(180) translate(10,0)"
31+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
33+ id="path998" />
34+ </marker>
35+ <marker
36+ inkscape:isstock="true"
37+ style="overflow:visible;"
38+ id="marker1127"
39+ refX="0.0"
40+ refY="0.0"
41+ orient="auto"
42+ inkscape:stockid="Arrow1Mend">
43+ <path
44+ transform="scale(0.4) rotate(180) translate(10,0)"
45+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
46+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
47+ id="path1125" />
48+ </marker>
49+ <marker
50+ inkscape:isstock="true"
51+ style="overflow:visible;"
52+ id="marker1123"
53+ refX="0.0"
54+ refY="0.0"
55+ orient="auto"
56+ inkscape:stockid="Arrow1Mend">
57+ <path
58+ transform="scale(0.4) rotate(180) translate(10,0)"
59+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"
60+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
61+ id="path1121" />
62+ </marker>
63+ <marker
64+ inkscape:isstock="true"
65+ style="overflow:visible;"
66+ id="marker1117"
67+ refX="0.0"
68+ refY="0.0"
69+ orient="auto"
70+ inkscape:stockid="Arrow1Mend">
71+ <path
72+ transform="scale(0.4) rotate(180) translate(10,0)"
73+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"
74+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
75+ id="path1115" />
76+ </marker>
77+ <marker
78+ inkscape:stockid="Arrow1Mend"
79+ orient="auto"
80+ refY="0.0"
81+ refX="0.0"
82+ id="marker1111"
83+ style="overflow:visible;"
84+ inkscape:isstock="true"
85+ inkscape:collect="always">
86+ <path
87+ id="path1109"
88+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
89+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"
90+ transform="scale(0.4) rotate(180) translate(10,0)" />
91+ </marker>
92+ <marker
93+ inkscape:isstock="true"
94+ style="overflow:visible;"
95+ id="marker1105"
96+ refX="0.0"
97+ refY="0.0"
98+ orient="auto"
99+ inkscape:stockid="Arrow1Mend"
100+ inkscape:collect="always">
101+ <path
102+ transform="scale(0.4) rotate(180) translate(10,0)"
103+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"
104+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
105+ id="path1103" />
106+ </marker>
107+ <marker
108+ inkscape:isstock="true"
109+ style="overflow:visible;"
110+ id="marker1057"
111+ refX="0.0"
112+ refY="0.0"
113+ orient="auto"
114+ inkscape:stockid="Arrow1Mend">
115+ <path
116+ transform="scale(0.4) rotate(180) translate(10,0)"
117+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
118+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
119+ id="path1055" />
120+ </marker>
121+ <marker
122+ inkscape:stockid="Arrow1Mend"
123+ orient="auto"
124+ refY="0.0"
125+ refX="0.0"
126+ id="marker1045"
127+ style="overflow:visible;"
128+ inkscape:isstock="true"
129+ inkscape:collect="always">
130+ <path
131+ id="path1043"
132+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
133+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
134+ transform="scale(0.4) rotate(180) translate(10,0)" />
135+ </marker>
136+ <marker
137+ inkscape:stockid="Arrow1Mend"
138+ orient="auto"
139+ refY="0.0"
140+ refX="0.0"
141+ id="marker1033"
142+ style="overflow:visible;"
143+ inkscape:isstock="true">
144+ <path
145+ id="path1031"
146+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
147+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
148+ transform="scale(0.4) rotate(180) translate(10,0)" />
149+ </marker>
150+ <marker
151+ inkscape:stockid="Arrow1Mend"
152+ orient="auto"
153+ refY="0.0"
154+ refX="0.0"
155+ id="marker1027"
156+ style="overflow:visible;"
157+ inkscape:isstock="true">
158+ <path
159+ id="path1025"
160+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
161+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
162+ transform="scale(0.4) rotate(180) translate(10,0)" />
163+ </marker>
164+ <marker
165+ inkscape:isstock="true"
166+ style="overflow:visible;"
167+ id="marker1015"
168+ refX="0.0"
169+ refY="0.0"
170+ orient="auto"
171+ inkscape:stockid="Arrow1Mend"
172+ inkscape:collect="always">
173+ <path
174+ transform="scale(0.4) rotate(180) translate(10,0)"
175+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
176+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
177+ id="path1013" />
178+ </marker>
179+ <marker
180+ inkscape:isstock="true"
181+ style="overflow:visible;"
182+ id="marker1009"
183+ refX="0.0"
184+ refY="0.0"
185+ orient="auto"
186+ inkscape:stockid="Arrow1Mend">
187+ <path
188+ transform="scale(0.4) rotate(180) translate(10,0)"
189+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
190+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
191+ id="path1007" />
192+ </marker>
193+ <marker
194+ inkscape:isstock="true"
195+ style="overflow:visible;"
196+ id="marker1003"
197+ refX="0.0"
198+ refY="0.0"
199+ orient="auto"
200+ inkscape:stockid="Arrow1Mend">
201+ <path
202+ transform="scale(0.4) rotate(180) translate(10,0)"
203+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
204+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
205+ id="path1001" />
206+ </marker>
207+ <marker
208+ inkscape:stockid="Arrow1Mend"
209+ orient="auto"
210+ refY="0.0"
211+ refX="0.0"
212+ id="marker997"
213+ style="overflow:visible;"
214+ inkscape:isstock="true"
215+ inkscape:collect="always">
216+ <path
217+ id="path995"
218+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
219+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
220+ transform="scale(0.4) rotate(180) translate(10,0)" />
221+ </marker>
222+ <marker
223+ inkscape:isstock="true"
224+ style="overflow:visible;"
225+ id="marker991"
226+ refX="0.0"
227+ refY="0.0"
228+ orient="auto"
229+ inkscape:stockid="Arrow1Mend"
230+ inkscape:collect="always">
231+ <path
232+ transform="scale(0.4) rotate(180) translate(10,0)"
233+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
234+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
235+ id="path989" />
236+ </marker>
237+ <marker
238+ inkscape:stockid="Arrow1Mend"
239+ orient="auto"
240+ refY="0.0"
241+ refX="0.0"
242+ id="marker967"
243+ style="overflow:visible;"
244+ inkscape:isstock="true"
245+ inkscape:collect="always">
246+ <path
247+ id="path965"
248+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
249+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
250+ transform="scale(0.4) rotate(180) translate(10,0)" />
251+ </marker>
252+ <marker
253+ inkscape:isstock="true"
254+ style="overflow:visible;"
255+ id="marker961"
256+ refX="0.0"
257+ refY="0.0"
258+ orient="auto"
259+ inkscape:stockid="Arrow1Mend"
260+ inkscape:collect="always">
261+ <path
262+ transform="scale(0.4) rotate(180) translate(10,0)"
263+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
264+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
265+ id="path959" />
266+ </marker>
267+ <marker
268+ inkscape:isstock="true"
269+ style="overflow:visible;"
270+ id="marker3617"
271+ refX="0.0"
272+ refY="0.0"
273+ orient="auto"
274+ inkscape:stockid="Arrow1Mend">
275+ <path
276+ transform="scale(0.4) rotate(180) translate(10,0)"
277+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
278+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
279+ id="path3615" />
280+ </marker>
281+ <marker
282+ inkscape:stockid="Arrow1Mend"
283+ orient="auto"
284+ refY="0.0"
285+ refX="0.0"
286+ id="marker2891"
287+ style="overflow:visible;"
288+ inkscape:isstock="true"
289+ inkscape:collect="always">
290+ <path
291+ id="path2889"
292+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
293+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
294+ transform="scale(0.4) rotate(180) translate(10,0)" />
295+ </marker>
296+ <marker
297+ inkscape:stockid="Arrow1Mend"
298+ orient="auto"
299+ refY="0.0"
300+ refX="0.0"
301+ id="marker2049"
302+ style="overflow:visible;"
303+ inkscape:isstock="true"
304+ inkscape:collect="always">
305+ <path
306+ id="path2047"
307+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
308+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
309+ transform="scale(0.4) rotate(180) translate(10,0)" />
310+ </marker>
311+ <marker
312+ inkscape:isstock="true"
313+ style="overflow:visible;"
314+ id="marker1539"
315+ refX="0.0"
316+ refY="0.0"
317+ orient="auto"
318+ inkscape:stockid="Arrow1Mend"
319+ inkscape:collect="always">
320+ <path
321+ transform="scale(0.4) rotate(180) translate(10,0)"
322+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
323+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
324+ id="path1537" />
325+ </marker>
326+ <marker
327+ inkscape:stockid="Arrow1Mend"
328+ orient="auto"
329+ refY="0.0"
330+ refX="0.0"
331+ id="Arrow1Mend"
332+ style="overflow:visible;"
333+ inkscape:isstock="true"
334+ inkscape:collect="always">
335+ <path
336+ id="path830"
337+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
338+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
339+ transform="scale(0.4) rotate(180) translate(10,0)" />
340+ </marker>
341+ </defs>
342+ <sodipodi:namedview
343+ id="base"
344+ pagecolor="#ffffff"
345+ bordercolor="#666666"
346+ borderopacity="1.0"
347+ inkscape:pageopacity="0.0"
348+ inkscape:pageshadow="2"
349+ inkscape:zoom="1"
350+ inkscape:cx="368.33949"
351+ inkscape:cy="554.8721"
352+ inkscape:document-units="mm"
353+ inkscape:current-layer="layer1"
354+ showgrid="false"
355+ inkscape:window-width="1359"
356+ inkscape:window-height="1011"
357+ inkscape:window-x="-4"
358+ inkscape:window-y="0"
359+ inkscape:window-maximized="0" />
360+ <metadata
361+ id="metadata5">
362+ <rdf:RDF>
363+ <cc:Work
364+ rdf:about="">
365+ <dc:format>image/svg+xml</dc:format>
366+ <dc:type
367+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
368+ <dc:title />
369+ </cc:Work>
370+ </rdf:RDF>
371+ </metadata>
372+ <g
373+ inkscape:label="Layer 1"
374+ inkscape:groupmode="layer"
375+ id="layer1">
376+ <rect
377+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
378+ id="rect815"
379+ width="35.983334"
380+ height="18.25625"
381+ x="37.835415"
382+ y="52.260437"
383+ inkscape:export-xdpi="61.120499"
384+ inkscape:export-ydpi="61.120499" />
385+ <rect
386+ y="52.260437"
387+ x="92.868744"
388+ height="18.25625"
389+ width="35.983334"
390+ id="rect817"
391+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
392+ inkscape:export-xdpi="61.120499"
393+ inkscape:export-ydpi="61.120499" />
394+ <path
395+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
396+ d="m 74.083333,61.25627 16.66875,-0.26459"
397+ id="path819"
398+ inkscape:connector-curvature="0"
399+ inkscape:export-xdpi="61.120499"
400+ inkscape:export-ydpi="61.120499" />
401+ <path
402+ inkscape:connector-curvature="0"
403+ id="path1535"
404+ d="m 19.314583,61.520853 16.66875,-0.26459"
405+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1539)"
406+ inkscape:export-xdpi="61.120499"
407+ inkscape:export-ydpi="61.120499" />
408+ <path
409+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2049)"
410+ d="m 128.85208,60.991686 16.66875,-0.26459"
411+ id="path2045"
412+ inkscape:connector-curvature="0"
413+ inkscape:export-xdpi="61.120499"
414+ inkscape:export-ydpi="61.120499" />
415+ <text
416+ xml:space="preserve"
417+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
418+ x="20.902082"
419+ y="58.345871"
420+ id="text2857"
421+ inkscape:export-xdpi="61.120499"
422+ inkscape:export-ydpi="61.120499"><tspan
423+ sodipodi:role="line"
424+ id="tspan2855"
425+ x="20.902082"
426+ y="58.345871"
427+ 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">String</tspan></text>
428+ <text
429+ id="text2861"
430+ y="53.583374"
431+ x="76.729164"
432+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
433+ xml:space="preserve"
434+ inkscape:export-xdpi="61.120499"
435+ inkscape:export-ydpi="61.120499"><tspan
436+ 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"
437+ y="53.583374"
438+ x="76.729164"
439+ sodipodi:role="line"
440+ id="tspan2867">List</tspan><tspan
441+ 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"
442+ y="58.875042"
443+ x="76.729164"
444+ sodipodi:role="line"
445+ id="tspan2871">Token</tspan></text>
446+ <text
447+ xml:space="preserve"
448+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
449+ x="131.49791"
450+ y="57.816704"
451+ id="text2865"
452+ inkscape:export-xdpi="61.120499"
453+ inkscape:export-ydpi="61.120499"><tspan
454+ sodipodi:role="line"
455+ id="tspan2863"
456+ x="131.49791"
457+ y="57.816704"
458+ 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">PTerm</tspan></text>
459+ <text
460+ id="text2875"
461+ y="62.050041"
462+ x="47.889584"
463+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
464+ xml:space="preserve"
465+ inkscape:export-xdpi="61.120499"
466+ inkscape:export-ydpi="61.120499"><tspan
467+ 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:#0000ff;stroke-width:0.26458332"
468+ y="62.050041"
469+ x="47.889584"
470+ id="tspan2873"
471+ sodipodi:role="line">Lexer</tspan></text>
472+ <text
473+ xml:space="preserve"
474+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
475+ x="100.80624"
476+ y="61.785461"
477+ id="text2879"
478+ inkscape:export-xdpi="61.120499"
479+ inkscape:export-ydpi="61.120499"><tspan
480+ sodipodi:role="line"
481+ id="tspan2877"
482+ x="100.80624"
483+ y="61.785461"
484+ 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:#0000ff;stroke-width:0.26458332">Parser</tspan></text>
485+ <path
486+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2891)"
487+ d="m 53.445833,44.322936 v 7.67291"
488+ id="path2887"
489+ inkscape:connector-curvature="0"
490+ sodipodi:nodetypes="cc"
491+ inkscape:export-xdpi="61.120499"
492+ inkscape:export-ydpi="61.120499" />
493+ <path
494+ sodipodi:nodetypes="cc"
495+ inkscape:connector-curvature="0"
496+ id="path3613"
497+ d="m 109.27292,44.322936 v 7.67291"
498+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker3617)"
499+ inkscape:export-xdpi="61.120499"
500+ inkscape:export-ydpi="61.120499" />
501+ <text
502+ id="text4173"
503+ y="42.735458"
504+ x="43.920834"
505+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
506+ xml:space="preserve"
507+ inkscape:export-xdpi="61.120499"
508+ inkscape:export-ydpi="61.120499"><tspan
509+ 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"
510+ y="42.735458"
511+ x="43.920834"
512+ id="tspan4171"
513+ sodipodi:role="line">Recogniser</tspan></text>
514+ <text
515+ xml:space="preserve"
516+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
517+ x="97.631248"
518+ y="42.470879"
519+ id="text4177"
520+ inkscape:export-xdpi="61.120499"
521+ inkscape:export-ydpi="61.120499"><tspan
522+ sodipodi:role="line"
523+ id="tspan4175"
524+ x="97.631248"
525+ y="42.470879"
526+ 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">Grammar</tspan></text>
527+ <text
528+ inkscape:export-ydpi="61.120499"
529+ inkscape:export-xdpi="61.120499"
530+ id="text854"
531+ y="119.72919"
532+ x="131.23334"
533+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
534+ xml:space="preserve"><tspan
535+ 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"
536+ y="129.46077"
537+ x="131.23334"
538+ id="tspan852"
539+ sodipodi:role="line" /></text>
540+ <rect
541+ inkscape:export-ydpi="61.120499"
542+ inkscape:export-xdpi="61.120499"
543+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
544+ id="rect875"
545+ width="43.656246"
546+ height="18.520832"
547+ x="92.339577"
548+ y="110.20418" />
549+ <path
550+ inkscape:export-ydpi="61.120499"
551+ inkscape:export-xdpi="61.120499"
552+ inkscape:connector-curvature="0"
553+ id="path881"
554+ d="m 135.73129,118.93554 16.66875,-0.26459"
555+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2049)" />
556+ <text
557+ inkscape:export-ydpi="61.120499"
558+ inkscape:export-xdpi="61.120499"
559+ id="text895"
560+ y="115.76046"
561+ x="138.37698"
562+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
563+ xml:space="preserve"><tspan
564+ 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"
565+ y="115.76046"
566+ x="138.37698"
567+ id="tspan893"
568+ sodipodi:role="line">PTerm</tspan></text>
569+ <text
570+ inkscape:export-ydpi="61.120499"
571+ inkscape:export-xdpi="61.120499"
572+ id="text903"
573+ y="115.23129"
574+ x="93.927078"
575+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
576+ xml:space="preserve"><tspan
577+ 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:#0000ff;stroke-width:0.26458332"
578+ y="115.23129"
579+ x="93.927078"
580+ id="tspan901"
581+ sodipodi:role="line">module Idris.Parser</tspan><tspan
582+ 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:#0000ff;stroke-width:0.26458332"
583+ y="128.46045"
584+ x="93.927078"
585+ sodipodi:role="line"
586+ id="tspan1021" /></text>
587+ <rect
588+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
589+ id="rect905"
590+ width="44.185421"
591+ height="18.785423"
592+ x="40.463421"
593+ y="141.50723"
594+ inkscape:export-xdpi="61.120499"
595+ inkscape:export-ydpi="61.120499" />
596+ <rect
597+ y="155.183"
598+ x="95.51458"
599+ height="18.256256"
600+ width="49.212498"
601+ id="rect907"
602+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
603+ inkscape:export-xdpi="61.120499"
604+ inkscape:export-ydpi="61.120499" />
605+ <path
606+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker961)"
607+ d="m 84.648837,152.88468 9.013662,7.32603"
608+ id="path909"
609+ inkscape:connector-curvature="0"
610+ inkscape:export-xdpi="61.120499"
611+ inkscape:export-ydpi="61.120499"
612+ sodipodi:nodetypes="cc" />
613+ <path
614+ inkscape:connector-curvature="0"
615+ id="path911"
616+ d="m 22.471756,152.09108 16.66875,-0.26459"
617+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1539)"
618+ inkscape:export-xdpi="61.120499"
619+ inkscape:export-ydpi="61.120499" />
620+ <text
621+ xml:space="preserve"
622+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
623+ x="24.059256"
624+ y="148.91547"
625+ id="text917"
626+ inkscape:export-xdpi="61.120499"
627+ inkscape:export-ydpi="61.120499"><tspan
628+ sodipodi:role="line"
629+ id="tspan915"
630+ x="24.059256"
631+ y="148.91547"
632+ 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">String</tspan></text>
633+ <text
634+ id="text923"
635+ y="137.72075"
636+ x="65.087494"
637+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
638+ xml:space="preserve"
639+ inkscape:export-xdpi="61.120499"
640+ inkscape:export-ydpi="61.120499"><tspan
641+ 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"
642+ y="137.72075"
643+ x="65.087494"
644+ sodipodi:role="line"
645+ id="tspan921">List (TokenData Token)</tspan></text>
646+ <text
647+ id="text931"
648+ y="184.2872"
649+ x="37.041664"
650+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
651+ xml:space="preserve"
652+ inkscape:export-xdpi="61.120499"
653+ inkscape:export-ydpi="61.120499"><tspan
654+ 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:#0000ff;stroke-width:0.26458332"
655+ y="184.2872"
656+ x="37.041664"
657+ id="tspan929"
658+ sodipodi:role="line">module Text.Lexer</tspan></text>
659+ <text
660+ xml:space="preserve"
661+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
662+ x="98.160408"
663+ y="161.00386"
664+ id="text935"
665+ inkscape:export-xdpi="61.120499"
666+ inkscape:export-ydpi="61.120499"><tspan
667+ sodipodi:role="line"
668+ id="tspan933"
669+ x="98.160408"
670+ y="161.00386"
671+ 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:#0000ff;stroke-width:0.26458332">module Parser.Support</tspan></text>
672+ <rect
673+ inkscape:export-ydpi="61.120499"
674+ inkscape:export-xdpi="61.120499"
675+ y="180.05362"
676+ x="32.543747"
677+ height="6.3500061"
678+ width="43.656254"
679+ id="rect937"
680+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
681+ <rect
682+ inkscape:export-ydpi="61.120499"
683+ inkscape:export-xdpi="61.120499"
684+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
685+ id="rect939"
686+ width="42.862495"
687+ height="6.8791728"
688+ x="95.51458"
689+ y="180.05362" />
690+ <text
691+ inkscape:export-ydpi="61.120499"
692+ inkscape:export-xdpi="61.120499"
693+ xml:space="preserve"
694+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
695+ x="42.31551"
696+ y="147.59224"
697+ id="text951"><tspan
698+ sodipodi:role="line"
699+ id="tspan949"
700+ x="42.31551"
701+ y="147.59224"
702+ 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:#0000ff;stroke-width:0.26458332">module Parser.Lexer</tspan></text>
703+ <path
704+ sodipodi:nodetypes="cc"
705+ inkscape:export-ydpi="61.120499"
706+ inkscape:export-xdpi="61.120499"
707+ inkscape:connector-curvature="0"
708+ id="path963"
709+ d="m 53.828728,179.89081 1.006873,-18.52084"
710+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker967)" />
711+ <text
712+ inkscape:export-ydpi="61.120499"
713+ inkscape:export-xdpi="61.120499"
714+ xml:space="preserve"
715+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
716+ x="23.749693"
717+ y="216.88524"
718+ id="text971"><tspan
719+ sodipodi:role="line"
720+ id="tspan969"
721+ x="23.749693"
722+ y="216.88524"
723+ 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:#0000ff;stroke-width:0.26458332">module Text.Lexer.Core</tspan></text>
724+ <rect
725+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
726+ id="rect973"
727+ width="47.889587"
728+ height="6.3500061"
729+ x="22.162193"
730+ y="212.38707"
731+ inkscape:export-xdpi="61.120499"
732+ inkscape:export-ydpi="61.120499" />
733+ <path
734+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker991)"
735+ d="m 48.898483,194.70748 0.04943,-6.71548"
736+ id="path975"
737+ inkscape:connector-curvature="0"
738+ inkscape:export-xdpi="61.120499"
739+ inkscape:export-ydpi="61.120499"
740+ sodipodi:nodetypes="cc" />
741+ <text
742+ id="text979"
743+ y="207.83517"
744+ x="23.812496"
745+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
746+ xml:space="preserve"
747+ inkscape:export-xdpi="61.120499"
748+ inkscape:export-ydpi="61.120499"><tspan
749+ 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:#0000ff;stroke-width:0.26458332"
750+ y="207.83517"
751+ x="23.812496"
752+ id="tspan977"
753+ sodipodi:role="line">module Text.Quantity</tspan></text>
754+ <rect
755+ inkscape:export-ydpi="61.120499"
756+ inkscape:export-xdpi="61.120499"
757+ y="203.33701"
758+ x="22.224997"
759+ height="6.2469702"
760+ width="43.853985"
761+ id="rect981"
762+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
763+ <text
764+ inkscape:export-ydpi="61.120499"
765+ inkscape:export-xdpi="61.120499"
766+ xml:space="preserve"
767+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
768+ x="23.711607"
769+ y="199.55397"
770+ id="text985"><tspan
771+ sodipodi:role="line"
772+ id="tspan983"
773+ x="23.711607"
774+ y="199.55397"
775+ 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:#0000ff;stroke-width:0.26458332">module Text.Token</tspan></text>
776+ <rect
777+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
778+ id="rect987"
779+ width="39.011257"
780+ height="5.9464455"
781+ x="22.124107"
782+ y="195.0558"
783+ inkscape:export-xdpi="61.120499"
784+ inkscape:export-ydpi="61.120499" />
785+ <path
786+ sodipodi:nodetypes="cc"
787+ inkscape:export-ydpi="61.120499"
788+ inkscape:export-xdpi="61.120499"
789+ inkscape:connector-curvature="0"
790+ id="path993"
791+ d="M 63.527551,202.87958 63.375204,187.79022"
792+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker997)" />
793+ <path
794+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1003)"
795+ d="M 67.865826,212.16147 67.612589,187.58844"
796+ id="path999"
797+ inkscape:connector-curvature="0"
798+ inkscape:export-xdpi="61.120499"
799+ inkscape:export-ydpi="61.120499"
800+ sodipodi:nodetypes="cc" />
801+ <path
802+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1009)"
803+ d="M 74.466241,179.89081 95.51458,173.43977"
804+ id="path1005"
805+ inkscape:connector-curvature="0"
806+ inkscape:export-xdpi="61.120499"
807+ inkscape:export-ydpi="61.120499"
808+ sodipodi:nodetypes="cc" />
809+ <path
810+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1015)"
811+ d="m 113.36007,180.68456 -0.0515,-6.61459"
812+ id="path1011"
813+ inkscape:connector-curvature="0"
814+ inkscape:export-xdpi="61.120499"
815+ inkscape:export-ydpi="61.120499"
816+ sodipodi:nodetypes="cc" />
817+ <text
818+ inkscape:export-ydpi="61.120499"
819+ inkscape:export-xdpi="61.120499"
820+ id="text1019"
821+ y="184.81636"
822+ x="97.366661"
823+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
824+ xml:space="preserve"><tspan
825+ 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:#0000ff;stroke-width:0.26458332"
826+ y="184.81636"
827+ x="97.366661"
828+ id="tspan1017"
829+ sodipodi:role="line">module Text.Parser</tspan></text>
830+ <path
831+ sodipodi:nodetypes="cc"
832+ inkscape:export-ydpi="61.120499"
833+ inkscape:export-xdpi="61.120499"
834+ inkscape:connector-curvature="0"
835+ id="path1023"
836+ d="m 113.62466,154.75539 0.0397,-25.06978"
837+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1027)" />
838+ <path
839+ sodipodi:nodetypes="cc"
840+ inkscape:export-ydpi="61.120499"
841+ inkscape:export-xdpi="61.120499"
842+ inkscape:connector-curvature="0"
843+ id="path1029"
844+ d="M 83.757032,147.15485 97.991855,129.77582"
845+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1033)" />
846+ <rect
847+ y="142.91107"
848+ x="118.15033"
849+ height="6.6968417"
850+ width="45.2328"
851+ id="rect1035"
852+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
853+ inkscape:export-xdpi="61.120499"
854+ inkscape:export-ydpi="61.120499" />
855+ <path
856+ sodipodi:nodetypes="cc"
857+ inkscape:export-ydpi="61.120499"
858+ inkscape:export-xdpi="61.120499"
859+ inkscape:connector-curvature="0"
860+ id="path1037"
861+ d="m 121.83513,142.5835 -0.0515,-12.72267"
862+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1057)" />
863+ <text
864+ xml:space="preserve"
865+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
866+ x="120.00241"
867+ y="147.67372"
868+ id="text1041"
869+ inkscape:export-xdpi="61.120499"
870+ inkscape:export-ydpi="61.120499"><tspan
871+ sodipodi:role="line"
872+ id="tspan1039"
873+ x="120.00241"
874+ y="147.67372"
875+ 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:#0000ff;stroke-width:0.26458332">module TTImp.TTImp</tspan></text>
876+ <rect
877+ inkscape:export-ydpi="61.120499"
878+ inkscape:export-xdpi="61.120499"
879+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
880+ id="rect1047"
881+ width="42.862495"
882+ height="6.8791728"
883+ x="125.28364"
884+ y="133.0603" />
885+ <path
886+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1045)"
887+ d="m 145.18016,132.82376 -9.18434,-4.09859"
888+ id="path1049"
889+ inkscape:connector-curvature="0"
890+ inkscape:export-xdpi="61.120499"
891+ inkscape:export-ydpi="61.120499"
892+ sodipodi:nodetypes="cc" />
893+ <text
894+ inkscape:export-ydpi="61.120499"
895+ inkscape:export-xdpi="61.120499"
896+ id="text1053"
897+ y="137.82295"
898+ x="127.13572"
899+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
900+ xml:space="preserve"><tspan
901+ 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:#0000ff;stroke-width:0.26458332"
902+ y="137.82295"
903+ x="127.13572"
904+ id="tspan1051"
905+ sodipodi:role="line">module Idris.Syntax</tspan></text>
906+ <rect
907+ inkscape:export-ydpi="61.120499"
908+ inkscape:export-xdpi="61.120499"
909+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#00871c;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
910+ id="rect1061"
911+ width="59.266659"
912+ height="16.13958"
913+ x="92.339577"
914+ y="230.5896" />
915+ <path
916+ inkscape:export-ydpi="61.120499"
917+ inkscape:export-xdpi="61.120499"
918+ inkscape:connector-curvature="0"
919+ id="path1063"
920+ d="m 76.993749,160.21044 21.695834,69.32083"
921+ style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1105)"
922+ sodipodi:nodetypes="cc" />
923+ <text
924+ inkscape:export-ydpi="61.120499"
925+ inkscape:export-xdpi="61.120499"
926+ id="text1081"
927+ y="236.14587"
928+ x="153.19336"
929+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#008000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
930+ xml:space="preserve"><tspan
931+ 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:#008000;stroke-width:0.26458332"
932+ y="236.14587"
933+ x="153.19336"
934+ id="tspan1079"
935+ sodipodi:role="line">Either ParseError SExp</tspan></text>
936+ <text
937+ inkscape:export-ydpi="61.120499"
938+ inkscape:export-xdpi="61.120499"
939+ id="text1089"
940+ y="236.41046"
941+ x="94.191658"
942+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#008000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"
943+ xml:space="preserve"><tspan
944+ 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:#008000;stroke-width:0.26458332;"
945+ y="236.41046"
946+ x="94.191658"
947+ id="tspan1087"
948+ sodipodi:role="line">module Idris.IDEMode.Parser</tspan></text>
949+ <rect
950+ inkscape:export-ydpi="61.120499"
951+ inkscape:export-xdpi="61.120499"
952+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
953+ id="rect1097"
954+ width="35.983334"
955+ height="18.25625"
956+ x="124.08953"
957+ y="18.393738" />
958+ <text
959+ inkscape:export-ydpi="61.120499"
960+ inkscape:export-xdpi="61.120499"
961+ id="text1101"
962+ y="24.479179"
963+ x="126.99989"
964+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
965+ xml:space="preserve"><tspan
966+ 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:#0000ff;stroke-width:0.26458332"
967+ y="24.479179"
968+ x="126.99989"
969+ id="tspan1099"
970+ sodipodi:role="line">module Idris.REPL</tspan></text>
971+ <path
972+ sodipodi:nodetypes="cc"
973+ style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1111)"
974+ d="m 112.97708,187.46252 0.52917,41.80417"
975+ id="path1107"
976+ inkscape:connector-curvature="0"
977+ inkscape:export-xdpi="61.120499"
978+ inkscape:export-ydpi="61.120499" />
979+ <path
980+ inkscape:export-ydpi="61.120499"
981+ inkscape:export-xdpi="61.120499"
982+ inkscape:connector-curvature="0"
983+ id="path1113"
984+ d="m 144.72708,173.43925 -0.26458,56.35661"
985+ style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1117)"
986+ sodipodi:nodetypes="cc" />
987+ <path
988+ inkscape:export-ydpi="61.120499"
989+ inkscape:export-xdpi="61.120499"
990+ inkscape:connector-curvature="0"
991+ id="path1119"
992+ d="m 151.80639,239.22321 44.91435,-0.41532"
993+ style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1123)"
994+ sodipodi:nodetypes="cc" />
995+ <text
996+ id="text950"
997+ y="236.19983"
998+ x="22.69136"
999+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1000+ xml:space="preserve"
1001+ inkscape:export-xdpi="61.120499"
1002+ inkscape:export-ydpi="61.120499"><tspan
1003+ 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:#0000ff;stroke-width:0.26458332"
1004+ y="236.19983"
1005+ x="22.69136"
1006+ id="tspan948"
1007+ sodipodi:role="line">module Core.Core</tspan></text>
1008+ <rect
1009+ inkscape:export-ydpi="61.120499"
1010+ inkscape:export-xdpi="61.120499"
1011+ y="231.70166"
1012+ x="21.103861"
1013+ height="9.7895899"
1014+ width="47.889587"
1015+ id="rect952"
1016+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
1017+ <text
1018+ inkscape:export-ydpi="61.120499"
1019+ inkscape:export-xdpi="61.120499"
1020+ xml:space="preserve"
1021+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1022+ x="23.220528"
1023+ y="239.90399"
1024+ id="text956"><tspan
1025+ sodipodi:role="line"
1026+ id="tspan954"
1027+ x="23.220528"
1028+ y="239.90399"
1029+ 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:#000000;stroke-width:0.26458332">error messages</tspan></text>
1030+ <text
1031+ inkscape:export-ydpi="61.120499"
1032+ inkscape:export-xdpi="61.120499"
1033+ xml:space="preserve"
1034+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1035+ x="22.69136"
1036+ y="252.33942"
1037+ id="text960"><tspan
1038+ sodipodi:role="line"
1039+ id="tspan958"
1040+ x="22.69136"
1041+ y="252.33942"
1042+ 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:#0000ff;stroke-width:0.26458332">module Core.CompileExpr</tspan></text>
1043+ <rect
1044+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
1045+ id="rect962"
1046+ width="61.912495"
1047+ height="18.785419"
1048+ x="21.103861"
1049+ y="247.84125"
1050+ inkscape:export-xdpi="61.120499"
1051+ inkscape:export-ydpi="61.120499" />
1052+ <text
1053+ id="text966"
1054+ y="256.04358"
1055+ x="23.220528"
1056+ style="font-style:normal;font-weight:normal;font-size:3.52777767px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1057+ xml:space="preserve"
1058+ inkscape:export-xdpi="61.120499"
1059+ inkscape:export-ydpi="61.120499"><tspan
1060+ 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:#000000;stroke-width:0.26458332"
1061+ y="256.04358"
1062+ x="23.220528"
1063+ sodipodi:role="line"
1064+ id="tspan968">Representation of expressions ready</tspan><tspan
1065+ 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:#000000;stroke-width:0.26458332"
1066+ y="260.45331"
1067+ x="23.220528"
1068+ sodipodi:role="line"
1069+ id="tspan974">for compiling: CExp</tspan><tspan
1070+ 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:#000000;stroke-width:0.26458332"
1071+ y="264.86304"
1072+ x="23.220528"
1073+ sodipodi:role="line"
1074+ id="tspan972">Type erased, explicit case trees</tspan></text>
1075+ <text
1076+ inkscape:export-ydpi="61.120499"
1077+ inkscape:export-xdpi="61.120499"
1078+ xml:space="preserve"
1079+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1080+ x="22.69136"
1081+ y="90.151314"
1082+ id="text978"><tspan
1083+ sodipodi:role="line"
1084+ id="tspan976"
1085+ x="22.69136"
1086+ y="90.151314"
1087+ 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:#0000ff;stroke-width:0.26458332">module Idris.CommandLine</tspan></text>
1088+ <rect
1089+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
1090+ id="rect980"
1091+ width="55.827087"
1092+ height="10.054173"
1093+ x="21.103861"
1094+ y="85.653076"
1095+ inkscape:export-xdpi="61.120499"
1096+ inkscape:export-ydpi="61.120499" />
1097+ <text
1098+ id="text984"
1099+ y="93.855484"
1100+ x="23.220528"
1101+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1102+ xml:space="preserve"
1103+ inkscape:export-xdpi="61.120499"
1104+ inkscape:export-ydpi="61.120499"><tspan
1105+ 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:#000000;stroke-width:0.26458332"
1106+ y="93.855484"
1107+ x="23.220528"
1108+ id="tspan982"
1109+ sodipodi:role="line">command line options</tspan></text>
1110+ <text
1111+ id="text988"
1112+ y="106.82006"
1113+ x="22.69136"
1114+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1115+ xml:space="preserve"
1116+ inkscape:export-xdpi="61.120499"
1117+ inkscape:export-ydpi="61.120499"><tspan
1118+ 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:#0000ff;stroke-width:0.26458332"
1119+ y="106.82006"
1120+ x="22.69136"
1121+ id="tspan986"
1122+ sodipodi:role="line">module Idris.Error</tspan></text>
1123+ <rect
1124+ inkscape:export-ydpi="61.120499"
1125+ inkscape:export-xdpi="61.120499"
1126+ y="102.32182"
1127+ x="21.103861"
1128+ height="9.5250101"
1129+ width="37.835419"
1130+ id="rect990"
1131+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
1132+ <text
1133+ inkscape:export-ydpi="61.120499"
1134+ inkscape:export-xdpi="61.120499"
1135+ xml:space="preserve"
1136+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1137+ x="23.220528"
1138+ y="110.52423"
1139+ id="text994"><tspan
1140+ sodipodi:role="line"
1141+ id="tspan992"
1142+ x="23.220528"
1143+ y="110.52423"
1144+ 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:#000000;stroke-width:0.26458332">perror</tspan></text>
1145+ <path
1146+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1000)"
1147+ d="m 21.103861,231.70166 c -7.32197,0.078 -4.584313,-108.27557 0,-119.85483"
1148+ id="path996"
1149+ inkscape:connector-curvature="0"
1150+ inkscape:export-xdpi="61.120499"
1151+ inkscape:export-ydpi="61.120499"
1152+ sodipodi:nodetypes="cc" />
1153+ </g>
1154+</svg>
docs/image/parserTopLevel.pngnew file

Binary file not shown.

docs/image/parserTopLevel.svgnew file+294
@@ -0,0 +1,294 @@
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="topLevel.svg">
19+ <defs
20+ id="defs2">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker3617"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow1Mend">
29+ <path
30+ transform="scale(0.4) rotate(180) translate(10,0)"
31+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
33+ id="path3615" />
34+ </marker>
35+ <marker
36+ inkscape:stockid="Arrow1Mend"
37+ orient="auto"
38+ refY="0.0"
39+ refX="0.0"
40+ id="marker2891"
41+ style="overflow:visible;"
42+ inkscape:isstock="true"
43+ inkscape:collect="always">
44+ <path
45+ id="path2889"
46+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
47+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
48+ transform="scale(0.4) rotate(180) translate(10,0)" />
49+ </marker>
50+ <marker
51+ inkscape:stockid="Arrow1Mend"
52+ orient="auto"
53+ refY="0.0"
54+ refX="0.0"
55+ id="marker2049"
56+ style="overflow:visible;"
57+ inkscape:isstock="true">
58+ <path
59+ id="path2047"
60+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
61+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
62+ transform="scale(0.4) rotate(180) translate(10,0)" />
63+ </marker>
64+ <marker
65+ inkscape:isstock="true"
66+ style="overflow:visible;"
67+ id="marker1539"
68+ refX="0.0"
69+ refY="0.0"
70+ orient="auto"
71+ inkscape:stockid="Arrow1Mend"
72+ inkscape:collect="always">
73+ <path
74+ transform="scale(0.4) rotate(180) translate(10,0)"
75+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
76+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
77+ id="path1537" />
78+ </marker>
79+ <marker
80+ inkscape:stockid="Arrow1Mend"
81+ orient="auto"
82+ refY="0.0"
83+ refX="0.0"
84+ id="Arrow1Mend"
85+ style="overflow:visible;"
86+ inkscape:isstock="true"
87+ inkscape:collect="always">
88+ <path
89+ id="path830"
90+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
91+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"
92+ transform="scale(0.4) rotate(180) translate(10,0)" />
93+ </marker>
94+ </defs>
95+ <sodipodi:namedview
96+ id="base"
97+ pagecolor="#ffffff"
98+ bordercolor="#666666"
99+ borderopacity="1.0"
100+ inkscape:pageopacity="0.0"
101+ inkscape:pageshadow="2"
102+ inkscape:zoom="1"
103+ inkscape:cx="396.85039"
104+ inkscape:cy="560"
105+ inkscape:document-units="mm"
106+ inkscape:current-layer="layer1"
107+ showgrid="false"
108+ inkscape:window-width="1920"
109+ inkscape:window-height="1015"
110+ inkscape:window-x="0"
111+ inkscape:window-y="0"
112+ inkscape:window-maximized="1" />
113+ <metadata
114+ id="metadata5">
115+ <rdf:RDF>
116+ <cc:Work
117+ rdf:about="">
118+ <dc:format>image/svg+xml</dc:format>
119+ <dc:type
120+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
121+ <dc:title />
122+ </cc:Work>
123+ </rdf:RDF>
124+ </metadata>
125+ <g
126+ inkscape:label="Layer 1"
127+ inkscape:groupmode="layer"
128+ id="layer1">
129+ <rect
130+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
131+ id="rect815"
132+ width="35.983334"
133+ height="18.25625"
134+ x="37.306248"
135+ y="79.512497"
136+ inkscape:export-xdpi="61.120499"
137+ inkscape:export-ydpi="61.120499" />
138+ <rect
139+ y="79.512497"
140+ x="92.339577"
141+ height="18.25625"
142+ width="35.983334"
143+ id="rect817"
144+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
145+ inkscape:export-xdpi="61.120499"
146+ inkscape:export-ydpi="61.120499" />
147+ <path
148+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
149+ d="m 73.554166,88.508337 16.66875,-0.26459"
150+ id="path819"
151+ inkscape:connector-curvature="0"
152+ inkscape:export-xdpi="61.120499"
153+ inkscape:export-ydpi="61.120499" />
154+ <path
155+ inkscape:connector-curvature="0"
156+ id="path1535"
157+ d="m 18.785416,88.77292 16.66875,-0.26459"
158+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1539)"
159+ inkscape:export-xdpi="61.120499"
160+ inkscape:export-ydpi="61.120499" />
161+ <path
162+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2049)"
163+ d="m 128.32291,88.243753 16.66875,-0.26459"
164+ id="path2045"
165+ inkscape:connector-curvature="0"
166+ inkscape:export-xdpi="61.120499"
167+ inkscape:export-ydpi="61.120499" />
168+ <text
169+ xml:space="preserve"
170+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
171+ x="20.372915"
172+ y="85.597931"
173+ id="text2857"
174+ inkscape:export-xdpi="61.120499"
175+ inkscape:export-ydpi="61.120499"><tspan
176+ sodipodi:role="line"
177+ id="tspan2855"
178+ x="20.372915"
179+ y="85.597931"
180+ 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">String</tspan></text>
181+ <text
182+ id="text2861"
183+ y="80.835434"
184+ x="76.199997"
185+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
186+ xml:space="preserve"
187+ inkscape:export-xdpi="61.120499"
188+ inkscape:export-ydpi="61.120499"><tspan
189+ 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"
190+ y="80.835434"
191+ x="76.199997"
192+ sodipodi:role="line"
193+ id="tspan2867">List</tspan><tspan
194+ 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"
195+ y="86.127098"
196+ x="76.199997"
197+ sodipodi:role="line"
198+ id="tspan2871">Token</tspan></text>
199+ <text
200+ xml:space="preserve"
201+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
202+ x="130.96875"
203+ y="85.068764"
204+ id="text2865"
205+ inkscape:export-xdpi="61.120499"
206+ inkscape:export-ydpi="61.120499"><tspan
207+ sodipodi:role="line"
208+ id="tspan2863"
209+ x="130.96875"
210+ y="85.068764"
211+ 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">PTerm</tspan></text>
212+ <text
213+ id="text2875"
214+ y="89.302101"
215+ x="47.360416"
216+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332;"
217+ xml:space="preserve"
218+ inkscape:export-xdpi="61.120499"
219+ inkscape:export-ydpi="61.120499"><tspan
220+ 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;fill:#0000ff;"
221+ y="89.302101"
222+ x="47.360416"
223+ id="tspan2873"
224+ sodipodi:role="line">Lexer</tspan></text>
225+ <text
226+ xml:space="preserve"
227+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"
228+ x="100.27708"
229+ y="89.037521"
230+ id="text2879"
231+ inkscape:export-xdpi="61.120499"
232+ inkscape:export-ydpi="61.120499"><tspan
233+ sodipodi:role="line"
234+ id="tspan2877"
235+ x="100.27708"
236+ y="89.037521"
237+ 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:#0000ff;stroke-width:0.26458332">Parser</tspan></text>
238+ <path
239+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2891)"
240+ d="m 52.916666,71.575003 v 7.67291"
241+ id="path2887"
242+ inkscape:connector-curvature="0"
243+ sodipodi:nodetypes="cc"
244+ inkscape:export-xdpi="61.120499"
245+ inkscape:export-ydpi="61.120499" />
246+ <path
247+ sodipodi:nodetypes="cc"
248+ inkscape:connector-curvature="0"
249+ id="path3613"
250+ d="m 108.74375,71.575003 v 7.67291"
251+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker3617)"
252+ inkscape:export-xdpi="61.120499"
253+ inkscape:export-ydpi="61.120499" />
254+ <text
255+ id="text4173"
256+ y="69.987518"
257+ x="43.391666"
258+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
259+ xml:space="preserve"
260+ inkscape:export-xdpi="61.120499"
261+ inkscape:export-ydpi="61.120499"><tspan
262+ 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"
263+ y="69.987518"
264+ x="43.391666"
265+ id="tspan4171"
266+ sodipodi:role="line">Recogniser</tspan></text>
267+ <text
268+ xml:space="preserve"
269+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
270+ x="97.102081"
271+ y="69.722939"
272+ id="text4177"
273+ inkscape:export-xdpi="61.120499"
274+ inkscape:export-ydpi="61.120499"><tspan
275+ sodipodi:role="line"
276+ id="tspan4175"
277+ x="97.102081"
278+ y="69.722939"
279+ 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">Grammar</tspan></text>
280+ <text
281+ inkscape:export-ydpi="61.120499"
282+ inkscape:export-xdpi="61.120499"
283+ id="text854"
284+ y="93.800011"
285+ x="131.23334"
286+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
287+ xml:space="preserve"><tspan
288+ 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"
289+ y="103.5316"
290+ x="131.23334"
291+ id="tspan852"
292+ sodipodi:role="line" /></text>
293+ </g>
294+</svg>
docs/image/tokenise.pngnew file

Binary file not shown.

docs/image/tokenise.svgnew file+740
@@ -0,0 +1,740 @@
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="tokenise.svg">
19+ <defs
20+ id="defs2">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker7119"
25+ refX="0.0"
26+ refY="0.0"
27+ orient="auto"
28+ inkscape:stockid="Arrow1Mend">
29+ <path
30+ transform="scale(0.4) rotate(180) translate(10,0)"
31+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
33+ id="path7117" />
34+ </marker>
35+ <marker
36+ inkscape:stockid="Arrow1Mend"
37+ orient="auto"
38+ refY="0.0"
39+ refX="0.0"
40+ id="marker4031"
41+ style="overflow:visible;"
42+ inkscape:isstock="true"
43+ inkscape:collect="always">
44+ <path
45+ id="path4029"
46+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
47+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
48+ transform="scale(0.4) rotate(180) translate(10,0)" />
49+ </marker>
50+ <marker
51+ inkscape:isstock="true"
52+ style="overflow:visible;"
53+ id="marker1931"
54+ refX="0.0"
55+ refY="0.0"
56+ orient="auto"
57+ inkscape:stockid="Arrow1Mend"
58+ inkscape:collect="always">
59+ <path
60+ transform="scale(0.4) rotate(180) translate(10,0)"
61+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
62+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
63+ id="path1929" />
64+ </marker>
65+ <marker
66+ inkscape:stockid="Arrow1Mend"
67+ orient="auto"
68+ refY="0.0"
69+ refX="0.0"
70+ id="Arrow1Mend"
71+ style="overflow:visible;"
72+ inkscape:isstock="true"
73+ inkscape:collect="always">
74+ <path
75+ id="path1036"
76+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "
77+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
78+ transform="scale(0.4) rotate(180) translate(10,0)" />
79+ </marker>
80+ </defs>
81+ <sodipodi:namedview
82+ id="base"
83+ pagecolor="#ffffff"
84+ bordercolor="#666666"
85+ borderopacity="1.0"
86+ inkscape:pageopacity="0.0"
87+ inkscape:pageshadow="2"
88+ inkscape:zoom="1"
89+ inkscape:cx="497.48698"
90+ inkscape:cy="885.5"
91+ inkscape:document-units="mm"
92+ inkscape:current-layer="layer1"
93+ showgrid="false"
94+ inkscape:window-width="1920"
95+ inkscape:window-height="1015"
96+ inkscape:window-x="0"
97+ inkscape:window-y="0"
98+ inkscape:window-maximized="1" />
99+ <metadata
100+ id="metadata5">
101+ <rdf:RDF>
102+ <cc:Work
103+ rdf:about="">
104+ <dc:format>image/svg+xml</dc:format>
105+ <dc:type
106+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
107+ <dc:title></dc:title>
108+ </cc:Work>
109+ </rdf:RDF>
110+ </metadata>
111+ <g
112+ inkscape:label="Layer 1"
113+ inkscape:groupmode="layer"
114+ id="layer1">
115+ <rect
116+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
117+ id="rect815"
118+ width="4.3310161"
119+ height="4.3471913"
120+ x="61.383358"
121+ y="51.995804"
122+ inkscape:export-xdpi="61.120499"
123+ inkscape:export-ydpi="61.120499" />
124+ <text
125+ xml:space="preserve"
126+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
127+ x="62.917812"
128+ y="55.649193"
129+ id="text819"
130+ inkscape:export-xdpi="61.120499"
131+ inkscape:export-ydpi="61.120499"><tspan
132+ sodipodi:role="line"
133+ id="tspan817"
134+ x="62.917812"
135+ y="55.649193"
136+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">i</tspan></text>
137+ <rect
138+ y="51.995804"
139+ x="65.714371"
140+ height="4.3471913"
141+ width="4.3310161"
142+ id="rect823"
143+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
144+ inkscape:export-xdpi="61.120499"
145+ inkscape:export-ydpi="61.120499" />
146+ <text
147+ id="text827"
148+ y="55.307304"
149+ x="66.760414"
150+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
151+ xml:space="preserve"
152+ inkscape:export-xdpi="61.120499"
153+ inkscape:export-ydpi="61.120499"><tspan
154+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
155+ y="55.307304"
156+ x="66.760414"
157+ id="tspan825"
158+ sodipodi:role="line">n</tspan></text>
159+ <rect
160+ y="51.995804"
161+ x="70.045387"
162+ height="4.3471913"
163+ width="4.3310161"
164+ id="rect829"
165+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
166+ inkscape:export-xdpi="61.120499"
167+ inkscape:export-ydpi="61.120499" />
168+ <text
169+ id="text833"
170+ y="55.063095"
171+ x="71.237953"
172+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
173+ xml:space="preserve"
174+ inkscape:export-xdpi="61.120499"
175+ inkscape:export-ydpi="61.120499"><tspan
176+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
177+ y="55.063095"
178+ x="71.237953"
179+ id="tspan831"
180+ sodipodi:role="line">p</tspan></text>
181+ <rect
182+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
183+ id="rect835"
184+ width="4.3310161"
185+ height="4.3471913"
186+ x="74.376404"
187+ y="51.995804"
188+ inkscape:export-xdpi="61.120499"
189+ inkscape:export-ydpi="61.120499" />
190+ <text
191+ xml:space="preserve"
192+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
193+ x="75.422447"
194+ y="55.356148"
195+ id="text839"
196+ inkscape:export-xdpi="61.120499"
197+ inkscape:export-ydpi="61.120499"><tspan
198+ sodipodi:role="line"
199+ id="tspan837"
200+ x="75.422447"
201+ y="55.356148"
202+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">u</tspan></text>
203+ <rect
204+ y="51.995804"
205+ x="78.70742"
206+ height="4.3471913"
207+ width="4.3310161"
208+ id="rect841"
209+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
210+ inkscape:export-xdpi="61.120499"
211+ inkscape:export-ydpi="61.120499" />
212+ <text
213+ id="text845"
214+ y="55.649193"
215+ x="80.241875"
216+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
217+ xml:space="preserve"
218+ inkscape:export-xdpi="61.120499"
219+ inkscape:export-ydpi="61.120499"><tspan
220+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
221+ y="55.649193"
222+ x="80.241875"
223+ id="tspan843"
224+ sodipodi:role="line">t</tspan></text>
225+ <rect
226+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
227+ id="rect847"
228+ width="4.3310161"
229+ height="4.3471913"
230+ x="83.038437"
231+ y="51.995804"
232+ inkscape:export-xdpi="61.120499"
233+ inkscape:export-ydpi="61.120499" />
234+ <text
235+ xml:space="preserve"
236+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
237+ x="59.172871"
238+ y="88.457558"
239+ id="text851"><tspan
240+ sodipodi:role="line"
241+ id="tspan849"
242+ x="59.172871"
243+ y="92.350197"
244+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none" /></text>
245+ <rect
246+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
247+ id="rect853"
248+ width="4.3310161"
249+ height="4.3471913"
250+ x="87.369453"
251+ y="51.995804"
252+ inkscape:export-xdpi="61.120499"
253+ inkscape:export-ydpi="61.120499" />
254+ <text
255+ xml:space="preserve"
256+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
257+ x="88.46434"
258+ y="55.453827"
259+ id="text857"
260+ inkscape:export-xdpi="61.120499"
261+ inkscape:export-ydpi="61.120499"><tspan
262+ sodipodi:role="line"
263+ id="tspan855"
264+ x="88.46434"
265+ y="55.453827"
266+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">s</tspan></text>
267+ <rect
268+ y="51.995804"
269+ x="91.70047"
270+ height="4.3471913"
271+ width="4.3310161"
272+ id="rect859"
273+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
274+ inkscape:export-xdpi="61.120499"
275+ inkscape:export-ydpi="61.120499" />
276+ <text
277+ id="text863"
278+ y="55.649193"
279+ x="93.234924"
280+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
281+ xml:space="preserve"
282+ inkscape:export-xdpi="61.120499"
283+ inkscape:export-ydpi="61.120499"><tspan
284+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
285+ y="55.649193"
286+ x="93.234924"
287+ id="tspan861"
288+ sodipodi:role="line">t</tspan></text>
289+ <rect
290+ y="51.995804"
291+ x="96.031487"
292+ height="4.3471913"
293+ width="4.3310161"
294+ id="rect865"
295+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
296+ inkscape:export-xdpi="61.120499"
297+ inkscape:export-ydpi="61.120499" />
298+ <text
299+ id="text869"
300+ y="55.649193"
301+ x="97.565941"
302+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
303+ xml:space="preserve"
304+ inkscape:export-xdpi="61.120499"
305+ inkscape:export-ydpi="61.120499"><tspan
306+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
307+ y="55.649193"
308+ x="97.565941"
309+ id="tspan867"
310+ sodipodi:role="line">r</tspan></text>
311+ <rect
312+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
313+ id="rect871"
314+ width="4.3310161"
315+ height="4.3471913"
316+ x="100.3625"
317+ y="51.995804"
318+ inkscape:export-xdpi="61.120499"
319+ inkscape:export-ydpi="61.120499" />
320+ <text
321+ xml:space="preserve"
322+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
323+ x="101.89697"
324+ y="55.649193"
325+ id="text875"
326+ inkscape:export-xdpi="61.120499"
327+ inkscape:export-ydpi="61.120499"><tspan
328+ sodipodi:role="line"
329+ id="tspan873"
330+ x="101.89697"
331+ y="55.649193"
332+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">i</tspan></text>
333+ <rect
334+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
335+ id="rect877"
336+ width="4.3310161"
337+ height="4.3471913"
338+ x="104.69353"
339+ y="51.995804"
340+ inkscape:export-xdpi="61.120499"
341+ inkscape:export-ydpi="61.120499" />
342+ <text
343+ xml:space="preserve"
344+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
345+ x="105.73955"
346+ y="55.50267"
347+ id="text881"
348+ inkscape:export-xdpi="61.120499"
349+ inkscape:export-ydpi="61.120499"><tspan
350+ sodipodi:role="line"
351+ id="tspan879"
352+ x="105.73955"
353+ y="55.50267"
354+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">n</tspan></text>
355+ <rect
356+ y="51.995804"
357+ x="109.0245"
358+ height="4.3471913"
359+ width="4.3310161"
360+ id="rect883"
361+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
362+ inkscape:export-xdpi="61.120499"
363+ inkscape:export-ydpi="61.120499" />
364+ <text
365+ id="text887"
366+ y="54.965416"
367+ x="110.21709"
368+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
369+ xml:space="preserve"
370+ inkscape:export-xdpi="61.120499"
371+ inkscape:export-ydpi="61.120499"><tspan
372+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
373+ y="54.965416"
374+ x="110.21709"
375+ id="tspan885"
376+ sodipodi:role="line">g</tspan></text>
377+ <text
378+ xml:space="preserve"
379+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
380+ x="125.67681"
381+ y="55.359386"
382+ id="text893"
383+ inkscape:export-xdpi="61.120499"
384+ inkscape:export-ydpi="61.120499"><tspan
385+ sodipodi:role="line"
386+ id="tspan891"
387+ x="125.67681"
388+ y="55.359386"
389+ 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.70555556;stroke-miterlimit:4;stroke-dasharray:none">:String</tspan></text>
390+ <rect
391+ y="51.995804"
392+ x="113.35551"
393+ height="4.3471913"
394+ width="4.3310161"
395+ id="rect895"
396+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
397+ inkscape:export-xdpi="61.120499"
398+ inkscape:export-ydpi="61.120499" />
399+ <text
400+ id="text899"
401+ y="55.50267"
402+ x="114.40154"
403+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
404+ xml:space="preserve"><tspan
405+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
406+ y="59.395306"
407+ x="114.40154"
408+ id="tspan897"
409+ sodipodi:role="line" /></text>
410+ <rect
411+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
412+ id="rect901"
413+ width="4.3310161"
414+ height="4.3471913"
415+ x="117.68649"
416+ y="51.995804"
417+ inkscape:export-xdpi="61.120499"
418+ inkscape:export-ydpi="61.120499" />
419+ <text
420+ xml:space="preserve"
421+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
422+ x="118.87907"
423+ y="55.494583"
424+ id="text905"
425+ inkscape:export-xdpi="61.120499"
426+ inkscape:export-ydpi="61.120499"><tspan
427+ sodipodi:role="line"
428+ id="tspan903"
429+ x="118.87907"
430+ y="55.494583"
431+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">1</tspan></text>
432+ <g
433+ id="g950"
434+ transform="translate(-15.319488,0.319156)"
435+ inkscape:export-xdpi="61.120499"
436+ inkscape:export-ydpi="61.120499">
437+ <rect
438+ 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"
439+ id="rect907"
440+ width="11.990757"
441+ height="4.3471909"
442+ x="47.978806"
443+ y="69.310013" />
444+ <text
445+ xml:space="preserve"
446+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
447+ x="48.706326"
448+ y="72.963402"
449+ id="text911"><tspan
450+ sodipodi:role="line"
451+ id="tspan909"
452+ x="48.706326"
453+ y="72.963402"
454+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">token</tspan></text>
455+ <rect
456+ y="69.310013"
457+ x="59.969563"
458+ height="4.2674026"
459+ width="10.075821"
460+ id="rect913"
461+ 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" />
462+ <text
463+ id="text917"
464+ y="72.940666"
465+ x="61.015606"
466+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
467+ xml:space="preserve"><tspan
468+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
469+ y="72.940666"
470+ x="61.015606"
471+ id="tspan915"
472+ sodipodi:role="line">line</tspan></text>
473+ <rect
474+ y="69.389801"
475+ x="70.045387"
476+ height="4.1876144"
477+ width="7.5225825"
478+ id="rect919"
479+ 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" />
480+ <text
481+ id="text923"
482+ y="72.935829"
483+ x="70.998589"
484+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
485+ xml:space="preserve"><tspan
486+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
487+ y="72.935829"
488+ x="70.998589"
489+ id="tspan921"
490+ sodipodi:role="line">col</tspan></text>
491+ </g>
492+ <text
493+ id="text927"
494+ y="80.971657"
495+ x="40.541954"
496+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
497+ xml:space="preserve"
498+ inkscape:export-xdpi="61.120499"
499+ inkscape:export-ydpi="61.120499"><tspan
500+ 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.70555556;stroke-miterlimit:4;stroke-dasharray:none"
501+ y="80.971657"
502+ x="40.541954"
503+ sodipodi:role="line"
504+ id="tspan933">:(List (TokenData Token), Int, Int, String)</tspan></text>
505+ <g
506+ id="g970"
507+ transform="translate(16.596112,0.319156)"
508+ inkscape:export-xdpi="61.120499"
509+ inkscape:export-ydpi="61.120499">
510+ <rect
511+ y="69.310013"
512+ x="47.978806"
513+ height="4.3471909"
514+ width="11.990757"
515+ id="rect952"
516+ 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" />
517+ <text
518+ id="text956"
519+ y="72.963402"
520+ x="48.706326"
521+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
522+ xml:space="preserve"><tspan
523+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
524+ y="72.963402"
525+ x="48.706326"
526+ id="tspan954"
527+ sodipodi:role="line">token</tspan></text>
528+ <rect
529+ 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"
530+ id="rect958"
531+ width="10.075821"
532+ height="4.2674026"
533+ x="59.969563"
534+ y="69.310013" />
535+ <text
536+ xml:space="preserve"
537+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
538+ x="61.015606"
539+ y="72.940666"
540+ id="text962"><tspan
541+ sodipodi:role="line"
542+ id="tspan960"
543+ x="61.015606"
544+ y="72.940666"
545+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">line</tspan></text>
546+ <rect
547+ 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"
548+ id="rect964"
549+ width="7.5225825"
550+ height="4.1876144"
551+ x="70.045387"
552+ y="69.389801" />
553+ <text
554+ xml:space="preserve"
555+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
556+ x="70.998589"
557+ y="72.935829"
558+ id="text968"><tspan
559+ sodipodi:role="line"
560+ id="tspan966"
561+ x="70.998589"
562+ y="72.935829"
563+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">col</tspan></text>
564+ </g>
565+ <g
566+ transform="translate(48.591501,0.319156)"
567+ id="g990"
568+ inkscape:export-xdpi="61.120499"
569+ inkscape:export-ydpi="61.120499">
570+ <rect
571+ 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"
572+ id="rect972"
573+ width="11.990757"
574+ height="4.3471909"
575+ x="47.978806"
576+ y="69.310013" />
577+ <text
578+ xml:space="preserve"
579+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
580+ x="48.706326"
581+ y="72.963402"
582+ id="text976"><tspan
583+ sodipodi:role="line"
584+ id="tspan974"
585+ x="48.706326"
586+ y="72.963402"
587+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">token</tspan></text>
588+ <rect
589+ y="69.310013"
590+ x="59.969563"
591+ height="4.2674026"
592+ width="10.075821"
593+ id="rect978"
594+ 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" />
595+ <text
596+ id="text982"
597+ y="72.940666"
598+ x="61.015606"
599+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
600+ xml:space="preserve"><tspan
601+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
602+ y="72.940666"
603+ x="61.015606"
604+ id="tspan980"
605+ sodipodi:role="line">line</tspan></text>
606+ <rect
607+ y="69.389801"
608+ x="70.045387"
609+ height="4.1876144"
610+ width="7.5225825"
611+ id="rect984"
612+ 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" />
613+ <text
614+ id="text988"
615+ y="72.935829"
616+ x="70.998589"
617+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
618+ xml:space="preserve"><tspan
619+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
620+ y="72.935829"
621+ x="70.998589"
622+ id="tspan986"
623+ sodipodi:role="line">col</tspan></text>
624+ </g>
625+ <path
626+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"
627+ d="m 125.97308,68.549658 1.30238,0.0089 -0.0153,6.481345 h -1.30803"
628+ id="path992"
629+ inkscape:connector-curvature="0"
630+ sodipodi:nodetypes="cccc"
631+ inkscape:export-xdpi="61.120499"
632+ inkscape:export-ydpi="61.120499" />
633+ <path
634+ sodipodi:nodetypes="cccc"
635+ inkscape:connector-curvature="0"
636+ id="path994"
637+ d="m 32.561899,68.619523 -1.30238,0.0089 0.0153,6.481345 h 1.30803"
638+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
639+ inkscape:export-xdpi="61.120499"
640+ inkscape:export-ydpi="61.120499" />
641+ <rect
642+ 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"
643+ id="rect996"
644+ width="11.990757"
645+ height="4.3471909"
646+ x="155.60759"
647+ y="69.899559"
648+ inkscape:export-xdpi="61.120499"
649+ inkscape:export-ydpi="61.120499" />
650+ <text
651+ xml:space="preserve"
652+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
653+ x="156.33508"
654+ y="73.552948"
655+ id="text1000"
656+ inkscape:export-xdpi="61.120499"
657+ inkscape:export-ydpi="61.120499"><tspan
658+ sodipodi:role="line"
659+ id="tspan998"
660+ x="156.33508"
661+ y="73.552948"
662+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">string</tspan></text>
663+ <rect
664+ y="69.750786"
665+ x="130.3979"
666+ height="4.2674026"
667+ width="10.075821"
668+ id="rect1002"
669+ 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"
670+ inkscape:export-xdpi="61.120499"
671+ inkscape:export-ydpi="61.120499" />
672+ <text
673+ id="text1006"
674+ y="73.381439"
675+ x="131.44394"
676+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
677+ xml:space="preserve"
678+ inkscape:export-xdpi="61.120499"
679+ inkscape:export-ydpi="61.120499"><tspan
680+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
681+ y="73.381439"
682+ x="131.44394"
683+ id="tspan1004"
684+ sodipodi:role="line">line</tspan></text>
685+ <rect
686+ y="69.830574"
687+ x="143.64868"
688+ height="4.1876144"
689+ width="7.5225825"
690+ id="rect1008"
691+ 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"
692+ inkscape:export-xdpi="61.120499"
693+ inkscape:export-ydpi="61.120499" />
694+ <text
695+ id="text1012"
696+ y="73.376602"
697+ x="144.60188"
698+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
699+ xml:space="preserve"
700+ inkscape:export-xdpi="61.120499"
701+ inkscape:export-ydpi="61.120499"><tspan
702+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"
703+ y="73.376602"
704+ x="144.60188"
705+ id="tspan1010"
706+ sodipodi:role="line">col</tspan></text>
707+ <path
708+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"
709+ d="m 58.415342,69.700595 -0.143613,-5.887785 4.912582,-0.06048 0.03784,-6.371998"
710+ id="path1025"
711+ inkscape:connector-curvature="0"
712+ sodipodi:nodetypes="cccc"
713+ inkscape:export-xdpi="61.120499"
714+ inkscape:export-ydpi="61.120499" />
715+ <path
716+ inkscape:connector-curvature="0"
717+ id="path1927"
718+ d="m 89.918872,69.996556 -0.02264,-12.07186"
719+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1931)"
720+ sodipodi:nodetypes="cc"
721+ inkscape:export-xdpi="61.120499"
722+ inkscape:export-ydpi="61.120499" />
723+ <path
724+ sodipodi:nodetypes="cccc"
725+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4031)"
726+ d="m 122.08751,69.519138 -0.0832,-5.464386 -2.3456,-0.06048 -0.20406,-6.674425"
727+ id="path4027"
728+ inkscape:connector-curvature="0"
729+ inkscape:export-xdpi="61.120499"
730+ inkscape:export-ydpi="61.120499" />
731+ <path
732+ inkscape:connector-curvature="0"
733+ id="path7115"
734+ d="m 147.18896,69.882051 -0.0832,-5.827299 -22.72919,0 -0.446,-6.251027"
735+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker7119)"
736+ sodipodi:nodetypes="cccc"
737+ inkscape:export-xdpi="61.120499"
738+ inkscape:export-ydpi="61.120499" />
739+ </g>
740+</svg>
docs/index.rst+1
@@ -25,5 +25,6 @@ Documentation for the Idris Language
25 effects/index
25 effects/index
26 proofs/index
26 proofs/index
27 elaboratorReflection/index
27 elaboratorReflection/index
28+ parserLibrary/index
28 reference/index
29 reference/index
29 guides/index
30 guides/index
docs/parserLibrary/index.rstnew file+23
@@ -0,0 +1,23 @@
1+.. _parserLibrary:
2+
3+########################
4+Lexer and Parser Library
5+########################
6+
7+A tutorial on the lexer and parser library in Idris.
8+
9+.. note::
10+
11+ The documentation for Idris has been published under the Creative
12+ Commons CC0 License. As such to the extent possible under law, *The
13+ Idris Community* has waived all copyright and related or neighboring
14+ rights to Documentation for Idris.
15+
16+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
17+
18+.. toctree::
19+ :maxdepth: 1
20+
21+ introduction
22+ lexer
23+ parser
docs/parserLibrary/introduction.rstnew file+209
@@ -0,0 +1,209 @@
1+.. _parserLibrary:
2+
3+***************************
4+Parser Library Introduction
5+***************************
6+
7+The Idris elaborator is responsible for converting high-level Idris code into the core language.
8+It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.
9+For details, see `Edwin Brady's 2013 paper in the Journal of Functional
10+Programming <https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf>`_.
11+
12+Elaborator reflection makes the elaboration type as well as a selection of its tactics available to Idris code.
13+This means that metaprograms written in Idris can have complete control over the elaboration process, generating arbitrary code, and they have access to all of the facilities available in the elaborator, such as higher-order unification, type checking, and emitting auxiliary definitions.
14+
15+The Elaborator State
16+====================
17+
18+The elaborator state contains information about the ongoing elaboration process.
19+In particular, it contains a *goal type*, which is to be filled by an under-construction *proof term*.
20+The proof term can contain *holes*, each of which has a scope in which it is valid and a type.
21+Some holes may additionally contain *guesses*, which can be substituted in the scope of the hole.
22+The holes are tracked in a *hole queue*, and one of them is *focused*.
23+In addition to the goal type, proof term, and holes, the elaborator state contains a collection of unsolved unification problems that can affect elaboration.
24+
25+The elaborator state is not directly available to Idris programs.
26+Instead, it is modified through the use of *tactics*, which are operations that affect the elaborator state.
27+A tactic that returns a value of type ``a``, potentially modifying the elaborator state, has type ``Elab a``.
28+The default tactics are all in the namespace ``Language.Reflection.Elab.Tactics``.
29+
30+
31+Running Elaborator Scripts
32+==========================
33+
34+On their own, tactics have no effect.
35+The meta-operation ``%runElab script`` runs ``script`` in the current elaboration context.
36+Before you can use ``%runElab``, you will have to enable the language extension by adding
37+``%language ElabReflection`` in your file (or by passing ``-X ElabReflection`` to the
38+``idris`` executable from your command line).
39+For example, the following script constructs the identity function at type ``Nat``:
40+
41+.. code-block:: idris
42+
43+ idNat : Nat -> Nat
44+ idNat = %runElab (do intro `{{x}}
45+ fill (Var `{{x}})
46+ solve)
47+
48+
49+On the right-hand side, the Idris elaborator has the goal ``Nat -> Nat``.
50+When it encounters the ``%runElab`` directive, it fulfills this goal by running the provided script.
51+The first tactic, ``intro``, constructs a lambda that binds the name ``x``.
52+The name argument is optional because a default name can be taken from the function type.
53+Now, the proof term is of the form ``\x : Nat => {hole}``.
54+The second tactic, ``fill``, fills this hole with a guess, giving the term ``\x : Nat => {hole≈x}``.
55+Finally, the ``solve`` tactic instantiates the guess, giving the result ``\x : Nat => x``.
56+
57+Because elaborator scripts are ordinary Idris expressions, it is also possible to use them in multiple contexts.
58+Note that there is nothing ``Nat``-specific about the above script.
59+We can generate identity functions at any concrete type using the same script:
60+
61+.. code-block:: idris
62+
63+ mkId : Elab ()
64+ mkId = do intro `{{x}}
65+ fill (Var `{{x}})
66+ solve
67+
68+ idNat : Nat -> Nat
69+ idNat = %runElab mkId
70+
71+ idUnit : () -> ()
72+ idUnit = %runElab mkId
73+
74+ idString : String -> String
75+ idString = %runElab mkId
76+
77+
78+Interactively Building Elab Scripts
79+===================================
80+
81+You can build an ``Elab`` script interactively at the REPL.
82+Use the command ``:metavars``, or ``:m`` for short, to list the available holes.
83+Then, issue the ``:elab <hole>`` command at the REPL
84+to enter the elaboration shell.
85+
86+At the shell, you can enter proof tactics to alter the proof state.
87+You can view the system-provided tactics prior to entering the shell
88+by issuing the REPL command ``:browse Language.Reflection.Elab.Tactics``.
89+When you have discharged all goals, you can complete the proof
90+using the ``:qed`` command and receive in return an elaboration script
91+that fills the hole.
92+
93+The interactive elaboration shell accepts a limited number of commands,
94+including a subset of the commands understood by the normal Idris REPL
95+as well as some elaboration-specific commands. It also supports the
96+``do``-syntax, meaning you can write ``res <- command`` to bind the result of
97+``command`` to variable ``res``.
98+
99+General-purpose commands:
100+
101+- ``:eval <EXPR>``, or ``:e <EXPR>`` for short, evaluates the provided expression
102+ and prints the result.
103+
104+- ``:type <EXPR>``, or ``:t <EXPR>`` for short, prints the provided expression
105+ together with its type.
106+
107+- ``:search <TYPE>`` searches for definitions having the provided type.
108+
109+- ``:doc <NAME>`` searches for definitions with the provided name and prints their
110+ documentation.
111+
112+
113+Commands for viewing the proof state:
114+
115+- ``:state`` displays the current state of the term being constructed. It lists both
116+ other goals and the current goal.
117+
118+- ``:term`` displays the current proof term as well as its yet-to-be-filled holes.
119+
120+
121+Commands for manipulating the proof state:
122+
123+- ``:undo`` undoes the effects of the last tactic.
124+
125+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
126+
127+- ``:qed`` finishes the script and exits the elaboration shell. The shell will only accept
128+ this command once it reports, "No more goals." On exit, it will print out the finished
129+ elaboration script for you to copy into your program.
130+
131+
132+Failure
133+=======
134+
135+Some tactics may *fail*.
136+For example, ``intro`` will fail if the focused hole does not have a function type, ``solve`` will fail if the current hole does not contain a guess, and ``fill`` will fail if the term to be filled in has the wrong type.
137+Scripts can also fail explicitly using the ``fail`` tactic.
138+
139+To account for failure, there is an ``Alternative`` implementation for ``Elab``.
140+The ``<|>`` operator first tries the script to its left.
141+If that script fails, any changes that it made to the state are undone and the right argument is executed.
142+If the first argument succeeds, then the second argument is not executed.
143+
144+Querying the Elaboration State
145+==============================
146+
147+``Elab`` includes operations to query the elaboration state, allowing scripts to use information about their environment to steer the elaboration process.
148+The ordinary Idris bind syntax can be used to propagate this information.
149+For example, a tactic that solves the current goal when it is the unit type might look like this:
150+
151+.. code-block:: idris
152+
153+ triv : Elab ()
154+ triv = do compute
155+ g <- getGoal
156+ case (snd g) of
157+ `(() : Type) => do fill `(() : ())
158+ solve
159+ otherGoal => fail [ TermPart otherGoal
160+ , TextPart "is not trivial"
161+ ]
162+
163+
164+The tactic ``compute`` normalises the type of its goal with respect to the current context.
165+While not strictly necessary, this allows ``triv`` to be used in contexts where the triviality of the goal is not immediately apparent.
166+Then, ``getGoal`` is used, and its result is bound to ``g``.
167+Because it returns a pair consisting of the current goal's name and type, we case-split on its second projection.
168+If the goal type turns out to have been the unit type, we fill using the unit constructor and solve the goal.
169+Otherwise, we fail with an error message informing the user that the current goal is not trivial.
170+
171+Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
172+A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debugging" of elaboration scripts.
173+The message format used by ``debugMessage`` is the same for errors produced by the error reflection mechanism, allowing the re-use of the Idris pretty-printer when rendering messages.
174+
175+Changing the Global Context
176+===========================
177+
178+``Elab`` scripts can modify the global context during execution.
179+Just as the Idris elaborator produces auxiliary definitions to implement features such as ``where``-blocks and ``case`` expressions, user elaboration scripts may need to define functions.
180+Furthermore, this allows ``Elab`` reflection to be used to implement features such as interface deriving.
181+The operations ``declareType``, ``defineFunction``, and ``addImplementation`` allow ``Elab`` scripts to modify the global context.
182+
183+Using Idris's Features
184+======================
185+
186+The Idris compiler has a number of ways to automate the construction of terms.
187+On its own, the ``Elab`` state and its interactions with the unifier allow implicits to be solved using unification.
188+Additional operations use further features of Idris.
189+In particular, ``resolveTC`` solves the current goal using interface resolution, ``search`` invokes the proof search mechanism, and ``sourceLocation`` finds the context in the original file at which the elaboration script is invoked.
190+
191+
192+Recursive Elaboration
193+=====================
194+
195+The elaboration mechanism can be invoked recursively using the ``runElab`` tactic.
196+This tactic takes a goal type and an elaboration script as arguments and runs the script in a fresh lexical environment to create an inhabitant of the provided goal type.
197+This is primarily useful for code generation, particularly for generating pattern-matching clauses, where variable scope needs to be one that isn't the present local context.
198+
199+Learn More
200+==========
201+
202+Some tactics are introduced in the :ref:`proofs-index` section with further details, of those most relevant to elaborator reflection, on the following pages.
203+
204+The list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.
205+All of the built-in tactics contain documentation strings.
206+
207+For alternative ways to extend the Idris language see the :ref:`reference-index` section.
208+
209+The following pages explain more about the theory and practice of elaborator reflection.
docs/parserLibrary/lexer.rstnew file+60
@@ -0,0 +1,60 @@
1+Lexer
2+=====
3+
4+Idris provides a mechanism to modify the language without having to recompile Idris itself. We can think of this in terms of metaprogramming or domain specific languages or just building in new capabilities.
5+
6+In order to extend the language we need to know something about how Idris is compiled. This page explains only what is needed to customise the elaboration. For more information about the compiler's implementation see `Edwin Brady's 2013 paper`_ and for customising the elaboration process see `Elaborator reflection: extending Idris in Idris`_ and `David Christiansen's PhD thesis`_.
7+
8+Compilation of Idris proceeds through a number of stages.
9+
10+- First, Idris is desugared by inserting placeholders for terms to be guessed by the compiler and replacing certain syntactic forms, such as do-notation, with the functions that implement them.
11+- Then, this desugared Idris is translated into a much simpler core language, called TT. This translation process is called elaboration.
12+- Finally, TT is type checked a second time to rule out errors, and then compiled into the target language.
13+
14+.. image:: ../image/idrisTopLevel.png
15+ :width: 484px
16+ :height: 147px
17+ :alt: diagram illustrating these stages of Idris compilation
18+
19+TT is a core language which is syntactically very simple. This makes it easy for computers to process but very verbose and hard for humans to read. The Idris elaborator is written in Haskell using an elaboration library that was inspired by the tactics in interactive proof assistants such as Coq.
20+
21+.. list-table::
22+
23+ * - There are some similarities with a proof assistant but in Idris the elaborator is an interpreter of Idris source in the elaboration monad, where each syntactic construct of Idris is interpreted as a sequence of tactics.
24+ - .. image:: ../image/compareToProofAssist.png
25+ :width: 206px
26+ :height: 112px
27+ :alt: diagram comparing elaboration with proof assistant
28+
29+The primitives in the elaboration library are not just useful for the implementors of Idris itself. They can also be used by authors of extensions to the compiler, using a mechanism known as elaborator reflection.
30+During elaboration TT (Raw) structure contains:
31+
32+- holes - placeholders for terms that have not yet been filled in.
33+- guesses - similar to let bindings, except with no reduction rule, so that elaboration programs can control the precise shape of terms that are under construction.
34+
35+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
36+
37+The following diagram is intended to illustrate a high level view of the tactics and how this eventually results in the TT language being generated. It is not necessary to understand the details at this stage. The intention is to help build up some intuition so that, when we get into the details, we can recognise how this fits into the big picture.
38+
39+.. image:: ../image/elabOverview.png
40+ :width: 410px
41+ :height: 282px
42+ :alt: diagram illustrating overview of TT language being generated from tactics.
43+
44+As already mentioned the TT core language is kept syntactically very simple, for instance, here are the binders in TT with corresponding code and logic type validity rules:
45+
46+.. list-table::
47+
48+ * - This diagram illustrates the basis of the compilation process in logic (in this case for binders). It is not necessary to be an expert logician to understand elaborator reflection. However, when learning about tactics, they may appear arbitrary without knowing some theory. For more information about this see `Edwin Brady's 2013 paper`_.
49+ - .. image:: ../image/binders.png
50+ :width: 310px
51+ :height: 203px
52+ :alt: diagram illustrating basis of code in logic
53+
54+.. target-notes::
55+.. _`Edwin Brady's 2013 paper`: https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf
56+.. _`Elaborator reflection: extending Idris in Idris`: https://dl.acm.org/citation.cfm?doid=2951913.2951932
57+.. _`David Christiansen's PhD thesis`: https://davidchristiansen.dk/david-christiansen-phd.pdf
58+.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374
59+
60+
docs/parserLibrary/parser.rstnew file+192
@@ -0,0 +1,192 @@
1+Elaborator Reflection - Identity Example
2+========================================
3+
4+.. list-table::
5+
6+ * - This example of elaborator reflection steps through this metaprogram that generates the identity function:
7+ - .. code-block:: idris
8+
9+ %language ElabReflection
10+
11+ idNat : Nat -> Nat
12+ idNat = %runElab (do intro `{{x}}
13+ fill (Var `{{x}})
14+ solve)
15+
16+.. list-table::
17+ :widths: 200 100
18+
19+ * - At the beginning of executing the elaboration script, the initial state consists of a single hole of type Nat -> Nat.
20+
21+ As a first approximation, the state consists of a term with holes in it, an indicator of which hole is focused, a queue of the next holes to focus on, and miscellaneous information like a source of fresh names. The intro tactic modifies this state, replacing the focused hole with a lambda and focusing on the lambda's body.
22+ - .. image:: ../image/tree.png
23+ :width: 119px
24+ :height: 109px
25+
26+The following is a walkthough looking at the state after each tactic:
27+
28+.. list-table::
29+
30+ * - Start with the type signature like this:
31+ - .. code-block:: idris
32+
33+ %language ElabReflection
34+
35+ idNat : Nat -> Nat
36+ idNat = %runElab (do
37+
38+ * - In order to investigate how the program works this table shows the proof state at each stage as the tactics are applied. So here is the proof state at the start:
39+ - .. image:: ../image/elabProofStateEx1_1.png
40+ :width: 310px
41+ :height: 115px
42+
43+ * - This table shows the hole types and what they depend on. The aim is to illustrate the types by analogy with proofs, as a line with the premises above it and the conclusion below it.
44+ - .. image:: ../image/elabLogicEx1_1.png
45+ :width: 277px
46+ :height: 15px
47+
48+ * - The term is:
49+ - ?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}
50+
51+ * - It is possible to read the state from the script by calling getEnv, getGoal and getHoles.
52+
53+ - The output of these calls contain structures with TT code. To show the results I hacked this: `my code`_. TT code is not really designed to be readable by humans, all the names are fully expanded, everything has a type down to universes (type of types). This is shown here to illustrate the information available.
54+
55+ .. code-block:: idris
56+
57+ getEnv=[]
58+
59+ getGoal=(hole_2, __pi_arg:(Nat.["Nat", "Prelude"]:{
60+ type constructor tag=8 number=0}.Type:U=(20:./Prelude/Nat.idr)->.
61+ {name ref{type constructor tag=8 number=0}Nat.["Nat","Prelude"]:
62+ Type:U=(20:./Prelude/Nat.idr)
63+ })
64+ })
65+
66+ getHoles=[{hole_2},{hole_0}]
67+
68+ * - getGuess
69+ - error no guess
70+
71+ * - Introduce a lambda binding around the current hole and focus on the body.
72+ - intro \`{{x}}
73+
74+ * - The state now looks like this:
75+ - .. image:: ../image/elabProofStateEx1_2.png
76+ :width: 312px
77+ :height: 84px
78+
79+ * - The hole types now looks like this:
80+ - .. image:: ../image/elabLogicEx1_2.png
81+ :width: 279px
82+ :height: 26px
83+
84+ * - The term now looks like this:
85+ - ?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}
86+
87+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
88+
89+ - .. code-block:: idris
90+
91+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:{
92+ type constructor tag=8 number=0}).
93+ Type:U=(20:./Prelude/Nat.idr)
94+ })]
95+
96+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
97+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
98+ })
99+
100+ getHoles=[{hole_2},{hole_0}]
101+
102+ * - getGuess
103+ - error no guess
104+
105+ * - Place a term into a hole, unifying its type
106+ - fill (Var \`{{x}})
107+
108+ * - The state still looks like this:
109+ - .. image:: ../image/elabProofStateEx1_3.png
110+ :width: 312px
111+ :height: 57px
112+
113+ * - The hole types now looks like this:
114+ - .. image:: ../image/elabLogicEx1_3.png
115+ :width: 290px
116+ :height: 26px
117+
118+ * - The term now looks like this:
119+ - ?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}
120+
121+ * - Again we can check the state by calling getEnv, getGoal and getHoles: see `my code`_
122+
123+ - .. code-block:: idris
124+
125+ getEnv=[(x, {λ (Nat.["Nat", "Prelude"]:
126+ {type constructor tag=8 number=0}).
127+ Type:U=(20:./Prelude/Nat.idr)
128+ })]
129+
130+ getGoal=(hole_2, {name ref{type constructor tag=8 number=0}
131+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
132+ })
133+
134+ getHoles=[{hole_2}, {hole_0}]
135+
136+ * - getGuess
137+ - .. code-block:: idris
138+
139+ {name ref bound x:
140+ {name ref{type constructor tag=8 number=0}
141+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
142+ }
143+ }
144+
145+ * - Substitute a guess into a hole.
146+ - solve
147+
148+ * - The hole types now looks like this:
149+ - .. image:: ../image/elabLogicEx1_4.png
150+ :width: 131px
151+ :height: 14px
152+
153+ * - The term now looks like this:
154+ - ?{hole_0} ≈ λ x . x . {hole_0}
155+
156+ * - getEnv
157+
158+ getGoal
159+
160+ getHoles
161+
162+ - .. code-block:: idris
163+
164+ getEnv=[]
165+
166+ getGoal=(hole_0, __pi_arg:(Nat.["Nat", "Prelude"]:{
167+ type constructor tag=8 number=0}.
168+ Type:U=(20:./Prelude/Nat.idr)
169+ ->.{name ref
170+ {type constructor tag=8 number=0}
171+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
172+ })
173+ })
174+
175+ getHoles=[{hole_0}]
176+
177+ * - getGuess
178+ - .. code-block:: idris
179+
180+ x:({λ (Nat.["Nat", "Prelude"]:{
181+ type constructor tag=8 number=0}).
182+ Type:U=(20:./Prelude/Nat.idr)
183+ }.{
184+ name ref bound
185+ x:{name ref {type constructor tag=8 number=0}
186+ Nat.["Nat","Prelude"]:Type:U=(20:./Prelude/Nat.idr)
187+ }
188+ })
189+ }
190+
191+.. target-notes::
192+.. _`my code`: https://github.com/martinbaker/Idris-dev/blob/uglyTTPrinter/libs/prelude/Language/Reflection/TTPrinter.idr