eb780f7...master · Idris-dev

.travis.yml+53−35

since splitsnapshots

unifiedsplit

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

1−dist: trusty

1+dist: xenial

2−sudo: false

3

2

4language: c

3language: c

5

4

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

9

8

10matrix:

9matrix:

11 include:

10 include:

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

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

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

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

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

15− compiler: ": #GHC 7.10.3"

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

17−# Disabled because it's always timing out

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

19−# compiler: ": #GHC 8.0.1"

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

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

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

22 compiler: ": #GHC 8.2.2"

14 compiler: ": #GHC 8.2.2"

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

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

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

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

25 compiler: ": #GHC 8.2.2"

17 compiler: ": #GHC 8.2.2"

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

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

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

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

28 compiler: ": #GHC 8.2.2"

20 compiler: ": #GHC 8.2.2"

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

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

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

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

31−# Caused by the GHC backport to Trusty?

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

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

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

33−# compiler: ": #GHC 8.4.1"

29+ compiler: ": #GHC 8.4.4"

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

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

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

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

36−# compiler: ": #GHC 8.4.1"

35+ compiler: ": #GHC 8.8.3"

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

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

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

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

39−# compiler: ": #GHC 8.4.1"

38+ compiler: ": #GHC 8.8.3"

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

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

41 fast-finish: true

42 fast-finish: true

42

43

43cache:

44cache:

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

56 - unset CC

57 - unset CC

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

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

58 then

59 then

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

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

60 export SED=sed;

61 export SED=sed;

61 export ZCAT=zcat;

62 export ZCAT=zcat;

62 fi

63 fi

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

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

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

72 fi

73 fi

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

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

74

90

75install:

91install:

76 - which cabal

92 - which cabal

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

101 echo "cabal build-cache MISS";

117 echo "cabal build-cache MISS";

102 rm -rf $HOME/.cabsnap;

118 rm -rf $HOME/.cabsnap;

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

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

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

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

105 fi

121 fi

106 # snapshot package-db on cache miss

122 # snapshot package-db on cache miss

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

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

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

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

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

113 fi

129 fi

114

130

131+

115before_script:

132before_script:

116 - ORIGINAL_DIR=$(pwd)

133 - ORIGINAL_DIR=$(pwd)

117− - cabal sdist

134+ - cabal v1-sdist

118 - cd ..

135 - cd ..

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

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

120 - cd ${PKGNAME}*

137 - cd ${PKGNAME}*

121script:

138script:

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

122###

140###

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

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

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

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

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

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

126###

144###

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

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

128− - cabal build

146+ - cabal v1-build

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

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

130###

148###

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

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

132− - cabal copy

150+ - cabal v1-copy

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

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

134###

152###

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

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

136− - cabal register

154+ - cabal v1-register

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

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

138###

156###

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

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

CHANGELOG.md+3

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

1+# New since last release

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

3+

1# New in 1.3.2

4# New in 1.3.2

2+ Documentation added to proof section

5+ Documentation added to proof section

3

6

INSTALL.md+11−2

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

130## Issue with GHC on Ubuntu/Fedora

131

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

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

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

134+

134See the following GHC issue page for more information:

135See the following GHC issue page for more information:

135

136

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

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

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

141

142

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

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

143

144

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

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

146+

147+```bash

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

149+```

150+

151+## GHC 8.6

152+

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

Makefile+4−4

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

30 ./stylize.sh

31

32test_c:

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

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

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

35

36test_js:

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

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

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

39

40test_update:

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

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

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

43

44test_clean:

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

56

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

58doc: dist/setup-config

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

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

60

61lib_doc:

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

README.md+3

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

44

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

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

47+

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

49+of Idris, implemented in Idris.

Setup.hs−33

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

215 autogenComponentModulesDir lbi _ = autogenModulesDir lbi

216#endif

217

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−

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

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

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

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

250rewriteFileEx _ = rewriteFile

220rewriteFileEx _ = rewriteFile

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

353 , postInst = \_ flags pkg local ->

323 , postInst = \_ flags pkg local ->

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

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

355 NoCopyDest pkg local

325 NoCopyDest pkg local

356− , preSDist = idrisPreSDist

357− , sDistHook = idrisSDist (sDistHook simpleUserHooks)

358− , postSDist = idrisPostSDist

359 , testHook = idrisTestHook

326 , testHook = idrisTestHook

360 }

327 }

appveyor.yml+3−3

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

1version: 1.0.{build}

2init:

3- ps: >-

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

4+ choco install cabal --no-progress

5

6 mkdir C:\ghc

7

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

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

9

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

11

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

13

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

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

15

16 cabal v1-update

17

docs/conf.py+2−1

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

251# Additional stuff for the LaTeX preamble.

252'preamble': r'''

253\usepackage{lmodern}

254+\usepackage{textalpha}

254\usepackage[T1]{fontenc}

255\usepackage[T1]{fontenc}

255\usepackage[utf8x]{inputenc}

256\usepackage[utf8x]{inputenc}

256\usepackage{titlesec}

257\usepackage{titlesec}

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

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

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

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

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

302latex_documents = [

303latex_documents = [

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

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

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

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

305]

306]

306

307

docs/effects/introduction.rst+2−1

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

17This tutorial assumes familiarity with pure programming in Idris,

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

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

20−examples directory of the Idris repository.

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

21+is needed when starting Idris.

21

22

22Consider, for example, the following introductory function which

23Consider, for example, the following introductory function which

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

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

docs/parserLibrary/index.rst+1

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

21 introduction

22 lexer

23 parser

24+ whitespace

docs/parserLibrary/introduction.rst+27−15

@@ -5,16 +5,19 @@ Parser Library Introduction

5***************************

6

7The parser library can be used to build Idris structures from text. It involves a

8−certain amount of complexity and so it would typically be used for big projects. An

8+certain amount of complexity and so it would typically be used for big projects.

9−example might be a compiler for another language, written in Idris.

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 is

11+Of course the parser library can also be used to compile to Idris, this is what

12−done in Idris 2 and that is what the this library appears to have been written for.

12+is done in Idris 2 and that is what the this library appears to have been

13+written for.

13

14

14So a secondary use for this tutorial would be to help understanding the internal

15So a secondary use for this tutorial would be to help understanding the internal

15workings of Idris 2.

16workings of Idris 2.

16

17

18+The parser library is used in a similar way to Parsec which is a library for

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

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.

18

21

19.. list-table::

22.. list-table::

20

23

@@ -22,27 +25,36 @@ The parser library is used in a similar way to Parsec which is a library for wri

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

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

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

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

24

27

25−.. image:: ../image/parserTopLevel.png

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

26− :width: 307px

29+ :width: 307px

27− :height: 76px

30+ :height: 76px

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

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

29

32

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

33+The advantage of using two stages, like this, is that things like whitespace and

34+comments don't need to be considered in every parser rule.

31

35

36+The Idris parser library differs from Parsec in that you need to say, in the

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

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.

33

40

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

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

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

43+a string when a rule is matched.

35

44

36−The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a tutorial for the :ref:`parserLibraryParser`. These tutorials have a running

45+The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a

46+tutorial for the :ref:`parserLibraryParser`. These tutorials have a running

37example of a parser for integer expressions. This is a very simple example, there

47example of a parser for integer expressions. This is a very simple example, there

38−may be easier ways to do something so simple, but it illustrates some of the principles.

48+may be easier ways to do something so simple, but it illustrates some of the

49+principles.

39

50

40Parser Library and Idris 2

51Parser Library and Idris 2

41--------------------------

52--------------------------

42

53

43The parser library, in Idris 1, is almost the same as the code that the Idris 2

54The parser library, in Idris 1, is almost the same as the code that the Idris 2

44parser is built on. Even if you only want to use the Idris 1 parser library it

55parser is built on. Even if you only want to use the Idris 1 parser library it

45−is useful to look at the code in the Idris 2 compilers to see how the library can be used.

56+is useful to look at the code in the Idris 2 compilers to see how the library

57+can be used.

46

58

47Idris 2 has at least 3 compilers:

59Idris 2 has at least 3 compilers:

48

60

docs/parserLibrary/lexer.rst+35−27

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

10

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

12

13+.. list-table::

14+

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

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

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

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

17+ in error messages:

15

18

16−.. image:: ../image/tokenise.png

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

17− :width: 330px

20+ :width: 330px

18− :height: 73px

21+ :height: 73px

19− :alt: diagram illustrating these stages of lexer

22+ :alt: diagram illustrating these stages of lexer

20

23

21TokenMap

24TokenMap

22--------

25--------

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

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

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

27- A way to construct these individual tokens.

30- A way to construct these individual tokens.

28

31

29−This is given by the TokenMap which is a list of pairs containing this information:

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

33+this information:

30

34

31.. code-block:: idris

35.. code-block:: idris

32

36

33 (Lexer, String -> tokenType)

37 (Lexer, String -> tokenType)

34

38

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

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

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

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

37

41

38−from Text.Lexer.Core:

42+.. list-table::

39

43

40−.. code-block:: idris

44+ * - from Text.Lexer.Core

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

41

46

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

47+ - .. code-block:: idris

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

44

48

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

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

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

46

51

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

53+

47−.. code-block:: idris

54+ - .. code-block:: idris

48

55

49− myTokenMap : TokenMap Token

56+ myTokenMap : TokenMap Token

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

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

51

58

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

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

53

60

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

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

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

58

65

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

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

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

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

68+'is' function:

61

69

62.. code-block:: idris

70.. code-block:: idris

63

71

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

72

80

73.. list-table::

81.. list-table::

74

82

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

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

76− is guaranteed to consume a character.

84+ the sequence is guaranteed to consume a character.

77

85

78 - .. code-block:: idris

86 - .. code-block:: idris

79

87

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

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

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

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

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

83

91

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

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

85 to consumer a character:

93 to consumer a character:

86

94

87 - .. code-block:: idris

95 - .. code-block:: idris

@@ -130,9 +138,8 @@ is important to indicate blocks. In this case we might want to output a

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

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

131when the indent decreases.

139when the indent decreases.

132

140

133−This topic needs to be more fully expanded here. Until someone does that, a

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

134−possible way to get more information is to see how it is done in Idris 2

142+:ref:`parserLibraryWhitespace`.

135−: https://github.com/edwinb/Idris2/blob/master/src/Parser/Lexer.idr

136

143

137Simple Expression Example for Lexer

144Simple Expression Example for Lexer

138-----------------------------------

145-----------------------------------

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

160so we need:

167so we need:

161

168

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

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

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

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

164- Opening and closing Parentheses.

171- Opening and closing Parentheses.

165

172

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

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

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

177 | EndInput

184 | EndInput

178

185

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

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

180−implement 'show' for these tokens:

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

181

188

182.. code-block:: idris

189.. code-block:: idris

183

190

@@ -267,8 +274,9 @@ input string as parameters:

267 Int,

274 Int,

268 String)

275 String)

269

276

270−The lexer uses potentially infinite data structures. It has recursive arguments (codata type) so code is lazy. In the output above the indexes have not been computed but we can

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

271−pick out the tokens:

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

272

280

273- (Number 1)

281- (Number 1)

274- (Operator "+")

282- (Operator "+")

docs/parserLibrary/parser.rst+205−117

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

3Parser

4======

5

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

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

7

8

8.. code-block:: idris

9.. code-block:: idris

9

10

@@ -17,12 +18,13 @@ If successful this returns 'Right' with a pair of

17

18

18otherwise it returns 'Left' with the error message.

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

19

20

20−So we need to define the Grammar for our parser, this is done using the following

21+So we need to define the grammar for our parser, this is done using the following

21−'Grammar' data structure. This is a combinator structure, similar in principle to the

22+'Grammar' data structure. This is a combinator structure, similar in principle

22−recogniser combinator for the lexer, which was discussed on the previous page.

23+to the recogniser combinator for the lexer, which was discussed on the

24+previous page.

23

25

24−As with the Recogniser the Grammar type is dependent on a boolean 'consumes'

26+As with the Recogniser the ``Grammar`` type is dependent on a boolean 'consumes'

25−value which allows us to ensure that complicated Grammar structures will always

27+value which allows us to ensure that complicated ``Grammar`` structures will always

26consume input.

28consume input.

27

29

28.. code-block:: idris

30.. code-block:: idris

@@ -51,13 +53,13 @@ consume input.

51 Grammar tok c1 ty -> Grammar tok c2 ty ->

53 Grammar tok c1 ty -> Grammar tok c2 ty ->

52 Grammar tok (c1 && c2) ty

54 Grammar tok (c1 && c2) ty

53

55

54−So an example of a Grammer type may look something like this:

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

55−'Grammar (TokenData ExpressionToken) True Integer'.

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

56−

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

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

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

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

59to what is done in Idris 2

60to what is done in Idris 2

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

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

62+)

61

63

62.. code-block:: idris

64.. code-block:: idris

63

65

@@ -69,12 +71,12 @@ Parser Example

69--------------

71--------------

70

72

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

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

72−this page we will go on to implement a parser for this running example.

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

73

75

74.. list-table::

76.. list-table::

75

77

76− * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something

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

77− like this:

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

78 - .. code-block:: idris

80 - .. code-block:: idris

79

81

80 <expr> ::= <integer literal>

82 <expr> ::= <integer literal>

@@ -87,8 +89,8 @@ this page we will go on to implement a parser for this running example.

87

89

88.. list-table::

90.. list-table::

89

91

90− * - To start, here is a Grammar to parse an integer literal (that is, a

92+ * - To start, here is a grammar to parse an integer literal (that is, a

91− sequence of numbers).

93+ sequence of numeric characters).

92

94

93 - .. code-block:: idris

95 - .. code-block:: idris

94

96

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

111 (Integer, List (TokenData ExpressionToken))

113 (Integer, List (TokenData ExpressionToken))

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

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

113

115

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

116+As required, if we pass it a string which is a number literal then it will

115−number in the 'Right' option.

117+return the number in the 'Right' option.

116

118

117.. code-block:: idris

119.. code-block:: idris

118

120

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

142

144

143.. list-table::

145.. list-table::

144

146

145− * - The 'intLiteral' function above uses the 'terminal' function to

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

146 construct the grammar

148 construct the grammar

147 - .. code-block:: idris

149 - .. code-block:: idris

148

150

@@ -172,10 +174,10 @@ Idris 2 uses a slightly different version which stores an error message like

172 OParen => Just 0

174 OParen => Just 0

173 _ => Nothing)

175 _ => Nothing)

174

176

175−Integer value is not really relevant for parenthesis so '0' is used as

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

176a default value.

178a default value.

177

179

178−As before, we can test this out with a function like this:

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

179

181

180.. code-block:: idris

182.. code-block:: idris

181

183

@@ -200,10 +202,10 @@ error for anything else:

200 List (TokenData ExpressionToken))

202 List (TokenData ExpressionToken))

201

203

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

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

203−for 'openParen' followed by 'intLiteral', the two Grammars are combined using

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

204−'<*>'. The 'map const' part uses the integer value from the first.

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

205

207

206−The following test is looking for '(' followed by a number:

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

207

209

208.. code-block:: idris

210.. code-block:: idris

209

211

@@ -211,8 +213,8 @@ The following test is looking for '(' followed by a number:

211 (Integer, List (TokenData ExpressionToken))

213 (Integer, List (TokenData ExpressionToken))

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

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

213

215

214−We can see below that '(' followed by a number is successfully parsed but other

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

215−token lists are not:

217+required, other token lists are not:

216

218

217.. code-block:: idris

219.. code-block:: idris

218

220

@@ -260,28 +262,96 @@ token lists are not:

260

262

261.. list-table::

263.. list-table::

262

264

263− * - Now we can generate a Grammar for an expression inside parenthesis like this.

265+ * - Now we can generate a Grammar for an expression inside parenthesis

266+ like this.

264

267

265 - .. code-block:: idris

268 - .. code-block:: idris

266

269

267 paren : Rule Integer -> Rule Integer

270 paren : Rule Integer -> Rule Integer

268 paren exp = openParen *> exp <* closeParen

271 paren exp = openParen *> exp <* closeParen

269

272

270−The use of '*>' and '<*' instead of '<*>' is an easy way to use the integer

273+The use of ``*>`` and ``<*`` instead of ``<*>`` is an easy way to use the integer

271value from the inner expression.

274value from the inner expression.

272

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+

273.. list-table::

340.. list-table::

274

341

275− * - Now for the operations, in this case: '+', '-' and '*'.

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

276− The syntax we require is that operators like '+' are infix operators, which

343+ The syntax we require for these infix operators

277− would require a definition like this:

344+ would require recursive grammars like this:

278

345

279 - .. code-block:: idris

346 - .. code-block:: idris

280

347

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

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.

282

352

283−This is a potentially infinite structure which is not total.

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

284−In order to work up to this gradually I will start with prefix operators (sometimes known as Polish notation) then modify later for infix operators.

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

285

355

286.. list-table::

356.. list-table::

287

357

@@ -291,7 +361,7 @@ In order to work up to this gradually I will start with prefix operators (someti

291

361

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

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

293

363

294−where 'op' is defined like this:

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

295

365

296.. code-block:: idris

366.. code-block:: idris

297

367

@@ -304,7 +374,13 @@ where 'op' is defined like this:

304

374

305.. list-table::

375.. list-table::

306

376

307− * - and 'add' is defined like this:

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.

308

384

309 - .. code-block:: idris

385 - .. code-block:: idris

310

386

@@ -318,40 +394,37 @@ where 'op' is defined like this:

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

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

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

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

320

396

321−Where:

322

397

323−- x is the add operator.

324−- y is the first operand.

325−- z is the second operand.

326

398

327The resulting integer will be the sum of the two operands.

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

328

400

329−The other operators are defined in a similar way:

401+.. list-table::

330

402

331−.. code-block:: idris

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

332

404

333− subInt : Integer -> Integer -> Integer

405+ - .. code-block:: idris

334− subInt a b = a-b

335

406

336− export

407+ subInt : Integer -> Integer -> Integer

337− sub : Grammar tok c1 Integer ->

408+ subInt a b = a-b

338− Grammar tok c2 Integer ->

339− Grammar tok c3 Integer ->

340− Grammar tok ((c1 || c2) || c3) Integer

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

342

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

343

416

344− multInt : Integer -> Integer -> Integer

417+ multInt : Integer -> Integer -> Integer

345− multInt a b = a*b

418+ multInt a b = a*b

346

419

347− export

420+ export

348− mult : Grammar tok c1 Integer ->

421+ mult : Grammar tok c1 Integer ->

349− Grammar tok c2 Integer ->

422+ Grammar tok c2 Integer ->

350− Grammar tok c3 Integer ->

423+ Grammar tok c3 Integer ->

351− Grammar tok ((c1 || c2) || c3) Integer

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

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

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

353

426

354−So the top level Grammar can now be defined as follows. Note that this is

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

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

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

356

429

357.. code-block:: idris

430.. code-block:: idris

@@ -404,7 +477,7 @@ Then an invalid syntax:

404 List (TokenData ExpressionToken))

477 List (TokenData ExpressionToken))

405

478

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

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

407−then it will return 'Right' (to indicate success)

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

408

481

409.. code-block:: idris

482.. code-block:: idris

410

483

@@ -431,8 +504,8 @@ Infix Notation

431--------------

504--------------

432

505

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

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

434−'+ expr expr') but the aim is to implemented an infix notation (like this:

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

435−'expr + expr'). To do this we must be able to deal with potentially

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

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

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

437

510

438First alter the grammar to have infix operations:

511First alter the grammar to have infix operations:

@@ -490,16 +563,20 @@ If we have a rule like this:

490

563

491 A -> (x<*>y) <|> (x<*>z)

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

492

565

493−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has already consumed 'x', so now 'x<*>z' will fail.

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.

494

568

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

495−so we could write code to backtrack. That is 'try' 'x<*>y' without consuming so that, if the first token succeeds but the following tokens fail, then the first tokens would not be consumed.

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

571+first tokens would not be consumed.

496

572

497Another approach is left factoring:

573Another approach is left factoring:

498

574

499Left Factoring

575Left Factoring

500--------------

576--------------

501

577

502−Replace the rule with two rules (that is we add a non-terminal symbol) so for example, instead of:

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

579+for example, instead of:

503

580

504.. code-block:: idris

581.. code-block:: idris

505

582

@@ -512,54 +589,68 @@ we add an extra rule to give:

512 A -> x<*>N

589 A -> x<*>N

513 N -> y <|> z

590 N -> y <|> z

514

591

515−That is we convert a general context-free grammar to a LL(1) grammar. Although not every context-free grammar can be converted to a LL(1) grammar.

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.

516

594

517−This still does not solve the infinite recursion issue and there is another problem: the precedence of the operators +, - and * is not explicit.

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.

518

597

519−To resolve this we can alter the example like this:

598+.. list-table::

520−

521−.. code-block:: idris

522

599

523− paren : Rule Integer -> Rule Integer

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

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

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

525

602

526− addInt : Integer -> Integer -> Integer

603+ - .. code-block:: idris

527− addInt a b = a+b

528

604

529− subInt : Integer -> Integer -> Integer

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

530− subInt a b = a-b

531

606

532− multInt : Integer -> Integer -> Integer

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

533− multInt a b = a*b

534

608

535− partial

609+ 'factor' ::=

536− expr : Rule Integer

610+ number

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

537

612

538− partial

539− exprAtom : Rule Integer

540− exprAtom = intLiteral <|> (paren expr)

541

613

542− partial

614+.. code-block:: idris

543− expr1 : Rule Integer

544− expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)

545

615

546− partial

547− exprMult : Rule Integer

616+ expr : Rule Integer

548− exprMult = expr1 <|> exprAtom

549

617

550− partial

618+ factor : Rule Integer

619+ factor = intLiteral <|> do

620+ openParen

621+ r <- expr

622+ closeParen

623+ pure r

624+

551− expr2 : Rule Integer

625+ term : Rule Integer

552− expr2 = map addInt exprMult <*> ((op "+") *> exprMult)

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

640+ (Integer, List (TokenData ExpressionToken))

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

553

642

554− partial

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

555− exprAdd : Rule Integer

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

556− exprAdd = expr2 <|> exprMult

557

645

558− partial

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

559− expr3 : Rule Integer

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

560− expr3 = map subInt exprAdd <*> ((op "-") *> expr)

561

648

562− expr = expr3 <|> exprAdd

649+ main : IO ()

650+ main = do

651+ putStr "alg>"

652+ x <- getLine

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

563

654

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

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

565

656

@@ -569,44 +660,41 @@ As the following tests show, this now handles infix operators and precedence.

569

660

570 - .. code-block:: idris

661 - .. code-block:: idris

571

662

572− *parserExInfix> test "2*3"

663+ *algebraREPL> :exec

573− Right (6,

664+ alg>2*3

574− []) : Either (ParseError (TokenData ExpressionToken))

665+ right (6, [])

575− (Integer, List (TokenData ExpressionToken))

576

666

577 * - Check that atomic number literals work:

667 * - Check that atomic number literals work:

578

668

579 - .. code-block:: idris

669 - .. code-block:: idris

580

670

581− *parserExInfix> test "2"

671+ *algebraREPL> :exec

582− Right (2,

672+ alg>2

583− []) : Either (ParseError (TokenData ExpressionToken))

673+ right (2, [])

584− (Integer, List (TokenData ExpressionToken))

585

674

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

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

587

676

588 - .. code-block:: idris

677 - .. code-block:: idris

589

678

590− *parserExInfix> test "2+3*4"

679+ *algebraREPL> :exec

591− Right (14,

680+ alg>2+3*4

592− []) : Either (ParseError (TokenData ExpressionToken))

681+ right (14, [])

593− (Integer, List (TokenData ExpressionToken))

594

682

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

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

596

684

597 - .. code-block:: idris

685 - .. code-block:: idris

598

686

599− *parserExInfix> test "3*4+2"

687+ *algebraREPL> :exec

600− Right (14,

688+ alg>3*4+2

601− []) : Either (ParseError (TokenData ExpressionToken))

689+ right (14, [])

602− (Integer, List (TokenData ExpressionToken))

603

690

604 * - Also precedence can be overridden by parenthesis.

691 * - Also precedence can be overridden by parenthesis.

605

692

606 - .. code-block:: idris

693 - .. code-block:: idris

607

694

608− *parserExInfix> test "(2+3)*4"

695+ *algebraREPL> :exec

609− Right (20,

696+ alg>(2+3)*4

610− []) : Either (ParseError (TokenData ExpressionToken))

697+ right (20, [])

611− (Integer, List (TokenData ExpressionToken))

612

698

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

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

docs/parserLibrary/whitespace.rstnew file+250

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

1+.. _parserLibraryWhitespace:

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:

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

37

38

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

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

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

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

41−using the `closure-compiler

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

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

42+Google.

43

44::

45

docs/reference/misc.rst+5−5

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

115 import Syntax.PreorderReasoning

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

117 multThree a b c =

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

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

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

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

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

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

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

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

122− (c * a * b) QED

122+ (c * a * b) QED

123

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

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

idris-tutorial.pdf

Binary file not shown.

idris.cabal+101−47

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

1+Cabal-Version: 2.4

1Name: idris

2Name: idris

2Version: 1.3.2

3Version: 1.3.2

3−License: BSD3

4+License: BSD-3-Clause

4License-file: LICENSE

5License-file: LICENSE

5Author: Edwin Brady

6Author: Edwin Brady

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

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

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

41 .

42 .

42 * Hugs style interactive environment

43 * Hugs style interactive environment

43

44

44−Cabal-Version: >= 1.22

45−

46Build-type: Custom

45Build-type: Custom

47

46

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

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

49

48

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

50+-- heavily discouraged.

50Data-files: idrisdoc/styles.css

51Data-files: idrisdoc/styles.css

51− jsrts/jsbn/jsbn-browser.js

52+ jsrts/jsbn/*.js

52− jsrts/jsbn/jsbn-node.js

53− jsrts/Runtime-common.js

54− jsrts/Runtime-javascript.js

55− jsrts/Runtime-node.js

53+ jsrts/*.js

56 jsrts/jsbn/LICENSE

54 jsrts/jsbn/LICENSE

55+ rts/Makefile

56+ rts/*.c

57+ rts/seL4/*.c

57− rts/arduino/idris_main.c

58+ rts/arduino/*.c

58− rts/idris_bitstring.c

59+ rts/windows/*.c

59− rts/idris_bitstring.h

60+ rts/windows/*.h

60− rts/idris_gc.c

61+ rts/*.h

61− rts/idris_gc.h

62+ rts/seL4/CMakeLists.txt

62− rts/idris_gmp.c

63+ rts/seL4/README.md

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

80

64

81Extra-doc-files:

65Extra-doc-files:

82 CHANGELOG.md

66 CHANGELOG.md

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

86 README.md

70 README.md

87 RELEASE-CHECKS.md

71 RELEASE-CHECKS.md

88 idris-tutorial.pdf

72 idris-tutorial.pdf

73+ man/idris.1

89 samples/effects/*.idr

74 samples/effects/*.idr

90 samples/misc/*.idr

75 samples/misc/*.idr

91− samples/misc/*.lidr

92 samples/tutorial/*.idr

76 samples/tutorial/*.idr

77+ samples/ST/*.idr

78+ samples/ST/Graphics/*.idr

79+ samples/ST/Net/*.idr

80+ samples/misc/*.lidr

93

81

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

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

95Extra-source-files:

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

96

142

97source-repository head

143source-repository head

98 type: git

144 type: git

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

100

146

101custom-setup

147custom-setup

102 setup-depends:

148 setup-depends:

103− Cabal >= 1.10 && <2.5,

149+ Cabal >= 2.4 && < 3.1,

104 base >= 4 && <5,

150 base >= 4 && <5,

105 directory,

151 directory,

106 filepath,

152 filepath,

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

261 Util.Pretty

307 Util.Pretty

262 , Util.Net

308 , Util.Net

263

309

264−

265−

266− -- Auto Generated

267 , Paths_idris

310 , Paths_idris

268 , Version_idris

311 , Version_idris

269 , Tools_idris

312 , Tools_idris

270 , BuildFlags_idris

313 , BuildFlags_idris

271

314

315+ -- Auto Generated

316+ Autogen-modules: Paths_idris

317+ , Version_idris

318+ , Tools_idris

319+ , BuildFlags_idris

320+

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

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

273 , aeson >= 0.6 && < 1.5

322 , aeson >= 0.6 && < 1.5

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

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

275− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

276 , ansi-wl-pprint < 0.7

325 , ansi-wl-pprint < 0.7

277 , array >= 0.4.0.1 && < 0.6

326 , array >= 0.4.0.1 && < 0.6

278 , base64-bytestring < 1.1

327 , base64-bytestring < 1.1

279 , binary >= 0.8.4.1 && < 0.9

328 , binary >= 0.8.4.1 && < 0.9

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

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

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

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

282 , bytestring < 0.11

331 , bytestring < 0.11

283− , cheapskate >= 0.1.1 && < 0.2

332+ , cheapskate >= 0.1.1.2 && < 0.2

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

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

285 , containers >= 0.5 && < 0.7

334 , containers >= 0.5 && < 0.7

286 , deepseq < 1.5

335 , deepseq < 1.5

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

289 , fingertree >= 0.1.4.1 && < 0.2

338 , fingertree >= 0.1.4.1 && < 0.2

290 , haskeline >= 0.7 && < 0.8

339 , haskeline >= 0.7 && < 0.8

291 , ieee754 >= 0.7 && < 0.9

340 , ieee754 >= 0.7 && < 0.9

292− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

293 , mtl >= 2.1 && < 2.3

342 , mtl >= 2.1 && < 2.3

294− , network >= 2.7 && < 2.9

343+ , network >= 2.7 && < 3.1.2

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

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

296 , parser-combinators >= 1.0.0

345 , parser-combinators >= 1.0.0

297 , pretty < 1.2

346 , pretty < 1.2

298 , process < 1.7

347 , process < 1.7

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

300 , safe >= 0.3.9

349 , safe >= 0.3.9

301 , split < 0.3

350 , split < 0.3

302 , terminal-size < 0.4

351 , terminal-size < 0.4

303− , text >=1.2.1.0 && < 1.3

352+ , text >=1.2.1.0 && < 1.4

304− , time >= 1.4 && < 1.9

353+ , time >= 1.4 && < 2.0

305 , transformers >= 0.5 && < 0.6

354 , transformers >= 0.5 && < 0.6

306 , uniplate >=1.6 && < 1.7

355 , uniplate >=1.6 && < 1.7

307 , unordered-containers < 0.3

356 , unordered-containers < 0.3

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

309 , vector < 0.13

358 , vector < 0.13

310 , vector-binary-instances < 0.3

359 , vector-binary-instances < 0.3

311 , zip-archive > 0.2.3.5 && < 0.5

360 , zip-archive > 0.2.3.5 && < 0.5

312− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

313 , async < 2.3

362 , async < 2.3

314

363

315 if !impl(ghc >= 8.0)

364 if !impl(ghc >= 8.0)

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

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

366+ , fail == 4.9.0.*

317

367

318 Default-Language: Haskell2010

368 Default-Language: Haskell2010

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

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

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

332 cpp-options: -DIDRIS_GMP

382 cpp-options: -DIDRIS_GMP

333 if flag(freestanding)

383 if flag(freestanding)

334 other-modules: Target_idris

384 other-modules: Target_idris

385+ autogen-modules: Target_idris

335 cpp-options: -DFREESTANDING

386 cpp-options: -DFREESTANDING

336 if flag(CI)

387 if flag(CI)

337 ghc-options: -Werror

388 ghc-options: -Werror

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

365 , filepath

416 , filepath

366 , directory

417 , directory

367 , haskeline >= 0.7

418 , haskeline >= 0.7

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

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

369 , tagged

420 , tagged

370 , tasty >= 0.8

421 , tasty >= 0.8

371 , tasty-golden >= 2.0

422 , tasty-golden >= 2.0

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

380

431

381Executable idris-codegen-c

432Executable idris-codegen-c

382 Main-is: Main.hs

433 Main-is: Main.hs

434+ autogen-modules: Paths_idris

383 other-modules: Paths_idris

435 other-modules: Paths_idris

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

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

385

437

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

395

447

396Executable idris-codegen-javascript

448Executable idris-codegen-javascript

397 Main-is: Main.hs

449 Main-is: Main.hs

450+ autogen-modules: Paths_idris

398 other-modules: Paths_idris

451 other-modules: Paths_idris

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

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

400

453

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

410

463

411Executable idris-codegen-node

464Executable idris-codegen-node

412 Main-is: Main.hs

465 Main-is: Main.hs

466+ autogen-modules: Paths_idris

413 other-modules: Paths_idris

467 other-modules: Paths_idris

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

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

415

469

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

@@ -17,21 +17,22 @@ record Iso a b where

17

18-- Isomorphism properties

19

20−||| Isomorphism is Reflexive

20+||| Isomorphism is reflexive

21isoRefl : Iso a a

22−isoRefl = MkIso id id (\x => Refl) (\x => Refl)

22+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)

23

24||| Isomorphism is transitive

25isoTrans : Iso a b -> Iso b c -> Iso a c

26isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =

27− MkIso (\x => to' (to x))

27+ MkIso xto xfrom xtoFrom xfromTo where

28− (\y => from (from' y))

28+ xto : a -> c

29− (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=

29+ xto = to' . to

30+ xfrom : c -> a

31+ xfrom = from . from'

32+ xtoFrom : (z : c) -> xto (xfrom z) = z

30− (to' (from' y)) ={ toFrom' y }=

33+ xtoFrom z = rewrite toFrom $ from' z in toFrom' z

31− y QED)

34+ xfromTo : (x : a) -> xfrom (xto x) = x

32− (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=

35+ xfromTo x = rewrite fromTo' (to x) in fromTo x

33− (from (to x)) ={ fromTo x }=

34− x QED)

35

36

36Category Iso where

37Category Iso where

37 id = isoRefl

38 id = isoRefl

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

99

100

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

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

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

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

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

103− (MkIso to from toFrom fromTo)

103+eitherCong (MkIso to from toFrom fromTo)

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

105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2

106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'

@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2

143

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

145pairUnitRight : Iso (a, ()) a

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

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

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

148− ok (x, ()) = Refl

149

147

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

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

151pairUnitLeft : Iso ((), a) a

149pairUnitLeft : Iso ((), a) a

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

161

159

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

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

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

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

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

165− (MkIso to from toFrom fromTo)

162+pairCong (MkIso to from toFrom fromTo)

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

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

167 MkIso to'' from'' iso1 iso2

164 MkIso to'' from'' iso1 iso2

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

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

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

205

202

206||| Products distribute over sums

203||| Products distribute over sums

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

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

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

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

209

206

210

207

211-- Enable preorder reasoning syntax over isomorphisms

208-- Enable preorder reasoning syntax over isomorphisms

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

222-- Isomorphisms over Maybe

219-- Isomorphisms over Maybe

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

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

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

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

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

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

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

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

227 ok1 Nothing = Refl

224 ok1 Nothing = Refl

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

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

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

253 () QED

250 () QED

254

251

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

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

256−eitherMaybeLeftMaybe {a} {b} =

253+eitherMaybeLeftMaybe =

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

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

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

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

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

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

@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =

263

260

264

261

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

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

266−eitherMaybeRightMaybe {a} {b} =

263+eitherMaybeRightMaybe =

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

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

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

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

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

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

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

288 fb (FS x) = Refl

285 fb (FS x) = Refl

289

286

290finZeroBot : Iso (Fin 0) Void

287finZeroBot : Iso (Fin 0) Void

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

288+finZeroBot = MkIso (void . uninhabited)

292− (\x => void x)

289+ void

293 (\x => void x)

290 (\x => void x)

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

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

295

292

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

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

6

7%access export

8

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+

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

23+||| -0 = 0 in any verified group.

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

24+inverseNeutralIsNeutral : VerifiedGroup t =>

25+ inverse (the t A.neutral) = A.neutral

11inverseNeutralIsNeutral {t} =

26inverseNeutralIsNeutral {t} =

12− let zero = the t neutral

27+ let e = the t neutral in

13− step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)

14− step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1

28+ rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in

15− in

16− replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2

29+ rewrite monoidNeutralIsNeutralR $ inverse e in

30+ inverseSquaredIsIdentity e

17

31

18−||| A proof that -(-x) = x in any verified group.

32+||| -(x + y) = -y + -x in any verified group.

19−inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x

33+inverseOfSum : VerifiedGroup t => (l, r : t) ->

20−inverseSquaredIsIdentity {t} x =

34+ inverse (l <+> r) = inverse r <+> inverse l

35+inverseOfSum {t} l r =

36+ let

21− let zero = the t neutral

37+ e = the t neutral

22− step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))

38+ il = inverse l

23− step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1

39+ ir = inverse r

24− step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2

40+ sum = l <+> r

41+ ilr = inverse sum

42+ iril = ir <+> il

43+ ile = il <+> e

44+ in

45+ -- expand

25− step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3

46+ rewrite sym $ monoidNeutralIsNeutralR ilr in

26− 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

27− replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4

60+ rewrite monoidNeutralIsNeutralL e in

61+ Refl

28

62

29−||| A proof that -(x + y) = -x - y in any verified abelian group.

63+||| -(x + y) = -x + -y in any verified abelian group.

30−inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r

64+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->

65+ inverse (l <+> r) = inverse l <+> inverse r

31−inverseDistributesOverGroupOp {t} l r =

66+inverseDistributesOverGroupOp 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

67+ rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in

68+ inverseOfSum l r

45

69

46−||| A proof that anything multiplied by zero yields zero back.

70+||| Anything multiplied by zero yields zero back in a verified ring.

47−multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral

71+multNeutralAbsorbingL : VerifiedRing t => (r : t) ->

72+ A.neutral <.> r = A.neutral

48−multNeutralAbsorbingL r =

73+multNeutralAbsorbingL {t} r =

49− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)

74+ let

75+ e = the t neutral

76+ ir = inverse r

77+ exr = e <.> r

78+ iexr = inverse exr

79+ in

50− step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1

80+ rewrite sym $ monoidNeutralIsNeutralR exr in

51− step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2

81+ rewrite sym $ groupInverseIsInverseR exr in

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

82+ rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in

55− step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6

83+ rewrite groupInverseIsInverseR exr in

56− in

84+ rewrite sym $ ringOpIsDistributiveR e e r in

57− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7

85+ rewrite monoidNeutralIsNeutralR e in

86+ groupInverseIsInverseR exr

58

87

59−||| A proof that anything multiplied by zero yields zero back.

88+||| Anything multiplied by zero yields zero back in a verified ring.

60−multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral

89+multNeutralAbsorbingR : VerifiedRing t => (l : t) ->

90+ l <.> A.neutral = A.neutral

61−multNeutralAbsorbingR l =

91+multNeutralAbsorbingR {t} l =

62− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)

92+ let

63− step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1

93+ e = the t neutral

64− step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2

94+ il = inverse l

65− step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3

95+ lxe = l <.> e

66− step5 = cong {f = \x => x <+> inverse l} step4

96+ ilxe = inverse lxe

97+ in

98+ rewrite sym $ monoidNeutralIsNeutralL lxe in

99+ rewrite sym $ groupInverseIsInverseL lxe in

67− step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5

100+ rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in

68− step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6

101+ rewrite groupInverseIsInverseL lxe in

69− in

102+ rewrite sym $ ringOpIsDistributiveL l e e in

70− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7

103+ rewrite monoidNeutralIsNeutralL e in

104+ groupInverseIsInverseL lxe

71

105

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

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

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

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

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

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

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

75multInverseInversesL l r =

110multInverseInversesL 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

76− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)

121+ rewrite groupInverseIsInverseL l in

77− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1

122+ rewrite multNeutralAbsorbingL r in

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

123+ monoidNeutralIsNeutralL i_lxr

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

84

124

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

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

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

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

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

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

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

88multInverseInversesR l r =

129multInverseInversesR l r =

89− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)

130+ let

90− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1

131+ ir = inverse r

91− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2

132+ lxr = l <.> r

133+ lxir = l <.> ir

134+ ilxr = inverse lxr

135+ in

92− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3

136+ rewrite sym $ monoidNeutralIsNeutralL lxir in

137+ rewrite sym $ groupInverseIsInverseL lxr in

93− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4

138+ rewrite semigroupOpIsAssociative lxir lxr ilxr in

139+ rewrite sym $ ringOpIsDistributiveL l ir r in

94− step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5

140+ rewrite groupInverseIsInverseR r in

95− in

141+ rewrite multNeutralAbsorbingR l in

96− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6

142+ monoidNeutralIsNeutralR ilxr

97

143

98−||| A proof that multiplication of inverses is the same as multiplication of original

144+||| Multiplication of inverses is the same as multiplication of

99−||| elements. (-x)(-y) = xy

145+||| original elements.

146+||| (-x)(-y) = xy

100−multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r

147+multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->

148+ inverse l <.> inverse r = l <.> r

101multNegativeByNegativeIsPositive l r =

149multNegativeByNegativeIsPositive l r =

102 rewrite multInverseInversesR (inverse l) r in

150 rewrite multInverseInversesR (inverse l) r in

103 rewrite sym $ multInverseInversesL (inverse l) r in

151 rewrite sym $ multInverseInversesL (inverse l) r in

libs/contrib/Data/List/Extra.idrdeleted−46

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

1−module Data.List.Extra

2−

3−%default total

4−%access export

5−

6−||| The final segment of the accumulator is the final segment of the result.

7−reverseOntoAcc : (xs, ys, zs : List a) ->

8− reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs

9−reverseOntoAcc [] _ _ = Refl

10−reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

11−

12−||| Serves as a specification for reverseOnto.

13−reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

14−reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

15−

16−||| The reverse of an empty list is an empty list. Together with reverseCons,

17−||| serves as a specification for reverse.

18−reverseNil : reverse [] = []

19−reverseNil = Refl

20−

21−||| The reverse of a cons is the reverse of the tail followed by the head.

22−||| Together with reverseNil serves as a specification for reverse.

23−reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]

24−reverseCons x xs = reverseOntoSpec [x] xs

25−

26−||| Reversing an append is appending reversals backwards.

27−reverseAppend : (xs, ys : List a) ->

28− reverse (xs ++ ys) = reverse ys ++ reverse xs

29−reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))

30−reverseAppend (x :: xs) ys =

31− rewrite reverseCons x (xs ++ ys) in

32− rewrite reverseAppend xs ys in

33− rewrite reverseCons x xs in

34− sym $ appendAssociative (reverse ys) (reverse xs) [x]

35−

36−||| Reversing a singleton list is a no-op.

37−reverseSingletonId : (x : a) -> reverse [x] = [x]

38−reverseSingletonId _ = Refl

39−

40−||| Reversing a reverse gives the original.

41−reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

42−reverseReverseId [] = Refl

43−reverseReverseId (x :: xs) =

44− rewrite reverseCons x xs in

45− rewrite reverseAppend (reverse xs) [x] in

46− cong $ reverseReverseId xs

libs/contrib/Data/List/Reverse.idrnew file+99

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

1+||| Properties of the reverse function.

2+module Data.List.Reverse

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.idrnew file+56

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

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

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

2

3%access public export

4

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

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

6−-- Parity

7−--------------------------------------------------------------------------------

8

6

9−mutual

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

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

17

8

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

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

19Even : Nat -> Type

10Even : Nat -> Type

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

23Odd : Nat -> Type

14Odd : Nat -> Type

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

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

25

16

17+----------------------------------------

18+

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

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

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

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

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

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

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

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

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

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

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

54

47

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+

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

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

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

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

57−evenOrOdd Z = Left (0 ** Refl)

103+evenOrOdd n = case evenorodd n of

58−evenOrOdd (S k) = case evenOrOdd k of

104+ Left e => Left $ evenEvenConverse e

59− Left (half ** pf) => Right (half ** cong {f = S} pf)

105+ Right o => Right $ oddOddConverse o

60− Right (haf ** pf) => Left (S haf ** cong {f = S} pf)

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

61

111

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

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

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

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

64−notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd

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

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)

69

115

70||| Evenness is decidable.

116||| Evenness is decidable.

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

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

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

79 Left even => No $ notEvenAndOdd even

125 Left even => No $ notEvenAndOdd even

80 Right odd => Yes odd

126 Right odd => Yes odd

81

127

82−mutual

128+----------------------------------------

83− ||| Evens are even.

129+

84− evenEven : Even n -> even n = True

130+||| An Odd is the successor of an Even.

85− evenEven {n = Z} _ = Refl

131+oddSuccEven : Odd n -> (m : Nat ** (n = S m, Even m))

86− evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

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)

87

168

88− ||| Odds are odd.

169+||| A helper fact.

89− oddOdd : Odd n -> odd n = True

170+multShuffle : (a, b, c : Nat) ->

90− oddOdd {n = Z} (_ ** pf) = absurd pf

171+ (a * c) * (b * c) = ((a * b) * c) * c

91− oddOdd {n = S _} pf = evenEven $ predOddEven pf

172+multShuffle a b c =

173+ rewrite multAssociative (a * c) b c in

174+ rewrite multCommutative (a * c) b in

175+ rewrite multAssociative b a c in

176+ rewrite multCommutative b a in

177+ Refl

178+

179+||| Even times Even is Even.

180+evenMultEven : Even j -> Even k -> Even (j * k)

181+evenMultEven (half_j ** pf_j) (half_k ** pf_k) =

182+ (half_j * half_k * 2 **

183+ rewrite pf_j in

184+ rewrite pf_k in

185+ multShuffle half_j half_k 2)

186+

187+||| Odd times Even is Even.

188+oddMultEven : Odd j -> Even k -> Even (j * k)

189+oddMultEven oj (half_k ** pf_k) =

190+ let

191+ (i ** (ipj, ei)) = oddSuccEven oj

192+ (half_ik ** oik) = evenMultEven ei (half_k ** pf_k)

193+ in

194+ (half_k + half_ik **

195+ rewrite multDistributesOverPlusLeft half_k half_ik 2 in

196+ rewrite ipj in

197+ rewrite oik in

198+ rewrite pf_k in

199+ Refl)

200+

201+||| Even times Odd is Even.

202+evenMultOdd : Even j -> Odd k -> Even (j * k)

203+evenMultOdd {j} {k} ej ok = rewrite multCommutative j k in oddMultEven ok ej

204+

205+||| Odd times Odd is Odd.

206+oddMultOdd : Odd j -> Odd k -> Odd (j * k)

207+oddMultOdd oj (haf_k ** pf_k) =

208+ let

209+ (i ** (ipj, ei)) = oddSuccEven oj

210+ (half_ik ** eik) = evenMultOdd ei (haf_k ** pf_k)

211+ in

212+ (haf_k + half_ik **

213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in

214+ rewrite ipj in

215+ rewrite eik in

216+ rewrite pf_k in

217+ Refl)

libs/contrib/contrib.ipkg+1−1

@@ -43,7 +43,7 @@ modules = CFFI

43 , Data.Heap

44 , Data.IOArray

45 , Data.List.Zipper

46− , Data.List.Extra

46+ , Data.List.Reverse

47

48 , Data.Matrix

49 , Data.Matrix.Algebraic

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

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

150private

151do_getFileModifiedTime : Ptr -> IO Integer

152do_getFileModifiedTime h =

153+ do vm <- getMyVM

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

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

154 pure i

155 pure i

155

156

156private

157private

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

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

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

176fileModifiedTime (FHandle h)

177fileModifiedTime (FHandle h)

177 = do s <- do_getFileModifiedTime h

178 = do s <- do_getFileModifiedTime h

178− if (s < 0)

179+ if (s == -1)

179 then Left <$> getFileError

180 then Left <$> getFileError

180 else pure (Right s)

181 else pure (Right s)

181

182

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

@@ -512,19 +512,18 @@ plusLeftCancel (S left) right right' p =

512

513total plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->

514 (p : left + right = left' + right) -> left = left'

515−plusRightCancel left left' Z p = rewrite sym (plusZeroRightNeutral left) in

515+plusRightCancel left left' right p =

516− rewrite sym (plusZeroRightNeutral left') in

516+ plusLeftCancel right left left' $

517− p

517+ rewrite plusCommutative right left in

518−plusRightCancel left left' (S right) p =

518+ rewrite plusCommutative right left' in

519− plusRightCancel left left' right

519+ p

520− (succInjective _ _ (rewrite plusSuccRightSucc left right in

521− rewrite plusSuccRightSucc left' right in p))

522

520

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

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

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

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

525−plusLeftLeftRightZero Z right p = p

523+plusLeftLeftRightZero left right p =

526−plusLeftLeftRightZero (S left) right p =

524+ plusLeftCancel left right Z $

527− plusLeftLeftRightZero left right (succInjective _ _ p)

525+ rewrite plusZeroRightNeutral left in

526+ p

528

527

529-- Mult

528-- Mult

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

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

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

558 rewrite multRightSuccPlus right left in

557 rewrite multRightSuccPlus right left in

559 Refl

558 Refl

560

559

561−total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

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

563−multDistributesOverPlusRight Z centre right = Refl

564−multDistributesOverPlusRight (S left) centre right =

565− let inductiveHypothesis = multDistributesOverPlusRight left centre right in

566− rewrite inductiveHypothesis in

567− rewrite plusAssociative (plus centre (mult left centre)) right (mult left right) in

568− rewrite sym (plusAssociative centre (mult left centre) right) in

569− rewrite plusCommutative (mult left centre) right in

570− rewrite plusAssociative centre right (mult left centre) in

571− rewrite plusAssociative (plus centre right) (mult left centre) (mult left right) in

572− Refl

573−

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

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

575 (left + centre) * right = (left * right) + (centre * right)

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

576−multDistributesOverPlusLeft Z centre right = Refl

562+multDistributesOverPlusLeft Z centre right = Refl

577−multDistributesOverPlusLeft (S left) centre right =

563+multDistributesOverPlusLeft (S k) centre right =

578− let inductiveHypothesis = multDistributesOverPlusLeft left centre right in

564+ rewrite multDistributesOverPlusLeft k centre right in

579− rewrite inductiveHypothesis in

580− rewrite plusAssociative right (mult left right) (mult centre right) in

565+ rewrite plusAssociative right (k * right) (centre * right) in

581− Refl

566+ Refl

567+

568+total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->

569+ left * (centre + right) = (left * centre) + (left * right)

570+multDistributesOverPlusRight left centre right =

571+ rewrite multCommutative left (centre + right) in

572+ rewrite multCommutative left centre in

573+ rewrite multCommutative left right in

574+ multDistributesOverPlusLeft centre right left

582

575

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

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

584 left * (centre * right) = (left * centre) * right

577 left * (centre * right) = (left * centre) * right

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

590 Refl

583 Refl

591

584

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

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

593−multOneLeftNeutral Z = Refl

586+multOneLeftNeutral right = plusZeroRightNeutral right

594−multOneLeftNeutral (S right) =

595− let inductiveHypothesis = multOneLeftNeutral right in

596− rewrite inductiveHypothesis in

597− Refl

598

587

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

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

600−multOneRightNeutral Z = Refl

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

601−multOneRightNeutral (S left) =

602− let inductiveHypothesis = multOneRightNeutral left in

603− rewrite inductiveHypothesis in

604− Refl

605

590

606-- Minus

591-- Minus

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

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

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

689powerZeroOne base = Refl

674powerZeroOne base = Refl

690

675

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

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

692−powerOneNeutral Z = Refl

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

693−powerOneNeutral (S base) =

694− let inductiveHypothesis = powerOneNeutral base in

695− rewrite inductiveHypothesis in Refl

696

678

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

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

698powerOneSuccOne Z = Refl

680powerOneSuccOne Z = Refl

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

701 rewrite inductiveHypothesis in Refl

683 rewrite inductiveHypothesis in Refl

702

684

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

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

704−powerSuccSuccMult Z = Refl

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

686+powerSuccSuccMult base = rewrite multOneRightNeutral base in Refl

706

687

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

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

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

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

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

796minimumIdempotent (S k) = cong (minimumIdempotent k)

777minimumIdempotent (S k) = cong (minimumIdempotent k)

797

778

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

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

799−minimumZeroZeroRight Z = Refl

780+minimumZeroZeroRight right = Refl

800−minimumZeroZeroRight (S right) = minimumZeroZeroRight right

801

781

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

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

803−minimumZeroZeroLeft Z = Refl

783+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl

804−minimumZeroZeroLeft (S left) = Refl

805

784

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

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

807 minimum (S left) (S right) = S (minimum left right)

786 minimum (S left) (S right) = S (minimum left right)

808−minimumSuccSucc Z Z = Refl

787+minimumSuccSucc left right = Refl

809−minimumSuccSucc (S left) Z = Refl

810−minimumSuccSucc Z (S right) = Refl

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

812

788

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

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

814−maximumZeroNRight Z = Refl

790+maximumZeroNRight right = Refl

815−maximumZeroNRight (S right) = Refl

816

791

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

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

818−maximumZeroNLeft Z = Refl

793+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl

819−maximumZeroNLeft (S left) = Refl

820

794

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

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

822 S (maximum left right) = maximum (S left) (S right)

796 S (maximum left right) = maximum (S left) (S right)

823−maximumSuccSucc Z Z = Refl

797+maximumSuccSucc left right = Refl

824−maximumSuccSucc (S left) Z = Refl

825−maximumSuccSucc Z (S right) = Refl

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

827

798

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

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

829sucMaxL Z = Refl

800sucMaxL Z = Refl

rts/idris_bitstring.c−2

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

1−#include <assert.h>

2−

3#include "idris_rts.h"

1#include "idris_rts.h"

4

2

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

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

rts/idris_rts.c−10

@@ -1158,16 +1158,6 @@ void idris_disableBuffering(void) {

1158 setvbuf(stdout, NULL, _IONBF, 0);

1159}

1160

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−

1171void stackOverflow(void) {

1161void stackOverflow(void) {

1172 fprintf(stderr, "Stack overflow");

1162 fprintf(stderr, "Stack overflow");

1173 exit(-1);

1163 exit(-1);

rts/idris_rts.h−4

@@ -507,10 +507,6 @@ const char *idris_getArg(int i);

507// disable stdin/stdout buffering

508void idris_disableBuffering(void);

509

510−#ifndef SEL4

511−int idris_usleep(int usec);

512−#endif // SEL4

513−

514// Handle stack overflow.

510// Handle stack overflow.

515// Just reports an error and exits.

511// Just reports an error and exits.

516

512

rts/idris_stdfgn.c+12−2

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

74 }

75}

76

77−VAL fileModifiedTime(void* h) {

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

78 FILE* f = (FILE*)h;

79 int fd = fileno(f);

80

81 struct stat buf;

82 if (fstat(fd, &buf) == 0) {

83− return MKBIGI(buf.st_mtime);

83+ return MKBIGUI(vm, buf.st_mtime);

84 } else {

85 return MKBIGI(-1);

86 }

@@ -228,6 +228,16 @@ VAL idris_clock(VM* vm) {

228 return result;

229}

230

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+

231VAL idris_mkFileError(VM* vm) {

241VAL idris_mkFileError(VM* vm) {

232 VAL result;

242 VAL result;

233 switch(errno) {

243 switch(errno) {

rts/idris_stdfgn.h+4−1

@@ -18,7 +18,7 @@ int fileSize(void* h);

18

19// Return a negative number if not a file (e.g. directory or device)

20VAL fileAccessTime(void* h);

21−VAL fileModifiedTime(void* h);

21+VAL fileModifiedTime(VM* vm, void* h);

22VAL fileStatusTime(void* h);

23

24void* idris_dirOpen(char* dname);

@@ -54,6 +54,9 @@ char* getEnvPair(int i);

54

55VAL idris_time();

56VAL idris_clock(VM* vm);

57+#ifndef SEL4

58+int idris_usleep(int usec);

59+#endif // SEL4

57

60

58void idris_forceGC();

61void idris_forceGC();

59

62

rts/idris_utf8.c−1

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

1#include "idris_utf8.h"

2−#include <stdio.h>

3#include <string.h>

2#include <string.h>

4#include <stdlib.h>

3#include <stdlib.h>

5

4

src/Idris/CmdOptions.hs+3−2

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

18import Idris.Options

19import IRTS.CodegenCommon

20

21+import qualified Control.Monad.Fail as Fail

21import Control.Monad.Trans (lift)

22import Control.Monad.Trans (lift)

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

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

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

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

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

264parseCodegen "bytecode" = Bytecode

265parseCodegen "bytecode" = Bytecode

265parseCodegen cg = Via IBCFormat (map toLower cg)

266parseCodegen cg = Via IBCFormat (map toLower cg)

266

267

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

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

268parseLogCats s =

269parseLogCats s =

269 case lastMay (readP_to_S doParse s) of

270 case lastMay (readP_to_S doParse s) of

270 Just (xs, _) -> return xs

271 Just (xs, _) -> return xs

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

290 s <- look

291 s <- look

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

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

292

293

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

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

294parseConsoleWidth "auto" = return AutomaticWidth

295parseConsoleWidth "auto" = return AutomaticWidth

295parseConsoleWidth "infinite" = return InfinitelyWide

296parseConsoleWidth "infinite" = return InfinitelyWide

296parseConsoleWidth s =

297parseConsoleWidth s =

src/Idris/Core/CaseTree.hs+1−1

@@ -627,7 +627,7 @@ groupCons cs = gc [] cs

627 PConst cval -> return $ addConG cval (ps, res) acc

628 PSuc n -> return $ addg False CSuc [n] (ps, res) acc

629 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc

630− pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

630+ pat -> error $ show pat ++ " is not a constructor or constant (can't happen)"

631

632 addg uniq c conargs res []

633 = [ConGroup uniq c [(conargs, res)]]

src/Idris/Core/TT.hs+6

@@ -70,6 +70,7 @@ import qualified Prelude as S (Semigroup(..))

70import Control.Applicative (Alternative, Applicative(..))

71import qualified Control.Applicative as A (Alternative(..))

72import Control.DeepSeq (($!!))

73+import qualified Control.Monad.Fail as Fail

73import Control.Monad.State.Strict

74import Control.Monad.State.Strict

74import Data.Binary hiding (get, put)

75import Data.Binary hiding (get, put)

75import Data.Char

76import Data.Char

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

324instance Monad TC where

325instance Monad TC where

325 return x = OK x

326 return x = OK x

326 x >>= k = bindTC x k

327 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

327 fail e = Error (InternalMsg e)

333 fail e = Error (InternalMsg e)

328

334

329instance MonadPlus TC where

335instance MonadPlus TC where

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

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

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

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

9module Idris.Parser.Stack

10 ( -- * Parsing

11 Parser(..)

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

36import Idris.Output (Message(..))

37

38import Control.Arrow (app)

39+import qualified Control.Monad.Fail as Fail

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

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

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

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

41 runWriterT, tell)

42 runWriterT, tell)

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

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

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

52

53

53-- | A constraint for parsing without state

54-- | A constraint for parsing without state

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

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

55

56

56-- | Run the Idris parser stack

57-- | Run the Idris parser stack

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

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

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

76instance Message ParseError where

77instance Message ParseError where

77 messageExtent err = sourcePositionFC pos

78 messageExtent err = sourcePositionFC pos

78 where

79 where

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

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

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

83+#else

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

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

85+#endif

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

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

81 messageSource err = Just sline

87 messageSource err = Just sline

82 where

88 where

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

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

91+#else

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

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

93+#endif

84

94

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

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

86prettyError :: ParseError -> String

96prettyError :: ParseError -> String

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

88

98

89{- * Mark and restore -}

99{- * Mark and restore -}

90

100

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

102+type Mark = P.State String Void

103+#else

91type Mark = P.State String

104type Mark = P.State String

105+#endif

92

106

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

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

94mark :: Parsing m => m Mark

108mark :: Parsing m => m Mark

stack-11.22.yamlnew file+21

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

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

2+resolver: lts-11.22

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

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

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

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

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

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

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

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

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

2−resolver: lts-11.4

3−

4−packages:

5− - location: .

6−

7−extra-deps:

8− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

9− - Cabal-2.2.0.1@sha256:2a80d8fb655474f0eaeb20434c47f64f84e6302e55973056f00df8ca050b9683

10− - megaparsec-7.0.4

11− - parser-combinators-1.0.0

12− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

13− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

14−

15−flags:

16− idris:

17− FFI: true

18− GMP: true

19−

20−ghc-options:

21− idris: -fwarn-unused-imports -fwarn-unused-binds

22−

23−nix:

24− enable: false

25− shell-file: stack-shell.nix

stack.yamlmode 100644 → 120000+1−24

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

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

2−resolver: lts-13.21

3−

4−extra-deps:

5− - network-2.8.0.0@sha256:aae171e6c6028a7791dbe4de5b9d2da398056359e3cc7927465ffa3cdae1aa0b

6− - megaparsec-7.0.4

7− - parser-combinators-1.0.0

8− - zip-archive-0.3.3@sha256:47cf2d66cc8e237f7226837758e1b041e24048ef3820d3d10276c500edb921bf

9− - containers-0.5.11.0@sha256:28ad7337057442f75bc689315ab4ec7bdf5e6b2c39668f306672cecd82c02798

10− - tasty-rerun-1.1.14@sha256:ba9c19a281535bea566e1044bc02c36ef17abcb310af4b6a149ec11780c7ce35

11− - binary-0.8.7.0@sha256:ae3e6cca723ac55c54bbb3fa771bcf18142bc727afd57818e66d6ee6c8044f12

12− - text-1.2.4.0@sha256:8c24450feb8e3bbb7ea3e17af24ef57e85db077c4bf53e5bcc345b283d1b1d5b

13−

14−flags:

15− idris:

16− FFI: true

17− GMP: true

18−

19−ghc-options:

20− idris: -fwarn-unused-imports -fwarn-unused-binds

21−

22−nix:

23− enable: false

24− shell-file: stack-shell.nix

@@ -0,0 +1 @@

1+stack-15.4.yaml

test/README.md+5−5

@@ -113,18 +113,18 @@ and somewhat self-explanatory.

113

1141. Choose the family your test shall belong to and remember its identifier.

1152. Pick the next available integer in the test family. It will be the index.

116−3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run` script.

116+3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run.sh` script.

1174. Modify the `run` script to your liking. If you want to call the idris executable, write `${IDRIS:-idris} $@`.

1185. Add any file you may need in the directory. If they don't end in `.idr`, you should remember them for the next step.

1196. Add your test in `TestData.hs`. Each family has a list of `(Index, CompatCodegen)`. See the next section for the available values in `CompatCodegen`. In most cases, you should write `( 42, ANY)`.

120−7. Generate the `expected` file by doing:

120+7. Generate the `expected.out` file by doing:

121 ```

122 # Using cabal

123 cabal test --test-options="--pattern foo042 --accept"

124 # Using stack

125 stack test --test-arguments="--pattern foo042 --accept"

126 ```

127−8. Check the content of `expected`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

127+8. Check the content of `expected.out`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

128

129### Specifying compatible backends

130

@@ -146,7 +146,7 @@ Currently, `NONE` has the same effect as `ANY`, but this will change.

146

147### Updating golden files

148

149−To update the `expected` file for every test, do one of the following:

149+To update the `expected.out` file for every test, do one of the following:

150

151```

152# Using make

@@ -157,4 +157,4 @@ cabal test --test-options="--accept"

157stack test --test-arguments="--accept"

158```

159

160−"Accepted" tests are the ones that update the golden file. A test can still fail if the `run` script itself crashes.

160+"Accepted" tests are the ones that update the golden file. A test can still fail if the `run.sh` script itself crashes.

test/TestRun.hs+2−2

@@ -62,7 +62,7 @@ ingredients = defaultIngredients ++

62test :: String -> String -> IO () -> TestTree

63test testName path = goldenVsFileDiff testName diff ref output

64 where

65− ref = path </> "expected"

65+ ref = path </> "expected.out"

66 output = path </> "output"

67 diff ref new | os == "openbsd" = ["diff", "-u", new, ref]

68 | otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]

@@ -92,7 +92,7 @@ mkGoldenTests testFamilies flags =

92-- this thing.

93runTest :: String -> Flags -> IO ()

94runTest path flags = do

95− let run = (proc "bash" ("run" : flags)) {cwd = Just path}

95+ let run = (proc "bash" ("run.sh" : flags)) {cwd = Just path}

96 (_, output, error_out) <- readCreateProcessWithExitCode run ""

97 writeFile (path </> "output") (normalise output)

98 when (error_out /= "") $ hPutStrLn stderr ("\nError: " ++ path ++ "\n" ++ error_out)

test/base001/expected → test/base001/expected.outrenamed

The content is the same.

test/base001/run → test/base001/run.shrenamed+1−1

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

3set -u

4

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

6− cat expected # skip this test on Windows

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

7else

8 ${IDRIS:-idris} "$@" --build base001.ipkg | grep -v 'make.*:'

9 ./base001 2>&1 | grep -v '^sh:.*\./does-not-exist:'

test/basic001/expected → test/basic001/expected.outrenamed

The content is the same.

test/basic001/run → test/basic001/run.shrenamed

Only the mode changed.

test/basic002/expected → test/basic002/expected.outrenamed

The content is the same.

test/basic002/run → test/basic002/run.shrenamed

Only the mode changed.

test/basic003/expected → test/basic003/expected.outrenamed

The content is the same.

test/basic003/run → test/basic003/run.shrenamed

Only the mode changed.

test/basic004/expected → test/basic004/expected.outrenamed

The content is the same.

test/basic004/run → test/basic004/run.shrenamed

Only the mode changed.

test/basic005/expected → test/basic005/expected.outrenamed

The content is the same.

test/basic005/run → test/basic005/run.shrenamed

Only the mode changed.

test/basic006/expected → test/basic006/expected.outrenamed

The content is the same.

test/basic006/run → test/basic006/run.shrenamed

Only the mode changed.

test/basic007/expected → test/basic007/expected.outrenamed

The content is the same.

test/basic007/run → test/basic007/run.shrenamed

Only the mode changed.

test/basic008/expected → test/basic008/expected.outrenamed

The content is the same.

test/basic008/run → test/basic008/run.shrenamed

Only the mode changed.

test/basic009/expected → test/basic009/expected.outrenamed

The content is the same.

test/basic009/run → test/basic009/run.shrenamed

Only the mode changed.

test/basic010/expected → test/basic010/expected.outrenamed

The content is the same.

test/basic010/run → test/basic010/run.shrenamed

Only the mode changed.

test/basic011/expected → test/basic011/expected.outrenamed

The content is the same.

test/basic011/run → test/basic011/run.shrenamed

Only the mode changed.

test/basic012/expected → test/basic012/expected.outrenamed

The content is the same.

test/basic012/run → test/basic012/run.shrenamed

Only the mode changed.

test/basic013/expected → test/basic013/expected.outrenamed

The content is the same.

test/basic013/run → test/basic013/run.shrenamed

Only the mode changed.

test/basic014/expected → test/basic014/expected.outrenamed

The content is the same.

test/basic014/run → test/basic014/run.shrenamed

Only the mode changed.

test/basic015/expected → test/basic015/expected.outrenamed

The content is the same.

test/basic015/run → test/basic015/run.shrenamed

Only the mode changed.

test/basic016/expected → test/basic016/expected.outrenamed

The content is the same.

test/basic016/run → test/basic016/run.shrenamed

Only the mode changed.

test/basic017/expected → test/basic017/expected.outrenamed

The content is the same.

test/basic017/run → test/basic017/run.shrenamed

Only the mode changed.

test/basic018/expected → test/basic018/expected.outrenamed

The content is the same.

test/basic018/run → test/basic018/run.shrenamed

Only the mode changed.

test/basic019/expected → test/basic019/expected.outrenamed

The content is the same.

test/basic019/run → test/basic019/run.shrenamed

Only the mode changed.

test/basic020/expected → test/basic020/expected.outrenamed

The content is the same.

test/basic020/run → test/basic020/run.shrenamed

Only the mode changed.

test/basic021/expected → test/basic021/expected.outrenamed

The content is the same.

test/basic021/run → test/basic021/run.shrenamed

Only the mode changed.

test/basic022/expected → test/basic022/expected.outrenamed

The content is the same.

test/basic022/run → test/basic022/run.shrenamed

Only the mode changed.

test/basic023/expected → test/basic023/expected.outrenamed

The content is the same.

test/basic023/run → test/basic023/run.shrenamed

Only the mode changed.

test/basic024/expected → test/basic024/expected.outrenamed

The content is the same.

test/basic024/input → test/basic024/input.inrenamed

The content is the same.

test/basic024/run → test/basic024/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2

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

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

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

5

6./basic024

test/basic025/expected → test/basic025/expected.outrenamed

The content is the same.

test/basic025/input → test/basic025/input.inrenamed

The content is the same.

test/basic025/run → test/basic025/run.shrenamed+2−2

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

1#!/usr/bin/env bash

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

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

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

4

5−./basic025 input

5+./basic025 input.in

6

7rm -f basic025 *.ibc

test/basic026/expected → test/basic026/expected.outrenamed

The content is the same.

test/basic026/run → test/basic026/run.shrenamed

The content is the same.

test/bignum001/expected → test/bignum001/expected.outrenamed

The content is the same.

test/bignum001/run → test/bignum001/run.shrenamed

Only the mode changed.

test/bignum002/expected → test/bignum002/expected.outrenamed

The content is the same.

test/bignum002/run → test/bignum002/run.shrenamed

Only the mode changed.

test/bignum003/expected → test/bignum003/expected.outrenamed

The content is the same.

test/bignum003/run → test/bignum003/run.shrenamed

Only the mode changed.

test/bounded001/expected → test/bounded001/expected.outrenamed

The content is the same.

test/bounded001/run → test/bounded001/run.shrenamed

Only the mode changed.

test/buffer001/expected → test/buffer001/expected.outrenamed

The content is the same.

test/buffer001/run → test/buffer001/run.shrenamed

Only the mode changed.

test/buffer002/expected → test/buffer002/expected.outrenamed

The content is the same.

test/buffer002/run → test/buffer002/run.shrenamed

Only the mode changed.

test/contrib001/expected → test/contrib001/expected.outrenamed

The content is the same.

test/contrib001/run → test/contrib001/run.shrenamed

Only the mode changed.

test/corecords001/expected → test/corecords001/expected.outrenamed

The content is the same.

test/corecords001/run → test/corecords001/run.shrenamed

Only the mode changed.

test/corecords002/expected → test/corecords002/expected.outrenamed

The content is the same.

test/corecords002/run → test/corecords002/run.shrenamed

Only the mode changed.

test/delab001/expected → test/delab001/expected.outrenamed

The content is the same.

test/delab001/input → test/delab001/input.inrenamed

The content is the same.

test/delab001/run → test/delab001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/directives001/expected → test/directives001/expected.outrenamed

The content is the same.

test/directives001/run → test/directives001/run.shrenamed

Only the mode changed.

test/directives002/expected → test/directives002/expected.outrenamed

The content is the same.

test/directives002/run → test/directives002/run.shrenamed

The content is the same.

test/directives003/expected → test/directives003/expected.outrenamed

The content is the same.

test/directives003/run → test/directives003/run.shrenamed

Only the mode changed.

test/disambig002/expected → test/disambig002/expected.outrenamed

The content is the same.

test/disambig002/run → test/disambig002/run.shrenamed

Only the mode changed.

test/docs001/expected → test/docs001/expected.outrenamed

The content is the same.

test/docs001/input → test/docs001/input.inrenamed

The content is the same.

test/docs001/run → test/docs001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs002/expected → test/docs002/expected.outrenamed

The content is the same.

test/docs002/input → test/docs002/input.inrenamed

The content is the same.

test/docs002/run → test/docs002/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs003/expected → test/docs003/expected.outrenamed

The content is the same.

test/docs003/input → test/docs003/input.inrenamed

The content is the same.

test/docs003/run → test/docs003/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs004/expected → test/docs004/expected.outrenamed

The content is the same.

test/docs004/input → test/docs004/input.inrenamed

The content is the same.

test/docs004/run → test/docs004/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs005/expected → test/docs005/expected.outrenamed

The content is the same.

test/docs005/input → test/docs005/input.inrenamed

The content is the same.

test/docs005/run → test/docs005/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/docs006/expected → test/docs006/expected.outrenamed

The content is the same.

test/docs006/input → test/docs006/input.inrenamed

The content is the same.

test/docs006/run → test/docs006/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm *.ibc

test/dsl001/expected → test/dsl001/expected.outrenamed

The content is the same.

test/dsl001/input → test/dsl001/input.inrenamed

The content is the same.

test/dsl001/run → test/dsl001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ test001.idr -o test001 --partial-eval

3./test001

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

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

5rm -f test001 test001.ibc

test/dsl002/expected → test/dsl002/expected.outrenamed

The content is the same.

test/dsl002/run → test/dsl002/run.shrenamed

Only the mode changed.

test/dsl002/test → test/dsl002/test.inrenamed

The content is the same.

test/dsl002/test014.idr+1−1

@@ -64,6 +64,6 @@ readH fn = res (do let x = open fn Reading

64 else rputStrLn "Error")

65

66main : IO ()

67−main = run (readH "test")

67+main = run (readH "test.in")

68

69

test/dsl003/expected → test/dsl003/expected.outrenamed

The content is the same.

test/dsl003/run → test/dsl003/run.shrenamed

Only the mode changed.

test/dsl004/expected → test/dsl004/expected.outrenamed

The content is the same.

test/dsl004/run → test/dsl004/run.shrenamed

Only the mode changed.

test/effects001/expected → test/effects001/expected.outrenamed

The content is the same.

test/effects001/run → test/effects001/run.shrenamed

Only the mode changed.

test/effects001/test021.idr+1−1

@@ -31,7 +31,7 @@ readFileCount = readAcc []

31

32testFile : TestFileIO () ()

33testFile = do

34− Success <- open "testFile" Read

34+ Success <- open "testFile.in" Read

35 | (FError err) => do

36 putStrLn "Error!"

37 pure ()

test/effects001/testFile → test/effects001/testFile.inrenamed

The content is the same.

test/effects002/expected → test/effects002/expected.outrenamed

The content is the same.

test/effects002/run → test/effects002/run.shrenamed

Only the mode changed.

test/effects003/expected → test/effects003/expected.outrenamed

The content is the same.

test/effects003/input → test/effects003/input.inrenamed

The content is the same.

test/effects003/run → test/effects003/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

3−./hangman < input

3+./hangman < input.in

4rm -f hangman *.ibc

test/effects004/expected → test/effects004/expected.outrenamed

The content is the same.

test/effects004/input → test/effects004/input.inrenamed

The content is the same.

test/effects004/run → test/effects004/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ effects004.idr -o effects004 -p effects

3−./effects004 < input

3+./effects004 < input.in

4rm -f effects004 *.ibc

test/effects005/expected → test/effects005/expected.outrenamed

The content is the same.

test/effects005/run → test/effects005/run.shrenamed

Only the mode changed.

test/error001/expected → test/error001/expected.outrenamed

The content is the same.

test/error001/run → test/error001/run.shrenamed

Only the mode changed.

test/error002/expected → test/error002/expected.outrenamed

The content is the same.

test/error002/run → test/error002/run.shrenamed

Only the mode changed.

test/error003/expected → test/error003/expected.outrenamed

The content is the same.

test/error003/run → test/error003/run.shrenamed

Only the mode changed.

test/error004/expected → test/error004/expected.outrenamed

The content is the same.

test/error004/run → test/error004/run.shrenamed

Only the mode changed.

test/error005/expected → test/error005/expected.outrenamed

The content is the same.

test/error005/run → test/error005/run.shrenamed

Only the mode changed.

test/error006/expected → test/error006/expected.outrenamed

The content is the same.

test/error006/run → test/error006/run.shrenamed

Only the mode changed.

test/error007/expected → test/error007/expected.outrenamed

The content is the same.

test/error007/run → test/error007/run.shrenamed

Only the mode changed.

test/error008/expected → test/error008/expected.outrenamed

The content is the same.

test/error008/run → test/error008/run.shrenamed

Only the mode changed.

test/error009/expected → test/error009/expected.outrenamed

The content is the same.

test/error009/run → test/error009/run.shrenamed

Only the mode changed.

test/ffi001/expected → test/ffi001/expected.outrenamed

The content is the same.

test/ffi001/run → test/ffi001/run.shrenamed

Only the mode changed.

test/ffi002/expected → test/ffi002/expected.outrenamed

The content is the same.

test/ffi002/run → test/ffi002/run.shrenamed

Only the mode changed.

test/ffi003/expected → test/ffi003/expected.outrenamed

The content is the same.

test/ffi003/input → test/ffi003/input.inrenamed

The content is the same.

test/ffi003/run → test/ffi003/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour test024.idr --exec main < input.in

3rm -f *.ibc

test/ffi004/expected → test/ffi004/expected.outrenamed

The content is the same.

test/ffi004/run → test/ffi004/run.shrenamed

Only the mode changed.

test/ffi005/expected → test/ffi005/expected.outrenamed

The content is the same.

test/ffi005/run → test/ffi005/run.shrenamed

Only the mode changed.

test/ffi006/expected → test/ffi006/expected.outrenamed

The content is the same.

test/ffi006/run → test/ffi006/run.shrenamed

Only the mode changed.

test/ffi007/expected → test/ffi007/expected.outrenamed

The content is the same.

test/ffi007/run → test/ffi007/run.shrenamed

The content is the same.

test/ffi008/expected → test/ffi008/expected.outrenamed

The content is the same.

test/ffi008/run → test/ffi008/run.shrenamed

The content is the same.

test/ffi009/expected → test/ffi009/expected.outrenamed

The content is the same.

test/ffi009/run → test/ffi009/run.shrenamed

Only the mode changed.

test/ffi010/expected → test/ffi010/expected.outrenamed

The content is the same.

test/ffi010/run → test/ffi010/run.shrenamed

Only the mode changed.

test/ffi011/expected → test/ffi011/expected.outrenamed

The content is the same.

test/ffi011/ffi011 → test/ffi011/ffi011.jsrenamed

The content is the same.

test/ffi011/run → test/ffi011/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ ffi011.idr --interface -o lib.js

3−node ./ffi011

3+node ./ffi011.js

4rm -f *.ibc lib.js

test/ffi012/expected → test/ffi012/expected.outrenamed

The content is the same.

test/ffi012/ffi012 → test/ffi012/ffi012.jsrenamed

The content is the same.

test/ffi012/run → test/ffi012/run.shrenamed

Only the mode changed.

test/ffi013/expected → test/ffi013/expected.outrenamed

The content is the same.

test/ffi013/run → test/ffi013/run.shrenamed

Only the mode changed.

test/folding001/expected → test/folding001/expected.outrenamed

The content is the same.

test/folding001/run → test/folding001/run.shrenamed

Only the mode changed.

test/idrisdoc001/expected → test/idrisdoc001/expected.outrenamed

The content is the same.

test/idrisdoc001/run → test/idrisdoc001/run.shrenamed

Only the mode changed.

test/idrisdoc002/expected → test/idrisdoc002/expected.outrenamed

The content is the same.

test/idrisdoc002/run → test/idrisdoc002/run.shrenamed

Only the mode changed.

test/idrisdoc003/expected → test/idrisdoc003/expected.outrenamed

The content is the same.

test/idrisdoc003/run → test/idrisdoc003/run.shrenamed

Only the mode changed.

test/idrisdoc004/expected → test/idrisdoc004/expected.outrenamed

The content is the same.

test/idrisdoc004/run → test/idrisdoc004/run.shrenamed

Only the mode changed.

test/idrisdoc005/expected → test/idrisdoc005/expected.outrenamed

The content is the same.

test/idrisdoc005/run → test/idrisdoc005/run.shrenamed

Only the mode changed.

test/idrisdoc006/expected → test/idrisdoc006/expected.outrenamed

The content is the same.

test/idrisdoc006/run → test/idrisdoc006/run.shrenamed

Only the mode changed.

test/idrisdoc007/expected → test/idrisdoc007/expected.outrenamed

The content is the same.

test/idrisdoc007/run → test/idrisdoc007/run.shrenamed

Only the mode changed.

test/idrisdoc008/expected → test/idrisdoc008/expected.outrenamed

The content is the same.

test/idrisdoc008/run → test/idrisdoc008/run.shrenamed

Only the mode changed.

test/idrisdoc009/expected → test/idrisdoc009/expected.outrenamed

The content is the same.

test/idrisdoc009/input → test/idrisdoc009/input.inrenamed

The content is the same.

test/idrisdoc009/run → test/idrisdoc009/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

2+${IDRIS:-idris} $@ --nocolour --quiet --port none Test.idr < input.in

3rm -f *.ibc

test/interactive001/expected → test/interactive001/expected.outrenamed

The content is the same.

test/interactive001/input → test/interactive001/input.inrenamed

The content is the same.

test/interactive001/run → test/interactive001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2

3−${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input

3+${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input.in

4

5rm -f *.ibc

test/interactive002/expected → test/interactive002/expected.outrenamed

The content is the same.

test/interactive002/input → test/interactive002/input.inrenamed

The content is the same.

test/interactive002/run → test/interactive002/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive003/expected → test/interactive003/expected.outrenamed

The content is the same.

test/interactive003/input → test/interactive003/input.inrenamed

The content is the same.

test/interactive003/run → test/interactive003/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive004/expected → test/interactive004/expected.outrenamed

The content is the same.

test/interactive004/input → test/interactive004/input.inrenamed

The content is the same.

test/interactive004/run → test/interactive004/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive005/expected → test/interactive005/expected.outrenamed

The content is the same.

test/interactive005/input → test/interactive005/input.inrenamed

The content is the same.

test/interactive005/run → test/interactive005/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input

2+${IDRIS:-idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input.in

3rm -f *.ibc

4rm -f hello.bytecode

5rm -f hello

test/interactive006/expected → test/interactive006/expected.outrenamed

The content is the same.

test/interactive006/input → test/interactive006/input.inrenamed

The content is the same.

test/interactive006/run → test/interactive006/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

2+${IDRIS:-idris} $@ --quiet --port none --port 5000 interactive006.idr < input.in

3rm -f *.ibc

test/interactive007/expected → test/interactive007/expected.outrenamed

The content is the same.

test/interactive007/input → test/interactive007/input.inrenamed

The content is the same.

test/interactive007/run → test/interactive007/run.shrenamed+1−1

@@ -1,2 +1,2 @@

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input | perl -pe 's-Data\\Z-Data/Z-g'

2+${IDRIS:-idris} $@ -p contrib --nobanner --nocolor --port none < input.in | perl -pe 's-Data\\Z-Data/Z-g'

test/interactive008/expected → test/interactive008/expected.outrenamed

The content is the same.

test/interactive008/input → test/interactive008/input.inrenamed

The content is the same.

test/interactive008/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nobanner --nocolor --port none < input

test/interactive008/run.shnew file+2

@@ -0,0 +1,2 @@

1+#!/usr/bin/env bash

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

test/interactive009/expected → test/interactive009/expected.outrenamed

The content is the same.

test/interactive009/input → test/interactive009/input.inrenamed

The content is the same.

test/interactive009/run → test/interactive009/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive010/expected → test/interactive010/expected.outrenamed

The content is the same.

test/interactive010/input → test/interactive010/input.inrenamed

The content is the same.

test/interactive010/run → test/interactive010/run.shrenamed+1−1

@@ -1,2 +1,2 @@

1#!/usr/bin/env bash

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

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

test/interactive011/expected → test/interactive011/expected.outrenamed

The content is the same.

test/interactive011/input → test/interactive011/input.inrenamed

The content is the same.

test/interactive011/run → test/interactive011/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2

3cd src

4−${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input

4+${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input.in

5

6rm -f *.ibc

test/interactive012/expected → test/interactive012/expected.outrenamed

The content is the same.

test/interactive012/input → test/interactive012/input.inrenamed

The content is the same.

test/interactive012/run → test/interactive012/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input.in

3rm -f *.ibc

test/interactive013/expected → test/interactive013/expected.outrenamed

The content is the same.

test/interactive013/input → test/interactive013/input.inrenamed

The content is the same.

test/interactive013/run → test/interactive013/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive014/expected → test/interactive014/expected.outrenamed

The content is the same.

test/interactive014/input → test/interactive014/input.inrenamed

The content is the same.

test/interactive014/run → test/interactive014/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

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

3rm -f *.ibc

test/interactive015/expected → test/interactive015/expected.outrenamed

The content is the same.

test/interactive015/input → test/interactive015/input.inrenamed

The content is the same.

test/interactive015/run → test/interactive015/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2

3cp src/interactive015.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input.in

5

6cat interactive015.idr

7

test/interactive016/expected → test/interactive016/expected.outrenamed

The content is the same.

test/interactive016/input → test/interactive016/input.inrenamed

The content is the same.

test/interactive016/run → test/interactive016/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2

3cp src/interactive016.idr .

4−${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input.in

5

6cat interactive016.idr

7

test/interactive017/expected → test/interactive017/expected.outrenamed

The content is the same.

test/interactive017/run → test/interactive017/run.shrenamed

Only the mode changed.

test/interactive018/expected → test/interactive018/expected.outrenamed

The content is the same.

test/interactive018/input → test/interactive018/input.inrenamed

The content is the same.

test/interactive018/rundeleted−3

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

1−#!/usr/bin/env bash

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

3−rm -f *.ibc

test/interactive018/run.shnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc

test/interfaces001/expected → test/interfaces001/expected.outrenamed

The content is the same.

test/interfaces001/input → test/interfaces001/input.inrenamed

The content is the same.

test/interfaces001/run → test/interfaces001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour --consolewidth 70 InterfaceName.idr < input.in

3rm -f *.ibc

test/interfaces002/expected → test/interfaces002/expected.outrenamed

The content is the same.

test/interfaces002/run → test/interfaces002/run.shrenamed

Only the mode changed.

test/interfaces003/expected → test/interfaces003/expected.outrenamed

The content is the same.

test/interfaces003/run → test/interfaces003/run.shrenamed

Only the mode changed.

test/interfaces004/expected → test/interfaces004/expected.outrenamed

The content is the same.

test/interfaces004/run → test/interfaces004/run.shrenamed

Only the mode changed.

test/interfaces005/expected → test/interfaces005/expected.outrenamed

The content is the same.

test/interfaces005/run → test/interfaces005/run.shrenamed

Only the mode changed.

test/interfaces006/expected → test/interfaces006/expected.outrenamed

The content is the same.

test/interfaces006/run → test/interfaces006/run.shrenamed

Only the mode changed.

test/interfaces007/expected → test/interfaces007/expected.outrenamed

The content is the same.

test/interfaces007/run → test/interfaces007/run.shrenamed

Only the mode changed.

test/interfaces008/expected → test/interfaces008/expected.outrenamed

The content is the same.

test/interfaces008/run → test/interfaces008/run.shrenamed

Only the mode changed.

test/interfaces009/expected → test/interfaces009/expected.outrenamed

The content is the same.

test/interfaces009/run → test/interfaces009/run.shrenamed

Only the mode changed.

test/interfaces010/expected → test/interfaces010/expected.outrenamed

The content is the same.

test/interfaces010/run → test/interfaces010/run.shrenamed

Only the mode changed.

test/interpret001/expected → test/interpret001/expected.outrenamed

The content is the same.

test/interpret001/input → test/interpret001/input.inrenamed

The content is the same.

test/interpret001/run → test/interpret001/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour double-echo.idr < input.in

3rm -f *.ibc

test/interpret002/expected → test/interpret002/expected.outrenamed

The content is the same.

test/interpret002/input → test/interpret002/input.inrenamed

The content is the same.

test/interpret002/run → test/interpret002/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input

2+${IDRIS:-idris} $@ --quiet --port none --nocolour file-error.idr < input.in

3rm -f *.ibc

test/interpret003/expected → test/interpret003/expected.outrenamed

The content is the same.

test/interpret003/input → test/interpret003/input.inrenamed

The content is the same.

test/interpret003/run → test/interpret003/run.shrenamed+1−1

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

1#!/usr/bin/env bash

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

2+${IDRIS:-idris} $@ --quiet --port none --nocolour interpret003.idr < input.in

3rm -f *.ibc

test/io001/expected → test/io001/expected.outrenamed

The content is the same.

test/io001/run → test/io001/run.shrenamed

Only the mode changed.

test/io002/expected → test/io002/expected.outrenamed

The content is the same.

test/io002/run → test/io002/run.shrenamed

Only the mode changed.

test/io003/expected → test/io003/expected.outrenamed

The content is the same.

test/io003/run → test/io003/run.shrenamed

Only the mode changed.

test/layout001/expected → test/layout001/expected.outrenamed

The content is the same.

test/layout001/run → test/layout001/run.shrenamed

Only the mode changed.

test/literate001/expected → test/literate001/expected.outrenamed

The content is the same.

test/literate001/run → test/literate001/run.shrenamed

Only the mode changed.

test/meta001/expected → test/meta001/expected.outrenamed

The content is the same.

test/meta001/run → test/meta001/run.shrenamed

Only the mode changed.

test/meta002/expected → test/meta002/expected.outrenamed

The content is the same.

test/meta002/run → test/meta002/run.shrenamed

Only the mode changed.

test/meta003/expected → test/meta003/expected.outrenamed

The content is the same.

test/meta003/run → test/meta003/run.shrenamed

Only the mode changed.

test/meta004/expected → test/meta004/expected.outrenamed

The content is the same.

test/meta004/run → test/meta004/run.shrenamed

Only the mode changed.

test/pkg001/expected → test/pkg001/expected.outrenamed

The content is the same.

test/pkg001/run → test/pkg001/run.shrenamed

Only the mode changed.

test/pkg002/expected → test/pkg002/expected.outrenamed

The content is the same.

test/pkg002/run → test/pkg002/run.shrenamed

Only the mode changed.

test/pkg003/expected → test/pkg003/expected.outrenamed

The content is the same.

test/pkg003/run → test/pkg003/run.shrenamed

Only the mode changed.

test/pkg004/expected → test/pkg004/expected.outrenamed

The content is the same.

test/pkg004/run → test/pkg004/run.shrenamed

Only the mode changed.

test/pkg005/expected → test/pkg005/expected.outrenamed

The content is the same.

test/pkg005/run → test/pkg005/run.shrenamed

Only the mode changed.

test/pkg006/expected → test/pkg006/expected.outrenamed

The content is the same.

test/pkg006/run → test/pkg006/run.shrenamed

Only the mode changed.

test/pkg007/expected → test/pkg007/expected.outrenamed

The content is the same.

test/pkg007/input → test/pkg007/input.inrenamed

The content is the same.

test/pkg007/run → test/pkg007/run.shrenamed+1−1

@@ -2,6 +2,6 @@

2cd toy

3${IDRIS:-idris} $@ --build toy.ipkg --ibcsubdir ../ibcout

4cd ../ibcout

5−${IDRIS:-idris} $@ --quiet < ../input

5+${IDRIS:-idris} $@ --quiet < ../input.in

6cd ..

7rm -rf ibcout

test/pkg008/expected → test/pkg008/expected.outrenamed

The content is the same.

test/pkg008/run → test/pkg008/run.shrenamed

Only the mode changed.

test/pkg009/expected → test/pkg009/expected.outrenamed

The content is the same.

test/pkg009/run → test/pkg009/run.shrenamed

Only the mode changed.

test/pkg010/expecteddeleted−31

@@ -1,31 +0,0 @@

1−Uncaught error: user error (wrongopts.ipkg:4:1:

2− |

3−4 | <empty line>

4− | ^

5−Invalid option `-total'

6−

8− [--client ARG] | [--log LEVEL] | [--logging-categories CATS] |

9− [--nobasepkgs] | [--noprelude] | [--nobuiltins] | [--check] |

11− [--partial] | [--warnpartial] | [--warnreach] | [--warnipkg] |

12− [--nocoverage] | [--errorcontext] | [--info] | [--listlogcats] |

14− | [--V1] | [-V|--V0|--verbose] | [--ibcsubdir FILE] |

15− [-i|--idrispath ARG] | [--sourcepath ARG] | [--warn] |

17− [--repl IPKG] | [--clean IPKG] | [--mkdoc IPKG] | [--installdoc IPKG] |

18− [--checkpkg IPKG] | [--testpkg IPKG] | [--indent-with INDENT] |

19− [--indent-clause INDENT] | [--bytecode ARG] | [-S|--codegenonly] |

20− [-c|--compileonly] | [--dumpdefuns ARG] | [--dumpcases ARG] |

21− [--codegen TARGET] | [--portable-codegen TARGET] | [--cg-opt ARG] |

23− [--O3] | [--O2] | [--O1] | [--O0] | [--partial-eval] |

24− [--no-partial-eval] |

25− [--optimise-nat-like-types|--optimize-nat-like-types] |

26− [--no-optimise-nat-like-types|--no-optimize-nat-like-types] |

29− [--no-tactic-deprecation-warnings] |

30− [--allow-capitalized-pattern-variables]) [FILES] [-v|--version]

31−)

test/pkg010/expected.outnew file+29

@@ -0,0 +1,29 @@

1+Uncaught error: user error (wrongopts.ipkg:4:1:

2+ |

3+4 | <empty line>

4+ | ^

5+Invalid option `-total'

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 → test/pkg010/run.shrenamed

Only the mode changed.

test/prelude001/expected → test/prelude001/expected.outrenamed

The content is the same.

test/prelude001/run → test/prelude001/run.shrenamed

Only the mode changed.

test/primitives001/expected → test/primitives001/expected.outrenamed

The content is the same.

test/primitives001/input → test/primitives001/input.inrenamed

The content is the same.

test/primitives001/run → test/primitives001/run.shrenamed+1−1

@@ -2,5 +2,5 @@

2${IDRIS:-idris} $@ test005.idr -o test005

3./test005

4${IDRIS:-idris} $@ substring.idr -o substring

5−./substring < input

5+./substring < input.in

6rm -f test005 substring *.ibc

test/primitives002/expected → test/primitives002/expected.outrenamed

The content is the same.

test/primitives002/run → test/primitives002/run.shrenamed

Only the mode changed.

test/primitives003/expected → test/primitives003/expected.outrenamed

The content is the same.

test/primitives003/run → test/primitives003/run.shrenamed

Only the mode changed.

test/primitives004-disabled/expected → test/primitives004-disabled/expected.outrenamed

The content is the same.

test/primitives004-disabled/run → test/primitives004-disabled/run.shrenamed

Only the mode changed.

test/primitives005/expected → test/primitives005/expected.outrenamed

The content is the same.

test/primitives005/run → test/primitives005/run.shrenamed

The content is the same.

test/primitives006/expected → test/primitives006/expected.outrenamed

The content is the same.

test/primitives006/run → test/primitives006/run.shrenamed

Only the mode changed.

test/proof001/expected → test/proof001/expected.outrenamed

The content is the same.

test/proof001/run → test/proof001/run.shrenamed

Only the mode changed.

test/proof002/expected → test/proof002/expected.outrenamed

The content is the same.

test/proof002/run → test/proof002/run.shrenamed

Only the mode changed.

test/proof003/expected → test/proof003/expected.outrenamed

The content is the same.

test/proof003/run → test/proof003/run.shrenamed

Only the mode changed.

test/proof004/expected → test/proof004/expected.outrenamed

The content is the same.

test/proof004/run → test/proof004/run.shrenamed

Only the mode changed.

test/proof005/expected → test/proof005/expected.outrenamed

The content is the same.

test/proof005/run → test/proof005/run.shrenamed

Only the mode changed.

test/proof006/expected → test/proof006/expected.outrenamed

The content is the same.

test/proof006/run → test/proof006/run.shrenamed

Only the mode changed.

test/proof007/expected → test/proof007/expected.outrenamed

The content is the same.

test/proof007/run → test/proof007/run.shrenamed

Only the mode changed.

test/proof008/expected → test/proof008/expected.outrenamed

The content is the same.

test/proof008/run → test/proof008/run.shrenamed

Only the mode changed.

test/proof009/expected → test/proof009/expected.outrenamed

The content is the same.

test/proof009/input → test/proof009/input.inrenamed

The content is the same.

test/proof009/run → test/proof009/run.shrenamed+1−1

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

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input

2+${IDRIS:-idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input.in

3rm -f *.ibc

test/proof010/expected → test/proof010/expected.outrenamed

The content is the same.

test/proof010/run → test/proof010/run.shrenamed

Only the mode changed.

test/proof011/expected → test/proof011/expected.outrenamed

The content is the same.

test/proof011/run → test/proof011/run.shrenamed

Only the mode changed.

test/proofsearch001/expected → test/proofsearch001/expected.outrenamed

The content is the same.

test/proofsearch001/run → test/proofsearch001/run.shrenamed

Only the mode changed.

test/proofsearch002/expected → test/proofsearch002/expected.outrenamed

The content is the same.

test/proofsearch002/run → test/proofsearch002/run.shrenamed

Only the mode changed.

test/proofsearch003/expected → test/proofsearch003/expected.outrenamed

The content is the same.

test/proofsearch003/run → test/proofsearch003/run.shrenamed

Only the mode changed.

test/pruviloj001/expected → test/pruviloj001/expected.outrenamed

The content is the same.

test/pruviloj001/run → test/pruviloj001/run.shrenamed

Only the mode changed.

test/quasiquote001/expected → test/quasiquote001/expected.outrenamed

The content is the same.

test/quasiquote001/run → test/quasiquote001/run.shrenamed

Only the mode changed.

test/quasiquote002/expected → test/quasiquote002/expected.outrenamed

The content is the same.

test/quasiquote002/run → test/quasiquote002/run.shrenamed

Only the mode changed.

test/quasiquote003/expected → test/quasiquote003/expected.outrenamed

The content is the same.

test/quasiquote003/run → test/quasiquote003/run.shrenamed

Only the mode changed.

test/quasiquote004/expected → test/quasiquote004/expected.outrenamed

The content is the same.

test/quasiquote004/run → test/quasiquote004/run.shrenamed

Only the mode changed.

test/quasiquote005/expected → test/quasiquote005/expected.outrenamed

The content is the same.

test/quasiquote005/run → test/quasiquote005/run.shrenamed

Only the mode changed.

test/quasiquote006/expected → test/quasiquote006/expected.outrenamed

The content is the same.

test/quasiquote006/run → test/quasiquote006/run.shrenamed

Only the mode changed.

test/records001/expected → test/records001/expected.outrenamed

The content is the same.

test/records001/run → test/records001/run.shrenamed

Only the mode changed.

test/records002/expected → test/records002/expected.outrenamed

The content is the same.

test/records002/run → test/records002/run.shrenamed

Only the mode changed.

test/records003/expected → test/records003/expected.outrenamed

The content is the same.

test/records003/run → test/records003/run.shrenamed

Only the mode changed.

test/records004/expected → test/records004/expected.outrenamed

The content is the same.

test/records004/run → test/records004/run.shrenamed

Only the mode changed.

test/records005/expected → test/records005/expected.outrenamed

The content is the same.

test/records005/run → test/records005/run.shrenamed

Only the mode changed.

test/reg001/expected → test/reg001/expected.outrenamed

The content is the same.

test/reg001/run → test/reg001/run.shrenamed

Only the mode changed.

test/reg002/expected → test/reg002/expected.outrenamed

The content is the same.

test/reg002/run → test/reg002/run.shrenamed

Only the mode changed.

test/reg004/expected → test/reg004/expected.outrenamed

The content is the same.

test/reg004/run → test/reg004/run.shrenamed

Only the mode changed.

test/reg005/expected → test/reg005/expected.outrenamed

The content is the same.

test/reg005/run → test/reg005/run.shrenamed

Only the mode changed.

test/reg007/expected → test/reg007/expected.outrenamed

The content is the same.

test/reg007/run → test/reg007/run.shrenamed

Only the mode changed.

test/reg013/expected → test/reg013/expected.outrenamed

The content is the same.

test/reg013/run → test/reg013/run.shrenamed

Only the mode changed.

test/reg016/expected → test/reg016/expected.outrenamed

The content is the same.

test/reg016/run → test/reg016/run.shrenamed

Only the mode changed.

test/reg017/expected → test/reg017/expected.outrenamed

The content is the same.

test/reg017/run → test/reg017/run.shrenamed

Only the mode changed.

test/reg020/expected → test/reg020/expected.outrenamed

The content is the same.

test/reg020/run → test/reg020/run.shrenamed

Only the mode changed.

test/reg024/expected → test/reg024/expected.outrenamed

The content is the same.

test/reg024/run → test/reg024/run.shrenamed

Only the mode changed.

test/reg025/expected → test/reg025/expected.outrenamed

The content is the same.

test/reg025/run → test/reg025/run.shrenamed

Only the mode changed.

test/reg027/expected → test/reg027/expected.outrenamed

The content is the same.

test/reg027/run → test/reg027/run.shrenamed

Only the mode changed.

test/reg029/expected → test/reg029/expected.outrenamed

The content is the same.

test/reg029/run → test/reg029/run.shrenamed

Only the mode changed.

test/reg031/expected → test/reg031/expected.outrenamed

The content is the same.

test/reg031/run → test/reg031/run.shrenamed

Only the mode changed.

test/reg032/expected → test/reg032/expected.outrenamed

The content is the same.

test/reg032/run → test/reg032/run.shrenamed

Only the mode changed.

test/reg039/expected → test/reg039/expected.outrenamed

The content is the same.

test/reg039/run → test/reg039/run.shrenamed

Only the mode changed.

test/reg040/expected → test/reg040/expected.outrenamed

The content is the same.

test/reg040/run → test/reg040/run.shrenamed

Only the mode changed.

test/reg041/expected → test/reg041/expected.outrenamed

The content is the same.

test/reg041/run → test/reg041/run.shrenamed

Only the mode changed.

test/reg042/expected → test/reg042/expected.outrenamed

The content is the same.

test/reg042/run → test/reg042/run.shrenamed

Only the mode changed.

test/reg045/expected → test/reg045/expected.outrenamed

The content is the same.

test/reg045/run → test/reg045/run.shrenamed

Only the mode changed.

test/reg048/expected → test/reg048/expected.outrenamed

The content is the same.

test/reg048/run → test/reg048/run.shrenamed

Only the mode changed.

test/reg051-disabled/expected → test/reg051-disabled/expected.outrenamed

The content is the same.

test/reg051-disabled/run → test/reg051-disabled/run.shrenamed

Only the mode changed.

test/reg052/expected → test/reg052/expected.outrenamed

The content is the same.

test/reg052/run → test/reg052/run.shrenamed

Only the mode changed.

test/reg067/expected → test/reg067/expected.outrenamed

The content is the same.

test/reg067/run → test/reg067/run.shrenamed

Only the mode changed.

test/reg075/expected → test/reg075/expected.outrenamed

The content is the same.

test/reg075/input → test/reg075/input.inrenamed

The content is the same.

test/reg075/rundeleted−3

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

1−#!/usr/bin/env bash

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

3−rm -f *.ibc

test/reg075/run.shnew file+3

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

1+#!/usr/bin/env bash

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

3+rm -f *.ibc

test/reg076/expected → test/reg076/expected.outrenamed

The content is the same.

test/reg076/input → test/reg076/input.inrenamed

The content is the same.

test/reg076/run → test/reg076/run.shrenamed

Only the mode changed.

test/reg077/expected → test/reg077/expected.outrenamed

The content is the same.

test/reg077/run → test/reg077/run.shrenamed

Only the mode changed.

test/regression001/expected → test/regression001/expected.outrenamed

The content is the same.

test/regression001/run → test/regression001/run.shrenamed

Only the mode changed.

test/regression002/expected → test/regression002/expected.outrenamed

The content is the same.

test/regression002/run → test/regression002/run.shrenamed

Only the mode changed.

test/regression003/expected → test/regression003/expected.outrenamed

The content is the same.

test/regression003/run → test/regression003/run.shrenamed

Only the mode changed.

test/sourceLocation001/expected → test/sourceLocation001/expected.outrenamed

The content is the same.

test/sourceLocation001/run → test/sourceLocation001/run.shrenamed

Only the mode changed.

test/st001/expected → test/st001/expected.outrenamed

The content is the same.

test/st001/run → test/st001/run.shrenamed

Only the mode changed.

test/st001/test001.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

40

41testFile : (ConsoleIO m, File m) => ST m () []

42testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

44 | Left ferr => do putStrLn (show ferr)

45 pure ()

46 count <- new 0

test/st001/testFile → test/st001/testFile.inrenamed

The content is the same.

test/st002/expected → test/st002/expected.outrenamed

The content is the same.

test/st002/run → test/st002/run.shrenamed

Only the mode changed.

test/st002/test002.idr+1−1

@@ -40,7 +40,7 @@ readFileCount fh cnt =

40

41testFile : (ConsoleIO m, File m) => ST m () []

42testFile = with ST do

43− Right fileHandle <- open "testFile" Read

43+ Right fileHandle <- open "testFile.in" Read

44 | Left ferr => do putStrLn (show ferr)

45 pure ()

46 count <- new 0

test/st002/testFile → test/st002/testFile.inrenamed

The content is the same.

test/st003/expected → test/st003/expected.outrenamed

The content is the same.

test/st003/run → test/st003/run.shrenamed

Only the mode changed.

test/st003/test003.idr+1−1

@@ -7,7 +7,7 @@ import Control.ST.ImplicitCall

7

8testFile : (ConsoleIO m, File m) => ST m () []

9testFile = with ST do

10− Right str <- readFile "testFile"

10+ Right str <- readFile "testFile.in"

11 | Left ferr => do putStrLn (show ferr)

12 pure ()

13 putStrLn str

test/st003/testFile → test/st003/testFile.inrenamed

The content is the same.

test/st004/expected → test/st004/expected.outrenamed

The content is the same.

test/st004/run → test/st004/run.shrenamed

Only the mode changed.

test/st005/expected → test/st005/expected.outrenamed

The content is the same.

test/st005/run → test/st005/run.shrenamed

Only the mode changed.

test/st006/expected → test/st006/expected.outrenamed

The content is the same.

test/st006/run → test/st006/run.shrenamed

Only the mode changed.

test/st007/expected → test/st007/expected.outrenamed

The content is the same.

test/st007/run → test/st007/run.shrenamed

Only the mode changed.

test/sugar001/expected → test/sugar001/expected.outrenamed

The content is the same.

test/sugar001/run → test/sugar001/run.shrenamed

Only the mode changed.

test/sugar002/expected → test/sugar002/expected.outrenamed

The content is the same.

test/sugar002/run → test/sugar002/run.shrenamed

Only the mode changed.

test/sugar003/expected → test/sugar003/expected.outrenamed

The content is the same.

test/sugar003/run → test/sugar003/run.shrenamed

Only the mode changed.

test/sugar004/expected → test/sugar004/expected.outrenamed

The content is the same.

test/sugar004/run → test/sugar004/run.shrenamed

Only the mode changed.

test/sugar005/expected → test/sugar005/expected.outrenamed

The content is the same.

test/sugar005/run → test/sugar005/run.shrenamed

Only the mode changed.

test/syntax001/expected → test/syntax001/expected.outrenamed

The content is the same.

test/syntax001/run → test/syntax001/run.shrenamed

Only the mode changed.

test/syntax002/expected → test/syntax002/expected.outrenamed

The content is the same.

test/syntax002/run → test/syntax002/run.shrenamed

Only the mode changed.

test/tactics001/expected → test/tactics001/expected.outrenamed

The content is the same.

test/tactics001/run → test/tactics001/run.shrenamed

Only the mode changed.

test/totality001/expected → test/totality001/expected.outrenamed

The content is the same.

test/totality001/run → test/totality001/run.shrenamed

Only the mode changed.

test/totality002/expected → test/totality002/expected.outrenamed

The content is the same.

test/totality002/run → test/totality002/run.shrenamed

Only the mode changed.

test/totality003/expected → test/totality003/expected.outrenamed

The content is the same.

test/totality003/run → test/totality003/run.shrenamed

Only the mode changed.

test/totality004/expected → test/totality004/expected.outrenamed

The content is the same.

test/totality004/run → test/totality004/run.shrenamed

Only the mode changed.

test/totality005/expected → test/totality005/expected.outrenamed

The content is the same.

test/totality005/run → test/totality005/run.shrenamed

Only the mode changed.

test/totality006/expected → test/totality006/expected.outrenamed

The content is the same.

test/totality006/run → test/totality006/run.shrenamed

Only the mode changed.

test/totality007/expected → test/totality007/expected.outrenamed

The content is the same.

test/totality007/run → test/totality007/run.shrenamed

Only the mode changed.

test/totality008/expected → test/totality008/expected.outrenamed

The content is the same.

test/totality008/run → test/totality008/run.shrenamed

Only the mode changed.

test/totality009/expected → test/totality009/expected.outrenamed

The content is the same.

test/totality009/run → test/totality009/run.shrenamed

Only the mode changed.

test/totality010/expected → test/totality010/expected.outrenamed

The content is the same.

test/totality010/run → test/totality010/run.shrenamed

Only the mode changed.

test/totality011/expected → test/totality011/expected.outrenamed

The content is the same.

test/totality011/run → test/totality011/run.shrenamed

Only the mode changed.

test/totality012/expected → test/totality012/expected.outrenamed

The content is the same.

test/totality012/run → test/totality012/run.shrenamed

Only the mode changed.

test/totality013/expected → test/totality013/expected.outrenamed

The content is the same.

test/totality013/run → test/totality013/run.shrenamed

Only the mode changed.

test/totality014/expected → test/totality014/expected.outrenamed

The content is the same.

test/totality014/run → test/totality014/run.shrenamed

Only the mode changed.

test/totality015/expected → test/totality015/expected.outrenamed

The content is the same.

test/totality015/run → test/totality015/run.shrenamed

Only the mode changed.

test/totality016/expected → test/totality016/expected.outrenamed

The content is the same.

test/totality016/run → test/totality016/run.shrenamed

Only the mode changed.

test/totality017/expected → test/totality017/expected.outrenamed

The content is the same.

test/totality017/run → test/totality017/run.shrenamed

Only the mode changed.

test/totality018/expected → test/totality018/expected.outrenamed

The content is the same.

test/totality018/run → test/totality018/run.shrenamed

Only the mode changed.

test/totality019/expected → test/totality019/expected.outrenamed

The content is the same.

test/totality019/run → test/totality019/run.shrenamed

Only the mode changed.

test/totality020/expected → test/totality020/expected.outrenamed

The content is the same.

test/totality020/run → test/totality020/run.shrenamed

Only the mode changed.

test/totality021/expected → test/totality021/expected.outrenamed

The content is the same.

test/totality021/run → test/totality021/run.shrenamed

Only the mode changed.

test/totality022/expected → test/totality022/expected.outrenamed

The content is the same.

test/totality022/run → test/totality022/run.shrenamed

Only the mode changed.

test/totality023/expected → test/totality023/expected.outrenamed

The content is the same.

test/totality023/run → test/totality023/run.shrenamed

Only the mode changed.

test/totality024/expected → test/totality024/expected.outrenamed

The content is the same.

test/totality024/run → test/totality024/run.shrenamed

Only the mode changed.

test/totality025/expected → test/totality025/expected.outrenamed

The content is the same.

test/totality025/run → test/totality025/run.shrenamed

Only the mode changed.

test/totality026/expected → test/totality026/expected.outrenamed

The content is the same.

test/totality026/run → test/totality026/run.shrenamed

Only the mode changed.

test/tutorial001/expected → test/tutorial001/expected.outrenamed

The content is the same.

test/tutorial001/run → test/tutorial001/run.shrenamed

Only the mode changed.

test/tutorial002/expected → test/tutorial002/expected.outrenamed

The content is the same.

test/tutorial002/run → test/tutorial002/run.shrenamed

Only the mode changed.

test/tutorial003/expected → test/tutorial003/expected.outrenamed

The content is the same.

test/tutorial003/run → test/tutorial003/run.shrenamed

Only the mode changed.

test/tutorial004/expected → test/tutorial004/expected.outrenamed

The content is the same.

test/tutorial004/run → test/tutorial004/run.shrenamed

Only the mode changed.

test/tutorial005/expected → test/tutorial005/expected.outrenamed

The content is the same.

test/tutorial005/run → test/tutorial005/run.shrenamed

Only the mode changed.

test/tutorial006/expected → test/tutorial006/expected.outrenamed

The content is the same.

test/tutorial006/run → test/tutorial006/run.shrenamed

Only the mode changed.

test/tutorial007/expected → test/tutorial007/expected.outrenamed

The content is the same.

test/tutorial007/run → test/tutorial007/run.shrenamed

Only the mode changed.

test/unique001/expected → test/unique001/expected.outrenamed

The content is the same.

test/unique001/run → test/unique001/run.shrenamed

Only the mode changed.

test/unique004/expected → test/unique004/expected.outrenamed

The content is the same.

test/unique004/run → test/unique004/run.shrenamed

Only the mode changed.

test/universes001/expected → test/universes001/expected.outrenamed

The content is the same.

test/universes001/run → test/universes001/run.shrenamed

Only the mode changed.

test/universes002/expected → test/universes002/expected.outrenamed

The content is the same.

test/universes002/run → test/universes002/run.shrenamed

Only the mode changed.

test/views001/expected → test/views001/expected.outrenamed

The content is the same.

test/views001/run → test/views001/run.shrenamed

Only the mode changed.

test/views002/expected → test/views002/expected.outrenamed

The content is the same.

test/views002/run → test/views002/run.shrenamed

Only the mode changed.

test/views003/expected → test/views003/expected.outrenamed

The content is the same.

test/views003/run → test/views003/run.shrenamed

Only the mode changed.