git.iko.soy/Idris-dev
on master help sign in
work on parser page
af2766cmartinbaker
docs/conf.py+1−1
compare with master
unifiedsplit
@@ -51,7 +51,7 @@ master_doc = 'index'
51
51
52# General information about the project.
52# General information about the project.
53project = u'Idris'
53project = u'Idris'
54−copyright = u'2017-2019, The Idris Community'
54+copyright = u'2017-2020, The Idris Community'
55author = u'The Idris Community'
55author = u'The Idris Community'
56
56
57# The version info for the project you're documenting, acts as replacement for
57# The version info for the project you're documenting, acts as replacement for
docs/image/parserModules.png

Binary file not shown.

docs/image/parserModules.svg+382−285
@@ -15,9 +15,127 @@
15 version="1.1"
15 version="1.1"
16 id="svg8"
16 id="svg8"
17 inkscape:version="0.92.2 5c3e80d, 2017-08-06"
17 inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18− sodipodi:docname="modules.svg">
18+ sodipodi:docname="parserModules.svg">
19 <defs
19 <defs
20 id="defs2">
20 id="defs2">
21+ <marker
22+ inkscape:isstock="true"
23+ style="overflow:visible;"
24+ id="marker1078"
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="path1076" />
34+ </marker>
35+ <marker
36+ inkscape:isstock="true"
37+ style="overflow:visible"
38+ id="marker1074"
39+ refX="0.0"
40+ refY="0.0"
41+ orient="auto"
42+ inkscape:stockid="Arrow1Mstart">
43+ <path
44+ transform="scale(0.4) translate(10,0)"
45+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;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="path1072" />
48+ </marker>
49+ <marker
50+ inkscape:stockid="Arrow1Mend"
51+ orient="auto"
52+ refY="0.0"
53+ refX="0.0"
54+ id="marker1021"
55+ style="overflow:visible;"
56+ inkscape:isstock="true"
57+ inkscape:collect="always">
58+ <path
59+ id="path1019"
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:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
62+ transform="scale(0.4) rotate(180) translate(10,0)" />
63+ </marker>
64+ <marker
65+ inkscape:stockid="Arrow1Mstart"
66+ orient="auto"
67+ refY="0.0"
68+ refX="0.0"
69+ id="marker1017"
70+ style="overflow:visible"
71+ inkscape:isstock="true"
72+ inkscape:collect="always">
73+ <path
74+ id="path1015"
75+ 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 "
76+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
77+ transform="scale(0.4) translate(10,0)" />
78+ </marker>
79+ <marker
80+ inkscape:isstock="true"
81+ style="overflow:visible;"
82+ id="marker973"
83+ refX="0.0"
84+ refY="0.0"
85+ orient="auto"
86+ inkscape:stockid="Arrow1Mend"
87+ inkscape:collect="always">
88+ <path
89+ transform="scale(0.4) rotate(180) translate(10,0)"
90+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
91+ 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 "
92+ id="path971" />
93+ </marker>
94+ <marker
95+ inkscape:isstock="true"
96+ style="overflow:visible"
97+ id="marker969"
98+ refX="0.0"
99+ refY="0.0"
100+ orient="auto"
101+ inkscape:stockid="Arrow1Mstart"
102+ inkscape:collect="always">
103+ <path
104+ transform="scale(0.4) translate(10,0)"
105+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
106+ 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 "
107+ id="path967" />
108+ </marker>
109+ <marker
110+ inkscape:stockid="Arrow1Mend"
111+ orient="auto"
112+ refY="0.0"
113+ refX="0.0"
114+ id="Arrow1Mend"
115+ style="overflow:visible;"
116+ inkscape:isstock="true"
117+ inkscape:collect="always">
118+ <path
119+ id="path1214"
120+ 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 "
121+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
122+ transform="scale(0.4) rotate(180) translate(10,0)" />
123+ </marker>
124+ <marker
125+ inkscape:stockid="Arrow1Mstart"
126+ orient="auto"
127+ refY="0.0"
128+ refX="0.0"
129+ id="Arrow1Mstart"
130+ style="overflow:visible"
131+ inkscape:isstock="true"
132+ inkscape:collect="always">
133+ <path
134+ id="path1211"
135+ 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 "
136+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"
137+ transform="scale(0.4) translate(10,0)" />
138+ </marker>
21 <marker
139 <marker
22 inkscape:isstock="true"
140 inkscape:isstock="true"
23 style="overflow:visible;"
141 style="overflow:visible;"
@@ -278,21 +396,6 @@
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 "
396 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" />
397 id="path3615" />
280 </marker>
398 </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
399 <marker
297 inkscape:stockid="Arrow1Mend"
400 inkscape:stockid="Arrow1Mend"
298 orient="auto"
401 orient="auto"
@@ -323,21 +426,6 @@
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 "
426 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" />
427 id="path1537" />
325 </marker>
428 </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>
429 </defs>
342 <sodipodi:namedview
430 <sodipodi:namedview
343 id="base"
431 id="base"
@@ -348,15 +436,16 @@
348 inkscape:pageshadow="2"
436 inkscape:pageshadow="2"
349 inkscape:zoom="1"
437 inkscape:zoom="1"
350 inkscape:cx="368.33949"
438 inkscape:cx="368.33949"
351− inkscape:cy="554.8721"
439+ inkscape:cy="617.07597"
352 inkscape:document-units="mm"
440 inkscape:document-units="mm"
353 inkscape:current-layer="layer1"
441 inkscape:current-layer="layer1"
354 showgrid="false"
442 showgrid="false"
355− inkscape:window-width="1359"
443+ inkscape:window-width="1800"
356 inkscape:window-height="1011"
444 inkscape:window-height="1011"
357− inkscape:window-x="-4"
445+ inkscape:window-x="0"
358 inkscape:window-y="0"
446 inkscape:window-y="0"
359− inkscape:window-maximized="0" />
447+ inkscape:window-maximized="0"
448+ inkscape:snap-nodes="false" />
360 <metadata
449 <metadata
361 id="metadata5">
450 id="metadata5">
362 <rdf:RDF>
451 <rdf:RDF>
@@ -373,157 +462,6 @@
373 inkscape:label="Layer 1"
462 inkscape:label="Layer 1"
374 inkscape:groupmode="layer"
463 inkscape:groupmode="layer"
375 id="layer1">
464 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
465 <text
528 inkscape:export-ydpi="61.120499"
466 inkscape:export-ydpi="61.120499"
529 inkscape:export-xdpi="61.120499"
467 inkscape:export-xdpi="61.120499"
@@ -645,15 +583,15 @@
645 id="tspan921">List (TokenData Token)</tspan></text>
583 id="tspan921">List (TokenData Token)</tspan></text>
646 <text
584 <text
647 id="text931"
585 id="text931"
648− y="184.2872"
586+ y="218.41846"
649− x="37.041664"
587+ x="36.512497"
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"
588 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"
589 xml:space="preserve"
652 inkscape:export-xdpi="61.120499"
590 inkscape:export-xdpi="61.120499"
653 inkscape:export-ydpi="61.120499"><tspan
591 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"
592 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"
593+ y="218.41846"
656− x="37.041664"
594+ x="36.512497"
657 id="tspan929"
595 id="tspan929"
658 sodipodi:role="line">module Text.Lexer</tspan></text>
596 sodipodi:role="line">module Text.Lexer</tspan></text>
659 <text
597 <text
@@ -672,8 +610,8 @@
672 <rect
610 <rect
673 inkscape:export-ydpi="61.120499"
611 inkscape:export-ydpi="61.120499"
674 inkscape:export-xdpi="61.120499"
612 inkscape:export-xdpi="61.120499"
675− y="180.05362"
613+ y="214.18488"
676− x="32.543747"
614+ x="32.01458"
677 height="6.3500061"
615 height="6.3500061"
678 width="43.656254"
616 width="43.656254"
679 id="rect937"
617 id="rect937"
@@ -685,8 +623,8 @@
685 id="rect939"
623 id="rect939"
686 width="42.862495"
624 width="42.862495"
687 height="6.8791728"
625 height="6.8791728"
688− x="95.51458"
626+ x="94.985413"
689− y="180.05362" />
627+ y="214.18488" />
690 <text
628 <text
691 inkscape:export-ydpi="61.120499"
629 inkscape:export-ydpi="61.120499"
692 inkscape:export-xdpi="61.120499"
630 inkscape:export-xdpi="61.120499"
@@ -706,33 +644,33 @@
706 inkscape:export-xdpi="61.120499"
644 inkscape:export-xdpi="61.120499"
707 inkscape:connector-curvature="0"
645 inkscape:connector-curvature="0"
708 id="path963"
646 id="path963"
709− d="m 53.828728,179.89081 1.006873,-18.52084"
647+ d="m 53.299561,213.22831 1.53604,-51.85834"
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)" />
648 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
649 <text
712 inkscape:export-ydpi="61.120499"
650 inkscape:export-ydpi="61.120499"
713 inkscape:export-xdpi="61.120499"
651 inkscape:export-xdpi="61.120499"
714 xml:space="preserve"
652 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"
653 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"
654+ x="23.220526"
717− y="216.88524"
655+ y="251.01649"
718 id="text971"><tspan
656 id="text971"><tspan
719 sodipodi:role="line"
657 sodipodi:role="line"
720 id="tspan969"
658 id="tspan969"
721− x="23.749693"
659+ x="23.220526"
722− y="216.88524"
660+ y="251.01649"
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>
661 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
662 <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"
663 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"
664 id="rect973"
727 width="47.889587"
665 width="47.889587"
728 height="6.3500061"
666 height="6.3500061"
729− x="22.162193"
667+ x="21.633026"
730− y="212.38707"
668+ y="246.51833"
731 inkscape:export-xdpi="61.120499"
669 inkscape:export-xdpi="61.120499"
732 inkscape:export-ydpi="61.120499" />
670 inkscape:export-ydpi="61.120499" />
733 <path
671 <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)"
672 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"
673+ d="m 48.369316,228.83873 0.04943,-6.71548"
736 id="path975"
674 id="path975"
737 inkscape:connector-curvature="0"
675 inkscape:connector-curvature="0"
738 inkscape:export-xdpi="61.120499"
676 inkscape:export-xdpi="61.120499"
@@ -740,22 +678,22 @@
740 sodipodi:nodetypes="cc" />
678 sodipodi:nodetypes="cc" />
741 <text
679 <text
742 id="text979"
680 id="text979"
743− y="207.83517"
681+ y="241.96643"
744− x="23.812496"
682+ x="23.283329"
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"
683 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"
684 xml:space="preserve"
747 inkscape:export-xdpi="61.120499"
685 inkscape:export-xdpi="61.120499"
748 inkscape:export-ydpi="61.120499"><tspan
686 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"
687 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"
688+ y="241.96643"
751− x="23.812496"
689+ x="23.283329"
752 id="tspan977"
690 id="tspan977"
753 sodipodi:role="line">module Text.Quantity</tspan></text>
691 sodipodi:role="line">module Text.Quantity</tspan></text>
754 <rect
692 <rect
755 inkscape:export-ydpi="61.120499"
693 inkscape:export-ydpi="61.120499"
756 inkscape:export-xdpi="61.120499"
694 inkscape:export-xdpi="61.120499"
757− y="203.33701"
695+ y="237.46826"
758− x="22.224997"
696+ x="21.695829"
759 height="6.2469702"
697 height="6.2469702"
760 width="43.853985"
698 width="43.853985"
761 id="rect981"
699 id="rect981"
@@ -765,21 +703,21 @@
765 inkscape:export-xdpi="61.120499"
703 inkscape:export-xdpi="61.120499"
766 xml:space="preserve"
704 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"
705 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"
706+ x="23.18244"
769− y="199.55397"
707+ y="233.68523"
770 id="text985"><tspan
708 id="text985"><tspan
771 sodipodi:role="line"
709 sodipodi:role="line"
772 id="tspan983"
710 id="tspan983"
773− x="23.711607"
711+ x="23.18244"
774− y="199.55397"
712+ y="233.68523"
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>
713 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
714 <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"
715 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"
716 id="rect987"
779 width="39.011257"
717 width="39.011257"
780 height="5.9464455"
718 height="5.9464455"
781− x="22.124107"
719+ x="21.59494"
782− y="195.0558"
720+ y="229.18706"
783 inkscape:export-xdpi="61.120499"
721 inkscape:export-xdpi="61.120499"
784 inkscape:export-ydpi="61.120499" />
722 inkscape:export-ydpi="61.120499" />
785 <path
723 <path
@@ -788,11 +726,11 @@
788 inkscape:export-xdpi="61.120499"
726 inkscape:export-xdpi="61.120499"
789 inkscape:connector-curvature="0"
727 inkscape:connector-curvature="0"
790 id="path993"
728 id="path993"
791− d="M 63.527551,202.87958 63.375204,187.79022"
729+ d="M 62.998384,237.01083 62.846037,221.92147"
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)" />
730 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
731 <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)"
732 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"
733+ d="M 67.336659,246.29272 67.083422,221.71969"
796 id="path999"
734 id="path999"
797 inkscape:connector-curvature="0"
735 inkscape:connector-curvature="0"
798 inkscape:export-xdpi="61.120499"
736 inkscape:export-xdpi="61.120499"
@@ -800,7 +738,7 @@
800 sodipodi:nodetypes="cc" />
738 sodipodi:nodetypes="cc" />
801 <path
739 <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)"
740 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"
741+ d="M 73.937074,214.02206 94.72083,169.47102"
804 id="path1005"
742 id="path1005"
805 inkscape:connector-curvature="0"
743 inkscape:connector-curvature="0"
806 inkscape:export-xdpi="61.120499"
744 inkscape:export-xdpi="61.120499"
@@ -808,7 +746,7 @@
808 sodipodi:nodetypes="cc" />
746 sodipodi:nodetypes="cc" />
809 <path
747 <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)"
748 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"
749+ d="M 108.0684,213.75748 108.0169,173.5408"
812 id="path1011"
750 id="path1011"
813 inkscape:connector-curvature="0"
751 inkscape:connector-curvature="0"
814 inkscape:export-xdpi="61.120499"
752 inkscape:export-xdpi="61.120499"
@@ -818,13 +756,13 @@
818 inkscape:export-ydpi="61.120499"
756 inkscape:export-ydpi="61.120499"
819 inkscape:export-xdpi="61.120499"
757 inkscape:export-xdpi="61.120499"
820 id="text1019"
758 id="text1019"
821− y="184.81636"
759+ y="218.94762"
822− x="97.366661"
760+ x="96.837494"
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"
761 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
762 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"
763 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"
764+ y="218.94762"
827− x="97.366661"
765+ x="96.837494"
828 id="tspan1017"
766 id="tspan1017"
829 sodipodi:role="line">module Text.Parser</tspan></text>
767 sodipodi:role="line">module Text.Parser</tspan></text>
830 <path
768 <path
@@ -910,68 +848,68 @@
910 id="rect1061"
848 id="rect1061"
911 width="59.266659"
849 width="59.266659"
912 height="16.13958"
850 height="16.13958"
913− x="92.339577"
851+ x="97.102074"
914− y="230.5896" />
852+ y="186.93335" />
915 <path
853 <path
916 inkscape:export-ydpi="61.120499"
854 inkscape:export-ydpi="61.120499"
917 inkscape:export-xdpi="61.120499"
855 inkscape:export-xdpi="61.120499"
918 inkscape:connector-curvature="0"
856 inkscape:connector-curvature="0"
919 id="path1063"
857 id="path1063"
920− d="m 76.993749,160.21044 21.695834,69.32083"
858+ d="m 76.993749,160.21044 18.785417,28.83958"
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)"
859 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" />
860 sodipodi:nodetypes="cc" />
923 <text
861 <text
924 inkscape:export-ydpi="61.120499"
862 inkscape:export-ydpi="61.120499"
925 inkscape:export-xdpi="61.120499"
863 inkscape:export-xdpi="61.120499"
926 id="text1081"
864 id="text1081"
927− y="236.14587"
865+ y="192.48962"
928− x="153.19336"
866+ x="157.95586"
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"
867 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
868 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"
869 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"
870+ y="192.48962"
933− x="153.19336"
871+ x="157.95586"
934 id="tspan1079"
872 id="tspan1079"
935− sodipodi:role="line">Either ParseError SExp</tspan></text>
873+ sodipodi:role="line">SExp</tspan></text>
936 <text
874 <text
937 inkscape:export-ydpi="61.120499"
875 inkscape:export-ydpi="61.120499"
938 inkscape:export-xdpi="61.120499"
876 inkscape:export-xdpi="61.120499"
939 id="text1089"
877 id="text1089"
940− y="236.41046"
878+ y="192.75421"
941− x="94.191658"
879+ x="98.954155"
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;"
880+ 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
881 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;"
882+ 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"
883+ y="192.75421"
946− x="94.191658"
884+ x="98.954155"
947 id="tspan1087"
885 id="tspan1087"
948 sodipodi:role="line">module Idris.IDEMode.Parser</tspan></text>
886 sodipodi:role="line">module Idris.IDEMode.Parser</tspan></text>
949 <rect
887 <rect
950 inkscape:export-ydpi="61.120499"
888 inkscape:export-ydpi="61.120499"
951 inkscape:export-xdpi="61.120499"
889 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"
890+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#7c007d;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"
891 id="rect1097"
954− width="35.983334"
892+ width="55.033333"
955− height="18.25625"
893+ height="14.287498"
956− x="124.08953"
894+ x="20.637447"
957− y="18.393738" />
895+ y="52.524986" />
958 <text
896 <text
959 inkscape:export-ydpi="61.120499"
897 inkscape:export-ydpi="61.120499"
960 inkscape:export-xdpi="61.120499"
898 inkscape:export-xdpi="61.120499"
961 id="text1101"
899 id="text1101"
962− y="24.479179"
900+ y="58.610428"
963− x="126.99989"
901+ x="23.54781"
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"
902+ 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:#800080;fill-opacity:1;stroke:none;stroke-width:0.26458332;"
965 xml:space="preserve"><tspan
903 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"
904+ 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:#800080;stroke-width:0.26458332;"
967− y="24.479179"
905+ y="58.610428"
968− x="126.99989"
906+ x="23.54781"
969 id="tspan1099"
907 id="tspan1099"
970 sodipodi:role="line">module Idris.REPL</tspan></text>
908 sodipodi:role="line">module Idris.REPL</tspan></text>
971 <path
909 <path
972 sodipodi:nodetypes="cc"
910 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)"
911 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"
912+ d="m 112.97708,174.23335 0,14.02292"
975 id="path1107"
913 id="path1107"
976 inkscape:connector-curvature="0"
914 inkscape:connector-curvature="0"
977 inkscape:export-xdpi="61.120499"
915 inkscape:export-xdpi="61.120499"
@@ -981,7 +919,7 @@
981 inkscape:export-xdpi="61.120499"
919 inkscape:export-xdpi="61.120499"
982 inkscape:connector-curvature="0"
920 inkscape:connector-curvature="0"
983 id="path1113"
921 id="path1113"
984− d="m 144.72708,173.43925 -0.26458,56.35661"
922+ d="m 148.43125,150.15592 0.26458,35.71911"
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)"
923 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" />
924 sodipodi:nodetypes="cc" />
987 <path
925 <path
@@ -989,27 +927,27 @@
989 inkscape:export-xdpi="61.120499"
927 inkscape:export-xdpi="61.120499"
990 inkscape:connector-curvature="0"
928 inkscape:connector-curvature="0"
991 id="path1119"
929 id="path1119"
992− d="m 151.80639,239.22321 44.91435,-0.41532"
930+ d="m 156.56889,195.56696 13.16435,-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)"
931 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" />
932 sodipodi:nodetypes="cc" />
995 <text
933 <text
996 id="text950"
934 id="text950"
997− y="236.19983"
935+ y="99.410255"
998− x="22.69136"
936+ x="145.19345"
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"
937 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"
938 xml:space="preserve"
1001 inkscape:export-xdpi="61.120499"
939 inkscape:export-xdpi="61.120499"
1002 inkscape:export-ydpi="61.120499"><tspan
940 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"
941 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"
942+ y="99.410255"
1005− x="22.69136"
943+ x="145.19345"
1006 id="tspan948"
944 id="tspan948"
1007 sodipodi:role="line">module Core.Core</tspan></text>
945 sodipodi:role="line">module Core.Core</tspan></text>
1008 <rect
946 <rect
1009 inkscape:export-ydpi="61.120499"
947 inkscape:export-ydpi="61.120499"
1010 inkscape:export-xdpi="61.120499"
948 inkscape:export-xdpi="61.120499"
1011− y="231.70166"
949+ y="94.912086"
1012− x="21.103861"
950+ x="143.60594"
1013 height="9.7895899"
951 height="9.7895899"
1014 width="47.889587"
952 width="47.889587"
1015 id="rect952"
953 id="rect952"
@@ -1019,57 +957,57 @@
1019 inkscape:export-xdpi="61.120499"
957 inkscape:export-xdpi="61.120499"
1020 xml:space="preserve"
958 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"
959 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"
960+ x="145.72261"
1023− y="239.90399"
961+ y="103.11442"
1024 id="text956"><tspan
962 id="text956"><tspan
1025 sodipodi:role="line"
963 sodipodi:role="line"
1026 id="tspan954"
964 id="tspan954"
1027− x="23.220528"
965+ x="145.72261"
1028− y="239.90399"
966+ y="103.11442"
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>
967 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
968 <text
1031 inkscape:export-ydpi="61.120499"
969 inkscape:export-ydpi="61.120499"
1032 inkscape:export-xdpi="61.120499"
970 inkscape:export-xdpi="61.120499"
1033 xml:space="preserve"
971 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"
972 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"
973+ x="83.81012"
1036− y="252.33942"
974+ y="78.243584"
1037 id="text960"><tspan
975 id="text960"><tspan
1038 sodipodi:role="line"
976 sodipodi:role="line"
1039 id="tspan958"
977 id="tspan958"
1040− x="22.69136"
978+ x="83.81012"
1041− y="252.33942"
979+ y="78.243584"
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>
980 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
981 <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"
982 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"
983 id="rect962"
1046 width="61.912495"
984 width="61.912495"
1047 height="18.785419"
985 height="18.785419"
1048− x="21.103861"
986+ x="82.22261"
1049− y="247.84125"
987+ y="73.745415"
1050 inkscape:export-xdpi="61.120499"
988 inkscape:export-xdpi="61.120499"
1051 inkscape:export-ydpi="61.120499" />
989 inkscape:export-ydpi="61.120499" />
1052 <text
990 <text
1053 id="text966"
991 id="text966"
1054− y="256.04358"
992+ y="81.947746"
1055− x="23.220528"
993+ x="84.339279"
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"
994 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"
995 xml:space="preserve"
1058 inkscape:export-xdpi="61.120499"
996 inkscape:export-xdpi="61.120499"
1059 inkscape:export-ydpi="61.120499"><tspan
997 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"
998 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"
999+ y="81.947746"
1062− x="23.220528"
1000+ x="84.339279"
1063 sodipodi:role="line"
1001 sodipodi:role="line"
1064 id="tspan968">Representation of expressions ready</tspan><tspan
1002 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"
1003 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"
1004+ y="86.357468"
1067− x="23.220528"
1005+ x="84.339279"
1068 sodipodi:role="line"
1006 sodipodi:role="line"
1069 id="tspan974">for compiling: CExp</tspan><tspan
1007 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"
1008 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"
1009+ y="90.767189"
1072− x="23.220528"
1010+ x="84.339279"
1073 sodipodi:role="line"
1011 sodipodi:role="line"
1074 id="tspan972">Type erased, explicit case trees</tspan></text>
1012 id="tspan972">Type erased, explicit case trees</tspan></text>
1075 <text
1013 <text
@@ -1077,34 +1015,34 @@
1077 inkscape:export-xdpi="61.120499"
1015 inkscape:export-xdpi="61.120499"
1078 xml:space="preserve"
1016 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"
1017 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"
1018+ x="22.162193"
1081− y="90.151314"
1019+ y="73.217979"
1082 id="text978"><tspan
1020 id="text978"><tspan
1083 sodipodi:role="line"
1021 sodipodi:role="line"
1084 id="tspan976"
1022 id="tspan976"
1085− x="22.69136"
1023+ x="22.162193"
1086− y="90.151314"
1024+ y="73.217979"
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>
1025 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
1026 <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"
1027 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"
1028 id="rect980"
1091 width="55.827087"
1029 width="55.827087"
1092 height="10.054173"
1030 height="10.054173"
1093− x="21.103861"
1031+ x="20.574694"
1094− y="85.653076"
1032+ y="68.719742"
1095 inkscape:export-xdpi="61.120499"
1033 inkscape:export-xdpi="61.120499"
1096 inkscape:export-ydpi="61.120499" />
1034 inkscape:export-ydpi="61.120499" />
1097 <text
1035 <text
1098 id="text984"
1036 id="text984"
1099− y="93.855484"
1037+ y="76.92215"
1100− x="23.220528"
1038+ x="22.69136"
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"
1039 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"
1040 xml:space="preserve"
1103 inkscape:export-xdpi="61.120499"
1041 inkscape:export-xdpi="61.120499"
1104 inkscape:export-ydpi="61.120499"><tspan
1042 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"
1043 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"
1044+ y="76.92215"
1107− x="23.220528"
1045+ x="22.69136"
1108 id="tspan982"
1046 id="tspan982"
1109 sodipodi:role="line">command line options</tspan></text>
1047 sodipodi:role="line">command line options</tspan></text>
1110 <text
1048 <text
@@ -1144,11 +1082,170 @@
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>
1082 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
1083 <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)"
1084 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"
1085+ d="m 142.54761,98.087086 c -7.32197,0.078 -68.613479,2.584834 -83.608332,4.234734"
1148 id="path996"
1086 id="path996"
1149 inkscape:connector-curvature="0"
1087 inkscape:connector-curvature="0"
1150 inkscape:export-xdpi="61.120499"
1088 inkscape:export-xdpi="61.120499"
1151 inkscape:export-ydpi="61.120499"
1089 inkscape:export-ydpi="61.120499"
1152 sodipodi:nodetypes="cc" />
1090 sodipodi:nodetypes="cc" />
1091+ <path
1092+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"
1093+ d="M 15.081249,210.48125 H 200.02499"
1094+ id="path1201"
1095+ inkscape:connector-curvature="0"
1096+ sodipodi:nodetypes="cc"
1097+ inkscape:export-xdpi="61.120499"
1098+ inkscape:export-ydpi="61.120499" />
1099+ <path
1100+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none;marker-start:url(#Arrow1Mstart);marker-end:url(#Arrow1Mend)"
1101+ d="m 154.78125,214.97917 -0.26459,40.21666"
1102+ id="path1203"
1103+ inkscape:connector-curvature="0"
1104+ inkscape:export-xdpi="61.120499"
1105+ inkscape:export-ydpi="61.120499" />
1106+ <text
1107+ xml:space="preserve"
1108+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:0.40000001;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1109+ x="158.75"
1110+ y="226.09137"
1111+ id="text1473"
1112+ inkscape:export-xdpi="61.120499"
1113+ inkscape:export-ydpi="61.120499"><tspan
1114+ sodipodi:role="line"
1115+ id="tspan1471"
1116+ x="158.75"
1117+ y="226.09137"
1118+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332">'text' modules are</tspan><tspan
1119+ sodipodi:role="line"
1120+ x="158.75"
1121+ y="230.92491"
1122+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1123+ id="tspan1475">also in Idris 1</tspan><tspan
1124+ sodipodi:role="line"
1125+ x="158.75"
1126+ y="235.75845"
1127+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1128+ id="tspan1477">library.</tspan></text>
1129+ <path
1130+ inkscape:connector-curvature="0"
1131+ id="path957"
1132+ d="m 172.77292,166.03125 -0.26459,40.21666"
1133+ 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-start:url(#marker969);marker-end:url(#marker973)"
1134+ inkscape:export-xdpi="61.120499"
1135+ inkscape:export-ydpi="61.120499" />
1136+ <text
1137+ inkscape:export-ydpi="61.120499"
1138+ inkscape:export-xdpi="61.120499"
1139+ id="text965"
1140+ y="177.14345"
1141+ x="176.74167"
1142+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:0.40000001;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#008000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"
1143+ xml:space="preserve"><tspan
1144+ id="tspan963"
1145+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1146+ y="177.14345"
1147+ x="176.74167"
1148+ sodipodi:role="line">'IDEMode is for</tspan><tspan
1149+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1150+ y="181.97699"
1151+ x="176.74167"
1152+ sodipodi:role="line"
1153+ id="tspan981">communicating</tspan><tspan
1154+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1155+ y="186.81053"
1156+ x="176.74167"
1157+ sodipodi:role="line"
1158+ id="tspan984">with external</tspan><tspan
1159+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1160+ y="191.64406"
1161+ x="176.74167"
1162+ sodipodi:role="line"
1163+ id="tspan987">editors. It uses</tspan><tspan
1164+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1165+ y="196.4776"
1166+ x="176.74167"
1167+ sodipodi:role="line"
1168+ id="tspan989">SExp structure</tspan><tspan
1169+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1170+ y="201.31114"
1171+ x="176.74167"
1172+ sodipodi:role="line"
1173+ id="tspan991">which is Lisp-</tspan><tspan
1174+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#008000;stroke-width:0.26458332;"
1175+ y="206.14468"
1176+ x="176.74167"
1177+ sodipodi:role="line"
1178+ id="tspan993">like.</tspan></text>
1179+ <path
1180+ 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-start:url(#marker1017);marker-end:url(#marker1021)"
1181+ d="m 172.77292,110.20417 -0.26459,40.21666"
1182+ id="path997"
1183+ inkscape:connector-curvature="0"
1184+ inkscape:export-xdpi="61.120499"
1185+ inkscape:export-ydpi="61.120499" />
1186+ <text
1187+ xml:space="preserve"
1188+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:0.40000001;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"
1189+ x="176.21251"
1190+ y="115.76012"
1191+ id="text1013"
1192+ inkscape:export-xdpi="61.120499"
1193+ inkscape:export-ydpi="61.120499"><tspan
1194+ id="tspan1011"
1195+ sodipodi:role="line"
1196+ x="176.21251"
1197+ y="115.76012"
1198+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332">Idris.Parser</tspan><tspan
1199+ sodipodi:role="line"
1200+ x="176.21251"
1201+ y="120.59366"
1202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1203+ id="tspan1050">reads from a</tspan><tspan
1204+ sodipodi:role="line"
1205+ x="176.21251"
1206+ y="125.42719"
1207+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1208+ id="tspan1052">file and outputs</tspan><tspan
1209+ sodipodi:role="line"
1210+ x="176.21251"
1211+ y="130.26073"
1212+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1213+ id="tspan1054">to a PTerm</tspan><tspan
1214+ sodipodi:role="line"
1215+ x="176.21251"
1216+ y="135.09427"
1217+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332"
1218+ id="tspan1056">structure.</tspan></text>
1219+ <path
1220+ inkscape:connector-curvature="0"
1221+ id="path1058"
1222+ d="m 171.97917,51.731253 -0.26459,19.57916"
1223+ 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-start:url(#marker1074);marker-end:url(#marker1078)"
1224+ sodipodi:nodetypes="cc"
1225+ inkscape:export-xdpi="61.120499"
1226+ inkscape:export-ydpi="61.120499" />
1227+ <text
1228+ inkscape:export-ydpi="61.120499"
1229+ inkscape:export-xdpi="61.120499"
1230+ id="text1070"
1231+ y="57.287201"
1232+ x="175.41876"
1233+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:0.40000001;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#800080;fill-opacity:1;stroke:none;stroke-width:0.26458332;"
1234+ xml:space="preserve"><tspan
1235+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#800080;stroke-width:0.26458332;"
1236+ y="57.287201"
1237+ x="175.41876"
1238+ sodipodi:role="line"
1239+ id="tspan1060">Idris.Parser</tspan><tspan
1240+ id="tspan1068"
1241+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#800080;stroke-width:0.26458332;"
1242+ y="62.120739"
1243+ x="175.41876"
1244+ sodipodi:role="line">reads from the</tspan><tspan
1245+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:0.40000001;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#800080;stroke-width:0.26458332;"
1246+ y="66.954277"
1247+ x="175.41876"
1248+ sodipodi:role="line"
1249+ id="tspan1089">command line.</tspan></text>
1153 </g>
1250 </g>
1154</svg>
1251</svg>
docs/parserLibrary/introduction.rst+32−4
@@ -4,6 +4,16 @@
4Parser Library Introduction
4Parser Library Introduction
5***************************
5***************************
6
6
7+The parser library can be used to build Idris structures from text. It involves a
8+certain amount of complexity and so it would typically be used for big projects. An
9+example might be a compiler for another language, written in Idris.
10+
11+Of course the parser library can also be used to compile to Idris, this is what is
12+done in Idris 2 and that is what the this library appears to have been written for.
13+
14+So a secondary use for this tutorial would be to help understanding the internal
15+workings of Idris 2.
16+
7The parser library is used in a similar way to Parsec which is a library for writing parsers in Haskell. It is based on higher-order parser combinators, so a complicated parser can be made out of many smaller ones.
17The parser library is used in a similar way to Parsec which is a library for writing parsers in Haskell. It is based on higher-order parser combinators, so a complicated parser can be made out of many smaller ones.
8
18
9.. list-table::
19.. list-table::
@@ -13,8 +23,8 @@ The parser library is used in a similar way to Parsec which is a library for wri
13 - Parser - This takes the list of tokens and outputs the code.
23 - Parser - This takes the list of tokens and outputs the code.
14
24
15.. image:: ../image/parserTopLevel.png
25.. image:: ../image/parserTopLevel.png
16− :width: 484px
26+ :width: 307px
17− :height: 147px
27+ :height: 76px
18 :alt: diagram illustrating these stages of lexer and parser
28 :alt: diagram illustrating these stages of lexer and parser
19
29
20The advantage of using two stages, like this, is that things like whitespace and comments don't need to be considered in every parser rule.
30The advantage of using two stages, like this, is that things like whitespace and comments don't need to be considered in every parser rule.
@@ -23,12 +33,30 @@ The Idris parser library differs from Parsec in that you need to say in the Rec
23
33
24The Lexer is similar but works at the level of characters rather than tokens, and you need to provide a TokenMap which says how to build a token representation from a string when a rule is matched.
34The Lexer is similar but works at the level of characters rather than tokens, and you need to provide a TokenMap which says how to build a token representation from a string when a rule is matched.
25
35
36+The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a tutorial for the :ref:`parserLibraryParser`. These tutorials have a running
37+example of a parser for integer expressions. This is a very simple example, there
38+may be easier ways to do something so simple, but it illustrates some of the principles.
39+
40+Parser Library and Idris 2
41+--------------------------
42+
43+The parser library, in Idris 1, is almost the same as the code that the Idris 2
44+parser is built on. Even if you only want to use the Idris 1 parser library it
45+is useful to look at the code in the Idris 2 compilers to see how the library can be used.
46+
47+Idris 2 has at least 3 compilers:
26
48
49+- IDEMode - complies to SExp which is a Lisp-like structure used to communicate
50+ with external editors like Emacs and Vim.
51+- Idris.Parser - This is the main compiler which compiles from a file to
52+ PTerm (and eventually TT structure).
53+- REPL - compiles input from the command line.
27
54
55+The following diagram is my attempt to work out how the modules in Idris 2 fit together.
28
56
29.. image:: ../image/parserModules.png
57.. image:: ../image/parserModules.png
30− :width: 484px
58+ :width: 460px
31− :height: 147px
59+ :height: 496px
32 :alt: diagram illustrating these stages of lexer and parser
60 :alt: diagram illustrating these stages of lexer and parser
33
61
34
62
docs/parserLibrary/lexer.rst+17
@@ -1,3 +1,5 @@
1+.. _parserLibraryLexer:
2+
1Lexer
3Lexer
2=====
4=====
3
5
@@ -97,6 +99,21 @@ This diagram shows the recogniser combinator with some of its constructors:
97 :height: 249px
99 :height: 249px
98 :alt: recogniser data structure
100 :alt: recogniser data structure
99
101
102+A recogniser consumes its input, that is it advances the index to its input
103+string, as it generates the token list. In some cases we don't want this to
104+happen, for instance, we may need to lookahead before consuming the input
105+string.
106+
107+If a recogniser does not consume input there is a danger of an infinite loop.
108+To prevent this the recogniser is dependent on a boolean called 'consumes' which
109+is true if the recogniser is guaranteed to consume at least one character.
110+
111+The constructors of Recognise allow us to ensure that, event though parts of
112+the recogniser may not consume, overall the recogniser will consume.
113+
114+Since 'Recognise True' is more common than 'Recognise False' it is convenient to
115+use 'Lexer' as a type synonym for 'Recognise True'.
116+
100Whitespace and Comments
117Whitespace and Comments
101-----------------------
118-----------------------
102
119
docs/parserLibrary/parser.rst+217−35
@@ -1,18 +1,29 @@
1+.. _parserLibraryParser:
2+
1Parser
3Parser
2======
4======
3
5
4−On the previous page we implemented a lexer to lex a very simple expression, on this
5−page we will go on to implement a parser for it.
6−
7−To run our parser we call 'doParse'. This requires the output from the lexer (a list of tokens) and a Grammar.
6+To run our parser we call 'parse'. This requires a Grammar and the output from the lexer (a list of tokens).
8
7
9.. code-block:: idris
8.. code-block:: idris
10
9
11− doParse : {c : Bool} ->
12− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
10+ parse : (act : Grammar tok c ty) -> (xs : List tok) ->
13− ParseResult xs c ty
11+ Either (ParseError tok) (ty, List tok)
12+
13+If successful this returns 'Right' with a pair of
14+
15+- the parse result
16+- the unparsed tokens (the remaining input)
14
17
18+otherwise it returns 'Left' with the error message.
19+
15−So we need to define the Grammar for our parser
20+So we need to define the Grammar for our parser, this is done using the following
21+'Grammar' data structure, this is a combinator structure similar in principle to the
22+recogniser combinator for the lexer which was discussed on the previous page.
23+
24+As with the Recogniser the Grammar type is dependent on a boolean 'consumes'
25+value which allows us to ensure that complicated Grammar structures will always
26+consume input.
16
27
17.. code-block:: idris
28.. code-block:: idris
18
29
@@ -40,27 +51,56 @@ So we need to define the Grammar for our parser
40 Grammar tok c1 ty -> Grammar tok c2 ty ->
51 Grammar tok c1 ty -> Grammar tok c2 ty ->
41 Grammar tok (c1 && c2) ty
52 Grammar tok (c1 && c2) ty
42
53
54+So an example of a Grammer type may look something like this:
55+'Grammar (TokenData ExpressionToken) True Integer'.
56+
57+This is a complicated type name and a given parser will need to use it a lot.
58+So to reduce the amount of typing we can use the following type synonym (similar
59+to what is done in Idris 2
60+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
61+
43.. code-block:: idris
62.. code-block:: idris
44
63
45− -- from Idris2/src/Parser/Support.idr
46 public export
64 public export
47 Rule : Type -> Type
65 Rule : Type -> Type
48 Rule ty = Grammar (TokenData ExpressionToken) True ty
66 Rule ty = Grammar (TokenData ExpressionToken) True ty
49
67
68+Parser Example
69+--------------
70+
71+On the previous page we implemented a lexer to 'lex' a very simple expression, on
72+this page we will go on to implement a parser for this running example.
73+
74+Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something
75+like this:
76+
77+.. code-block:: idris
78+
79+ <expr> ::= <integer literal>
80+ | <expr>'+'<expr>
81+ | <expr>'-'<expr>
82+ | <expr>'*'<expr>
83+ | '('<expr>')'
84+
85+ <integer literal> ::= <digit>|<integer literal><digit>
86+
87+To start, here is a Grammar to parse an integer literal (that is, a sequence of
88+numbers).
89+
50.. code-block:: idris
90.. code-block:: idris
51
91
52 export
92 export
53 intLiteral : Rule Integer
93 intLiteral : Rule Integer
54 intLiteral
94 intLiteral
55− = terminal --"Expected integer literal"
56− (\x => case tok x of
95+ = terminal (\x => case tok x of
57 Number i => Just i
96 Number i => Just i
58 _ => Nothing)
97 _ => Nothing)
59
98
60In order to try this out, here is a temporary function, this calls
99In order to try this out, here is a temporary function, this calls
61parse which takes two parameters:
100parse which takes two parameters:
101+
62−* The grammar (in this case intLiteral)
102+- The grammar (in this case intLiteral)
63−* The token list from the lexer.
103+- The token list from the lexer.
64
104
65.. code-block:: idris
105.. code-block:: idris
66
106
@@ -97,6 +137,13 @@ successful, this is because we are not specifically checking for end-of-file.
97 (Integer, List (TokenData ExpressionToken))
137 (Integer, List (TokenData ExpressionToken))
98 *parserEx>
138 *parserEx>
99
139
140+The 'intLiteral' function above uses the 'terminal' function to construct
141+the grammar, this is defined here
142+: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Parser/Core.idr
143+Idris 2 uses a slightly different version which stores an error message like
144+"Expected integer literal" which can be output if the rule fails
145+: https://github.com/edwinb/Idris2/blob/master/src/Text/Parser/Core.idr
146+
100.. code-block:: idris
147.. code-block:: idris
101
148
102 ||| Succeeds if running the predicate on the next token returns Just x,
149 ||| Succeeds if running the predicate on the next token returns Just x,
@@ -105,6 +152,9 @@ successful, this is because we are not specifically checking for end-of-file.
105 terminal : (tok -> Maybe a) -> Grammar tok True a
152 terminal : (tok -> Maybe a) -> Grammar tok True a
106 terminal = Terminal
153 terminal = Terminal
107
154
155+The 'terminal' function is also used to construct the other elements of the
156+grammar that we require, for instance, opening parenthesis:
157+
108.. code-block:: idris
158.. code-block:: idris
109
159
110 openParen : Rule Integer
160 openParen : Rule Integer
@@ -112,12 +162,19 @@ successful, this is because we are not specifically checking for end-of-file.
112 OParen => Just 0
162 OParen => Just 0
113 _ => Nothing)
163 _ => Nothing)
114
164
165+Integer value is not really relevant for parenthesis so '0' is used as
166+a default value.
167+As before, we can test this out with a function like this:
168+
115.. code-block:: idris
169.. code-block:: idris
116
170
117 test2 : String -> Either (ParseError (TokenData ExpressionToken))
171 test2 : String -> Either (ParseError (TokenData ExpressionToken))
118 (Integer, List (TokenData ExpressionToken))
172 (Integer, List (TokenData ExpressionToken))
119 test2 s = parse openParen (fst (lex expressionTokens s))
173 test2 s = parse openParen (fst (lex expressionTokens s))
120
174
175+We can see below that it correctly parses an open parenthesis and gives an
176+error for anything else:
177+
121.. code-block:: idris
178.. code-block:: idris
122
179
123 *parserEx> test2 "("
180 *parserEx> test2 "("
@@ -130,7 +187,12 @@ successful, this is because we are not specifically checking for end-of-file.
130 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
187 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
131 (Integer,
188 (Integer,
132 List (TokenData ExpressionToken))
189 List (TokenData ExpressionToken))
133− *parserEx>
190+
191+Now we have two Grammars we can try combining them. The following test looks
192+for 'openParen' followed by 'intLiteral', the two Grammars are combined using
193+'<*>'. The 'map const' part uses the integer value from the first.
194+
195+The following test is looking for '(' followed by a number:
134
196
135.. code-block:: idris
197.. code-block:: idris
136
198
@@ -138,6 +200,9 @@ successful, this is because we are not specifically checking for end-of-file.
138 (Integer, List (TokenData ExpressionToken))
200 (Integer, List (TokenData ExpressionToken))
139 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
201 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
140
202
203+We can see below that '(' followed by a number is successfully parsed but other
204+token lists are not:
205+
141.. code-block:: idris
206.. code-block:: idris
142
207
143 *parserEx> test3 "(123"
208 *parserEx> test3 "(123"
@@ -170,7 +235,8 @@ successful, this is because we are not specifically checking for end-of-file.
170 (incol, b) => cast (length incol))
235 (incol, b) => cast (length incol))
171 OParen]) : Either (ParseError (TokenData ExpressionToken))
236 OParen]) : Either (ParseError (TokenData ExpressionToken))
172 (Integer, List (TokenData ExpressionToken))
237 (Integer, List (TokenData ExpressionToken))
173− *parserEx>
238+
239+The closing parenthesis is constructed in the same way.
174
240
175.. code-block:: idris
241.. code-block:: idris
176
242
@@ -179,6 +245,36 @@ successful, this is because we are not specifically checking for end-of-file.
179 CParen => Just 0
245 CParen => Just 0
180 _ => Nothing)
246 _ => Nothing)
181
247
248+Now we can generate a Grammar for an expression inside parenthesis like this.
249+
250+.. code-block:: idris
251+
252+ paren : Rule Integer -> Rule Integer
253+ paren exp = openParen *> exp <* closeParen
254+
255+The use of '*>' and '<*' instead of '<*>' is an easy way to use the integer
256+value from the inner expression.
257+
258+Now for the operations, in this case: '+', '-' and '*'.
259+The syntax we require is that operators like '+' are infix operators, which
260+would require a definition like this:
261+
262+.. code-block:: idris
263+
264+ expr = (add expr (op "+") expr)
265+
266+This is a potentially infinite structure which is not total.
267+In order to work up to this gradually I will start with prefix operators (sometimes known as Polish notation)
268+then modify later for infix operators.
269+
270+So prefix operators would have this sort of form:
271+
272+.. code-block:: idris
273+
274+ expr = (add (op "+") expr expr)
275+
276+where 'op' is defined like this:
277+
182.. code-block:: idris
278.. code-block:: idris
183
279
184 ||| Matches if this is an operator token and string matches, that is,
280 ||| Matches if this is an operator token and string matches, that is,
@@ -188,10 +284,7 @@ successful, this is because we are not specifically checking for end-of-file.
188 (Operator s1) => if s==s1 then Just 0 else Nothing
284 (Operator s1) => if s==s1 then Just 0 else Nothing
189 _ => Nothing)
285 _ => Nothing)
190
286
191−.. code-block:: idris
287+and 'add' is defined like this:
192−
193− paren : Rule Integer -> Rule Integer
194− paren exp = openParen *> exp <* closeParen
195
288
196.. code-block:: idris
289.. code-block:: idris
197
290
@@ -205,6 +298,16 @@ successful, this is because we are not specifically checking for end-of-file.
205 Grammar tok ((c1 || c2) || c3) Integer
298 Grammar tok ((c1 || c2) || c3) Integer
206 add x y z = map addInt (x *> y) <*> z
299 add x y z = map addInt (x *> y) <*> z
207
300
301+Where:
302+
303+- x is the add operator.
304+- y is the first operand.
305+- z is the second operand.
306+
307+The resulting integer will be the sum of the two operands.
308+
309+The other operators are defined in a similar way:
310+
208.. code-block:: idris
311.. code-block:: idris
209
312
210 subInt : Integer -> Integer -> Integer
313 subInt : Integer -> Integer -> Integer
@@ -228,6 +331,9 @@ successful, this is because we are not specifically checking for end-of-file.
228 Grammar tok ((c1 || c2) || c3) Integer
331 Grammar tok ((c1 || c2) || c3) Integer
229 mult x y z = map multInt (x *> y) <*> z
332 mult x y z = map multInt (x *> y) <*> z
230
333
334+So the top level Grammar can now be defined as follows. Note that this is
335+partial as it is a potentially infinite structure and so not total.
336+
231.. code-block:: idris
337.. code-block:: idris
232
338
233 partial
339 partial
@@ -237,40 +343,116 @@ successful, this is because we are not specifically checking for end-of-file.
237 <|> (mult (op "*") expr expr)
343 <|> (mult (op "*") expr expr)
238 <|> intLiteral <|> (paren expr)
344 <|> intLiteral <|> (paren expr)
239
345
346+To make the testing easier we can use this function:
347+
240.. code-block:: idris
348.. code-block:: idris
241
349
350+ partial
351+ test : String -> Either (ParseError (TokenData ExpressionToken))
352+ (Integer, List (TokenData ExpressionToken))
242− *parserEx> parse expr (fst (lex expressionTokens "(1)"))
353+ test s = parse expr (fst (lex expressionTokens s))
243− Right (1, []) : Either (ParseError (TokenData ExpressionToken))
354+
244− (Integer, List (TokenData ExpressionToken))
355+First test a valid (prefix) expression:
245− *parserEx>
246
356
247.. code-block:: idris
357.. code-block:: idris
248
358
249− parse : (act : Grammar tok c ty) -> (xs : List tok)
359+ *parserEx> test "+1*6(4)"
360+ Right (25,
361+ []) : Either (ParseError (TokenData ExpressionToken))
362+ (Integer, List (TokenData ExpressionToken))
250
363
251− parse intLiteral (fst (lex expressionTokens "1"))
364+Then an invalid syntax:
252
365
253.. code-block:: idris
366.. code-block:: idris
254
367
255− *parserEx> parse expr (fst (lex expressionTokens "1+2"))
368+ *parserEx> test "))"
369+ Left (Error "Unrecognised token"
370+ [MkToken 0 0 CParen,
371+ MkToken 0
372+ (case fspan (\ARG =>
373+ not (intToBool (prim__eqChar ARG
374+ '\n')))
375+ ")" of
376+ (incol, "") => c + cast (length incol)
377+ (incol, b) => cast (length incol))
378+ CParen]) : Either (ParseError (TokenData ExpressionToken))
379+ (Integer,
380+ List (TokenData ExpressionToken))
381+
382+However if we try something that is invalid, but starts with a valid token,
383+then it will return 'Right' (to indicate success)
384+
385+.. code-block:: idris
386+
387+ *parserEx> test "1))"
256 Right (1,
388 Right (1,
257 [MkToken 0
389 [MkToken 0
390+ (case fspan (\ARG =>
258− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
391+ not (intToBool (prim__eqChar ARG '\n')))
392+ "1" of
259 (incol, "") => c + cast (length incol)
393 (incol, "") => c + cast (length incol)
260 (incol, b) => cast (length incol))
394 (incol, b) => cast (length incol))
261− (Operator "+"),
395+ CParen,
262 MkToken 0
396 MkToken 0
397+ (case fspan (\ARG =>
263− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
398+ not (intToBool (prim__eqChar ARG '\n')))
399+ ")" of
264 (incol, "") => c + cast (length incol)
400 (incol, "") => c + cast (length incol)
265 (incol, b) => cast (length incol))
401 (incol, b) => cast (length incol))
266− (Number 2)]) : Either (ParseError (TokenData ExpressionToken))
402+ CParen]) : Either (ParseError (TokenData ExpressionToken))
403+ (Integer,
267− (Integer, List (TokenData ExpressionToken))
404+ List (TokenData ExpressionToken))
268− *parserEx>
405+
406+Infix Notation
407+--------------
408+
409+So far we have implemented a prefix notation for operators (like this: '+ expr expr')
410+but the aim is to implemented an infix notation (like this: 'expr + expr'). To do
411+this we must be able to deal with potentially infinite data structures (see Codata Types
412+here :ref:`sect-typefuns`).
413+
414+First alter the grammar to have infix operations:
269
415
270.. code-block:: idris
416.. code-block:: idris
271
417
418+ addInt : Integer -> Integer -> Integer
419+ addInt a b = a+b
420+
421+ export
422+ add : Grammar tok c1 Integer ->
423+ Grammar tok c2 Integer ->
424+ Grammar tok c3 Integer ->
425+ Grammar tok ((c1 || c2) || c3) Integer
426+ add x y z = map addInt (x <* y) <*> z
427+
428+ subInt : Integer -> Integer -> Integer
429+ subInt a b = a-b
430+
431+ export
432+ sub : Grammar tok c1 Integer ->
433+ Grammar tok c2 Integer ->
434+ Grammar tok c3 Integer ->
435+ Grammar tok ((c1 || c2) || c3) Integer
436+ sub x y z = map subInt (x <* y) <*> z
437+
438+
439+ multInt : Integer -> Integer -> Integer
440+ multInt a b = a*b
441+
442+ export
443+ mult : Grammar tok c1 Integer ->
444+ Grammar tok c2 Integer ->
445+ Grammar tok c3 Integer ->
446+ Grammar tok ((c1 || c2) || c3) Integer
447+ mult x y z = map multInt (x <* y) <*> z
448+
272 partial
449 partial
273− test : String -> Either (ParseError (TokenData ExpressionToken))
450+ expr : Rule Integer
274− (Integer, List (TokenData ExpressionToken))
451+ expr = (add expr (op "+") expr)
275− test s = parse expr (fst (lex expressionTokens s))
452+ <|> (sub expr (op "-") expr)
453+ <|> (mult expr (op "*") expr)
454+ <|> intLiteral <|> (paren expr)
455+
456+However, if this was run, the code would not terminate.
457+
276
458