f80809a...master · Idris-dev

.travis.yml+23−14

since splitsnapshots

unifiedsplit

@@ -8,7 +8,7 @@ env:

8

9matrix:

10 include:

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

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

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

14 compiler: ": #GHC 8.2.2"

@@ -19,18 +19,26 @@ matrix:

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

20 compiler: ": #GHC 8.2.2"

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

22− - env: CABALVER="3.0" GHCVER="8.8.2" IDRIS2=YES

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

23+ compiler: ": #GHC 8.4.4"

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

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

26+ compiler: ": #GHC 8.4.4"

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

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

29+ compiler: ": #GHC 8.4.4"

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

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

32+ compiler: ": #GHC 8.8.3"

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

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

35+ compiler: ": #GHC 8.8.3"

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

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

38+ compiler: ": #GHC 8.8.3"

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

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

23− addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.2], sources: [hvr-ghc]}}

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

24−

25−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="lib_doc doc"

26−# compiler: ": #GHC 8.8.1"

27−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

28−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_js"

29−# compiler: ": #GHC 8.8.1"

30−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

31−# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_c"

32−# compiler: ": #GHC 8.8.1"

33−# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}

34 fast-finish: true

42 fast-finish: true

35

43

36cache:

44cache:

@@ -119,7 +127,7 @@ install:

119 cp -a $HOME/.ghc $HOME/.cabsnap/ghc;

127 cp -a $HOME/.ghc $HOME/.cabsnap/ghc;

120 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/;

121 fi

129 fi

122−

130+

123

131

124before_script:

132before_script:

125 - ORIGINAL_DIR=$(pwd)

133 - ORIGINAL_DIR=$(pwd)

@@ -128,6 +136,7 @@ before_script:

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

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

129 - cd ${PKGNAME}*

137 - cd ${PKGNAME}*

130script:

138script:

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

131###

140###

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

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

133 - cabal v1-configure -f FFI -f CI --enable-tests

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

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.

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/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+31−15

@@ -46,12 +46,19 @@ Build-type: Custom

46

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

48

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

50+-- heavily discouraged.

49Data-files: idrisdoc/styles.css

51Data-files: idrisdoc/styles.css

50− jsrts/**/*.js

52+ jsrts/jsbn/*.js

53+ jsrts/*.js

51 jsrts/jsbn/LICENSE

54 jsrts/jsbn/LICENSE

52 rts/Makefile

55 rts/Makefile

53− rts/**/*.c

56+ rts/*.c

57+ rts/seL4/*.c

58+ rts/arduino/*.c

59+ rts/windows/*.c

54− rts/**/*.h

60+ rts/windows/*.h

61+ rts/*.h

55 rts/seL4/CMakeLists.txt

62 rts/seL4/CMakeLists.txt

56 rts/seL4/README.md

63 rts/seL4/README.md

57

64

@@ -64,8 +71,13 @@ Extra-doc-files:

64 RELEASE-CHECKS.md

71 RELEASE-CHECKS.md

65 idris-tutorial.pdf

72 idris-tutorial.pdf

66 man/idris.1

73 man/idris.1

67− samples/**/*.idr

74+ samples/effects/*.idr

75+ samples/misc/*.idr

76+ samples/tutorial/*.idr

77+ samples/ST/*.idr

78+ samples/ST/Graphics/*.idr

79+ samples/ST/Net/*.idr

68− samples/**/*.lidr

80+ samples/misc/*.lidr

69

81

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

71Extra-source-files:

83Extra-source-files:

@@ -73,15 +85,20 @@ Extra-source-files:

73 config.mk

85 config.mk

74 custom.mk-alldeps

86 custom.mk-alldeps

75 mkpkg.sh

87 mkpkg.sh

76− stack-alt.yaml

77 stack-shell.nix

88 stack-shell.nix

78 stack.yaml

89 stack.yaml

79 stylize.sh

90 stylize.sh

80 win-release.sh

91 win-release.sh

81−

92+

82 benchmarks/*.pl

93 benchmarks/*.pl

83− benchmarks/**/*.idr

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

84− benchmarks/**/*.ipkg

101+ benchmarks/trivial/*.ipkg

85 benchmarks/quasigroups/board

102 benchmarks/quasigroups/board

86

103

87 icons/*.png

104 icons/*.png

@@ -304,13 +321,13 @@ Library

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

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

305 , aeson >= 0.6 && < 1.5

322 , aeson >= 0.6 && < 1.5

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

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

307− , ansi-terminal < 0.10

324+ , ansi-terminal < 0.11

308 , ansi-wl-pprint < 0.7

325 , ansi-wl-pprint < 0.7

309 , array >= 0.4.0.1 && < 0.6

326 , array >= 0.4.0.1 && < 0.6

310 , base64-bytestring < 1.1

327 , base64-bytestring < 1.1

311 , binary >= 0.8.4.1 && < 0.9

328 , binary >= 0.8.4.1 && < 0.9

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

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

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

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

314 , bytestring < 0.11

331 , bytestring < 0.11

315 , cheapskate >= 0.1.1.2 && < 0.2

332 , cheapskate >= 0.1.1.2 && < 0.2

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

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

@@ -321,9 +338,9 @@ Library

321 , fingertree >= 0.1.4.1 && < 0.2

338 , fingertree >= 0.1.4.1 && < 0.2

322 , haskeline >= 0.7 && < 0.8

339 , haskeline >= 0.7 && < 0.8

323 , ieee754 >= 0.7 && < 0.9

340 , ieee754 >= 0.7 && < 0.9

324− , megaparsec >= 7.0.4 && < 8

341+ , megaparsec >= 7.0.4 && < 9

325 , mtl >= 2.1 && < 2.3

342 , mtl >= 2.1 && < 2.3

326− , network >= 2.7 && < 2.9

343+ , network >= 2.7 && < 3.1.2

327 , optparse-applicative >= 0.13 && < 0.16

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

328 , parser-combinators >= 1.0.0

345 , parser-combinators >= 1.0.0

329 , pretty < 1.2

346 , pretty < 1.2

@@ -341,7 +358,7 @@ Library

341 , vector < 0.13

358 , vector < 0.13

342 , vector-binary-instances < 0.3

359 , vector-binary-instances < 0.3

343 , zip-archive > 0.2.3.5 && < 0.5

360 , zip-archive > 0.2.3.5 && < 0.5

344− , fsnotify >= 0.2 && < 2.2

361+ , fsnotify >= 0.2 && < 0.4

345 , async < 2.3

362 , async < 2.3

346

363

347 if !impl(ghc >= 8.0)

364 if !impl(ghc >= 8.0)

@@ -459,4 +476,3 @@ Executable idris-codegen-node

459 Default-Language: Haskell2010

476 Default-Language: Haskell2010

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

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

461 ghc-options: -threaded -rtsopts -funbox-strict-fields

478 ghc-options: -threaded -rtsopts -funbox-strict-fields

462−

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/Parity.idr+123−69

@@ -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,42 +125,46 @@ 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.

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

85− evenEven {n = Z} _ = Refl

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

87

129

88− ||| Odds are odd.

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

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

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

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

132+oddSuccEven (haf ** pf) = (haf * 2 ** (pf, (haf ** Refl)))

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

92

133

93||| Even plus Even is Even.

134||| Even plus Even is Even.

94evenPlusEven : Even j -> Even k -> Even (j + k)

135evenPlusEven : Even j -> Even k -> Even (j + k)

95evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =

136evenPlusEven (half_j ** pf_j) (half_k ** pf_k) =

96− rewrite pf_j in

97− rewrite pf_k in

98− (half_j + half_k **

137+ (half_j + half_k **

138+ rewrite pf_j in

139+ rewrite pf_k in

99 sym $ multDistributesOverPlusLeft half_j half_k 2)

140 sym $ multDistributesOverPlusLeft half_j half_k 2)

100

141

101−||| Odd plus Odd is Even.

142+||| Odd plus Even is Odd.

102−oddPlusOdd : Odd j -> Odd k -> Even (j + k)

143+oddPlusEven : Odd j -> Even k -> Odd (j + k)

103−oddPlusOdd (haf_j ** pf_j) (haf_k ** pf_k) =

144+oddPlusEven oj ek =

104− rewrite pf_j in

145+ let

105− rewrite pf_k in

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

106− rewrite sym $ plusSuccRightSucc (haf_j * 2) (haf_k * 2) in

147+ (half_ik ** eik) = evenPlusEven ei ek

107− rewrite sym $ multDistributesOverPlusLeft haf_j haf_k 2 in

148+ in

108− (S (haf_j + haf_k) ** Refl)

149+ (half_ik **

150+ rewrite ipj in

151+ cong {f = S} eik)

109

152

110||| Even plus Odd is Odd.

153||| Even plus Odd is Odd.

111evenPlusOdd : Even j -> Odd k -> Odd (j + k)

154evenPlusOdd : Even j -> Odd k -> Odd (j + k)

112−evenPlusOdd (half_j ** pf_j) (haf_k ** pf_k) =

155+evenPlusOdd {j} {k} ej ok = rewrite plusCommutative j k in oddPlusEven ok ej

113− rewrite pf_j in

156+

114− rewrite pf_k in

157+||| Odd plus Odd is Even.

115− rewrite sym $ plusSuccRightSucc (half_j * 2) (haf_k * 2) in

158+oddPlusOdd : Odd j -> Odd k -> Even (j + k)

116− rewrite sym $ multDistributesOverPlusLeft half_j haf_k 2 in

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

117− (half_j + haf_k ** Refl)

167+ Refl)

118

168

119||| A helper fact.

169||| A helper fact.

120multShuffle : (a, b, c : Nat) ->

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

@@ -129,35 +179,39 @@ multShuffle a b c =

129||| Even times Even is Even.

179||| Even times Even is Even.

130evenMultEven : Even j -> Even k -> Even (j * k)

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

131evenMultEven (half_j ** pf_j) (half_k ** pf_k) =

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

132− rewrite pf_j in

133− rewrite pf_k in

134− (half_j * half_k * 2 **

182+ (half_j * half_k * 2 **

183+ rewrite pf_j in

184+ rewrite pf_k in

135 multShuffle half_j half_k 2)

185 multShuffle half_j half_k 2)

136

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+

137||| Even times Odd is Even.

201||| Even times Odd is Even.

138evenMultOdd : Even j -> Odd k -> Even (j * k)

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

139−evenMultOdd (half_j ** pf_j) (haf_k ** pf_k) =

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

140− let half = half_j * haf_k * 2 in

141− rewrite pf_j in

142− rewrite pf_k in

143− rewrite multRightSuccPlus (half_j * 2) (haf_k * 2) in

144− rewrite multShuffle half_j haf_k 2 in

145− (half_j + half **

146− sym $ multDistributesOverPlusLeft half_j half 2)

147

204

148||| Odd times Odd is Odd.

205||| Odd times Odd is Odd.

149oddMultOdd : Odd j -> Odd k -> Odd (j * k)

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

150−oddMultOdd (haf_j ** pf_j) (haf_k ** pf_k) =

207+oddMultOdd oj (haf_k ** pf_k) =

151 let

208 let

152− haf = haf_j * haf_k * 2

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

153− rem = haf_j + haf_k

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

154 in

211 in

155− rewrite pf_j in

212+ (haf_k + half_ik **

156− rewrite pf_k in

213+ rewrite multDistributesOverPlusLeft haf_k half_ik 2 in

157− rewrite multRightSuccPlus (haf_j * 2) (haf_k * 2) in

214+ rewrite ipj in

158− rewrite multShuffle haf_j haf_k 2 in

215+ rewrite eik in

159− rewrite plusAssociative (haf_k * 2) (haf_j * 2) (haf * 2) in

216+ rewrite pf_k in

160− rewrite sym $ multDistributesOverPlusLeft haf_k haf_j 2 in

161− rewrite plusCommutative haf_k haf_j in

162− rewrite sym $ multDistributesOverPlusLeft rem haf 2 in

163− (rem + haf ** Refl)

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_stdfgn.c+2−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 }

rts/idris_stdfgn.h+1−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);

src/Idris/Core/TT.hs+1−1

@@ -325,7 +325,7 @@ bindTC x k = case x of

325instance Monad TC where

326 return x = OK x

327 x >>= k = bindTC x k

328−#if !(MIN_VERSION_base(4,12,0))

328+#if !(MIN_VERSION_base(4,13,0))

329 fail = Fail.fail

330#endif

331

src/Idris/Parser/Stack.hs+14−1

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

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

77instance Message ParseError where

78 messageExtent err = sourcePositionFC pos

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

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

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

85+#endif

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

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

82 messageSource err = Just sline

87 messageSource err = Just sline

83 where

88 where

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

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

91+#else

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

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

93+#endif

85

94

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

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

87prettyError :: ParseError -> String

96prettyError :: ParseError -> String

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

89

98

90{- * Mark and restore -}

99{- * Mark and restore -}

91

100

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

102+type Mark = P.State String Void

103+#else

92type Mark = P.State String

104type Mark = P.State String

105+#endif

93

106

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

95mark :: 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−26

@@ -1,26 +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− - HsYAML-0.2.1.0@sha256:e4677daeba57f7a1e9a709a1f3022fe937336c91513e893166bd1f023f530d68,5311

14− - HsYAML-aeson-0.2.0.0@sha256:04796abfc01cffded83f37a10e6edba4f0c0a15d45bef44fc5bb4313d9c87757,1791

15−

16−flags:

17− idris:

18− FFI: true

19− GMP: true

20−

21−ghc-options:

22− idris: -fwarn-unused-imports -fwarn-unused-binds

23−

24−nix:

25− enable: false

26− shell-file: stack-shell.nix

@@ -0,0 +1 @@

1+stack-15.4.yaml