e79aaaa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'origin/master' into ghc-8.8

commite79aaaae22c9522afc40050c898bac780d17362e authorNiklas Larsson <niklas@mm.st> dateSat 25 Jan 2020, 03:58 (7 years ago) parent57624a8 1f9ad21

72 files changed+4128−87

compare with master

unifiedsplit

CITATION.md+1−1

@@ -17,7 +17,7 @@ If you use `Idris` in your work we would prefer it if you would use the followin

1717 pages = {552--593},

1818 numpages = {42},

1919 doi = {10.1017/S095679681300018X},

20− URL = {http://journals.cambridge.org/article_S095679681300018X},

20+ URL = {https://journals.cambridge.org/article_S095679681300018X},

2121}

2222```

2323

CONTRIBUTING.md+5−5

@@ -6,9 +6,9 @@ Here are a few guidelines that we would like contributors to follow so that we c

77## Getting Started

9−1. Make sure you are familiar with [Git](http://git-scm.com/book).

9+1. Make sure you are familiar with [Git](https://git-scm.com/book).

10101. Make sure you have a [GitHub account](https://github.com/signup/free).

11−1. Make sure you are familiar with: [Idris](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).

11+1. Make sure you are familiar with: [Idris](https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).

12121. Make sure you can install Idris:

1313 * [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)

1414 * [Ubuntu](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Ubuntu)

@@ -72,7 +72,7 @@ We do not want you wasting your time nor duplicating somebody's work!

7272

7373## Making Changes

7474

75−Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).

75+Idris developers and hackers try to adhere to something similar to the [successful git branching model](https://nvie.com/posts/a-successful-git-branching-model/).

7676The steps are described below.

7777

7878### New contributors

@@ -175,8 +175,8 @@ To help increase the chance of your pull request being accepted:

175175* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);

176176* [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);

177177* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);

178−* [Idris News](http://www.idris-lang.org/news/);

179−* [other Idris docs](http://www.idris-lang.org/documentation/).

178+* [Idris News](https://www.idris-lang.org/news/);

179+* [other Idris docs](https://www.idris-lang.org/documentation/).

180180* [Using Pull Requests](https://help.github.com/articles/using-pull-requests)

181181* [General GitHub Documentation](https://help.github.com/).

182182

Makefile+1−1

@@ -56,7 +56,7 @@ linecount:

5656

5757#Note: this doesn't yet link to Hackage properly

5858doc: dist/setup-config

59− $(CABAL) v1-haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

59+ $(CABAL) v1-haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

6060

6161lib_doc:

6262 $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc

README.md+4−4

@@ -4,11 +4,11 @@

44[![Appveyor build](https://ci.appveyor.com/api/projects/status/xi8yu81oy1134g7o/branch/master?svg=true)](https://ci.appveyor.com/project/idrislang/idris-dev)

55[![Documentation Status](https://readthedocs.org/projects/idris/badge/?version=latest)](https://readthedocs.org/projects/idris/?badge=latest)

66[![Hackage](https://img.shields.io/hackage/v/idris.svg)](https://hackage.haskell.org/package/idris)

7−[![Stackage LTS](http://stackage.org/package/idris/badge/lts)](http://stackage.org/lts/package/idris)

8−[![Stackage Nightly](http://stackage.org/package/idris/badge/nightly)](http://stackage.org/nightly/package/idris)

7+[![Stackage LTS](https://stackage.org/package/idris/badge/lts)](https://stackage.org/lts/package/idris)

8+[![Stackage Nightly](https://stackage.org/package/idris/badge/nightly)](https://stackage.org/nightly/package/idris)

99[![IRC](https://img.shields.io/badge/IRC-%23idris-1e72ff.svg?style=flat)](https://www.irccloud.com/invite?channel=%23idris&hostname=irc.freenode.net&port=6697&ssl=1)

1010

11−Idris (http://idris-lang.org/) is a general-purpose functional programming

11+Idris (https://idris-lang.org/) is a general-purpose functional programming

1212language with dependent types.

1313

1414## Installation Guides.

@@ -28,7 +28,7 @@ Idris has support for external code generators. Supplied with the distribution

2828is a C code generator to compile executables, and a JavaScript code generator

2929with support for node.js and browser JavaScript.

3030

31−More information about [code generators can be found on the wiki](http://idris.readthedocs.io/en/latest/reference/codegen.html).

31+More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html).

3232

3333## More Information

3434

appveyor.yml+1−1

@@ -5,7 +5,7 @@ init:

66 mkdir C:\ghc

8− Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

8+ Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

1010 7z x C:\ghc\ghc.tar.xz -oC:\ghc

1111

azure-pipelines.yml+1−1

@@ -68,7 +68,7 @@ jobs:

6868 choco install 7zip.portable -y --no-progress

6969 choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"

7070 mkdir C:\ghc

71− Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

71+ Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"

7272 7z x C:\ghc\ghc.tar.xz -oC:\ghc

7373 7z x C:\ghc\ghc.tar -oC:\ghc

7474 displayName: "Setting up environment"

benchmarks/pidigits/pidigits.idr+1−1

@@ -3,7 +3,7 @@ import Data.Vect

44{- Toy program that outputs the n first digits of Pi.

6− Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.

6+ Inspired from https://www.haskell.org/haskellwiki/Shootout/Pidigits.

77 The original ns and str lazy lists have been replaced by strict functions.

99 Memory usage seems to be excessive. One of the branches of str is tail recursive, and

docs/LICENSE+1−1

@@ -7,4 +7,4 @@ rights to Documentation for Idris.

88More information concerning the CC0 can be found online at:

10− http://creativecommons.org/publicdomain/zero/1.0/

10+ https://creativecommons.org/publicdomain/zero/1.0/

docs/Makefile+1−1

@@ -9,7 +9,7 @@ BUILDDIR = _build

1010# User-friendly check for sphinx-build

1111ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)

12−$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from http://sphinx-doc.org/)

12+$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)

1313endif

1414

1515# Internal variables.

docs/README.md+3−3

@@ -1,7 +1,7 @@

11# Documentation for the Idris Language.

4−This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](http://sphinx-doc.org) for future inclusion on [Read The Docs](http://www.readthedocs.org).

4+This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://www.readthedocs.org).

66## Dependencies

@@ -12,7 +12,7 @@ To build the manual the following dependencies must be met. We assume that you h

1212Python should be installed by default on most systems.

1313Sphinx can be installed either through your hosts package manager or using pip/easy_install.

1414

15−*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx

15+*Note* [ReadTheDocs](https://www.readthedocs.org) works with Sphinx

1616 `v1.2.2`. If you install a more recent version of sphinx then

1717 'incorrectly' marked up documentation may get passed the build system

1818 of readthedocs and be ignored. In the past we had several code-blocks

@@ -45,7 +45,7 @@ rights to Documentation for Idris.

4545

4646More information concerning the CC0 can be found online at:

4747

48− http://creativecommons.org/publicdomain/zero/1.0/

48+ https://creativecommons.org/publicdomain/zero/1.0/

4949

5050

5151When contributing material to the manual please bear in mind that the work will be licensed as above.

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/effects/conclusions.rst+1−1

@@ -51,7 +51,7 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.

5151 Programming Languages and Systems (APLAS '09), Zhenjiang Hu

5252 (Ed.). Springer-Verlag, Berlin, Heidelberg,

5353 95-110. DOI=10.1007/978-3-642-10672-9_9

54− http://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9

54+ https://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9

5555

5656

5757.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in

docs/effects/index.rst+1−1

@@ -25,7 +25,7 @@ A tutorial on the `Effects` package in `Idris`.

2525 Idris Community* has waived all copyright and related or neighbouring

2626 rights to Documentation for Idris.

2727

28− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

28+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

2929

3030.. toctree::

3131 :maxdepth: 1

docs/effects/introduction.rst+1−1

@@ -3,7 +3,7 @@ Introduction

33************

55Pure functional languages with dependent types such as `Idris

6−<http://www.idris-lang.org/>`_ support reasoning about programs directly

6+<https://www.idris-lang.org/>`_ support reasoning about programs directly

77in the type system, promising that we can *know* a program will run

88correctly (i.e. according to the specification in its type) simply

99because it compiles. Realistically, though, things are not so simple:

docs/proofs/elabReflection.rst → docs/elaboratorReflection/elabReflection.rstrenamed

The content is the same.

docs/reference/elaborator-reflection.rst → docs/elaboratorReflection/elaborator-reflection.rstrenamed+11−5

@@ -1,8 +1,8 @@

11.. _elaborator-reflection:

3−*********************

4−Elaborator Reflection

5−*********************

3+**********************************

4+Elaborator Reflection Introduction

5+**********************************

77The Idris elaborator is responsible for converting high-level Idris code into the core language.

88It is implemented as a kind of embedded tactic language in Haskell, where tactic scripts are written in an *elaboration monad* that provides error handling and a proof state.

@@ -198,6 +198,12 @@ This is primarily useful for code generation, particularly for generating patter

198198

199199Learn More

200200==========

201−While this documentation is still incomplete, elaboration reflection works in Idris today.

202−As you wait for the completion of the documentation, the list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.

201+

202+Some tactics are introduced in the :ref:`proofs-index` section with further details, of those most relevant to elaborator reflection, on the following pages.

203+

204+The list of built-in tactics can be obtained using the ``:browse`` command in an Idris REPL or the corresponding feature in one of the graphical IDE clients to explore the ``Language.Reflection.Elab.Tactics`` namespace.

203205All of the built-in tactics contain documentation strings.

206+

207+For alternative ways to extend the Idris language see the :ref:`reference-index` section.

208+

209+The following pages explain more about the theory and practice of elaborator reflection.

docs/proofs/example1.rst → docs/elaboratorReflection/example1.rstrenamed

The content is the same.

docs/proofs/generatingData.rst → docs/elaboratorReflection/generatingData.rstrenamed

The content is the same.

docs/proofs/holes.rst → docs/elaboratorReflection/holes.rstrenamed

The content is the same.

docs/elaboratorReflection/index.rstnew file+27

@@ -0,0 +1,27 @@

1+.. _elaborator-index:

3+#####################

4+Elaborator Reflection

5+#####################

7+A tutorial on theorem proving in Idris.

9+.. note::

10+

11+ The documentation for Idris has been published under the Creative

12+ Commons CC0 License. As such to the extent possible under law, *The

13+ Idris Community* has waived all copyright and related or neighboring

14+ rights to Documentation for Idris.

15+

16+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

17+

18+.. toctree::

19+ :maxdepth: 1

20+

21+ elaborator-reflection

22+ elabReflection

23+ tactics

24+ holes

25+ example1

26+ primitive

27+ generatingData

docs/proofs/primitive.rst → docs/elaboratorReflection/primitive.rstrenamed

The content is the same.

docs/proofs/tactics.rst → docs/elaboratorReflection/tactics.rstrenamed

The content is the same.

docs/faq/faq.rst+2−2

@@ -37,7 +37,7 @@ Is there some documentation for the standard lib? List of functions?

3737=====================================================================

3838

3939API documentation for the shipped packages is listed on `the

40−documentation page <http://www.idris-lang.org/documentation/>`_.

40+documentation page <https://www.idris-lang.org/documentation/>`_.

4141

4242Unfortunately, the default prelude and shipped packages for `Idris`

4343are not necessarily complete with regards to documentation. Other

@@ -310,7 +310,7 @@ better and it will make sense to revisit this. For now, however, Idris will not

310310be offering arbitrary Unicode symbols in operators.

311311

312312This seems like an instance of `Wadler's

313−Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.

313+Law <https://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.

314314

315315This answer is based on Edwin Brady's response in the following

316316`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.

docs/guides/index.rst+1−1

@@ -12,7 +12,7 @@ Tutorials submitted by community members.

1212 Idris Community* has waived all copyright and related or neighboring

1313 rights to Documentation for Idris.

1414

15− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

15+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1616

1717

1818.. toctree::

docs/guides/theorem-prover.rst+1−1

@@ -22,7 +22,7 @@ We will be given the following prompt, in future releases the version string wil

2222 ____ __ _

2323 / _/___/ /____(_)____

2424 / // __ / ___/ / ___/ Version 0.9.18.1

25− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

25+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

2626 /___/\__,_/_/ /_/____/ Type :? for help

2727

2828 Idris is free software with ABSOLUTELY NO WARRANTY.

docs/guides/type-providers-ffi.rst+1−1

@@ -3,7 +3,7 @@ Type Providers in Idris

33***********************

55`Type providers in Idris

6−<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__

6+<https://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__

77are simple enough, but there are a few caveats to using them that it

88would be worthwhile to go through the basic steps. We also go over

99foreign functions, because these will often be used with type

docs/image/parserModules.pngnew file

Binary file not shown.

docs/image/parserModules.svgnew file+1251

@@ -0,0 +1,1251 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

4+<svg

5+ xmlns:dc="http://purl.org/dc/elements/1.1/"

6+ xmlns:cc="http://creativecommons.org/ns#"

7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

8+ xmlns:svg="http://www.w3.org/2000/svg"

9+ xmlns="http://www.w3.org/2000/svg"

10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"

11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"

12+ width="210mm"

13+ height="297mm"

14+ viewBox="0 0 210 297"

15+ version="1.1"

16+ id="svg8"

17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"

18+ sodipodi:docname="parserModules.svg">

19+ <defs

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>

139+ <marker

140+ inkscape:isstock="true"

141+ style="overflow:visible;"

142+ id="marker1000"

143+ refX="0.0"

144+ refY="0.0"

145+ orient="auto"

146+ inkscape:stockid="Arrow1Mend">

147+ <path

148+ transform="scale(0.4) rotate(180) translate(10,0)"

149+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

150+ 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 "

151+ id="path998" />

152+ </marker>

153+ <marker

154+ inkscape:isstock="true"

155+ style="overflow:visible;"

156+ id="marker1127"

157+ refX="0.0"

158+ refY="0.0"

159+ orient="auto"

160+ inkscape:stockid="Arrow1Mend">

161+ <path

162+ transform="scale(0.4) rotate(180) translate(10,0)"

163+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

164+ 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 "

165+ id="path1125" />

166+ </marker>

167+ <marker

168+ inkscape:isstock="true"

169+ style="overflow:visible;"

170+ id="marker1123"

171+ refX="0.0"

172+ refY="0.0"

173+ orient="auto"

174+ inkscape:stockid="Arrow1Mend">

175+ <path

176+ transform="scale(0.4) rotate(180) translate(10,0)"

177+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"

178+ 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 "

179+ id="path1121" />

180+ </marker>

181+ <marker

182+ inkscape:isstock="true"

183+ style="overflow:visible;"

184+ id="marker1117"

185+ refX="0.0"

186+ refY="0.0"

187+ orient="auto"

188+ inkscape:stockid="Arrow1Mend">

189+ <path

190+ transform="scale(0.4) rotate(180) translate(10,0)"

191+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"

192+ 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 "

193+ id="path1115" />

194+ </marker>

195+ <marker

196+ inkscape:stockid="Arrow1Mend"

197+ orient="auto"

198+ refY="0.0"

199+ refX="0.0"

200+ id="marker1111"

201+ style="overflow:visible;"

202+ inkscape:isstock="true"

203+ inkscape:collect="always">

204+ <path

205+ id="path1109"

206+ 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 "

207+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"

208+ transform="scale(0.4) rotate(180) translate(10,0)" />

209+ </marker>

210+ <marker

211+ inkscape:isstock="true"

212+ style="overflow:visible;"

213+ id="marker1105"

214+ refX="0.0"

215+ refY="0.0"

216+ orient="auto"

217+ inkscape:stockid="Arrow1Mend"

218+ inkscape:collect="always">

219+ <path

220+ transform="scale(0.4) rotate(180) translate(10,0)"

221+ style="fill-rule:evenodd;stroke:#00aa3f;stroke-width:1pt;stroke-opacity:1;fill:#00aa3f;fill-opacity:1"

222+ 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 "

223+ id="path1103" />

224+ </marker>

225+ <marker

226+ inkscape:isstock="true"

227+ style="overflow:visible;"

228+ id="marker1057"

229+ refX="0.0"

230+ refY="0.0"

231+ orient="auto"

232+ inkscape:stockid="Arrow1Mend">

233+ <path

234+ transform="scale(0.4) rotate(180) translate(10,0)"

235+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

236+ 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 "

237+ id="path1055" />

238+ </marker>

239+ <marker

240+ inkscape:stockid="Arrow1Mend"

241+ orient="auto"

242+ refY="0.0"

243+ refX="0.0"

244+ id="marker1045"

245+ style="overflow:visible;"

246+ inkscape:isstock="true"

247+ inkscape:collect="always">

248+ <path

249+ id="path1043"

250+ 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 "

251+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

252+ transform="scale(0.4) rotate(180) translate(10,0)" />

253+ </marker>

254+ <marker

255+ inkscape:stockid="Arrow1Mend"

256+ orient="auto"

257+ refY="0.0"

258+ refX="0.0"

259+ id="marker1033"

260+ style="overflow:visible;"

261+ inkscape:isstock="true">

262+ <path

263+ id="path1031"

264+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

265+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

266+ transform="scale(0.4) rotate(180) translate(10,0)" />

267+ </marker>

268+ <marker

269+ inkscape:stockid="Arrow1Mend"

270+ orient="auto"

271+ refY="0.0"

272+ refX="0.0"

273+ id="marker1027"

274+ style="overflow:visible;"

275+ inkscape:isstock="true">

276+ <path

277+ id="path1025"

278+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

279+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

280+ transform="scale(0.4) rotate(180) translate(10,0)" />

281+ </marker>

282+ <marker

283+ inkscape:isstock="true"

284+ style="overflow:visible;"

285+ id="marker1015"

286+ refX="0.0"

287+ refY="0.0"

288+ orient="auto"

289+ inkscape:stockid="Arrow1Mend"

290+ inkscape:collect="always">

291+ <path

292+ transform="scale(0.4) rotate(180) translate(10,0)"

293+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

294+ 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 "

295+ id="path1013" />

296+ </marker>

297+ <marker

298+ inkscape:isstock="true"

299+ style="overflow:visible;"

300+ id="marker1009"

301+ refX="0.0"

302+ refY="0.0"

303+ orient="auto"

304+ inkscape:stockid="Arrow1Mend">

305+ <path

306+ transform="scale(0.4) rotate(180) translate(10,0)"

307+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

308+ 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 "

309+ id="path1007" />

310+ </marker>

311+ <marker

312+ inkscape:isstock="true"

313+ style="overflow:visible;"

314+ id="marker1003"

315+ refX="0.0"

316+ refY="0.0"

317+ orient="auto"

318+ inkscape:stockid="Arrow1Mend">

319+ <path

320+ transform="scale(0.4) rotate(180) translate(10,0)"

321+ style="fill-rule:evenodd;stroke:#ff0000;stroke-width:1pt;stroke-opacity:1;fill:#ff0000;fill-opacity:1"

322+ 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 "

323+ id="path1001" />

324+ </marker>

325+ <marker

326+ inkscape:stockid="Arrow1Mend"

327+ orient="auto"

328+ refY="0.0"

329+ refX="0.0"

330+ id="marker997"

331+ style="overflow:visible;"

332+ inkscape:isstock="true"

333+ inkscape:collect="always">

334+ <path

335+ id="path995"

336+ 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 "

337+ style="fill-rule:evenodd;stroke:#ff0000;stroke-width:1pt;stroke-opacity:1;fill:#ff0000;fill-opacity:1"

338+ transform="scale(0.4) rotate(180) translate(10,0)" />

339+ </marker>

340+ <marker

341+ inkscape:isstock="true"

342+ style="overflow:visible;"

343+ id="marker991"

344+ refX="0.0"

345+ refY="0.0"

346+ orient="auto"

347+ inkscape:stockid="Arrow1Mend"

348+ inkscape:collect="always">

349+ <path

350+ transform="scale(0.4) rotate(180) translate(10,0)"

351+ style="fill-rule:evenodd;stroke:#ff0000;stroke-width:1pt;stroke-opacity:1;fill:#ff0000;fill-opacity:1"

352+ 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 "

353+ id="path989" />

354+ </marker>

355+ <marker

356+ inkscape:stockid="Arrow1Mend"

357+ orient="auto"

358+ refY="0.0"

359+ refX="0.0"

360+ id="marker967"

361+ style="overflow:visible;"

362+ inkscape:isstock="true"

363+ inkscape:collect="always">

364+ <path

365+ id="path965"

366+ 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 "

367+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

368+ transform="scale(0.4) rotate(180) translate(10,0)" />

369+ </marker>

370+ <marker

371+ inkscape:isstock="true"

372+ style="overflow:visible;"

373+ id="marker961"

374+ refX="0.0"

375+ refY="0.0"

376+ orient="auto"

377+ inkscape:stockid="Arrow1Mend"

378+ inkscape:collect="always">

379+ <path

380+ transform="scale(0.4) rotate(180) translate(10,0)"

381+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

382+ 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 "

383+ id="path959" />

384+ </marker>

385+ <marker

386+ inkscape:isstock="true"

387+ style="overflow:visible;"

388+ id="marker3617"

389+ refX="0.0"

390+ refY="0.0"

391+ orient="auto"

392+ inkscape:stockid="Arrow1Mend">

393+ <path

394+ transform="scale(0.4) rotate(180) translate(10,0)"

395+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

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 "

397+ id="path3615" />

398+ </marker>

399+ <marker

400+ inkscape:stockid="Arrow1Mend"

401+ orient="auto"

402+ refY="0.0"

403+ refX="0.0"

404+ id="marker2049"

405+ style="overflow:visible;"

406+ inkscape:isstock="true"

407+ inkscape:collect="always">

408+ <path

409+ id="path2047"

410+ 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 "

411+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

412+ transform="scale(0.4) rotate(180) translate(10,0)" />

413+ </marker>

414+ <marker

415+ inkscape:isstock="true"

416+ style="overflow:visible;"

417+ id="marker1539"

418+ refX="0.0"

419+ refY="0.0"

420+ orient="auto"

421+ inkscape:stockid="Arrow1Mend"

422+ inkscape:collect="always">

423+ <path

424+ transform="scale(0.4) rotate(180) translate(10,0)"

425+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

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 "

427+ id="path1537" />

428+ </marker>

429+ </defs>

430+ <sodipodi:namedview

431+ id="base"

432+ pagecolor="#ffffff"

433+ bordercolor="#666666"

434+ borderopacity="1.0"

435+ inkscape:pageopacity="0.0"

436+ inkscape:pageshadow="2"

437+ inkscape:zoom="1"

438+ inkscape:cx="368.33949"

439+ inkscape:cy="547.05121"

440+ inkscape:document-units="mm"

441+ inkscape:current-layer="layer1"

442+ showgrid="false"

443+ inkscape:window-width="1800"

444+ inkscape:window-height="1011"

445+ inkscape:window-x="86"

446+ inkscape:window-y="0"

447+ inkscape:window-maximized="0"

448+ inkscape:snap-nodes="false" />

449+ <metadata

450+ id="metadata5">

451+ <rdf:RDF>

452+ <cc:Work

453+ rdf:about="">

454+ <dc:format>image/svg+xml</dc:format>

455+ <dc:type

456+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

457+ <dc:title />

458+ </cc:Work>

459+ </rdf:RDF>

460+ </metadata>

461+ <g

462+ inkscape:label="Layer 1"

463+ inkscape:groupmode="layer"

464+ id="layer1">

465+ <text

466+ inkscape:export-ydpi="61.120499"

467+ inkscape:export-xdpi="61.120499"

468+ id="text854"

469+ y="119.72919"

470+ x="131.23334"

471+ 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"

472+ xml:space="preserve"><tspan

473+ 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"

474+ y="129.46077"

475+ x="131.23334"

476+ id="tspan852"

477+ sodipodi:role="line" /></text>

478+ <rect

479+ inkscape:export-ydpi="61.120499"

480+ inkscape:export-xdpi="61.120499"

481+ 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"

482+ id="rect875"

483+ width="43.656246"

484+ height="18.520832"

485+ x="92.339577"

486+ y="110.20418" />

487+ <path

488+ inkscape:export-ydpi="61.120499"

489+ inkscape:export-xdpi="61.120499"

490+ inkscape:connector-curvature="0"

491+ id="path881"

492+ d="m 135.73129,118.93554 16.66875,-0.26459"

493+ 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)" />

494+ <text

495+ inkscape:export-ydpi="61.120499"

496+ inkscape:export-xdpi="61.120499"

497+ id="text895"

498+ y="115.76046"

499+ x="138.37698"

500+ 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"

501+ xml:space="preserve"><tspan

502+ 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"

503+ y="115.76046"

504+ x="138.37698"

505+ id="tspan893"

506+ sodipodi:role="line">PTerm</tspan></text>

507+ <text

508+ inkscape:export-ydpi="61.120499"

509+ inkscape:export-xdpi="61.120499"

510+ id="text903"

511+ y="115.23129"

512+ x="93.927078"

513+ 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"

514+ xml:space="preserve"><tspan

515+ 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"

516+ y="115.23129"

517+ x="93.927078"

518+ id="tspan901"

519+ sodipodi:role="line">module Idris.Parser</tspan><tspan

520+ 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"

521+ y="128.46045"

522+ x="93.927078"

523+ sodipodi:role="line"

524+ id="tspan1021" /></text>

525+ <rect

526+ 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"

527+ id="rect905"

528+ width="44.185421"

529+ height="18.785423"

530+ x="40.463421"

531+ y="141.50723"

532+ inkscape:export-xdpi="61.120499"

533+ inkscape:export-ydpi="61.120499" />

534+ <rect

535+ y="155.183"

536+ x="95.51458"

537+ height="18.256256"

538+ width="49.212498"

539+ id="rect907"

540+ 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"

541+ inkscape:export-xdpi="61.120499"

542+ inkscape:export-ydpi="61.120499" />

543+ <path

544+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker961)"

545+ d="m 84.648837,152.88468 9.013662,7.32603"

546+ id="path909"

547+ inkscape:connector-curvature="0"

548+ inkscape:export-xdpi="61.120499"

549+ inkscape:export-ydpi="61.120499"

550+ sodipodi:nodetypes="cc" />

551+ <path

552+ inkscape:connector-curvature="0"

553+ id="path911"

554+ d="m 22.471756,152.09108 16.66875,-0.26459"

555+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1539)"

556+ inkscape:export-xdpi="61.120499"

557+ inkscape:export-ydpi="61.120499" />

558+ <text

559+ xml:space="preserve"

560+ 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"

561+ x="24.059256"

562+ y="148.91547"

563+ id="text917"

564+ inkscape:export-xdpi="61.120499"

565+ inkscape:export-ydpi="61.120499"><tspan

566+ sodipodi:role="line"

567+ id="tspan915"

568+ x="24.059256"

569+ y="148.91547"

570+ 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>

571+ <text

572+ id="text923"

573+ y="137.72075"

574+ x="65.087494"

575+ 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"

576+ xml:space="preserve"

577+ inkscape:export-xdpi="61.120499"

578+ inkscape:export-ydpi="61.120499"><tspan

579+ 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"

580+ y="137.72075"

581+ x="65.087494"

582+ sodipodi:role="line"

583+ id="tspan921">List (TokenData Token)</tspan></text>

584+ <text

585+ id="text931"

586+ y="218.41846"

587+ x="36.512497"

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:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

589+ xml:space="preserve"

590+ inkscape:export-xdpi="61.120499"

591+ inkscape:export-ydpi="61.120499"><tspan

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:#ff0000;stroke-width:0.26458332;"

593+ y="218.41846"

594+ x="36.512497"

595+ id="tspan929"

596+ sodipodi:role="line">module Text.Lexer</tspan></text>

597+ <text

598+ xml:space="preserve"

599+ 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"

600+ x="98.160408"

601+ y="161.00386"

602+ id="text935"

603+ inkscape:export-xdpi="61.120499"

604+ inkscape:export-ydpi="61.120499"><tspan

605+ sodipodi:role="line"

606+ id="tspan933"

607+ x="98.160408"

608+ y="161.00386"

609+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">module Parser.Support</tspan></text>

610+ <rect

611+ inkscape:export-ydpi="61.120499"

612+ inkscape:export-xdpi="61.120499"

613+ y="214.18488"

614+ x="32.01458"

615+ height="6.3500061"

616+ width="43.656254"

617+ id="rect937"

618+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

619+ <rect

620+ inkscape:export-ydpi="61.120499"

621+ inkscape:export-xdpi="61.120499"

622+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

623+ id="rect939"

624+ width="42.862495"

625+ height="6.8791728"

626+ x="94.985413"

627+ y="214.18488" />

628+ <text

629+ inkscape:export-ydpi="61.120499"

630+ inkscape:export-xdpi="61.120499"

631+ xml:space="preserve"

632+ 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"

633+ x="42.31551"

634+ y="147.59224"

635+ id="text951"><tspan

636+ sodipodi:role="line"

637+ id="tspan949"

638+ x="42.31551"

639+ y="147.59224"

640+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">module Parser.Lexer</tspan></text>

641+ <path

642+ sodipodi:nodetypes="cc"

643+ inkscape:export-ydpi="61.120499"

644+ inkscape:export-xdpi="61.120499"

645+ inkscape:connector-curvature="0"

646+ id="path963"

647+ d="m 53.299561,213.22831 1.53604,-51.85834"

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)" />

649+ <text

650+ inkscape:export-ydpi="61.120499"

651+ inkscape:export-xdpi="61.120499"

652+ xml:space="preserve"

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:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

654+ x="23.220526"

655+ y="251.01649"

656+ id="text971"><tspan

657+ sodipodi:role="line"

658+ id="tspan969"

659+ x="23.220526"

660+ y="251.01649"

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:#ff0000;stroke-width:0.26458332;">module Text.Lexer.Core</tspan></text>

662+ <rect

663+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

664+ id="rect973"

665+ width="47.889587"

666+ height="6.3500061"

667+ x="21.633026"

668+ y="246.51833"

669+ inkscape:export-xdpi="61.120499"

670+ inkscape:export-ydpi="61.120499" />

671+ <path

672+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker991)"

673+ d="m 48.369316,228.83873 0.04943,-6.71548"

674+ id="path975"

675+ inkscape:connector-curvature="0"

676+ inkscape:export-xdpi="61.120499"

677+ inkscape:export-ydpi="61.120499"

678+ sodipodi:nodetypes="cc" />

679+ <text

680+ id="text979"

681+ y="241.96643"

682+ x="23.283329"

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:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

684+ xml:space="preserve"

685+ inkscape:export-xdpi="61.120499"

686+ inkscape:export-ydpi="61.120499"><tspan

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:#ff0000;stroke-width:0.26458332;"

688+ y="241.96643"

689+ x="23.283329"

690+ id="tspan977"

691+ sodipodi:role="line">module Text.Quantity</tspan></text>

692+ <rect

693+ inkscape:export-ydpi="61.120499"

694+ inkscape:export-xdpi="61.120499"

695+ y="237.46826"

696+ x="21.695829"

697+ height="6.2469702"

698+ width="43.853985"

699+ id="rect981"

700+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

701+ <text

702+ inkscape:export-ydpi="61.120499"

703+ inkscape:export-xdpi="61.120499"

704+ xml:space="preserve"

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:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

706+ x="23.18244"

707+ y="233.68523"

708+ id="text985"><tspan

709+ sodipodi:role="line"

710+ id="tspan983"

711+ x="23.18244"

712+ y="233.68523"

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:#ff0000;stroke-width:0.26458332;">module Text.Token</tspan></text>

714+ <rect

715+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

716+ id="rect987"

717+ width="39.011257"

718+ height="5.9464455"

719+ x="21.59494"

720+ y="229.18706"

721+ inkscape:export-xdpi="61.120499"

722+ inkscape:export-ydpi="61.120499" />

723+ <path

724+ sodipodi:nodetypes="cc"

725+ inkscape:export-ydpi="61.120499"

726+ inkscape:export-xdpi="61.120499"

727+ inkscape:connector-curvature="0"

728+ id="path993"

729+ d="M 62.998384,237.01083 62.846037,221.92147"

730+ style="fill:#ff0000;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker997)" />

731+ <path

732+ style="fill:#ff0000;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1003)"

733+ d="M 67.336659,246.29272 67.083422,221.71969"

734+ id="path999"

735+ inkscape:connector-curvature="0"

736+ inkscape:export-xdpi="61.120499"

737+ inkscape:export-ydpi="61.120499"

738+ sodipodi:nodetypes="cc" />

739+ <path

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)"

741+ d="M 73.937074,214.02206 94.72083,169.47102"

742+ id="path1005"

743+ inkscape:connector-curvature="0"

744+ inkscape:export-xdpi="61.120499"

745+ inkscape:export-ydpi="61.120499"

746+ sodipodi:nodetypes="cc" />

747+ <path

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)"

749+ d="M 108.0684,213.75748 108.0169,173.5408"

750+ id="path1011"

751+ inkscape:connector-curvature="0"

752+ inkscape:export-xdpi="61.120499"

753+ inkscape:export-ydpi="61.120499"

754+ sodipodi:nodetypes="cc" />

755+ <text

756+ inkscape:export-ydpi="61.120499"

757+ inkscape:export-xdpi="61.120499"

758+ id="text1019"

759+ y="218.94762"

760+ x="96.837494"

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:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

762+ xml:space="preserve"><tspan

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:#ff0000;stroke-width:0.26458332;"

764+ y="218.94762"

765+ x="96.837494"

766+ id="tspan1017"

767+ sodipodi:role="line">module Text.Parser</tspan></text>

768+ <path

769+ sodipodi:nodetypes="cc"

770+ inkscape:export-ydpi="61.120499"

771+ inkscape:export-xdpi="61.120499"

772+ inkscape:connector-curvature="0"

773+ id="path1023"

774+ d="m 113.62466,154.75539 0.0397,-25.06978"

775+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1027)" />

776+ <path

777+ sodipodi:nodetypes="cc"

778+ inkscape:export-ydpi="61.120499"

779+ inkscape:export-xdpi="61.120499"

780+ inkscape:connector-curvature="0"

781+ id="path1029"

782+ d="M 83.757032,147.15485 97.991855,129.77582"

783+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1033)" />

784+ <rect

785+ y="142.91107"

786+ x="118.15033"

787+ height="6.6968417"

788+ width="45.2328"

789+ id="rect1035"

790+ 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"

791+ inkscape:export-xdpi="61.120499"

792+ inkscape:export-ydpi="61.120499" />

793+ <path

794+ sodipodi:nodetypes="cc"

795+ inkscape:export-ydpi="61.120499"

796+ inkscape:export-xdpi="61.120499"

797+ inkscape:connector-curvature="0"

798+ id="path1037"

799+ d="m 121.83513,142.5835 -0.0515,-12.72267"

800+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1057)" />

801+ <text

802+ xml:space="preserve"

803+ 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"

804+ x="120.00241"

805+ y="147.67372"

806+ id="text1041"

807+ inkscape:export-xdpi="61.120499"

808+ inkscape:export-ydpi="61.120499"><tspan

809+ sodipodi:role="line"

810+ id="tspan1039"

811+ x="120.00241"

812+ y="147.67372"

813+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">module TTImp.TTImp</tspan></text>

814+ <rect

815+ inkscape:export-ydpi="61.120499"

816+ inkscape:export-xdpi="61.120499"

817+ 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"

818+ id="rect1047"

819+ width="42.862495"

820+ height="6.8791728"

821+ x="125.28364"

822+ y="133.0603" />

823+ <path

824+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1045)"

825+ d="m 145.18016,132.82376 -9.18434,-4.09859"

826+ id="path1049"

827+ inkscape:connector-curvature="0"

828+ inkscape:export-xdpi="61.120499"

829+ inkscape:export-ydpi="61.120499"

830+ sodipodi:nodetypes="cc" />

831+ <text

832+ inkscape:export-ydpi="61.120499"

833+ inkscape:export-xdpi="61.120499"

834+ id="text1053"

835+ y="137.82295"

836+ x="127.13572"

837+ 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"

838+ xml:space="preserve"><tspan

839+ 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"

840+ y="137.82295"

841+ x="127.13572"

842+ id="tspan1051"

843+ sodipodi:role="line">module Idris.Syntax</tspan></text>

844+ <rect

845+ inkscape:export-ydpi="61.120499"

846+ inkscape:export-xdpi="61.120499"

847+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#00871c;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

848+ id="rect1061"

849+ width="59.266659"

850+ height="16.13958"

851+ x="97.102074"

852+ y="186.93335" />

853+ <path

854+ inkscape:export-ydpi="61.120499"

855+ inkscape:export-xdpi="61.120499"

856+ inkscape:connector-curvature="0"

857+ id="path1063"

858+ d="m 76.993749,160.21044 18.785417,28.83958"

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)"

860+ sodipodi:nodetypes="cc" />

861+ <text

862+ inkscape:export-ydpi="61.120499"

863+ inkscape:export-xdpi="61.120499"

864+ id="text1081"

865+ y="192.48962"

866+ x="157.95586"

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"

868+ xml:space="preserve"><tspan

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"

870+ y="192.48962"

871+ x="157.95586"

872+ id="tspan1079"

873+ sodipodi:role="line">SExp</tspan></text>

874+ <text

875+ inkscape:export-ydpi="61.120499"

876+ inkscape:export-xdpi="61.120499"

877+ id="text1089"

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"

881+ xml:space="preserve"><tspan

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"

885+ id="tspan1087"

886+ sodipodi:role="line">module Idris.IDEMode.Parser</tspan></text>

887+ <rect

888+ inkscape:export-ydpi="61.120499"

889+ inkscape:export-xdpi="61.120499"

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"

891+ id="rect1097"

892+ width="55.033333"

893+ height="14.287498"

894+ x="20.637447"

895+ y="52.524986" />

896+ <text

897+ inkscape:export-ydpi="61.120499"

898+ inkscape:export-xdpi="61.120499"

899+ id="text1101"

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;"

903+ xml:space="preserve"><tspan

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"

907+ id="tspan1099"

908+ sodipodi:role="line">module Idris.REPL</tspan></text>

909+ <path

910+ sodipodi:nodetypes="cc"

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)"

912+ d="m 112.97708,174.23335 0,14.02292"

913+ id="path1107"

914+ inkscape:connector-curvature="0"

915+ inkscape:export-xdpi="61.120499"

916+ inkscape:export-ydpi="61.120499" />

917+ <path

918+ inkscape:export-ydpi="61.120499"

919+ inkscape:export-xdpi="61.120499"

920+ inkscape:connector-curvature="0"

921+ id="path1113"

922+ d="m 148.43125,150.15592 0.26458,35.71911"

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)"

924+ sodipodi:nodetypes="cc" />

925+ <path

926+ inkscape:export-ydpi="61.120499"

927+ inkscape:export-xdpi="61.120499"

928+ inkscape:connector-curvature="0"

929+ id="path1119"

930+ d="m 156.56889,195.56696 13.16435,-0.41532"

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)"

932+ sodipodi:nodetypes="cc" />

933+ <text

934+ id="text950"

935+ y="104.70191"

936+ x="22.426785"

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"

938+ xml:space="preserve"

939+ inkscape:export-xdpi="61.120499"

940+ inkscape:export-ydpi="61.120499"><tspan

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"

942+ y="104.70191"

943+ x="22.426785"

944+ id="tspan948"

945+ sodipodi:role="line">module Core.Core</tspan></text>

946+ <rect

947+ inkscape:export-ydpi="61.120499"

948+ inkscape:export-xdpi="61.120499"

949+ y="100.20374"

950+ x="20.839275"

951+ height="9.7895899"

952+ width="47.889587"

953+ id="rect952"

954+ 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" />

955+ <text

956+ inkscape:export-ydpi="61.120499"

957+ inkscape:export-xdpi="61.120499"

958+ xml:space="preserve"

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"

960+ x="22.955944"

961+ y="108.40608"

962+ id="text956"><tspan

963+ sodipodi:role="line"

964+ id="tspan954"

965+ x="22.955944"

966+ y="108.40608"

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>

968+ <text

969+ inkscape:export-ydpi="61.120499"

970+ inkscape:export-xdpi="61.120499"

971+ xml:space="preserve"

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"

973+ x="79.312202"

974+ y="92.266502"

975+ id="text960"><tspan

976+ sodipodi:role="line"

977+ id="tspan958"

978+ x="79.312202"

979+ y="92.266502"

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>

981+ <rect

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"

983+ id="rect962"

984+ width="61.912495"

985+ height="18.785419"

986+ x="77.724693"

987+ y="87.768333"

988+ inkscape:export-xdpi="61.120499"

989+ inkscape:export-ydpi="61.120499" />

990+ <text

991+ id="text966"

992+ y="95.970665"

993+ x="79.841362"

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"

995+ xml:space="preserve"

996+ inkscape:export-xdpi="61.120499"

997+ inkscape:export-ydpi="61.120499"><tspan

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"

999+ y="95.970665"

1000+ x="79.841362"

1001+ sodipodi:role="line"

1002+ id="tspan968">Representation of expressions ready</tspan><tspan

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"

1004+ y="100.38039"

1005+ x="79.841362"

1006+ sodipodi:role="line"

1007+ id="tspan974">for compiling: CExp</tspan><tspan

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"

1009+ y="104.79011"

1010+ x="79.841362"

1011+ sodipodi:role="line"

1012+ id="tspan972">Type erased, explicit case trees</tspan></text>

1013+ <text

1014+ inkscape:export-ydpi="61.120499"

1015+ inkscape:export-xdpi="61.120499"

1016+ xml:space="preserve"

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"

1018+ x="22.162193"

1019+ y="73.217979"

1020+ id="text978"><tspan

1021+ sodipodi:role="line"

1022+ id="tspan976"

1023+ x="22.162193"

1024+ y="73.217979"

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>

1026+ <rect

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"

1028+ id="rect980"

1029+ width="55.827087"

1030+ height="10.054173"

1031+ x="20.574694"

1032+ y="68.719742"

1033+ inkscape:export-xdpi="61.120499"

1034+ inkscape:export-ydpi="61.120499" />

1035+ <text

1036+ id="text984"

1037+ y="76.92215"

1038+ x="22.69136"

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"

1040+ xml:space="preserve"

1041+ inkscape:export-xdpi="61.120499"

1042+ inkscape:export-ydpi="61.120499"><tspan

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"

1044+ y="76.92215"

1045+ x="22.69136"

1046+ id="tspan982"

1047+ sodipodi:role="line">command line options</tspan></text>

1048+ <text

1049+ id="text988"

1050+ y="89.886726"

1051+ x="22.162193"

1052+ 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"

1053+ xml:space="preserve"

1054+ inkscape:export-xdpi="61.120499"

1055+ inkscape:export-ydpi="61.120499"><tspan

1056+ 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"

1057+ y="89.886726"

1058+ x="22.162193"

1059+ id="tspan986"

1060+ sodipodi:role="line">module Idris.Error</tspan></text>

1061+ <rect

1062+ inkscape:export-ydpi="61.120499"

1063+ inkscape:export-xdpi="61.120499"

1064+ y="85.388489"

1065+ x="20.574694"

1066+ height="9.5250101"

1067+ width="37.835419"

1068+ id="rect990"

1069+ 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" />

1070+ <text

1071+ inkscape:export-ydpi="61.120499"

1072+ inkscape:export-xdpi="61.120499"

1073+ xml:space="preserve"

1074+ 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"

1075+ x="22.69136"

1076+ y="93.590897"

1077+ id="text994"><tspan

1078+ sodipodi:role="line"

1079+ id="tspan992"

1080+ x="22.69136"

1081+ y="93.590897"

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>

1083+ <path

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)"

1085+ d="m 66.876776,99.410007 c -0.17822,-10.50534 -0.880145,-7.9985 -7.143748,-8.99444"

1086+ id="path996"

1087+ inkscape:connector-curvature="0"

1088+ inkscape:export-xdpi="61.120499"

1089+ inkscape:export-ydpi="61.120499"

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:#ff0000;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:#ff0000;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:#ff0000;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:#ff0000;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>

1250+ </g>

1251+</svg>

docs/image/parserTopLevel.pngnew file

Binary file not shown.

docs/image/parserTopLevel.svgnew file+294

@@ -0,0 +1,294 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

4+<svg

5+ xmlns:dc="http://purl.org/dc/elements/1.1/"

6+ xmlns:cc="http://creativecommons.org/ns#"

7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

8+ xmlns:svg="http://www.w3.org/2000/svg"

9+ xmlns="http://www.w3.org/2000/svg"

10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"

11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"

12+ width="210mm"

13+ height="297mm"

14+ viewBox="0 0 210 297"

15+ version="1.1"

16+ id="svg8"

17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"

18+ sodipodi:docname="topLevel.svg">

19+ <defs

20+ id="defs2">

21+ <marker

22+ inkscape:isstock="true"

23+ style="overflow:visible;"

24+ id="marker3617"

25+ refX="0.0"

26+ refY="0.0"

27+ orient="auto"

28+ inkscape:stockid="Arrow1Mend">

29+ <path

30+ transform="scale(0.4) rotate(180) translate(10,0)"

31+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

33+ id="path3615" />

34+ </marker>

35+ <marker

36+ inkscape:stockid="Arrow1Mend"

37+ orient="auto"

38+ refY="0.0"

39+ refX="0.0"

40+ id="marker2891"

41+ style="overflow:visible;"

42+ inkscape:isstock="true"

43+ inkscape:collect="always">

44+ <path

45+ id="path2889"

46+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

47+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

48+ transform="scale(0.4) rotate(180) translate(10,0)" />

49+ </marker>

50+ <marker

51+ inkscape:stockid="Arrow1Mend"

52+ orient="auto"

53+ refY="0.0"

54+ refX="0.0"

55+ id="marker2049"

56+ style="overflow:visible;"

57+ inkscape:isstock="true">

58+ <path

59+ id="path2047"

60+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

61+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

62+ transform="scale(0.4) rotate(180) translate(10,0)" />

63+ </marker>

64+ <marker

65+ inkscape:isstock="true"

66+ style="overflow:visible;"

67+ id="marker1539"

68+ refX="0.0"

69+ refY="0.0"

70+ orient="auto"

71+ inkscape:stockid="Arrow1Mend"

72+ inkscape:collect="always">

73+ <path

74+ transform="scale(0.4) rotate(180) translate(10,0)"

75+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

76+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

77+ id="path1537" />

78+ </marker>

79+ <marker

80+ inkscape:stockid="Arrow1Mend"

81+ orient="auto"

82+ refY="0.0"

83+ refX="0.0"

84+ id="Arrow1Mend"

85+ style="overflow:visible;"

86+ inkscape:isstock="true"

87+ inkscape:collect="always">

88+ <path

89+ id="path830"

90+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

91+ style="fill-rule:evenodd;stroke:#0000ff;stroke-width:1pt;stroke-opacity:1;fill:#0000ff;fill-opacity:1"

92+ transform="scale(0.4) rotate(180) translate(10,0)" />

93+ </marker>

94+ </defs>

95+ <sodipodi:namedview

96+ id="base"

97+ pagecolor="#ffffff"

98+ bordercolor="#666666"

99+ borderopacity="1.0"

100+ inkscape:pageopacity="0.0"

101+ inkscape:pageshadow="2"

102+ inkscape:zoom="1"

103+ inkscape:cx="396.85039"

104+ inkscape:cy="560"

105+ inkscape:document-units="mm"

106+ inkscape:current-layer="layer1"

107+ showgrid="false"

108+ inkscape:window-width="1920"

109+ inkscape:window-height="1015"

110+ inkscape:window-x="0"

111+ inkscape:window-y="0"

112+ inkscape:window-maximized="1" />

113+ <metadata

114+ id="metadata5">

115+ <rdf:RDF>

116+ <cc:Work

117+ rdf:about="">

118+ <dc:format>image/svg+xml</dc:format>

119+ <dc:type

120+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

121+ <dc:title />

122+ </cc:Work>

123+ </rdf:RDF>

124+ </metadata>

125+ <g

126+ inkscape:label="Layer 1"

127+ inkscape:groupmode="layer"

128+ id="layer1">

129+ <rect

130+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

131+ id="rect815"

132+ width="35.983334"

133+ height="18.25625"

134+ x="37.306248"

135+ y="79.512497"

136+ inkscape:export-xdpi="61.120499"

137+ inkscape:export-ydpi="61.120499" />

138+ <rect

139+ y="79.512497"

140+ x="92.339577"

141+ height="18.25625"

142+ width="35.983334"

143+ id="rect817"

144+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

145+ inkscape:export-xdpi="61.120499"

146+ inkscape:export-ydpi="61.120499" />

147+ <path

148+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"

149+ d="m 73.554166,88.508337 16.66875,-0.26459"

150+ id="path819"

151+ inkscape:connector-curvature="0"

152+ inkscape:export-xdpi="61.120499"

153+ inkscape:export-ydpi="61.120499" />

154+ <path

155+ inkscape:connector-curvature="0"

156+ id="path1535"

157+ d="m 18.785416,88.77292 16.66875,-0.26459"

158+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1539)"

159+ inkscape:export-xdpi="61.120499"

160+ inkscape:export-ydpi="61.120499" />

161+ <path

162+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2049)"

163+ d="m 128.32291,88.243753 16.66875,-0.26459"

164+ id="path2045"

165+ inkscape:connector-curvature="0"

166+ inkscape:export-xdpi="61.120499"

167+ inkscape:export-ydpi="61.120499" />

168+ <text

169+ xml:space="preserve"

170+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

171+ x="20.372915"

172+ y="85.597931"

173+ id="text2857"

174+ inkscape:export-xdpi="61.120499"

175+ inkscape:export-ydpi="61.120499"><tspan

176+ sodipodi:role="line"

177+ id="tspan2855"

178+ x="20.372915"

179+ y="85.597931"

180+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332">String</tspan></text>

181+ <text

182+ id="text2861"

183+ y="80.835434"

184+ x="76.199997"

185+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

186+ xml:space="preserve"

187+ inkscape:export-xdpi="61.120499"

188+ inkscape:export-ydpi="61.120499"><tspan

189+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

190+ y="80.835434"

191+ x="76.199997"

192+ sodipodi:role="line"

193+ id="tspan2867">List</tspan><tspan

194+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

195+ y="86.127098"

196+ x="76.199997"

197+ sodipodi:role="line"

198+ id="tspan2871">Token</tspan></text>

199+ <text

200+ xml:space="preserve"

201+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

202+ x="130.96875"

203+ y="85.068764"

204+ id="text2865"

205+ inkscape:export-xdpi="61.120499"

206+ inkscape:export-ydpi="61.120499"><tspan

207+ sodipodi:role="line"

208+ id="tspan2863"

209+ x="130.96875"

210+ y="85.068764"

211+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332">PTerm</tspan></text>

212+ <text

213+ id="text2875"

214+ y="89.302101"

215+ x="47.360416"

216+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332;"

217+ xml:space="preserve"

218+ inkscape:export-xdpi="61.120499"

219+ inkscape:export-ydpi="61.120499"><tspan

220+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332;fill:#0000ff;"

221+ y="89.302101"

222+ x="47.360416"

223+ id="tspan2873"

224+ sodipodi:role="line">Lexer</tspan></text>

225+ <text

226+ xml:space="preserve"

227+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"

228+ x="100.27708"

229+ y="89.037521"

230+ id="text2879"

231+ inkscape:export-xdpi="61.120499"

232+ inkscape:export-ydpi="61.120499"><tspan

233+ sodipodi:role="line"

234+ id="tspan2877"

235+ x="100.27708"

236+ y="89.037521"

237+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">Parser</tspan></text>

238+ <path

239+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker2891)"

240+ d="m 52.916666,71.575003 v 7.67291"

241+ id="path2887"

242+ inkscape:connector-curvature="0"

243+ sodipodi:nodetypes="cc"

244+ inkscape:export-xdpi="61.120499"

245+ inkscape:export-ydpi="61.120499" />

246+ <path

247+ sodipodi:nodetypes="cc"

248+ inkscape:connector-curvature="0"

249+ id="path3613"

250+ d="m 108.74375,71.575003 v 7.67291"

251+ style="fill:none;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker3617)"

252+ inkscape:export-xdpi="61.120499"

253+ inkscape:export-ydpi="61.120499" />

254+ <text

255+ id="text4173"

256+ y="69.987518"

257+ x="43.391666"

258+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

259+ xml:space="preserve"

260+ inkscape:export-xdpi="61.120499"

261+ inkscape:export-ydpi="61.120499"><tspan

262+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

263+ y="69.987518"

264+ x="43.391666"

265+ id="tspan4171"

266+ sodipodi:role="line">Recogniser</tspan></text>

267+ <text

268+ xml:space="preserve"

269+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

270+ x="97.102081"

271+ y="69.722939"

272+ id="text4177"

273+ inkscape:export-xdpi="61.120499"

274+ inkscape:export-ydpi="61.120499"><tspan

275+ sodipodi:role="line"

276+ id="tspan4175"

277+ x="97.102081"

278+ y="69.722939"

279+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332">Grammar</tspan></text>

280+ <text

281+ inkscape:export-ydpi="61.120499"

282+ inkscape:export-xdpi="61.120499"

283+ id="text854"

284+ y="93.800011"

285+ x="131.23334"

286+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

287+ xml:space="preserve"><tspan

288+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

289+ y="103.5316"

290+ x="131.23334"

291+ id="tspan852"

292+ sodipodi:role="line" /></text>

293+ </g>

294+</svg>

docs/image/recogniser.pngnew file

Binary file not shown.

docs/image/recogniser.svgnew file+477

@@ -0,0 +1,477 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

4+<svg

5+ xmlns:dc="http://purl.org/dc/elements/1.1/"

6+ xmlns:cc="http://creativecommons.org/ns#"

7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

8+ xmlns:svg="http://www.w3.org/2000/svg"

9+ xmlns="http://www.w3.org/2000/svg"

10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"

11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"

12+ width="210mm"

13+ height="297mm"

14+ viewBox="0 0 210 297"

15+ version="1.1"

16+ id="svg8"

17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"

18+ sodipodi:docname="recogniser.svg">

19+ <defs

20+ id="defs2" />

21+ <sodipodi:namedview

22+ id="base"

23+ pagecolor="#ffffff"

24+ bordercolor="#666666"

25+ borderopacity="1.0"

26+ inkscape:pageopacity="0.0"

27+ inkscape:pageshadow="2"

28+ inkscape:zoom="1"

29+ inkscape:cx="384.45994"

30+ inkscape:cy="560"

31+ inkscape:document-units="mm"

32+ inkscape:current-layer="layer1"

33+ showgrid="false"

34+ inkscape:window-width="1920"

35+ inkscape:window-height="1015"

36+ inkscape:window-x="0"

37+ inkscape:window-y="0"

38+ inkscape:window-maximized="1" />

39+ <metadata

40+ id="metadata5">

41+ <rdf:RDF>

42+ <cc:Work

43+ rdf:about="">

44+ <dc:format>image/svg+xml</dc:format>

45+ <dc:type

46+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

47+ <dc:title />

48+ </cc:Work>

49+ </rdf:RDF>

50+ </metadata>

51+ <g

52+ inkscape:label="Layer 1"

53+ inkscape:groupmode="layer"

54+ id="layer1">

55+ <rect

56+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70599997;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

57+ id="rect815"

58+ width="112.44793"

59+ height="77.258354"

60+ x="6.3499999"

61+ y="63.108334"

62+ ry="3.96875"

63+ inkscape:export-xdpi="61.120499"

64+ inkscape:export-ydpi="61.120499" />

65+ <text

66+ xml:space="preserve"

67+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:5.64444447px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#0000ff;fill-opacity:1;stroke:none;stroke-width:0.26458332"

68+ x="11.112496"

69+ y="68.399994"

70+ id="text819"

71+ inkscape:export-xdpi="61.120499"

72+ inkscape:export-ydpi="61.120499"><tspan

73+ sodipodi:role="line"

74+ id="tspan817"

75+ x="11.112496"

76+ y="68.399994"

77+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:5.64444447px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#0000ff;stroke-width:0.26458332">Text.Lexer.Core</tspan></text>

78+ <text

79+ id="text823"

80+ y="74.749992"

81+ x="8.7312441"

82+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

83+ xml:space="preserve"

84+ inkscape:export-xdpi="61.120499"

85+ inkscape:export-ydpi="61.120499"><tspan

86+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

87+ y="74.749992"

88+ x="8.7312441"

89+ id="tspan821"

90+ sodipodi:role="line">data Recognise : (consumes : Bool) -> Type where</tspan><tspan

91+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

92+ y="80.041656"

93+ x="8.7312441"

94+ sodipodi:role="line"

95+ id="tspan825"> Empty : Recognise False</tspan><tspan

96+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

97+ y="85.333328"

98+ x="8.7312441"

99+ sodipodi:role="line"

100+ id="tspan827"> Fail : Recognise c</tspan><tspan

101+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

102+ y="90.624992"

103+ x="8.7312441"

104+ sodipodi:role="line"

105+ id="tspan829"> Lookahead : (positive : Bool) -> Recognise c -> Recognise False</tspan><tspan

106+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

107+ y="95.916656"

108+ x="8.7312441"

109+ sodipodi:role="line"

110+ id="tspan831"> Pred : (Char -> Bool) -> Recognise True</tspan><tspan

111+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

112+ y="101.20832"

113+ x="8.7312441"

114+ sodipodi:role="line"

115+ id="tspan835"> SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True</tspan><tspan

116+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

117+ y="106.49999"

118+ x="8.7312441"

119+ sodipodi:role="line"

120+ id="tspan837"> SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)</tspan><tspan

121+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

122+ y="111.79166"

123+ x="8.7312441"

124+ sodipodi:role="line"

125+ id="tspan839"> Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)</tspan><tspan

126+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

127+ y="117.08332"

128+ x="8.7312441"

129+ sodipodi:role="line"

130+ id="tspan841" /><tspan

131+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

132+ y="122.37499"

133+ x="8.7312441"

134+ sodipodi:role="line"

135+ id="tspan843">||| A token recogniser. Guaranteed to consume at least one character.</tspan><tspan

136+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

137+ y="127.66666"

138+ x="8.7312441"

139+ sodipodi:role="line"

140+ id="tspan845">public export</tspan><tspan

141+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

142+ y="132.95833"

143+ x="8.7312441"

144+ sodipodi:role="line"

145+ id="tspan847">Lexer : Type</tspan><tspan

146+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

147+ y="138.24998"

148+ x="8.7312441"

149+ sodipodi:role="line"

150+ id="tspan849">Lexer = Recognise True</tspan><tspan

151+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.26458332"

152+ y="143.54166"

153+ x="8.7312441"

154+ sodipodi:role="line"

155+ id="tspan851" /></text>

156+ <rect

157+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

158+ id="rect850"

159+ width="111.65417"

160+ height="10.318749"

161+ x="9.7895756"

162+ y="97.504166"

163+ inkscape:export-xdpi="61.120499"

164+ inkscape:export-ydpi="61.120499" />

165+ <rect

166+ y="97.504166"

167+ x="9.7895756"

168+ height="15.610415"

169+ width="111.38958"

170+ id="rect852"

171+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

172+ inkscape:export-xdpi="61.120499"

173+ inkscape:export-ydpi="61.120499" />

174+ <text

175+ inkscape:export-ydpi="61.120499"

176+ inkscape:export-xdpi="61.120499"

177+ id="text870"

178+ y="98.297905"

179+ x="129.64584"

180+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

181+ xml:space="preserve"><tspan

182+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

183+ y="98.297905"

184+ x="129.64584"

185+ sodipodi:role="line"

186+ id="tspan908">(<+>) : Recognise c1 -> inf c1 (Recognise c2) -> </tspan><tspan

187+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

188+ y="103.58957"

189+ x="129.64584"

190+ sodipodi:role="line"

191+ id="tspan929"> Recognise (c1 || c2)</tspan><tspan

192+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

193+ y="108.88124"

194+ x="129.64584"

195+ sodipodi:role="line"

196+ id="tspan916">Sequence two recognisers. If either consumes a</tspan><tspan

197+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

198+ y="114.1729"

199+ x="129.64584"

200+ sodipodi:role="line"

201+ id="tspan918">character, the sequence is guaranteed to</tspan><tspan

202+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

203+ y="119.46457"

204+ x="129.64584"

205+ sodipodi:role="line"

206+ id="tspan935">consume a character</tspan><tspan

207+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

208+ y="124.75623"

209+ x="129.64584"

210+ sodipodi:role="line"

211+ id="tspan912" /><tspan

212+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

213+ y="130.04791"

214+ x="129.64584"

215+ sodipodi:role="line"

216+ id="tspan868" /></text>

217+ <path

218+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

219+ d="m 129.38124,100.41458 -7.9375,-2.910414"

220+ id="path937"

221+ inkscape:connector-curvature="0"

222+ sodipodi:nodetypes="cc"

223+ inkscape:export-xdpi="61.120499"

224+ inkscape:export-ydpi="61.120499" />

225+ <text

226+ xml:space="preserve"

227+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

228+ x="130.175"

229+ y="129.25418"

230+ id="text953"

231+ inkscape:export-xdpi="61.120499"

232+ inkscape:export-ydpi="61.120499"><tspan

233+ sodipodi:role="line"

234+ x="130.175"

235+ y="129.25418"

236+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

237+ id="tspan973">(<|>) : Recognise c1 -> Recognise c2 -></tspan><tspan

238+ sodipodi:role="line"

239+ x="130.175"

240+ y="134.54584"

241+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

242+ id="tspan975"> Recognise (c1 && c2)</tspan><tspan

243+ sodipodi:role="line"

244+ x="130.175"

245+ y="139.83751"

246+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

247+ id="tspan983">Alternative recognisers. If both consume, the</tspan><tspan

248+ sodipodi:role="line"

249+ x="130.175"

250+ y="145.12917"

251+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

252+ id="tspan985">combination is guaranteed to consumer a</tspan><tspan

253+ sodipodi:role="line"

254+ x="130.175"

255+ y="150.42084"

256+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

257+ id="tspan992">character.</tspan><tspan

258+ sodipodi:role="line"

259+ x="130.175"

260+ y="155.71251"

261+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

262+ id="tspan977" /><tspan

263+ id="tspan949"

264+ sodipodi:role="line"

265+ x="130.175"

266+ y="161.00417"

267+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan

268+ id="tspan951"

269+ sodipodi:role="line"

270+ x="130.175"

271+ y="166.29584"

272+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>

273+ <path

274+ inkscape:connector-curvature="0"

275+ id="path996"

276+ d="M 128.05833,126.87292 110.33125,110.46875"

277+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

278+ sodipodi:nodetypes="cc"

279+ inkscape:export-xdpi="61.120499"

280+ inkscape:export-ydpi="61.120499" />

281+ <text

282+ xml:space="preserve"

283+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

284+ x="28.045837"

285+ y="51.731236"

286+ id="text1012"

287+ inkscape:export-xdpi="61.120499"

288+ inkscape:export-ydpi="61.120499"><tspan

289+ id="tspan1006"

290+ sodipodi:role="line"

291+ x="28.045837"

292+ y="51.731236"

293+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">empty : Recognise False</tspan><tspan

294+ sodipodi:role="line"

295+ x="28.045837"

296+ y="57.022903"

297+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

298+ id="tspan1087">Recognise no input (doesn't consume any input)</tspan><tspan

299+ id="tspan1008"

300+ sodipodi:role="line"

301+ x="28.045837"

302+ y="62.314568"

303+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan

304+ id="tspan1010"

305+ sodipodi:role="line"

306+ x="28.045837"

307+ y="67.606232"

308+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>

309+ <text

310+ inkscape:export-ydpi="61.120499"

311+ inkscape:export-xdpi="61.120499"

312+ id="text1031"

313+ y="49.614574"

314+ x="114.56458"

315+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

316+ xml:space="preserve"><tspan

317+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

318+ y="49.614574"

319+ x="114.56458"

320+ sodipodi:role="line"

321+ id="tspan1025">fail : Recognise c</tspan><tspan

322+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

323+ y="54.906242"

324+ x="114.56458"

325+ sodipodi:role="line"

326+ id="tspan1089">A recogniser that always fails.</tspan><tspan

327+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

328+ y="60.197906"

329+ x="114.56458"

330+ sodipodi:role="line"

331+ id="tspan1027" /><tspan

332+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

333+ y="65.489571"

334+ x="114.56458"

335+ sodipodi:role="line"

336+ id="tspan1029" /></text>

337+ <text

338+ inkscape:export-ydpi="61.120499"

339+ inkscape:export-xdpi="61.120499"

340+ id="text1039"

341+ y="61.785423"

342+ x="128.32292"

343+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

344+ xml:space="preserve"><tspan

345+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

346+ y="61.785423"

347+ x="128.32292"

348+ sodipodi:role="line"

349+ id="tspan1051">expect : Recognise c -> Recognise False</tspan><tspan

350+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

351+ y="67.077087"

352+ x="128.32292"

353+ sodipodi:role="line"

354+ id="tspan1059">Positive lookahead. Never consumes input.</tspan><tspan

355+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

356+ y="72.368759"

357+ x="128.32292"

358+ sodipodi:role="line"

359+ id="tspan1035" /><tspan

360+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

361+ y="77.660423"

362+ x="128.32292"

363+ sodipodi:role="line"

364+ id="tspan1037" /></text>

365+ <text

366+ xml:space="preserve"

367+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

368+ x="125.14791"

369+ y="86.39167"

370+ id="text1047"

371+ inkscape:export-xdpi="61.120499"

372+ inkscape:export-ydpi="61.120499"><tspan

373+ id="tspan1041"

374+ sodipodi:role="line"

375+ x="125.14791"

376+ y="86.39167"

377+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">pred : (Char -> Bool) -> Lexer</tspan><tspan

378+ sodipodi:role="line"

379+ x="125.14791"

380+ y="91.683334"

381+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

382+ id="tspan1085">Recognise a character that matches a predicate</tspan><tspan

383+ id="tspan1043"

384+ sodipodi:role="line"

385+ x="125.14791"

386+ y="96.975006"

387+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan

388+ id="tspan1045"

389+ sodipodi:role="line"

390+ x="125.14791"

391+ y="102.26667"

392+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>

393+ <rect

394+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

395+ id="rect1053"

396+ width="79.904167"

397+ height="23.283327"

398+ x="121.70833"

399+ y="57.816666"

400+ inkscape:export-xdpi="61.120499"

401+ inkscape:export-ydpi="61.120499" />

402+ <text

403+ xml:space="preserve"

404+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';letter-spacing:0px;word-spacing:0px;fill:#ff0000;fill-opacity:1;stroke:none;stroke-width:0.26458332"

405+ x="128.32291"

406+ y="72.897926"

407+ id="text1069"

408+ inkscape:export-xdpi="61.120499"

409+ inkscape:export-ydpi="61.120499"><tspan

410+ id="tspan1063"

411+ sodipodi:role="line"

412+ x="128.32291"

413+ y="72.897926"

414+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332">reject : Recognise c -> Recognise False</tspan><tspan

415+ sodipodi:role="line"

416+ x="128.32291"

417+ y="78.18959"

418+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

419+ id="tspan1073">Negative lookahead. Never consumes input.</tspan><tspan

420+ sodipodi:role="line"

421+ x="128.32291"

422+ y="83.481262"

423+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332"

424+ id="tspan1075" /><tspan

425+ id="tspan1065"

426+ sodipodi:role="line"

427+ x="128.32291"

428+ y="88.772926"

429+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /><tspan

430+ id="tspan1067"

431+ sodipodi:role="line"

432+ x="128.32291"

433+ y="94.06459"

434+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#ff0000;stroke-width:0.26458332" /></text>

435+ <path

436+ sodipodi:nodetypes="cc"

437+ inkscape:connector-curvature="0"

438+ id="path1081"

439+ d="M 124.35416,89.83125 76.99375,94.858333"

440+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

441+ inkscape:export-xdpi="61.120499"

442+ inkscape:export-ydpi="61.120499" />

443+ <path

444+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

445+ d="M 123.82499,66.01875 112.97708,86.391666"

446+ id="path1083"

447+ inkscape:connector-curvature="0"

448+ sodipodi:nodetypes="cc"

449+ inkscape:export-xdpi="61.120499"

450+ inkscape:export-ydpi="61.120499" />

451+ <path

452+ sodipodi:nodetypes="cc"

453+ inkscape:connector-curvature="0"

454+ id="path1091"

455+ d="M 33.33749,59.139583 20.90208,76.337499"

456+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

457+ inkscape:export-xdpi="61.120499"

458+ inkscape:export-ydpi="61.120499" />

459+ <path

460+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

461+ d="M 113.77082,51.73125 42.068747,83.481249"

462+ id="path1093"

463+ inkscape:connector-curvature="0"

464+ sodipodi:nodetypes="cc"

465+ inkscape:export-xdpi="61.120499"

466+ inkscape:export-ydpi="61.120499" />

467+ <rect

468+ y="94.064583"

469+ x="129.64583"

470+ height="27.51667"

471+ width="78.316658"

472+ id="rect899"

473+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

474+ inkscape:export-xdpi="61.120499"

475+ inkscape:export-ydpi="61.120499" />

476+ </g>

477+</svg>

docs/image/tokenise.pngnew file

Binary file not shown.

docs/image/tokenise.svgnew file+740

@@ -0,0 +1,740 @@

1+<?xml version="1.0" encoding="UTF-8" standalone="no"?>

2+

4+<svg

5+ xmlns:dc="http://purl.org/dc/elements/1.1/"

6+ xmlns:cc="http://creativecommons.org/ns#"

7+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"

8+ xmlns:svg="http://www.w3.org/2000/svg"

9+ xmlns="http://www.w3.org/2000/svg"

10+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"

11+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"

12+ width="210mm"

13+ height="297mm"

14+ viewBox="0 0 210 297"

15+ version="1.1"

16+ id="svg8"

17+ inkscape:version="0.92.2 5c3e80d, 2017-08-06"

18+ sodipodi:docname="tokenise.svg">

19+ <defs

20+ id="defs2">

21+ <marker

22+ inkscape:isstock="true"

23+ style="overflow:visible;"

24+ id="marker7119"

25+ refX="0.0"

26+ refY="0.0"

27+ orient="auto"

28+ inkscape:stockid="Arrow1Mend">

29+ <path

30+ transform="scale(0.4) rotate(180) translate(10,0)"

31+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

32+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

33+ id="path7117" />

34+ </marker>

35+ <marker

36+ inkscape:stockid="Arrow1Mend"

37+ orient="auto"

38+ refY="0.0"

39+ refX="0.0"

40+ id="marker4031"

41+ style="overflow:visible;"

42+ inkscape:isstock="true"

43+ inkscape:collect="always">

44+ <path

45+ id="path4029"

46+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

47+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

48+ transform="scale(0.4) rotate(180) translate(10,0)" />

49+ </marker>

50+ <marker

51+ inkscape:isstock="true"

52+ style="overflow:visible;"

53+ id="marker1931"

54+ refX="0.0"

55+ refY="0.0"

56+ orient="auto"

57+ inkscape:stockid="Arrow1Mend"

58+ inkscape:collect="always">

59+ <path

60+ transform="scale(0.4) rotate(180) translate(10,0)"

61+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

62+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

63+ id="path1929" />

64+ </marker>

65+ <marker

66+ inkscape:stockid="Arrow1Mend"

67+ orient="auto"

68+ refY="0.0"

69+ refX="0.0"

70+ id="Arrow1Mend"

71+ style="overflow:visible;"

72+ inkscape:isstock="true"

73+ inkscape:collect="always">

74+ <path

75+ id="path1036"

76+ d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

77+ style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1;fill:#000000;fill-opacity:1"

78+ transform="scale(0.4) rotate(180) translate(10,0)" />

79+ </marker>

80+ </defs>

81+ <sodipodi:namedview

82+ id="base"

83+ pagecolor="#ffffff"

84+ bordercolor="#666666"

85+ borderopacity="1.0"

86+ inkscape:pageopacity="0.0"

87+ inkscape:pageshadow="2"

88+ inkscape:zoom="1"

89+ inkscape:cx="497.48698"

90+ inkscape:cy="885.5"

91+ inkscape:document-units="mm"

92+ inkscape:current-layer="layer1"

93+ showgrid="false"

94+ inkscape:window-width="1920"

95+ inkscape:window-height="1015"

96+ inkscape:window-x="0"

97+ inkscape:window-y="0"

98+ inkscape:window-maximized="1" />

99+ <metadata

100+ id="metadata5">

101+ <rdf:RDF>

102+ <cc:Work

103+ rdf:about="">

104+ <dc:format>image/svg+xml</dc:format>

105+ <dc:type

106+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />

107+ <dc:title></dc:title>

108+ </cc:Work>

109+ </rdf:RDF>

110+ </metadata>

111+ <g

112+ inkscape:label="Layer 1"

113+ inkscape:groupmode="layer"

114+ id="layer1">

115+ <rect

116+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

117+ id="rect815"

118+ width="4.3310161"

119+ height="4.3471913"

120+ x="61.383358"

121+ y="51.995804"

122+ inkscape:export-xdpi="61.120499"

123+ inkscape:export-ydpi="61.120499" />

124+ <text

125+ xml:space="preserve"

126+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

127+ x="62.917812"

128+ y="55.649193"

129+ id="text819"

130+ inkscape:export-xdpi="61.120499"

131+ inkscape:export-ydpi="61.120499"><tspan

132+ sodipodi:role="line"

133+ id="tspan817"

134+ x="62.917812"

135+ y="55.649193"

136+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">i</tspan></text>

137+ <rect

138+ y="51.995804"

139+ x="65.714371"

140+ height="4.3471913"

141+ width="4.3310161"

142+ id="rect823"

143+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

144+ inkscape:export-xdpi="61.120499"

145+ inkscape:export-ydpi="61.120499" />

146+ <text

147+ id="text827"

148+ y="55.307304"

149+ x="66.760414"

150+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

151+ xml:space="preserve"

152+ inkscape:export-xdpi="61.120499"

153+ inkscape:export-ydpi="61.120499"><tspan

154+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

155+ y="55.307304"

156+ x="66.760414"

157+ id="tspan825"

158+ sodipodi:role="line">n</tspan></text>

159+ <rect

160+ y="51.995804"

161+ x="70.045387"

162+ height="4.3471913"

163+ width="4.3310161"

164+ id="rect829"

165+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

166+ inkscape:export-xdpi="61.120499"

167+ inkscape:export-ydpi="61.120499" />

168+ <text

169+ id="text833"

170+ y="55.063095"

171+ x="71.237953"

172+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

173+ xml:space="preserve"

174+ inkscape:export-xdpi="61.120499"

175+ inkscape:export-ydpi="61.120499"><tspan

176+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

177+ y="55.063095"

178+ x="71.237953"

179+ id="tspan831"

180+ sodipodi:role="line">p</tspan></text>

181+ <rect

182+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

183+ id="rect835"

184+ width="4.3310161"

185+ height="4.3471913"

186+ x="74.376404"

187+ y="51.995804"

188+ inkscape:export-xdpi="61.120499"

189+ inkscape:export-ydpi="61.120499" />

190+ <text

191+ xml:space="preserve"

192+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

193+ x="75.422447"

194+ y="55.356148"

195+ id="text839"

196+ inkscape:export-xdpi="61.120499"

197+ inkscape:export-ydpi="61.120499"><tspan

198+ sodipodi:role="line"

199+ id="tspan837"

200+ x="75.422447"

201+ y="55.356148"

202+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">u</tspan></text>

203+ <rect

204+ y="51.995804"

205+ x="78.70742"

206+ height="4.3471913"

207+ width="4.3310161"

208+ id="rect841"

209+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

210+ inkscape:export-xdpi="61.120499"

211+ inkscape:export-ydpi="61.120499" />

212+ <text

213+ id="text845"

214+ y="55.649193"

215+ x="80.241875"

216+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

217+ xml:space="preserve"

218+ inkscape:export-xdpi="61.120499"

219+ inkscape:export-ydpi="61.120499"><tspan

220+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

221+ y="55.649193"

222+ x="80.241875"

223+ id="tspan843"

224+ sodipodi:role="line">t</tspan></text>

225+ <rect

226+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

227+ id="rect847"

228+ width="4.3310161"

229+ height="4.3471913"

230+ x="83.038437"

231+ y="51.995804"

232+ inkscape:export-xdpi="61.120499"

233+ inkscape:export-ydpi="61.120499" />

234+ <text

235+ xml:space="preserve"

236+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

237+ x="59.172871"

238+ y="88.457558"

239+ id="text851"><tspan

240+ sodipodi:role="line"

241+ id="tspan849"

242+ x="59.172871"

243+ y="92.350197"

244+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none" /></text>

245+ <rect

246+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

247+ id="rect853"

248+ width="4.3310161"

249+ height="4.3471913"

250+ x="87.369453"

251+ y="51.995804"

252+ inkscape:export-xdpi="61.120499"

253+ inkscape:export-ydpi="61.120499" />

254+ <text

255+ xml:space="preserve"

256+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

257+ x="88.46434"

258+ y="55.453827"

259+ id="text857"

260+ inkscape:export-xdpi="61.120499"

261+ inkscape:export-ydpi="61.120499"><tspan

262+ sodipodi:role="line"

263+ id="tspan855"

264+ x="88.46434"

265+ y="55.453827"

266+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">s</tspan></text>

267+ <rect

268+ y="51.995804"

269+ x="91.70047"

270+ height="4.3471913"

271+ width="4.3310161"

272+ id="rect859"

273+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

274+ inkscape:export-xdpi="61.120499"

275+ inkscape:export-ydpi="61.120499" />

276+ <text

277+ id="text863"

278+ y="55.649193"

279+ x="93.234924"

280+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

281+ xml:space="preserve"

282+ inkscape:export-xdpi="61.120499"

283+ inkscape:export-ydpi="61.120499"><tspan

284+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

285+ y="55.649193"

286+ x="93.234924"

287+ id="tspan861"

288+ sodipodi:role="line">t</tspan></text>

289+ <rect

290+ y="51.995804"

291+ x="96.031487"

292+ height="4.3471913"

293+ width="4.3310161"

294+ id="rect865"

295+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

296+ inkscape:export-xdpi="61.120499"

297+ inkscape:export-ydpi="61.120499" />

298+ <text

299+ id="text869"

300+ y="55.649193"

301+ x="97.565941"

302+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

303+ xml:space="preserve"

304+ inkscape:export-xdpi="61.120499"

305+ inkscape:export-ydpi="61.120499"><tspan

306+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

307+ y="55.649193"

308+ x="97.565941"

309+ id="tspan867"

310+ sodipodi:role="line">r</tspan></text>

311+ <rect

312+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

313+ id="rect871"

314+ width="4.3310161"

315+ height="4.3471913"

316+ x="100.3625"

317+ y="51.995804"

318+ inkscape:export-xdpi="61.120499"

319+ inkscape:export-ydpi="61.120499" />

320+ <text

321+ xml:space="preserve"

322+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

323+ x="101.89697"

324+ y="55.649193"

325+ id="text875"

326+ inkscape:export-xdpi="61.120499"

327+ inkscape:export-ydpi="61.120499"><tspan

328+ sodipodi:role="line"

329+ id="tspan873"

330+ x="101.89697"

331+ y="55.649193"

332+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">i</tspan></text>

333+ <rect

334+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

335+ id="rect877"

336+ width="4.3310161"

337+ height="4.3471913"

338+ x="104.69353"

339+ y="51.995804"

340+ inkscape:export-xdpi="61.120499"

341+ inkscape:export-ydpi="61.120499" />

342+ <text

343+ xml:space="preserve"

344+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

345+ x="105.73955"

346+ y="55.50267"

347+ id="text881"

348+ inkscape:export-xdpi="61.120499"

349+ inkscape:export-ydpi="61.120499"><tspan

350+ sodipodi:role="line"

351+ id="tspan879"

352+ x="105.73955"

353+ y="55.50267"

354+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">n</tspan></text>

355+ <rect

356+ y="51.995804"

357+ x="109.0245"

358+ height="4.3471913"

359+ width="4.3310161"

360+ id="rect883"

361+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

362+ inkscape:export-xdpi="61.120499"

363+ inkscape:export-ydpi="61.120499" />

364+ <text

365+ id="text887"

366+ y="54.965416"

367+ x="110.21709"

368+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

369+ xml:space="preserve"

370+ inkscape:export-xdpi="61.120499"

371+ inkscape:export-ydpi="61.120499"><tspan

372+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

373+ y="54.965416"

374+ x="110.21709"

375+ id="tspan885"

376+ sodipodi:role="line">g</tspan></text>

377+ <text

378+ xml:space="preserve"

379+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

380+ x="125.67681"

381+ y="55.359386"

382+ id="text893"

383+ inkscape:export-xdpi="61.120499"

384+ inkscape:export-ydpi="61.120499"><tspan

385+ sodipodi:role="line"

386+ id="tspan891"

387+ x="125.67681"

388+ y="55.359386"

389+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">:String</tspan></text>

390+ <rect

391+ y="51.995804"

392+ x="113.35551"

393+ height="4.3471913"

394+ width="4.3310161"

395+ id="rect895"

396+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

397+ inkscape:export-xdpi="61.120499"

398+ inkscape:export-ydpi="61.120499" />

399+ <text

400+ id="text899"

401+ y="55.50267"

402+ x="114.40154"

403+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

404+ xml:space="preserve"><tspan

405+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

406+ y="59.395306"

407+ x="114.40154"

408+ id="tspan897"

409+ sodipodi:role="line" /></text>

410+ <rect

411+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#0000ff;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

412+ id="rect901"

413+ width="4.3310161"

414+ height="4.3471913"

415+ x="117.68649"

416+ y="51.995804"

417+ inkscape:export-xdpi="61.120499"

418+ inkscape:export-ydpi="61.120499" />

419+ <text

420+ xml:space="preserve"

421+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

422+ x="118.87907"

423+ y="55.494583"

424+ id="text905"

425+ inkscape:export-xdpi="61.120499"

426+ inkscape:export-ydpi="61.120499"><tspan

427+ sodipodi:role="line"

428+ id="tspan903"

429+ x="118.87907"

430+ y="55.494583"

431+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">1</tspan></text>

432+ <g

433+ id="g950"

434+ transform="translate(-15.319488,0.319156)"

435+ inkscape:export-xdpi="61.120499"

436+ inkscape:export-ydpi="61.120499">

437+ <rect

438+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

439+ id="rect907"

440+ width="11.990757"

441+ height="4.3471909"

442+ x="47.978806"

443+ y="69.310013" />

444+ <text

445+ xml:space="preserve"

446+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

447+ x="48.706326"

448+ y="72.963402"

449+ id="text911"><tspan

450+ sodipodi:role="line"

451+ id="tspan909"

452+ x="48.706326"

453+ y="72.963402"

454+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">token</tspan></text>

455+ <rect

456+ y="69.310013"

457+ x="59.969563"

458+ height="4.2674026"

459+ width="10.075821"

460+ id="rect913"

461+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

462+ <text

463+ id="text917"

464+ y="72.940666"

465+ x="61.015606"

466+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

467+ xml:space="preserve"><tspan

468+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

469+ y="72.940666"

470+ x="61.015606"

471+ id="tspan915"

472+ sodipodi:role="line">line</tspan></text>

473+ <rect

474+ y="69.389801"

475+ x="70.045387"

476+ height="4.1876144"

477+ width="7.5225825"

478+ id="rect919"

479+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

480+ <text

481+ id="text923"

482+ y="72.935829"

483+ x="70.998589"

484+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

485+ xml:space="preserve"><tspan

486+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

487+ y="72.935829"

488+ x="70.998589"

489+ id="tspan921"

490+ sodipodi:role="line">col</tspan></text>

491+ </g>

492+ <text

493+ id="text927"

494+ y="80.971657"

495+ x="40.541954"

496+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

497+ xml:space="preserve"

498+ inkscape:export-xdpi="61.120499"

499+ inkscape:export-ydpi="61.120499"><tspan

500+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:4.23333311px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

501+ y="80.971657"

502+ x="40.541954"

503+ sodipodi:role="line"

504+ id="tspan933">:(List (TokenData Token), Int, Int, String)</tspan></text>

505+ <g

506+ id="g970"

507+ transform="translate(16.596112,0.319156)"

508+ inkscape:export-xdpi="61.120499"

509+ inkscape:export-ydpi="61.120499">

510+ <rect

511+ y="69.310013"

512+ x="47.978806"

513+ height="4.3471909"

514+ width="11.990757"

515+ id="rect952"

516+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

517+ <text

518+ id="text956"

519+ y="72.963402"

520+ x="48.706326"

521+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

522+ xml:space="preserve"><tspan

523+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

524+ y="72.963402"

525+ x="48.706326"

526+ id="tspan954"

527+ sodipodi:role="line">token</tspan></text>

528+ <rect

529+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

530+ id="rect958"

531+ width="10.075821"

532+ height="4.2674026"

533+ x="59.969563"

534+ y="69.310013" />

535+ <text

536+ xml:space="preserve"

537+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

538+ x="61.015606"

539+ y="72.940666"

540+ id="text962"><tspan

541+ sodipodi:role="line"

542+ id="tspan960"

543+ x="61.015606"

544+ y="72.940666"

545+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">line</tspan></text>

546+ <rect

547+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

548+ id="rect964"

549+ width="7.5225825"

550+ height="4.1876144"

551+ x="70.045387"

552+ y="69.389801" />

553+ <text

554+ xml:space="preserve"

555+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

556+ x="70.998589"

557+ y="72.935829"

558+ id="text968"><tspan

559+ sodipodi:role="line"

560+ id="tspan966"

561+ x="70.998589"

562+ y="72.935829"

563+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">col</tspan></text>

564+ </g>

565+ <g

566+ transform="translate(48.591501,0.319156)"

567+ id="g990"

568+ inkscape:export-xdpi="61.120499"

569+ inkscape:export-ydpi="61.120499">

570+ <rect

571+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

572+ id="rect972"

573+ width="11.990757"

574+ height="4.3471909"

575+ x="47.978806"

576+ y="69.310013" />

577+ <text

578+ xml:space="preserve"

579+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

580+ x="48.706326"

581+ y="72.963402"

582+ id="text976"><tspan

583+ sodipodi:role="line"

584+ id="tspan974"

585+ x="48.706326"

586+ y="72.963402"

587+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">token</tspan></text>

588+ <rect

589+ y="69.310013"

590+ x="59.969563"

591+ height="4.2674026"

592+ width="10.075821"

593+ id="rect978"

594+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

595+ <text

596+ id="text982"

597+ y="72.940666"

598+ x="61.015606"

599+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

600+ xml:space="preserve"><tspan

601+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

602+ y="72.940666"

603+ x="61.015606"

604+ id="tspan980"

605+ sodipodi:role="line">line</tspan></text>

606+ <rect

607+ y="69.389801"

608+ x="70.045387"

609+ height="4.1876144"

610+ width="7.5225825"

611+ id="rect984"

612+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />

613+ <text

614+ id="text988"

615+ y="72.935829"

616+ x="70.998589"

617+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

618+ xml:space="preserve"><tspan

619+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

620+ y="72.935829"

621+ x="70.998589"

622+ id="tspan986"

623+ sodipodi:role="line">col</tspan></text>

624+ </g>

625+ <path

626+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none"

627+ d="m 125.97308,68.549658 1.30238,0.0089 -0.0153,6.481345 h -1.30803"

628+ id="path992"

629+ inkscape:connector-curvature="0"

630+ sodipodi:nodetypes="cccc"

631+ inkscape:export-xdpi="61.120499"

632+ inkscape:export-ydpi="61.120499" />

633+ <path

634+ sodipodi:nodetypes="cccc"

635+ inkscape:connector-curvature="0"

636+ id="path994"

637+ d="m 32.561899,68.619523 -1.30238,0.0089 0.0153,6.481345 h 1.30803"

638+ style="fill:none;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1"

639+ inkscape:export-xdpi="61.120499"

640+ inkscape:export-ydpi="61.120499" />

641+ <rect

642+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

643+ id="rect996"

644+ width="11.990757"

645+ height="4.3471909"

646+ x="155.60759"

647+ y="69.899559"

648+ inkscape:export-xdpi="61.120499"

649+ inkscape:export-ydpi="61.120499" />

650+ <text

651+ xml:space="preserve"

652+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

653+ x="156.33508"

654+ y="73.552948"

655+ id="text1000"

656+ inkscape:export-xdpi="61.120499"

657+ inkscape:export-ydpi="61.120499"><tspan

658+ sodipodi:role="line"

659+ id="tspan998"

660+ x="156.33508"

661+ y="73.552948"

662+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none">string</tspan></text>

663+ <rect

664+ y="69.750786"

665+ x="130.3979"

666+ height="4.2674026"

667+ width="10.075821"

668+ id="rect1002"

669+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

670+ inkscape:export-xdpi="61.120499"

671+ inkscape:export-ydpi="61.120499" />

672+ <text

673+ id="text1006"

674+ y="73.381439"

675+ x="131.44394"

676+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

677+ xml:space="preserve"

678+ inkscape:export-xdpi="61.120499"

679+ inkscape:export-ydpi="61.120499"><tspan

680+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

681+ y="73.381439"

682+ x="131.44394"

683+ id="tspan1004"

684+ sodipodi:role="line">line</tspan></text>

685+ <rect

686+ y="69.830574"

687+ x="143.64868"

688+ height="4.1876144"

689+ width="7.5225825"

690+ id="rect1008"

691+ style="opacity:1;vector-effect:none;fill:none;fill-opacity:0.97596154;fill-rule:evenodd;stroke:#ff0000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"

692+ inkscape:export-xdpi="61.120499"

693+ inkscape:export-ydpi="61.120499" />

694+ <text

695+ id="text1012"

696+ y="73.376602"

697+ x="144.60188"

698+ style="font-style:normal;font-weight:normal;font-size:4.23333311px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

699+ xml:space="preserve"

700+ inkscape:export-xdpi="61.120499"

701+ inkscape:export-ydpi="61.120499"><tspan

702+ style="font-size:4.23333311px;stroke-width:0.70555556;stroke-miterlimit:4;stroke-dasharray:none"

703+ y="73.376602"

704+ x="144.60188"

705+ id="tspan1010"

706+ sodipodi:role="line">col</tspan></text>

707+ <path

708+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#Arrow1Mend)"

709+ d="m 58.415342,69.700595 -0.143613,-5.887785 4.912582,-0.06048 0.03784,-6.371998"

710+ id="path1025"

711+ inkscape:connector-curvature="0"

712+ sodipodi:nodetypes="cccc"

713+ inkscape:export-xdpi="61.120499"

714+ inkscape:export-ydpi="61.120499" />

715+ <path

716+ inkscape:connector-curvature="0"

717+ id="path1927"

718+ d="m 89.918872,69.996556 -0.02264,-12.07186"

719+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1931)"

720+ sodipodi:nodetypes="cc"

721+ inkscape:export-xdpi="61.120499"

722+ inkscape:export-ydpi="61.120499" />

723+ <path

724+ sodipodi:nodetypes="cccc"

725+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker4031)"

726+ d="m 122.08751,69.519138 -0.0832,-5.464386 -2.3456,-0.06048 -0.20406,-6.674425"

727+ id="path4027"

728+ inkscape:connector-curvature="0"

729+ inkscape:export-xdpi="61.120499"

730+ inkscape:export-ydpi="61.120499" />

731+ <path

732+ inkscape:connector-curvature="0"

733+ id="path7115"

734+ d="m 147.18896,69.882051 -0.0832,-5.827299 -22.72919,0 -0.446,-6.251027"

735+ style="fill:none;stroke:#000000;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker7119)"

736+ sodipodi:nodetypes="cccc"

737+ inkscape:export-xdpi="61.120499"

738+ inkscape:export-ydpi="61.120499" />

739+ </g>

740+</svg>

docs/index.rst+3−1

@@ -13,7 +13,7 @@ Documentation for the Idris Language

1313 Idris Community* has waived all copyright and related or neighboring

1414 rights to Documentation for Idris.

1515

16− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

16+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1717

1818

1919.. toctree::

@@ -24,5 +24,7 @@ Documentation for the Idris Language

2424 st/index

2525 effects/index

2626 proofs/index

27+ elaboratorReflection/index

28+ parserLibrary/index

2729 reference/index

2830 guides/index

docs/listing/idris-prompt-helloworld.txt+1−1

@@ -2,7 +2,7 @@ $ idris hello.idr

22 ____ __ _

33 / _/___/ /____(_)____

44 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

66 /___/\__,_/_/ /_/____/ Type :? for help

88Type checking ./hello.idr

docs/listing/idris-prompt-interp.txt+1−1

@@ -2,7 +2,7 @@ $ idris interp.idr

22 ____ __ _

33 / _/___/ /____(_)____

44 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

66 /___/\__,_/_/ /_/____/ Type :? for help

88Type checking ./interp.idr

docs/listing/idris-prompt-start.txt+1−1

@@ -2,7 +2,7 @@ $ idris

22 ____ __ _

33 / _/___/ /____(_)____

44 / // __ / ___/ / ___/ Version 1.3.2

5− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

5+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

66/___/\__,_/_/ /_/____/ Type :? for help

88Idris>

docs/make.bat+1−1

@@ -65,7 +65,7 @@ if errorlevel 9009 (

6565 echo.may add the Sphinx directory to PATH.

6666 echo.

6767 echo.If you don't have Sphinx installed, grab it from

68− echo.http://sphinx-doc.org/

68+ echo.https://www.sphinx-doc.org/

6969 exit /b 1

7070)

7171

docs/parserLibrary/index.rstnew file+24

@@ -0,0 +1,24 @@

1+.. _parserLibrary:

3+########################

4+Lexer and Parser Library

5+########################

7+A tutorial on the lexer and parser library in Idris.

9+.. note::

10+

11+ The documentation for Idris has been published under the Creative

12+ Commons CC0 License. As such to the extent possible under law, *The

13+ Idris Community* has waived all copyright and related or neighboring

14+ rights to Documentation for Idris.

15+

16+ More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

17+

18+.. toctree::

19+ :maxdepth: 1

20+

21+ introduction

22+ lexer

23+ parser

24+ whitespace

docs/parserLibrary/introduction.rstnew file+76

@@ -0,0 +1,76 @@

1+.. _parserLibraryIntro:

3+***************************

4+Parser Library Introduction

5+***************************

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.

9+An 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

12+is done in Idris 2 and that is what the this library appears to have been

13+written for.

14+

15+So a secondary use for this tutorial would be to help understanding the internal

16+workings of Idris 2.

17+

18+The parser library is used in a similar way to Parsec which is a library for

19+writing parsers in Haskell. It is based on higher-order parser combinators, so a

20+complicated parser can be made out of many smaller ones.

21+

22+.. list-table::

23+

24+ * - This is a two stage process:

25+ - Lexer - This takes the input string and turns it into a list of Tokens.

26+ - Parser - This takes the list of tokens and outputs the code.

27+

28+.. image:: ../image/parserTopLevel.png

29+ :width: 307px

30+ :height: 76px

31+ :alt: diagram illustrating these stages of lexer and parser

32+

33+The advantage of using two stages, like this, is that things like whitespace and

34+comments don't need to be considered in every parser rule.

35+

36+The Idris parser library differs from Parsec in that you need to say in the

37+Recogniser whether a rule is guaranteed to consume input. This means that the

38+Idris type system prevents the construction of recognisers/rules that can't

39+consume the input.

40+

41+The Lexer is similar but works at the level of characters rather than tokens, and

42+you need to provide a TokenMap which says how to build a token representation from

43+a string when a rule is matched.

44+

45+The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a

46+tutorial for the :ref:`parserLibraryParser`. These tutorials have a running

47+example of a parser for integer expressions. This is a very simple example, there

48+may be easier ways to do something so simple, but it illustrates some of the

49+principles.

50+

51+Parser Library and Idris 2

52+--------------------------

53+

54+The parser library, in Idris 1, is almost the same as the code that the Idris 2

55+parser is built on. Even if you only want to use the Idris 1 parser library it

56+is useful to look at the code in the Idris 2 compilers to see how the library

57+can be used.

58+

59+Idris 2 has at least 3 compilers:

60+

61+- IDEMode - complies to SExp which is a Lisp-like structure used to communicate

62+ with external editors like Emacs and Vim.

63+- Idris.Parser - This is the main compiler which compiles from a file to

64+ PTerm (and eventually TT structure).

65+- REPL - compiles input from the command line.

66+

67+The following diagram is my first attempt to work out how some of the modules in

68+Idris 2 fit together (with a few of the dependencies between them shown). The

69+Idris 1 library is based on the modules at the bottom of the diagram (shown

70+in red).

71+

72+.. image:: ../image/parserModules.png

73+ :width: 460px

74+ :height: 496px

75+ :alt: diagram illustrating these stages of lexer and parser

76+

docs/parserLibrary/lexer.rstnew file+282

@@ -0,0 +1,282 @@

1+.. _parserLibraryLexer:

3+Lexer

4+=====

6+The lexer is run by calling the 'lex' function in the Text.Lexer.Core

7+module:

9+.. code-block:: idris

10+

11+ lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

12+

13+This function takes a String and returns a list of tokens. With the tokens we

14+have indexes back to the original string which can be used in error messages:

15+

16+.. image:: ../image/tokenise.png

17+ :width: 330px

18+ :height: 73px

19+ :alt: diagram illustrating these stages of lexer

20+

21+TokenMap

22+--------

23+

24+In order to construct this list of tokens we need:

25+

26+- A way to recognise the tokens in the input string.

27+- A way to construct these individual tokens.

28+

29+This is given by the TokenMap which is a list of pairs containing

30+this information:

31+

32+.. code-block:: idris

33+

34+ (Lexer, String -> tokenType)

35+

36+So for each Lexer in the list, if a substring in the input matches, run

37+the associated function to produce a token of type `tokenType`

38+

39+from Text.Lexer.Core:

40+

41+.. code-block:: idris

42+

43+ TokenMap : (tokenType : Type) -> Type

44+ TokenMap tokenType = List (Lexer, String -> tokenType)

45+

46+We can create a tokenMap by using a function like this:

47+

48+.. code-block:: idris

49+

50+ myTokenMap : TokenMap Token

51+ myTokenMap = [(is 'a',CharLit)]

52+

53+Once we have a TokenMap we can use it to lex many strings.

54+

55+Recognisers

56+-----------

57+

58+The first part of each entry in the TokenMap is the recogniser.

59+

60+A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to

61+test whether to accept the character. It can be constructed using the

62+'is' function:

63+

64+.. code-block:: idris

65+

66+ *parserEx> is 'a'

67+ Pred (\ARG =>

68+ intToBool (prim__eqChar ARG 'a'))

69+ : Recognise True

70+

71+More complicated structures can be recognised as tokens, this is done using

72+the combinator structure of recognisers. This allows recognisers to be

73+combined, for example,

74+

75+.. list-table::

76+

77+ * - <+> means sequence two recognisers. If either consumes a character,

78+ the sequence is guaranteed to consume a character.

79+

80+ - .. code-block:: idris

81+

82+ *parserEx> is 'a' <+> is 'b'

83+ SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

84+ (Delay (is 'b')) : Recognise True

85+

86+ * - <|> means if both consume, the combination is guaranteed

87+ to consumer a character:

88+

89+ - .. code-block:: idris

90+

91+ *parserEx> is 'a' <|> is 'b'

92+ Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

93+ (Pred (\ARG => intToBool (prim__eqChar ARG 'b')))

94+ : Recognise True

95+

96+This diagram shows the recogniser combinator with some of its constructors:

97+

98+.. image:: ../image/recogniser.png

99+ :width: 487px

100+ :height: 249px

101+ :alt: recogniser data structure

102+

103+A recogniser consumes its input, that is it advances the index to its input

104+string, as it generates the token list. In some cases we don't want this to

105+happen, for instance, we may need to lookahead before consuming the input

106+string.

107+

108+If a recogniser does not consume input there is a danger of an infinite loop.

109+To prevent this the recogniser is dependent on a boolean called 'consumes' which

110+is true if the recogniser is guaranteed to consume at least one character.

111+

112+The constructors of Recognise allow us to ensure that, even though parts of

113+the recogniser may not consume, overall the recogniser will consume.

114+

115+Since 'Recognise True' is more common than 'Recognise False' it is convenient to

116+use 'Lexer' as a type synonym for 'Recognise True'.

117+

118+Whitespace and Comments

119+-----------------------

120+

121+An important reason to have a lexer is to simplify the parser when whitespace

122+or comments are required. Without this the parser would require a match for

123+every combination, with and without, whitespace and comments.

124+

125+In some languages the lexer needs to remove whitespace and comments so that

126+they don't appear in the token list. In some cases whitespace is significant

127+but a single whitespace token can stand for any number of spaces, tabs,

128+carriage returns and so on.

129+

130+In some cases, such as when parsing the Idris language itself, whitespace

131+is important to indicate blocks. In this case we might want to output a

132+start-of-block token when the indent increases and an end-of-block token

133+when the indent decreases.

134+

135+This topic will be discussed more fully on this page

136+:ref:`parserLibraryWhitespace`.

137+

138+Simple Expression Example for Lexer

139+-----------------------------------

140+

141+On this page we will implement a lexer to 'lex' a very simple expression as

142+a running example, on the next page, we will go on to implement a parser for it.

143+

144+First import the lexer and parser code:

145+

146+.. code-block:: idris

147+

148+ module ParserExample

149+

150+ import Text.Lexer

151+ import public Text.Parser.Core

152+ import public Text.Parser

153+

154+Then decide on the tokens that are needed. For this example the idea is to be

155+able to parse simple arithmetic expressions, like this:

156+

157+.. code-block:: idris

158+

159+ 1+(2*3)

160+

161+so we need:

162+

163+- Numbers (for now integer literals are good enough).

164+- Some operators (for now '+', '-' and '*' will do.

165+- Opening and closing Parentheses.

166+

167+We can define these, as tokens, like this:

168+

169+.. code-block:: idris

170+

171+ %default total

172+

173+ public export

174+ data ExpressionToken = Number Integer

175+ | Operator String

176+ | OParen

177+ | CParen

178+ | EndInput

179+

180+It may help with debugging and to implement error messages to

181+implement 'show' for these tokens:

182+

183+.. code-block:: idris

184+

185+ export

186+ Show ExpressionToken where

187+ show (Number x) = "number " ++ show x

188+ show (Operator x) = "operator " ++ x

189+ show OParen = "("

190+ show CParen = ")"

191+ show EndInput = "end of input"

192+

193+ export

194+ Show (TokenData ExpressionToken) where

195+ show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t

196+

197+The following defines the 'TokenMap' for this example:

198+

199+.. code-block:: idris

200+

201+ ||| integer arithmetic operators plus, minus and multiply.

202+ export

203+ opChars : String

204+ opChars = "+-*"

205+

206+ operator : Lexer

207+ operator = some (oneOf opChars)

208+

209+ toInt' : String -> Integer

210+ toInt' = cast

211+

212+ expressionTokens : TokenMap ExpressionToken

213+ expressionTokens =

214+ [(digits, \x => Number (toInt' x)),

215+ (operator, \x => Operator x),

216+ (is '(' ,\x => OParen),

217+ (is ')' ,\x => CParen)]

218+

219+This specifies the lexer. It gives, for each token, a function to recognise

220+the token type and a function to construct the token.

221+

222+The library module 'Text.Lexer' contains useful functions to help with this.

223+For example, the digits function used above, which reads one or more

224+numeric characters.

225+

226+We can now run the code with various strings to see what output the lexer

227+produces. This is done by calling the 'lex' function with the TokenMap and

228+input string as parameters:

229+

230+.. code-block:: idris

231+

232+ cd Idris-dev/libs/contrib

233+ idris -p contrib parserEx.idr

234+ ____ __ _

235+ / _/___/ /____(_)____

236+ / // __ / ___/ / ___/ Version 1.3.2

237+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/

238+ /___/\__,_/_/ /_/____/ Type :? for help

239+

240+ Idris is free software with ABSOLUTELY NO WARRANTY.

241+ For details type :warranty.

242+ Type checking ./Text/Token.idr

243+ Type checking ./Text/Quantity.idr

244+ Type checking ./Control/Delayed.idr

245+ Type checking ./Data/Bool/Extra.idr

246+ Type checking ./Text/Lexer/Core.idr

247+ Type checking ./Text/Lexer.idr

248+ Type checking ./parserEx.idr

249+

250+ *parserEx> lex expressionTokens "1+2"

251+ ([MkToken 0 0 (Number 1),

252+ MkToken 0

253+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of

254+ (incol, "") => c + cast (length incol)

255+ (incol, b) => cast (length incol))

256+ (Operator "+"),

257+ MkToken 0

258+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of

259+ (incol, "") => c + cast (length incol)

260+ (incol, b) => cast (length incol))

261+ (Number 2)],

262+ 0,

263+ case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "2" of

264+ (incol, "") => c + cast (length incol)

265+ (incol, b) => cast (length incol),

266+ getString (MkStrLen "" 0)) : (List (TokenData ExpressionToken),

267+ Int,

268+ Int,

269+ String)

270+

271+The lexer uses potentially infinite data structures. It has recursive

272+arguments (codata type) so code is lazy. In the output above the indexes

273+have not been computed but we can pick out the tokens:

274+

275+- (Number 1)

276+- (Operator "+")

277+- (Number 2)

278+

279+So the code is working.

280+

281+We can now go ahead and parse this token list. A parser for this example will

282+be constructed on the next page.

docs/parserLibrary/parser.rstnew file+622

@@ -0,0 +1,622 @@

1+.. _parserLibraryParser:

3+Parser

4+======

6+To run our parser we call 'parse'. This requires a Grammar and the output

7+from the lexer (a list of tokens).

9+.. code-block:: idris

10+

11+ parse : (act : Grammar tok c ty) -> (xs : List tok) ->

12+ Either (ParseError tok) (ty, List tok)

13+

14+If successful this returns 'Right' with a pair of

15+

16+- the parse result.

17+- the unparsed tokens (the remaining input).

18+

19+otherwise it returns 'Left' with the error message.

20+

21+So we need to define the Grammar for our parser, this is done using the following

22+'Grammar' data structure. This is a combinator structure, similar in principle

23+to the recogniser combinator for the lexer, which was discussed on the

24+previous page.

25+

26+As with the Recogniser the Grammar type is dependent on a boolean 'consumes'

27+value which allows us to ensure that complicated Grammar structures will always

28+consume input.

29+

30+.. code-block:: idris

31+

32+ ||| Description of a language's grammar. The `tok` parameter is the type

33+ ||| of tokens, and the `consumes` flag is True if the language is guaranteed

34+ ||| to be non-empty - that is, successfully parsing the language is guaranteed

35+ ||| to consume some input.

36+ public export

37+ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where

38+ Empty : (val : ty) -> Grammar tok False ty

39+ Terminal : String -> (tok -> Maybe a) -> Grammar tok True a

40+ NextIs : String -> (tok -> Bool) -> Grammar tok False tok

41+ EOF : Grammar tok False ()

42+

43+ Fail : Bool -> String -> Grammar tok c ty

44+ Commit : Grammar tok False ()

45+ MustWork : Grammar tok c a -> Grammar tok c a

46+

47+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->

48+ Grammar tok True b

49+ SeqEmpty : {c1, c2 : Bool} ->

50+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->

51+ Grammar tok (c1 || c2) b

52+ Alt : {c1, c2 : Bool} ->

53+ Grammar tok c1 ty -> Grammar tok c2 ty ->

54+ Grammar tok (c1 && c2) ty

55+

56+So an example of a Grammer type may look something like this:

57+'Grammar (TokenData ExpressionToken) True Integer'.

58+

59+This is a complicated type name and a given parser will need to use it a lot.

60+So to reduce the amount of typing we can use the following type synonym (similar

61+to what is done in Idris 2

62+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

63+

64+.. code-block:: idris

65+

66+ public export

67+ Rule : Type -> Type

68+ Rule ty = Grammar (TokenData ExpressionToken) True ty

69+

70+Parser Example

71+--------------

72+

73+On the previous page we implemented a lexer to 'lex' a very simple expression, on

74+this page we will go on to implement a parser for this running example.

75+

76+.. list-table::

77+

78+ * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something

79+ like this:

80+ - .. code-block:: idris

81+

82+ <expr> ::= <integer literal>

83+ | <expr>'+'<expr>

84+ | <expr>'-'<expr>

85+ | <expr>'*'<expr>

86+ | '('<expr>')'

87+

88+ <integer literal> ::= <digit>|<integer literal><digit>

89+

90+.. list-table::

91+

92+ * - To start, here is a Grammar to parse an integer literal (that is, a

93+ sequence of numbers).

94+

95+ - .. code-block:: idris

96+

97+ export

98+ intLiteral : Rule Integer

99+ intLiteral

100+ = terminal (\x => case tok x of

101+ Number i => Just i

102+ _ => Nothing)

103+

104+In order to try this out, here is a temporary function, this calls

105+parse which takes two parameters:

106+

107+- The grammar (in this case intLiteral)

108+- The token list from the lexer.

109+

110+.. code-block:: idris

111+

112+ test1 : String -> Either (ParseError (TokenData ExpressionToken))

113+ (Integer, List (TokenData ExpressionToken))

114+ test1 s = parse intLiteral (fst (lex expressionTokens s))

115+

116+As required, if we pass it a string which is a number literal then it will

117+return the number in the 'Right' option.

118+

119+.. code-block:: idris

120+

121+ *parserEx> test1 "123"

122+ Right (123, []) : Either (ParseError (TokenData ExpressionToken))

123+ (Integer, List (TokenData ExpressionToken))

124+

125+If we pass it a string which is not a number literal then it will return an

126+error message.

127+

128+.. code-block:: idris

129+

130+ *parserEx> test1 "a"

131+ Left (Error "End of input"

132+ []) : Either (ParseError (TokenData ExpressionToken))

133+ (Integer, List (TokenData ExpressionToken))

134+

135+If we pass it a number followed by something else, then it will still be

136+successful, this is because we are not specifically checking for end-of-file.

137+

138+.. code-block:: idris

139+

140+ *parserEx> test1 "123a"

141+ Right (123, []) : Either (ParseError (TokenData ExpressionToken))

142+ (Integer, List (TokenData ExpressionToken))

143+ *parserEx>

144+

145+.. list-table::

146+

147+ * - The 'intLiteral' function above uses the 'terminal' function to

148+ construct the grammar

149+ - .. code-block:: idris

150+

151+ ||| Succeeds if running the predicate on the

152+ ||| next token returns Just x, returning x.

153+ ||| Otherwise fails.

154+ export

155+ terminal : (tok -> Maybe a) -> Grammar tok True a

156+ terminal = Terminal

157+

158+This is defined here

159+: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Parser/Core.idr

160+Idris 2 uses a slightly different version which stores an error message like

161+"Expected integer literal" which can be output if the rule fails

162+: https://github.com/edwinb/Idris2/blob/master/src/Text/Parser/Core.idr

163+

164+.. list-table::

165+

166+ * - The 'terminal' function is also used to construct the other

167+ elements of the grammar that we require, for instance,

168+ opening parenthesis:

169+

170+ - .. code-block:: idris

171+

172+ openParen : Rule Integer

173+ openParen = terminal (\x => case tok x of

174+ OParen => Just 0

175+ _ => Nothing)

176+

177+Integer value is not really relevant for parenthesis so '0' is used as

178+a default value.

179+

180+As before, we can test this out with a function like this:

181+

182+.. code-block:: idris

183+

184+ test2 : String -> Either (ParseError (TokenData ExpressionToken))

185+ (Integer, List (TokenData ExpressionToken))

186+ test2 s = parse openParen (fst (lex expressionTokens s))

187+

188+We can see below that it correctly parses an open parenthesis and gives an

189+error for anything else:

190+

191+.. code-block:: idris

192+

193+ *parserEx> test2 "("

194+ Right (0, []) : Either (ParseError (TokenData ExpressionToken))

195+ (Integer, List (TokenData ExpressionToken))

196+ *parserEx> test2 "123"

197+ Left (Error "Unrecognised token"

198+ [MkToken 0

199+ 0

200+ (Number 123)]) : Either (ParseError (TokenData ExpressionToken))

201+ (Integer,

202+ List (TokenData ExpressionToken))

203+

204+Now we have two Grammars we can try combining them. The following test looks

205+for 'openParen' followed by 'intLiteral', the two Grammars are combined using

206+'<*>'. The 'map const' part uses the integer value from the first.

207+

208+The following test is looking for '(' followed by a number:

209+

210+.. code-block:: idris

211+

212+ test3 : String -> Either (ParseError (TokenData ExpressionToken))

213+ (Integer, List (TokenData ExpressionToken))

214+ test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))

215+

216+We can see below that '(' followed by a number is successfully parsed but other

217+token lists are not:

218+

219+.. code-block:: idris

220+

221+ *parserEx> test3 "(123"

222+ Right (0, []) : Either (ParseError (TokenData ExpressionToken))

223+ (Integer, List (TokenData ExpressionToken))

224+ *parserEx> test3 "(("

225+ Left (Error "Unrecognised token"

226+ [MkToken 0

227+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))

228+ "(" of

229+ (incol, "") => c + cast (length incol)

230+ (incol, b) => cast (length incol))

231+ OParen]) : Either (ParseError (TokenData ExpressionToken))

232+ (Integer, List (TokenData ExpressionToken))

233+

234+ *parserEx> test3 "123"

235+ Left (Error "Unrecognised token"

236+ [MkToken 0

237+ 0

238+ (Number 123)]) : Either (ParseError (TokenData ExpressionToken))

239+ (Integer,

240+ List (TokenData ExpressionToken))

241+ *parserEx> test3 "123("

242+ Left (Error "Unrecognised token"

243+ [MkToken 0 0 (Number 123),

244+ MkToken 0

245+ (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))

246+ "321" of

247+ (incol, "") => c + cast (length incol)

248+ (incol, b) => cast (length incol))

249+ OParen]) : Either (ParseError (TokenData ExpressionToken))

250+ (Integer, List (TokenData ExpressionToken))

251+

252+.. list-table::

253+

254+ * - The closing parenthesis is constructed in the same way.

255+

256+ - .. code-block:: idris

257+

258+ closeParen : Rule Integer

259+ closeParen = terminal (\x => case tok x of

260+ CParen => Just 0

261+ _ => Nothing)

262+

263+.. list-table::

264+

265+ * - Now we can generate a Grammar for an expression inside parenthesis

266+ like this.

267+

268+ - .. code-block:: idris

269+

270+ paren : Rule Integer -> Rule Integer

271+ paren exp = openParen *> exp <* closeParen

272+

273+The use of '*>' and '<*' instead of '<*>' is an easy way to use the integer

274+value from the inner expression.

275+

276+.. list-table::

277+

278+ * - Now for the operations, in this case: '+', '-' and '*'.

279+ The syntax we require is that operators like '+' are infix operators, which

280+ would require a definition like this:

281+

282+ - .. code-block:: idris

283+

284+ expr = (add expr (op "+") expr)

285+

286+This is a potentially infinite structure which is not total.

287+In order to work up to this gradually I will start with prefix operators

288+(sometimes known as Polish notation) then modify later for infix operators.

289+

290+.. list-table::

291+

292+ * - So prefix operators would have this sort of form:

293+

294+ - .. code-block:: idris

295+

296+ expr = (add (op "+") expr expr)

297+

298+where 'op' is defined like this:

299+

300+.. code-block:: idris

301+

302+ ||| Matches if this is an operator token and string matches, that is,

303+ ||| it is the required type of operator.

304+ op : String -> Rule Integer

305+ op s = terminal (\x => case tok x of

306+ (Operator s1) => if s==s1 then Just 0 else Nothing

307+ _ => Nothing)

308+

309+.. list-table::

310+

311+ * - and 'add' is defined like this:

312+

313+ - .. code-block:: idris

314+

315+ addInt : Integer -> Integer -> Integer

316+ addInt a b = a+b

317+

318+ export

319+ add : Grammar tok c1 Integer ->

320+ Grammar tok c2 Integer ->

321+ Grammar tok c3 Integer ->

322+ Grammar tok ((c1 || c2) || c3) Integer

323+ add x y z = map addInt (x *> y) <*> z

324+

325+Where:

326+

327+- x is the add operator.

328+- y is the first operand.

329+- z is the second operand.

330+

331+The resulting integer will be the sum of the two operands.

332+

333+The other operators are defined in a similar way:

334+

335+.. code-block:: idris

336+

337+ subInt : Integer -> Integer -> Integer

338+ subInt a b = a-b

339+

340+ export

341+ sub : Grammar tok c1 Integer ->

342+ Grammar tok c2 Integer ->

343+ Grammar tok c3 Integer ->

344+ Grammar tok ((c1 || c2) || c3) Integer

345+ sub x y z = map subInt (x *> y) <*> z

346+

347+

348+ multInt : Integer -> Integer -> Integer

349+ multInt a b = a*b

350+

351+ export

352+ mult : Grammar tok c1 Integer ->

353+ Grammar tok c2 Integer ->

354+ Grammar tok c3 Integer ->

355+ Grammar tok ((c1 || c2) || c3) Integer

356+ mult x y z = map multInt (x *> y) <*> z

357+

358+So the top level Grammar can now be defined as follows. Note that this is

359+partial as it is a potentially infinite structure and so not total.

360+

361+.. code-block:: idris

362+

363+ partial

364+ expr : Rule Integer

365+ expr = (add (op "+") expr expr)

366+ <|> (sub (op "-") expr expr)

367+ <|> (mult (op "*") expr expr)

368+ <|> intLiteral <|> (paren expr)

369+

370+.. list-table::

371+

372+ * - To make the testing easier we can use this function:

373+

374+ - .. code-block:: idris

375+

376+ partial

377+ test : String -> Either (ParseError (TokenData ExpressionToken))

378+ (Integer, List (TokenData ExpressionToken))

379+ test s = parse expr (fst (lex expressionTokens s))

380+

381+.. list-table::

382+

383+ * - First test a valid (prefix) expression:

384+

385+ - .. code-block:: idris

386+

387+ *parserEx> test "+1*6(4)"

388+ Right (25,

389+ []) : Either (ParseError (TokenData ExpressionToken))

390+ (Integer, List (TokenData ExpressionToken))

391+

392+Then an invalid syntax:

393+

394+.. code-block:: idris

395+

396+ *parserEx> test "))"

397+ Left (Error "Unrecognised token"

398+ [MkToken 0 0 CParen,

399+ MkToken 0

400+ (case fspan (\ARG =>

401+ not (intToBool (prim__eqChar ARG

402+ '\n')))

403+ ")" of

404+ (incol, "") => c + cast (length incol)

405+ (incol, b) => cast (length incol))

406+ CParen]) : Either (ParseError (TokenData ExpressionToken))

407+ (Integer,

408+ List (TokenData ExpressionToken))

409+

410+However if we try something that is invalid, but starts with a valid token,

411+then it will return 'Right' (to indicate success)

412+

413+.. code-block:: idris

414+

415+ *parserEx> test "1))"

416+ Right (1,

417+ [MkToken 0

418+ (case fspan (\ARG =>

419+ not (intToBool (prim__eqChar ARG '\n')))

420+ "1" of

421+ (incol, "") => c + cast (length incol)

422+ (incol, b) => cast (length incol))

423+ CParen,

424+ MkToken 0

425+ (case fspan (\ARG =>

426+ not (intToBool (prim__eqChar ARG '\n')))

427+ ")" of

428+ (incol, "") => c + cast (length incol)

429+ (incol, b) => cast (length incol))

430+ CParen]) : Either (ParseError (TokenData ExpressionToken))

431+ (Integer,

432+ List (TokenData ExpressionToken))

433+

434+Infix Notation

435+--------------

436+

437+So far we have implemented a prefix notation for operators (like this:

438+'+ expr expr') but the aim is to implemented an infix notation (like this:

439+'expr + expr'). To do this we must be able to deal with potentially

440+infinite data structures (see Codata Types here :ref:`sect-typefuns`).

441+

442+First alter the grammar to have infix operations:

443+

444+.. code-block:: idris

445+

446+ addInt : Integer -> Integer -> Integer

447+ addInt a b = a+b

448+

449+ export

450+ add : Grammar tok c1 Integer ->

451+ Grammar tok c2 Integer ->

452+ Grammar tok c3 Integer ->

453+ Grammar tok ((c1 || c2) || c3) Integer

454+ add x y z = map addInt (x <* y) <*> z

455+

456+ subInt : Integer -> Integer -> Integer

457+ subInt a b = a-b

458+

459+ export

460+ sub : Grammar tok c1 Integer ->

461+ Grammar tok c2 Integer ->

462+ Grammar tok c3 Integer ->

463+ Grammar tok ((c1 || c2) || c3) Integer

464+ sub x y z = map subInt (x <* y) <*> z

465+

466+

467+ multInt : Integer -> Integer -> Integer

468+ multInt a b = a*b

469+

470+ export

471+ mult : Grammar tok c1 Integer ->

472+ Grammar tok c2 Integer ->

473+ Grammar tok c3 Integer ->

474+ Grammar tok ((c1 || c2) || c3) Integer

475+ mult x y z = map multInt (x <* y) <*> z

476+

477+ partial

478+ expr : Rule Integer

479+ expr = (add expr (op "+") expr)

480+ <|> (sub expr (op "-") expr)

481+ <|> (mult expr (op "*") expr)

482+ <|> intLiteral <|> (paren expr)

483+

484+However, if this was run, the code would not terminate.

485+

486+Implement Left Recursion Elimination

487+------------------------------------

488+

489+Left factoring, like this, is a general problem.

490+

491+If we have a rule like this:

492+

493+.. code-block:: idris

494+

495+ A -> (x<*>y) <|> (x<*>z)

496+

497+If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has

498+already consumed 'x', so now 'x<*>z' will fail.

499+

500+so we could write code to backtrack. That is 'try' 'x<*>y' without consuming

501+so that, if the first token succeeds but the following tokens fail, then the

502+first tokens would not be consumed.

503+

504+Another approach is left factoring:

505+

506+Left Factoring

507+--------------

508+

509+Replace the rule with two rules (that is we add a non-terminal symbol) so

510+for example, instead of:

511+

512+.. code-block:: idris

513+

514+ A -> (x<*>y) <|> (x<*>z)

515+

516+we add an extra rule to give:

517+

518+.. code-block:: idris

519+

520+ A -> x<*>N

521+ N -> y <|> z

522+

523+That is we convert a general context-free grammar to a LL(1) grammar. Although

524+not every context-free grammar can be converted to a LL(1) grammar.

525+

526+This still does not solve the infinite recursion issue and there is another

527+problem: the precedence of the operators +, - and * is not explicit.

528+

529+To resolve this we can alter the example like this:

530+

531+.. code-block:: idris

532+

533+ paren : Rule Integer -> Rule Integer

534+ paren exp = openParen *> exp <* closeParen

535+

536+ addInt : Integer -> Integer -> Integer

537+ addInt a b = a+b

538+

539+ subInt : Integer -> Integer -> Integer

540+ subInt a b = a-b

541+

542+ multInt : Integer -> Integer -> Integer

543+ multInt a b = a*b

544+

545+ partial

546+ expr : Rule Integer

547+

548+ partial

549+ exprAtom : Rule Integer

550+ exprAtom = intLiteral <|> (paren expr)

551+

552+ partial

553+ expr1 : Rule Integer

554+ expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)

555+

556+ partial

557+ exprMult : Rule Integer

558+ exprMult = expr1 <|> exprAtom

559+

560+ partial

561+ expr2 : Rule Integer

562+ expr2 = map addInt exprMult <*> ((op "+") *> exprMult)

563+

564+ partial

565+ exprAdd : Rule Integer

566+ exprAdd = expr2 <|> exprMult

567+

568+ partial

569+ expr3 : Rule Integer

570+ expr3 = map subInt exprAdd <*> ((op "-") *> expr)

571+

572+ expr = expr3 <|> exprAdd

573+

574+As the following tests show, this now handles infix operators and precedence.

575+

576+.. list-table::

577+

578+ * - For example '*' is an infix operator:

579+

580+ - .. code-block:: idris

581+

582+ *parserExInfix> test "2*3"

583+ Right (6,

584+ []) : Either (ParseError (TokenData ExpressionToken))

585+ (Integer, List (TokenData ExpressionToken))

586+

587+ * - Check that atomic number literals work:

588+

589+ - .. code-block:: idris

590+

591+ *parserExInfix> test "2"

592+ Right (2,

593+ []) : Either (ParseError (TokenData ExpressionToken))

594+ (Integer, List (TokenData ExpressionToken))

595+

596+ * - Check that '*' has a higher precedence than '+'.

597+

598+ - .. code-block:: idris

599+

600+ *parserExInfix> test "2+3*4"

601+ Right (14,

602+ []) : Either (ParseError (TokenData ExpressionToken))

603+ (Integer, List (TokenData ExpressionToken))

604+

605+ * - Also '*' has a higher precedence than '+' when the order is reversed.

606+

607+ - .. code-block:: idris

608+

609+ *parserExInfix> test "3*4+2"

610+ Right (14,

611+ []) : Either (ParseError (TokenData ExpressionToken))

612+ (Integer, List (TokenData ExpressionToken))

613+

614+ * - Also precedence can be overridden by parenthesis.

615+

616+ - .. code-block:: idris

617+

618+ *parserExInfix> test "(2+3)*4"

619+ Right (20,

620+ []) : Either (ParseError (TokenData ExpressionToken))

621+ (Integer, List (TokenData ExpressionToken))

622+

docs/parserLibrary/whitespace.rstnew file+154

@@ -0,0 +1,154 @@

1+.. _parserLibraryWhitespace:

3+Whitespace and Comments

4+=======================

6+The previous two pages introduced the lexer and parser but have not yet

7+discussed how to handle whitespace and comments.

9+In some grammars whitespace and comments would not be considered significant and

10+so we might be tempted not to generate any tokens for them. However, in the

11+running example, we may want to make spaces significant. For example, we might

12+want to implement function application expressed by juxtaposition as in

13+Haskell and Idris like this: ``f x``.

14+

15+Also, I'm not sure if it is an problem for error messages and so on if some

16+text does not have corresponding tokens.

17+

18+So, on this page, we will add a token for whitespace and comments.

19+

20+Whitespace and Comments in Lexer

21+--------------------------------

22+

23+To start with we can use the same token for both whitespace and comments. Here

24+it is called ``Comment`` and added to the ``ExpressionToken`` data structure

25+like this:

26+

27+.. code-block:: idris

28+

29+ public export

30+ data ExpressionToken = Number Integer

31+ | Operator String

32+ | OParen

33+ | CParen

34+ | Comment String

35+ | EndInput

36+

37+This is added to the ``TokenMap`` like this:

38+

39+.. code-block:: idris

40+

41+ ||| from https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr

42+ comment : Lexer

43+ comment = is '-' <+> is '-' <+> many (isNot '\n')

44+

45+ expressionTokens : TokenMap ExpressionToken

46+ expressionTokens =

47+ [(digits, \x => Number (toInt' x)),

48+ (operator, \x => Operator x),

49+ (is '(' ,\x => OParen),

50+ (is ')' ,\x => CParen),

51+ (spaces, Comment),

52+ (comment, Comment)]

53+

54+As you can see, the comment is defined like a single line Idris comment,

55+it starts with ``--`` and continues for the remainder of the line.

56+

57+We don't need to define ``spaces`` because it is already defined in

58+: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr

59+like this:

60+

61+.. code-block:: idris

62+

63+ ||| Recognise a single whitespace character

64+ ||| /\\s/

65+ space : Lexer

66+ space = pred isSpace

67+

68+ ||| Recognise one or more whitespace characters

69+ ||| /\\s+/

70+ spaces : Lexer

71+ spaces = some space

72+

73+Whitespace and Comments in Parser

74+---------------------------------

75+

76+Now that there are ``Comment`` tokens the parser needs to be able to handle them.

77+

78+.. code-block:: idris

79+

80+ commentSpace : Rule Integer

81+ commentSpace = terminal (\x => case tok x of

82+ Comment s => Just 0

83+ _ => Nothing)

84+

85+So far we don't have any syntax that requires spaces to be significant so we

86+need to define the grammar so that it will parse with, or without, spaces.

87+This needs to be done in a systematic way, here I have defined the grammar so

88+that there is an optional space to the right of every atom or operator:

89+

90+.. code-block:: idris

91+

92+ partial

93+ exprAtom : Rule Integer

94+ exprAtom = (intLiteral <* commentSpace)

95+ <|> intLiteral <|> (paren expr)

96+

97+ partial

98+ expr1 : Rule Integer

99+ expr1 = map multInt exprAtom <*> (

100+ (((op "*") <* commentSpace) <|> (op "*"))

101+ *> exprAtom)

102+

103+ partial

104+ exprMult : Rule Integer

105+ exprMult = expr1 <|> exprAtom

106+

107+ partial

108+ expr2 : Rule Integer

109+ expr2 = map addInt exprMult <*> (

110+ (((op "+") <* commentSpace) <|> (op "+"))

111+ *> exprMult)

112+

113+ partial

114+ exprAdd : Rule Integer

115+ exprAdd = expr2 <|> exprMult

116+

117+ partial

118+ expr3 : Rule Integer

119+ expr3 = map subInt exprAdd <*> (

120+ (((op "-") <* commentSpace) <|> (op "-"))

121+ *> expr)

122+

123+ expr = expr3 <|> exprAdd

124+

125+Defining Block Structure using Indents

126+--------------------------------------

127+

128+Many languages such as Python, Haskell and Idris use indents to delimit

129+the block structure of the language.

130+

131+We can see how Idris2 does it here

132+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

133+

134+.. code-block:: idris

135+

136+ export

137+ IndentInfo : Type

138+ IndentInfo = Int

139+

140+ export

141+ init : IndentInfo

142+ init = 0

143+

144+

145+

146+

147+

148+

149+

150+

151+

152+

153+

154+

docs/proofs/index.rst+5−10

@@ -1,8 +1,8 @@

11.. _proofs-index:

3−#########################################

4−Theorem Proving and Elaborator Reflection

5−#########################################

3+###############

4+Theorem Proving

5+###############

77A tutorial on theorem proving in Idris.

@@ -13,7 +13,7 @@ A tutorial on theorem proving in Idris.

1313 Idris Community* has waived all copyright and related or neighboring

1414 rights to Documentation for Idris.

1515

16− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

16+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1717

1818.. toctree::

1919 :maxdepth: 1

@@ -25,9 +25,4 @@ A tutorial on theorem proving in Idris.

2525 propositional

2626 interactive

2727 interactiveOld

28− elabReflection

29− tactics

30− holes

31− example1

32− primitive

33− generatingData

28+

docs/proofs/interactive.rst+1−1

@@ -129,7 +129,7 @@ On running , two global names are created, ``plusredZ_Z`` and

129129

130130 . / _/___/ /____(_)____

131131 / // __ / ___/ / ___/ Version 1.2.0

132− _/ // /_/ / / / (__ ) http://www.idris-lang.org/

132+ _/ // /_/ / / / (__ ) https://www.idris-lang.org/

133133 /___/\__,_/_/ /_/____/ Type :? for help

134134

135135 Idris is free software with ABSOLUTELY NO WARRANTY.

docs/proofs/propositional.rst+1−1

@@ -34,7 +34,7 @@ Replace

3434

3535This implements the *indiscernability of identicals* principle, if two terms are equal then they have the same properties. In other words, if ``x=y``, then we can substitute ``y`` for ``x`` in any expression. In our proofs we can express this as:

3636

37−.. code-block::

37+.. code-block:: idris

3838

3939 if x=y

4040 then P x = P y

docs/reference/erasure.rst+2−2

@@ -254,7 +254,7 @@ Benchmarks

254254==========

255255

256256- source: https://github.com/ziman/idris-benchmarks

257−- results: http://ziman.functor.sk/erasure-bm/

257+- results: https://ziman.functor.sk/erasure-bm/

258258

259259It can be clearly seen that asymptotics are improved by erasure.

260260

@@ -499,4 +499,4 @@ References

499499

500500.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive

501501 families need not store their indices

502− <http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

502+ <https://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__

docs/reference/index.rst+1−2

@@ -14,7 +14,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor

1414 Idris Community* has waived all copyright and related or neighboring

1515 rights to Documentation for Idris.

1616

17− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

17+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1818

1919

2020.. toctree::

@@ -36,7 +36,6 @@ This will tell you how Idris works, for using it you should read the Idris Tutor

3636 internals

3737 language-features

3838 language-extensions

39− elaborator-reflection

4039 type-directed-search

4140 partial-evaluation

4241 misc

docs/reference/language-extensions.rst+8−3

@@ -3,13 +3,12 @@ Language Extensions

33*******************

6−

76Type Providers

87===============

109Idris type providers are a way to get the type system to reflect

1110observations about the world outside of Idris. Similarly to `F# type

12−providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,

11+providers <https://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,

1312they cause effectful computations to run during type checking, returning

1413information that the type checker can use when checking the rest of the

1514program. While F# type providers are based on code generation, Idris

@@ -32,5 +31,11 @@ to the user.

3231Example Idris type providers can be seen at `this

3332repository <https://github.com/david-christiansen/idris-type-providers>`__.

3433More detailed descriptions are available in David Christiansen's `WGP

35−'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.

34+'13 paper <https://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.

3635thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.

36+

37+Elaborator Reflection

38+=====================

39+

40+Another way to extend the language is elaborator reflection which is described

41+in the :ref:`elaborator-index` section.

docs/reference/partial-evaluation.rst+2−2

@@ -8,7 +8,7 @@ of functions with arguments annotated as ``%static``.

99(This is an implementation of the partial evaluator described in `this

1010ICFP 2010

11−paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.

11+paper <https://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.

1212Please refer to this for more precise definitions of what follows.)

1313

1414Partial evaluation is switched off by default since Idris 1.0. It can

@@ -207,7 +207,7 @@ Specialising Interpreters

207207A particularly useful situation where partial evaluation becomes

208208effective is in defining an interpreter for a well-typed expression

209209language, defined as follows (see the `Idris tutorial, section

210−4 <http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__

210+4 <https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__

211211for more details on how this works):

212212

213213::

docs/reference/type-directed-search.rst+1−1

@@ -4,7 +4,7 @@ Type Directed Search ``:search``

55Idris' ``:search`` command searches for terms according to their

66approximate type signature (much like

7−`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For

7+`Hoogle <https://www.haskell.org/hoogle/>`__ for Haskell). For

88example::

1010 Idris> :search e -> List e -> List e

docs/reference/uniqueness-types.rst+1−1

@@ -13,7 +13,7 @@ ideally while giving up as little high level conveniences as possible.

1313

1414They are inspired by linear types, `Uniqueness Types

1515<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean

16−<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

16+<https://wiki.clean.cs.ru.nl/Clean>`__ programming language, and

1717ownership types and borrowed pointers in the `Rust

1818<https://www.rust-lang.org/>`__ programming language.

1919

docs/st/index.rst+1−1

@@ -14,7 +14,7 @@ the `Control.ST` library in `Idris`.

1414 Idris Community* has waived all copyright and related or neighbouring

1515 rights to Documentation for Idris.

1616

17− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

17+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1818

1919.. toctree::

2020 :maxdepth: 1

docs/st/introduction.rst+1−1

@@ -3,7 +3,7 @@ Overview

33********

55Pure functional languages with dependent types such as `Idris

6−<http://www.idris-lang.org/>`_ support reasoning about programs directly

6+<https://www.idris-lang.org/>`_ support reasoning about programs directly

77in the type system, promising that we can *know* a program will run

88correctly (i.e. according to the specification in its type) simply

99because it compiles.

docs/tutorial/conclusions.rst+5−5

@@ -7,7 +7,7 @@ Further Reading

77Further information about Idris programming, and programming with

88dependent types in general, can be obtained from various sources:

10−- The Idris web site (http://www.idris-lang.org/) and by asking

10+- The Idris web site (https://www.idris-lang.org/) and by asking

1111 questions on the mailing list.

1212

1313- The IRC channel ``#idris``, on

@@ -25,7 +25,7 @@ dependent types in general, can be obtained from various sources:

2525 https://github.com/idris-lang/Idris-dev.

2626

2727- Existing projects on the ``Idris Hackers`` web space:

28− http://idris-hackers.github.io.

28+ https://idris-hackers.github.io.

2929

3030- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly

3131 describe older versions of Idris.

@@ -36,14 +36,14 @@ dependent types in general, can be obtained from various sources:

3636 Aspects of Declarative Languages (PADL'12), Claudio Russo and

3737 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,

3838 242-257. DOI=10.1007/978-3-642-27694-1_18

39− http://dx.doi.org/10.1007/978-3-642-27694-1_18

39+ https://dx.doi.org/10.1007/978-3-642-27694-1_18

4040

4141.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full

4242 dependent types. In Proceedings of the 5th ACM workshop on

4343 Programming languages meets program verification (PLPV

4444 '11). ACM, New York, NY, USA,

4545 43-54. DOI=10.1145/1929529.1929536

46− http://doi.acm.org/10.1145/1929529.1929536

46+ https://doi.acm.org/10.1145/1929529.1929536

4747

4848.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your

4949 inefficient engine: using partial evaluation to improve

@@ -51,4 +51,4 @@ dependent types in general, can be obtained from various sources:

5151 15th ACM SIGPLAN international conference on Functional

5252 programming (ICFP '10). ACM, New York, NY, USA,

5353 297-308. DOI=10.1145/1863543.1863587

54− http://doi.acm.org/10.1145/1863543.1863587

54+ https://doi.acm.org/10.1145/1863543.1863587

docs/tutorial/index.rst+1−1

@@ -15,7 +15,7 @@ existing functional programming language such as Haskell or OCaml.

1515 Idris Community* has waived all copyright and related or neighboring

1616 rights to Documentation for Idris.

1717

18− More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/

18+ More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/

1919

2020

2121.. toctree::

docs/tutorial/introduction.rst+2−2

@@ -6,7 +6,7 @@ Introduction

77In conventional programming languages, there is a clear distinction

88between *types* and *values*. For example, in `Haskell

9−<http://www.haskell.org>`_, the following are types, representing

9+<https://www.haskell.org>`_, the following are types, representing

1010integers, characters, lists of characters, and lists of any value

1111respectively:

1212

@@ -49,7 +49,7 @@ Intended Audience

4949

5050This tutorial is intended as a brief introduction to the language, and

5151is aimed at readers already familiar with a functional language such

52−as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.

52+as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.

5353In particular, a certain amount of familiarity with Haskell syntax is

5454assumed, although most concepts will at least be explained

5555briefly. The reader is also assumed to have some interest in using

docs/tutorial/miscellany.rst+1−1

@@ -560,7 +560,7 @@ But what about the type of ``Type``? If we ask Idris it reports:

560560 Type : Type 1

561561

562562If ``Type`` were its own type, it would lead to an inconsistency due to

563−`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,

563+`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,

564564so internally there is a *hierarchy* of types (or *universes*):

565565

566566.. code-block:: idris

docs/tutorial/syntax.rst+3−3

@@ -196,16 +196,16 @@ syntax rule, we can even go as far as:

196196 Aspects of Declarative Languages (PADL'12), Claudio Russo and

197197 Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,

198198 242-257. DOI=10.1007/978-3-642-27694-1_18

199− http://dx.doi.org/10.1007/978-3-642-27694-1_18

199+ https://dx.doi.org/10.1007/978-3-642-27694-1_18

200200

201201.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full

202202 dependent types. In Proceedings of the 5th ACM workshop on

203203 Programming languages meets program verification (PLPV

204204 '11). ACM, New York, NY, USA,

205205 43-54. DOI=10.1145/1929529.1929536

206− http://doi.acm.org/10.1145/1929529.1929536

206+ https://doi.acm.org/10.1145/1929529.1929536

207207

208208.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction

209209 Concurrency: Using Dependent Types to Verify Implementations of

210210 Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April

211− 2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636

211+ 2010), 145-176. https://dl.acm.org/citation.cfm?id=1883636

idris.cabal+2−2

@@ -5,7 +5,7 @@ License: BSD-3-Clause

55License-file: LICENSE

66Author: Edwin Brady

77Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>

8−Homepage: http://www.idris-lang.org/

8+Homepage: https://www.idris-lang.org/

99Bug-reports: https://github.com/idris-lang/Idris-dev/issues

1010

1111Stability: Beta

@@ -17,7 +17,7 @@ Description: Idris is a general purpose language with full dependent types.

1717 meaning that some aspects of a program's behaviour can be

1818 specified precisely in the type. The language is closely

1919 related to Epigram and Agda. There is a tutorial at

20− <http://www.idris-lang.org/documentation>.

20+ <https://www.idris-lang.org/documentation>.

2121 Features include:

2222 .

2323 * Full, first class, dependent types with dependent pattern matching

libs/base/Data/Fin.idr+9

@@ -65,6 +65,11 @@ weakenN : (n : Nat) -> Fin m -> Fin (m + n)

6565weakenN n FZ = FZ

6666weakenN n (FS f) = FS (weakenN n f)

6767

68+||| Weaken the bound on a Fin using an inequality proof

69+weakenLTE : LTE n m -> Fin n -> Fin m

70+weakenLTE (LTESucc p) FZ = FZ

71+weakenLTE (LTESucc p) (FS f) = FS $ weakenLTE p f

72+

6873||| Attempt to tighten the bound on a Fin.

6974||| Return `Left` if the bound could not be tightened, or `Right` if it could.

7075strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

@@ -101,6 +106,10 @@ implementation MinBound (Fin (S n)) where

101106implementation MaxBound (Fin (S n)) where

102107 maxBound = last

103108

109+||| Add two Fins

110+addFin : (x : Fin n) -> (y : Fin m) -> Fin (finToNat x + m)

111+addFin FZ y = y

112+addFin (FS x) y = FS $ addFin x y

104113

105114-- Construct a Fin from an integer literal which must fit in the given Fin

106115

libs/base/Data/List/Quantifiers.idr+5

@@ -75,3 +75,8 @@ all d (x::xs) with (d x)

7575 case all d xs of

7676 Yes prf' => Yes (prf :: prf')

7777 No prf' => No (notAllThere prf')

78+

79+||| Given a proof of membership for some element, extract the property proof for it

80+indexAll : Elem x xs -> All p xs -> p x

81+indexAll Here (p::_ ) = p

82+indexAll (There e) ( _::ps) = indexAll e ps

libs/contrib/Data/Combinators.idr+2−2

@@ -26,13 +26,13 @@ infixl 9 ...

2626(...) = (.) . (.)

2727

2828||| Warbler, as named in "To Mock a Mockingbird".

29−||| See http://code.jsoftware.com/wiki/Vocabulary/tilde

29+||| See https://code.jsoftware.com/wiki/Vocabulary/tilde

3030||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)

3131reflex : (a -> a -> b) -> (a -> b)

3232reflex f x = f x x

3333

3434||| Phoenix, according to Data.Aviary.

35−||| See http://code.jsoftware.com/wiki/Vocabulary/fork.

35+||| See https://code.jsoftware.com/wiki/Vocabulary/fork.

3636||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)

3737fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)

3838fork2 f g h x = f (g x) (h x)

libs/contrib/Data/Nat/Parity.idr+72

@@ -89,3 +89,75 @@ mutual

8989 oddOdd : Odd n -> odd n = True

9090 oddOdd {n = Z} (_ ** pf) = absurd pf

9191 oddOdd {n = S _} pf = evenEven $ predOddEven pf

92+

93+||| Even plus Even is Even.

94+evenPlusEven : Even j -> Even k -> Even (j + k)

95+evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =

96+ rewrite pf_j in

97+ rewrite pf_k in

98+ (half_j + half_k **

99+ sym $ multDistributesOverPlusLeft half_j half_k 2)

100+

101+||| Odd plus Odd is Even.

102+oddPlusOdd : Odd j -> Odd k -> Even (j + k)

103+oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =

104+ rewrite pf_j in

105+ rewrite pf_k in

106+ rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in

107+ rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in

108+ (S (haf_j + haf_k) ** Refl)

109+

110+||| Even plus Odd is Odd.

111+evenPlusOdd : Even j -> Odd k -> Odd (j + k)

112+evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =

113+ rewrite pf_j in

114+ rewrite pf_k in

115+ rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in

116+ rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in

117+ (half_j + haf_k ** Refl)

118+

119+||| A helper fact.

120+multShuffle : (a, b, c : Nat) ->

121+ (a * c) * (b * c) = ((a * b) * c) * c

122+multShuffle a b c =

123+ rewrite multAssociative (a * c) b c in

124+ rewrite multCommutative (a * c) b in

125+ rewrite multAssociative b a c in

126+ rewrite multCommutative b a in

127+ Refl

128+

129+||| Even times Even is Even.

130+evenMultEven : Even j -> Even k -> Even (j * k)

131+evenMultEven (half_j ** pf_j) (half_k ** pf_k) =

132+ rewrite pf_j in

133+ rewrite pf_k in

134+ (half_j * half_k * 2 **

135+ multShuffle half_j half_k 2)

136+

137+||| Even times Odd is Even.

138+evenMultOdd : Even j -> Odd k -> Even (j * k)

139+evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =

140+ let half = half_j * haf_k * 2 in

141+ rewrite pf_j in

142+ rewrite pf_k in

143+ rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in

144+ rewrite multShuffle half_j haf_k 2 in

145+ (half_j + half **

146+ sym $ multDistributesOverPlusLeft half_j half 2)

147+

148+||| Odd times Odd is Odd.

149+oddMultOdd : Odd j -> Odd k -> Odd (j * k)

150+oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =

151+ let

152+ haf = haf_j * haf_k * 2

153+ rem = haf_j + haf_k

154+ in

155+ rewrite pf_j in

156+ rewrite pf_k in

157+ rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in

158+ rewrite multShuffle haf_j haf_k 2 in

159+ rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in

160+ rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in

161+ rewrite plusCommutative haf_k haf_j in

162+ rewrite sym $ multDistributesOverPlusLeft rem haf 2 in

163+ (rem + haf ** Refl)

libs/contrib/Language/JSON.idr+1−1

@@ -1,4 +1,4 @@

1−||| The JSON language, as described at http://json.org/

1+||| The JSON language, as described at https://json.org/

22module Language.JSON

44import Language.JSON.Lexer

libs/prelude/IO.idr+1−1

@@ -80,7 +80,7 @@ foreign_prim f fname (FFun arg sc) env

8080||| Idris compiler backend in use. For the default C backend, see the

8181||| documentation for `FFI_C`.

8282|||

83−||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).

83+||| For more details, please consult [the Idris documentation](https://idris.readthedocs.io/en/latest/reference/ffi.html).

8484|||

8585||| @ f an FFI descriptor, which is specific to the compiler backend.

8686||| @ fname the name of the foreign function

man/idris.1+1−1

@@ -113,7 +113,7 @@ should not necessarily be seen as production ready nor for industrial use.

113113

114114.SH SEE ALSO

115115

116−+ The IDRIS web site (http://idris-lang.org/

116++ The IDRIS web site (https://idris-lang.org/

117117

118118+ The IRC channel #idris, on chat.freenode.net

119119

src/IRTS/Portable.hs+1

@@ -265,6 +265,7 @@ instance ToJSON BC where

265265 toJSON (FOREIGNCALL r fd ret exps) = object ["FOREIGNCALL" .= (r, fd, ret, exps)]

266266 toJSON (SLIDE i) = object ["SLIDE" .= i]

267267 toJSON (RESERVE i) = object ["RESERVE" .= i]

268+ toJSON (RESERVENOALLOC i) = object ["RESERVENOALLOC" .= i]

268269 toJSON (ADDTOP i) = object ["ADDTOP" .= i]

269270 toJSON (TOPBASE i) = object ["TOPBASE" .= i]

270271 toJSON (BASETOP i) = object ["BASETOP" .= i]

src/Idris/CmdOptions.hs+1−1

@@ -72,7 +72,7 @@ runArgParser = do opts <- execParser $ info parser

7272 PP.empty,

7373 PP.text "More details over Idris can be found online here:",

7474 PP.empty,

75− PP.indent 4 (PP.text "http://www.idris-lang.org/")]

75+ PP.indent 4 (PP.text "https://www.idris-lang.org/")]

7676

7777execArgParserPure :: [String] -> ParserResult [Opt]

7878execArgParserPure args = preProcOpts <$> execParserPure (prefs idm) (info parser idm) args

src/Idris/ModeCommon.hs+1−1

@@ -167,7 +167,7 @@ loadInputs inputs toline -- furthest line to read in input source files

167167banner = " ____ __ _ \n" ++

168168 " / _/___/ /____(_)____ \n" ++

169169 " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++

170− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

170+ " _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" ++

171171 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++

172172 "\n" ++

173173 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++

test/pkg001/test-pkg.ipkg+3−3

@@ -12,6 +12,6 @@ license = BSD3 but see LICENSE for more information

1212brief = "This is a test package."

1313readme = README.md

1414version = 1234

15−homepage = http://www.idris-lang.org

16−sourceloc = http://ww.github.com/idris-lang/Idris-Dev

17−bugtracker = http://ww.github.com/idris-lang/Idris-Dev/issues

15+homepage = https://www.idris-lang.org

16+sourceloc = https://www.github.com/idris-lang/Idris-Dev

17+bugtracker = https://www.github.com/idris-lang/Idris-Dev/issues