3ce4e48...master · Idris-dev

git.iko.soy/Idris-dev

617 files changed+2250−1018

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+150−80

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

4653

47− myTokenMap : TokenMap Token

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

54+ - .. code-block:: idris

55+

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,12 +64,12 @@ 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

62− Idris> :module Lexer2

63− *Lexer2> is 'a'

72+ *parserEx> is 'a'

6473 Pred (\ARG =>

6574 intToBool (prim__eqChar ARG 'a'))

6675 : Recognise True

@@ -71,44 +80,74 @@ combined, for example,

7180

7281.. list-table::

7382

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

75− 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.

7685

7786 - .. code-block:: idris

7887

79− *Lexer2> is 'a' <+> is 'b'

88+ *parserEx> is 'a' <+> is 'b'

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

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

82− *Lexer2>

8391

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

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

8593 to consumer a character:

8694

8795 - .. code-block:: idris

8896

89− *Lexer2> is 'a' <|> is 'b'

97+ *parserEx> is 'a' <|> is 'b'

9098 Alt (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

91− (Pred (\ARG => intToBool (prim__eqChar ARG 'b'))) : Recognise True

92− *Lexer2>

99+ (Pred (\ARG => intToBool (prim__eqChar ARG 'b')))

100+ : Recognise True

93101

102+This diagram shows the recogniser combinator with some of its constructors:

94103

95104.. image:: ../image/recogniser.png

96105 :width: 487px

97106 :height: 249px

98107 :alt: recogniser data structure

99108

100−There are constructors and combinators to allow the construction of the lexer definition:

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.

101130

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.

102135

103−So far, this is static code, to define the lexical structure. To lex a given text we need to pass this to the runtime code.

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.

104140

105−However this can only cut up the string into a list of substrings, these must be converted into tokens so we need a way to construct tokens. This will also depend on the lexical structure we require.

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

142+:ref:`parserLibraryWhitespace`.

106143

107144Simple Expression Example for Lexer

108145-----------------------------------

109146

110−On this page we will implement a lexer to lex a very simple expression, on the

111−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.

149+

150+First import the lexer and parser code:

112151

113152.. code-block:: idris

114153

@@ -118,54 +157,20 @@ next page we will go on to implement a parser for it.

118157 import public Text.Parser.Core

119158 import public Text.Parser

120159

121−

122−to run:

160+Then decide on the tokens that are needed. For this example the idea is to be

161+able to parse simple arithmetic expressions, like this:

123162

124163.. code-block:: idris

125164

126− cd Idris-dev/libs/contrib

127− idris -p contrib parserEx.idr

128− ____ __ _

129− / _/___/ /____(_)____

130− / // __ / ___/ / ___/ Version 1.3.2

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

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

133−

134− Idris is free software with ABSOLUTELY NO WARRANTY.

135− For details type :warranty.

136− Type checking ./Text/Token.idr

137− Type checking ./Text/Quantity.idr

138− Type checking ./Control/Delayed.idr

139− Type checking ./Data/Bool/Extra.idr

140− Type checking ./Text/Lexer/Core.idr

141− Type checking ./Text/Lexer.idr

142− Type checking ./parserEx.idr

165+ 1+(2*3)

143166

144−.. code-block:: idris

167+so we need:

145168

146− *parserEx> lex expressionTokens "1+2"

147− ([MkToken 0 0 (Number 1),

148− MkToken 0

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

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

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

152− (Operator "+"),

153− MkToken 0

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

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

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

157− (Number 2)],

158− 0,

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

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

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

162− getString (MkStrLen "" 0)) : (List (TokenData ExpressionToken),

163− Int,

164− Int,

165− String)

166− *parserEx>

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

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

171+- Opening and closing Parentheses.

167172

168−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy.

173+We can define these, as tokens, like this:

169174

170175.. code-block:: idris

171176

@@ -178,6 +183,9 @@ The lexer uses potentially infinite data structures. It has recursive arguments

178183 | CParen

179184 | EndInput

180185

186+It may help with debugging and to implement error messages to

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

188+

181189.. code-block:: idris

182190

183191 export

@@ -188,15 +196,15 @@ The lexer uses potentially infinite data structures. It has recursive arguments

188196 show CParen = ")"

189197 show EndInput = "end of input"

190198

191−.. code-block:: idris

192−

193199 export

194200 Show (TokenData ExpressionToken) where

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

196202

203+The following defines the 'TokenMap' for this example:

204+

197205.. code-block:: idris

198206

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

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

200208 export

201209 opChars : String

202210 opChars = "+-*"

@@ -204,15 +212,77 @@ The lexer uses potentially infinite data structures. It has recursive arguments

204212 operator : Lexer

205213 operator = some (oneOf opChars)

206214

207−.. code-block:: idris

208−

209215 toInt' : String -> Integer

210216 toInt' = cast

211217

212218 expressionTokens : TokenMap ExpressionToken

213219 expressionTokens =

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

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

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

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

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

218224

225+This specifies the lexer. It gives, for each token, a function to recognise

226+the token type and a function to construct the token.

227+

228+The library module 'Text.Lexer' contains useful functions to help with this.

229+For example, the digits function used above, which reads one or more

230+numeric characters.

231+

232+We can now run the code with various strings to see what output the lexer

233+produces. This is done by calling the 'lex' function with the TokenMap and

234+input string as parameters:

235+

236+.. code-block:: idris

237+

238+ cd Idris-dev/libs/contrib

239+ idris -p contrib parserEx.idr

240+ ____ __ _

241+ / _/___/ /____(_)____

242+ / // __ / ___/ / ___/ Version 1.3.2

243+ _/ // /_/ / / / (__ ) http://www.idris-lang.org/

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

245+

246+ Idris is free software with ABSOLUTELY NO WARRANTY.

247+ For details type :warranty.

248+ Type checking ./Text/Token.idr

249+ Type checking ./Text/Quantity.idr

250+ Type checking ./Control/Delayed.idr

251+ Type checking ./Data/Bool/Extra.idr

252+ Type checking ./Text/Lexer/Core.idr

253+ Type checking ./Text/Lexer.idr

254+ Type checking ./parserEx.idr

255+

256+ *parserEx> lex expressionTokens "1+2"

257+ ([MkToken 0 0 (Number 1),

258+ MkToken 0

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

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

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

262+ (Operator "+"),

263+ MkToken 0

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

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

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

267+ (Number 2)],

268+ 0,

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

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

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

272+ getString (MkStrLen "" 0)) : (List (TokenData ExpressionToken),

273+ Int,

274+ Int,

275+ String)

276+

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:

280+

281+- (Number 1)

282+- (Operator "+")

283+- (Number 2)

284+

285+So the code is working.

286+

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.