master..3ce4e48 · Idris-dev

git.iko.soy/Idris-dev

617 files changed+1018−2250

unifiedsplit

.travis.yml+35−53

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

1−dist: xenial

1+dist: trusty

2+sudo: false

34language: c

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

910matrix:

1011 include:

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

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

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

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

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"

1422 compiler: ": #GHC 8.2.2"

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"

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"

1725 compiler: ": #GHC 8.2.2"

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"

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"

2028 compiler: ": #GHC 8.2.2"

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]}}

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]}}

4241 fast-finish: true

4342

4443cache:

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

5756 - unset CC

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

5958 then

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

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

6160 export SED=sed;

6261 export ZCAT=zcat;

6362 fi

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

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

7372 fi

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

9074

9175install:

9276 - which cabal

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

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

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

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

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

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

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

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

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

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

117101 echo "cabal build-cache MISS";

118102 rm -rf $HOME/.cabsnap;

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

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

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

121105 fi

122106 # snapshot package-db on cache miss

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

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

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

129113 fi

130114

131−

132115before_script:

133116 - ORIGINAL_DIR=$(pwd)

134− - cabal v1-sdist

117+ - cabal sdist

135118 - cd ..

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

137120 - cd ${PKGNAME}*

138121script:

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

140122###

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

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

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

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

144126###

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

146− - cabal v1-build

128+ - cabal build

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

148130###

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

150− - cabal v1-copy

132+ - cabal copy

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

152134###

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

154− - cabal v1-register

136+ - cabal register

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

156138###

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

CHANGELOG.md−3

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

1−# New since last release

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

3−

41# New in 1.3.2

52+ Documentation added to proof section

INSTALL.md+2−11

@@ -130,8 +130,7 @@ 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 uses the version of libFFI shipped with GHC, instead of the system version.

134−

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

135134See the following GHC issue page for more information:

136135

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

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

142141

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

144143

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.

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.

Makefile+4−4

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

3030 ./stylize.sh

3131

3232test_c:

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

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

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

3535

3636test_js:

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

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

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

3939

4040test_update:

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

41+ $(CABAL) 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) v1-haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"

59+ $(CABAL) 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,6 +44,3 @@ 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,6 +215,36 @@ 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+

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

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

220250rewriteFileEx _ = rewriteFile

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

323353 , postInst = \_ flags pkg local ->

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

325355 NoCopyDest pkg local

356+ , preSDist = idrisPreSDist

357+ , sDistHook = idrisSDist (sDistHook simpleUserHooks)

358+ , postSDist = idrisPostSDist

326359 , testHook = idrisTestHook

327360 }

appveyor.yml+3−3

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

11version: 1.0.{build}

22init:

33- ps: >-

4− choco install cabal --no-progress

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

66 mkdir C:\ghc

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"

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

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

1111

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

1313

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

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

1515

1616 cabal v1-update

1717

docs/conf.py+2−3

@@ -51,7 +51,7 @@ master_doc = 'index'

5151

5252# General information about the project.

5353project = u'Idris'

54−copyright = u'2017-2020, The Idris Community'

54+copyright = u'2017-2019, The Idris Community'

5555author = u'The Idris Community'

5656

5757# The version info for the project you're documenting, acts as replacement for

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

251251# Additional stuff for the LaTeX preamble.

252252'preamble': r'''

253253\usepackage{lmodern}

254−\usepackage{textalpha}

255254\usepackage[T1]{fontenc}

256255\usepackage[utf8x]{inputenc}

257256\usepackage{titlesec}

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

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

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

303302latex_documents = [

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

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

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

306305]

307306

docs/effects/introduction.rst+1−2

@@ -17,8 +17,7 @@ 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. The ``-p effects`` flag

21−is needed when starting Idris.

20+examples directory of the Idris repository.

2221

2322Consider, for example, the following introductory function which

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

docs/image/parserModules.png

Binary file not shown.

docs/image/parserModules.svg+316−413

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

1515 version="1.1"

1616 id="svg8"

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

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

18+ sodipodi:docname="modules.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>

13921 <marker

14022 inkscape:isstock="true"

14123 style="overflow:visible;"

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

318200 inkscape:stockid="Arrow1Mend">

319201 <path

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

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

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

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

323205 id="path1001" />

324206 </marker>

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

334216 <path

335217 id="path995"

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

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

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

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

339221 </marker>

340222 <marker

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

348230 inkscape:collect="always">

349231 <path

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

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

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

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

353235 id="path989" />

354236 </marker>

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

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

397279 id="path3615" />

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

399296 <marker

400297 inkscape:stockid="Arrow1Mend"

401298 orient="auto"

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

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

427324 id="path1537" />

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

429341 </defs>

430342 <sodipodi:namedview

431343 id="base"

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

436348 inkscape:pageshadow="2"

437349 inkscape:zoom="1"

438350 inkscape:cx="368.33949"

439− inkscape:cy="547.05121"

351+ inkscape:cy="554.8721"

440352 inkscape:document-units="mm"

441353 inkscape:current-layer="layer1"

442354 showgrid="false"

443− inkscape:window-width="1800"

355+ inkscape:window-width="1359"

444356 inkscape:window-height="1011"

445− inkscape:window-x="86"

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

446358 inkscape:window-y="0"

447− inkscape:window-maximized="0"

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

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

449360 <metadata

450361 id="metadata5">

451362 <rdf:RDF>

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

462373 inkscape:label="Layer 1"

463374 inkscape:groupmode="layer"

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

465527 <text

466528 inkscape:export-ydpi="61.120499"

467529 inkscape:export-xdpi="61.120499"

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

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

584646 <text

585647 id="text931"

586− y="218.41846"

587− x="36.512497"

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

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"

589651 xml:space="preserve"

590652 inkscape:export-xdpi="61.120499"

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

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

593− y="218.41846"

594− x="36.512497"

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"

595657 id="tspan929"

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

597659 <text

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

610672 <rect

611673 inkscape:export-ydpi="61.120499"

612674 inkscape:export-xdpi="61.120499"

613− y="214.18488"

614− x="32.01458"

675+ y="180.05362"

676+ x="32.543747"

615677 height="6.3500061"

616678 width="43.656254"

617679 id="rect937"

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

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

619681 <rect

620682 inkscape:export-ydpi="61.120499"

621683 inkscape:export-xdpi="61.120499"

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

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"

623685 id="rect939"

624686 width="42.862495"

625687 height="6.8791728"

626− x="94.985413"

627− y="214.18488" />

688+ x="95.51458"

689+ y="180.05362" />

628690 <text

629691 inkscape:export-ydpi="61.120499"

630692 inkscape:export-xdpi="61.120499"

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

644706 inkscape:export-xdpi="61.120499"

645707 inkscape:connector-curvature="0"

646708 id="path963"

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

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

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

649711 <text

650712 inkscape:export-ydpi="61.120499"

651713 inkscape:export-xdpi="61.120499"

652714 xml:space="preserve"

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

654− x="23.220526"

655− y="251.01649"

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"

656718 id="text971"><tspan

657719 sodipodi:role="line"

658720 id="tspan969"

659− x="23.220526"

660− y="251.01649"

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

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>

662724 <rect

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

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"

664726 id="rect973"

665727 width="47.889587"

666728 height="6.3500061"

667− x="21.633026"

668− y="246.51833"

729+ x="22.162193"

730+ y="212.38707"

669731 inkscape:export-xdpi="61.120499"

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

671733 <path

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

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

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"

674736 id="path975"

675737 inkscape:connector-curvature="0"

676738 inkscape:export-xdpi="61.120499"

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

678740 sodipodi:nodetypes="cc" />

679741 <text

680742 id="text979"

681− y="241.96643"

682− x="23.283329"

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

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"

684746 xml:space="preserve"

685747 inkscape:export-xdpi="61.120499"

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

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

688− y="241.96643"

689− x="23.283329"

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"

690752 id="tspan977"

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

692754 <rect

693755 inkscape:export-ydpi="61.120499"

694756 inkscape:export-xdpi="61.120499"

695− y="237.46826"

696− x="21.695829"

757+ y="203.33701"

758+ x="22.224997"

697759 height="6.2469702"

698760 width="43.853985"

699761 id="rect981"

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

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

701763 <text

702764 inkscape:export-ydpi="61.120499"

703765 inkscape:export-xdpi="61.120499"

704766 xml:space="preserve"

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

706− x="23.18244"

707− y="233.68523"

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"

708770 id="text985"><tspan

709771 sodipodi:role="line"

710772 id="tspan983"

711− x="23.18244"

712− y="233.68523"

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

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>

714776 <rect

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

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"

716778 id="rect987"

717779 width="39.011257"

718780 height="5.9464455"

719− x="21.59494"

720− y="229.18706"

781+ x="22.124107"

782+ y="195.0558"

721783 inkscape:export-xdpi="61.120499"

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

723785 <path

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

726788 inkscape:export-xdpi="61.120499"

727789 inkscape:connector-curvature="0"

728790 id="path993"

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

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

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

731793 <path

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

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

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"

734796 id="path999"

735797 inkscape:connector-curvature="0"

736798 inkscape:export-xdpi="61.120499"

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

738800 sodipodi:nodetypes="cc" />

739801 <path

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

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

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

742804 id="path1005"

743805 inkscape:connector-curvature="0"

744806 inkscape:export-xdpi="61.120499"

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

746808 sodipodi:nodetypes="cc" />

747809 <path

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

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

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

750812 id="path1011"

751813 inkscape:connector-curvature="0"

752814 inkscape:export-xdpi="61.120499"

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

756818 inkscape:export-ydpi="61.120499"

757819 inkscape:export-xdpi="61.120499"

758820 id="text1019"

759− y="218.94762"

760− x="96.837494"

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

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"

762824 xml:space="preserve"><tspan

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

764− y="218.94762"

765− x="96.837494"

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"

766828 id="tspan1017"

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

768830 <path

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

848910 id="rect1061"

849911 width="59.266659"

850912 height="16.13958"

851− x="97.102074"

852− y="186.93335" />

913+ x="92.339577"

914+ y="230.5896" />

853915 <path

854916 inkscape:export-ydpi="61.120499"

855917 inkscape:export-xdpi="61.120499"

856918 inkscape:connector-curvature="0"

857919 id="path1063"

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

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

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

860922 sodipodi:nodetypes="cc" />

861923 <text

862924 inkscape:export-ydpi="61.120499"

863925 inkscape:export-xdpi="61.120499"

864926 id="text1081"

865− y="192.48962"

866− x="157.95586"

927+ y="236.14587"

928+ x="153.19336"

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

868930 xml:space="preserve"><tspan

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

870− y="192.48962"

871− x="157.95586"

932+ y="236.14587"

933+ x="153.19336"

872934 id="tspan1079"

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

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

874936 <text

875937 inkscape:export-ydpi="61.120499"

876938 inkscape:export-xdpi="61.120499"

877939 id="text1089"

878− y="192.75421"

879− x="98.954155"

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

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

881943 xml:space="preserve"><tspan

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

883− y="192.75421"

884− x="98.954155"

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"

885947 id="tspan1087"

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

887949 <rect

888950 inkscape:export-ydpi="61.120499"

889951 inkscape:export-xdpi="61.120499"

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

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"

891953 id="rect1097"

892− width="55.033333"

893− height="14.287498"

894− x="20.637447"

895− y="52.524986" />

954+ width="35.983334"

955+ height="18.25625"

956+ x="124.08953"

957+ y="18.393738" />

896958 <text

897959 inkscape:export-ydpi="61.120499"

898960 inkscape:export-xdpi="61.120499"

899961 id="text1101"

900− y="58.610428"

901− x="23.54781"

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

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"

903965 xml:space="preserve"><tspan

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

905− y="58.610428"

906− x="23.54781"

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"

907969 id="tspan1099"

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

909971 <path

910972 sodipodi:nodetypes="cc"

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

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

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

913975 id="path1107"

914976 inkscape:connector-curvature="0"

915977 inkscape:export-xdpi="61.120499"

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

919981 inkscape:export-xdpi="61.120499"

920982 inkscape:connector-curvature="0"

921983 id="path1113"

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

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

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

924986 sodipodi:nodetypes="cc" />

925987 <path

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

927989 inkscape:export-xdpi="61.120499"

928990 inkscape:connector-curvature="0"

929991 id="path1119"

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

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

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

932994 sodipodi:nodetypes="cc" />

933995 <text

934996 id="text950"

935− y="104.70191"

936− x="22.426785"

997+ y="236.19983"

998+ x="22.69136"

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

9381000 xml:space="preserve"

9391001 inkscape:export-xdpi="61.120499"

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

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

942− y="104.70191"

943− x="22.426785"

1004+ y="236.19983"

1005+ x="22.69136"

9441006 id="tspan948"

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

9461008 <rect

9471009 inkscape:export-ydpi="61.120499"

9481010 inkscape:export-xdpi="61.120499"

949− y="100.20374"

950− x="20.839275"

1011+ y="231.70166"

1012+ x="21.103861"

9511013 height="9.7895899"

9521014 width="47.889587"

9531015 id="rect952"

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

9571019 inkscape:export-xdpi="61.120499"

9581020 xml:space="preserve"

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

960− x="22.955944"

961− y="108.40608"

1022+ x="23.220528"

1023+ y="239.90399"

9621024 id="text956"><tspan

9631025 sodipodi:role="line"

9641026 id="tspan954"

965− x="22.955944"

966− y="108.40608"

1027+ x="23.220528"

1028+ y="239.90399"

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

9681030 <text

9691031 inkscape:export-ydpi="61.120499"

9701032 inkscape:export-xdpi="61.120499"

9711033 xml:space="preserve"

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

973− x="79.312202"

974− y="92.266502"

1035+ x="22.69136"

1036+ y="252.33942"

9751037 id="text960"><tspan

9761038 sodipodi:role="line"

9771039 id="tspan958"

978− x="79.312202"

979− y="92.266502"

1040+ x="22.69136"

1041+ y="252.33942"

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

9811043 <rect

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

9831045 id="rect962"

9841046 width="61.912495"

9851047 height="18.785419"

986− x="77.724693"

987− y="87.768333"

1048+ x="21.103861"

1049+ y="247.84125"

9881050 inkscape:export-xdpi="61.120499"

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

9901052 <text

9911053 id="text966"

992− y="95.970665"

993− x="79.841362"

1054+ y="256.04358"

1055+ x="23.220528"

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

9951057 xml:space="preserve"

9961058 inkscape:export-xdpi="61.120499"

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

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

999− y="95.970665"

1000− x="79.841362"

1061+ y="256.04358"

1062+ x="23.220528"

10011063 sodipodi:role="line"

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

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

1004− y="100.38039"

1005− x="79.841362"

1066+ y="260.45331"

1067+ x="23.220528"

10061068 sodipodi:role="line"

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

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

1009− y="104.79011"

1010− x="79.841362"

1071+ y="264.86304"

1072+ x="23.220528"

10111073 sodipodi:role="line"

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

10131075 <text

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

10151077 inkscape:export-xdpi="61.120499"

10161078 xml:space="preserve"

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

1018− x="22.162193"

1019− y="73.217979"

1080+ x="22.69136"

1081+ y="90.151314"

10201082 id="text978"><tspan

10211083 sodipodi:role="line"

10221084 id="tspan976"

1023− x="22.162193"

1024− y="73.217979"

1085+ x="22.69136"

1086+ y="90.151314"

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

10261088 <rect

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

10281090 id="rect980"

10291091 width="55.827087"

10301092 height="10.054173"

1031− x="20.574694"

1032− y="68.719742"

1093+ x="21.103861"

1094+ y="85.653076"

10331095 inkscape:export-xdpi="61.120499"

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

10351097 <text

10361098 id="text984"

1037− y="76.92215"

1038− x="22.69136"

1099+ y="93.855484"

1100+ x="23.220528"

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

10401102 xml:space="preserve"

10411103 inkscape:export-xdpi="61.120499"

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

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

1044− y="76.92215"

1045− x="22.69136"

1106+ y="93.855484"

1107+ x="23.220528"

10461108 id="tspan982"

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

10481110 <text

10491111 id="text988"

1050− y="89.886726"

1051− x="22.162193"

1112+ y="106.82006"

1113+ x="22.69136"

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

10531115 xml:space="preserve"

10541116 inkscape:export-xdpi="61.120499"

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

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

1057− y="89.886726"

1058− x="22.162193"

1119+ y="106.82006"

1120+ x="22.69136"

10591121 id="tspan986"

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

10611123 <rect

10621124 inkscape:export-ydpi="61.120499"

10631125 inkscape:export-xdpi="61.120499"

1064− y="85.388489"

1065− x="20.574694"

1126+ y="102.32182"

1127+ x="21.103861"

10661128 height="9.5250101"

10671129 width="37.835419"

10681130 id="rect990"

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

10721134 inkscape:export-xdpi="61.120499"

10731135 xml:space="preserve"

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

1075− x="22.69136"

1076− y="93.590897"

1137+ x="23.220528"

1138+ y="110.52423"

10771139 id="text994"><tspan

10781140 sodipodi:role="line"

10791141 id="tspan992"

1080− x="22.69136"

1081− y="93.590897"

1142+ x="23.220528"

1143+ y="110.52423"

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

10831145 <path

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

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

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

10861148 id="path996"

10871149 inkscape:connector-curvature="0"

10881150 inkscape:export-xdpi="61.120499"

10891151 inkscape:export-ydpi="61.120499"

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

12501153 </g>

12511154</svg>

docs/parserLibrary/index.rst−1

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

2121 introduction

2222 lexer

2323 parser

24− whitespace

docs/parserLibrary/introduction.rst+12−52

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

44Parser Library Introduction

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

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.

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.

218

229.. list-table::

2310

@@ -25,52 +12,25 @@ complicated parser can be made out of many smaller ones.

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

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

2714

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

29− :width: 307px

30− :height: 76px

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

15+.. image:: ../image/parserTopLevel.png

16+ :width: 484px

17+ :height: 147px

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

3219

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.

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.

3521

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.

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.

4023

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.

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.

4425

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.

5026

51−Parser Library and Idris 2

52−--------------------------

5327

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.

5828

59−Idris 2 has at least 3 compilers:

29+.. image:: ../image/parserModules.png

30+ :width: 484px

31+ :height: 147px

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

6033

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.

6634

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

7135

72−.. image:: ../image/parserModules.png

73− :width: 460px

74− :height: 496px

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

7636

docs/parserLibrary/lexer.rst+80−150

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

1−.. _parserLibraryLexer:

2−

31Lexer

42=====

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

108

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

1210

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:

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:

1813

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

20− :width: 330px

21− :height: 73px

22− :alt: diagram illustrating these stages of lexer

14+.. image:: ../image/tokenise.png

15+ :width: 330px

16+ :height: 73px

17+ :alt: diagram illustrating these stages of lexer

2318

2419TokenMap

2520--------

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

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

3025- A way to construct these individual tokens.

3126

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

33−this information:

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

3428

3529.. code-block:: idris

3630

3731 (Lexer, String -> tokenType)

3832

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

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

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

4135

42−.. list-table::

36+from Text.Lexer.Core:

4337

44− * - from Text.Lexer.Core

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

46−

47− - .. code-block:: idris

38+.. code-block:: idris

4839

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

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

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

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

5142

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

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

5344

54− - .. code-block:: idris

45+.. code-block:: idris

5546

56− myTokenMap : TokenMap Token

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

47+ myTokenMap : TokenMap Token

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

5849

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

6051

@@ -64,12 +55,12 @@ Recognisers

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

6556

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

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

68−'is' function:

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

6959

7060.. code-block:: idris

7161

72− *parserEx> is 'a'

62+ Idris> :module Lexer2

63+ *Lexer2> is 'a'

7364 Pred (\ARG =>

7465 intToBool (prim__eqChar ARG 'a'))

7566 : Recognise True

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

8071

8172.. list-table::

8273

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

84− the sequence is guaranteed to consume a character.

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

75+ is guaranteed to consume a character.

8576

8677 - .. code-block:: idris

8778

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

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

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

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

82+ *Lexer2>

9183

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

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

9385 to consumer a character:

9486

9587 - .. code-block:: idris

9688

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

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

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

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

100− : Recognise True

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

92+ *Lexer2>

10193

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

10394

10495.. image:: ../image/recogniser.png

10596 :width: 487px

10697 :height: 249px

10798 :alt: recogniser data structure

10899

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.

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

130101

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.

135102

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.

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.

140104

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

142−:ref:`parserLibraryWhitespace`.

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.

143106

144107Simple Expression Example for Lexer

145108-----------------------------------

146109

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:

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.

151112

152113.. code-block:: idris

153114

@@ -157,20 +118,54 @@ First import the lexer and parser code:

157118 import public Text.Parser.Core

158119 import public Text.Parser

159120

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:

121+

122+to run:

162123

163124.. code-block:: idris

164125

165− 1+(2*3)

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

166143

167−so we need:

144+.. code-block:: idris

168145

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

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

171−- Opening and closing Parentheses.

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>

172167

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

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

174169

175170.. code-block:: idris

176171

@@ -183,9 +178,6 @@ We can define these, as tokens, like this:

183178 | CParen

184179 | EndInput

185180

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

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

188−

189181.. code-block:: idris

190182

191183 export

@@ -196,15 +188,15 @@ implement ``show`` for these tokens:

196188 show CParen = ")"

197189 show EndInput = "end of input"

198190

191+.. code-block:: idris

192+

199193 export

200194 Show (TokenData ExpressionToken) where

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

202196

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

204−

205197.. code-block:: idris

206198

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

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

208200 export

209201 opChars : String

210202 opChars = "+-*"

@@ -212,77 +204,15 @@ The following defines the 'TokenMap' for this example:

212204 operator : Lexer

213205 operator = some (oneOf opChars)

214206

207+.. code-block:: idris

208+

215209 toInt' : String -> Integer

216210 toInt' = cast

217211

218212 expressionTokens : TokenMap ExpressionToken

219213 expressionTokens =

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

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

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

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

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

224218

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+68−492

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

1−.. _parserLibraryParser:

2−

31Parser

42======

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

8−

9−.. code-block:: idris

10−

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

12− Either (ParseError tok) (ty, List tok)

13−

14−If successful this returns 'Right' with a pair of

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.

156

16−- the parse result.

17−- the unparsed tokens (the remaining input).

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

188

19−otherwise it returns 'Left' with the error message.

9+.. code-block:: idris

2010

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.

11+ doParse : {c : Bool} ->

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

13+ ParseResult xs c ty

2514

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.

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

2916

3017.. code-block:: idris

3118

@@ -53,59 +40,27 @@ consume input.

5340 Grammar tok c1 ty -> Grammar tok c2 ty ->

5441 Grammar tok (c1 && c2) ty

5542

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−

6443.. code-block:: idris

6544

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

6646 public export

6747 Rule : Type -> Type

6848 Rule ty = Grammar (TokenData ExpressionToken) True ty

6949

70−Parser Example

71−--------------

72−

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

74−this page we will go on to 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

50+.. code-block:: idris

9651

97− export

98− intLiteral : Rule Integer

99− intLiteral

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

52+ export

53+ intLiteral : Rule Integer

54+ intLiteral

55+ = terminal --"Expected integer literal"

56+ (\x => case tok x of

10157 Number i => Just i

10258 _ => Nothing)

10359

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

10561parse which takes two parameters:

106−

107−- The grammar (in this case intLiteral)

108−- The token list from the lexer.

62+* The grammar (in this case intLiteral)

63+* The token list from the lexer.

10964

11065.. code-block:: idris

11166

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

11368 (Integer, List (TokenData ExpressionToken))

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

11570

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.

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.

11873

11974.. code-block:: idris

12075

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

14297 (Integer, List (TokenData ExpressionToken))

14398 *parserEx>

14499

145−.. list-table::

146−

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

148− construct the grammar

149− - .. code-block:: idris

150−

151− ||| Succeeds if running the predicate on the

152− ||| next token returns Just x, returning x.

153− ||| Otherwise fails.

154− export

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

156− terminal = Terminal

157−

158−This is defined here

159−: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Parser/Core.idr

160−Idris 2 uses a slightly different version which stores an error message like

161−"Expected integer literal" which can be output if the rule fails

162−: https://github.com/edwinb/Idris2/blob/master/src/Text/Parser/Core.idr

163−

164−.. list-table::

100+.. code-block:: idris

165101

166− * - The 'terminal' function is also used to construct the other

167− elements of the grammar that we require, for instance,

168− opening parenthesis:

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

169107

170− - .. code-block:: idris

108+.. code-block:: idris

171109

172− openParen : Rule Integer

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

110+ openParen : Rule Integer

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

174112 OParen => Just 0

175113 _ => Nothing)

176114

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−

182115.. code-block:: idris

183116

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

185118 (Integer, List (TokenData ExpressionToken))

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

187120

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

189−error for anything else:

190−

191121.. code-block:: idris

192122

193123 *parserEx> test2 "("

@@ -200,12 +130,7 @@ error for anything else:

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

201131 (Integer,

202132 List (TokenData ExpressionToken))

203−

204−Now we have two Grammars we can try combining them. The following test looks

205−for ``openParen`` followed by ``intLiteral``, the two Grammars are combined using

206−``<*>``. The ``map const`` part uses the integer value from the first.

207−

208−The following test is looking for ``(`` followed by a number:

133+ *parserEx>

209134

210135.. code-block:: idris

211136

@@ -213,9 +138,6 @@ The following test is looking for ``(`` followed by a number:

213138 (Integer, List (TokenData ExpressionToken))

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

215140

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

217−required, other token lists are not:

218−

219141.. code-block:: idris

220142

221143 *parserEx> test3 "(123"

@@ -248,121 +170,15 @@ required, other token lists are not:

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

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

250172 (Integer, List (TokenData ExpressionToken))

173+ *parserEx>

251174

252−.. list-table::

253−

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

255−

256− - .. code-block:: idris

175+.. code-block:: idris

257176

258− closeParen : Rule Integer

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

177+ closeParen : Rule Integer

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

260179 CParen => Just 0

261180 _ => Nothing)

262181

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−

366182.. code-block:: idris

367183

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

@@ -372,143 +188,10 @@ where ``op`` is defined like this:

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

373189 _ => Nothing)

374190

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−

430191.. code-block:: idris

431192

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:

193+ paren : Rule Integer -> Rule Integer

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

512195

513196.. code-block:: idris

514197

@@ -520,7 +203,9 @@ First alter the grammar to have infix operations:

520203 Grammar tok c2 Integer ->

521204 Grammar tok c3 Integer ->

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

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

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

207+

208+.. code-block:: idris

524209

525210 subInt : Integer -> Integer -> Integer

526211 subInt a b = a-b

@@ -530,7 +215,7 @@ First alter the grammar to have infix operations:

530215 Grammar tok c2 Integer ->

531216 Grammar tok c3 Integer ->

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

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

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

534219

535220

536221 multInt : Integer -> Integer -> Integer

@@ -541,160 +226,51 @@ First alter the grammar to have infix operations:

541226 Grammar tok c2 Integer ->

542227 Grammar tok c3 Integer ->

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

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

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

230+

231+.. code-block:: idris

545232

546233 partial

547234 expr : Rule Integer

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

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

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

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

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

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

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

552239

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−

562240.. code-block:: idris

563241

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:

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

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

244+ (Integer, List (TokenData ExpressionToken))

245+ *parserEx>

580246

581247.. code-block:: idris

582248

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

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

584250

585−we add an extra rule to give:

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

586252

587253.. code-block:: idris

588254

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−

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>

613269

614270.. code-block:: idris

615271

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

272+ partial

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

640274 (Integer, List (TokenData ExpressionToken))

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, [])

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

698276

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.rstdeleted−250

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

1−.. _parserLibraryWhitespace:

2−

3−Whitespace and Comments

4−=======================

5−

6−The previous two pages introduced the lexer and parser but have not yet

7−discussed how to handle whitespace and comments.

8−

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

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.

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+47−101

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

1−Cabal-Version: 2.4

21Name: idris

32Version: 1.3.2

4−License: BSD-3-Clause

3+License: BSD3

54License-file: LICENSE

65Author: Edwin Brady

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

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

4241 .

4342 * Hugs style interactive environment

4443

44+Cabal-Version: >= 1.22

45+

4546Build-type: Custom

4647

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

4849

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

50−-- heavily discouraged.

5150Data-files: idrisdoc/styles.css

52− jsrts/jsbn/*.js

53− jsrts/*.js

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

5456 jsrts/jsbn/LICENSE

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

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

6480

6581Extra-doc-files:

6682 CHANGELOG.md

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

7086 README.md

7187 RELEASE-CHECKS.md

7288 idris-tutorial.pdf

73− man/idris.1

7489 samples/effects/*.idr

7590 samples/misc/*.idr

76− samples/tutorial/*.idr

77− samples/ST/*.idr

78− samples/ST/Graphics/*.idr

79− samples/ST/Net/*.idr

8091 samples/misc/*.lidr

92+ samples/tutorial/*.idr

8193

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

8395Extra-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

14296

14397source-repository head

14498 type: git

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

146100

147101custom-setup

148102 setup-depends:

149− Cabal >= 2.4 && < 3.1,

103+ Cabal >= 1.10 && <2.5,

150104 base >= 4 && <5,

151105 directory,

152106 filepath,

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

307261 Util.Pretty

308262 , Util.Net

309263

264+

265+

266+ -- Auto Generated

310267 , Paths_idris

311268 , Version_idris

312269 , Tools_idris

313270 , BuildFlags_idris

314271

315− -- Auto Generated

316− Autogen-modules: Paths_idris

317− , Version_idris

318− , Tools_idris

319− , BuildFlags_idris

320−

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

322273 , aeson >= 0.6 && < 1.5

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

324− , ansi-terminal < 0.11

275+ , ansi-terminal < 0.10

325276 , ansi-wl-pprint < 0.7

326277 , array >= 0.4.0.1 && < 0.6

327278 , base64-bytestring < 1.1

328279 , binary >= 0.8.4.1 && < 0.9

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

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

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

331282 , bytestring < 0.11

332− , cheapskate >= 0.1.1.2 && < 0.2

283+ , cheapskate >= 0.1.1 && < 0.2

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

334285 , containers >= 0.5 && < 0.7

335286 , deepseq < 1.5

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

338289 , fingertree >= 0.1.4.1 && < 0.2

339290 , haskeline >= 0.7 && < 0.8

340291 , ieee754 >= 0.7 && < 0.9

341− , megaparsec >= 7.0.4 && < 9

292+ , megaparsec >= 7.0.4 && < 8

342293 , mtl >= 2.1 && < 2.3

343− , network >= 2.7 && < 3.1.2

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

294+ , network >= 2.7 && < 2.9

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

345296 , parser-combinators >= 1.0.0

346297 , pretty < 1.2

347298 , process < 1.7

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

349300 , safe >= 0.3.9

350301 , split < 0.3

351302 , terminal-size < 0.4

352− , text >=1.2.1.0 && < 1.4

353− , time >= 1.4 && < 2.0

303+ , text >=1.2.1.0 && < 1.3

304+ , time >= 1.4 && < 1.9

354305 , transformers >= 0.5 && < 0.6

355306 , uniplate >=1.6 && < 1.7

356307 , unordered-containers < 0.3

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

358309 , vector < 0.13

359310 , vector-binary-instances < 0.3

360311 , zip-archive > 0.2.3.5 && < 0.5

361− , fsnotify >= 0.2 && < 0.4

312+ , fsnotify >= 0.2 && < 2.2

362313 , async < 2.3

363314

364315 if !impl(ghc >= 8.0)

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

366− , fail == 4.9.0.*

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

367317

368318 Default-Language: Haskell2010

369319 ghc-prof-options: -auto-all -caf-all

@@ -382,7 +332,6 @@ Library

382332 cpp-options: -DIDRIS_GMP

383333 if flag(freestanding)

384334 other-modules: Target_idris

385− autogen-modules: Target_idris

386335 cpp-options: -DFREESTANDING

387336 if flag(CI)

388337 ghc-options: -Werror

@@ -416,7 +365,7 @@ Test-suite regression-and-feature-tests

416365 , filepath

417366 , directory

418367 , haskeline >= 0.7

419− , optparse-applicative >= 0.13 && < 0.16

368+ , optparse-applicative >= 0.13 && < 0.15

420369 , tagged

421370 , tasty >= 0.8

422371 , tasty-golden >= 2.0

@@ -431,7 +380,6 @@ Test-suite regression-and-feature-tests

431380

432381Executable idris-codegen-c

433382 Main-is: Main.hs

434− autogen-modules: Paths_idris

435383 other-modules: Paths_idris

436384 hs-source-dirs: codegen/idris-codegen-c

437385

@@ -447,7 +395,6 @@ Executable idris-codegen-c

447395

448396Executable idris-codegen-javascript

449397 Main-is: Main.hs

450− autogen-modules: Paths_idris

451398 other-modules: Paths_idris

452399 hs-source-dirs: codegen/idris-codegen-javascript

453400

@@ -463,7 +410,6 @@ Executable idris-codegen-javascript

463410

464411Executable idris-codegen-node

465412 Main-is: Main.hs

466− autogen-modules: Paths_idris

467413 other-modules: Paths_idris

468414 hs-source-dirs: codegen/idris-codegen-node

469415

libs/base/Control/Isomorphism.idr+23−20

@@ -17,22 +17,21 @@ 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 (\_ => Refl) (\_ => Refl)

22+isoRefl = MkIso id id (\x => Refl) (\x => 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 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

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)

3635

3736Category Iso where

3837 id = isoRefl

@@ -100,7 +99,8 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft

10099

101100||| Isomorphism is a congruence with regards to disjunction

102101eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')

103−eitherCong (MkIso to from toFrom fromTo)

102+eitherCong {a = a} {a' = a'} {b = b} {b' = b'}

103+ (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,7 +143,9 @@ 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, ())) (\_ => Refl) (\(_, ()) => Refl)

146+pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok

147+ where ok : (x : (a, ())) -> (fst x, ()) = x

148+ ok (x, ()) = Refl

147149

148150||| Conjunction with truth is a no-op

149151pairUnitLeft : Iso ((), a) a

@@ -159,7 +161,8 @@ pairBotRight = isoTrans pairComm pairBotLeft

159161

160162||| Isomorphism is a congruence with regards to conjunction

161163pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')

162−pairCong (MkIso to from toFrom fromTo)

164+pairCong {a = a} {a' = a'} {b = b} {b' = b'}

165+ (MkIso to from toFrom fromTo)

163166 (MkIso to' from' toFrom' fromTo') =

164167 MkIso to'' from'' iso1 iso2

165168 where to'' : (a, b) -> (a', b')

@@ -202,7 +205,7 @@ distribLeft = MkIso to from toFrom fromTo

202205

203206||| Products distribute over sums

204207distribRight : Iso (a, Either b c) (Either (a, b) (a, c))

205−distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

208+distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm

206209

207210

208211-- Enable preorder reasoning syntax over isomorphisms

@@ -219,7 +222,7 @@ step a iso1 iso2 = isoTrans iso1 iso2

219222-- Isomorphisms over Maybe

220223||| Isomorphism is a congruence with respect to Maybe

221224maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)

222−maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

225+maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2

223226 where ok1 : (y : Maybe b) -> map to (map from y) = y

224227 ok1 Nothing = Refl

225228 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED

@@ -250,7 +253,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=

250253 () QED

251254

252255eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))

253−eitherMaybeLeftMaybe =

256+eitherMaybeLeftMaybe {a} {b} =

254257 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=

255258 (Either (Either a ()) b) ={ eitherAssoc }=

256259 (Either a (Either () b)) ={ eitherCongRight eitherComm }=

@@ -260,7 +263,7 @@ eitherMaybeLeftMaybe =

260263

261264

262265eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))

263−eitherMaybeRightMaybe =

266+eitherMaybeRightMaybe {a} {b} =

264267 (Either a (Maybe b)) ={ eitherComm }=

265268 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=

266269 (Maybe (Either b a)) ={ maybeCong eitherComm }=

@@ -285,8 +288,8 @@ maybeIsoS = MkIso forth back fb bf

285288 fb (FS x) = Refl

286289

287290finZeroBot : Iso (Fin 0) Void

288−finZeroBot = MkIso (void . uninhabited)

289− void

291+finZeroBot = MkIso (\x => void (uninhabited x))

292+ (\x => void x)

290293 (\x => void x)

291294 (\x => void (uninhabited x))

292295

libs/contrib/Control/Algebra/Laws.idr+80−128

@@ -6,146 +6,98 @@ import Interfaces.Verified

77%access export

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

9+||| A prof that -0 = 0 in any verified group.

10+inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral

2611inverseNeutralIsNeutral {t} =

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

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

3117

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

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

6228

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

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

6945

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

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

8758

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

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

10571

106−||| Inverse operator can be extracted before multiplication.

72+||| A proof that inverse operator can be extracted before multiplication

10773||| (-x)y = -(xy)

108−multInverseInversesL : VerifiedRing t => (l, r : t) ->

109− inverse l <.> r = inverse (l <.> r)

74+multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)

11075multInverseInversesL l r =

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

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

12484

125−||| Inverse operator can be extracted before multiplication.

85+||| A proof that inverse operator can be extracted before multiplication

12686||| x(-y) = -(xy)

127−multInverseInversesR : VerifiedRing t => (l, r : t) ->

128− l <.> inverse r = inverse (l <.> r)

87+multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)

12988multInverseInversesR l r =

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

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

14397

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

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

149101multNegativeByNegativeIsPositive l r =

150102 rewrite multInverseInversesR (inverse l) r in

151103 rewrite sym $ multInverseInversesL (inverse l) r in

libs/contrib/Data/List/Extra.idrnew file+46

@@ -0,0 +1,46 @@

1+module Data.List.Extra

3+%default total

4+%access export

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.idrdeleted−99

@@ -1,99 +0,0 @@

1−||| Properties of the reverse function.

2−module Data.List.Reverse

3−

4−%default total

5−%access export

6−

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.idrdeleted−56

@@ -1,56 +0,0 @@

1−||| Properties of factorial functions.

2−module Data.Nat.Fact

3−

4−%access public export

5−

6−%default total

7−

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+29−155

@@ -2,9 +2,18 @@ module Data.Nat.Parity

33%access public export

5−----------------------------------------

5+--------------------------------------------------------------------------------

6+-- Parity

7+--------------------------------------------------------------------------------

7−-- Type-level, constructive definitions of parity.

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

817

918||| A nat is Even when it is twice some other nat.

1019Even : Nat -> Type

@@ -14,8 +23,6 @@ Even n = (half : Nat ** n = half * 2)

1423Odd : Nat -> Type

1524Odd n = (haf : Nat ** n = S $ haf * 2)

1625

17−----------------------------------------

18−

1926||| Two more than an Even is Even.

2027add2Even : Even n -> Even (2 + n)

2128add2Even (half ** pf) = (S half ** cong {f = (+) 2} pf)

@@ -45,73 +52,20 @@ succDoublePredPred {k = S _} prf = cong {f = Nat.pred} prf

4552predEvenOdd : Even (S n) -> Odd n

4653predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)

4754

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−

10155||| Every nat is either Even or Odd.

10256evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)

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

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)

11161

11262||| No nat is both Even and Odd.

11363notEvenAndOdd : Even n -> Odd n -> Void

114−notEvenAndOdd en on = notevenandodd (evenEven en) (oddOdd on)

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)

11569

11670||| Evenness is decidable.

11771evenDec : (n : Nat) -> Dec $ Even n

@@ -125,93 +79,13 @@ oddDec n = case evenOrOdd n of

12579 Left even => No $ notEvenAndOdd even

12680 Right odd => Yes odd

12781

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)

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

16887

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)

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

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

46+ , Data.List.Extra

4747

4848 , Data.Matrix

4949 , Data.Matrix.Algebraic

libs/prelude/Prelude/File.idr+2−3

@@ -150,8 +150,7 @@ do_getFileAccessTime h =

150150private

151151do_getFileModifiedTime : Ptr -> IO Integer

152152do_getFileModifiedTime h =

153− do vm <- getMyVM

154− MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> Ptr -> IO (Raw Integer)) vm h

153+ do MkRaw i <- foreign FFI_C "fileModifiedTime" (Ptr -> IO (Raw Integer)) h

155154 pure i

156155

157156private

@@ -176,7 +175,7 @@ export

176175fileModifiedTime : File -> IO (Either FileError Integer)

177176fileModifiedTime (FHandle h)

178177 = do s <- do_getFileModifiedTime h

179− if (s == -1)

178+ if (s < 0)

180179 then Left <$> getFileError

181180 else pure (Right s)

182181

libs/prelude/Prelude/Nat.idr+61−32

@@ -512,18 +512,19 @@ 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' right p =

516− plusLeftCancel right left left' $

517− rewrite plusCommutative right left in

518− rewrite plusCommutative right left' in

519− p

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

520522

521523total plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->

522524 (p : left + right = left) -> right = Z

523−plusLeftLeftRightZero left right p =

524− plusLeftCancel left right Z $

525− rewrite plusZeroRightNeutral left in

526− p

525+plusLeftLeftRightZero Z right p = p

526+plusLeftLeftRightZero (S left) right p =

527+ plusLeftLeftRightZero left right (succInjective _ _ p)

527528

528529-- Mult

529530total multZeroLeftZero : (right : Nat) -> Z * right = Z

@@ -557,21 +558,27 @@ multCommutative (S left) right =

557558 rewrite multRightSuccPlus right left in

558559 Refl

559560

560−total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

561− (left + centre) * right = (left * right) + (centre * right)

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−

568561total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

569562 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

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+

574+total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

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

575582

576583total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

577584 left * (centre * right) = (left * centre) * right

@@ -583,10 +590,18 @@ multAssociative (S left) centre right =

583590 Refl

584591

585592total multOneLeftNeutral : (right : Nat) -> 1 * right = right

586−multOneLeftNeutral right = plusZeroRightNeutral right

593+multOneLeftNeutral Z = Refl

594+multOneLeftNeutral (S right) =

595+ let inductiveHypothesis = multOneLeftNeutral right in

596+ rewrite inductiveHypothesis in

597+ Refl

587598

588599total multOneRightNeutral : (left : Nat) -> left * 1 = left

589−multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left

600+multOneRightNeutral Z = Refl

601+multOneRightNeutral (S left) =

602+ let inductiveHypothesis = multOneRightNeutral left in

603+ rewrite inductiveHypothesis in

604+ Refl

590605

591606-- Minus

592607total minusSuccSucc : (left : Nat) -> (right : Nat) ->

@@ -674,7 +689,10 @@ total powerZeroOne : (base : Nat) -> power base 0 = S Z

674689powerZeroOne base = Refl

675690

676691total powerOneNeutral : (base : Nat) -> power base 1 = base

677−powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base

692+powerOneNeutral Z = Refl

693+powerOneNeutral (S base) =

694+ let inductiveHypothesis = powerOneNeutral base in

695+ rewrite inductiveHypothesis in Refl

678696

679697total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z

680698powerOneSuccOne Z = Refl

@@ -683,7 +701,8 @@ powerOneSuccOne (S exp) =

683701 rewrite inductiveHypothesis in Refl

684702

685703total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base

686−powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl

704+powerSuccSuccMult Z = Refl

705+powerSuccSuccMult (S base) = rewrite multOneRightNeutral base in Refl

687706

688707total powerPowerMultPower : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->

689708 power (power base exp) exp' = power base (exp * exp')

@@ -777,24 +796,34 @@ minimumIdempotent Z = Refl

777796minimumIdempotent (S k) = cong (minimumIdempotent k)

778797

779798total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z

780−minimumZeroZeroRight right = Refl

799+minimumZeroZeroRight Z = Refl

800+minimumZeroZeroRight (S right) = minimumZeroZeroRight right

781801

782802total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z

783−minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

803+minimumZeroZeroLeft Z = Refl

804+minimumZeroZeroLeft (S left) = Refl

784805

785806total minimumSuccSucc : (left : Nat) -> (right : Nat) ->

786807 minimum (S left) (S right) = S (minimum left right)

787−minimumSuccSucc left right = Refl

808+minimumSuccSucc Z Z = Refl

809+minimumSuccSucc (S left) Z = Refl

810+minimumSuccSucc Z (S right) = Refl

811+minimumSuccSucc (S left) (S right) = Refl

788812

789813total maximumZeroNRight : (right : Nat) -> maximum Z right = right

790−maximumZeroNRight right = Refl

814+maximumZeroNRight Z = Refl

815+maximumZeroNRight (S right) = Refl

791816

792817total maximumZeroNLeft : (left : Nat) -> maximum left Z = left

793−maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

818+maximumZeroNLeft Z = Refl

819+maximumZeroNLeft (S left) = Refl

794820

795821total maximumSuccSucc : (left : Nat) -> (right : Nat) ->

796822 S (maximum left right) = maximum (S left) (S right)

797−maximumSuccSucc left right = Refl

823+maximumSuccSucc Z Z = Refl

824+maximumSuccSucc (S left) Z = Refl

825+maximumSuccSucc Z (S right) = Refl

826+maximumSuccSucc (S left) (S right) = Refl

798827

799828total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)

800829sucMaxL Z = Refl

rts/idris_bitstring.c+2

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

1+#include <assert.h>

13#include "idris_rts.h"

35VAL idris_b8const(VM *vm, uint8_t a) {

rts/idris_rts.c+10

@@ -1158,6 +1158,16 @@ 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+

11611171void stackOverflow(void) {

11621172 fprintf(stderr, "Stack overflow");

11631173 exit(-1);

rts/idris_rts.h+4

@@ -507,6 +507,10 @@ 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+

510514// Handle stack overflow.

511515// Just reports an error and exits.

512516

rts/idris_stdfgn.c+2−12

@@ -74,13 +74,13 @@ VAL fileAccessTime(void* h) {

7474 }

7575}

7676

77−VAL fileModifiedTime(VM* vm, void* h) {

77+VAL fileModifiedTime(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 MKBIGUI(vm, buf.st_mtime);

83+ return MKBIGI(buf.st_mtime);

8484 } else {

8585 return MKBIGI(-1);

8686 }

@@ -228,16 +228,6 @@ 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−

241231VAL idris_mkFileError(VM* vm) {

242232 VAL result;

243233 switch(errno) {

rts/idris_stdfgn.h+1−4

@@ -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(VM* vm, void* h);

21+VAL fileModifiedTime(void* h);

2222VAL fileStatusTime(void* h);

2323

2424void* idris_dirOpen(char* dname);

@@ -54,9 +54,6 @@ 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

6057

6158void idris_forceGC();

6259

rts/idris_utf8.c+1

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

11#include "idris_utf8.h"

2+#include <stdio.h>

23#include <string.h>

34#include <stdlib.h>

src/Idris/CmdOptions.hs+2−3

@@ -18,7 +18,6 @@ import Idris.Info (getIdrisVersion)

1818import Idris.Options

1919import IRTS.CodegenCommon

2020

21−import qualified Control.Monad.Fail as Fail

2221import Control.Monad.Trans (lift)

2322import Control.Monad.Trans.Except (throwE)

2423import Control.Monad.Trans.Reader (ask)

@@ -265,7 +264,7 @@ parseCodegen :: String -> Codegen

265264parseCodegen "bytecode" = Bytecode

266265parseCodegen cg = Via IBCFormat (map toLower cg)

267266

268−parseLogCats :: Fail.MonadFail m => String -> m [LogCat]

267+parseLogCats :: Monad m => String -> m [LogCat]

269268parseLogCats s =

270269 case lastMay (readP_to_S doParse s) of

271270 Just (xs, _) -> return xs

@@ -291,7 +290,7 @@ parseLogCats s =

291290 s <- look

292291 fail $ "Category: " ++ s ++ " is not recognised."

293292

294−parseConsoleWidth :: Fail.MonadFail m => String -> m ConsoleWidth

293+parseConsoleWidth :: Monad m => String -> m ConsoleWidth

295294parseConsoleWidth "auto" = return AutomaticWidth

296295parseConsoleWidth "infinite" = return InfinitelyWide

297296parseConsoleWidth 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 -> error $ show pat ++ " is not a constructor or constant (can't happen)"

630+ pat -> fail $ 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,7 +70,6 @@ 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

7473import Control.Monad.State.Strict

7574import Data.Binary hiding (get, put)

7675import Data.Char

@@ -325,11 +324,6 @@ bindTC x k = case x of

325324instance Monad TC where

326325 return x = OK x

327326 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

333327 fail e = Error (InternalMsg e)

334328

335329instance MonadPlus TC where

src/Idris/Parser/Stack.hs+2−16

@@ -5,7 +5,7 @@ Description : Idris parser stack and its primitives.

55License : BSD3

66Maintainer : The Idris Community.

77-}

8−{-# LANGUAGE CPP, ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

8+{-# LANGUAGE ConstraintKinds, FlexibleContexts, MultiParamTypeClasses #-}

99module Idris.Parser.Stack

1010 ( -- * Parsing

1111 Parser(..)

@@ -36,7 +36,6 @@ import Idris.Core.TT (FC(..))

3636import Idris.Output (Message(..))

3737

3838import Control.Arrow (app)

39−import qualified Control.Monad.Fail as Fail

4039import Control.Monad.State.Strict (StateT(..), evalStateT)

4140import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,

4241 runWriterT, tell)

@@ -52,7 +51,7 @@ import qualified Util.Pretty as PP

5251type Parser s = StateT s (WriterT FC (P.Parsec Void String))

5352

5453-- | A constraint for parsing without state

55−type Parsing m = (Fail.MonadFail m, P.MonadParsec Void String m, MonadWriter FC m)

54+type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)

5655

5756-- | Run the Idris parser stack

5857runparser :: Parser st res -> st -> String -> String -> Either ParseError res

@@ -77,20 +76,11 @@ parseErrorOffset = P.errorOffset . parseError

7776instance Message ParseError where

7877 messageExtent err = sourcePositionFC pos

7978 where

80−#if MIN_VERSION_megaparsec(8,0,0)

81− P.PosState {P.pstateSourcePos = pos} =

82− P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

83−#else

8479 (pos, _) = P.reachOffsetNoLine (parseErrorOffset err) (parseErrorPosState err)

85−#endif

8680 messageText = PP.text . init . P.parseErrorTextPretty . parseError

8781 messageSource err = Just sline

8882 where

89−#if MIN_VERSION_megaparsec(8,0,0)

90− (sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

91−#else

9283 (_, sline, _) = P.reachOffset (parseErrorOffset err) (parseErrorPosState err)

93−#endif

9484

9585-- | A fully formatted parse error, with caret and bar, etc.

9686prettyError :: ParseError -> String

@@ -98,11 +88,7 @@ prettyError = P.errorBundlePretty . unParseError

9888

9989{- * Mark and restore -}

10090

101−#if MIN_VERSION_megaparsec(8,0,0)

102−type Mark = P.State String Void

103−#else

10491type Mark = P.State String

105−#endif

10692

10793-- | Retrieve the parser state so we can restart from this point later.

10894mark :: Parsing m => m Mark

stack-11.22.yamldeleted−21

@@ -1,21 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-11.22

3−

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.yamldeleted−20

@@ -1,20 +0,0 @@

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-12.26

3−

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−

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.yamldeleted−17

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

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-15.3

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−

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.yamldeleted−17

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

1−#recheck extra-deps next on resolver or cabal file change

2−resolver: lts-15.4

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−

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.yamlnew file+25

@@ -0,0 +1,25 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-11.4

4+packages:

5+ - location: .

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 120000 → 100644+24−1

@@ -1 +0,0 @@

1−stack-15.4.yaml

@@ -0,0 +1,24 @@

1+#recheck extra-deps next on resolver or cabal file change

2+resolver: lts-13.21

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

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.sh` 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` 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.out` file by doing:

120+7. Generate the `expected` 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.out`. 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`. 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.out` file for every test, do one of the following:

149+To update the `expected` 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.sh` script itself crashes.

160+"Accepted" tests are the ones that update the golden file. A test can still fail if the `run` 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.out"

65+ ref = path </> "expected"

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.sh" : flags)) {cwd = Just path}

95+ let run = (proc "bash" ("run" : 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.out → test/base001/expectedrenamed

The content is the same.

test/base001/run.sh → test/base001/runrenamed+1−1

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

33set -u

55if [[ ${OSTYPE} = 'msys' ]]; then

6− cat expected.out # skip this test on Windows

6+ cat expected # 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.out → test/basic001/expectedrenamed

The content is the same.

test/basic001/run.sh → test/basic001/runrenamed

Only the mode changed.

test/basic002/expected.out → test/basic002/expectedrenamed

The content is the same.

test/basic002/run.sh → test/basic002/runrenamed

Only the mode changed.

test/basic003/expected.out → test/basic003/expectedrenamed

The content is the same.

test/basic003/run.sh → test/basic003/runrenamed

Only the mode changed.

test/basic004/expected.out → test/basic004/expectedrenamed

The content is the same.

test/basic004/run.sh → test/basic004/runrenamed

Only the mode changed.

test/basic005/expected.out → test/basic005/expectedrenamed

The content is the same.

test/basic005/run.sh → test/basic005/runrenamed

Only the mode changed.

test/basic006/expected.out → test/basic006/expectedrenamed

The content is the same.

test/basic006/run.sh → test/basic006/runrenamed

Only the mode changed.

test/basic007/expected.out → test/basic007/expectedrenamed

The content is the same.

test/basic007/run.sh → test/basic007/runrenamed

Only the mode changed.

test/basic008/expected.out → test/basic008/expectedrenamed

The content is the same.

test/basic008/run.sh → test/basic008/runrenamed

Only the mode changed.

test/basic009/expected.out → test/basic009/expectedrenamed

The content is the same.

test/basic009/run.sh → test/basic009/runrenamed

Only the mode changed.

test/basic010/expected.out → test/basic010/expectedrenamed

The content is the same.

test/basic010/run.sh → test/basic010/runrenamed

Only the mode changed.

test/basic011/expected.out → test/basic011/expectedrenamed

The content is the same.

test/basic011/run.sh → test/basic011/runrenamed

Only the mode changed.

test/basic012/expected.out → test/basic012/expectedrenamed

The content is the same.

test/basic012/run.sh → test/basic012/runrenamed

Only the mode changed.

test/basic013/expected.out → test/basic013/expectedrenamed

The content is the same.

test/basic013/run.sh → test/basic013/runrenamed

Only the mode changed.

test/basic014/expected.out → test/basic014/expectedrenamed

The content is the same.

test/basic014/run.sh → test/basic014/runrenamed

Only the mode changed.

test/basic015/expected.out → test/basic015/expectedrenamed

The content is the same.

test/basic015/run.sh → test/basic015/runrenamed

Only the mode changed.

test/basic016/expected.out → test/basic016/expectedrenamed

The content is the same.

test/basic016/run.sh → test/basic016/runrenamed

Only the mode changed.

test/basic017/expected.out → test/basic017/expectedrenamed

The content is the same.

test/basic017/run.sh → test/basic017/runrenamed

Only the mode changed.

test/basic018/expected.out → test/basic018/expectedrenamed

The content is the same.

test/basic018/run.sh → test/basic018/runrenamed

Only the mode changed.

test/basic019/expected.out → test/basic019/expectedrenamed

The content is the same.

test/basic019/run.sh → test/basic019/runrenamed

Only the mode changed.

test/basic020/expected.out → test/basic020/expectedrenamed

The content is the same.

test/basic020/run.sh → test/basic020/runrenamed

Only the mode changed.

test/basic021/expected.out → test/basic021/expectedrenamed

The content is the same.

test/basic021/run.sh → test/basic021/runrenamed

Only the mode changed.

test/basic022/expected.out → test/basic022/expectedrenamed

The content is the same.

test/basic022/run.sh → test/basic022/runrenamed

Only the mode changed.

test/basic023/expected.out → test/basic023/expectedrenamed

The content is the same.

test/basic023/run.sh → test/basic023/runrenamed

Only the mode changed.

test/basic024/expected.out → test/basic024/expectedrenamed

The content is the same.

test/basic024/input.in → test/basic024/inputrenamed

The content is the same.

test/basic024/run.sh → test/basic024/runrenamed+1−1

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

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none < input.in

3+${IDRIS:-idris} $@ --quiet --port none < input

44${IDRIS:-idris} $@ basic024.idr -o basic024

66./basic024

test/basic025/expected.out → test/basic025/expectedrenamed

The content is the same.

test/basic025/input.in → test/basic025/inputrenamed

The content is the same.

test/basic025/run.sh → test/basic025/runrenamed+2−2

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none < input.in

2+${IDRIS:-idris} $@ --quiet --port none < input

33${IDRIS:-idris} $@ -o basic025 basic025.idr

5−./basic025 input.in

5+./basic025 input

77rm -f basic025 *.ibc

test/basic026/expected.out → test/basic026/expectedrenamed

The content is the same.

test/basic026/run.sh → test/basic026/runrenamed

The content is the same.

test/bignum001/expected.out → test/bignum001/expectedrenamed

The content is the same.

test/bignum001/run.sh → test/bignum001/runrenamed

Only the mode changed.

test/bignum002/expected.out → test/bignum002/expectedrenamed

The content is the same.

test/bignum002/run.sh → test/bignum002/runrenamed

Only the mode changed.

test/bignum003/expected.out → test/bignum003/expectedrenamed

The content is the same.

test/bignum003/run.sh → test/bignum003/runrenamed

Only the mode changed.

test/bounded001/expected.out → test/bounded001/expectedrenamed

The content is the same.

test/bounded001/run.sh → test/bounded001/runrenamed

Only the mode changed.

test/buffer001/expected.out → test/buffer001/expectedrenamed

The content is the same.

test/buffer001/run.sh → test/buffer001/runrenamed

Only the mode changed.

test/buffer002/expected.out → test/buffer002/expectedrenamed

The content is the same.

test/buffer002/run.sh → test/buffer002/runrenamed

Only the mode changed.

test/contrib001/expected.out → test/contrib001/expectedrenamed

The content is the same.

test/contrib001/run.sh → test/contrib001/runrenamed

Only the mode changed.

test/corecords001/expected.out → test/corecords001/expectedrenamed

The content is the same.

test/corecords001/run.sh → test/corecords001/runrenamed

Only the mode changed.

test/corecords002/expected.out → test/corecords002/expectedrenamed

The content is the same.

test/corecords002/run.sh → test/corecords002/runrenamed

Only the mode changed.

test/delab001/expected.out → test/delab001/expectedrenamed

The content is the same.

test/delab001/input.in → test/delab001/inputrenamed

The content is the same.

test/delab001/run.sh → test/delab001/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input

33rm -f *.ibc

test/directives001/expected.out → test/directives001/expectedrenamed

The content is the same.

test/directives001/run.sh → test/directives001/runrenamed

Only the mode changed.

test/directives002/expected.out → test/directives002/expectedrenamed

The content is the same.

test/directives002/run.sh → test/directives002/runrenamed

The content is the same.

test/directives003/expected.out → test/directives003/expectedrenamed

The content is the same.

test/directives003/run.sh → test/directives003/runrenamed

Only the mode changed.

test/disambig002/expected.out → test/disambig002/expectedrenamed

The content is the same.

test/disambig002/run.sh → test/disambig002/runrenamed

Only the mode changed.

test/docs001/expected.out → test/docs001/expectedrenamed

The content is the same.

test/docs001/input.in → test/docs001/inputrenamed

The content is the same.

test/docs001/run.sh → test/docs001/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input

33rm *.ibc

test/docs002/expected.out → test/docs002/expectedrenamed

The content is the same.

test/docs002/input.in → test/docs002/inputrenamed

The content is the same.

test/docs002/run.sh → test/docs002/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input.in

2+${IDRIS:-idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input

33rm *.ibc

test/docs003/expected.out → test/docs003/expectedrenamed

The content is the same.

test/docs003/input.in → test/docs003/inputrenamed

The content is the same.

test/docs003/run.sh → test/docs003/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs003.idr < input

33rm *.ibc

test/docs004/expected.out → test/docs004/expectedrenamed

The content is the same.

test/docs004/input.in → test/docs004/inputrenamed

The content is the same.

test/docs004/run.sh → test/docs004/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs004.idr < input

33rm *.ibc

test/docs005/expected.out → test/docs005/expectedrenamed

The content is the same.

test/docs005/input.in → test/docs005/inputrenamed

The content is the same.

test/docs005/run.sh → test/docs005/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs005.idr < input

33rm *.ibc

test/docs006/expected.out → test/docs006/expectedrenamed

The content is the same.

test/docs006/input.in → test/docs006/inputrenamed

The content is the same.

test/docs006/run.sh → test/docs006/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

33rm *.ibc

test/dsl001/expected.out → test/dsl001/expectedrenamed

The content is the same.

test/dsl001/input.in → test/dsl001/inputrenamed

The content is the same.

test/dsl001/run.sh → test/dsl001/runrenamed+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.in

4+${IDRIS:-idris} $@ test001.idr --partial-eval --quiet --port none < input

55rm -f test001 test001.ibc

test/dsl002/expected.out → test/dsl002/expectedrenamed

The content is the same.

test/dsl002/run.sh → test/dsl002/runrenamed

Only the mode changed.

test/dsl002/test.in → test/dsl002/testrenamed

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

67+main = run (readH "test")

6868

6969

test/dsl003/expected.out → test/dsl003/expectedrenamed

The content is the same.

test/dsl003/run.sh → test/dsl003/runrenamed

Only the mode changed.

test/dsl004/expected.out → test/dsl004/expectedrenamed

The content is the same.

test/dsl004/run.sh → test/dsl004/runrenamed

Only the mode changed.

test/effects001/expected.out → test/effects001/expectedrenamed

The content is the same.

test/effects001/run.sh → test/effects001/runrenamed

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.in" Read

34+ Success <- open "testFile" Read

3535 | (FError err) => do

3636 putStrLn "Error!"

3737 pure ()

test/effects001/testFile.in → test/effects001/testFilerenamed

The content is the same.

test/effects002/expected.out → test/effects002/expectedrenamed

The content is the same.

test/effects002/run.sh → test/effects002/runrenamed

Only the mode changed.

test/effects003/expected.out → test/effects003/expectedrenamed

The content is the same.

test/effects003/input.in → test/effects003/inputrenamed

The content is the same.

test/effects003/run.sh → test/effects003/runrenamed+1−1

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

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ hangman.idr --nocolour -p effects -o hangman

3−./hangman < input.in

3+./hangman < input

44rm -f hangman *.ibc

test/effects004/expected.out → test/effects004/expectedrenamed

The content is the same.

test/effects004/input.in → test/effects004/inputrenamed

The content is the same.

test/effects004/run.sh → test/effects004/runrenamed+1−1

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

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ effects004.idr -o effects004 -p effects

3−./effects004 < input.in

3+./effects004 < input

44rm -f effects004 *.ibc

test/effects005/expected.out → test/effects005/expectedrenamed

The content is the same.

test/effects005/run.sh → test/effects005/runrenamed

Only the mode changed.

test/error001/expected.out → test/error001/expectedrenamed

The content is the same.

test/error001/run.sh → test/error001/runrenamed

Only the mode changed.

test/error002/expected.out → test/error002/expectedrenamed

The content is the same.

test/error002/run.sh → test/error002/runrenamed

Only the mode changed.

test/error003/expected.out → test/error003/expectedrenamed

The content is the same.

test/error003/run.sh → test/error003/runrenamed

Only the mode changed.

test/error004/expected.out → test/error004/expectedrenamed

The content is the same.

test/error004/run.sh → test/error004/runrenamed

Only the mode changed.

test/error005/expected.out → test/error005/expectedrenamed

The content is the same.

test/error005/run.sh → test/error005/runrenamed

Only the mode changed.

test/error006/expected.out → test/error006/expectedrenamed

The content is the same.

test/error006/run.sh → test/error006/runrenamed

Only the mode changed.

test/error007/expected.out → test/error007/expectedrenamed

The content is the same.

test/error007/run.sh → test/error007/runrenamed

Only the mode changed.

test/error008/expected.out → test/error008/expectedrenamed

The content is the same.

test/error008/run.sh → test/error008/runrenamed

Only the mode changed.

test/error009/expected.out → test/error009/expectedrenamed

The content is the same.

test/error009/run.sh → test/error009/runrenamed

Only the mode changed.

test/ffi001/expected.out → test/ffi001/expectedrenamed

The content is the same.

test/ffi001/run.sh → test/ffi001/runrenamed

Only the mode changed.

test/ffi002/expected.out → test/ffi002/expectedrenamed

The content is the same.

test/ffi002/run.sh → test/ffi002/runrenamed

Only the mode changed.

test/ffi003/expected.out → test/ffi003/expectedrenamed

The content is the same.

test/ffi003/input.in → test/ffi003/inputrenamed

The content is the same.

test/ffi003/run.sh → test/ffi003/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input

33rm -f *.ibc

test/ffi004/expected.out → test/ffi004/expectedrenamed

The content is the same.

test/ffi004/run.sh → test/ffi004/runrenamed

Only the mode changed.

test/ffi005/expected.out → test/ffi005/expectedrenamed

The content is the same.

test/ffi005/run.sh → test/ffi005/runrenamed

Only the mode changed.

test/ffi006/expected.out → test/ffi006/expectedrenamed

The content is the same.

test/ffi006/run.sh → test/ffi006/runrenamed

Only the mode changed.

test/ffi007/expected.out → test/ffi007/expectedrenamed

The content is the same.

test/ffi007/run.sh → test/ffi007/runrenamed

The content is the same.

test/ffi008/expected.out → test/ffi008/expectedrenamed

The content is the same.

test/ffi008/run.sh → test/ffi008/runrenamed

The content is the same.

test/ffi009/expected.out → test/ffi009/expectedrenamed

The content is the same.

test/ffi009/run.sh → test/ffi009/runrenamed

Only the mode changed.

test/ffi010/expected.out → test/ffi010/expectedrenamed

The content is the same.

test/ffi010/run.sh → test/ffi010/runrenamed

Only the mode changed.

test/ffi011/expected.out → test/ffi011/expectedrenamed

The content is the same.

test/ffi011/ffi011.js → test/ffi011/ffi011renamed

The content is the same.

test/ffi011/run.sh → test/ffi011/runrenamed+1−1

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

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ ffi011.idr --interface -o lib.js

3−node ./ffi011.js

3+node ./ffi011

44rm -f *.ibc lib.js

test/ffi012/expected.out → test/ffi012/expectedrenamed

The content is the same.

test/ffi012/ffi012.js → test/ffi012/ffi012renamed

The content is the same.

test/ffi012/run.sh → test/ffi012/runrenamed

Only the mode changed.

test/ffi013/expected.out → test/ffi013/expectedrenamed

The content is the same.

test/ffi013/run.sh → test/ffi013/runrenamed

Only the mode changed.

test/folding001/expected.out → test/folding001/expectedrenamed

The content is the same.

test/folding001/run.sh → test/folding001/runrenamed

Only the mode changed.

test/idrisdoc001/expected.out → test/idrisdoc001/expectedrenamed

The content is the same.

test/idrisdoc001/run.sh → test/idrisdoc001/runrenamed

Only the mode changed.

test/idrisdoc002/expected.out → test/idrisdoc002/expectedrenamed

The content is the same.

test/idrisdoc002/run.sh → test/idrisdoc002/runrenamed

Only the mode changed.

test/idrisdoc003/expected.out → test/idrisdoc003/expectedrenamed

The content is the same.

test/idrisdoc003/run.sh → test/idrisdoc003/runrenamed

Only the mode changed.

test/idrisdoc004/expected.out → test/idrisdoc004/expectedrenamed

The content is the same.

test/idrisdoc004/run.sh → test/idrisdoc004/runrenamed

Only the mode changed.

test/idrisdoc005/expected.out → test/idrisdoc005/expectedrenamed

The content is the same.

test/idrisdoc005/run.sh → test/idrisdoc005/runrenamed

Only the mode changed.

test/idrisdoc006/expected.out → test/idrisdoc006/expectedrenamed

The content is the same.

test/idrisdoc006/run.sh → test/idrisdoc006/runrenamed

Only the mode changed.

test/idrisdoc007/expected.out → test/idrisdoc007/expectedrenamed

The content is the same.

test/idrisdoc007/run.sh → test/idrisdoc007/runrenamed

Only the mode changed.

test/idrisdoc008/expected.out → test/idrisdoc008/expectedrenamed

The content is the same.

test/idrisdoc008/run.sh → test/idrisdoc008/runrenamed

Only the mode changed.

test/idrisdoc009/expected.out → test/idrisdoc009/expectedrenamed

The content is the same.

test/idrisdoc009/input.in → test/idrisdoc009/inputrenamed

The content is the same.

test/idrisdoc009/run.sh → test/idrisdoc009/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input.in

2+${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input

33rm -f *.ibc

test/interactive001/expected.out → test/interactive001/expectedrenamed

The content is the same.

test/interactive001/input.in → test/interactive001/inputrenamed

The content is the same.

test/interactive001/run.sh → test/interactive001/runrenamed+1−1

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

11#!/usr/bin/env bash

3−${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input.in

3+${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input

55rm -f *.ibc

test/interactive002/expected.out → test/interactive002/expectedrenamed

The content is the same.

test/interactive002/input.in → test/interactive002/inputrenamed

The content is the same.

test/interactive002/run.sh → test/interactive002/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive002.idr < input

33rm -f *.ibc

test/interactive003/expected.out → test/interactive003/expectedrenamed

The content is the same.

test/interactive003/input.in → test/interactive003/inputrenamed

The content is the same.

test/interactive003/run.sh → test/interactive003/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive003.idr < input

33rm -f *.ibc

test/interactive004/expected.out → test/interactive004/expectedrenamed

The content is the same.

test/interactive004/input.in → test/interactive004/inputrenamed

The content is the same.

test/interactive004/run.sh → test/interactive004/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive004.idr < input

33rm -f *.ibc

test/interactive005/expected.out → test/interactive005/expectedrenamed

The content is the same.

test/interactive005/input.in → test/interactive005/inputrenamed

The content is the same.

test/interactive005/run.sh → test/interactive005/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input.in

2+${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input

33rm -f *.ibc

44rm -f hello.bytecode

55rm -f hello

test/interactive006/expected.out → test/interactive006/expectedrenamed

The content is the same.

test/interactive006/input.in → test/interactive006/inputrenamed

The content is the same.

test/interactive006/run.sh → test/interactive006/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input

33rm -f *.ibc

test/interactive007/expected.out → test/interactive007/expectedrenamed

The content is the same.

test/interactive007/input.in → test/interactive007/inputrenamed

The content is the same.

test/interactive007/run.sh → test/interactive007/runrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input.in | perl -pe 's-Data\\Z-Data/Z-g'

2+${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input | perl -pe 's-Data\\Z-Data/Z-g'

test/interactive008/expected.out → test/interactive008/expectedrenamed

The content is the same.

test/interactive008/input.in → test/interactive008/inputrenamed

The content is the same.

test/interactive008/runnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nobanner --nocolor --port none < input

test/interactive008/run.shdeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --port none < input.in

test/interactive009/expected.out → test/interactive009/expectedrenamed

The content is the same.

test/interactive009/input.in → test/interactive009/inputrenamed

The content is the same.

test/interactive009/run.sh → test/interactive009/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive009.idr < input

33rm -f *.ibc

test/interactive010/expected.out → test/interactive010/expectedrenamed

The content is the same.

test/interactive010/input.in → test/interactive010/inputrenamed

The content is the same.

test/interactive010/run.sh → test/interactive010/runrenamed+1−1

@@ -1,2 +1,2 @@

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nobanner --nocolor < input

test/interactive011/expected.out → test/interactive011/expectedrenamed

The content is the same.

test/interactive011/input.in → test/interactive011/inputrenamed

The content is the same.

test/interactive011/run.sh → test/interactive011/runrenamed+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.in

4+${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input

66rm -f *.ibc

test/interactive012/expected.out → test/interactive012/expectedrenamed

The content is the same.

test/interactive012/input.in → test/interactive012/inputrenamed

The content is the same.

test/interactive012/run.sh → test/interactive012/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input.in

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input

33rm -f *.ibc

test/interactive013/expected.out → test/interactive013/expectedrenamed

The content is the same.

test/interactive013/input.in → test/interactive013/inputrenamed

The content is the same.

test/interactive013/run.sh → test/interactive013/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive013.idr < input

33rm -f *.ibc

test/interactive014/expected.out → test/interactive014/expectedrenamed

The content is the same.

test/interactive014/input.in → test/interactive014/inputrenamed

The content is the same.

test/interactive014/run.sh → test/interactive014/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input

33rm -f *.ibc

test/interactive015/expected.out → test/interactive015/expectedrenamed

The content is the same.

test/interactive015/input.in → test/interactive015/inputrenamed

The content is the same.

test/interactive015/run.sh → test/interactive015/runrenamed+1−1

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

11#!/usr/bin/env bash

33cp src/interactive015.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input.in

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

66cat interactive015.idr

test/interactive016/expected.out → test/interactive016/expectedrenamed

The content is the same.

test/interactive016/input.in → test/interactive016/inputrenamed

The content is the same.

test/interactive016/run.sh → test/interactive016/runrenamed+1−1

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

11#!/usr/bin/env bash

33cp src/interactive016.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input.in

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

66cat interactive016.idr

test/interactive017/expected.out → test/interactive017/expectedrenamed

The content is the same.

test/interactive017/run.sh → test/interactive017/runrenamed

Only the mode changed.

test/interactive018/expected.out → test/interactive018/expectedrenamed

The content is the same.

test/interactive018/input.in → test/interactive018/inputrenamed

The content is the same.

test/interactive018/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none Top.idr < input

3+rm -f *.ibc

test/interactive018/run.shdeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none Top.idr < input.in

3−rm -f *.ibc

test/interfaces001/expected.out → test/interfaces001/expectedrenamed

The content is the same.

test/interfaces001/input.in → test/interfaces001/inputrenamed

The content is the same.

test/interfaces001/run.sh → test/interfaces001/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input

33rm -f *.ibc

test/interfaces002/expected.out → test/interfaces002/expectedrenamed

The content is the same.

test/interfaces002/run.sh → test/interfaces002/runrenamed

Only the mode changed.

test/interfaces003/expected.out → test/interfaces003/expectedrenamed

The content is the same.

test/interfaces003/run.sh → test/interfaces003/runrenamed

Only the mode changed.

test/interfaces004/expected.out → test/interfaces004/expectedrenamed

The content is the same.

test/interfaces004/run.sh → test/interfaces004/runrenamed

Only the mode changed.

test/interfaces005/expected.out → test/interfaces005/expectedrenamed

The content is the same.

test/interfaces005/run.sh → test/interfaces005/runrenamed

Only the mode changed.

test/interfaces006/expected.out → test/interfaces006/expectedrenamed

The content is the same.

test/interfaces006/run.sh → test/interfaces006/runrenamed

Only the mode changed.

test/interfaces007/expected.out → test/interfaces007/expectedrenamed

The content is the same.

test/interfaces007/run.sh → test/interfaces007/runrenamed

Only the mode changed.

test/interfaces008/expected.out → test/interfaces008/expectedrenamed

The content is the same.

test/interfaces008/run.sh → test/interfaces008/runrenamed

Only the mode changed.

test/interfaces009/expected.out → test/interfaces009/expectedrenamed

The content is the same.

test/interfaces009/run.sh → test/interfaces009/runrenamed

Only the mode changed.

test/interfaces010/expected.out → test/interfaces010/expectedrenamed

The content is the same.

test/interfaces010/run.sh → test/interfaces010/runrenamed

Only the mode changed.

test/interpret001/expected.out → test/interpret001/expectedrenamed

The content is the same.

test/interpret001/input.in → test/interpret001/inputrenamed

The content is the same.

test/interpret001/run.sh → test/interpret001/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input

33rm -f *.ibc

test/interpret002/expected.out → test/interpret002/expectedrenamed

The content is the same.

test/interpret002/input.in → test/interpret002/inputrenamed

The content is the same.

test/interpret002/run.sh → test/interpret002/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input

33rm -f *.ibc

test/interpret003/expected.out → test/interpret003/expectedrenamed

The content is the same.

test/interpret003/input.in → test/interpret003/inputrenamed

The content is the same.

test/interpret003/run.sh → test/interpret003/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input.in

2+${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input

33rm -f *.ibc

test/io001/expected.out → test/io001/expectedrenamed

The content is the same.

test/io001/run.sh → test/io001/runrenamed

Only the mode changed.

test/io002/expected.out → test/io002/expectedrenamed

The content is the same.

test/io002/run.sh → test/io002/runrenamed

Only the mode changed.

test/io003/expected.out → test/io003/expectedrenamed

The content is the same.

test/io003/run.sh → test/io003/runrenamed

Only the mode changed.

test/layout001/expected.out → test/layout001/expectedrenamed

The content is the same.

test/layout001/run.sh → test/layout001/runrenamed

Only the mode changed.

test/literate001/expected.out → test/literate001/expectedrenamed

The content is the same.

test/literate001/run.sh → test/literate001/runrenamed

Only the mode changed.

test/meta001/expected.out → test/meta001/expectedrenamed

The content is the same.

test/meta001/run.sh → test/meta001/runrenamed

Only the mode changed.

test/meta002/expected.out → test/meta002/expectedrenamed

The content is the same.

test/meta002/run.sh → test/meta002/runrenamed

Only the mode changed.

test/meta003/expected.out → test/meta003/expectedrenamed

The content is the same.

test/meta003/run.sh → test/meta003/runrenamed

Only the mode changed.

test/meta004/expected.out → test/meta004/expectedrenamed

The content is the same.

test/meta004/run.sh → test/meta004/runrenamed

Only the mode changed.

test/pkg001/expected.out → test/pkg001/expectedrenamed

The content is the same.

test/pkg001/run.sh → test/pkg001/runrenamed

Only the mode changed.

test/pkg002/expected.out → test/pkg002/expectedrenamed

The content is the same.

test/pkg002/run.sh → test/pkg002/runrenamed

Only the mode changed.

test/pkg003/expected.out → test/pkg003/expectedrenamed

The content is the same.

test/pkg003/run.sh → test/pkg003/runrenamed

Only the mode changed.

test/pkg004/expected.out → test/pkg004/expectedrenamed

The content is the same.

test/pkg004/run.sh → test/pkg004/runrenamed

Only the mode changed.

test/pkg005/expected.out → test/pkg005/expectedrenamed

The content is the same.

test/pkg005/run.sh → test/pkg005/runrenamed

Only the mode changed.

test/pkg006/expected.out → test/pkg006/expectedrenamed

The content is the same.

test/pkg006/run.sh → test/pkg006/runrenamed

Only the mode changed.

test/pkg007/expected.out → test/pkg007/expectedrenamed

The content is the same.

test/pkg007/input.in → test/pkg007/inputrenamed

The content is the same.

test/pkg007/run.sh → test/pkg007/runrenamed+1−1

@@ -2,6 +2,6 @@

22cd toy

33${IDRIS:-idris} $@ --build toy.ipkg --ibcsubdir ../ibcout

44cd ../ibcout

5−${IDRIS:-idris} $@ --quiet < ../input.in

5+${IDRIS:-idris} $@ --quiet < ../input

66cd ..

77rm -rf ibcout

test/pkg008/expected.out → test/pkg008/expectedrenamed

The content is the same.

test/pkg008/run.sh → test/pkg008/runrenamed

Only the mode changed.

test/pkg009/expected.out → test/pkg009/expectedrenamed

The content is the same.

test/pkg009/run.sh → test/pkg009/runrenamed

Only the mode changed.

test/pkg010/expectednew file+31

@@ -0,0 +1,31 @@

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

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.outdeleted−29

@@ -1,29 +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 |

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.sh → test/pkg010/runrenamed

Only the mode changed.

test/prelude001/expected.out → test/prelude001/expectedrenamed

The content is the same.

test/prelude001/run.sh → test/prelude001/runrenamed

Only the mode changed.

test/primitives001/expected.out → test/primitives001/expectedrenamed

The content is the same.

test/primitives001/input.in → test/primitives001/inputrenamed

The content is the same.

test/primitives001/run.sh → test/primitives001/runrenamed+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.in

5+./substring < input

66rm -f test005 substring *.ibc

test/primitives002/expected.out → test/primitives002/expectedrenamed

The content is the same.

test/primitives002/run.sh → test/primitives002/runrenamed

Only the mode changed.

test/primitives003/expected.out → test/primitives003/expectedrenamed

The content is the same.

test/primitives003/run.sh → test/primitives003/runrenamed

Only the mode changed.

test/primitives004-disabled/expected.out → test/primitives004-disabled/expectedrenamed

The content is the same.

test/primitives004-disabled/run.sh → test/primitives004-disabled/runrenamed

Only the mode changed.

test/primitives005/expected.out → test/primitives005/expectedrenamed

The content is the same.

test/primitives005/run.sh → test/primitives005/runrenamed

The content is the same.

test/primitives006/expected.out → test/primitives006/expectedrenamed

The content is the same.

test/primitives006/run.sh → test/primitives006/runrenamed

Only the mode changed.

test/proof001/expected.out → test/proof001/expectedrenamed

The content is the same.

test/proof001/run.sh → test/proof001/runrenamed

Only the mode changed.

test/proof002/expected.out → test/proof002/expectedrenamed

The content is the same.

test/proof002/run.sh → test/proof002/runrenamed

Only the mode changed.

test/proof003/expected.out → test/proof003/expectedrenamed

The content is the same.

test/proof003/run.sh → test/proof003/runrenamed

Only the mode changed.

test/proof004/expected.out → test/proof004/expectedrenamed

The content is the same.

test/proof004/run.sh → test/proof004/runrenamed

Only the mode changed.

test/proof005/expected.out → test/proof005/expectedrenamed

The content is the same.

test/proof005/run.sh → test/proof005/runrenamed

Only the mode changed.

test/proof006/expected.out → test/proof006/expectedrenamed

The content is the same.

test/proof006/run.sh → test/proof006/runrenamed

Only the mode changed.

test/proof007/expected.out → test/proof007/expectedrenamed

The content is the same.

test/proof007/run.sh → test/proof007/runrenamed

Only the mode changed.

test/proof008/expected.out → test/proof008/expectedrenamed

The content is the same.

test/proof008/run.sh → test/proof008/runrenamed

Only the mode changed.

test/proof009/expected.out → test/proof009/expectedrenamed

The content is the same.

test/proof009/input.in → test/proof009/inputrenamed

The content is the same.

test/proof009/run.sh → test/proof009/runrenamed+1−1

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

11#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input.in

2+${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input

33rm -f *.ibc

test/proof010/expected.out → test/proof010/expectedrenamed

The content is the same.

test/proof010/run.sh → test/proof010/runrenamed

Only the mode changed.

test/proof011/expected.out → test/proof011/expectedrenamed

The content is the same.

test/proof011/run.sh → test/proof011/runrenamed

Only the mode changed.

test/proofsearch001/expected.out → test/proofsearch001/expectedrenamed

The content is the same.

test/proofsearch001/run.sh → test/proofsearch001/runrenamed

Only the mode changed.

test/proofsearch002/expected.out → test/proofsearch002/expectedrenamed

The content is the same.

test/proofsearch002/run.sh → test/proofsearch002/runrenamed

Only the mode changed.

test/proofsearch003/expected.out → test/proofsearch003/expectedrenamed

The content is the same.

test/proofsearch003/run.sh → test/proofsearch003/runrenamed

Only the mode changed.

test/pruviloj001/expected.out → test/pruviloj001/expectedrenamed

The content is the same.

test/pruviloj001/run.sh → test/pruviloj001/runrenamed

Only the mode changed.

test/quasiquote001/expected.out → test/quasiquote001/expectedrenamed

The content is the same.

test/quasiquote001/run.sh → test/quasiquote001/runrenamed

Only the mode changed.

test/quasiquote002/expected.out → test/quasiquote002/expectedrenamed

The content is the same.

test/quasiquote002/run.sh → test/quasiquote002/runrenamed

Only the mode changed.

test/quasiquote003/expected.out → test/quasiquote003/expectedrenamed

The content is the same.

test/quasiquote003/run.sh → test/quasiquote003/runrenamed

Only the mode changed.

test/quasiquote004/expected.out → test/quasiquote004/expectedrenamed

The content is the same.

test/quasiquote004/run.sh → test/quasiquote004/runrenamed

Only the mode changed.

test/quasiquote005/expected.out → test/quasiquote005/expectedrenamed

The content is the same.

test/quasiquote005/run.sh → test/quasiquote005/runrenamed

Only the mode changed.

test/quasiquote006/expected.out → test/quasiquote006/expectedrenamed

The content is the same.

test/quasiquote006/run.sh → test/quasiquote006/runrenamed

Only the mode changed.

test/records001/expected.out → test/records001/expectedrenamed

The content is the same.

test/records001/run.sh → test/records001/runrenamed

Only the mode changed.

test/records002/expected.out → test/records002/expectedrenamed

The content is the same.

test/records002/run.sh → test/records002/runrenamed

Only the mode changed.

test/records003/expected.out → test/records003/expectedrenamed

The content is the same.

test/records003/run.sh → test/records003/runrenamed

Only the mode changed.

test/records004/expected.out → test/records004/expectedrenamed

The content is the same.

test/records004/run.sh → test/records004/runrenamed

Only the mode changed.

test/records005/expected.out → test/records005/expectedrenamed

The content is the same.

test/records005/run.sh → test/records005/runrenamed

Only the mode changed.

test/reg001/expected.out → test/reg001/expectedrenamed

The content is the same.

test/reg001/run.sh → test/reg001/runrenamed

Only the mode changed.

test/reg002/expected.out → test/reg002/expectedrenamed

The content is the same.

test/reg002/run.sh → test/reg002/runrenamed

Only the mode changed.

test/reg004/expected.out → test/reg004/expectedrenamed

The content is the same.

test/reg004/run.sh → test/reg004/runrenamed

Only the mode changed.

test/reg005/expected.out → test/reg005/expectedrenamed

The content is the same.

test/reg005/run.sh → test/reg005/runrenamed

Only the mode changed.

test/reg007/expected.out → test/reg007/expectedrenamed

The content is the same.

test/reg007/run.sh → test/reg007/runrenamed

Only the mode changed.

test/reg013/expected.out → test/reg013/expectedrenamed

The content is the same.

test/reg013/run.sh → test/reg013/runrenamed

Only the mode changed.

test/reg016/expected.out → test/reg016/expectedrenamed

The content is the same.

test/reg016/run.sh → test/reg016/runrenamed

Only the mode changed.

test/reg017/expected.out → test/reg017/expectedrenamed

The content is the same.

test/reg017/run.sh → test/reg017/runrenamed

Only the mode changed.

test/reg020/expected.out → test/reg020/expectedrenamed

The content is the same.

test/reg020/run.sh → test/reg020/runrenamed

Only the mode changed.

test/reg024/expected.out → test/reg024/expectedrenamed

The content is the same.

test/reg024/run.sh → test/reg024/runrenamed

Only the mode changed.

test/reg025/expected.out → test/reg025/expectedrenamed

The content is the same.

test/reg025/run.sh → test/reg025/runrenamed

Only the mode changed.

test/reg027/expected.out → test/reg027/expectedrenamed

The content is the same.

test/reg027/run.sh → test/reg027/runrenamed

Only the mode changed.

test/reg029/expected.out → test/reg029/expectedrenamed

The content is the same.

test/reg029/run.sh → test/reg029/runrenamed

Only the mode changed.

test/reg031/expected.out → test/reg031/expectedrenamed

The content is the same.

test/reg031/run.sh → test/reg031/runrenamed

Only the mode changed.

test/reg032/expected.out → test/reg032/expectedrenamed

The content is the same.

test/reg032/run.sh → test/reg032/runrenamed

Only the mode changed.

test/reg039/expected.out → test/reg039/expectedrenamed

The content is the same.

test/reg039/run.sh → test/reg039/runrenamed

Only the mode changed.

test/reg040/expected.out → test/reg040/expectedrenamed

The content is the same.

test/reg040/run.sh → test/reg040/runrenamed

Only the mode changed.

test/reg041/expected.out → test/reg041/expectedrenamed

The content is the same.

test/reg041/run.sh → test/reg041/runrenamed

Only the mode changed.

test/reg042/expected.out → test/reg042/expectedrenamed

The content is the same.

test/reg042/run.sh → test/reg042/runrenamed

Only the mode changed.

test/reg045/expected.out → test/reg045/expectedrenamed

The content is the same.

test/reg045/run.sh → test/reg045/runrenamed

Only the mode changed.

test/reg048/expected.out → test/reg048/expectedrenamed

The content is the same.

test/reg048/run.sh → test/reg048/runrenamed

Only the mode changed.

test/reg051-disabled/expected.out → test/reg051-disabled/expectedrenamed

The content is the same.

test/reg051-disabled/run.sh → test/reg051-disabled/runrenamed

Only the mode changed.

test/reg052/expected.out → test/reg052/expectedrenamed

The content is the same.

test/reg052/run.sh → test/reg052/runrenamed

Only the mode changed.

test/reg067/expected.out → test/reg067/expectedrenamed

The content is the same.

test/reg067/run.sh → test/reg067/runrenamed

Only the mode changed.

test/reg075/expected.out → test/reg075/expectedrenamed

The content is the same.

test/reg075/input.in → test/reg075/inputrenamed

The content is the same.

test/reg075/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none reg075.idr < input

3+rm -f *.ibc

test/reg075/run.shdeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none reg075.idr < input.in

3−rm -f *.ibc

test/reg076/expected.out → test/reg076/expectedrenamed

The content is the same.

test/reg076/input.in → test/reg076/inputrenamed

The content is the same.

test/reg076/run.sh → test/reg076/runrenamed

Only the mode changed.

test/reg077/expected.out → test/reg077/expectedrenamed

The content is the same.

test/reg077/run.sh → test/reg077/runrenamed

Only the mode changed.

test/regression001/expected.out → test/regression001/expectedrenamed

The content is the same.

test/regression001/run.sh → test/regression001/runrenamed

Only the mode changed.

test/regression002/expected.out → test/regression002/expectedrenamed

The content is the same.

test/regression002/run.sh → test/regression002/runrenamed

Only the mode changed.

test/regression003/expected.out → test/regression003/expectedrenamed

The content is the same.

test/regression003/run.sh → test/regression003/runrenamed

Only the mode changed.

test/sourceLocation001/expected.out → test/sourceLocation001/expectedrenamed

The content is the same.

test/sourceLocation001/run.sh → test/sourceLocation001/runrenamed

Only the mode changed.

test/st001/expected.out → test/st001/expectedrenamed

The content is the same.

test/st001/run.sh → test/st001/runrenamed

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.in" Read

43+ Right fileHandle <- open "testFile" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st001/testFile.in → test/st001/testFilerenamed

The content is the same.

test/st002/expected.out → test/st002/expectedrenamed

The content is the same.

test/st002/run.sh → test/st002/runrenamed

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.in" Read

43+ Right fileHandle <- open "testFile" Read

4444 | Left ferr => do putStrLn (show ferr)

4545 pure ()

4646 count <- new 0

test/st002/testFile.in → test/st002/testFilerenamed

The content is the same.

test/st003/expected.out → test/st003/expectedrenamed

The content is the same.

test/st003/run.sh → test/st003/runrenamed

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.in"

10+ Right str <- readFile "testFile"

1111 | Left ferr => do putStrLn (show ferr)

1212 pure ()

1313 putStrLn str

test/st003/testFile.in → test/st003/testFilerenamed

The content is the same.

test/st004/expected.out → test/st004/expectedrenamed

The content is the same.

test/st004/run.sh → test/st004/runrenamed

Only the mode changed.

test/st005/expected.out → test/st005/expectedrenamed

The content is the same.

test/st005/run.sh → test/st005/runrenamed

Only the mode changed.

test/st006/expected.out → test/st006/expectedrenamed

The content is the same.

test/st006/run.sh → test/st006/runrenamed

Only the mode changed.

test/st007/expected.out → test/st007/expectedrenamed

The content is the same.

test/st007/run.sh → test/st007/runrenamed

Only the mode changed.

test/sugar001/expected.out → test/sugar001/expectedrenamed

The content is the same.

test/sugar001/run.sh → test/sugar001/runrenamed

Only the mode changed.

test/sugar002/expected.out → test/sugar002/expectedrenamed

The content is the same.

test/sugar002/run.sh → test/sugar002/runrenamed

Only the mode changed.

test/sugar003/expected.out → test/sugar003/expectedrenamed

The content is the same.

test/sugar003/run.sh → test/sugar003/runrenamed

Only the mode changed.

test/sugar004/expected.out → test/sugar004/expectedrenamed

The content is the same.

test/sugar004/run.sh → test/sugar004/runrenamed

Only the mode changed.

test/sugar005/expected.out → test/sugar005/expectedrenamed

The content is the same.

test/sugar005/run.sh → test/sugar005/runrenamed

Only the mode changed.

test/syntax001/expected.out → test/syntax001/expectedrenamed

The content is the same.

test/syntax001/run.sh → test/syntax001/runrenamed

Only the mode changed.

test/syntax002/expected.out → test/syntax002/expectedrenamed

The content is the same.

test/syntax002/run.sh → test/syntax002/runrenamed

Only the mode changed.

test/tactics001/expected.out → test/tactics001/expectedrenamed

The content is the same.

test/tactics001/run.sh → test/tactics001/runrenamed

Only the mode changed.

test/totality001/expected.out → test/totality001/expectedrenamed

The content is the same.

test/totality001/run.sh → test/totality001/runrenamed

Only the mode changed.

test/totality002/expected.out → test/totality002/expectedrenamed

The content is the same.

test/totality002/run.sh → test/totality002/runrenamed

Only the mode changed.

test/totality003/expected.out → test/totality003/expectedrenamed

The content is the same.

test/totality003/run.sh → test/totality003/runrenamed

Only the mode changed.

test/totality004/expected.out → test/totality004/expectedrenamed

The content is the same.

test/totality004/run.sh → test/totality004/runrenamed

Only the mode changed.

test/totality005/expected.out → test/totality005/expectedrenamed

The content is the same.

test/totality005/run.sh → test/totality005/runrenamed

Only the mode changed.

test/totality006/expected.out → test/totality006/expectedrenamed

The content is the same.

test/totality006/run.sh → test/totality006/runrenamed

Only the mode changed.

test/totality007/expected.out → test/totality007/expectedrenamed

The content is the same.

test/totality007/run.sh → test/totality007/runrenamed

Only the mode changed.

test/totality008/expected.out → test/totality008/expectedrenamed

The content is the same.

test/totality008/run.sh → test/totality008/runrenamed

Only the mode changed.

test/totality009/expected.out → test/totality009/expectedrenamed

The content is the same.

test/totality009/run.sh → test/totality009/runrenamed

Only the mode changed.

test/totality010/expected.out → test/totality010/expectedrenamed

The content is the same.

test/totality010/run.sh → test/totality010/runrenamed

Only the mode changed.

test/totality011/expected.out → test/totality011/expectedrenamed

The content is the same.

test/totality011/run.sh → test/totality011/runrenamed

Only the mode changed.

test/totality012/expected.out → test/totality012/expectedrenamed

The content is the same.

test/totality012/run.sh → test/totality012/runrenamed

Only the mode changed.

test/totality013/expected.out → test/totality013/expectedrenamed

The content is the same.

test/totality013/run.sh → test/totality013/runrenamed

Only the mode changed.

test/totality014/expected.out → test/totality014/expectedrenamed

The content is the same.

test/totality014/run.sh → test/totality014/runrenamed

Only the mode changed.

test/totality015/expected.out → test/totality015/expectedrenamed

The content is the same.

test/totality015/run.sh → test/totality015/runrenamed

Only the mode changed.

test/totality016/expected.out → test/totality016/expectedrenamed

The content is the same.

test/totality016/run.sh → test/totality016/runrenamed

Only the mode changed.

test/totality017/expected.out → test/totality017/expectedrenamed

The content is the same.

test/totality017/run.sh → test/totality017/runrenamed

Only the mode changed.

test/totality018/expected.out → test/totality018/expectedrenamed

The content is the same.

test/totality018/run.sh → test/totality018/runrenamed

Only the mode changed.

test/totality019/expected.out → test/totality019/expectedrenamed

The content is the same.

test/totality019/run.sh → test/totality019/runrenamed

Only the mode changed.

test/totality020/expected.out → test/totality020/expectedrenamed

The content is the same.

test/totality020/run.sh → test/totality020/runrenamed

Only the mode changed.

test/totality021/expected.out → test/totality021/expectedrenamed

The content is the same.

test/totality021/run.sh → test/totality021/runrenamed

Only the mode changed.

test/totality022/expected.out → test/totality022/expectedrenamed

The content is the same.

test/totality022/run.sh → test/totality022/runrenamed

Only the mode changed.

test/totality023/expected.out → test/totality023/expectedrenamed

The content is the same.

test/totality023/run.sh → test/totality023/runrenamed

Only the mode changed.

test/totality024/expected.out → test/totality024/expectedrenamed

The content is the same.

test/totality024/run.sh → test/totality024/runrenamed

Only the mode changed.

test/totality025/expected.out → test/totality025/expectedrenamed

The content is the same.

test/totality025/run.sh → test/totality025/runrenamed

Only the mode changed.

test/totality026/expected.out → test/totality026/expectedrenamed

The content is the same.

test/totality026/run.sh → test/totality026/runrenamed

Only the mode changed.

test/tutorial001/expected.out → test/tutorial001/expectedrenamed

The content is the same.

test/tutorial001/run.sh → test/tutorial001/runrenamed

Only the mode changed.

test/tutorial002/expected.out → test/tutorial002/expectedrenamed

The content is the same.

test/tutorial002/run.sh → test/tutorial002/runrenamed

Only the mode changed.

test/tutorial003/expected.out → test/tutorial003/expectedrenamed

The content is the same.

test/tutorial003/run.sh → test/tutorial003/runrenamed

Only the mode changed.

test/tutorial004/expected.out → test/tutorial004/expectedrenamed

The content is the same.

test/tutorial004/run.sh → test/tutorial004/runrenamed

Only the mode changed.

test/tutorial005/expected.out → test/tutorial005/expectedrenamed

The content is the same.

test/tutorial005/run.sh → test/tutorial005/runrenamed

Only the mode changed.

test/tutorial006/expected.out → test/tutorial006/expectedrenamed

The content is the same.

test/tutorial006/run.sh → test/tutorial006/runrenamed

Only the mode changed.

test/tutorial007/expected.out → test/tutorial007/expectedrenamed

The content is the same.

test/tutorial007/run.sh → test/tutorial007/runrenamed

Only the mode changed.

test/unique001/expected.out → test/unique001/expectedrenamed

The content is the same.

test/unique001/run.sh → test/unique001/runrenamed

Only the mode changed.

test/unique004/expected.out → test/unique004/expectedrenamed

The content is the same.

test/unique004/run.sh → test/unique004/runrenamed

Only the mode changed.

test/universes001/expected.out → test/universes001/expectedrenamed

The content is the same.

test/universes001/run.sh → test/universes001/runrenamed

Only the mode changed.

test/universes002/expected.out → test/universes002/expectedrenamed

The content is the same.

test/universes002/run.sh → test/universes002/runrenamed

Only the mode changed.

test/views001/expected.out → test/views001/expectedrenamed

The content is the same.

test/views001/run.sh → test/views001/runrenamed

Only the mode changed.

test/views002/expected.out → test/views002/expectedrenamed

The content is the same.

test/views002/run.sh → test/views002/runrenamed

Only the mode changed.

test/views003/expected.out → test/views003/expectedrenamed

The content is the same.

test/views003/run.sh → test/views003/runrenamed

Only the mode changed.