master..76c37e7 · Idris-dev

.travis.yml+14−23

since splitsnapshots

unifiedsplit

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

8

9matrix:

10 include:

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

11+ - env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="14.15" 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,26 +19,18 @@ 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="2.4" GHCVER="8.4.4" TESTS="lib_doc doc"

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

23− compiler: ": #GHC 8.4.4"

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

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

26− compiler: ": #GHC 8.4.4"

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

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

29− compiler: ": #GHC 8.4.4"

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

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

32− compiler: ": #GHC 8.8.3"

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

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

35− compiler: ": #GHC 8.8.3"

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

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

38− compiler: ": #GHC 8.8.3"

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

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

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

23+ addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.2], 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]}}

42 fast-finish: true

34 fast-finish: true

43

35

44cache:

36cache:

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

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

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

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

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

129 fi

121 fi

130−

122+

131

123

132before_script:

124before_script:

133 - ORIGINAL_DIR=$(pwd)

125 - ORIGINAL_DIR=$(pwd)

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

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

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

137 - cd ${PKGNAME}*

129 - cd ${PKGNAME}*

138script:

130script:

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

140###

131###

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

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

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

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

INSTALL.md+2−11

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

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

134−

135See the following GHC issue page for more information:

134See the following GHC issue page for more information:

136

135

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

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

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

142

141

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

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

144

143

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

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.

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+1−2

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

251# Additional stuff for the LaTeX preamble.

252'preamble': r'''

253\usepackage{lmodern}

254−\usepackage{textalpha}

255\usepackage[T1]{fontenc}

254\usepackage[T1]{fontenc}

256\usepackage[utf8x]{inputenc}

255\usepackage[utf8x]{inputenc}

257\usepackage{titlesec}

256\usepackage{titlesec}

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

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

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

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

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

303latex_documents = [

302latex_documents = [

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

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

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

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

306]

305]

307

306

docs/effects/introduction.rst+1−2

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

20+examples directory of the Idris repository.

21−is needed when starting Idris.

22

21

23Consider, for example, the following introductory function which

22Consider, for example, the following introductory function which

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

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

@@ -46,19 +46,12 @@ 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.

51Data-files: idrisdoc/styles.css

49Data-files: idrisdoc/styles.css

52− jsrts/jsbn/*.js

50+ jsrts/**/*.js

53− jsrts/*.js

54 jsrts/jsbn/LICENSE

51 jsrts/jsbn/LICENSE

55 rts/Makefile

52 rts/Makefile

56− rts/*.c

53+ rts/**/*.c

57− rts/seL4/*.c

54+ rts/**/*.h

58− rts/arduino/*.c

59− rts/windows/*.c

60− rts/windows/*.h

61− rts/*.h

62 rts/seL4/CMakeLists.txt

55 rts/seL4/CMakeLists.txt

63 rts/seL4/README.md

56 rts/seL4/README.md

64

57

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

71 RELEASE-CHECKS.md

64 RELEASE-CHECKS.md

72 idris-tutorial.pdf

65 idris-tutorial.pdf

73 man/idris.1

66 man/idris.1

74− samples/effects/*.idr

67+ samples/**/*.idr

75− samples/misc/*.idr

76− samples/tutorial/*.idr

68+ samples/**/*.lidr

77− samples/ST/*.idr

78− samples/ST/Graphics/*.idr

79− samples/ST/Net/*.idr

80− samples/misc/*.lidr

81

69

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

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

83Extra-source-files:

71Extra-source-files:

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

85 config.mk

73 config.mk

86 custom.mk-alldeps

74 custom.mk-alldeps

87 mkpkg.sh

75 mkpkg.sh

76+ stack-alt.yaml

88 stack-shell.nix

77 stack-shell.nix

89 stack.yaml

78 stack.yaml

90 stylize.sh

79 stylize.sh

91 win-release.sh

80 win-release.sh

92−

81+

93 benchmarks/*.pl

82 benchmarks/*.pl

94− benchmarks/fasta/*.idr

83+ benchmarks/**/*.idr

95− benchmarks/fasta/*.ipkg

84+ benchmarks/**/*.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

85 benchmarks/quasigroups/board

103

86

104 icons/*.png

87 icons/*.png

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

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

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

322 , aeson >= 0.6 && < 1.5

305 , aeson >= 0.6 && < 1.5

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

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

324− , ansi-terminal < 0.11

307+ , ansi-terminal < 0.10

325 , ansi-wl-pprint < 0.7

308 , ansi-wl-pprint < 0.7

326 , array >= 0.4.0.1 && < 0.6

309 , array >= 0.4.0.1 && < 0.6

327 , base64-bytestring < 1.1

310 , base64-bytestring < 1.1

328 , binary >= 0.8.4.1 && < 0.9

311 , binary >= 0.8.4.1 && < 0.9

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

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

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

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

331 , bytestring < 0.11

314 , bytestring < 0.11

332 , cheapskate >= 0.1.1.2 && < 0.2

315 , cheapskate >= 0.1.1.2 && < 0.2

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

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

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

338 , fingertree >= 0.1.4.1 && < 0.2

321 , fingertree >= 0.1.4.1 && < 0.2

339 , haskeline >= 0.7 && < 0.8

322 , haskeline >= 0.7 && < 0.8

340 , ieee754 >= 0.7 && < 0.9

323 , ieee754 >= 0.7 && < 0.9

341− , megaparsec >= 7.0.4 && < 9

324+ , megaparsec >= 7.0.4 && < 8

342 , mtl >= 2.1 && < 2.3

325 , mtl >= 2.1 && < 2.3

343− , network >= 2.7 && < 3.1.2

326+ , network >= 2.7 && < 2.9

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

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

345 , parser-combinators >= 1.0.0

328 , parser-combinators >= 1.0.0

346 , pretty < 1.2

329 , pretty < 1.2

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

358 , vector < 0.13

341 , vector < 0.13

359 , vector-binary-instances < 0.3

342 , vector-binary-instances < 0.3

360 , zip-archive > 0.2.3.5 && < 0.5

343 , zip-archive > 0.2.3.5 && < 0.5

361− , fsnotify >= 0.2 && < 0.4

344+ , fsnotify >= 0.2 && < 2.2

362 , async < 2.3

345 , async < 2.3

363

346

364 if !impl(ghc >= 8.0)

347 if !impl(ghc >= 8.0)

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

476 Default-Language: Haskell2010

459 Default-Language: Haskell2010

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

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

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

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

462+

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

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

22+isoRefl = MkIso id id (\x => Refl) (\x => 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 xto xfrom xtoFrom xfromTo where

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

28− xto : a -> c

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

29− xto = to' . to

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

30− xfrom : c -> a

31− xfrom = from . from'

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

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

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

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

31+ y QED)

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)

36

35

37Category Iso where

36Category Iso where

38 id = isoRefl

37 id = isoRefl

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

100

99

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

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

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

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

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

103−eitherCong (MkIso to from toFrom fromTo)

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

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

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

148+ ok (x, ()) = Refl

147

149

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

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

149pairUnitLeft : Iso ((), a) a

151pairUnitLeft : Iso ((), a) a

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

159

161

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

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

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

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

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

162−pairCong (MkIso to from toFrom fromTo)

165+ (MkIso to from toFrom fromTo)

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

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

164 MkIso to'' from'' iso1 iso2

167 MkIso to'' from'' iso1 iso2

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

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

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

202

205

203||| Products distribute over sums

206||| Products distribute over sums

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

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

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

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

206

209

207

210

208-- Enable preorder reasoning syntax over isomorphisms

211-- Enable preorder reasoning syntax over isomorphisms

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

219-- Isomorphisms over Maybe

222-- Isomorphisms over Maybe

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

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

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

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

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

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

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

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

224 ok1 Nothing = Refl

227 ok1 Nothing = Refl

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

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

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

250 () QED

253 () QED

251

254

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

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

253−eitherMaybeLeftMaybe =

256+eitherMaybeLeftMaybe {a} {b} =

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

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

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

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

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

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

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

260

263

261

264

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

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

263−eitherMaybeRightMaybe =

266+eitherMaybeRightMaybe {a} {b} =

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

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

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

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

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

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

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

285 fb (FS x) = Refl

288 fb (FS x) = Refl

286

289

287finZeroBot : Iso (Fin 0) Void

290finZeroBot : Iso (Fin 0) Void

288−finZeroBot = MkIso (void . uninhabited)

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

289− void

292+ (\x => void x)

290 (\x => void x)

293 (\x => void x)

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

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

292

295

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,13,0))

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

329 fail = Fail.fail

330#endif

331

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

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

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

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

9module Idris.Parser.Stack

10 ( -- * Parsing

11 Parser(..)

@@ -77,20 +77,11 @@ 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

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

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

85−#endif

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

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

87 messageSource err = Just sline

82 messageSource err = Just sline

88 where

83 where

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

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

91−#else

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

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

93−#endif

94

85

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

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

96prettyError :: ParseError -> String

87prettyError :: ParseError -> String

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

98

89

99{- * Mark and restore -}

90{- * Mark and restore -}

100

91

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

102−type Mark = P.State String Void

103−#else

104type Mark = P.State String

92type Mark = P.State String

105−#endif

106

93

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

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

108mark :: Parsing m => m Mark

95mark :: Parsing m => m Mark

stack-11.22.yamldeleted−21

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

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

2−resolver: lts-11.22

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−- megaparsec-7.0.5

7−- Cabal-2.4.1.0

8−- network-3.1.1.1

9−- parser-combinators-1.0.0

10−

11−flags:

12− idris:

13− FFI: true

14− GMP: true

15−

16−ghc-options:

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

18−

19−nix:

20− enable: false

21− shell-file: stack-shell.nix

stack-12.26.yamldeleted−20

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

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

2−resolver: lts-12.26

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−- megaparsec-7.0.5

7−- Cabal-2.4.1.0

8−- network-3.1.1.1

9−

10−flags:

11− idris:

12− FFI: true

13− GMP: true

14−

15−ghc-options:

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

17−

18−nix:

19− enable: false

20− shell-file: stack-shell.nix

stack-15.3.yamldeleted−17

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

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

2−resolver: lts-15.3

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−

7−flags:

8− idris:

9− FFI: true

10− GMP: true

11−

12−ghc-options:

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

14−

15−nix:

16− enable: false

17− shell-file: stack-shell.nix

stack-15.4.yamldeleted−17

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

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

2−resolver: lts-15.4

3−

4−extra-deps:

5−- cheapskate-0.1.1.2

6−

7−flags:

8− idris:

9− FFI: true

10− GMP: true

11−

12−ghc-options:

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

14−

15−nix:

16− enable: false

17− shell-file: stack-shell.nix

stack-alt.yamlnew file+25

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

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

2+resolver: lts-11.4

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

@@ -1 +0,0 @@

1−stack-15.4.yaml

@@ -0,0 +1,26 @@

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