b2dd4bc...master · Idris-dev

git.iko.soy/Idris-dev

617 files changed+2178−968

since splitsnapshots

unifiedsplit

.travis.yml+53−35

@@ -1,5 +1,4 @@

1−dist: trusty

2−sudo: false

1+dist: xenial

43language: c

@@ -9,35 +8,37 @@ env:

109matrix:

1110 include:

12− - env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="14.15" STYLISH=YES

11+ - env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="15.4" STYLISH=YES

1312 addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.5,hscolour], sources: [hvr-ghc]}}

14− - env: CABALVER="2.2" GHCVER="7.10.3" TESTS="test_c"

15− compiler: ": #GHC 7.10.3"

16− addons: {apt: {packages: [cabal-install-2.2,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}

17−# Disabled because it's always timing out

18−# - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"

19−# compiler: ": #GHC 8.0.1"

20−# addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}

21− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="lib_doc doc"

13+ - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="lib_doc doc"

2214 compiler: ": #GHC 8.2.2"

23− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

24− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_js"

15+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

16+ - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_js"

2517 compiler: ": #GHC 8.2.2"

26− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

27− - env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_c"

18+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

19+ - env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_c"

2820 compiler: ": #GHC 8.2.2"

29− addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

30−#TODO: The idris built with those fails due to libffi dynamic linking version mismatch.

31−# Caused by the GHC backport to Trusty?

32−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="lib_doc doc"

33−# compiler: ": #GHC 8.4.1"

34−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

35−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_js"

36−# compiler: ": #GHC 8.4.1"

37−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

38−# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_c"

39−# compiler: ": #GHC 8.4.1"

40−# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}

21+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}

22+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="lib_doc doc"

23+ compiler: ": #GHC 8.4.4"

24+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

25+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="test_js"

26+ compiler: ": #GHC 8.4.4"

27+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

28+ - env: CABALVER="2.4" GHCVER="8.4.4" TESTS="test_c"

29+ compiler: ": #GHC 8.4.4"

30+ addons: {apt: {packages: [cabal-install-2.4,ghc-8.4.4,cppcheck,hscolour], sources: [hvr-ghc]}}

31+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="lib_doc doc"

32+ compiler: ": #GHC 8.8.3"

33+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

34+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="test_js"

35+ compiler: ": #GHC 8.8.3"

36+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

37+ - env: CABALVER="3.0" GHCVER="8.8.3" TESTS="test_c"

38+ compiler: ": #GHC 8.8.3"

39+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3,cppcheck,hscolour], sources: [hvr-ghc]}}

40+ - env: CABALVER="3.0" GHCVER="8.8.3" IDRIS2=YES

41+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.3], sources: [hvr-ghc]}}

4142 fast-finish: true

4243

4344cache:

@@ -56,7 +57,7 @@ before_install:

5657 - unset CC

5758 - if [[ $TRAVIS_OS_NAME == 'linux' ]];

5859 then

59− export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$PATH;

60+ export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$HOME/.cabal/bin:$HOME/opt/scheme/bin/:$PATH;

6061 export SED=sed;

6162 export ZCAT=zcat;

6263 fi

@@ -71,6 +72,21 @@ before_install:

7172 export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:$PKG_CONFIG_PATH;

7273 fi

7374 - if [ -n "$STYLISH" ]; then ./stylize.sh; exit $?; fi

75+ - if [ -n "$IDRIS2" ];

76+ then

77+ git clone https://github.com/edwinb/Idris2 &&

78+ wget https://github.com/cisco/ChezScheme/archive/v9.5.2.tar.gz &&

79+ tar xvzf v9.5.2.tar.gz &&

80+ cd ChezScheme-9.5.2 &&

81+ ./configure --threads --installprefix=$HOME/opt/scheme &&

82+ make -j install &&

83+ cd .. &&

84+ cabal v1-update &&

85+ travis_wait cabal v1-install &&

86+ cd Idris2 &&

87+ make idris2 && make base && make contrib;

88+ exit $?;

89+ fi

7490

7591install:

7692 - which cabal

@@ -88,7 +104,7 @@ install:

88104 # causing cabal's default configuration (jobs: $ncpus)

89105 # to run into the GHC #9221 bug which can result in longer build-times.

90106 - $SED -i -r 's/(^jobs:).*/\1 2/' $HOME/.cabal/config

91− - cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt

107+ - cabal v1-install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt

92108 - $SED -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt

93109 # check whether current requested install-plan matches cached package-db snapshot

94110 - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;

@@ -101,7 +117,7 @@ install:

101117 echo "cabal build-cache MISS";

102118 rm -rf $HOME/.cabsnap;

103119 mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;

104− cabal install -f FFI --only-dependencies --enable-tests;

120+ cabal v1-install -f FFI --only-dependencies --enable-tests;

105121 fi

106122 # snapshot package-db on cache miss

107123 - if [ ! -d $HOME/.cabsnap ];

@@ -112,28 +128,30 @@ install:

112128 cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;

113129 fi

114130

131+

115132before_script:

116133 - ORIGINAL_DIR=$(pwd)

117− - cabal sdist

134+ - cabal v1-sdist

118135 - cd ..

119136 - tar -xf ${ORIGINAL_DIR}/dist/${PKGNAME}*.tar.gz

120137 - cd ${PKGNAME}*

121138script:

139+ - export LD_PRELOAD=/opt/ghc/${GHCVER}/lib/ghc-${GHCVER}/rts/libffi.so.7

122140###

123141 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'

124− - cabal configure -f FFI -f CI --enable-tests

142+ - cabal v1-configure -f FFI -f CI --enable-tests

125143 - echo -en 'travis_fold:end:script.configure\\r'

126144###

127145 - echo 'Build...' && echo -en 'travis_fold:start:script.build\\r'

128− - cabal build

146+ - cabal v1-build

129147 - echo -en 'travis_fold:end:script.build\\r'

130148###

131149 - echo 'Copy...' && echo -en 'travis_fold:start:script.copy\\r'

132− - cabal copy

150+ - cabal v1-copy

133151 - echo -en 'travis_fold:end:script.copy\\r'

134152###

135153 - echo 'Register...' && echo -en 'travis_fold:start:script.register\\r'

136− - cabal register

154+ - cabal v1-register

137155 - echo -en 'travis_fold:end:script.register\\r'

138156###

139157 - echo 'Cppcheck...' && echo -en 'travis_fold:start:script.cppcheck\\r'

CHANGELOG.md+3

@@ -1,3 +1,6 @@

1+# New since last release

2++ Updated to work with GHC 8.8 and cabal 3.0

14# New in 1.3.2

25+ Documentation added to proof section

INSTALL.md+11−2

@@ -130,7 +130,8 @@ PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig stack build

130130## Issue with GHC on Ubuntu/Fedora

131131

132132There is an upstream issue with GHC on some Ubuntu and Fedora machines.

133−The issue is that for GHC versions greater than 8.4.X linking to libFFI is broken.

133+The issue is that for GHC versions greater than 8.4.X linking to libFFI uses the version of libFFI shipped with GHC, instead of the system version.

134+

134135See the following GHC issue page for more information:

135136

136137 <https://gitlab.haskell.org/ghc/ghc/issues/15397>

@@ -141,4 +142,12 @@ Specifically, one will see an error message along the lines of:

141142

142143> error while loading shared libraries: libffi.so.7: cannot open shared object file: No such file or directory

143144

144−We have supplied an alternative stack configuration file (`stack-alt.yaml`) that will use a version of GHC prior to the upstream issue being introduced.

145+A workround for this bug is to override the used libffi version (this is what we use on CI):

146+

147+```bash

148+export LD_PRELOAD=/opt/ghc/${GHCVER}/lib/ghc-${GHCVER}/rts/libffi.so.7

149+```

150+

151+## GHC 8.6

152+

153+For reasons that haven't been investigated building the Idris compiler with GHC 8.6 leads to a compiler which doesn't pass test.

Makefile+4−4

@@ -30,15 +30,15 @@ stylize:

3030 ./stylize.sh

3131

3232test_c:

33− $(CABAL) test $(ARGS) --test-options \

33+ $(CABAL) v1-test $(ARGS) --test-options \

3434 "$(TEST-ARGS) --rerun-update +RTS -N$(TEST-JOBS) -RTS"

3535

3636test_js:

37− $(CABAL) test $(ARGS) --test-options \

37+ $(CABAL) v1-test $(ARGS) --test-options \

3838 "$(TEST-ARGS) --node --rerun-update +RTS -N$(TEST-JOBS) -RTS"

3939

4040test_update:

41− $(CABAL) test $(ARGS) --test-options \

41+ $(CABAL) v1-test $(ARGS) --test-options \

4242 "$(TEST-ARGS) --accept +RTS -N$(TEST-JOBS) -RTS"

4343

4444test_clean:

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

5656

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

5858doc: dist/setup-config

59− $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://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+3

@@ -44,3 +44,6 @@ where some interesting projects are being hosted.

4444

4545For those interested in contributing to Idris directly we kindly ask that

4646prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first.

47+

48+[Idris 2](https://github.com/edwinb/Idris2) is an early preview of the next generation

49+of Idris, implemented in Idris.

Setup.hs−33

@@ -215,36 +215,6 @@ idrisConfigure _ flags pkgdesc local = do

215215 autogenComponentModulesDir lbi _ = autogenModulesDir lbi

216216#endif

217217

218−idrisPreSDist args flags = do

219− let dir = S.fromFlag (S.sDistDirectory flags)

220− let verb = S.fromFlag (S.sDistVerbosity flags)

221− generateVersionModule verb "src" True

222− generateBuildFlagsModule verb "src" []

223− generateTargetModule verb "src" "./libs"

224− generateToolchainModule verb "src" Nothing

225− preSDist simpleUserHooks args flags

226−

227−idrisSDist sdist pkgDesc bi hooks flags = do

228− pkgDesc' <- addGitFiles pkgDesc

229− sdist pkgDesc' bi hooks flags

230− where

231− addGitFiles :: PackageDescription -> IO PackageDescription

232− addGitFiles pkgDesc = do

233− files <- gitFiles

234− return $ pkgDesc { extraSrcFiles = extraSrcFiles pkgDesc ++ files}

235− gitFiles :: IO [FilePath]

236− gitFiles = liftM lines (readProcess "git" ["ls-files"] "")

237−

238−idrisPostSDist args flags desc lbi = do

239− Control.Exception.catch (do let file = "src" </> "Version_idris" Px.<.> "hs"

240− let targetFile = "src" </> "Target_idris" Px.<.> "hs"

241− putStrLn $ "Removing generated modules:\n "

242− ++ file ++ "\n" ++ targetFile

243− removeFile file

244− removeFile targetFile)

245− (\e -> let e' = (e :: SomeException) in return ())

246− postSDist simpleUserHooks args flags desc lbi

247−

248218#if !(MIN_VERSION_Cabal(2,0,0))

249219rewriteFileEx :: Verbosity -> FilePath -> String -> IO ()

250220rewriteFileEx _ = rewriteFile

@@ -353,8 +323,5 @@ main = defaultMainWithHooks $ simpleUserHooks

353323 , postInst = \_ flags pkg local ->

354324 idrisInstall (S.fromFlag $ S.installVerbosity flags)

355325 NoCopyDest pkg local

356− , preSDist = idrisPreSDist

357− , sDistHook = idrisSDist (sDistHook simpleUserHooks)

358− , postSDist = idrisPostSDist

359326 , testHook = idrisTestHook

360327 }

appveyor.yml+3−3

@@ -1,17 +1,17 @@

11version: 1.0.{build}

22init:

33- ps: >-

4− choco install cabal --version=2.4.1.0 --no-progress

4+ choco install cabal --no-progress

66 mkdir C:\ghc

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"

8+ Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.8.2/ghc-8.8.2-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

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

1313

14− $env:PATH="$env:PATH;c:\ghc\ghc-8.4.3\bin;$HOME\AppData\Roaming\cabal\bin"

14+ $env:PATH="$env:PATH;c:\ghc\ghc-8.8.2\bin;$HOME\AppData\Roaming\cabal\bin"

1515

1616 cabal v1-update

1717

docs/conf.py+3−2

@@ -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

@@ -251,6 +251,7 @@ latex_elements = {

251251# Additional stuff for the LaTeX preamble.

252252'preamble': r'''

253253\usepackage{lmodern}

254+\usepackage{textalpha}

254255\usepackage[T1]{fontenc}

255256\usepackage[utf8x]{inputenc}

256257\usepackage{titlesec}

@@ -300,7 +301,7 @@ latex_elements = {

300301# (source start file, target name, title,

301302# author, documentclass [howto, manual, or own class]).

302303latex_documents = [

303− ('index', 'idris-documentation-complete.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report'),

304+ # (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')

304305 ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),

305306]

306307

docs/effects/introduction.rst+2−1

@@ -17,7 +17,8 @@ exceptions, and verified resource management.

1717This tutorial assumes familiarity with pure programming in Idris,

1818as described in Sections 1–6 of the main tutorial [1]_. The examples

1919presented are tested with Idris and can be found in the

20−examples directory of the Idris repository.

20+examples directory of the Idris repository. The ``-p effects`` flag

21+is needed when starting Idris.

2122

2223Consider, for example, the following introductory function which

2324illustrates the kind of properties which can be expressed in the type

docs/image/parserModules.png

Binary file not shown.

docs/image/parserModules.svg+413−316

@@ -15,9 +15,127 @@

1515 version="1.1"

1616 id="svg8"

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

18− sodipodi:docname="modules.svg">

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

1919 <defs

2020 id="defs2">

21+ <marker

22+ inkscape:isstock="true"

23+ style="overflow:visible;"

24+ id="marker1078"

25+ refX="0.0"

26+ refY="0.0"

27+ orient="auto"

28+ inkscape:stockid="Arrow1Mend">

29+ <path

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

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

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

33+ id="path1076" />

34+ </marker>

35+ <marker

36+ inkscape:isstock="true"

37+ style="overflow:visible"

38+ id="marker1074"

39+ refX="0.0"

40+ refY="0.0"

41+ orient="auto"

42+ inkscape:stockid="Arrow1Mstart">

43+ <path

44+ transform="scale(0.4) translate(10,0)"

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

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

47+ id="path1072" />

48+ </marker>

49+ <marker

50+ inkscape:stockid="Arrow1Mend"

51+ orient="auto"

52+ refY="0.0"

53+ refX="0.0"

54+ id="marker1021"

55+ style="overflow:visible;"

56+ inkscape:isstock="true"

57+ inkscape:collect="always">

58+ <path

59+ id="path1019"

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

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

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

63+ </marker>

64+ <marker

65+ inkscape:stockid="Arrow1Mstart"

66+ orient="auto"

67+ refY="0.0"

68+ refX="0.0"

69+ id="marker1017"

70+ style="overflow:visible"

71+ inkscape:isstock="true"

72+ inkscape:collect="always">

73+ <path

74+ id="path1015"

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

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

77+ transform="scale(0.4) translate(10,0)" />

78+ </marker>

79+ <marker

80+ inkscape:isstock="true"

81+ style="overflow:visible;"

82+ id="marker973"

83+ refX="0.0"

84+ refY="0.0"

85+ orient="auto"

86+ inkscape:stockid="Arrow1Mend"

87+ inkscape:collect="always">

88+ <path

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

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

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

92+ id="path971" />

93+ </marker>

94+ <marker

95+ inkscape:isstock="true"

96+ style="overflow:visible"

97+ id="marker969"

98+ refX="0.0"

99+ refY="0.0"

100+ orient="auto"

101+ inkscape:stockid="Arrow1Mstart"

102+ inkscape:collect="always">

103+ <path

104+ transform="scale(0.4) translate(10,0)"

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

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

107+ id="path967" />

108+ </marker>

109+ <marker

110+ inkscape:stockid="Arrow1Mend"

111+ orient="auto"

112+ refY="0.0"

113+ refX="0.0"

114+ id="Arrow1Mend"

115+ style="overflow:visible;"

116+ inkscape:isstock="true"

117+ inkscape:collect="always">

118+ <path

119+ id="path1214"

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

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

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

123+ </marker>

124+ <marker

125+ inkscape:stockid="Arrow1Mstart"

126+ orient="auto"

127+ refY="0.0"

128+ refX="0.0"

129+ id="Arrow1Mstart"

130+ style="overflow:visible"

131+ inkscape:isstock="true"

132+ inkscape:collect="always">

133+ <path

134+ id="path1211"

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

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

137+ transform="scale(0.4) translate(10,0)" />

138+ </marker>

21139 <marker

22140 inkscape:isstock="true"

23141 style="overflow:visible;"

@@ -200,7 +318,7 @@

200318 inkscape:stockid="Arrow1Mend">

201319 <path

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

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

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

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

205323 id="path1001" />

206324 </marker>

@@ -216,7 +334,7 @@

216334 <path

217335 id="path995"

218336 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

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

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

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

221339 </marker>

222340 <marker

@@ -230,7 +348,7 @@

230348 inkscape:collect="always">

231349 <path

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

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

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

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

235353 id="path989" />

236354 </marker>

@@ -278,21 +396,6 @@

278396 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

279397 id="path3615" />

280398 </marker>

281− <marker

282− inkscape:stockid="Arrow1Mend"

283− orient="auto"

284− refY="0.0"

285− refX="0.0"

286− id="marker2891"

287− style="overflow:visible;"

288− inkscape:isstock="true"

289− inkscape:collect="always">

290− <path

291− id="path2889"

292− d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

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

294− transform="scale(0.4) rotate(180) translate(10,0)" />

295− </marker>

296399 <marker

297400 inkscape:stockid="Arrow1Mend"

298401 orient="auto"

@@ -323,21 +426,6 @@

323426 d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

324427 id="path1537" />

325428 </marker>

326− <marker

327− inkscape:stockid="Arrow1Mend"

328− orient="auto"

329− refY="0.0"

330− refX="0.0"

331− id="Arrow1Mend"

332− style="overflow:visible;"

333− inkscape:isstock="true"

334− inkscape:collect="always">

335− <path

336− id="path830"

337− d="M 0.0,0.0 L 5.0,-5.0 L -12.5,0.0 L 5.0,5.0 L 0.0,0.0 z "

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

339− transform="scale(0.4) rotate(180) translate(10,0)" />

340− </marker>

341429 </defs>

342430 <sodipodi:namedview

343431 id="base"

@@ -348,15 +436,16 @@

348436 inkscape:pageshadow="2"

349437 inkscape:zoom="1"

350438 inkscape:cx="368.33949"

351− inkscape:cy="554.8721"

439+ inkscape:cy="547.05121"

352440 inkscape:document-units="mm"

353441 inkscape:current-layer="layer1"

354442 showgrid="false"

355− inkscape:window-width="1359"

443+ inkscape:window-width="1800"

356444 inkscape:window-height="1011"

357− inkscape:window-x="-4"

445+ inkscape:window-x="86"

358446 inkscape:window-y="0"

359− inkscape:window-maximized="0" />

447+ inkscape:window-maximized="0"

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

360449 <metadata

361450 id="metadata5">

362451 <rdf:RDF>

@@ -373,157 +462,6 @@

373462 inkscape:label="Layer 1"

374463 inkscape:groupmode="layer"

375464 id="layer1">

376− <rect

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

378− id="rect815"

379− width="35.983334"

380− height="18.25625"

381− x="37.835415"

382− y="52.260437"

383− inkscape:export-xdpi="61.120499"

384− inkscape:export-ydpi="61.120499" />

385− <rect

386− y="52.260437"

387− x="92.868744"

388− height="18.25625"

389− width="35.983334"

390− id="rect817"

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

392− inkscape:export-xdpi="61.120499"

393− inkscape:export-ydpi="61.120499" />

394− <path

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

396− d="m 74.083333,61.25627 16.66875,-0.26459"

397− id="path819"

398− inkscape:connector-curvature="0"

399− inkscape:export-xdpi="61.120499"

400− inkscape:export-ydpi="61.120499" />

401− <path

402− inkscape:connector-curvature="0"

403− id="path1535"

404− d="m 19.314583,61.520853 16.66875,-0.26459"

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

406− inkscape:export-xdpi="61.120499"

407− inkscape:export-ydpi="61.120499" />

408− <path

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

410− d="m 128.85208,60.991686 16.66875,-0.26459"

411− id="path2045"

412− inkscape:connector-curvature="0"

413− inkscape:export-xdpi="61.120499"

414− inkscape:export-ydpi="61.120499" />

415− <text

416− xml:space="preserve"

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

418− x="20.902082"

419− y="58.345871"

420− id="text2857"

421− inkscape:export-xdpi="61.120499"

422− inkscape:export-ydpi="61.120499"><tspan

423− sodipodi:role="line"

424− id="tspan2855"

425− x="20.902082"

426− y="58.345871"

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

428− <text

429− id="text2861"

430− y="53.583374"

431− x="76.729164"

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

433− xml:space="preserve"

434− inkscape:export-xdpi="61.120499"

435− inkscape:export-ydpi="61.120499"><tspan

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

437− y="53.583374"

438− x="76.729164"

439− sodipodi:role="line"

440− id="tspan2867">List</tspan><tspan

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

442− y="58.875042"

443− x="76.729164"

444− sodipodi:role="line"

445− id="tspan2871">Token</tspan></text>

446− <text

447− xml:space="preserve"

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

449− x="131.49791"

450− y="57.816704"

451− id="text2865"

452− inkscape:export-xdpi="61.120499"

453− inkscape:export-ydpi="61.120499"><tspan

454− sodipodi:role="line"

455− id="tspan2863"

456− x="131.49791"

457− y="57.816704"

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

459− <text

460− id="text2875"

461− y="62.050041"

462− x="47.889584"

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

464− xml:space="preserve"

465− inkscape:export-xdpi="61.120499"

466− inkscape:export-ydpi="61.120499"><tspan

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

468− y="62.050041"

469− x="47.889584"

470− id="tspan2873"

471− sodipodi:role="line">Lexer</tspan></text>

472− <text

473− xml:space="preserve"

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

475− x="100.80624"

476− y="61.785461"

477− id="text2879"

478− inkscape:export-xdpi="61.120499"

479− inkscape:export-ydpi="61.120499"><tspan

480− sodipodi:role="line"

481− id="tspan2877"

482− x="100.80624"

483− y="61.785461"

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

485− <path

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

487− d="m 53.445833,44.322936 v 7.67291"

488− id="path2887"

489− inkscape:connector-curvature="0"

490− sodipodi:nodetypes="cc"

491− inkscape:export-xdpi="61.120499"

492− inkscape:export-ydpi="61.120499" />

493− <path

494− sodipodi:nodetypes="cc"

495− inkscape:connector-curvature="0"

496− id="path3613"

497− d="m 109.27292,44.322936 v 7.67291"

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

499− inkscape:export-xdpi="61.120499"

500− inkscape:export-ydpi="61.120499" />

501− <text

502− id="text4173"

503− y="42.735458"

504− x="43.920834"

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

506− xml:space="preserve"

507− inkscape:export-xdpi="61.120499"

508− inkscape:export-ydpi="61.120499"><tspan

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

510− y="42.735458"

511− x="43.920834"

512− id="tspan4171"

513− sodipodi:role="line">Recogniser</tspan></text>

514− <text

515− xml:space="preserve"

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

517− x="97.631248"

518− y="42.470879"

519− id="text4177"

520− inkscape:export-xdpi="61.120499"

521− inkscape:export-ydpi="61.120499"><tspan

522− sodipodi:role="line"

523− id="tspan4175"

524− x="97.631248"

525− y="42.470879"

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

527465 <text

528466 inkscape:export-ydpi="61.120499"

529467 inkscape:export-xdpi="61.120499"

@@ -645,15 +583,15 @@

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

646584 <text

647585 id="text931"

648− y="184.2872"

649− x="37.041664"

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

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

651589 xml:space="preserve"

652590 inkscape:export-xdpi="61.120499"

653591 inkscape:export-ydpi="61.120499"><tspan

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

655− y="184.2872"

656− x="37.041664"

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"

657595 id="tspan929"

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

659597 <text

@@ -672,21 +610,21 @@

672610 <rect

673611 inkscape:export-ydpi="61.120499"

674612 inkscape:export-xdpi="61.120499"

675− y="180.05362"

676− x="32.543747"

613+ y="214.18488"

614+ x="32.01458"

677615 height="6.3500061"

678616 width="43.656254"

679617 id="rect937"

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

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

681619 <rect

682620 inkscape:export-ydpi="61.120499"

683621 inkscape:export-xdpi="61.120499"

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

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"

685623 id="rect939"

686624 width="42.862495"

687625 height="6.8791728"

688− x="95.51458"

689− y="180.05362" />

626+ x="94.985413"

627+ y="214.18488" />

690628 <text

691629 inkscape:export-ydpi="61.120499"

692630 inkscape:export-xdpi="61.120499"

@@ -706,33 +644,33 @@

706644 inkscape:export-xdpi="61.120499"

707645 inkscape:connector-curvature="0"

708646 id="path963"

709− d="m 53.828728,179.89081 1.006873,-18.52084"

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

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

711649 <text

712650 inkscape:export-ydpi="61.120499"

713651 inkscape:export-xdpi="61.120499"

714652 xml:space="preserve"

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

716− x="23.749693"

717− y="216.88524"

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"

718656 id="text971"><tspan

719657 sodipodi:role="line"

720658 id="tspan969"

721− x="23.749693"

722− y="216.88524"

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

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>

724662 <rect

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

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

726664 id="rect973"

727665 width="47.889587"

728666 height="6.3500061"

729− x="22.162193"

730− y="212.38707"

667+ x="21.633026"

668+ y="246.51833"

731669 inkscape:export-xdpi="61.120499"

732670 inkscape:export-ydpi="61.120499" />

733671 <path

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

735− d="m 48.898483,194.70748 0.04943,-6.71548"

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"

736674 id="path975"

737675 inkscape:connector-curvature="0"

738676 inkscape:export-xdpi="61.120499"

@@ -740,46 +678,46 @@

740678 sodipodi:nodetypes="cc" />

741679 <text

742680 id="text979"

743− y="207.83517"

744− x="23.812496"

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

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

746684 xml:space="preserve"

747685 inkscape:export-xdpi="61.120499"

748686 inkscape:export-ydpi="61.120499"><tspan

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

750− y="207.83517"

751− x="23.812496"

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"

752690 id="tspan977"

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

754692 <rect

755693 inkscape:export-ydpi="61.120499"

756694 inkscape:export-xdpi="61.120499"

757− y="203.33701"

758− x="22.224997"

695+ y="237.46826"

696+ x="21.695829"

759697 height="6.2469702"

760698 width="43.853985"

761699 id="rect981"

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

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

763701 <text

764702 inkscape:export-ydpi="61.120499"

765703 inkscape:export-xdpi="61.120499"

766704 xml:space="preserve"

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

768− x="23.711607"

769− y="199.55397"

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"

770708 id="text985"><tspan

771709 sodipodi:role="line"

772710 id="tspan983"

773− x="23.711607"

774− y="199.55397"

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

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>

776714 <rect

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

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

778716 id="rect987"

779717 width="39.011257"

780718 height="5.9464455"

781− x="22.124107"

782− y="195.0558"

719+ x="21.59494"

720+ y="229.18706"

783721 inkscape:export-xdpi="61.120499"

784722 inkscape:export-ydpi="61.120499" />

785723 <path

@@ -788,11 +726,11 @@

788726 inkscape:export-xdpi="61.120499"

789727 inkscape:connector-curvature="0"

790728 id="path993"

791− d="M 63.527551,202.87958 63.375204,187.79022"

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

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

793731 <path

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

795− d="M 67.865826,212.16147 67.612589,187.58844"

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"

796734 id="path999"

797735 inkscape:connector-curvature="0"

798736 inkscape:export-xdpi="61.120499"

@@ -800,7 +738,7 @@

800738 sodipodi:nodetypes="cc" />

801739 <path

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

803− d="M 74.466241,179.89081 95.51458,173.43977"

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

804742 id="path1005"

805743 inkscape:connector-curvature="0"

806744 inkscape:export-xdpi="61.120499"

@@ -808,7 +746,7 @@

808746 sodipodi:nodetypes="cc" />

809747 <path

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

811− d="m 113.36007,180.68456 -0.0515,-6.61459"

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

812750 id="path1011"

813751 inkscape:connector-curvature="0"

814752 inkscape:export-xdpi="61.120499"

@@ -818,13 +756,13 @@

818756 inkscape:export-ydpi="61.120499"

819757 inkscape:export-xdpi="61.120499"

820758 id="text1019"

821− y="184.81636"

822− x="97.366661"

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

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

824762 xml:space="preserve"><tspan

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

826− y="184.81636"

827− x="97.366661"

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"

828766 id="tspan1017"

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

830768 <path

@@ -910,68 +848,68 @@

910848 id="rect1061"

911849 width="59.266659"

912850 height="16.13958"

913− x="92.339577"

914− y="230.5896" />

851+ x="97.102074"

852+ y="186.93335" />

915853 <path

916854 inkscape:export-ydpi="61.120499"

917855 inkscape:export-xdpi="61.120499"

918856 inkscape:connector-curvature="0"

919857 id="path1063"

920− d="m 76.993749,160.21044 21.695834,69.32083"

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

921859 style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1105)"

922860 sodipodi:nodetypes="cc" />

923861 <text

924862 inkscape:export-ydpi="61.120499"

925863 inkscape:export-xdpi="61.120499"

926864 id="text1081"

927− y="236.14587"

928− x="153.19336"

865+ y="192.48962"

866+ x="157.95586"

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

930868 xml:space="preserve"><tspan

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

932− y="236.14587"

933− x="153.19336"

870+ y="192.48962"

871+ x="157.95586"

934872 id="tspan1079"

935− sodipodi:role="line">Either ParseError SExp</tspan></text>

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

936874 <text

937875 inkscape:export-ydpi="61.120499"

938876 inkscape:export-xdpi="61.120499"

939877 id="text1089"

940− y="236.41046"

941− x="94.191658"

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

878+ y="192.75421"

879+ x="98.954155"

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

943881 xml:space="preserve"><tspan

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

945− y="236.41046"

946− x="94.191658"

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

883+ y="192.75421"

884+ x="98.954155"

947885 id="tspan1087"

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

949887 <rect

950888 inkscape:export-ydpi="61.120499"

951889 inkscape:export-xdpi="61.120499"

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

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

953891 id="rect1097"

954− width="35.983334"

955− height="18.25625"

956− x="124.08953"

957− y="18.393738" />

892+ width="55.033333"

893+ height="14.287498"

894+ x="20.637447"

895+ y="52.524986" />

958896 <text

959897 inkscape:export-ydpi="61.120499"

960898 inkscape:export-xdpi="61.120499"

961899 id="text1101"

962− y="24.479179"

963− x="126.99989"

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

900+ y="58.610428"

901+ x="23.54781"

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

965903 xml:space="preserve"><tspan

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

967− y="24.479179"

968− x="126.99989"

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

905+ y="58.610428"

906+ x="23.54781"

969907 id="tspan1099"

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

971909 <path

972910 sodipodi:nodetypes="cc"

973911 style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1111)"

974− d="m 112.97708,187.46252 0.52917,41.80417"

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

975913 id="path1107"

976914 inkscape:connector-curvature="0"

977915 inkscape:export-xdpi="61.120499"

@@ -981,7 +919,7 @@

981919 inkscape:export-xdpi="61.120499"

982920 inkscape:connector-curvature="0"

983921 id="path1113"

984− d="m 144.72708,173.43925 -0.26458,56.35661"

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

985923 style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1117)"

986924 sodipodi:nodetypes="cc" />

987925 <path

@@ -989,27 +927,27 @@

989927 inkscape:export-xdpi="61.120499"

990928 inkscape:connector-curvature="0"

991929 id="path1119"

992− d="m 151.80639,239.22321 44.91435,-0.41532"

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

993931 style="fill:none;stroke:#00aa3f;stroke-width:0.70555556;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1123)"

994932 sodipodi:nodetypes="cc" />

995933 <text

996934 id="text950"

997− y="236.19983"

998− x="22.69136"

935+ y="104.70191"

936+ x="22.426785"

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

1000938 xml:space="preserve"

1001939 inkscape:export-xdpi="61.120499"

1002940 inkscape:export-ydpi="61.120499"><tspan

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

1004− y="236.19983"

1005− x="22.69136"

942+ y="104.70191"

943+ x="22.426785"

1006944 id="tspan948"

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

1008946 <rect

1009947 inkscape:export-ydpi="61.120499"

1010948 inkscape:export-xdpi="61.120499"

1011− y="231.70166"

1012− x="21.103861"

949+ y="100.20374"

950+ x="20.839275"

1013951 height="9.7895899"

1014952 width="47.889587"

1015953 id="rect952"

@@ -1019,57 +957,57 @@

1019957 inkscape:export-xdpi="61.120499"

1020958 xml:space="preserve"

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

1022− x="23.220528"

1023− y="239.90399"

960+ x="22.955944"

961+ y="108.40608"

1024962 id="text956"><tspan

1025963 sodipodi:role="line"

1026964 id="tspan954"

1027− x="23.220528"

1028− y="239.90399"

965+ x="22.955944"

966+ y="108.40608"

1029967 style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52777767px;font-family:sans-serif;-inkscape-font-specification:'sans-serif Bold';fill:#000000;stroke-width:0.26458332">error messages</tspan></text>

1030968 <text

1031969 inkscape:export-ydpi="61.120499"

1032970 inkscape:export-xdpi="61.120499"

1033971 xml:space="preserve"

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

1035− x="22.69136"

1036− y="252.33942"

973+ x="79.312202"

974+ y="92.266502"

1037975 id="text960"><tspan

1038976 sodipodi:role="line"

1039977 id="tspan958"

1040− x="22.69136"

1041− y="252.33942"

978+ x="79.312202"

979+ y="92.266502"

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

1043981 <rect

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

1045983 id="rect962"

1046984 width="61.912495"

1047985 height="18.785419"

1048− x="21.103861"

1049− y="247.84125"

986+ x="77.724693"

987+ y="87.768333"

1050988 inkscape:export-xdpi="61.120499"

1051989 inkscape:export-ydpi="61.120499" />

1052990 <text

1053991 id="text966"

1054− y="256.04358"

1055− x="23.220528"

992+ y="95.970665"

993+ x="79.841362"

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

1057995 xml:space="preserve"

1058996 inkscape:export-xdpi="61.120499"

1059997 inkscape:export-ydpi="61.120499"><tspan

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

1061− y="256.04358"

1062− x="23.220528"

999+ y="95.970665"

1000+ x="79.841362"

10631001 sodipodi:role="line"

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

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

1066− y="260.45331"

1067− x="23.220528"

1004+ y="100.38039"

1005+ x="79.841362"

10681006 sodipodi:role="line"

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

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

1071− y="264.86304"

1072− x="23.220528"

1009+ y="104.79011"

1010+ x="79.841362"

10731011 sodipodi:role="line"

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

10751013 <text

@@ -1077,54 +1015,54 @@

10771015 inkscape:export-xdpi="61.120499"

10781016 xml:space="preserve"

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

1080− x="22.69136"

1081− y="90.151314"

1018+ x="22.162193"

1019+ y="73.217979"

10821020 id="text978"><tspan

10831021 sodipodi:role="line"

10841022 id="tspan976"

1085− x="22.69136"

1086− y="90.151314"

1023+ x="22.162193"

1024+ y="73.217979"

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

10881026 <rect

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

10901028 id="rect980"

10911029 width="55.827087"

10921030 height="10.054173"

1093− x="21.103861"

1094− y="85.653076"

1031+ x="20.574694"

1032+ y="68.719742"

10951033 inkscape:export-xdpi="61.120499"

10961034 inkscape:export-ydpi="61.120499" />

10971035 <text

10981036 id="text984"

1099− y="93.855484"

1100− x="23.220528"

1037+ y="76.92215"

1038+ x="22.69136"

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

11021040 xml:space="preserve"

11031041 inkscape:export-xdpi="61.120499"

11041042 inkscape:export-ydpi="61.120499"><tspan

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

1106− y="93.855484"

1107− x="23.220528"

1044+ y="76.92215"

1045+ x="22.69136"

11081046 id="tspan982"

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

11101048 <text

11111049 id="text988"

1112− y="106.82006"

1113− x="22.69136"

1050+ y="89.886726"

1051+ x="22.162193"

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

11151053 xml:space="preserve"

11161054 inkscape:export-xdpi="61.120499"

11171055 inkscape:export-ydpi="61.120499"><tspan

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

1119− y="106.82006"

1120− x="22.69136"

1057+ y="89.886726"

1058+ x="22.162193"

11211059 id="tspan986"

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

11231061 <rect

11241062 inkscape:export-ydpi="61.120499"

11251063 inkscape:export-xdpi="61.120499"

1126− y="102.32182"

1127− x="21.103861"

1064+ y="85.388489"

1065+ x="20.574694"

11281066 height="9.5250101"

11291067 width="37.835419"

11301068 id="rect990"

@@ -1134,21 +1072,180 @@

11341072 inkscape:export-xdpi="61.120499"

11351073 xml:space="preserve"

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

1137− x="23.220528"

1138− y="110.52423"

1075+ x="22.69136"

1076+ y="93.590897"

11391077 id="text994"><tspan

11401078 sodipodi:role="line"

11411079 id="tspan992"

1142− x="23.220528"

1143− y="110.52423"

1080+ x="22.69136"

1081+ y="93.590897"

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

11451083 <path

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

1147− d="m 21.103861,231.70166 c -7.32197,0.078 -4.584313,-108.27557 0,-119.85483"

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

11481086 id="path996"

11491087 inkscape:connector-curvature="0"

11501088 inkscape:export-xdpi="61.120499"

11511089 inkscape:export-ydpi="61.120499"

11521090 sodipodi:nodetypes="cc" />

1091+ <path

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

1093+ d="M 15.081249,210.48125 H 200.02499"

1094+ id="path1201"

1095+ inkscape:connector-curvature="0"

1096+ sodipodi:nodetypes="cc"

1097+ inkscape:export-xdpi="61.120499"

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

1099+ <path

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

1101+ d="m 154.78125,214.97917 -0.26459,40.21666"

1102+ id="path1203"

1103+ inkscape:connector-curvature="0"

1104+ inkscape:export-xdpi="61.120499"

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

1106+ <text

1107+ xml:space="preserve"

1108+ style="font-style:normal;font-weight:normal;font-size:10.58333302px;line-height:0.40000001;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#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>

11531250 </g>

11541251</svg>

docs/parserLibrary/index.rst+1

@@ -21,3 +21,4 @@ A tutorial on the lexer and parser library in Idris.

2121 introduction

2222 lexer

2323 parser

24+ whitespace

docs/parserLibrary/introduction.rst+52−12

@@ -4,7 +4,20 @@

44Parser Library Introduction

55***************************

7−The parser library is used in a similar way to Parsec which is a library for writing parsers in Haskell. It is based on higher-order parser combinators, so a complicated parser can be made out of many smaller ones.

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.

821

922.. list-table::

1023

@@ -12,25 +25,52 @@ The parser library is used in a similar way to Parsec which is a library for wri

1225 - Lexer - This takes the input string and turns it into a list of Tokens.

1326 - Parser - This takes the list of tokens and outputs the code.

1427

15−.. image:: ../image/parserTopLevel.png

16− :width: 484px

17− :height: 147px

18− :alt: diagram illustrating these stages of lexer and parser

28+ - .. image:: ../image/parserTopLevel.png

29+ :width: 307px

30+ :height: 76px

31+ :alt: diagram illustrating these stages of lexer and parser

1932

20−The advantage of using two stages, like this, is that things like whitespace and comments don't need to be considered in every parser rule.

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.

2135

22−The Idris parser library differs from Parsec in that you need to say in the Recogniser whether a rule is guaranteed to consume input. This means that the Idris type system prevents the construction of recognisers/rules that can't consume the input.

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.

2340

24−The Lexer is similar but works at the level of characters rather than tokens, and you need to provide a TokenMap which says how to build a token representation from a string when a rule is matched.

41+The Lexer is similar but works at the level of characters rather than tokens, and

42+you need to provide a TokenMap which defines how to build a token from

43+a string when a rule is matched.

2544

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.

2650

51+Parser Library and Idris 2

52+--------------------------

2753

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.

2858

29−.. image:: ../image/parserModules.png

30− :width: 484px

31− :height: 147px

32− :alt: diagram illustrating these stages of lexer and parser

59+Idris 2 has at least 3 compilers:

3360

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.

3466

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

3571

72+.. image:: ../image/parserModules.png

73+ :width: 460px

74+ :height: 496px

75+ :alt: diagram illustrating these stages of lexer and parser

3676

docs/parserLibrary/lexer.rst+78−30

@@ -1,3 +1,5 @@

1+.. _parserLibraryLexer:

13Lexer

24=====

@@ -8,13 +10,16 @@ module:

810

911 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

1012

11−This function takes a String and returns a list of tokens. With the tokens we have

12−indexes back to the original string which can be used in error messages:

13+.. list-table::

14+

15+ * - This function takes a String and returns a list of tokens. With the

16+ tokens we have indexes back to the original string which can be used

17+ in error messages:

1318

14−.. image:: ../image/tokenise.png

15− :width: 330px

16− :height: 73px

17− :alt: diagram illustrating these stages of lexer

19+ - .. image:: ../image/tokenise.png

20+ :width: 330px

21+ :height: 73px

22+ :alt: diagram illustrating these stages of lexer

1823

1924TokenMap

2025--------

@@ -24,28 +29,32 @@ In order to construct this list of tokens we need:

2429- A way to recognise the tokens in the input string.

2530- A way to construct these individual tokens.

2631

27−This is given by the TokenMap. This is a mapping from lexers to the tokens they produce. This is a list of pairs:

32+This is given by the TokenMap which is a list of pairs containing

33+this information:

2834

2935.. code-block:: idris

3036

3137 (Lexer, String -> tokenType)

3238

3339So for each Lexer in the list, if a substring in the input matches, run

34−the associated function to produce a token of type `tokenType`

40+the associated function to produce a token of type ``tokenType``

3541

36−from Text.Lexer.Core:

42+.. list-table::

3743

38−.. code-block:: idris

44+ * - from Text.Lexer.Core

45+ : https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer/Core.idr

3946

40− TokenMap : (tokenType : Type) -> Type

41− TokenMap tokenType = List (Lexer, String -> tokenType)

47+ - .. code-block:: idris

4248

43−We can create a tokenMap by using a function like this:

49+ TokenMap : (tokenType : Type) -> Type

50+ TokenMap tokenType = List (Lexer, String -> tokenType)

4451

45−.. code-block:: idris

52+ * - We can create a tokenMap by using a function like this:

53+

54+ - .. code-block:: idris

4655

47− myTokenMap : TokenMap Token

48− myTokenMap = [(is 'a',CharLit)]

56+ myTokenMap : TokenMap Token

57+ myTokenMap = [(is 'a',CharLit)]

4958

5059Once we have a TokenMap we can use it to lex many strings.

5160

@@ -55,7 +64,8 @@ Recognisers

5564The first part of each entry in the TokenMap is the recogniser.

5665

5766A simple recogniser is 'Pred' which uses a predicate (Char -> Bool) to

58−test whether to accept the character. It can be constructed using the 'is' function:

67+test whether to accept the character. It can be constructed using the

68+'is' function:

5969

6070.. code-block:: idris

6171

@@ -70,8 +80,8 @@ combined, for example,

7080

7181.. list-table::

7282

73− * - <+> means sequence two recognisers. If either consumes a character, the sequence

74− is guaranteed to consume a character.

83+ * - ``<+>`` means sequence two recognisers. If either consumes a character,

84+ the sequence is guaranteed to consume a character.

7585

7686 - .. code-block:: idris

7787

@@ -79,7 +89,7 @@ combined, for example,

7989 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

8090 (Delay (is 'b')) : Recognise True

8191

82− * - <|> means if both consume, the combination is guaranteed

92+ * - ``<|>`` means if both consume, the combination is guaranteed

8393 to consumer a character:

8494

8595 - .. code-block:: idris

@@ -96,11 +106,46 @@ This diagram shows the recogniser combinator with some of its constructors:

96106 :height: 249px

97107 :alt: recogniser data structure

98108

109+A recogniser consumes its input, that is it advances the index to its input

110+string, as it generates the token list. In some cases we don't want this to

111+happen, for instance, we may need to lookahead before consuming the input

112+string.

113+

114+If a recogniser does not consume input there is a danger of an infinite loop.

115+To prevent this the recogniser is dependent on a boolean called 'consumes' which

116+is true if the recogniser is guaranteed to consume at least one character.

117+

118+The constructors of Recognise allow us to ensure that, even though parts of

119+the recogniser may not consume, overall the recogniser will consume.

120+

121+Since 'Recognise True' is more common than 'Recognise False' it is convenient to

122+use 'Lexer' as a type synonym for 'Recognise True'.

123+

124+Whitespace and Comments

125+-----------------------

126+

127+An important reason to have a lexer is to simplify the parser when whitespace

128+or comments are required. Without this the parser would require a match for

129+every combination, with and without, whitespace and comments.

130+

131+In some languages the lexer needs to remove whitespace and comments so that

132+they don't appear in the token list. In some cases whitespace is significant

133+but a single whitespace token can stand for any number of spaces, tabs,

134+carriage returns and so on.

135+

136+In some cases, such as when parsing the Idris language itself, whitespace

137+is important to indicate blocks. In this case we might want to output a

138+start-of-block token when the indent increases and an end-of-block token

139+when the indent decreases.

140+

141+This topic will be discussed more fully on this page

142+:ref:`parserLibraryWhitespace`.

143+

99144Simple Expression Example for Lexer

100145-----------------------------------

101146

102−On this page we will implement a lexer to lex a very simple expression as

103−a running example, on the next page we will go on to implement a parser for it.

147+On this page we will implement a lexer to 'lex' a very simple expression as

148+a running example, on the next page, we will go on to implement a parser for it.

104149

105150First import the lexer and parser code:

106151

@@ -122,7 +167,7 @@ able to parse simple arithmetic expressions, like this:

122167so we need:

123168

124169- Numbers (for now integer literals are good enough).

125−- Some operators (for now '+', '-' and '*' will do.

170+- Some operators (for now ``+``, ``-`` and ``*`` will do.

126171- Opening and closing Parentheses.

127172

128173We can define these, as tokens, like this:

@@ -139,7 +184,7 @@ We can define these, as tokens, like this:

139184 | EndInput

140185

141186It may help with debugging and to implement error messages to

142−implement 'show' for these tokens:

187+implement ``show`` for these tokens:

143188

144189.. code-block:: idris

145190

@@ -155,11 +200,11 @@ implement 'show' for these tokens:

155200 Show (TokenData ExpressionToken) where

156201 show (MkToken l c t) = "line=" ++ show l ++ " col=" ++ show c ++ "tok=" ++ show t

157202

158−.. code-block:: idris

159−

160203The following defines the 'TokenMap' for this example:

161204

162− -- integer arithmetic operators plus, minus and multiply.

205+.. code-block:: idris

206+

207+ ||| integer arithmetic operators plus, minus and multiply.

163208 export

164209 opChars : String

165210 opChars = "+-*"

@@ -172,7 +217,7 @@ The following defines the 'TokenMap' for this example:

172217

173218 expressionTokens : TokenMap ExpressionToken

174219 expressionTokens =

175− [(digits, \x => Number (toInt' x)),

220+ [(digits, \x => Number (toInt' x)),

176221 (operator, \x => Operator x),

177222 (is '(' ,\x => OParen),

178223 (is ')' ,\x => CParen)]

@@ -229,7 +274,9 @@ input string as parameters:

229274 Int,

230275 String)

231276

232−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy. In the example the indexes have not been computed but we can pick out the tokens:

277+The lexer uses potentially infinite data structures. It has recursive

278+arguments (codata type) so code is lazy. In the output above the indexes

279+have not been computed but we can pick out the tokens:

233280

234281- (Number 1)

235282- (Operator "+")

@@ -237,4 +284,5 @@ The lexer uses potentially infinite data structures. It has recursive arguments

237284

238285So the code is working.

239286

240−A parser for this example will be constructed on the next page.

287+We can now go ahead and parse this token list. A parser for this example will

288+be constructed on the next page.

docs/parserLibrary/parser.rst+492−68

@@ -1,18 +1,31 @@

1+.. _parserLibraryParser:

13Parser

24======

4−On the previous page we implemented a lexer to lex a very simple expression, on this

5−page we will go on to implement a parser for it.

6−

7−To run our parser we call 'doParse'. This requires the output from the lexer (a list of tokens) and a Grammar.

6+To run the parser we call ``parse``. This requires a grammar and the output

7+from the lexer (which is a list of tokens).

99.. code-block:: idris

1010

11− doParse : {c : Bool} ->

12− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->

13− ParseResult xs c ty

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.

1425

15−So we need to define the Grammar for our parser

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.

1629

1730.. code-block:: idris

1831

@@ -40,27 +53,59 @@ So we need to define the Grammar for our parser

4053 Grammar tok c1 ty -> Grammar tok c2 ty ->

4154 Grammar tok (c1 && c2) ty

4255

56+So an example of a grammer type may look something like this:

57+``Grammar (TokenData ExpressionToken) True Integer``.

58+This is a complicated type name and a given parser will need to use it a lot.

59+So to reduce the amount of typing we can use the following type synonym (similar

60+to what is done in Idris 2

61+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

62+)

63+

4364.. code-block:: idris

4465

45− -- from Idris2/src/Parser/Support.idr

4666 public export

4767 Rule : Type -> Type

4868 Rule ty = Grammar (TokenData ExpressionToken) True ty

4969

50−.. code-block:: idris

70+Parser Example

71+--------------

5172

52− export

53− intLiteral : Rule Integer

54− intLiteral

55− = terminal --"Expected integer literal"

56− (\x => case tok x of

73+On the previous page we implemented a lexer to 'lex' a very simple expression, on

74+this page we will go on to add a parser for this running example.

75+

76+.. list-table::

77+

78+ * - The syntax we are aiming at is something

79+ like this (expressed in Backus–Naur form (BNF)):

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 numeric characters).

94+

95+ - .. code-block:: idris

96+

97+ export

98+ intLiteral : Rule Integer

99+ intLiteral

100+ = terminal (\x => case tok x of

57101 Number i => Just i

58102 _ => Nothing)

59103

60104In order to try this out, here is a temporary function, this calls

61105parse which takes two parameters:

62−* The grammar (in this case intLiteral)

63−* The token list from the lexer.

106+

107+- The grammar (in this case intLiteral)

108+- The token list from the lexer.

64109

65110.. code-block:: idris

66111

@@ -68,8 +113,8 @@ parse which takes two parameters:

68113 (Integer, List (TokenData ExpressionToken))

69114 test1 s = parse intLiteral (fst (lex expressionTokens s))

70115

71−As required, if we pass it a string which is a number literal then it will return the

72−number in the 'Right' option.

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.

73118

74119.. code-block:: idris

75120

@@ -97,27 +142,52 @@ successful, this is because we are not specifically checking for end-of-file.

97142 (Integer, List (TokenData ExpressionToken))

98143 *parserEx>

99144

100−.. code-block:: idris

145+.. list-table::

101146

102− ||| Succeeds if running the predicate on the next token returns Just x,

103− ||| returning x. Otherwise fails.

104− export

105− terminal : (tok -> Maybe a) -> Grammar tok True a

106− terminal = Terminal

147+ * - The ``intLiteral`` function above uses the ``terminal`` function to

148+ construct the grammar

149+ - .. code-block:: idris

107150

108−.. code-block:: idris

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::

109165

110− openParen : Rule Integer

111− openParen = terminal (\x => case tok x of

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

112174 OParen => Just 0

113175 _ => Nothing)

114176

177+Integer value is not really relevant for parenthesis so ``0`` (zero) is used as

178+a default value.

179+

180+As before, this can be tested with a function like this:

181+

115182.. code-block:: idris

116183

117184 test2 : String -> Either (ParseError (TokenData ExpressionToken))

118185 (Integer, List (TokenData ExpressionToken))

119186 test2 s = parse openParen (fst (lex expressionTokens s))

120187

188+We can see below that it correctly parses an open parenthesis and gives an

189+error for anything else:

190+

121191.. code-block:: idris

122192

123193 *parserEx> test2 "("

@@ -130,7 +200,12 @@ successful, this is because we are not specifically checking for end-of-file.

130200 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))

131201 (Integer,

132202 List (TokenData ExpressionToken))

133− *parserEx>

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:

134209

135210.. code-block:: idris

136211

@@ -138,6 +213,9 @@ successful, this is because we are not specifically checking for end-of-file.

138213 (Integer, List (TokenData ExpressionToken))

139214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))

140215

216+We can see below that ``(`` followed by a number is successfully parsed but, as

217+required, other token lists are not:

218+

141219.. code-block:: idris

142220

143221 *parserEx> test3 "(123"

@@ -170,15 +248,121 @@ successful, this is because we are not specifically checking for end-of-file.

170248 (incol, b) => cast (length incol))

171249 OParen]) : Either (ParseError (TokenData ExpressionToken))

172250 (Integer, List (TokenData ExpressionToken))

173− *parserEx>

174251

175−.. code-block:: idris

252+.. list-table::

253+

254+ * - The closing parenthesis is constructed in the same way.

255+

256+ - .. code-block:: idris

176257

177− closeParen : Rule Integer

178− closeParen = terminal (\x => case tok x of

258+ closeParen : Rule Integer

259+ closeParen = terminal (\x => case tok x of

179260 CParen => Just 0

180261 _ => Nothing)

181262

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+So lets try to use this to define a grammar which recognises either:

277+

278+- An integer literal

279+- An integer literal inside parenthesis

280+- An integer literal inside parenthesis inside parenthesis

281+- ... and so on.

282+

283+.. list-table::

284+

285+ * - This requires a recursively defined structure like this:

286+

287+ - .. code-block:: idris

288+

289+ partial

290+ expr : Rule Integer

291+ expr = intLiteral <|> (paren expr)

292+

293+This is a valid grammar because every time it is called it is guaranteed to

294+consume a token. However, as an Idris structure, it is problematic due to

295+the recursion. Defining it as partial allows it to compile but at runtime

296+we are likely to get a crash with an (unhelpful) error message like

297+``killed by signal 11``.

298+

299+So a better method is to use ``do`` notation as described in the following

300+section.

301+

302+Monadic Combinator

303+------------------

304+

305+In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is

306+defined like this:

307+

308+.. code-block:: idris

309+

310+ ||| Sequence two grammars. If either consumes some input, the sequence is

311+ ||| guaranteed to consume some input. If the first one consumes input, the

312+ ||| second is allowed to be recursive (because it means some input has been

313+ ||| consumed and therefore the input is smaller)

314+ export %inline

315+ (>>=) : {c1 : Bool} ->

316+ Grammar tok c1 a ->

317+ inf c1 (a -> Grammar tok c2 b) ->

318+ Grammar tok (c1 || c2) b

319+ (>>=) {c1 = False} = SeqEmpty

320+ (>>=) {c1 = True} = SeqEat

321+

322+.. list-table::

323+

324+ * - This allows us to use ``do`` notation for the previous parenthesis example:

325+

326+ - .. code-block:: idris

327+

328+ expr = intLiteral <|> do

329+ openParen

330+ r <- expr

331+ closeParen

332+ pure r

333+

334+This can be more flexible than using the ``<*>`` operator. Also it is defined

335+using ``Inf`` so we can implement recursively defined grammars as above.

336+

337+Implementing the Arithmetic Operators

338+-------------------------------------

339+

340+.. list-table::

341+

342+ * - Now for the operations, in this case: ``+``, ``-`` and ``*``.

343+ The syntax we require for these infix operators

344+ would require recursive grammars like this:

345+

346+ - .. code-block:: idris

347+

348+ expr = expr (op "+") expr

349+

350+As already explained, ``do`` notation can allow us to use recursive

351+definitions but not necessarily left-recursion like this.

352+

353+In order to work up to this gradually lets start with prefix operators

354+(sometimes known as Polish notation) then modify later for infix operators.

355+

356+.. list-table::

357+

358+ * - So prefix operators would have this sort of form:

359+

360+ - .. code-block:: idris

361+

362+ expr = (add (op "+") expr expr)

363+

364+where ``op`` is defined like this:

365+

182366.. code-block:: idris

183367

184368 ||| Matches if this is an operator token and string matches, that is,

@@ -188,10 +372,143 @@ successful, this is because we are not specifically checking for end-of-file.

188372 (Operator s1) => if s==s1 then Just 0 else Nothing

189373 _ => Nothing)

190374

375+.. list-table::

376+

377+ * - and ``add`` is defined like this:

378+

379+ Where:

380+

381+ - x is the add operator.

382+ - y is the first operand.

383+ - z is the second operand.

384+

385+ - .. code-block:: idris

386+

387+ addInt : Integer -> Integer -> Integer

388+ addInt a b = a+b

389+

390+ export

391+ add : Grammar tok c1 Integer ->

392+ Grammar tok c2 Integer ->

393+ Grammar tok c3 Integer ->

394+ Grammar tok ((c1 || c2) || c3) Integer

395+ add x y z = map addInt (x *> y) <*> z

396+

397+

398+

399+The resulting integer will be the sum of the two operands.

400+

401+.. list-table::

402+

403+ * - The other operators are defined in a similar way:

404+

405+ - .. code-block:: idris

406+

407+ subInt : Integer -> Integer -> Integer

408+ subInt a b = a-b

409+

410+ export

411+ sub : Grammar tok c1 Integer ->

412+ Grammar tok c2 Integer ->

413+ Grammar tok c3 Integer ->

414+ Grammar tok ((c1 || c2) || c3) Integer

415+ sub x y z = map subInt (x *> y) <*> z

416+

417+ multInt : Integer -> Integer -> Integer

418+ multInt a b = a*b

419+

420+ export

421+ mult : Grammar tok c1 Integer ->

422+ Grammar tok c2 Integer ->

423+ Grammar tok c3 Integer ->

424+ Grammar tok ((c1 || c2) || c3) Integer

425+ mult x y z = map multInt (x *> y) <*> z

426+

427+So the top level ``Grammar`` can now be defined as follows. Note that this is

428+partial as it is a potentially infinite structure and so not total.

429+

191430.. code-block:: idris

192431

193− paren : Rule Integer -> Rule Integer

194− paren exp = openParen *> exp <* closeParen

432+ partial

433+ expr : Rule Integer

434+ expr = (add (op "+") expr expr)

435+ <|> (sub (op "-") expr expr)

436+ <|> (mult (op "*") expr expr)

437+ <|> intLiteral <|> (paren expr)

438+

439+.. list-table::

440+

441+ * - To make the testing easier we can use this function:

442+

443+ - .. code-block:: idris

444+

445+ partial

446+ test : String -> Either (ParseError (TokenData ExpressionToken))

447+ (Integer, List (TokenData ExpressionToken))

448+ test s = parse expr (fst (lex expressionTokens s))

449+

450+.. list-table::

451+

452+ * - First test a valid (prefix) expression:

453+

454+ - .. code-block:: idris

455+

456+ *parserEx> test "+1*6(4)"

457+ Right (25,

458+ []) : Either (ParseError (TokenData ExpressionToken))

459+ (Integer, List (TokenData ExpressionToken))

460+

461+Then an invalid syntax:

462+

463+.. code-block:: idris

464+

465+ *parserEx> test "))"

466+ Left (Error "Unrecognised token"

467+ [MkToken 0 0 CParen,

468+ MkToken 0

469+ (case fspan (\ARG =>

470+ not (intToBool (prim__eqChar ARG

471+ '\n')))

472+ ")" of

473+ (incol, "") => c + cast (length incol)

474+ (incol, b) => cast (length incol))

475+ CParen]) : Either (ParseError (TokenData ExpressionToken))

476+ (Integer,

477+ List (TokenData ExpressionToken))

478+

479+However if we try something that is invalid, but starts with a valid token,

480+then it will return ``Right`` (to indicate success)

481+

482+.. code-block:: idris

483+

484+ *parserEx> test "1))"

485+ Right (1,

486+ [MkToken 0

487+ (case fspan (\ARG =>

488+ not (intToBool (prim__eqChar ARG '\n')))

489+ "1" of

490+ (incol, "") => c + cast (length incol)

491+ (incol, b) => cast (length incol))

492+ CParen,

493+ MkToken 0

494+ (case fspan (\ARG =>

495+ not (intToBool (prim__eqChar ARG '\n')))

496+ ")" of

497+ (incol, "") => c + cast (length incol)

498+ (incol, b) => cast (length incol))

499+ CParen]) : Either (ParseError (TokenData ExpressionToken))

500+ (Integer,

501+ List (TokenData ExpressionToken))

502+

503+Infix Notation

504+--------------

505+

506+So far we have implemented a prefix notation for operators (like this:

507+``+ expr expr``) but the aim is to implemented an infix notation (like this:

508+``expr + expr``). To do this we must be able to deal with potentially

509+infinite data structures (see Codata Types here :ref:`sect-typefuns`).

510+

511+First alter the grammar to have infix operations:

195512

196513.. code-block:: idris

197514

@@ -203,9 +520,7 @@ successful, this is because we are not specifically checking for end-of-file.

203520 Grammar tok c2 Integer ->

204521 Grammar tok c3 Integer ->

205522 Grammar tok ((c1 || c2) || c3) Integer

206− add x y z = map addInt (x *> y) <*> z

207−

208−.. code-block:: idris

523+ add x y z = map addInt (x <* y) <*> z

209524

210525 subInt : Integer -> Integer -> Integer

211526 subInt a b = a-b

@@ -215,7 +530,7 @@ successful, this is because we are not specifically checking for end-of-file.

215530 Grammar tok c2 Integer ->

216531 Grammar tok c3 Integer ->

217532 Grammar tok ((c1 || c2) || c3) Integer

218− sub x y z = map subInt (x *> y) <*> z

533+ sub x y z = map subInt (x <* y) <*> z

219534

220535

221536 multInt : Integer -> Integer -> Integer

@@ -226,51 +541,160 @@ successful, this is because we are not specifically checking for end-of-file.

226541 Grammar tok c2 Integer ->

227542 Grammar tok c3 Integer ->

228543 Grammar tok ((c1 || c2) || c3) Integer

229− mult x y z = map multInt (x *> y) <*> z

230−

231−.. code-block:: idris

544+ mult x y z = map multInt (x <* y) <*> z

232545

233546 partial

234547 expr : Rule Integer

235− expr = (add (op "+") expr expr)

236− <|> (sub (op "-") expr expr)

237− <|> (mult (op "*") expr expr)

548+ expr = (add expr (op "+") expr)

549+ <|> (sub expr (op "-") expr)

550+ <|> (mult expr (op "*") expr)

238551 <|> intLiteral <|> (paren expr)

239552

553+However, if this was run, the code would not terminate.

554+

555+Implement Left Recursion Elimination

556+------------------------------------

557+

558+Left factoring, like this, is a general problem.

559+

560+If we have a rule like this:

561+

240562.. code-block:: idris

241563

242− *parserEx> parse expr (fst (lex expressionTokens "(1)"))

243− Right (1, []) : Either (ParseError (TokenData ExpressionToken))

244− (Integer, List (TokenData ExpressionToken))

245− *parserEx>

564+ A -> (x<*>y) <|> (x<*>z)

565+

566+If ``x<*>y`` fails but ``x<*>z`` would succeed a problem is that, ``x<*>y`` has

567+already consumed ``x``, so now ``x<*>z`` will fail.

568+

569+so we could write code to backtrack. That is ``try`` ``x<*>y`` without consuming

570+so that, if the first token succeeds but the following tokens fail, then the

571+first tokens would not be consumed.

572+

573+Another approach is left factoring:

574+

575+Left Factoring

576+--------------

577+

578+Replace the rule with two rules (that is we add a non-terminal symbol) so

579+for example, instead of:

246580

247581.. code-block:: idris

248582

249− parse : (act : Grammar tok c ty) -> (xs : List tok)

583+ A -> (x<*>y) <|> (x<*>z)

250584

251− parse intLiteral (fst (lex expressionTokens "1"))

585+we add an extra rule to give:

252586

253587.. code-block:: idris

254588

255− *parserEx> parse expr (fst (lex expressionTokens "1+2"))

256− Right (1,

257− [MkToken 0

258− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of

259− (incol, "") => c + cast (length incol)

260− (incol, b) => cast (length incol))

261− (Operator "+"),

262− MkToken 0

263− (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of

264− (incol, "") => c + cast (length incol)

265− (incol, b) => cast (length incol))

266− (Number 2)]) : Either (ParseError (TokenData ExpressionToken))

267− (Integer, List (TokenData ExpressionToken))

268− *parserEx>

589+ A -> x<*>N

590+ N -> y <|> z

591+

592+That is we convert a general context-free grammar to a LL(1) grammar. Although

593+not every context-free grammar can be converted to a LL(1) grammar.

594+

595+This still does not solve the infinite recursion issue and there is another

596+problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.

597+

598+.. list-table::

599+

600+ * - To resolve this we can alter the example to have a BNF like this:

601+ Where braces ``{ ... }`` mean the contents can occur 1 or more times.

602+

603+ - .. code-block:: idris

604+

605+ 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}

606+

607+ 'term' ::= 'factor' {'*' 'factor'}

608+

609+ 'factor' ::=

610+ number

611+ | '(' 'expression' ')'

612+

269613

270614.. code-block:: idris

271615

272− partial

273− test : String -> Either (ParseError (TokenData ExpressionToken))

616+ expr : Rule Integer

617+

618+ factor : Rule Integer

619+ factor = intLiteral <|> do

620+ openParen

621+ r <- expr

622+ closeParen

623+ pure r

624+

625+ term : Rule Integer

626+ term = map multInt factor <*> (

627+ (op "*")

628+ *> factor)

629+ <|> factor

630+

631+ expr = map addInt term <*> (

632+ (op "+")

633+ *> term)

634+ <|> map subInt term <*> (

635+ (op "-")

636+ *> term)

637+ <|> term

638+

639+ calc : String -> Either (ParseError (TokenData ExpressionToken))

274640 (Integer, List (TokenData ExpressionToken))

275− test s = parse expr (fst (lex expressionTokens s))

641+ calc s = parse expr (fst (lex expressionTokens s))

642+

643+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()

644+ lft (Error s lst) = putStrLn ("error:"++s)

645+

646+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()

647+ rht i = putStrLn ("right " ++ (show i))

648+

649+ main : IO ()

650+ main = do

651+ putStr "alg>"

652+ x <- getLine

653+ either lft rht (calc x) -- eliminator for Either

654+

655+As the following tests show, this now handles infix operators and precedence.

656+

657+.. list-table::

658+

659+ * - For example '*' is an infix operator:

660+

661+ - .. code-block:: idris

662+

663+ *algebraREPL> :exec

664+ alg>2*3

665+ right (6, [])

666+

667+ * - Check that atomic number literals work:

668+

669+ - .. code-block:: idris

670+

671+ *algebraREPL> :exec

672+ alg>2

673+ right (2, [])

674+

675+ * - Check that '*' has a higher precedence than '+'.

676+

677+ - .. code-block:: idris

678+

679+ *algebraREPL> :exec

680+ alg>2+3*4

681+ right (14, [])

682+

683+ * - Also '*' has a higher precedence than '+' when the order is reversed.

684+

685+ - .. code-block:: idris

686+

687+ *algebraREPL> :exec

688+ alg>3*4+2

689+ right (14, [])

690+

691+ * - Also precedence can be overridden by parenthesis.

692+

693+ - .. code-block:: idris

694+

695+ *algebraREPL> :exec

696+ alg>(2+3)*4

697+ right (20, [])

276698

699+This is still not correct because it does not correctly parse multiple sums or terms

700+like ``1+2+3`` or ``1*2*3``.

docs/parserLibrary/whitespace.rstnew file+250

@@ -0,0 +1,250 @@

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 in the future. For

12+example, we might want to implement function application expressed by

13+juxtaposition as in Haskell and Idris like this: ``f x``.

14+

15+So, on this page, we will add a token for whitespace and comments. We will

16+then consider two ways to process this:

17+

18+- Filter all whitespace tokens from the lexer results before passing to

19+ the parser.

20+- Process the whitespace tokens in the parser.

21+

22+Whitespace and Comments in Lexer

23+--------------------------------

24+

25+To start with we can use the same token for both whitespace and comments. Here

26+it is called ``Comment`` and added to the ``ExpressionToken`` data structure

27+like this:

28+

29+.. code-block:: idris

30+

31+ public export

32+ data ExpressionToken = Number Integer

33+ | Operator String

34+ | OParen

35+ | CParen

36+ | Comment String

37+ | EndInput

38+

39+This is added to the ``TokenMap`` like this:

40+

41+.. code-block:: idris

42+

43+ ||| from https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr

44+ comment : Lexer

45+ comment = is '-' <+> is '-' <+> many (isNot '\n')

46+

47+ expressionTokens : TokenMap ExpressionToken

48+ expressionTokens =

49+ [(digits, \x => Number (toInt' x)),

50+ (operator, \x => Operator x),

51+ (is '(' ,\x => OParen),

52+ (is ')' ,\x => CParen),

53+ (spaces, Comment),

54+ (comment, Comment)]

55+

56+As you can see, the comment is defined like a single line Idris comment,

57+it starts with ``--`` and continues for the remainder of the line.

58+

59+We don't need to define ``spaces`` because it is already defined in

60+: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr

61+like this:

62+

63+.. code-block:: idris

64+

65+ ||| Recognise a single whitespace character

66+ ||| /\\s/

67+ space : Lexer

68+ space = pred isSpace

69+

70+ ||| Recognise one or more whitespace characters

71+ ||| /\\s+/

72+ spaces : Lexer

73+ spaces = some space

74+

75+If these whitespace tokens are not significant, that is, they can appear

76+anywhere and they are optional then we can filter them out before the parser

77+gets them like this:

78+

79+.. code-block:: idris

80+

81+ processWhitespace : (List (TokenData ExpressionToken), Int, Int, String)

82+ -> (List (TokenData ExpressionToken), Int, Int, String)

83+ processWhitespace (x,l,c,s) = ((filter notComment x),l,c,s) where

84+ notComment : TokenData ExpressionToken -> Bool

85+ notComment t = case tok t of

86+ Comment _ => False

87+ _ => True

88+

89+ calc : String -> Either (ParseError (TokenData ExpressionToken))

90+ (Integer, List (TokenData ExpressionToken))

91+ calc s = parse expr (fst (processWhitespace (lex expressionTokens s)))

92+

93+

94+Whitespace and Comments in Parser

95+---------------------------------

96+

97+If we sometimes require whitespace to be significant then we can't filter

98+them out as above. In this case the ``Comment`` tokens are sent to the parser

99+which now needs to be able to handle them.

100+

101+.. code-block:: idris

102+

103+ commentSpace : Rule Integer

104+ commentSpace = terminal (\x => case tok x of

105+ Comment s => Just 0

106+ _ => Nothing)

107+

108+So far we don't have any syntax that requires spaces to be significant so we

109+need to define the grammar so that it will parse with, or without, spaces.

110+This needs to be done in a systematic way, here I have defined the grammar so

111+that there is an optional space to the right of every atom or operator.

112+First add versions of ``intLiteral`` , ``openParen`` , ``closeParen``

113+and ``op`` that allow optional spaces/comments to the right of them:

114+

115+.. code-block:: idris

116+

117+ intLiteralC : Rule Integer

118+ intLiteralC = (intLiteral <* commentSpace) <|> intLiteral

119+

120+ openParenC : Rule Integer

121+ openParenC = (openParen <* commentSpace) <|> openParen

122+

123+ closeParenC : Rule Integer

124+ closeParenC = (closeParen <* commentSpace) <|> closeParen

125+

126+ ||| like op but followed by optional comment or space

127+ opC : String -> Rule Integer

128+ opC s = ((op s) <* commentSpace) <|> (op s)

129+

130+Then just use these functions instead of the original functions:

131+

132+.. code-block:: idris

133+

134+ expr : Rule Integer

135+

136+ factor : Rule Integer

137+ factor = intLiteralC <|> do

138+ openParenC

139+ r <- expr

140+ closeParenC

141+ pure r

142+

143+ term : Rule Integer

144+ term = map multInt factor <*> (

145+ (opC "*")

146+ *> factor)

147+ <|> factor

148+

149+ expr = map addInt term <*> (

150+ (opC "+")

151+ *> term)

152+ <|> map subInt term <*> (

153+ (opC "-")

154+ *> term)

155+ <|> term

156+

157+ calc : String -> Either (ParseError (TokenData ExpressionToken))

158+ (Integer, List (TokenData ExpressionToken))

159+ calc s = parse expr (fst (lex expressionTokens s))

160+

161+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()

162+ lft (Error s lst) = putStrLn ("error:"++s)

163+

164+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()

165+ rht i = putStrLn ("right " ++ (show i))

166+

167+ main : IO ()

168+ main = do

169+ putStr "alg>"

170+ x <- getLine

171+ either lft rht (calc x) -- eliminator for Either

172+

173+

174+Defining Block Structure using Indents

175+--------------------------------------

176+

177+Many languages such as Python, Haskell and Idris use indents to delimit

178+the block structure of the language.

179+

180+We can see how Idris2 does it here

181+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

182+

183+.. code-block:: idris

184+

185+ export

186+ IndentInfo : Type

187+ IndentInfo = Int

188+

189+ export

190+ init : IndentInfo

191+ init = 0

192+

193+EndInput Token

194+--------------

195+

196+So far, the parser will return a successful result even if the full input

197+is not consumed. To ensure that the top level syntax is fully matched we

198+add a ``EndInput`` token to indicate the last token.

199+

200+``EndInput`` is added to the other tokens like this:

201+

202+.. code-block:: idris

203+

204+ data ExpressionToken = Number Integer

205+ | Operator String

206+ | OParen

207+ | CParen

208+ | Comment String

209+ | EndInput

210+

211+A rule to consume this token is added:

212+

213+.. code-block:: idris

214+

215+ eoi : Rule Integer

216+ eoi = terminal (\x => case tok x of

217+ EndInput => Just 0

218+ _ => Nothing)

219+

220+Instead of using ``expr`` at the top level of the syntax we can now define

221+``exprFull`` as shown here. This will make sure that only when ``EndInput``

222+is consumed will the parse be successful:

223+

224+.. code-block:: idris

225+

226+ exprFull : Rule Integer

227+ exprFull = expr <* eoi

228+

229+The following code makes sure ``EndInput`` is added to the end of the token

230+list:

231+

232+.. code-block:: idris

233+

234+ processWhitespace : (List (TokenData ExpressionToken), Int, Int, String)

235+ -> (List (TokenData ExpressionToken), Int, Int, String)

236+ processWhitespace (x,l,c,s) = ((filter notComment x)++

237+ [MkToken l c EndInput],l,c,s) where

238+ notComment : TokenData ExpressionToken -> Bool

239+ notComment t = case tok t of

240+ Comment _ => False

241+ _ => True

242+

243+All we have to do now is use ``exprFull`` instead of ``expr``:

244+

245+.. code-block:: idris

246+

247+ calc : String -> Either (ParseError (TokenData ExpressionToken))

248+ (Integer, List (TokenData ExpressionToken))

249+ calc s = parse exprFull (fst (processWhitespace (lex expressionTokens s)))

250+

docs/reference/codegen.rst+4−4

@@ -36,10 +36,10 @@ issue the following command:

3636 $ idris --codegen javascript hello.idr -o hello.js

3737

3838

39−Idris can produce very big chunks of JavaScript code (hello world

40−weighs in at 1500 lines). However, the generated code can be minified

41−using the `closure-compiler

42−<https://developers.google.com/closure/compiler/>`__ from Google.

39+Idris can produce big chunks of JavaScript code (hello world weighs in at about

40+60 lines). However, the generated code can be minified using the

41+`closure-compiler <https://developers.google.com/closure/compiler/>`__ from

42+Google.

4343

4444::

4545

docs/reference/misc.rst+5−5

@@ -115,11 +115,11 @@ Here is an example:

115115 import Syntax.PreorderReasoning

116116 multThree : (a, b, c : Nat) -> a * b * c = c * a * b

117117 multThree a b c =

118− (a * b * c) ={ sym (multAssociative a b c) }=

119− (a * (b * c)) ={ cong (multCommutative b c) }=

120− (a * (c * b)) ={ multAssociative a c b }=

121− (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=

122− (c * a * b) QED

118+ (a * b * c) ={ sym (multAssociative a b c) }=

119+ (a * (b * c)) ={ cong (multCommutative b c) }=

120+ (a * (c * b)) ={ multAssociative a c b }=

121+ (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=

122+ (c * a * b) QED

123123

124124Note that the parentheses are required -- only a simple expression can

125125be on the left of ``={ }=`` or ``QED``. Also, when using preorder

idris-tutorial.pdf

Binary file not shown.

idris.cabal+101−47

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

1+Cabal-Version: 2.4

12Name: idris

23Version: 1.3.2

3−License: BSD3

4+License: BSD-3-Clause

45License-file: LICENSE

56Author: Edwin Brady

67Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>

@@ -41,42 +42,25 @@ Description: Idris is a general purpose language with full dependent types.

4142 .

4243 * Hugs style interactive environment

4344

44−Cabal-Version: >= 1.22

45−

4645Build-type: Custom

4746

4847Tested-With: GHC == 7.10.3, GHC == 8.0.1

4948

49+-- NOTE: due to https://github.com/haskell/cabal/issues/6125 the use of ** is

50+-- heavily discouraged.

5051Data-files: idrisdoc/styles.css

51− jsrts/jsbn/jsbn-browser.js

52− jsrts/jsbn/jsbn-node.js

53− jsrts/Runtime-common.js

54− jsrts/Runtime-javascript.js

55− jsrts/Runtime-node.js

52+ jsrts/jsbn/*.js

53+ jsrts/*.js

5654 jsrts/jsbn/LICENSE

57− rts/arduino/idris_main.c

58− rts/idris_bitstring.c

59− rts/idris_bitstring.h

60− rts/idris_gc.c

61− rts/idris_gc.h

62− rts/idris_gmp.c

63− rts/idris_gmp.h

64− rts/idris_heap.c

65− rts/idris_heap.h

66− rts/idris_main.c

67− rts/idris_net.c

68− rts/idris_net.h

69− rts/idris_opts.c

70− rts/idris_opts.h

71− rts/idris_rts.c

72− rts/idris_rts.h

73− rts/idris_stats.c

74− rts/idris_stats.h

75− rts/idris_stdfgn.c

76− rts/idris_stdfgn.h

77− rts/mini-gmp.c

78− rts/mini-gmp.h

79− rts/libtest.c

55+ rts/Makefile

56+ rts/*.c

57+ rts/seL4/*.c

58+ rts/arduino/*.c

59+ rts/windows/*.c

60+ rts/windows/*.h

61+ rts/*.h

62+ rts/seL4/CMakeLists.txt

63+ rts/seL4/README.md

8064

8165Extra-doc-files:

8266 CHANGELOG.md

@@ -86,13 +70,75 @@ Extra-doc-files:

8670 README.md

8771 RELEASE-CHECKS.md

8872 idris-tutorial.pdf

73+ man/idris.1

8974 samples/effects/*.idr

9075 samples/misc/*.idr

91− samples/misc/*.lidr

9276 samples/tutorial/*.idr

77+ samples/ST/*.idr

78+ samples/ST/Graphics/*.idr

79+ samples/ST/Net/*.idr

80+ samples/misc/*.lidr

9381

9482-- extra-source-files is generated by Setup.hs using `git --ls-files`.

9583Extra-source-files:

84+ Makefile

85+ config.mk

86+ custom.mk-alldeps

87+ mkpkg.sh

88+ stack-shell.nix

89+ stack.yaml

90+ stylize.sh

91+ win-release.sh

92+

93+ benchmarks/*.pl

94+ benchmarks/fasta/*.idr

95+ benchmarks/fasta/*.ipkg

96+ benchmarks/pidigits/*.idr

97+ benchmarks/pidigits/*.ipkg

98+ benchmarks/quasigroups/*.idr

99+ benchmarks/quasigroups/*.ipkg

100+ benchmarks/trivial/*.idr

101+ benchmarks/trivial/*.ipkg

102+ benchmarks/quasigroups/board

103+

104+ icons/*.png

105+ icons/*.ico

106+ icons/*.rc

107+ icons/*.svg

108+ icons/*.xml

109+

110+ libs/**/*.idr

111+ libs/**/*.ipkg

112+ libs/**/*.txt

113+ libs/Makefile

114+ libs/base/Makefile

115+ libs/contrib/Makefile

116+ libs/effects/Makefile

117+ libs/prelude/Makefile

118+ libs/pruviloj/Makefile

119+

120+ scripts/generate-multi-ghc-travis-template

121+ scripts/runidris

122+ scripts/runidris-node

123+

124+ src/.ghci

125+

126+ test/*.md

127+ test/*.hs

128+ test/**/*.idr

129+ test/**/*.lidr

130+ test/**/*.ipkg

131+ test/**/*.out

132+ test/**/*.sh

133+ test/**/*.c

134+ test/**/*.h

135+ test/**/*.in

136+ test/**/*.txt

137+ test/**/*.js

138+ test/base001/Makefile

139+ test/ffi004/theOtherType

140+ test/ffi004/theType

141+ test/scripts/timeout

96142

97143source-repository head

98144 type: git

@@ -100,7 +146,7 @@ source-repository head

100146

101147custom-setup

102148 setup-depends:

103− Cabal >= 1.10 && <2.5,

149+ Cabal >= 2.4 && < 3.1,

104150 base >= 4 && <5,

105151 directory,

106152 filepath,

@@ -261,26 +307,29 @@ Library

261307 Util.Pretty

262308 , Util.Net

263309

264−

265−

266− -- Auto Generated

267310 , Paths_idris

268311 , Version_idris

269312 , Tools_idris

270313 , BuildFlags_idris

271314

315+ -- Auto Generated

316+ Autogen-modules: Paths_idris

317+ , Version_idris

318+ , Tools_idris

319+ , BuildFlags_idris

320+

272321 Build-depends: base >=4 && <5

273322 , aeson >= 0.6 && < 1.5

274323 , annotated-wl-pprint >= 0.7 && < 0.8

275− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

276325 , ansi-wl-pprint < 0.7

277326 , array >= 0.4.0.1 && < 0.6

278327 , base64-bytestring < 1.1

279328 , binary >= 0.8.4.1 && < 0.9

280329 , blaze-html >= 0.6.1.3 && < 0.10

281− , blaze-markup >= 0.5.2.1 && < 0.9

330+ , blaze-markup >= 0.5.2.1 && < 0.10

282331 , bytestring < 0.11

283− , cheapskate >= 0.1.1 && < 0.2

332+ , cheapskate >= 0.1.1.2 && < 0.2

284333 , code-page >= 0.1 && < 0.3

285334 , containers >= 0.5 && < 0.7

286335 , deepseq < 1.5

@@ -289,10 +338,10 @@ Library

289338 , fingertree >= 0.1.4.1 && < 0.2

290339 , haskeline >= 0.7 && < 0.8

291340 , ieee754 >= 0.7 && < 0.9

292− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

293342 , mtl >= 2.1 && < 2.3

294− , network >= 2.7 && < 2.9

295− , optparse-applicative >= 0.13 && < 0.15

343+ , network >= 2.7 && < 3.1.2

344+ , optparse-applicative >= 0.13 && < 0.16

296345 , parser-combinators >= 1.0.0

297346 , pretty < 1.2

298347 , process < 1.7

@@ -300,8 +349,8 @@ Library

300349 , safe >= 0.3.9

301350 , split < 0.3

302351 , terminal-size < 0.4

303− , text >=1.2.1.0 && < 1.3

304− , time >= 1.4 && < 1.9

352+ , text >=1.2.1.0 && < 1.4

353+ , time >= 1.4 && < 2.0

305354 , transformers >= 0.5 && < 0.6

306355 , uniplate >=1.6 && < 1.7

307356 , unordered-containers < 0.3

@@ -309,11 +358,12 @@ Library

309358 , vector < 0.13

310359 , vector-binary-instances < 0.3

311360 , zip-archive > 0.2.3.5 && < 0.5

312− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

313362 , async < 2.3

314363

315364 if !impl(ghc >= 8.0)

316− Build-Depends: semigroups == 0.18.*

365+ Build-Depends: semigroups == 0.18.*

366+ , fail == 4.9.0.*

317367

318368 Default-Language: Haskell2010

319369 ghc-prof-options: -auto-all -caf-all

@@ -332,6 +382,7 @@ Library

332382 cpp-options: -DIDRIS_GMP

333383 if flag(freestanding)

334384 other-modules: Target_idris

385+ autogen-modules: Target_idris

335386 cpp-options: -DFREESTANDING

336387 if flag(CI)

337388 ghc-options: -Werror

@@ -365,7 +416,7 @@ Test-suite regression-and-feature-tests

365416 , filepath

366417 , directory

367418 , haskeline >= 0.7

368− , optparse-applicative >= 0.13 && < 0.15

419+ , optparse-applicative >= 0.13 && < 0.16

369420 , tagged

370421 , tasty >= 0.8

371422 , tasty-golden >= 2.0

@@ -380,6 +431,7 @@ Test-suite regression-and-feature-tests

380431

381432Executable idris-codegen-c

382433 Main-is: Main.hs

434+ autogen-modules: Paths_idris

383435 other-modules: Paths_idris

384436 hs-source-dirs: codegen/idris-codegen-c

385437

@@ -395,6 +447,7 @@ Executable idris-codegen-c

395447

396448Executable idris-codegen-javascript

397449 Main-is: Main.hs

450+ autogen-modules: Paths_idris

398451 other-modules: Paths_idris

399452 hs-source-dirs: codegen/idris-codegen-javascript

400453

@@ -410,6 +463,7 @@ Executable idris-codegen-javascript

410463

411464Executable idris-codegen-node

412465 Main-is: Main.hs

466+ autogen-modules: Paths_idris

413467 other-modules: Paths_idris

414468 hs-source-dirs: codegen/idris-codegen-node

415469

libs/base/Control/Isomorphism.idr+20−23

@@ -17,21 +17,22 @@ record Iso a b where

1717

1818-- Isomorphism properties

1919

20−||| Isomorphism is Reflexive

20+||| Isomorphism is reflexive

2121isoRefl : Iso a a

22−isoRefl = MkIso id id (\x => Refl) (\x => Refl)

22+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)

2323

2424||| Isomorphism is transitive

2525isoTrans : Iso a b -> Iso b c -> Iso a c

2626isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =

27− MkIso (\x => to' (to x))

28− (\y => from (from' y))

29− (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=

30− (to' (from' y)) ={ toFrom' y }=

31− y QED)

32− (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=

33− (from (to x)) ={ fromTo x }=

34− x QED)

27+ MkIso xto xfrom xtoFrom xfromTo where

28+ xto : a -> c

29+ xto = to' . to

30+ xfrom : c -> a

31+ xfrom = from . from'

32+ xtoFrom : (z : c) -> xto (xfrom z) = z

33+ xtoFrom z = rewrite toFrom $ from' z in toFrom' z

34+ xfromTo : (x : a) -> xfrom (xto x) = x

35+ xfromTo x = rewrite fromTo' (to x) in fromTo x

3536

3637Category Iso where

3738 id = isoRefl

@@ -99,8 +100,7 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft

99100

100101||| Isomorphism is a congruence with regards to disjunction

101102eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')

102−eitherCong {a = a} {a' = a'} {b = b} {b' = b'}

103− (MkIso to from toFrom fromTo)

103+eitherCong (MkIso to from toFrom fromTo)

104104 (MkIso to' from' toFrom' fromTo') =

105105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2

106106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'

@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2

143143

144144||| Conjunction with truth is a no-op

145145pairUnitRight : Iso (a, ()) a

146−pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok

147− where ok : (x : (a, ())) -> (fst x, ()) = x

148− ok (x, ()) = Refl

146+pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)

149147

150148||| Conjunction with truth is a no-op

151149pairUnitLeft : Iso ((), a) a

@@ -161,8 +159,7 @@ pairBotRight = isoTrans pairComm pairBotLeft

161159

162160||| Isomorphism is a congruence with regards to conjunction

163161pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')

164−pairCong {a = a} {a' = a'} {b = b} {b' = b'}

165− (MkIso to from toFrom fromTo)

162+pairCong (MkIso to from toFrom fromTo)

166163 (MkIso to' from' toFrom' fromTo') =

167164 MkIso to'' from'' iso1 iso2

168165 where to'' : (a, b) -> (a', b')

@@ -205,7 +202,7 @@ distribLeft = MkIso to from toFrom fromTo

205202

206203||| Products distribute over sums

207204distribRight : Iso (a, Either b c) (Either (a, b) (a, c))

208−distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

205+distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

209206

210207

211208-- Enable preorder reasoning syntax over isomorphisms

@@ -222,7 +219,7 @@ step a iso1 iso2 = isoTrans iso1 iso2

222219-- Isomorphisms over Maybe

223220||| Isomorphism is a congruence with respect to Maybe

224221maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)

225−maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

222+maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

226223 where ok1 : (y : Maybe b) -> map to (map from y) = y

227224 ok1 Nothing = Refl

228225 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED

@@ -253,7 +250,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=

253250 () QED

254251

255252eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))

256−eitherMaybeLeftMaybe {a} {b} =

253+eitherMaybeLeftMaybe =

257254 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=

258255 (Either (Either a ()) b) ={ eitherAssoc }=

259256 (Either a (Either () b)) ={ eitherCongRight eitherComm }=

@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =

263260

264261

265262eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))

266−eitherMaybeRightMaybe {a} {b} =

263+eitherMaybeRightMaybe =

267264 (Either a (Maybe b)) ={ eitherComm }=

268265 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=

269266 (Maybe (Either b a)) ={ maybeCong eitherComm }=

@@ -288,8 +285,8 @@ maybeIsoS = MkIso forth back fb bf

288285 fb (FS x) = Refl

289286

290287finZeroBot : Iso (Fin 0) Void

291−finZeroBot = MkIso (\x => void (uninhabited x))

292− (\x => void x)

288+finZeroBot = MkIso (void . uninhabited)

289+ void

293290 (\x => void x)

294291 (\x => void (uninhabited x))

295292

libs/contrib/Control/Algebra/Laws.idr+128−80

@@ -6,98 +6,146 @@ import Interfaces.Verified

77%access export

9−||| A prof that -0 = 0 in any verified group.

10−inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral

9+||| -(-x) = x in any verified group.

10+inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->

11+ inverse (inverse x) = x

12+inverseSquaredIsIdentity x =

13+ let

14+ ix = inverse x

15+ iix = inverse ix

16+ in

17+ rewrite sym $ monoidNeutralIsNeutralR iix in

18+ rewrite sym $ groupInverseIsInverseL x in

19+ rewrite sym $ semigroupOpIsAssociative x ix iix in

20+ rewrite groupInverseIsInverseL ix in

21+ monoidNeutralIsNeutralL x

22+

23+||| -0 = 0 in any verified group.

24+inverseNeutralIsNeutral : VerifiedGroup t =>

25+ inverse (the t A.neutral) = A.neutral

1126inverseNeutralIsNeutral {t} =

12− let zero = the t neutral

13− step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)

14− step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1

15− in

16− replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2

27+ let e = the t neutral in

28+ rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in

29+ rewrite monoidNeutralIsNeutralR $ inverse e in

30+ inverseSquaredIsIdentity e

1731

18−||| A proof that -(-x) = x in any verified group.

19−inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x

20−inverseSquaredIsIdentity {t} x =

21− let zero = the t neutral

22− step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))

23− step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1

24− step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2

25− step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3

26− in

27− replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4

32+||| -(x + y) = -y + -x in any verified group.

33+inverseOfSum : VerifiedGroup t => (l, r : t) ->

34+ inverse (l <+> r) = inverse r <+> inverse l

35+inverseOfSum {t} l r =

36+ let

37+ e = the t neutral

38+ il = inverse l

39+ ir = inverse r

40+ sum = l <+> r

41+ ilr = inverse sum

42+ iril = ir <+> il

43+ ile = il <+> e

44+ in

45+ -- expand

46+ rewrite sym $ monoidNeutralIsNeutralR ilr in

47+ rewrite sym $ groupInverseIsInverseR r in

48+ rewrite sym $ monoidNeutralIsNeutralL ir in

49+ rewrite sym $ groupInverseIsInverseR l in

50+ -- shuffle

51+ rewrite semigroupOpIsAssociative ir il l in

52+ rewrite sym $ semigroupOpIsAssociative iril l r in

53+ rewrite sym $ semigroupOpIsAssociative iril sum ilr in

54+ -- contract

55+ rewrite sym $ monoidNeutralIsNeutralL il in

56+ rewrite groupInverseIsInverseL sum in

57+ rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in

58+ rewrite semigroupOpIsAssociative l il e in

59+ rewrite groupInverseIsInverseL l in

60+ rewrite monoidNeutralIsNeutralL e in

61+ Refl

2862

29−||| A proof that -(x + y) = -x - y in any verified abelian group.

30−inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r

31−inverseDistributesOverGroupOp {t} l r =

32− let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl

33− step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1

34− step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2

35− step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3

36− step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4

37− step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5

38− step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6

39− step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7

40− step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8

41− step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9

42− step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10

43− in

44− replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11

63+||| -(x + y) = -x + -y in any verified abelian group.

64+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->

65+ inverse (l <+> r) = inverse l <+> inverse r

66+inverseDistributesOverGroupOp l r =

67+ rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in

68+ inverseOfSum l r

4569

46−||| A proof that anything multiplied by zero yields zero back.

47−multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral

48−multNeutralAbsorbingL r =

49− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)

50− step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1

51− step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2

52− step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3

53− step5 = cong {f = \x => x <+> inverse r} step4

54− step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5

55− step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6

56− in

57− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7

70+||| Anything multiplied by zero yields zero back in a verified ring.

71+multNeutralAbsorbingL : VerifiedRing t => (r : t) ->

72+ A.neutral <.> r = A.neutral

73+multNeutralAbsorbingL {t} r =

74+ let

75+ e = the t neutral

76+ ir = inverse r

77+ exr = e <.> r

78+ iexr = inverse exr

79+ in

80+ rewrite sym $ monoidNeutralIsNeutralR exr in

81+ rewrite sym $ groupInverseIsInverseR exr in

82+ rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in

83+ rewrite groupInverseIsInverseR exr in

84+ rewrite sym $ ringOpIsDistributiveR e e r in

85+ rewrite monoidNeutralIsNeutralR e in

86+ groupInverseIsInverseR exr

5887

59−||| A proof that anything multiplied by zero yields zero back.

60−multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral

61−multNeutralAbsorbingR l =

62− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)

63− step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1

64− step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2

65− step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3

66− step5 = cong {f = \x => x <+> inverse l} step4

67− step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5

68− step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6

69− in

70− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7

88+||| Anything multiplied by zero yields zero back in a verified ring.

89+multNeutralAbsorbingR : VerifiedRing t => (l : t) ->

90+ l <.> A.neutral = A.neutral

91+multNeutralAbsorbingR {t} l =

92+ let

93+ e = the t neutral

94+ il = inverse l

95+ lxe = l <.> e

96+ ilxe = inverse lxe

97+ in

98+ rewrite sym $ monoidNeutralIsNeutralL lxe in

99+ rewrite sym $ groupInverseIsInverseL lxe in

100+ rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in

101+ rewrite groupInverseIsInverseL lxe in

102+ rewrite sym $ ringOpIsDistributiveL l e e in

103+ rewrite monoidNeutralIsNeutralL e in

104+ groupInverseIsInverseL lxe

71105

72−||| A proof that inverse operator can be extracted before multiplication

106+||| Inverse operator can be extracted before multiplication.

73107||| (-x)y = -(xy)

74−multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)

108+multInverseInversesL : VerifiedRing t => (l, r : t) ->

109+ inverse l <.> r = inverse (l <.> r)

75110multInverseInversesL l r =

76− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)

77− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1

78− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2

79− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3

80− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4

81− step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5

82− in

83− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6

111+ let

112+ il = inverse l

113+ lxr = l <.> r

114+ ilxr = il <.> r

115+ i_lxr = inverse lxr

116+ in

117+ rewrite sym $ monoidNeutralIsNeutralR ilxr in

118+ rewrite sym $ groupInverseIsInverseR lxr in

119+ rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in

120+ rewrite sym $ ringOpIsDistributiveR l il r in

121+ rewrite groupInverseIsInverseL l in

122+ rewrite multNeutralAbsorbingL r in

123+ monoidNeutralIsNeutralL i_lxr

84124

85−||| A proof that inverse operator can be extracted before multiplication

125+||| Inverse operator can be extracted before multiplication.

86126||| x(-y) = -(xy)

87−multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)

127+multInverseInversesR : VerifiedRing t => (l, r : t) ->

128+ l <.> inverse r = inverse (l <.> r)

88129multInverseInversesR l r =

89− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)

90− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1

91− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2

92− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3

93− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4

94− step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5

95− in

96− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6

130+ let

131+ ir = inverse r

132+ lxr = l <.> r

133+ lxir = l <.> ir

134+ ilxr = inverse lxr

135+ in

136+ rewrite sym $ monoidNeutralIsNeutralL lxir in

137+ rewrite sym $ groupInverseIsInverseL lxr in

138+ rewrite semigroupOpIsAssociative lxir lxr ilxr in

139+ rewrite sym $ ringOpIsDistributiveL l ir r in

140+ rewrite groupInverseIsInverseR r in

141+ rewrite multNeutralAbsorbingR l in

142+ monoidNeutralIsNeutralR ilxr

97143

98−||| A proof that multiplication of inverses is the same as multiplication of original

99−||| elements. (-x)(-y) = xy

100−multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r

144+||| Multiplication of inverses is the same as multiplication of

145+||| original elements.

146+||| (-x)(-y) = xy

147+multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->

148+ inverse l <.> inverse r = l <.> r

101149multNegativeByNegativeIsPositive l r =

102150 rewrite multInverseInversesR (inverse l) r in

103151 rewrite sym $ multInverseInversesL (inverse l) r in

libs/contrib/Data/List/Extra.idrdeleted−46

@@ -1,46 +0,0 @@

1−module Data.List.Extra

2−

3−%default total

4−%access export

5−

6−||| The final segment of the accumulator is the final segment of the result.

7−reverseOntoAcc : (xs, ys, zs : List a) ->

8− reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs

9−reverseOntoAcc [] _ _ = Refl

10−reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

11−

12−||| Serves as a specification for reverseOnto.

13−reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

14−reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

15−

16−||| The reverse of an empty list is an empty list. Together with reverseCons,

17−||| serves as a specification for reverse.

18−reverseNil : reverse [] = []

19−reverseNil = Refl

20−

21−||| The reverse of a cons is the reverse of the tail followed by the head.

22−||| Together with reverseNil serves as a specification for reverse.

23−reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]

24−reverseCons x xs = reverseOntoSpec [x] xs

25−

26−||| Reversing an append is appending reversals backwards.

27−reverseAppend : (xs, ys : List a) ->

28− reverse (xs ++ ys) = reverse ys ++ reverse xs

29−reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))

30−reverseAppend (x :: xs) ys =

31− rewrite reverseCons x (xs ++ ys) in

32− rewrite reverseAppend xs ys in

33− rewrite reverseCons x xs in

34− sym $ appendAssociative (reverse ys) (reverse xs) [x]

35−

36−||| Reversing a singleton list is a no-op.

37−reverseSingletonId : (x : a) -> reverse [x] = [x]

38−reverseSingletonId _ = Refl

39−

40−||| Reversing a reverse gives the original.

41−reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

42−reverseReverseId [] = Refl

43−reverseReverseId (x :: xs) =

44− rewrite reverseCons x xs in

45− rewrite reverseAppend (reverse xs) [x] in

46− cong $ reverseReverseId xs

libs/contrib/Data/List/Reverse.idrnew file+99

@@ -0,0 +1,99 @@

1+||| Properties of the reverse function.

2+module Data.List.Reverse

4+%default total

5+%access export

7+||| The final segment of the accumulator is the final segment of the result.

8+reverseOntoAcc : (xs, ys, zs : List a) ->

9+ reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs

10+reverseOntoAcc [] _ _ = Refl

11+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

12+

13+||| Serves as a specification for reverseOnto.

14+reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

15+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

16+

17+||| The reverse of an empty list is an empty list. Together with reverseCons,

18+||| serves as a specification for reverse.

19+reverseNil : reverse [] = []

20+reverseNil = Refl

21+

22+||| The reverse of a cons is the reverse of the tail followed by the head.

23+||| Together with reverseNil serves as a specification for reverse.

24+reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]

25+reverseCons x xs = reverseOntoSpec [x] xs

26+

27+||| Reversing an append is appending reversals backwards.

28+reverseAppend : (xs, ys : List a) ->

29+ reverse (xs ++ ys) = reverse ys ++ reverse xs

30+reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))

31+reverseAppend (x :: xs) ys =

32+ rewrite reverseCons x (xs ++ ys) in

33+ rewrite reverseAppend xs ys in

34+ rewrite reverseCons x xs in

35+ sym $ appendAssociative (reverse ys) (reverse xs) [x]

36+

37+||| A recursive definition of reverse.

38+reverseRec : List a -> List a

39+reverseRec [] = []

40+reverseRec (x :: xs) = reverseRec xs ++ [x]

41+

42+||| The iterative and recursive defintions of reverse are the same.

43+reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs

44+reverseEquiv [] = Refl

45+reverseEquiv (x :: xs) =

46+ rewrite reverseEquiv xs in

47+ rewrite reverseAppend [x] xs in

48+ Refl

49+

50+||| Reversing a singleton list is a no-op.

51+reverseSingletonId : (x : a) -> reverse [x] = [x]

52+reverseSingletonId _ = Refl

53+

54+||| Reversing a reverse gives the original.

55+reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

56+reverseReverseId [] = Refl

57+reverseReverseId (x :: xs) =

58+ rewrite reverseCons x xs in

59+ rewrite reverseAppend (reverse xs) [x] in

60+ cong $ reverseReverseId xs

61+

62+||| Reversing onto preserves list length.

63+reverseOntoLength : (xs, acc : List a) ->

64+ length $ reverseOnto acc xs = length acc + length xs

65+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl

66+reverseOntoLength (x :: xs) acc =

67+ rewrite reverseOntoLength xs (x :: acc) in

68+ plusSuccRightSucc (length acc) (length xs)

69+

70+||| Reversing preserves list length.

71+reverseLength : (xs : List a) -> length $ reverse xs = length xs

72+reverseLength xs = reverseOntoLength xs []

73+

74+||| Equal reversed lists are equal.

75+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys

76+reverseEqual xs ys prf =

77+ rewrite sym $ reverseReverseId xs in

78+ rewrite prf in

79+ reverseReverseId ys

80+

81+||| Do geese see God?

82+data Palindrome : (xs : List a) -> Type where

83+ Empty : Palindrome []

84+ Single : Palindrome [_]

85+ Multi : Palindrome xs -> Palindrome $ [x] ++ xs ++ [x]

86+

87+||| A Palindrome reversed is itself.

88+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs

89+palindromeReverse [] Empty = Refl

90+palindromeReverse [_] Single = Refl

91+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =

92+ rewrite reverseAppend ([x] ++ ys) [x] in

93+ rewrite reverseAppend [x] ys in

94+ rewrite palindromeReverse ys pf in

95+ Refl

96+

97+||| Only Palindromes are equal to their own reverse.

98+postulate -- This is a tough one. Any takers?

99+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs

libs/contrib/Data/Nat/Fact.idrnew file+56

@@ -0,0 +1,56 @@

1+||| Properties of factorial functions.

2+module Data.Nat.Fact

4+%access public export

6+%default total

8+||| Recursive definition of factorial.

9+factRec : Nat -> Nat

10+factRec Z = 1

11+factRec (S k) = (S k) * factRec k

12+

13+||| Tail-recursive accumulator for factItr.

14+factAcc : Nat -> Nat -> Nat

15+factAcc Z acc = acc

16+factAcc (S k) acc = factAcc k $ (S k) * acc

17+

18+||| Iterative definition of factorial.

19+factItr : Nat -> Nat

20+factItr n = factAcc n 1

21+

22+----------------------------------------

23+

24+||| Multiplicand-shuffling lemma.

25+multShuffle : (a, b, c : Nat) -> a * (b * c) = b * (a * c)

26+multShuffle a b c =

27+ rewrite multAssociative a b c in

28+ rewrite multCommutative a b in

29+ sym $ multAssociative b a c

30+

31+||| Multiplication of the accumulator.

32+factAccMult : (a, b, c : Nat) ->

33+ a * factAcc b c = factAcc b (a * c)

34+factAccMult _ Z _ = Refl

35+factAccMult a (S k) c =

36+ rewrite factAccMult a k (S k * c) in

37+ rewrite multShuffle a (S k) c in

38+ Refl

39+

40+||| Addition of accumulators.

41+factAccPlus : (a, b, c : Nat) ->

42+ factAcc a b + factAcc a c = factAcc a (b + c)

43+factAccPlus Z _ _ = Refl

44+factAccPlus (S k) b c =

45+ rewrite factAccPlus k (S k * b) (S k * c) in

46+ rewrite sym $ multDistributesOverPlusRight (S k) b c in

47+ Refl

48+

49+||| The recursive and iterative definitions are the equivalent.

50+factRecItr : (n : Nat) -> factRec n = factItr n

51+factRecItr Z = Refl

52+factRecItr (S k) =

53+ rewrite factRecItr k in

54+ rewrite factAccMult k k 1 in

55+ rewrite multOneRightNeutral k in

56+ factAccPlus k 1 k

libs/contrib/Data/Nat/Parity.idr+155−29

@@ -2,18 +2,9 @@ module Data.Nat.Parity

33%access public export

5−--------------------------------------------------------------------------------

6−-- Parity

7−--------------------------------------------------------------------------------

5+----------------------------------------

9−mutual

10− even : Nat -> Bool

11− even Z = True

12− even (S k) = odd k

13−

14− odd : Nat -> Bool

15− odd Z = False

16− odd (S k) = even k

7+-- Type-level, constructive definitions of parity.

178

189||| A nat is Even when it is twice some other nat.

1910Even : Nat -> Type

@@ -23,6 +14,8 @@ Even n = (half : Nat ** n = half * 2)

2314Odd : Nat -> Type

2415Odd n = (haf : Nat ** n = S $ haf * 2)

2516

17+----------------------------------------

18+

2619||| Two more than an Even is Even.

2720add2Even : Even n -> Even (2 + n)

2821add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)

@@ -52,20 +45,73 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf

5245predEvenOdd : Even (S n) -> Odd n

5346predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)

5447

48+----------------------------------------

49+

50+-- Boolean definitions of parity.

51+

52+mutual

53+ even : Nat -> Bool

54+ even Z = True

55+ even (S k) = odd k

56+

57+ odd : Nat -> Bool

58+ odd Z = False

59+ odd (S k) = even k

60+

61+----------------------------------------

62+

63+-- The boolean and type-level definitions are equivalent in the sense

64+-- that a proof of one can be gotten from a proof of the other.

65+

66+mutual

67+ ||| Evens are even.

68+ evenEven : Even n -> even n = True

69+ evenEven {n = Z} _ = Refl

70+ evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

71+

72+ ||| Odds are odd.

73+ oddOdd : Odd n -> odd n = True

74+ oddOdd {n = Z} (_ ** pf) = absurd pf

75+ oddOdd {n = S _} pf = evenEven $ predOddEven pf

76+

77+mutual

78+ ||| If it's even, it's Even.

79+ evenEvenConverse : even n = True -> Even n

80+ evenEvenConverse {n = Z} prf = (0 ** Refl)

81+ evenEvenConverse {n = S k} prf =

82+ let (haf ** pf) = oddOddConverse prf in

83+ (S haf ** cong pf)

84+

85+ ||| If it's odd, it's Odd

86+ oddOddConverse : odd n = True -> Odd n

87+ oddOddConverse {n = Z} prf = absurd prf

88+ oddOddConverse {n = S k} prf =

89+ let (half ** pf) = evenEvenConverse prf in

90+ (half ** cong pf)

91+

92+----------------------------------------

93+

94+||| Every nat is either even or odd.

95+evenorodd : (n : Nat) -> Either (even n = True) (odd n = True)

96+evenorodd Z = Left Refl

97+evenorodd (S k) = case evenorodd k of

98+ Left l => Right l

99+ Right r => Left r

100+

55101||| Every nat is either Even or Odd.

56102evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)

57−evenOrOdd Z = Left (0 ** Refl)

58−evenOrOdd (S k) = case evenOrOdd k of

59− Left (half ** pf) => Right (half ** cong {f = S} pf)

60− Right (haf ** pf) => Left (S haf ** cong {f = S} pf)

103+evenOrOdd n = case evenorodd n of

104+ Left e => Left $ evenEvenConverse e

105+ Right o => Right $ oddOddConverse o

106+

107+||| No nat is both even and odd.

108+notevenandodd : even n = True -> odd n = True -> Void

109+notevenandodd {n = Z} en on = absurd on

110+notevenandodd {n = S _} en on = notevenandodd on en

61111

62112||| No nat is both Even and Odd.

63113notEvenAndOdd : Even n -> Odd n -> Void

64−notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd

65−notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =

66− notEvenAndOdd {n = k}

67− (haf ** cong {f = Nat.pred} odd)

68− (pred half ** succDoublePredPred even)

114+notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)

69115

70116||| Evenness is decidable.

71117evenDec : (n : Nat) -> Dec $ Even n

@@ -79,13 +125,93 @@ oddDec n = case evenOrOdd n of

79125 Left even => No $ notEvenAndOdd even

80126 Right odd => Yes odd

81127

82−mutual

83− ||| Evens are even.

84− evenEven : Even n -> even n = True

85− evenEven {n = Z} _ = Refl

86− evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

128+----------------------------------------

129+

130+||| An Odd is the successor of an Even.

131+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))

132+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))

133+

134+||| Even plus Even is Even.

135+evenPlusEven : Even j -> Even k -> Even (j + k)

136+evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =

137+ (half_j + half_k **

138+ rewrite pf_j in

139+ rewrite pf_k in

140+ sym $ multDistributesOverPlusLeft half_j half_k 2)

141+

142+||| Odd plus Even is Odd.

143+oddPlusEven : Odd j -> Even k -> Odd (j + k)

144+oddPlusEven oj ek =

145+ let

146+ (i ** (ipj, ei)) = oddSuccEven oj

147+ (half_ik ** eik) = evenPlusEven ei ek

148+ in

149+ (half_ik **

150+ rewrite ipj in

151+ cong {f = S} eik)

152+

153+||| Even plus Odd is Odd.

154+evenPlusOdd : Even j -> Odd k -> Odd (j + k)

155+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej

156+

157+||| Odd plus Odd is Even.

158+oddPlusOdd : Odd j -> Odd k -> Even (j + k)

159+oddPlusOdd oj ok =

160+ let

161+ (i ** (ipj, ei)) = oddSuccEven oj

162+ (haf_ik ** oik) = evenPlusOdd ei ok

163+ in

164+ (S haf_ik **

165+ rewrite ipj in

166+ rewrite oik in

167+ Refl)

87168

88− ||| Odds are odd.

89− oddOdd : Odd n -> odd n = True

90− oddOdd {n = Z} (_ ** pf) = absurd pf

91− oddOdd {n = S _} pf = evenEven $ predOddEven pf

169+||| A helper fact.

170+multShuffle : (a, b, c : Nat) ->

171+ (a * c) * (b * c) = ((a * b) * c) * c

172+multShuffle a b c =

173+ rewrite multAssociative (a * c) b c in

174+ rewrite multCommutative (a * c) b in

175+ rewrite multAssociative b a c in

176+ rewrite multCommutative b a in

177+ Refl

178+

179+||| Even times Even is Even.

180+evenMultEven : Even j -> Even k -> Even (j * k)

181+evenMultEven (half_j ** pf_j) (half_k ** pf_k) =

182+ (half_j * half_k * 2 **

183+ rewrite pf_j in

184+ rewrite pf_k in

185+ multShuffle half_j half_k 2)

186+

187+||| Odd times Even is Even.

188+oddMultEven : Odd j -> Even k -> Even (j * k)

189+oddMultEven oj (half_k ** pf_k) =

190+ let

191+ (i ** (ipj, ei)) = oddSuccEven oj

192+ (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)

193+ in

194+ (half_k + half_ik **

195+ rewrite multDistributesOverPlusLeft half_k half_ik 2 in

196+ rewrite ipj in

197+ rewrite oik in

198+ rewrite pf_k in

199+ Refl)

200+

201+||| Even times Odd is Even.

202+evenMultOdd : Even j -> Odd k -> Even (j * k)

203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej

204+

205+||| Odd times Odd is Odd.

206+oddMultOdd : Odd j -> Odd k -> Odd (j * k)

207+oddMultOdd oj (haf_k ** pf_k) =

208+ let

209+ (i ** (ipj, ei)) = oddSuccEven oj

210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)

211+ in

212+ (haf_k + half_ik **

213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in

214+ rewrite ipj in

215+ rewrite eik in

216+ rewrite pf_k in

217+ Refl)

libs/contrib/contrib.ipkg+1−1

@@ -43,7 +43,7 @@ modules = CFFI

4343 , Data.Heap

4444 , Data.IOArray

4545 , Data.List.Zipper

46− , Data.List.Extra

46+ , Data.List.Reverse

4747

4848 , Data.Matrix

4949 , Data.Matrix.Algebraic

libs/prelude/Prelude/File.idr+3−2

@@ -150,7 +150,8 @@ do_getFileAccessTime h =

150150private

151151do_getFileModifiedTime : Ptr -> IO Integer

152152do_getFileModifiedTime h =

153− do MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> IO (Raw Integer)) h

153+ do vm <- getMyVM

154+ MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> Ptr -> IO (Raw Integer)) vm h

154155 pure i

155156

156157private

@@ -175,7 +176,7 @@ export

175176fileModifiedTime : File -> IO (Either FileError Integer)

176177fileModifiedTime (FHandle h)

177178 = do s <- do_getFileModifiedTime h

178− if (s < 0)

179+ if (s == -1)

179180 then Left <$> getFileError

180181 else pure (Right s)

181182

libs/prelude/Prelude/Nat.idr+32−61

@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =

512512

513513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->

514514 (p : left + right = left' + right) -> left = left'

515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in

516− rewrite sym (plusZeroRightNeutral left') in

517− p

518−plusRightCancel left left' (S right) p =

519− plusRightCancel left left' right

520− (succInjective _ _ (rewrite plusSuccRightSucc left right in

521− rewrite plusSuccRightSucc left' right in p))

515+plusRightCancel left left' right p =

516+ plusLeftCancel right left left' $

517+ rewrite plusCommutative right left in

518+ rewrite plusCommutative right left' in

519+ p

522520

523521total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->

524522 (p : left + right = left) -> right = Z

525−plusLeftLeftRightZero Z right p = p

526−plusLeftLeftRightZero (S left) right p =

527− plusLeftLeftRightZero left right (succInjective _ _ p)

523+plusLeftLeftRightZero left right p =

524+ plusLeftCancel left right Z $

525+ rewrite plusZeroRightNeutral left in

526+ p

528527

529528-- Mult

530529total multZeroLeftZero : (right : Nat) -> Z * right = Z

@@ -558,27 +557,21 @@ multCommutative (S left) right =

558557 rewrite multRightSuccPlus right left in

559558 Refl

560559

561−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

562− left * (centre + right) = (left * centre) + (left * right)

563−multDistributesOverPlusRight Z centre right = Refl

564−multDistributesOverPlusRight (S left) centre right =

565− let inductiveHypothesis = multDistributesOverPlusRight left centre right in

566− rewrite inductiveHypothesis in

567− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in

568− rewrite sym (plusAssociative centre (mult left centre) right) in

569− rewrite plusCommutative (mult left centre) right in

570− rewrite plusAssociative centre right (mult left centre) in

571− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in

572− Refl

573−

574560total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

575561 (left + centre) * right = (left * right) + (centre * right)

576−multDistributesOverPlusLeft Z centre right = Refl

577−multDistributesOverPlusLeft (S left) centre right =

578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in

579− rewrite inductiveHypothesis in

580− rewrite plusAssociative right (mult left right) (mult centre right) in

581− Refl

562+multDistributesOverPlusLeft Z centre right = Refl

563+multDistributesOverPlusLeft (S k) centre right =

564+ rewrite multDistributesOverPlusLeft k centre right in

565+ rewrite plusAssociative right (k * right) (centre * right) in

566+ Refl

567+

568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

569+ left * (centre + right) = (left * centre) + (left * right)

570+multDistributesOverPlusRight left centre right =

571+ rewrite multCommutative left (centre + right) in

572+ rewrite multCommutative left centre in

573+ rewrite multCommutative left right in

574+ multDistributesOverPlusLeft centre right left

582575

583576total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

584577 left * (centre * right) = (left * centre) * right

@@ -590,18 +583,10 @@ multAssociative (S left) centre right =

590583 Refl

591584

592585total multOneLeftNeutral : (right : Nat) -> 1 * right = right

593−multOneLeftNeutral Z = Refl

594−multOneLeftNeutral (S right) =

595− let inductiveHypothesis = multOneLeftNeutral right in

596− rewrite inductiveHypothesis in

597− Refl

586+multOneLeftNeutral right = plusZeroRightNeutral right

598587

599588total multOneRightNeutral : (left : Nat) -> left * 1 = left

600−multOneRightNeutral Z = Refl

601−multOneRightNeutral (S left) =

602− let inductiveHypothesis = multOneRightNeutral left in

603− rewrite inductiveHypothesis in

604− Refl

589+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left

605590

606591-- Minus

607592total minusSuccSucc : (left : Nat) -> (right : Nat) ->

@@ -689,10 +674,7 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z

689674powerZeroOne base = Refl

690675

691676total powerOneNeutral : (base : Nat) -> power base 1 = base

692−powerOneNeutral Z = Refl

693−powerOneNeutral (S base) =

694− let inductiveHypothesis = powerOneNeutral base in

695− rewrite inductiveHypothesis in Refl

677+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base

696678

697679total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z

698680powerOneSuccOne Z = Refl

@@ -701,8 +683,7 @@ powerOneSuccOne (S exp) =

701683 rewrite inductiveHypothesis in Refl

702684

703685total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base

704−powerSuccSuccMult Z = Refl

705−powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl

686+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl

706687

707688total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

708689 power (power base exp) exp' = power base (exp * exp')

@@ -796,34 +777,24 @@ minimumIdempotent Z = Refl

796777minimumIdempotent (S k) = cong (minimumIdempotent k)

797778

798779total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

799−minimumZeroZeroRight Z = Refl

800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right

780+minimumZeroZeroRight right = Refl

801781

802782total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

803−minimumZeroZeroLeft Z = Refl

804−minimumZeroZeroLeft (S left) = Refl

783+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

805784

806785total minimumSuccSucc : (left : Nat) -> (right : Nat) ->

807786 minimum (S left) (S right) = S (minimum left right)

808−minimumSuccSucc Z Z = Refl

809−minimumSuccSucc (S left) Z = Refl

810−minimumSuccSucc Z (S right) = Refl

811−minimumSuccSucc (S left) (S right) = Refl

787+minimumSuccSucc left right = Refl

812788

813789total maximumZeroNRight : (right : Nat) -> maximum Z right = right

814−maximumZeroNRight Z = Refl

815−maximumZeroNRight (S right) = Refl

790+maximumZeroNRight right = Refl

816791

817792total maximumZeroNLeft : (left : Nat) -> maximum left Z = left

818−maximumZeroNLeft Z = Refl

819−maximumZeroNLeft (S left) = Refl

793+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

820794

821795total maximumSuccSucc : (left : Nat) -> (right : Nat) ->

822796 S (maximum left right) = maximum (S left) (S right)

823−maximumSuccSucc Z Z = Refl

824−maximumSuccSucc (S left) Z = Refl

825−maximumSuccSucc Z (S right) = Refl

826−maximumSuccSucc (S left) (S right) = Refl

797+maximumSuccSucc left right = Refl

827798

828799total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)

829800sucMaxL Z = Refl

rts/idris_bitstring.c−2

@@ -1,5 +1,3 @@

1−#include <assert.h>

2−

31#include "idris_rts.h"

53VAL idris_b8const(VM *vm, uint8_t a) {

rts/idris_rts.c−10

@@ -1158,16 +1158,6 @@ void idris_disableBuffering(void) {

11581158 setvbuf(stdout, NULL, _IONBF, 0);

11591159}

11601160

1161−#ifndef SEL4

1162−int idris_usleep(int usec) {

1163− struct timespec t;

1164− t.tv_sec = usec / 1000000;

1165− t.tv_nsec = (usec % 1000000) * 1000;

1166−

1167− return nanosleep(&t, NULL);

1168−}

1169−#endif // SEL4

1170−

11711161void stackOverflow(void) {

11721162 fprintf(stderr, "Stack overflow");

11731163 exit(-1);

rts/idris_rts.h−4

@@ -507,10 +507,6 @@ const char *idris_getArg(int i);

507507// disable stdin/stdout buffering

508508void idris_disableBuffering(void);

509509

510−#ifndef SEL4

511−int idris_usleep(int usec);

512−#endif // SEL4

513−

514510// Handle stack overflow.

515511// Just reports an error and exits.

516512

rts/idris_stdfgn.c+12−2

@@ -74,13 +74,13 @@ VAL fileAccessTime(void* h) {

7474 }

7575}

7676

77−VAL fileModifiedTime(void* h) {

77+VAL fileModifiedTime(VM* vm, void* h) {

7878 FILE* f = (FILE*)h;

7979 int fd = fileno(f);

8080

8181 struct stat buf;

8282 if (fstat(fd, &buf) == 0) {

83− return MKBIGI(buf.st_mtime);

83+ return MKBIGUI(vm, buf.st_mtime);

8484 } else {

8585 return MKBIGI(-1);

8686 }

@@ -228,6 +228,16 @@ VAL idris_clock(VM* vm) {

228228 return result;

229229}

230230

231+#ifndef SEL4

232+int idris_usleep(int usec) {

233+ struct timespec t;

234+ t.tv_sec = usec / 1000000;

235+ t.tv_nsec = (usec % 1000000) * 1000;

236+

237+ return nanosleep(&t, NULL);

238+}

239+#endif // SEL4

240+

231241VAL idris_mkFileError(VM* vm) {

232242 VAL result;

233243 switch(errno) {

rts/idris_stdfgn.h+4−1

@@ -18,7 +18,7 @@ int fileSize(void* h);

1818

1919// Return a negative number if not a file (e.g. directory or device)

2020VAL fileAccessTime(void* h);

21−VAL fileModifiedTime(void* h);

21+VAL fileModifiedTime(VM* vm, void* h);

2222VAL fileStatusTime(void* h);

2323

2424void* idris_dirOpen(char* dname);

@@ -54,6 +54,9 @@ char* getEnvPair(int i);

5454

5555VAL idris_time();

5656VAL idris_clock(VM* vm);

57+#ifndef SEL4

58+int idris_usleep(int usec);

59+#endif // SEL4

5760

5861void idris_forceGC();

5962

rts/idris_utf8.c−1

@@ -1,5 +1,4 @@

11#include "idris_utf8.h"

2−#include <stdio.h>

32#include <string.h>

43#include <stdlib.h>

src/Idris/CmdOptions.hs+3−2

@@ -18,6 +18,7 @@ import Idris.Info (getIdrisVersion)

1818import Idris.Options

1919import IRTS.CodegenCommon

2020

21+import qualified Control.Monad.Fail as Fail

2122import Control.Monad.Trans (lift)

2223import Control.Monad.Trans.Except (throwE)

2324import Control.Monad.Trans.Reader (ask)

@@ -264,7 +265,7 @@ parseCodegen :: String -> Codegen

264265parseCodegen "bytecode" = Bytecode

265266parseCodegen cg = Via IBCFormat (map toLower cg)

266267

267−parseLogCats :: Monad m => String -> m [LogCat]

268+parseLogCats :: Fail.MonadFail m => String -> m [LogCat]

268269parseLogCats s =

269270 case lastMay (readP_to_S doParse s) of

270271 Just (xs, _) -> return xs

@@ -290,7 +291,7 @@ parseLogCats s =

290291 s <- look

291292 fail $ "Category: " ++ s ++ " is not recognised."

292293

293−parseConsoleWidth :: Monad m => String -> m ConsoleWidth

294+parseConsoleWidth :: Fail.MonadFail m => String -> m ConsoleWidth

294295parseConsoleWidth "auto" = return AutomaticWidth

295296parseConsoleWidth "infinite" = return InfinitelyWide

296297parseConsoleWidth s =

src/Idris/Core/CaseTree.hs+1−1

@@ -627,7 +627,7 @@ groupCons cs = gc [] cs

627627 PConst cval -> return $ addConG cval (ps, res) acc

628628 PSuc n -> return $ addg False CSuc [n] (ps, res) acc

629629 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc

630− pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

630+ pat -> error $ show pat ++ " is not a constructor or constant (can't happen)"

631631

632632 addg uniq c conargs res []

633633 = [ConGroup uniq c [(conargs, res)]]

src/Idris/Core/TT.hs+6

@@ -70,6 +70,7 @@ import qualified Prelude as S (Semigroup(..))

7070import Control.Applicative (Alternative, Applicative(..))

7171import qualified Control.Applicative as A (Alternative(..))

7272import Control.DeepSeq (($!!))

73+import qualified Control.Monad.Fail as Fail

7374import Control.Monad.State.Strict

7475import Data.Binary hiding (get, put)

7576import Data.Char

@@ -324,6 +325,11 @@ bindTC x k = case x of

324325instance Monad TC where

325326 return x = OK x

326327 x >>= k = bindTC x k

328+#if !(MIN_VERSION_base(4,13,0))

329+ fail = Fail.fail

330+#endif

331+

332+instance Fail.MonadFail TC where

327333 fail e = Error (InternalMsg e)

328334

329335instance MonadPlus TC where

src/Idris/Parser/Stack.hs+16−2

@@ -5,7 +5,7 @@ Description : Idris parser stack and its primitives.

55License : BSD3

66Maintainer : The Idris Community.

77-}

8−{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

8+{-# LANGUAGE CPP, ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

99module Idris.Parser.Stack

1010 ( -- * Parsing

1111 Parser(..)

@@ -36,6 +36,7 @@ import Idris.Core.TT (FC(..))

3636import Idris.Output (Message(..))

3737

3838import Control.Arrow (app)

39+import qualified Control.Monad.Fail as Fail

3940import Control.Monad.State.Strict (StateT(..), evalStateT)

4041import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,

4142 runWriterT, tell)

@@ -51,7 +52,7 @@ import qualified Util.Pretty as PP

5152type Parser s = StateT s (WriterT FC (P.Parsec Void String))

5253

5354-- | A constraint for parsing without state

54−type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)

55+type Parsing m = (Fail.MonadFail m, P.MonadParsec Void String m, MonadWriter FC m)

5556

5657-- | Run the Idris parser stack

5758runparser :: Parser st res -> st -> String -> String -> Either ParseError res

@@ -76,11 +77,20 @@ parseErrorOffset = P.errorOffset . parseError

7677instance Message ParseError where

7778 messageExtent err = sourcePositionFC pos

7879 where

80+#if MIN_VERSION_megaparsec(8,0,0)

81+ P.PosState {P.pstateSourcePos = pos} =

82+ P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

83+#else

7984 (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

85+#endif

8086 messageText = PP.text . init . P.parseErrorTextPretty . parseError

8187 messageSource err = Just sline

8288 where

89+#if MIN_VERSION_megaparsec(8,0,0)

90+ (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

91+#else

8392 (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

93+#endif

8494

8595-- | A fully formatted parse error, with caret and bar, etc.

8696prettyError :: ParseError -> String

@@ -88,7 +98,11 @@ prettyError = P.errorBundlePretty . unParseError

8898

8999{- * Mark and restore -}

90100

101+#if MIN_VERSION_megaparsec(8,0,0)

102+type Mark = P.State String Void

103+#else

91104type Mark = P.State String

105+#endif

92106

93107-- | Retrieve the parser state so we can restart from this point later.

94108mark :: Parsing m => m Mark

stack-11.22.yamlnew file+21

@@ -0,0 +1,21 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-11.22

4+extra-deps:

5+- cheapskate-0.1.1.2

6+- megaparsec-7.0.5

7+- Cabal-2.4.1.0

8+- network-3.1.1.1

9+- parser-combinators-1.0.0

10+

11+flags:

12+ idris:

13+ FFI: true

14+ GMP: true

15+

16+ghc-options:

17+ idris: -fwarn-unused-imports -fwarn-unused-binds

18+

19+nix:

20+ enable: false

21+ shell-file: stack-shell.nix

stack-12.26.yamlnew file+20

@@ -0,0 +1,20 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-12.26

4+extra-deps:

5+- cheapskate-0.1.1.2

6+- megaparsec-7.0.5

7+- Cabal-2.4.1.0

8+- network-3.1.1.1

10+flags:

11+ idris:

12+ FFI: true

13+ GMP: true

14+

15+ghc-options:

16+ idris: -fwarn-unused-imports -fwarn-unused-binds

17+

18+nix:

19+ enable: false

20+ shell-file: stack-shell.nix

stack-15.3.yamlnew file+17

@@ -0,0 +1,17 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-15.3

4+extra-deps:

5+- cheapskate-0.1.1.2

7+flags:

8+ idris:

9+ FFI: true

10+ GMP: true

11+

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

15+nix:

16+ enable: false

17+ shell-file: stack-shell.nix

stack-15.4.yamlnew file+17

@@ -0,0 +1,17 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-15.4

4+extra-deps:

5+- cheapskate-0.1.1.2

7+flags:

8+ idris:

9+ FFI: true

10+ GMP: true

11+

12+ghc-options:

13+ idris: -fwarn-unused-imports -fwarn-unused-binds

14+

15+nix:

16+ enable: false

17+ shell-file: stack-shell.nix

stack-alt.yamldeleted−25

@@ -1,25 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-11.4

3−

4−packages:

5− - location: .

6−

7−extra-deps:

8− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

9− - Cabal-2.2.0.1@sha256:2a80d8fb655474f0eaeb20434c47f64f84e6302e55973056f00df8ca050b9683

10− - megaparsec-7.0.4

11− - parser-combinators-1.0.0

12− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

13− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

14−

15−flags:

16− idris:

17− FFI: true

18− GMP: true

19−

20−ghc-options:

21− idris: -fwarn-unused-imports -fwarn-unused-binds

22−

23−nix:

24− enable: false

25− shell-file: stack-shell.nix

stack.yamlmode 100644 → 120000+1−24

@@ -1,24 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-13.21

3−

4−extra-deps:

5− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

6− - megaparsec-7.0.4

7− - parser-combinators-1.0.0

8− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

9− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

10− - tasty-rerun-1.1.14@sha256:ba9c19a281535bea566e1044bc02c36ef17abcb310af4b6a149ec11780c7ce35

11− - binary-0.8.7.0@sha256:ae3e6cca723ac55c54bbb3fa771bcf18142bc727afd57818e66d6ee6c8044f12

12− - text-1.2.4.0@sha256:8c24450feb8e3bbb7ea3e17af24ef57e85db077c4bf53e5bcc345b283d1b1d5b

13−

14−flags:

15− idris:

16− FFI: true

17− GMP: true

18−

19−ghc-options:

20− idris: -fwarn-unused-imports -fwarn-unused-binds

21−

22−nix:

23− enable: false

24− shell-file: stack-shell.nix

@@ -0,0 +1 @@

1+stack-15.4.yaml

test/README.md+5−5

@@ -113,18 +113,18 @@ and somewhat self-explanatory.

113113

1141141. Choose the family your test shall belong to and remember its identifier.

1151152. Pick the next available integer in the test family. It will be the index.

116−3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run` script.

116+3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run.sh` script.

1171174. Modify the `run` script to your liking. If you want to call the idris executable, write `${IDRIS:-idris} $@`.

1181185. Add any file you may need in the directory. If they don't end in `.idr`, you should remember them for the next step.

1191196. Add your test in `TestData.hs`. Each family has a list of `(Index, CompatCodegen)`. See the next section for the available values in `CompatCodegen`. In most cases, you should write `( 42, ANY)`.

120−7. Generate the `expected` file by doing:

120+7. Generate the `expected.out` file by doing:

121121 ```

122122 # Using cabal

123123 cabal test --test-options="--pattern foo042 --accept"

124124 # Using stack

125125 stack test --test-arguments="--pattern foo042 --accept"

126126 ```

127−8. Check the content of `expected`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

127+8. Check the content of `expected.out`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

128128

129129### Specifying compatible backends

130130

@@ -146,7 +146,7 @@ Currently, `NONE` has the same effect as `ANY`, but this will change.

146146

147147### Updating golden files

148148

149−To update the `expected` file for every test, do one of the following:

149+To update the `expected.out` file for every test, do one of the following:

150150

151151```

152152# Using make

@@ -157,4 +157,4 @@ cabal test --test-options="--accept"

157157stack test --test-arguments="--accept"

158158```

159159

160−"Accepted" tests are the ones that update the golden file. A test can still fail if the `run` script itself crashes.

160+"Accepted" tests are the ones that update the golden file. A test can still fail if the `run.sh` script itself crashes.

test/TestRun.hs+2−2

@@ -62,7 +62,7 @@ ingredients = defaultIngredients ++

6262test :: String -> String -> IO () -> TestTree

6363test testName path = goldenVsFileDiff testName diff ref output

6464 where

65− ref = path </> "expected"

65+ ref = path </> "expected.out"

6666 output = path </> "output"

6767 diff ref new | os == "openbsd" = ["diff", "-u", new, ref]

6868 | otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]

@@ -92,7 +92,7 @@ mkGoldenTests testFamilies flags =

9292-- this thing.

9393runTest :: String -> Flags -> IO ()

9494runTest path flags = do

95− let run = (proc "bash" ("run" : flags)) {cwd = Just path}

95+ let run = (proc "bash" ("run.sh" : flags)) {cwd = Just path}

9696 (_, output, error_out) <- readCreateProcessWithExitCode run ""

9797 writeFile (path </> "output") (normalise output)

9898 when (error_out /= "") $ hPutStrLn stderr ("\nError: " ++ path ++ "\n" ++ error_out)

test/base001/expected → test/base001/expected.outrenamed

The content is the same.

test/base001/run → test/base001/run.shrenamed+1−1

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

33set -u

55if [[ ${OSTYPE} = 'msys' ]]; then

6− cat expected # skip this test on Windows

6+ cat expected.out # skip this test on Windows

77else

88 ${IDRIS:-idris} "$@" --build base001.ipkg | grep -v 'make.*:'

99 ./base001 2>&1 | grep -v '^sh:.*\./does-not-exist:'

test/basic001/expected → test/basic001/expected.outrenamed

The content is the same.

test/basic001/run → test/basic001/run.shrenamed

Only the mode changed.

test/basic002/expected → test/basic002/expected.outrenamed

The content is the same.

test/basic002/run → test/basic002/run.shrenamed

Only the mode changed.

test/basic003/expected → test/basic003/expected.outrenamed

The content is the same.

test/basic003/run → test/basic003/run.shrenamed

Only the mode changed.

test/basic004/expected → test/basic004/expected.outrenamed

The content is the same.

test/basic004/run → test/basic004/run.shrenamed

Only the mode changed.

test/basic005/expected → test/basic005/expected.outrenamed

The content is the same.

test/basic005/run → test/basic005/run.shrenamed

Only the mode changed.

test/basic006/expected → test/basic006/expected.outrenamed

The content is the same.

test/basic006/run → test/basic006/run.shrenamed

Only the mode changed.

test/basic007/expected → test/basic007/expected.outrenamed

The content is the same.

test/basic007/run → test/basic007/run.shrenamed

Only the mode changed.

test/basic008/expected → test/basic008/expected.outrenamed

The content is the same.

test/basic008/run → test/basic008/run.shrenamed

Only the mode changed.

test/basic009/expected → test/basic009/expected.outrenamed

The content is the same.

test/basic009/run → test/basic009/run.shrenamed

Only the mode changed.

test/basic010/expected → test/basic010/expected.outrenamed

The content is the same.

test/basic010/run → test/basic010/run.shrenamed

Only the mode changed.

test/basic011/expected → test/basic011/expected.outrenamed

The content is the same.

test/basic011/run → test/basic011/run.shrenamed

Only the mode changed.

test/basic012/expected → test/basic012/expected.outrenamed

The content is the same.

test/basic012/run → test/basic012/run.shrenamed

Only the mode changed.

test/basic013/expected → test/basic013/expected.outrenamed

The content is the same.

test/basic013/run → test/basic013/run.shrenamed

Only the mode changed.

test/basic014/expected → test/basic014/expected.outrenamed

The content is the same.

test/basic014/run → test/basic014/run.shrenamed

Only the mode changed.

test/basic015/expected → test/basic015/expected.outrenamed

The content is the same.

test/basic015/run → test/basic015/run.shrenamed

Only the mode changed.

test/basic016/expected → test/basic016/expected.outrenamed

The content is the same.

test/basic016/run → test/basic016/run.shrenamed

Only the mode changed.

test/basic017/expected → test/basic017/expected.outrenamed

The content is the same.

test/basic017/run → test/basic017/run.shrenamed

Only the mode changed.

test/basic018/expected → test/basic018/expected.outrenamed

The content is the same.

test/basic018/run → test/basic018/run.shrenamed

Only the mode changed.

test/basic019/expected → test/basic019/expected.outrenamed

The content is the same.

test/basic019/run → test/basic019/run.shrenamed

Only the mode changed.

test/basic020/expected → test/basic020/expected.outrenamed

The content is the same.

test/basic020/run → test/basic020/run.shrenamed

Only the mode changed.

test/basic021/expected → test/basic021/expected.outrenamed

The content is the same.

test/basic021/run → test/basic021/run.shrenamed

Only the mode changed.

test/basic022/expected → test/basic022/expected.outrenamed

The content is the same.

test/basic022/run → test/basic022/run.shrenamed

Only the mode changed.

test/basic023/expected → test/basic023/expected.outrenamed

The content is the same.

test/basic023/run → test/basic023/run.shrenamed

Only the mode changed.

test/basic024/expected → test/basic024/expected.outrenamed

The content is the same.

test/basic024/input → test/basic024/input.inrenamed

The content is the same.

test/basic024/run → test/basic024/run.shrenamed+1−1

@@ -1,6 +1,6 @@

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none < input

3+${IDRIS:-idris} $@ --quiet --port none < input.in

44${IDRIS:-idris} $@ basic024.idr -o basic024

66./basic024

test/basic025/expected → test/basic025/expected.outrenamed

The content is the same.

test/basic025/input → test/basic025/input.inrenamed

The content is the same.

test/basic025/run → test/basic025/run.shrenamed+2−2

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none < input

2+${IDRIS:-idris} $@ --quiet --port none < input.in

33${IDRIS:-idris} $@ -o basic025 basic025.idr

5−./basic025 input

5+./basic025 input.in

77rm -f basic025 *.ibc

test/basic026/expected → test/basic026/expected.outrenamed

The content is the same.

test/basic026/run → test/basic026/run.shrenamed

The content is the same.

test/bignum001/expected → test/bignum001/expected.outrenamed

The content is the same.

test/bignum001/run → test/bignum001/run.shrenamed

Only the mode changed.

test/bignum002/expected → test/bignum002/expected.outrenamed

The content is the same.

test/bignum002/run → test/bignum002/run.shrenamed

Only the mode changed.

test/bignum003/expected → test/bignum003/expected.outrenamed

The content is the same.

test/bignum003/run → test/bignum003/run.shrenamed

Only the mode changed.

test/bounded001/expected → test/bounded001/expected.outrenamed

The content is the same.

test/bounded001/run → test/bounded001/run.shrenamed

Only the mode changed.

test/buffer001/expected → test/buffer001/expected.outrenamed

The content is the same.

test/buffer001/run → test/buffer001/run.shrenamed

Only the mode changed.

test/buffer002/expected → test/buffer002/expected.outrenamed

The content is the same.

test/buffer002/run → test/buffer002/run.shrenamed

Only the mode changed.

test/contrib001/expected → test/contrib001/expected.outrenamed

The content is the same.

test/contrib001/run → test/contrib001/run.shrenamed

Only the mode changed.

test/corecords001/expected → test/corecords001/expected.outrenamed

The content is the same.

test/corecords001/run → test/corecords001/run.shrenamed

Only the mode changed.

test/corecords002/expected → test/corecords002/expected.outrenamed

The content is the same.

test/corecords002/run → test/corecords002/run.shrenamed

Only the mode changed.

test/delab001/expected → test/delab001/expected.outrenamed

The content is the same.

test/delab001/input → test/delab001/input.inrenamed

The content is the same.

test/delab001/run → test/delab001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input.in

33rm -f *.ibc

test/directives001/expected → test/directives001/expected.outrenamed

The content is the same.

test/directives001/run → test/directives001/run.shrenamed

Only the mode changed.

test/directives002/expected → test/directives002/expected.outrenamed

The content is the same.

test/directives002/run → test/directives002/run.shrenamed

The content is the same.

test/directives003/expected → test/directives003/expected.outrenamed

The content is the same.

test/directives003/run → test/directives003/run.shrenamed

Only the mode changed.

test/disambig002/expected → test/disambig002/expected.outrenamed

The content is the same.

test/disambig002/run → test/disambig002/run.shrenamed

Only the mode changed.

test/docs001/expected → test/docs001/expected.outrenamed

The content is the same.

test/docs001/input → test/docs001/input.inrenamed

The content is the same.

test/docs001/run → test/docs001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input.in

33rm *.ibc

test/docs002/expected → test/docs002/expected.outrenamed

The content is the same.

test/docs002/input → test/docs002/input.inrenamed

The content is the same.

test/docs002/run → test/docs002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input

2+${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input.in

33rm *.ibc

test/docs003/expected → test/docs003/expected.outrenamed

The content is the same.

test/docs003/input → test/docs003/input.inrenamed

The content is the same.

test/docs003/run → test/docs003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input.in

33rm *.ibc

test/docs004/expected → test/docs004/expected.outrenamed

The content is the same.

test/docs004/input → test/docs004/input.inrenamed

The content is the same.

test/docs004/run → test/docs004/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input.in

33rm *.ibc

test/docs005/expected → test/docs005/expected.outrenamed

The content is the same.

test/docs005/input → test/docs005/input.inrenamed

The content is the same.

test/docs005/run → test/docs005/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input.in

33rm *.ibc

test/docs006/expected → test/docs006/expected.outrenamed

The content is the same.

test/docs006/input → test/docs006/input.inrenamed

The content is the same.

test/docs006/run → test/docs006/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input.in

33rm *.ibc

test/dsl001/expected → test/dsl001/expected.outrenamed

The content is the same.

test/dsl001/input → test/dsl001/input.inrenamed

The content is the same.

test/dsl001/run → test/dsl001/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ test001.idr -o test001 --partial-eval

33./test001

4−${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input

4+${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input.in

55rm -f test001 test001.ibc

test/dsl002/expected → test/dsl002/expected.outrenamed

The content is the same.

test/dsl002/run → test/dsl002/run.shrenamed

Only the mode changed.

test/dsl002/test → test/dsl002/test.inrenamed

The content is the same.

test/dsl002/test014.idr+1−1

@@ -64,6 +64,6 @@ readH fn = res (do let x = open fn Reading

6464 else rputStrLn "Error")

6565

6666main : IO ()

67−main = run (readH "test")

67+main = run (readH "test.in")

6868

6969

test/dsl003/expected → test/dsl003/expected.outrenamed

The content is the same.

test/dsl003/run → test/dsl003/run.shrenamed

Only the mode changed.

test/dsl004/expected → test/dsl004/expected.outrenamed

The content is the same.

test/dsl004/run → test/dsl004/run.shrenamed

Only the mode changed.

test/effects001/expected → test/effects001/expected.outrenamed

The content is the same.

test/effects001/run → test/effects001/run.shrenamed

Only the mode changed.

test/effects001/test021.idr+1−1

@@ -31,7 +31,7 @@ readFileCount = readAcc []

3131

3232testFile : TestFileIO () ()

3333testFile = do

34− Success <- open "testFile" Read

34+ Success <- open "testFile.in" Read

3535 | (FError err) => do

3636 putStrLn "Error!"

3737 pure ()

test/effects001/testFile → test/effects001/testFile.inrenamed

The content is the same.

test/effects002/expected → test/effects002/expected.outrenamed

The content is the same.

test/effects002/run → test/effects002/run.shrenamed

Only the mode changed.

test/effects003/expected → test/effects003/expected.outrenamed

The content is the same.

test/effects003/input → test/effects003/input.inrenamed

The content is the same.

test/effects003/run → test/effects003/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ hangman.idr --nocolour -p effects -o hangman

3−./hangman < input

3+./hangman < input.in

44rm -f hangman *.ibc

test/effects004/expected → test/effects004/expected.outrenamed

The content is the same.

test/effects004/input → test/effects004/input.inrenamed

The content is the same.

test/effects004/run → test/effects004/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ effects004.idr -o effects004 -p effects

3−./effects004 < input

3+./effects004 < input.in

44rm -f effects004 *.ibc

test/effects005/expected → test/effects005/expected.outrenamed

The content is the same.

test/effects005/run → test/effects005/run.shrenamed

Only the mode changed.

test/error001/expected → test/error001/expected.outrenamed

The content is the same.

test/error001/run → test/error001/run.shrenamed

Only the mode changed.

test/error002/expected → test/error002/expected.outrenamed

The content is the same.

test/error002/run → test/error002/run.shrenamed

Only the mode changed.

test/error003/expected → test/error003/expected.outrenamed

The content is the same.

test/error003/run → test/error003/run.shrenamed

Only the mode changed.

test/error004/expected → test/error004/expected.outrenamed

The content is the same.

test/error004/run → test/error004/run.shrenamed

Only the mode changed.

test/error005/expected → test/error005/expected.outrenamed

The content is the same.

test/error005/run → test/error005/run.shrenamed

Only the mode changed.

test/error006/expected → test/error006/expected.outrenamed

The content is the same.

test/error006/run → test/error006/run.shrenamed

Only the mode changed.

test/error007/expected → test/error007/expected.outrenamed

The content is the same.

test/error007/run → test/error007/run.shrenamed

Only the mode changed.

test/error008/expected → test/error008/expected.outrenamed

The content is the same.

test/error008/run → test/error008/run.shrenamed

Only the mode changed.

test/error009/expected → test/error009/expected.outrenamed

The content is the same.

test/error009/run → test/error009/run.shrenamed

Only the mode changed.

test/ffi001/expected → test/ffi001/expected.outrenamed

The content is the same.

test/ffi001/run → test/ffi001/run.shrenamed

Only the mode changed.

test/ffi002/expected → test/ffi002/expected.outrenamed

The content is the same.

test/ffi002/run → test/ffi002/run.shrenamed

Only the mode changed.

test/ffi003/expected → test/ffi003/expected.outrenamed

The content is the same.

test/ffi003/input → test/ffi003/input.inrenamed

The content is the same.

test/ffi003/run → test/ffi003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input.in

33rm -f *.ibc

test/ffi004/expected → test/ffi004/expected.outrenamed

The content is the same.

test/ffi004/run → test/ffi004/run.shrenamed

Only the mode changed.

test/ffi005/expected → test/ffi005/expected.outrenamed

The content is the same.

test/ffi005/run → test/ffi005/run.shrenamed

Only the mode changed.

test/ffi006/expected → test/ffi006/expected.outrenamed

The content is the same.

test/ffi006/run → test/ffi006/run.shrenamed

Only the mode changed.

test/ffi007/expected → test/ffi007/expected.outrenamed

The content is the same.

test/ffi007/run → test/ffi007/run.shrenamed

The content is the same.

test/ffi008/expected → test/ffi008/expected.outrenamed

The content is the same.

test/ffi008/run → test/ffi008/run.shrenamed

The content is the same.

test/ffi009/expected → test/ffi009/expected.outrenamed

The content is the same.

test/ffi009/run → test/ffi009/run.shrenamed

Only the mode changed.

test/ffi010/expected → test/ffi010/expected.outrenamed

The content is the same.

test/ffi010/run → test/ffi010/run.shrenamed

Only the mode changed.

test/ffi011/expected → test/ffi011/expected.outrenamed

The content is the same.

test/ffi011/ffi011 → test/ffi011/ffi011.jsrenamed

The content is the same.

test/ffi011/run → test/ffi011/run.shrenamed+1−1

@@ -1,4 +1,4 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ ffi011.idr --interface -o lib.js

3−node ./ffi011

3+node ./ffi011.js

44rm -f *.ibc lib.js

test/ffi012/expected → test/ffi012/expected.outrenamed

The content is the same.

test/ffi012/ffi012 → test/ffi012/ffi012.jsrenamed

The content is the same.

test/ffi012/run → test/ffi012/run.shrenamed

Only the mode changed.

test/ffi013/expected → test/ffi013/expected.outrenamed

The content is the same.

test/ffi013/run → test/ffi013/run.shrenamed

Only the mode changed.

test/folding001/expected → test/folding001/expected.outrenamed

The content is the same.

test/folding001/run → test/folding001/run.shrenamed

Only the mode changed.

test/idrisdoc001/expected → test/idrisdoc001/expected.outrenamed

The content is the same.

test/idrisdoc001/run → test/idrisdoc001/run.shrenamed

Only the mode changed.

test/idrisdoc002/expected → test/idrisdoc002/expected.outrenamed

The content is the same.

test/idrisdoc002/run → test/idrisdoc002/run.shrenamed

Only the mode changed.

test/idrisdoc003/expected → test/idrisdoc003/expected.outrenamed

The content is the same.

test/idrisdoc003/run → test/idrisdoc003/run.shrenamed

Only the mode changed.

test/idrisdoc004/expected → test/idrisdoc004/expected.outrenamed

The content is the same.

test/idrisdoc004/run → test/idrisdoc004/run.shrenamed

Only the mode changed.

test/idrisdoc005/expected → test/idrisdoc005/expected.outrenamed

The content is the same.

test/idrisdoc005/run → test/idrisdoc005/run.shrenamed

Only the mode changed.

test/idrisdoc006/expected → test/idrisdoc006/expected.outrenamed

The content is the same.

test/idrisdoc006/run → test/idrisdoc006/run.shrenamed

Only the mode changed.

test/idrisdoc007/expected → test/idrisdoc007/expected.outrenamed

The content is the same.

test/idrisdoc007/run → test/idrisdoc007/run.shrenamed

Only the mode changed.

test/idrisdoc008/expected → test/idrisdoc008/expected.outrenamed

The content is the same.

test/idrisdoc008/run → test/idrisdoc008/run.shrenamed

Only the mode changed.

test/idrisdoc009/expected → test/idrisdoc009/expected.outrenamed

The content is the same.

test/idrisdoc009/input → test/idrisdoc009/input.inrenamed

The content is the same.

test/idrisdoc009/run → test/idrisdoc009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input

2+${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input.in

33rm -f *.ibc

test/interactive001/expected → test/interactive001/expected.outrenamed

The content is the same.

test/interactive001/input → test/interactive001/input.inrenamed

The content is the same.

test/interactive001/run → test/interactive001/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input

3+${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input.in

55rm -f *.ibc

test/interactive002/expected → test/interactive002/expected.outrenamed

The content is the same.

test/interactive002/input → test/interactive002/input.inrenamed

The content is the same.

test/interactive002/run → test/interactive002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input.in

33rm -f *.ibc

test/interactive003/expected → test/interactive003/expected.outrenamed

The content is the same.

test/interactive003/input → test/interactive003/input.inrenamed

The content is the same.

test/interactive003/run → test/interactive003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input.in

33rm -f *.ibc

test/interactive004/expected → test/interactive004/expected.outrenamed

The content is the same.

test/interactive004/input → test/interactive004/input.inrenamed

The content is the same.

test/interactive004/run → test/interactive004/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input.in

33rm -f *.ibc

test/interactive005/expected → test/interactive005/expected.outrenamed

The content is the same.

test/interactive005/input → test/interactive005/input.inrenamed

The content is the same.

test/interactive005/run → test/interactive005/run.shrenamed+1−1

@@ -1,5 +1,5 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input

2+${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input.in

33rm -f *.ibc

44rm -f hello.bytecode

55rm -f hello

test/interactive006/expected → test/interactive006/expected.outrenamed

The content is the same.

test/interactive006/input → test/interactive006/input.inrenamed

The content is the same.

test/interactive006/run → test/interactive006/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input.in

33rm -f *.ibc

test/interactive007/expected → test/interactive007/expected.outrenamed

The content is the same.

test/interactive007/input → test/interactive007/input.inrenamed

The content is the same.

test/interactive007/run → test/interactive007/run.shrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input | perl -pe 's-Data\\Z-Data/Z-g'

2+${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input.in | perl -pe 's-Data\\Z-Data/Z-g'

test/interactive008/expected → test/interactive008/expected.outrenamed

The content is the same.

test/interactive008/input → test/interactive008/input.inrenamed

The content is the same.

test/interactive008/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --port none < input

test/interactive008/run.shnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nobanner --nocolor --port none < input.in

test/interactive009/expected → test/interactive009/expected.outrenamed

The content is the same.

test/interactive009/input → test/interactive009/input.inrenamed

The content is the same.

test/interactive009/run → test/interactive009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input.in

33rm -f *.ibc

test/interactive010/expected → test/interactive010/expected.outrenamed

The content is the same.

test/interactive010/input → test/interactive010/input.inrenamed

The content is the same.

test/interactive010/run → test/interactive010/run.shrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input

2+${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input.in

test/interactive011/expected → test/interactive011/expected.outrenamed

The content is the same.

test/interactive011/input → test/interactive011/input.inrenamed

The content is the same.

test/interactive011/run → test/interactive011/run.shrenamed+1−1

@@ -1,6 +1,6 @@

11#!/usr/bin/env bash

33cd src

4−${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input

4+${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input.in

66rm -f *.ibc

test/interactive012/expected → test/interactive012/expected.outrenamed

The content is the same.

test/interactive012/input → test/interactive012/input.inrenamed

The content is the same.

test/interactive012/run → test/interactive012/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input.in

33rm -f *.ibc

test/interactive013/expected → test/interactive013/expected.outrenamed

The content is the same.

test/interactive013/input → test/interactive013/input.inrenamed

The content is the same.

test/interactive013/run → test/interactive013/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input.in

33rm -f *.ibc

test/interactive014/expected → test/interactive014/expected.outrenamed

The content is the same.

test/interactive014/input → test/interactive014/input.inrenamed

The content is the same.

test/interactive014/run → test/interactive014/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input

2+${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input.in

33rm -f *.ibc

test/interactive015/expected → test/interactive015/expected.outrenamed

The content is the same.

test/interactive015/input → test/interactive015/input.inrenamed

The content is the same.

test/interactive015/run → test/interactive015/run.shrenamed+1−1

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

11#!/usr/bin/env bash

33cp src/interactive015.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input.in

66cat interactive015.idr

test/interactive016/expected → test/interactive016/expected.outrenamed

The content is the same.

test/interactive016/input → test/interactive016/input.inrenamed

The content is the same.

test/interactive016/run → test/interactive016/run.shrenamed+1−1

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

11#!/usr/bin/env bash

33cp src/interactive016.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input.in

66cat interactive016.idr

test/interactive017/expected → test/interactive017/expected.outrenamed

The content is the same.

test/interactive017/run → test/interactive017/run.shrenamed

Only the mode changed.

test/interactive018/expected → test/interactive018/expected.outrenamed

The content is the same.

test/interactive018/input → test/interactive018/input.inrenamed

The content is the same.

test/interactive018/rundeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none Top.idr < input

3−rm -f *.ibc

test/interactive018/run.shnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none Top.idr < input.in

3+rm -f *.ibc

test/interfaces001/expected → test/interfaces001/expected.outrenamed

The content is the same.

test/interfaces001/input → test/interfaces001/input.inrenamed

The content is the same.

test/interfaces001/run → test/interfaces001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input.in

33rm -f *.ibc

test/interfaces002/expected → test/interfaces002/expected.outrenamed

The content is the same.

test/interfaces002/run → test/interfaces002/run.shrenamed

Only the mode changed.

test/interfaces003/expected → test/interfaces003/expected.outrenamed

The content is the same.

test/interfaces003/run → test/interfaces003/run.shrenamed

Only the mode changed.

test/interfaces004/expected → test/interfaces004/expected.outrenamed

The content is the same.

test/interfaces004/run → test/interfaces004/run.shrenamed

Only the mode changed.

test/interfaces005/expected → test/interfaces005/expected.outrenamed

The content is the same.

test/interfaces005/run → test/interfaces005/run.shrenamed

Only the mode changed.

test/interfaces006/expected → test/interfaces006/expected.outrenamed

The content is the same.

test/interfaces006/run → test/interfaces006/run.shrenamed

Only the mode changed.

test/interfaces007/expected → test/interfaces007/expected.outrenamed

The content is the same.

test/interfaces007/run → test/interfaces007/run.shrenamed

Only the mode changed.

test/interfaces008/expected → test/interfaces008/expected.outrenamed

The content is the same.

test/interfaces008/run → test/interfaces008/run.shrenamed

Only the mode changed.

test/interfaces009/expected → test/interfaces009/expected.outrenamed

The content is the same.

test/interfaces009/run → test/interfaces009/run.shrenamed

Only the mode changed.

test/interfaces010/expected → test/interfaces010/expected.outrenamed

The content is the same.

test/interfaces010/run → test/interfaces010/run.shrenamed

Only the mode changed.

test/interpret001/expected → test/interpret001/expected.outrenamed

The content is the same.

test/interpret001/input → test/interpret001/input.inrenamed

The content is the same.

test/interpret001/run → test/interpret001/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input.in

33rm -f *.ibc

test/interpret002/expected → test/interpret002/expected.outrenamed

The content is the same.

test/interpret002/input → test/interpret002/input.inrenamed

The content is the same.

test/interpret002/run → test/interpret002/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input.in

33rm -f *.ibc

test/interpret003/expected → test/interpret003/expected.outrenamed

The content is the same.

test/interpret003/input → test/interpret003/input.inrenamed

The content is the same.

test/interpret003/run → test/interpret003/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input.in

33rm -f *.ibc

test/io001/expected → test/io001/expected.outrenamed

The content is the same.

test/io001/run → test/io001/run.shrenamed

Only the mode changed.

test/io002/expected → test/io002/expected.outrenamed

The content is the same.

test/io002/run → test/io002/run.shrenamed

Only the mode changed.

test/io003/expected → test/io003/expected.outrenamed

The content is the same.

test/io003/run → test/io003/run.shrenamed

Only the mode changed.

test/layout001/expected → test/layout001/expected.outrenamed

The content is the same.

test/layout001/run → test/layout001/run.shrenamed

Only the mode changed.

test/literate001/expected → test/literate001/expected.outrenamed

The content is the same.

test/literate001/run → test/literate001/run.shrenamed

Only the mode changed.

test/meta001/expected → test/meta001/expected.outrenamed

The content is the same.

test/meta001/run → test/meta001/run.shrenamed

Only the mode changed.

test/meta002/expected → test/meta002/expected.outrenamed

The content is the same.

test/meta002/run → test/meta002/run.shrenamed

Only the mode changed.

test/meta003/expected → test/meta003/expected.outrenamed

The content is the same.

test/meta003/run → test/meta003/run.shrenamed

Only the mode changed.

test/meta004/expected → test/meta004/expected.outrenamed

The content is the same.

test/meta004/run → test/meta004/run.shrenamed

Only the mode changed.

test/pkg001/expected → test/pkg001/expected.outrenamed

The content is the same.

test/pkg001/run → test/pkg001/run.shrenamed

Only the mode changed.

test/pkg002/expected → test/pkg002/expected.outrenamed

The content is the same.

test/pkg002/run → test/pkg002/run.shrenamed

Only the mode changed.

test/pkg003/expected → test/pkg003/expected.outrenamed

The content is the same.

test/pkg003/run → test/pkg003/run.shrenamed

Only the mode changed.

test/pkg004/expected → test/pkg004/expected.outrenamed

The content is the same.

test/pkg004/run → test/pkg004/run.shrenamed

Only the mode changed.

test/pkg005/expected → test/pkg005/expected.outrenamed

The content is the same.

test/pkg005/run → test/pkg005/run.shrenamed

Only the mode changed.

test/pkg006/expected → test/pkg006/expected.outrenamed

The content is the same.

test/pkg006/run → test/pkg006/run.shrenamed

Only the mode changed.

test/pkg007/expected → test/pkg007/expected.outrenamed

The content is the same.

test/pkg007/input → test/pkg007/input.inrenamed

The content is the same.

test/pkg007/run → test/pkg007/run.shrenamed+1−1

@@ -2,6 +2,6 @@

22cd toy

33${IDRIS:-idris} $@ --build toy.ipkg --ibcsubdir ../ibcout

44cd ../ibcout

5−${IDRIS:-idris} $@ --quiet < ../input

5+${IDRIS:-idris} $@ --quiet < ../input.in

66cd ..

77rm -rf ibcout

test/pkg008/expected → test/pkg008/expected.outrenamed

The content is the same.

test/pkg008/run → test/pkg008/run.shrenamed

Only the mode changed.

test/pkg009/expected → test/pkg009/expected.outrenamed

The content is the same.

test/pkg009/run → test/pkg009/run.shrenamed

Only the mode changed.

test/pkg010/expecteddeleted−31

@@ -1,31 +0,0 @@

1−Uncaught error: user error (wrongopts.ipkg:4:1:

2− |

3−4 | <empty line>

4− | ^

5−Invalid option `-total'

6−

8− [--client ARG] | [--log LEVEL] | [--logging-categories CATS] |

9− [--nobasepkgs] | [--noprelude] | [--nobuiltins] | [--check] |

11− [--partial] | [--warnpartial] | [--warnreach] | [--warnipkg] |

12− [--nocoverage] | [--errorcontext] | [--info] | [--listlogcats] |

14− | [--V1] | [-V|--V0|--verbose] | [--ibcsubdir FILE] |

15− [-i|--idrispath ARG] | [--sourcepath ARG] | [--warn] |

17− [--repl IPKG] | [--clean IPKG] | [--mkdoc IPKG] | [--installdoc IPKG] |

18− [--checkpkg IPKG] | [--testpkg IPKG] | [--indent-with INDENT] |

19− [--indent-clause INDENT] | [--bytecode ARG] | [-S|--codegenonly] |

20− [-c|--compileonly] | [--dumpdefuns ARG] | [--dumpcases ARG] |

21− [--codegen TARGET] | [--portable-codegen TARGET] | [--cg-opt ARG] |

23− [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |

24− [--no-partial-eval] |

25− [--optimise-nat-like-types|--optimize-nat-like-types] |

26− [--no-optimise-nat-like-types|--no-optimize-nat-like-types] |

29− [--no-tactic-deprecation-warnings] |

30− [--allow-capitalized-pattern-variables]) [FILES] [-v|--version]

31−)

test/pkg010/expected.outnew file+29

@@ -0,0 +1,29 @@

1+Uncaught error: user error (wrongopts.ipkg:4:1:

2+ |

3+4 | <empty line>

4+ | ^

5+Invalid option `-total'

8+ --client ARG | --log LEVEL | --logging-categories CATS |

9+ --nobasepkgs | --noprelude | --nobuiltins | --check |

13+ --libdir | --docdir | --include | --V2 | --V1 | (-V|--V0|--verbose) |

16+ --repl IPKG | --clean IPKG | --mkdoc IPKG | --installdoc IPKG |

17+ --checkpkg IPKG | --testpkg IPKG | --indent-with INDENT |

18+ --indent-clause INDENT | --bytecode ARG | (-S|--codegenonly) |

19+ (-c|--compileonly) | --dumpdefuns ARG | --dumpcases ARG |

20+ --codegen TARGET | --portable-codegen TARGET | --cg-opt ARG |

22+ --O3 | --O2 | --O1 | --O0 | --partial-eval | --no-partial-eval |

23+ (--optimise-nat-like-types|--optimize-nat-like-types) |

24+ (--no-optimise-nat-like-types|--no-optimize-nat-like-types) |

26+ (--nocolor|--nocolour) | --consolewidth WIDTH | --highlight |

27+ --no-tactic-deprecation-warnings |

28+ --allow-capitalized-pattern-variables] [FILES] [-v|--version]

29+)

test/pkg010/run → test/pkg010/run.shrenamed

Only the mode changed.

test/prelude001/expected → test/prelude001/expected.outrenamed

The content is the same.

test/prelude001/run → test/prelude001/run.shrenamed

Only the mode changed.

test/primitives001/expected → test/primitives001/expected.outrenamed

The content is the same.

test/primitives001/input → test/primitives001/input.inrenamed

The content is the same.

test/primitives001/run → test/primitives001/run.shrenamed+1−1

@@ -2,5 +2,5 @@

22${IDRIS:-idris} $@ test005.idr -o test005

33./test005

44${IDRIS:-idris} $@ substring.idr -o substring

5−./substring < input

5+./substring < input.in

66rm -f test005 substring *.ibc

test/primitives002/expected → test/primitives002/expected.outrenamed

The content is the same.

test/primitives002/run → test/primitives002/run.shrenamed

Only the mode changed.

test/primitives003/expected → test/primitives003/expected.outrenamed

The content is the same.

test/primitives003/run → test/primitives003/run.shrenamed

Only the mode changed.

test/primitives004-disabled/expected → test/primitives004-disabled/expected.outrenamed

The content is the same.

test/primitives004-disabled/run → test/primitives004-disabled/run.shrenamed

Only the mode changed.

test/primitives005/expected → test/primitives005/expected.outrenamed

The content is the same.

test/primitives005/run → test/primitives005/run.shrenamed

The content is the same.

test/primitives006/expected → test/primitives006/expected.outrenamed

The content is the same.

test/primitives006/run → test/primitives006/run.shrenamed

Only the mode changed.

test/proof001/expected → test/proof001/expected.outrenamed

The content is the same.

test/proof001/run → test/proof001/run.shrenamed

Only the mode changed.

test/proof002/expected → test/proof002/expected.outrenamed

The content is the same.

test/proof002/run → test/proof002/run.shrenamed

Only the mode changed.

test/proof003/expected → test/proof003/expected.outrenamed

The content is the same.

test/proof003/run → test/proof003/run.shrenamed

Only the mode changed.

test/proof004/expected → test/proof004/expected.outrenamed

The content is the same.

test/proof004/run → test/proof004/run.shrenamed

Only the mode changed.

test/proof005/expected → test/proof005/expected.outrenamed

The content is the same.

test/proof005/run → test/proof005/run.shrenamed

Only the mode changed.

test/proof006/expected → test/proof006/expected.outrenamed

The content is the same.

test/proof006/run → test/proof006/run.shrenamed

Only the mode changed.

test/proof007/expected → test/proof007/expected.outrenamed

The content is the same.

test/proof007/run → test/proof007/run.shrenamed

Only the mode changed.

test/proof008/expected → test/proof008/expected.outrenamed

The content is the same.

test/proof008/run → test/proof008/run.shrenamed

Only the mode changed.

test/proof009/expected → test/proof009/expected.outrenamed

The content is the same.

test/proof009/input → test/proof009/input.inrenamed

The content is the same.

test/proof009/run → test/proof009/run.shrenamed+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input

2+${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input.in

33rm -f *.ibc

test/proof010/expected → test/proof010/expected.outrenamed

The content is the same.

test/proof010/run → test/proof010/run.shrenamed

Only the mode changed.

test/proof011/expected → test/proof011/expected.outrenamed

The content is the same.

test/proof011/run → test/proof011/run.shrenamed

Only the mode changed.

test/proofsearch001/expected → test/proofsearch001/expected.outrenamed

The content is the same.

test/proofsearch001/run → test/proofsearch001/run.shrenamed

Only the mode changed.

test/proofsearch002/expected → test/proofsearch002/expected.outrenamed

The content is the same.

test/proofsearch002/run → test/proofsearch002/run.shrenamed

Only the mode changed.

test/proofsearch003/expected → test/proofsearch003/expected.outrenamed

The content is the same.

test/proofsearch003/run → test/proofsearch003/run.shrenamed

Only the mode changed.

test/pruviloj001/expected → test/pruviloj001/expected.outrenamed

The content is the same.

test/pruviloj001/run → test/pruviloj001/run.shrenamed

Only the mode changed.

test/quasiquote001/expected → test/quasiquote001/expected.outrenamed

The content is the same.

test/quasiquote001/run → test/quasiquote001/run.shrenamed

Only the mode changed.

test/quasiquote002/expected → test/quasiquote002/expected.outrenamed

The content is the same.

test/quasiquote002/run → test/quasiquote002/run.shrenamed

Only the mode changed.

test/quasiquote003/expected → test/quasiquote003/expected.outrenamed

The content is the same.

test/quasiquote003/run → test/quasiquote003/run.shrenamed

Only the mode changed.

test/quasiquote004/expected → test/quasiquote004/expected.outrenamed

The content is the same.

test/quasiquote004/run → test/quasiquote004/run.shrenamed

Only the mode changed.

test/quasiquote005/expected → test/quasiquote005/expected.outrenamed

The content is the same.

test/quasiquote005/run → test/quasiquote005/run.shrenamed

Only the mode changed.

test/quasiquote006/expected → test/quasiquote006/expected.outrenamed

The content is the same.

test/quasiquote006/run → test/quasiquote006/run.shrenamed

Only the mode changed.

test/records001/expected → test/records001/expected.outrenamed

The content is the same.

test/records001/run → test/records001/run.shrenamed

Only the mode changed.

test/records002/expected → test/records002/expected.outrenamed

The content is the same.

test/records002/run → test/records002/run.shrenamed

Only the mode changed.

test/records003/expected → test/records003/expected.outrenamed

The content is the same.

test/records003/run → test/records003/run.shrenamed

Only the mode changed.

test/records004/expected → test/records004/expected.outrenamed

The content is the same.

test/records004/run → test/records004/run.shrenamed

Only the mode changed.

test/records005/expected → test/records005/expected.outrenamed

The content is the same.

test/records005/run → test/records005/run.shrenamed

Only the mode changed.

test/reg001/expected → test/reg001/expected.outrenamed

The content is the same.

test/reg001/run → test/reg001/run.shrenamed

Only the mode changed.

test/reg002/expected → test/reg002/expected.outrenamed

The content is the same.

test/reg002/run → test/reg002/run.shrenamed

Only the mode changed.

test/reg004/expected → test/reg004/expected.outrenamed

The content is the same.

test/reg004/run → test/reg004/run.shrenamed

Only the mode changed.

test/reg005/expected → test/reg005/expected.outrenamed

The content is the same.

test/reg005/run → test/reg005/run.shrenamed

Only the mode changed.

test/reg007/expected → test/reg007/expected.outrenamed

The content is the same.

test/reg007/run → test/reg007/run.shrenamed

Only the mode changed.

test/reg013/expected → test/reg013/expected.outrenamed

The content is the same.

test/reg013/run → test/reg013/run.shrenamed

Only the mode changed.

test/reg016/expected → test/reg016/expected.outrenamed

The content is the same.

test/reg016/run → test/reg016/run.shrenamed

Only the mode changed.

test/reg017/expected → test/reg017/expected.outrenamed

The content is the same.

test/reg017/run → test/reg017/run.shrenamed

Only the mode changed.

test/reg020/expected → test/reg020/expected.outrenamed

The content is the same.

test/reg020/run → test/reg020/run.shrenamed

Only the mode changed.

test/reg024/expected → test/reg024/expected.outrenamed

The content is the same.

test/reg024/run → test/reg024/run.shrenamed

Only the mode changed.

test/reg025/expected → test/reg025/expected.outrenamed

The content is the same.

test/reg025/run → test/reg025/run.shrenamed

Only the mode changed.

test/reg027/expected → test/reg027/expected.outrenamed

The content is the same.

test/reg027/run → test/reg027/run.shrenamed

Only the mode changed.

test/reg029/expected → test/reg029/expected.outrenamed

The content is the same.

test/reg029/run → test/reg029/run.shrenamed

Only the mode changed.

test/reg031/expected → test/reg031/expected.outrenamed

The content is the same.

test/reg031/run → test/reg031/run.shrenamed

Only the mode changed.

test/reg032/expected → test/reg032/expected.outrenamed

The content is the same.

test/reg032/run → test/reg032/run.shrenamed

Only the mode changed.

test/reg039/expected → test/reg039/expected.outrenamed

The content is the same.

test/reg039/run → test/reg039/run.shrenamed

Only the mode changed.

test/reg040/expected → test/reg040/expected.outrenamed

The content is the same.

test/reg040/run → test/reg040/run.shrenamed

Only the mode changed.

test/reg041/expected → test/reg041/expected.outrenamed

The content is the same.

test/reg041/run → test/reg041/run.shrenamed

Only the mode changed.

test/reg042/expected → test/reg042/expected.outrenamed

The content is the same.

test/reg042/run → test/reg042/run.shrenamed

Only the mode changed.

test/reg045/expected → test/reg045/expected.outrenamed

The content is the same.

test/reg045/run → test/reg045/run.shrenamed

Only the mode changed.

test/reg048/expected → test/reg048/expected.outrenamed

The content is the same.

test/reg048/run → test/reg048/run.shrenamed

Only the mode changed.

test/reg051-disabled/expected → test/reg051-disabled/expected.outrenamed

The content is the same.

test/reg051-disabled/run → test/reg051-disabled/run.shrenamed

Only the mode changed.

test/reg052/expected → test/reg052/expected.outrenamed

The content is the same.

test/reg052/run → test/reg052/run.shrenamed

Only the mode changed.

test/reg067/expected → test/reg067/expected.outrenamed

The content is the same.

test/reg067/run → test/reg067/run.shrenamed

Only the mode changed.

test/reg075/expected → test/reg075/expected.outrenamed

The content is the same.

test/reg075/input → test/reg075/input.inrenamed

The content is the same.

test/reg075/rundeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none reg075.idr < input

3−rm -f *.ibc

test/reg075/run.shnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none reg075.idr < input.in

3+rm -f *.ibc

test/reg076/expected → test/reg076/expected.outrenamed

The content is the same.

test/reg076/input → test/reg076/input.inrenamed

The content is the same.

test/reg076/run → test/reg076/run.shrenamed

Only the mode changed.

test/reg077/expected → test/reg077/expected.outrenamed

The content is the same.

test/reg077/run → test/reg077/run.shrenamed

Only the mode changed.

test/regression001/expected → test/regression001/expected.outrenamed

The content is the same.

test/regression001/run → test/regression001/run.shrenamed

Only the mode changed.

test/regression002/expected → test/regression002/expected.outrenamed

The content is the same.

test/regression002/run → test/regression002/run.shrenamed

Only the mode changed.

test/regression003/expected → test/regression003/expected.outrenamed

The content is the same.

test/regression003/run → test/regression003/run.shrenamed

Only the mode changed.

test/sourceLocation001/expected → test/sourceLocation001/expected.outrenamed

The content is the same.

test/sourceLocation001/run → test/sourceLocation001/run.shrenamed

Only the mode changed.

test/st001/expected → test/st001/expected.outrenamed

The content is the same.

test/st001/run → test/st001/run.shrenamed

Only the mode changed.

test/st001/test001.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

4040

4141testFile : (ConsoleIO m, File m) => ST m () []

4242testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st001/testFile → test/st001/testFile.inrenamed

The content is the same.

test/st002/expected → test/st002/expected.outrenamed

The content is the same.

test/st002/run → test/st002/run.shrenamed

Only the mode changed.

test/st002/test002.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

4040

4141testFile : (ConsoleIO m, File m) => ST m () []

4242testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st002/testFile → test/st002/testFile.inrenamed

The content is the same.

test/st003/expected → test/st003/expected.outrenamed

The content is the same.

test/st003/run → test/st003/run.shrenamed

Only the mode changed.

test/st003/test003.idr+1−1

@@ -7,7 +7,7 @@ import Control.ST.ImplicitCall

88testFile : (ConsoleIO m, File m) => ST m () []

99testFile = with ST do

10− Right str <- readFile "testFile"

10+ Right str <- readFile "testFile.in"

1111 | Left ferr => do putStrLn (show ferr)

1212 pure ()

1313 putStrLn str

test/st003/testFile → test/st003/testFile.inrenamed

The content is the same.

test/st004/expected → test/st004/expected.outrenamed

The content is the same.

test/st004/run → test/st004/run.shrenamed

Only the mode changed.

test/st005/expected → test/st005/expected.outrenamed

The content is the same.

test/st005/run → test/st005/run.shrenamed

Only the mode changed.

test/st006/expected → test/st006/expected.outrenamed

The content is the same.

test/st006/run → test/st006/run.shrenamed

Only the mode changed.

test/st007/expected → test/st007/expected.outrenamed

The content is the same.

test/st007/run → test/st007/run.shrenamed

Only the mode changed.

test/sugar001/expected → test/sugar001/expected.outrenamed

The content is the same.

test/sugar001/run → test/sugar001/run.shrenamed

Only the mode changed.

test/sugar002/expected → test/sugar002/expected.outrenamed

The content is the same.

test/sugar002/run → test/sugar002/run.shrenamed

Only the mode changed.

test/sugar003/expected → test/sugar003/expected.outrenamed

The content is the same.

test/sugar003/run → test/sugar003/run.shrenamed

Only the mode changed.

test/sugar004/expected → test/sugar004/expected.outrenamed

The content is the same.

test/sugar004/run → test/sugar004/run.shrenamed

Only the mode changed.

test/sugar005/expected → test/sugar005/expected.outrenamed

The content is the same.

test/sugar005/run → test/sugar005/run.shrenamed

Only the mode changed.

test/syntax001/expected → test/syntax001/expected.outrenamed

The content is the same.

test/syntax001/run → test/syntax001/run.shrenamed

Only the mode changed.

test/syntax002/expected → test/syntax002/expected.outrenamed

The content is the same.

test/syntax002/run → test/syntax002/run.shrenamed

Only the mode changed.

test/tactics001/expected → test/tactics001/expected.outrenamed

The content is the same.

test/tactics001/run → test/tactics001/run.shrenamed

Only the mode changed.

test/totality001/expected → test/totality001/expected.outrenamed

The content is the same.

test/totality001/run → test/totality001/run.shrenamed

Only the mode changed.

test/totality002/expected → test/totality002/expected.outrenamed

The content is the same.

test/totality002/run → test/totality002/run.shrenamed

Only the mode changed.

test/totality003/expected → test/totality003/expected.outrenamed

The content is the same.

test/totality003/run → test/totality003/run.shrenamed

Only the mode changed.

test/totality004/expected → test/totality004/expected.outrenamed

The content is the same.

test/totality004/run → test/totality004/run.shrenamed

Only the mode changed.

test/totality005/expected → test/totality005/expected.outrenamed

The content is the same.

test/totality005/run → test/totality005/run.shrenamed

Only the mode changed.

test/totality006/expected → test/totality006/expected.outrenamed

The content is the same.

test/totality006/run → test/totality006/run.shrenamed

Only the mode changed.

test/totality007/expected → test/totality007/expected.outrenamed

The content is the same.

test/totality007/run → test/totality007/run.shrenamed

Only the mode changed.

test/totality008/expected → test/totality008/expected.outrenamed

The content is the same.

test/totality008/run → test/totality008/run.shrenamed

Only the mode changed.

test/totality009/expected → test/totality009/expected.outrenamed

The content is the same.

test/totality009/run → test/totality009/run.shrenamed

Only the mode changed.

test/totality010/expected → test/totality010/expected.outrenamed

The content is the same.

test/totality010/run → test/totality010/run.shrenamed

Only the mode changed.

test/totality011/expected → test/totality011/expected.outrenamed

The content is the same.

test/totality011/run → test/totality011/run.shrenamed

Only the mode changed.

test/totality012/expected → test/totality012/expected.outrenamed

The content is the same.

test/totality012/run → test/totality012/run.shrenamed

Only the mode changed.

test/totality013/expected → test/totality013/expected.outrenamed

The content is the same.

test/totality013/run → test/totality013/run.shrenamed

Only the mode changed.

test/totality014/expected → test/totality014/expected.outrenamed

The content is the same.

test/totality014/run → test/totality014/run.shrenamed

Only the mode changed.

test/totality015/expected → test/totality015/expected.outrenamed

The content is the same.

test/totality015/run → test/totality015/run.shrenamed

Only the mode changed.

test/totality016/expected → test/totality016/expected.outrenamed

The content is the same.

test/totality016/run → test/totality016/run.shrenamed

Only the mode changed.

test/totality017/expected → test/totality017/expected.outrenamed

The content is the same.

test/totality017/run → test/totality017/run.shrenamed

Only the mode changed.

test/totality018/expected → test/totality018/expected.outrenamed

The content is the same.

test/totality018/run → test/totality018/run.shrenamed

Only the mode changed.

test/totality019/expected → test/totality019/expected.outrenamed

The content is the same.

test/totality019/run → test/totality019/run.shrenamed

Only the mode changed.

test/totality020/expected → test/totality020/expected.outrenamed

The content is the same.

test/totality020/run → test/totality020/run.shrenamed

Only the mode changed.

test/totality021/expected → test/totality021/expected.outrenamed

The content is the same.

test/totality021/run → test/totality021/run.shrenamed

Only the mode changed.

test/totality022/expected → test/totality022/expected.outrenamed

The content is the same.

test/totality022/run → test/totality022/run.shrenamed

Only the mode changed.

test/totality023/expected → test/totality023/expected.outrenamed

The content is the same.

test/totality023/run → test/totality023/run.shrenamed

Only the mode changed.

test/totality024/expected → test/totality024/expected.outrenamed

The content is the same.

test/totality024/run → test/totality024/run.shrenamed

Only the mode changed.

test/totality025/expected → test/totality025/expected.outrenamed

The content is the same.

test/totality025/run → test/totality025/run.shrenamed

Only the mode changed.

test/totality026/expected → test/totality026/expected.outrenamed

The content is the same.

test/totality026/run → test/totality026/run.shrenamed

Only the mode changed.

test/tutorial001/expected → test/tutorial001/expected.outrenamed

The content is the same.

test/tutorial001/run → test/tutorial001/run.shrenamed

Only the mode changed.

test/tutorial002/expected → test/tutorial002/expected.outrenamed

The content is the same.

test/tutorial002/run → test/tutorial002/run.shrenamed

Only the mode changed.

test/tutorial003/expected → test/tutorial003/expected.outrenamed

The content is the same.

test/tutorial003/run → test/tutorial003/run.shrenamed

Only the mode changed.

test/tutorial004/expected → test/tutorial004/expected.outrenamed

The content is the same.

test/tutorial004/run → test/tutorial004/run.shrenamed

Only the mode changed.

test/tutorial005/expected → test/tutorial005/expected.outrenamed

The content is the same.

test/tutorial005/run → test/tutorial005/run.shrenamed

Only the mode changed.

test/tutorial006/expected → test/tutorial006/expected.outrenamed

The content is the same.

test/tutorial006/run → test/tutorial006/run.shrenamed

Only the mode changed.

test/tutorial007/expected → test/tutorial007/expected.outrenamed

The content is the same.

test/tutorial007/run → test/tutorial007/run.shrenamed

Only the mode changed.

test/unique001/expected → test/unique001/expected.outrenamed

The content is the same.

test/unique001/run → test/unique001/run.shrenamed

Only the mode changed.

test/unique004/expected → test/unique004/expected.outrenamed

The content is the same.

test/unique004/run → test/unique004/run.shrenamed

Only the mode changed.

test/universes001/expected → test/universes001/expected.outrenamed

The content is the same.

test/universes001/run → test/universes001/run.shrenamed

Only the mode changed.

test/universes002/expected → test/universes002/expected.outrenamed

The content is the same.

test/universes002/run → test/universes002/run.shrenamed

Only the mode changed.

test/views001/expected → test/views001/expected.outrenamed

The content is the same.

test/views001/run → test/views001/run.shrenamed

Only the mode changed.

test/views002/expected → test/views002/expected.outrenamed

The content is the same.

test/views002/run → test/views002/run.shrenamed

Only the mode changed.

test/views003/expected → test/views003/expected.outrenamed

The content is the same.

test/views003/run → test/views003/run.shrenamed

Only the mode changed.