git.iko.soy/Idris-dev
on master help sign in
work on parser page
commitaf2766ca1482e2a45d6ead5723f4a7bfc4379366 authormartinbaker <git29f185@martinb.com> dateThu 2 Jan 2020, 09:34 (7 years ago) parentfdc5a52
6 files changed+649−325
compare with master
unifiedsplit
docs/conf.py+1−1 docs/image/parserModules.png docs/image/parserModules.svg+382−285 docs/parserLibrary/introduction.rst+32−4 docs/parserLibrary/lexer.rst+17 docs/parserLibrary/parser.rst+217−35
docs/conf.py+1−1
@@ -51,7 +51,7 @@ master_doc = 'index'
5151
5252# General information about the project.
5353project = u'Idris'
54−copyright = u'2017-2019, The Idris Community'
54+copyright = u'2017-2020, The Idris Community'
5555author = u'The Idris Community'
5656
5757# 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 @@
1515 version="1.1"
1616 id="svg8"
1717 inkscape:version="0.92.2 5c3e80d, 2017-08-06"
18− sodipodi:docname="modules.svg">
18+ sodipodi:docname="parserModules.svg">
1919 <defs
2020 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>
21139 <marker
22140 inkscape:isstock="true"
23141 style="overflow:visible;"
@@ -278,21 +396,6 @@
278396 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 "
279397 id="path3615" />
280398 </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>
296399 <marker
297400 inkscape:stockid="Arrow1Mend"
298401 orient="auto"
@@ -323,21 +426,6 @@
323426 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 "
324427 id="path1537" />
325428 </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>
341429 </defs>
342430 <sodipodi:namedview
343431 id="base"
@@ -348,15 +436,16 @@
348436 inkscape:pageshadow="2"
349437 inkscape:zoom="1"
350438 inkscape:cx="368.33949"
351− inkscape:cy="554.8721"
439+ inkscape:cy="617.07597"
352440 inkscape:document-units="mm"
353441 inkscape:current-layer="layer1"
354442 showgrid="false"
355− inkscape:window-width="1359"
443+ inkscape:window-width="1800"
356444 inkscape:window-height="1011"
357− inkscape:window-x="-4"
445+ inkscape:window-x="0"
358446 inkscape:window-y="0"
359− inkscape:window-maximized="0" />
447+ inkscape:window-maximized="0"
448+ inkscape:snap-nodes="false" />
360449 <metadata
361450 id="metadata5">
362451 <rdf:RDF>
@@ -373,157 +462,6 @@
373462 inkscape:label="Layer 1"
374463 inkscape:groupmode="layer"
375464 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>
527465 <text
528466 inkscape:export-ydpi="61.120499"
529467 inkscape:export-xdpi="61.120499"
@@ -645,15 +583,15 @@
645583 id="tspan921">List (TokenData Token)</tspan></text>
646584 <text
647585 id="text931"
648− y="184.2872"
649− x="37.041664"
586+ y="218.41846"
587+ x="36.512497"
650588 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"
651589 xml:space="preserve"
652590 inkscape:export-xdpi="61.120499"
653591 inkscape:export-ydpi="61.120499"><tspan
654592 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"
593+ y="218.41846"
594+ x="36.512497"
657595 id="tspan929"
658596 sodipodi:role="line">module Text.Lexer</tspan></text>
659597 <text
@@ -672,8 +610,8 @@
672610 <rect
673611 inkscape:export-ydpi="61.120499"
674612 inkscape:export-xdpi="61.120499"
675− y="180.05362"
676− x="32.543747"
613+ y="214.18488"
614+ x="32.01458"
677615 height="6.3500061"
678616 width="43.656254"
679617 id="rect937"
@@ -685,8 +623,8 @@
685623 id="rect939"
686624 width="42.862495"
687625 height="6.8791728"
688− x="95.51458"
689− y="180.05362" />
626+ x="94.985413"
627+ y="214.18488" />
690628 <text
691629 inkscape:export-ydpi="61.120499"
692630 inkscape:export-xdpi="61.120499"
@@ -706,33 +644,33 @@
706644 inkscape:export-xdpi="61.120499"
707645 inkscape:connector-curvature="0"
708646 id="path963"
709− d="m 53.828728,179.89081 1.006873,-18.52084"
647+ d="m 53.299561,213.22831 1.53604,-51.85834"
710648 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)" />
711649 <text
712650 inkscape:export-ydpi="61.120499"
713651 inkscape:export-xdpi="61.120499"
714652 xml:space="preserve"
715653 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"
654+ x="23.220526"
655+ y="251.01649"
718656 id="text971"><tspan
719657 sodipodi:role="line"
720658 id="tspan969"
721− x="23.749693"
722− y="216.88524"
659+ x="23.220526"
660+ y="251.01649"
723661 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>
724662 <rect
725663 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"
726664 id="rect973"
727665 width="47.889587"
728666 height="6.3500061"
729− x="22.162193"
730− y="212.38707"
667+ x="21.633026"
668+ y="246.51833"
731669 inkscape:export-xdpi="61.120499"
732670 inkscape:export-ydpi="61.120499" />
733671 <path
734672 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"
736674 id="path975"
737675 inkscape:connector-curvature="0"
738676 inkscape:export-xdpi="61.120499"
@@ -740,22 +678,22 @@
740678 sodipodi:nodetypes="cc" />
741679 <text
742680 id="text979"
743− y="207.83517"
744− x="23.812496"
681+ y="241.96643"
682+ x="23.283329"
745683 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"
746684 xml:space="preserve"
747685 inkscape:export-xdpi="61.120499"
748686 inkscape:export-ydpi="61.120499"><tspan
749687 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"
688+ y="241.96643"
689+ x="23.283329"
752690 id="tspan977"
753691 sodipodi:role="line">module Text.Quantity</tspan></text>
754692 <rect
755693 inkscape:export-ydpi="61.120499"
756694 inkscape:export-xdpi="61.120499"
757− y="203.33701"
758− x="22.224997"
695+ y="237.46826"
696+ x="21.695829"
759697 height="6.2469702"
760698 width="43.853985"
761699 id="rect981"
@@ -765,21 +703,21 @@
765703 inkscape:export-xdpi="61.120499"
766704 xml:space="preserve"
767705 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"
706+ x="23.18244"
707+ y="233.68523"
770708 id="text985"><tspan
771709 sodipodi:role="line"
772710 id="tspan983"
773− x="23.711607"
774− y="199.55397"
711+ x="23.18244"
712+ y="233.68523"
775713 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>
776714 <rect
777715 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"
778716 id="rect987"
779717 width="39.011257"
780718 height="5.9464455"
781− x="22.124107"
782− y="195.0558"
719+ x="21.59494"
720+ y="229.18706"
783721 inkscape:export-xdpi="61.120499"
784722 inkscape:export-ydpi="61.120499" />
785723 <path
@@ -788,11 +726,11 @@
788726 inkscape:export-xdpi="61.120499"
789727 inkscape:connector-curvature="0"
790728 id="path993"
791− d="M 63.527551,202.87958 63.375204,187.79022"
729+ d="M 62.998384,237.01083 62.846037,221.92147"
792730 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)" />
793731 <path
794732 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"
796734 id="path999"
797735 inkscape:connector-curvature="0"
798736 inkscape:export-xdpi="61.120499"
@@ -800,7 +738,7 @@
800738 sodipodi:nodetypes="cc" />
801739 <path
802740 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"
804742 id="path1005"
805743 inkscape:connector-curvature="0"
806744 inkscape:export-xdpi="61.120499"
@@ -808,7 +746,7 @@
808746 sodipodi:nodetypes="cc" />
809747 <path
810748 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"
812750 id="path1011"
813751 inkscape:connector-curvature="0"
814752 inkscape:export-xdpi="61.120499"
@@ -818,13 +756,13 @@
818756 inkscape:export-ydpi="61.120499"
819757 inkscape:export-xdpi="61.120499"
820758 id="text1019"
821− y="184.81636"
822− x="97.366661"
759+ y="218.94762"
760+ x="96.837494"
823761 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"
824762 xml:space="preserve"><tspan
825763 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"
764+ y="218.94762"
765+ x="96.837494"
828766 id="tspan1017"
829767 sodipodi:role="line">module Text.Parser</tspan></text>
830768 <path
@@ -910,68 +848,68 @@
910848 id="rect1061"
911849 width="59.266659"
912850 height="16.13958"
913− x="92.339577"
914− y="230.5896" />
851+ x="97.102074"
852+ y="186.93335" />
915853 <path
916854 inkscape:export-ydpi="61.120499"
917855 inkscape:export-xdpi="61.120499"
918856 inkscape:connector-curvature="0"
919857 id="path1063"
920− d="m 76.993749,160.21044 21.695834,69.32083"
858+ d="m 76.993749,160.21044 18.785417,28.83958"
921859 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)"
922860 sodipodi:nodetypes="cc" />
923861 <text
924862 inkscape:export-ydpi="61.120499"
925863 inkscape:export-xdpi="61.120499"
926864 id="text1081"
927− y="236.14587"
928− x="153.19336"
865+ y="192.48962"
866+ x="157.95586"
929867 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"
930868 xml:space="preserve"><tspan
931869 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"
870+ y="192.48962"
871+ x="157.95586"
934872 id="tspan1079"
935− sodipodi:role="line">Either ParseError SExp</tspan></text>
873+ sodipodi:role="line">SExp</tspan></text>
936874 <text
937875 inkscape:export-ydpi="61.120499"
938876 inkscape:export-xdpi="61.120499"
939877 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;"
878+ y="192.75421"
879+ x="98.954155"
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"
943881 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"
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"
883+ y="192.75421"
884+ x="98.954155"
947885 id="tspan1087"
948886 sodipodi:role="line">module Idris.IDEMode.Parser</tspan></text>
949887 <rect
950888 inkscape:export-ydpi="61.120499"
951889 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"
953891 id="rect1097"
954− width="35.983334"
955− height="18.25625"
956− x="124.08953"
957− y="18.393738" />
892+ width="55.033333"
893+ height="14.287498"
894+ x="20.637447"
895+ y="52.524986" />
958896 <text
959897 inkscape:export-ydpi="61.120499"
960898 inkscape:export-xdpi="61.120499"
961899 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"
900+ y="58.610428"
901+ x="23.54781"
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;"
965903 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"
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;"
905+ y="58.610428"
906+ x="23.54781"
969907 id="tspan1099"
970908 sodipodi:role="line">module Idris.REPL</tspan></text>
971909 <path
972910 sodipodi:nodetypes="cc"
973911 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"
975913 id="path1107"
976914 inkscape:connector-curvature="0"
977915 inkscape:export-xdpi="61.120499"
@@ -981,7 +919,7 @@
981919 inkscape:export-xdpi="61.120499"
982920 inkscape:connector-curvature="0"
983921 id="path1113"
984− d="m 144.72708,173.43925 -0.26458,56.35661"
922+ d="m 148.43125,150.15592 0.26458,35.71911"
985923 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)"
986924 sodipodi:nodetypes="cc" />
987925 <path
@@ -989,27 +927,27 @@
989927 inkscape:export-xdpi="61.120499"
990928 inkscape:connector-curvature="0"
991929 id="path1119"
992− d="m 151.80639,239.22321 44.91435,-0.41532"
930+ d="m 156.56889,195.56696 13.16435,-0.41532"
993931 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)"
994932 sodipodi:nodetypes="cc" />
995933 <text
996934 id="text950"
997− y="236.19983"
998− x="22.69136"
935+ y="99.410255"
936+ x="145.19345"
999937 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"
1000938 xml:space="preserve"
1001939 inkscape:export-xdpi="61.120499"
1002940 inkscape:export-ydpi="61.120499"><tspan
1003941 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"
942+ y="99.410255"
943+ x="145.19345"
1006944 id="tspan948"
1007945 sodipodi:role="line">module Core.Core</tspan></text>
1008946 <rect
1009947 inkscape:export-ydpi="61.120499"
1010948 inkscape:export-xdpi="61.120499"
1011− y="231.70166"
1012− x="21.103861"
949+ y="94.912086"
950+ x="143.60594"
1013951 height="9.7895899"
1014952 width="47.889587"
1015953 id="rect952"
@@ -1019,57 +957,57 @@
1019957 inkscape:export-xdpi="61.120499"
1020958 xml:space="preserve"
1021959 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"
960+ x="145.72261"
961+ y="103.11442"
1024962 id="text956"><tspan
1025963 sodipodi:role="line"
1026964 id="tspan954"
1027− x="23.220528"
1028− y="239.90399"
965+ x="145.72261"
966+ y="103.11442"
1029967 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>
1030968 <text
1031969 inkscape:export-ydpi="61.120499"
1032970 inkscape:export-xdpi="61.120499"
1033971 xml:space="preserve"
1034972 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"
973+ x="83.81012"
974+ y="78.243584"
1037975 id="text960"><tspan
1038976 sodipodi:role="line"
1039977 id="tspan958"
1040− x="22.69136"
1041− y="252.33942"
978+ x="83.81012"
979+ y="78.243584"
1042980 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>
1043981 <rect
1044982 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"
1045983 id="rect962"
1046984 width="61.912495"
1047985 height="18.785419"
1048− x="21.103861"
1049− y="247.84125"
986+ x="82.22261"
987+ y="73.745415"
1050988 inkscape:export-xdpi="61.120499"
1051989 inkscape:export-ydpi="61.120499" />
1052990 <text
1053991 id="text966"
1054− y="256.04358"
1055− x="23.220528"
992+ y="81.947746"
993+ x="84.339279"
1056994 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"
1057995 xml:space="preserve"
1058996 inkscape:export-xdpi="61.120499"
1059997 inkscape:export-ydpi="61.120499"><tspan
1060998 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"
999+ y="81.947746"
1000+ x="84.339279"
10631001 sodipodi:role="line"
10641002 id="tspan968">Representation of expressions ready</tspan><tspan
10651003 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"
1004+ y="86.357468"
1005+ x="84.339279"
10681006 sodipodi:role="line"
10691007 id="tspan974">for compiling: CExp</tspan><tspan
10701008 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"
1009+ y="90.767189"
1010+ x="84.339279"
10731011 sodipodi:role="line"
10741012 id="tspan972">Type erased, explicit case trees</tspan></text>
10751013 <text
@@ -1077,34 +1015,34 @@
10771015 inkscape:export-xdpi="61.120499"
10781016 xml:space="preserve"
10791017 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"
1018+ x="22.162193"
1019+ y="73.217979"
10821020 id="text978"><tspan
10831021 sodipodi:role="line"
10841022 id="tspan976"
1085− x="22.69136"
1086− y="90.151314"
1023+ x="22.162193"
1024+ y="73.217979"
10871025 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>
10881026 <rect
10891027 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"
10901028 id="rect980"
10911029 width="55.827087"
10921030 height="10.054173"
1093− x="21.103861"
1094− y="85.653076"
1031+ x="20.574694"
1032+ y="68.719742"
10951033 inkscape:export-xdpi="61.120499"
10961034 inkscape:export-ydpi="61.120499" />
10971035 <text
10981036 id="text984"
1099− y="93.855484"
1100− x="23.220528"
1037+ y="76.92215"
1038+ x="22.69136"
11011039 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"
11021040 xml:space="preserve"
11031041 inkscape:export-xdpi="61.120499"
11041042 inkscape:export-ydpi="61.120499"><tspan
11051043 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"
1044+ y="76.92215"
1045+ x="22.69136"
11081046 id="tspan982"
11091047 sodipodi:role="line">command line options</tspan></text>
11101048 <text
@@ -1144,11 +1082,170 @@
11441082 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>
11451083 <path
11461084 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"
11481086 id="path996"
11491087 inkscape:connector-curvature="0"
11501088 inkscape:export-xdpi="61.120499"
11511089 inkscape:export-ydpi="61.120499"
11521090 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>
11531250 </g>
11541251</svg>
docs/parserLibrary/introduction.rst+32−4
@@ -4,6 +4,16 @@
44Parser Library Introduction
55***************************
66
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+
717The 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.
818
919.. list-table::
@@ -13,8 +23,8 @@ The parser library is used in a similar way to Parsec which is a library for wri
1323 - Parser - This takes the list of tokens and outputs the code.
1424
1525.. image:: ../image/parserTopLevel.png
16− :width: 484px
17− :height: 147px
26+ :width: 307px
27+ :height: 76px
1828 :alt: diagram illustrating these stages of lexer and parser
1929
2030The 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
2333
2434The 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.
2535
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:
2648
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.
2754
55+The following diagram is my attempt to work out how the modules in Idris 2 fit together.
2856
2957.. image:: ../image/parserModules.png
30− :width: 484px
31− :height: 147px
58+ :width: 460px
59+ :height: 496px
3260 :alt: diagram illustrating these stages of lexer and parser
3361
3462
docs/parserLibrary/lexer.rst+17
@@ -1,3 +1,5 @@
1+.. _parserLibraryLexer:
2+
13Lexer
24=====
35
@@ -97,6 +99,21 @@ This diagram shows the recogniser combinator with some of its constructors:
9799 :height: 249px
98100 :alt: recogniser data structure
99101
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+
100117Whitespace and Comments
101118-----------------------
102119
docs/parserLibrary/parser.rst+217−35
@@ -1,18 +1,29 @@
1+.. _parserLibraryParser:
2+
13Parser
24======
35
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).
87
98.. code-block:: idris
109
11− doParse : {c : Bool} ->
12− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
13− ParseResult xs c ty
10+ parse : (act : Grammar tok c ty) -> (xs : List tok) ->
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)
1417
15−So we need to define the Grammar for our parser
18+otherwise it returns 'Left' with the error message.
19+
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.
1627
1728.. code-block:: idris
1829
@@ -40,27 +51,56 @@ So we need to define the Grammar for our parser
4051 Grammar tok c1 ty -> Grammar tok c2 ty ->
4152 Grammar tok (c1 && c2) ty
4253
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+
4362.. code-block:: idris
4463
45− -- from Idris2/src/Parser/Support.idr
4664 public export
4765 Rule : Type -> Type
4866 Rule ty = Grammar (TokenData ExpressionToken) True ty
4967
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+
5090.. code-block:: idris
5191
5292 export
5393 intLiteral : Rule Integer
5494 intLiteral
55− = terminal --"Expected integer literal"
56− (\x => case tok x of
95+ = terminal (\x => case tok x of
5796 Number i => Just i
5897 _ => Nothing)
5998
6099In order to try this out, here is a temporary function, this calls
61100parse which takes two parameters:
62−* The grammar (in this case intLiteral)
63−* The token list from the lexer.
101+
102+- The grammar (in this case intLiteral)
103+- The token list from the lexer.
64104
65105.. code-block:: idris
66106
@@ -97,6 +137,13 @@ successful, this is because we are not specifically checking for end-of-file.
97137 (Integer, List (TokenData ExpressionToken))
98138 *parserEx>
99139
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+
100147.. code-block:: idris
101148
102149 ||| 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.
105152 terminal : (tok -> Maybe a) -> Grammar tok True a
106153 terminal = Terminal
107154
155+The 'terminal' function is also used to construct the other elements of the
156+grammar that we require, for instance, opening parenthesis:
157+
108158.. code-block:: idris
109159
110160 openParen : Rule Integer
@@ -112,12 +162,19 @@ successful, this is because we are not specifically checking for end-of-file.
112162 OParen => Just 0
113163 _ => Nothing)
114164
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+
115169.. code-block:: idris
116170
117171 test2 : String -> Either (ParseError (TokenData ExpressionToken))
118172 (Integer, List (TokenData ExpressionToken))
119173 test2 s = parse openParen (fst (lex expressionTokens s))
120174
175+We can see below that it correctly parses an open parenthesis and gives an
176+error for anything else:
177+
121178.. code-block:: idris
122179
123180 *parserEx> test2 "("
@@ -130,7 +187,12 @@ successful, this is because we are not specifically checking for end-of-file.
130187 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
131188 (Integer,
132189 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:
134196
135197.. code-block:: idris
136198
@@ -138,6 +200,9 @@ successful, this is because we are not specifically checking for end-of-file.
138200 (Integer, List (TokenData ExpressionToken))
139201 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
140202
203+We can see below that '(' followed by a number is successfully parsed but other
204+token lists are not:
205+
141206.. code-block:: idris
142207
143208 *parserEx> test3 "(123"
@@ -170,7 +235,8 @@ successful, this is because we are not specifically checking for end-of-file.
170235 (incol, b) => cast (length incol))
171236 OParen]) : Either (ParseError (TokenData ExpressionToken))
172237 (Integer, List (TokenData ExpressionToken))
173− *parserEx>
238+
239+The closing parenthesis is constructed in the same way.
174240
175241.. code-block:: idris
176242
@@ -179,6 +245,36 @@ successful, this is because we are not specifically checking for end-of-file.
179245 CParen => Just 0
180246 _ => Nothing)
181247
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+
182278.. code-block:: idris
183279
184280 ||| 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.
188284 (Operator s1) => if s==s1 then Just 0 else Nothing
189285 _ => Nothing)
190286
191−.. code-block:: idris
192−
193− paren : Rule Integer -> Rule Integer
194− paren exp = openParen *> exp <* closeParen
287+and 'add' is defined like this:
195288
196289.. code-block:: idris
197290
@@ -205,6 +298,16 @@ successful, this is because we are not specifically checking for end-of-file.
205298 Grammar tok ((c1 || c2) || c3) Integer
206299 add x y z = map addInt (x *> y) <*> z
207300
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+
208311.. code-block:: idris
209312
210313 subInt : Integer -> Integer -> Integer
@@ -228,6 +331,9 @@ successful, this is because we are not specifically checking for end-of-file.
228331 Grammar tok ((c1 || c2) || c3) Integer
229332 mult x y z = map multInt (x *> y) <*> z
230333
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+
231337.. code-block:: idris
232338
233339 partial
@@ -237,40 +343,116 @@ successful, this is because we are not specifically checking for end-of-file.
237343 <|> (mult (op "*") expr expr)
238344 <|> intLiteral <|> (paren expr)
239345
346+To make the testing easier we can use this function:
347+
240348.. code-block:: idris
241349
242− *parserEx> parse expr (fst (lex expressionTokens "(1)"))
243− Right (1, []) : Either (ParseError (TokenData ExpressionToken))
244− (Integer, List (TokenData ExpressionToken))
245− *parserEx>
350+ partial
351+ test : String -> Either (ParseError (TokenData ExpressionToken))
352+ (Integer, List (TokenData ExpressionToken))
353+ test s = parse expr (fst (lex expressionTokens s))
354+
355+First test a valid (prefix) expression:
246356
247357.. code-block:: idris
248358
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))
250363
251− parse intLiteral (fst (lex expressionTokens "1"))
364+Then an invalid syntax:
252365
253366.. code-block:: idris
254367
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))"
256388 Right (1,
257389 [MkToken 0
258− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
390+ (case fspan (\ARG =>
391+ not (intToBool (prim__eqChar ARG '\n')))
392+ "1" of
259393 (incol, "") => c + cast (length incol)
260394 (incol, b) => cast (length incol))
261− (Operator "+"),
395+ CParen,
262396 MkToken 0
263− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
397+ (case fspan (\ARG =>
398+ not (intToBool (prim__eqChar ARG '\n')))
399+ ")" of
264400 (incol, "") => c + cast (length incol)
265401 (incol, b) => cast (length incol))
266− (Number 2)]) : Either (ParseError (TokenData ExpressionToken))
267− (Integer, List (TokenData ExpressionToken))
268− *parserEx>
402+ CParen]) : Either (ParseError (TokenData ExpressionToken))
403+ (Integer,
404+ List (TokenData ExpressionToken))
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:
269415
270416.. code-block:: idris
271417
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+
272449 partial
273− test : String -> Either (ParseError (TokenData ExpressionToken))
274− (Integer, List (TokenData ExpressionToken))
275− test s = parse expr (fst (lex expressionTokens s))
450+ expr : Rule Integer
451+ expr = (add expr (op "+") expr)
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+
276458