a33905e · Idris-dev · git.iko.soy

docs/effects/impleff.rst+1−1

compare with master

unifiedsplit

@@ -144,7 +144,7 @@ functions in ``Eff``, as follows:

144

145**An implementation detail (aside):** The ``call`` function converts

146an ``Effect`` to a function in ``Eff``, given a proof that the effect

147−is available. This proof can be constructed automatically by , since

147+is available. This proof can be constructed automatically, since

148it is essentially an index into a statically known list of effects:

149

150.. code-block:: idris

docs/reference/ffi.rst+42−2

@@ -115,6 +115,24 @@ For C, this is:

115 FFI_C : FFI

116 FFI_C = MkFFI C_Types String String

117

118+Linking foreign code

119+====================

120+

121+This is the example of linking C code.

122+

123+.. code-block:: idris

124+ %include C "mylib.h"

125+ %link C "mylib.o"

126+

127+Example Makefile

128+

129+.. code-block:: shell

130+ DEFAULT: mylib.o main.idr

131+ idris main.idr -o executableFile

132+

133+ clean:

134+ rm -f executableFile mylib.o main.ibc

135+

118Foreign calls

136Foreign calls

119=============

137=============

120

138

@@ -336,9 +354,10 @@ Usage from C code

336

354

337 CData some_allocating_fun(int arg)

355 CData some_allocating_fun(int arg)

338 {

356 {

357+ size_t size = sizeof(...);

339− void * data = (void *) malloc(...);

358+ void * data = (void *) malloc(size);

340 // ...

359 // ...

341− return cdata_manage(data, finalizer);

360+ return cdata_manage(data, size, finalizer);

342 }

361 }

343

362

344 int other_fun(CData cd, int arg)

363 int other_fun(CData cd, int arg)

@@ -347,6 +366,27 @@ Usage from C code

347 return result;

366 return result;

348 }

367 }

349

368

369+The ``Raw`` type constructor allows you to access or return a runtime

370+representation of the value. For instance, if you want to copy a string

371+generated from C code into an Idris value, you may want to return a

372+``Raw String``instead of a ``String`` and use ``MKSTR`` or ``MKSTRlen`` to

373+copy it over.

374+

375+.. code-block:: idris

376+

377+ getString : () -> IO (Raw String)

378+ getString () = foreign FFI_C "get_string" (IO (Raw String))

379+

380+.. code-block:: cpp

381+

382+ const VAL get_string ()

383+ {

384+ char * c_string = get_string_allocated_with_malloc()

385+ const VAL idris_string = MKSTR(c_string);

386+ free(c_string);

387+ return idris_string

388+ }

389+

350FFI implementation

390FFI implementation

351------------------

391------------------

352

392

docs/reference/syntax-guide.rst+6

@@ -390,6 +390,12 @@ Totality

390 partial

391 covering

392

393+Sets explicitly to which extent pattern matching is terminating and/or

394+exhaustive. A ``partial`` pattern matching makes no assumption. A ``covering``

395+pattern matching ensures that pattern matching is exhaustive on its clauses.

396+Furthermore, a ``total`` pattern matching enforces both exhaustivity and

397+termination of the evaluation of its clauses.

398+

393Implicit Coercion

399Implicit Coercion

394^^^^^^^^^^^^^^^^^

400^^^^^^^^^^^^^^^^^

395

401

docs/st/state.rst+1−1

@@ -164,7 +164,7 @@ can define ``ioMakeAndIncrement`` as follows:

164 lift $ putStrLn ("var = " ++ show !(read var))

165 delete var

166

167−The ``lift`` function allows us to use funtions from the underlying

167+The ``lift`` function allows us to use functions from the underlying

168computation context (``IO`` here) directly. Again, we'll see the exact type

169of ``lift`` shortly.

170

docs/tutorial/conclusions.rst+1−1

@@ -11,7 +11,7 @@ dependent types in general, can be obtained from various sources:

11 questions on the mailing list.

12

13- The IRC channel ``#idris``, on

14− `chat.freenode.net <http://chat.freenode.net>`__.

14+ `webchat.freenode.net <https://webchat.freenode.net/>`__.

15

16- The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further

17 user provided information, in particular:

idris.cabal+8−7

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

100

101custom-setup

102 setup-depends:

103− Cabal >= 1.10 && <2.3,

103+ Cabal >= 1.10 && <2.5,

104 base >= 4 && <5,

105 directory,

106 filepath,

@@ -270,7 +270,7 @@ Library

270 , BuildFlags_idris

271

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

273− , aeson >= 0.6 && < 1.4

273+ , aeson >= 0.6 && < 1.5

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

275 , ansi-terminal < 0.9

276 , ansi-wl-pprint < 0.7

@@ -281,18 +281,19 @@ Library

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

282 , bytestring < 0.11

283 , cheapskate >= 0.1.1 && < 0.2

284− , code-page >= 0.1 && < 0.2

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

285− , containers >= 0.5 && < 0.6

285+ , containers >= 0.5 && < 0.7

286 , deepseq < 1.5

287 , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0

288 , filepath < 1.5

289 , fingertree >= 0.1.4.1 && < 0.2

290 , haskeline >= 0.7 && < 0.8

291 , ieee754 >= 0.7 && < 0.9

292− , megaparsec >= 6.2 && < 7

292+ , megaparsec >= 7.0.4 && < 8

293 , mtl >= 2.1 && < 2.3

294− , network < 2.8

294+ , network >= 2.7 && < 2.9

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

296+ , parser-combinators >= 1.0.0

296 , pretty < 1.2

297 , pretty < 1.2

297 , process < 1.7

298 , process < 1.7

298 , regex-tdfa >= 1.2

299 , regex-tdfa >= 1.2

@@ -307,7 +308,7 @@ Library

307 , utf8-string < 1.1

308 , utf8-string < 1.1

308 , vector < 0.13

309 , vector < 0.13

309 , vector-binary-instances < 0.3

310 , vector-binary-instances < 0.3

310− , zip-archive > 0.2.3.5 && < 0.4

311+ , zip-archive > 0.2.3.5 && < 0.5

311 , fsnotify >= 0.2 && < 2.2

312 , fsnotify >= 0.2 && < 2.2

312 , async < 2.3

313 , async < 2.3

313

314

jsrts/Runtime-javascript.js+6−2

@@ -7,5 +7,9 @@ $JSRTS.prim_systemInfo = function (index) {

7 }

8 return "";

9};

10+

10−$JSRTS.prim_writeStr = function (x) { return console.log(x) }

11+$JSRTS.prim_writeStr = function (x) { return console.log(x) };

12+

11−$JSRTS.prim_readStr = function () { return prompt('Prelude.getLine') };

13+$JSRTS.prim_readStr = function () { return prompt('Prelude.getLine') };

14+

15+$JSRTS.die = function (message) { throw new Error(message) };

jsrts/Runtime-node.js+10−1

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

1$JSRTS.os = require('os');

2+

2$JSRTS.fs = require('fs');

3$JSRTS.fs = require('fs');

4+

3$JSRTS.prim_systemInfo = function (index) {

5$JSRTS.prim_systemInfo = function (index) {

4 switch (index) {

6 switch (index) {

5 case 0:

7 case 0:

@@ -9,7 +11,9 @@ $JSRTS.prim_systemInfo = function (index) {

9 }

11 }

10 return "";

12 return "";

11};

13};

14+

12−$JSRTS.prim_writeStr = function (x) { return process.stdout.write(x) }

15+$JSRTS.prim_writeStr = function (x) { return process.stdout.write(x) };

16+

13$JSRTS.prim_readStr = function () {

17$JSRTS.prim_readStr = function () {

14 var ret = '';

18 var ret = '';

15 var b = new Buffer(1024);

19 var b = new Buffer(1024);

@@ -28,4 +32,9 @@ $JSRTS.prim_readStr = function () {

28 }

32 }

29 }

33 }

30 return ret;

34 return ret;

35+};

36+

37+$JSRTS.die = function (message) {

38+ console.error(message);

39+ process.exit(-1);

31};

40};

libs/base/Data/Vect.idr+2−1

@@ -315,7 +315,8 @@ concat (v::vs) = v ++ concat vs

315

316||| Foldr without seeding the accumulator

317foldr1 : (t -> t -> t) -> Vect (S n) t -> t

318−foldr1 f (x::xs) = foldr f x xs

318+foldr1 f [x] = x

319+foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))

319

320

320||| Foldl without seeding the accumulator

321||| Foldl without seeding the accumulator

321foldl1 : (t -> t -> t) -> Vect (S n) t -> t

322foldl1 : (t -> t -> t) -> Vect (S n) t -> t

libs/contrib/Data/Nat.idr+17

@@ -1,8 +1,25 @@

1module Data.Nat

2

3%default total

4+%access public export

4

5

5diff : Nat -> Nat -> Nat

6diff : Nat -> Nat -> Nat

6diff k Z = k

7diff k Z = k

7diff Z j = j

8diff Z j = j

8diff (S k) (S j) = diff k j

9diff (S k) (S j) = diff k j

10+

11+ltePlus : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 + m2) (n1 + n2)

12+ltePlus {n1=Z} LTEZero lte = lte

13+ltePlus {n1=S k} LTEZero lte = lteSuccRight $ ltePlus {n1=k} LTEZero lte

14+ltePlus (LTESucc lte1) lte2 = LTESucc $ ltePlus lte1 lte2

15+

16+lteCongPlus : (k : Nat) -> LTE m n -> LTE (m + k) (n + k)

17+lteCongPlus k lte = ltePlus lte lteRefl

18+

19+lteMult : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 * m2) (n1 * n2)

20+lteMult LTEZero _ = LTEZero

21+lteMult {m1=S k} (LTESucc _) LTEZero = rewrite multZeroRightZero k in LTEZero

22+lteMult (LTESucc lte1) (LTESucc lte2) = LTESucc $ ltePlus lte2 $ lteMult lte1 $ LTESucc lte2

23+

24+lteCongMult : (k : Nat) -> LTE m n -> LTE (m * k) (n * k)

25+lteCongMult k lte = lteMult lte lteRefl

libs/contrib/Data/SortedMap.idr+4

@@ -287,6 +287,10 @@ export

287mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v

288mergeLeft = mergeWith const

289

290+export

291+(Show k, Show v) => Show (SortedMap k v) where

292+ show m = "fromList " ++ (show $ toList m)

293+

290-- TODO: is this the right variant of merge to use for this? I think it is, but

294-- TODO: is this the right variant of merge to use for this? I think it is, but

291-- I could also see the advantages of using `mergeLeft`. The current approach is

295-- I could also see the advantages of using `mergeLeft`. The current approach is

292-- strictly more powerful I believe, because `mergeLeft` can be emulated with

296-- strictly more powerful I believe, because `mergeLeft` can be emulated with

libs/contrib/Text/Lexer.idr+4−4

@@ -161,14 +161,14 @@ hexDigits : Lexer

161hexDigits = some hexDigit

162

163||| Recognise a single octal digit

164−||| /[0-8]/

164+||| /[0-7]/

165octDigit : Lexer

166−octDigit = pred isHexDigit

166+octDigit = pred isOctDigit

167

168||| Recognise one or more octal digits

169−||| /[0-8]+/

169+||| /[0-7]+/

170octDigits : Lexer

171−octDigits = some hexDigit

171+octDigits = some octDigit

172

173||| Recognise a single alpha character

174||| /[A-Za-z]/

libs/prelude/Prelude/Bool.idr+1−1

@@ -12,7 +12,7 @@ data Bool = False | True

12||| The underlying implementation of the if ... then ... else ... syntax

13||| @ b the condition on the if

14||| @ t the value if b is true

15−||| @ e the falue if b is false

15+||| @ e the value if b is false

16ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

17ifThenElse True t e = t

18ifThenElse False t e = e

libs/prelude/Prelude/List.idr+10−4

@@ -436,12 +436,12 @@ intercalate sep xss = concat $ intersperse sep xss

436|||

437||| transpose [[], [1, 2]] = [[1], [2]]

438||| transpose (transpose [[], [1, 2]]) = [[1, 2]]

439−|||

440−||| TODO: Solution which satisfies the totality checker?

441transpose : List (List a) -> List (List a)

439transpose : List (List a) -> List (List a)

442transpose [] = []

440transpose [] = []

443−transpose ([] :: xss) = transpose xss

441+transpose (heads :: tails) = spreadHeads heads (transpose tails) where

444−transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))

442+ spreadHeads [] tails = tails

443+ spreadHeads (head :: heads) [] = [head] :: spreadHeads heads []

444+ spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails

445

446--------------------------------------------------------------------------------

447-- Membership tests

@@ -861,6 +861,12 @@ catMaybes (x::xs) =

861-- Properties

862--------------------------------------------------------------------------------

863

864+Uninhabited ([] = _ :: _) where

865+ uninhabited Refl impossible

866+

867+Uninhabited (_ :: _ = []) where

868+ uninhabited Refl impossible

869+

864||| (::) is injective

870||| (::) is injective

865consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->

871consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->

866 (x :: xs) = (y :: ys) -> (x = y, xs = ys)

872 (x :: xs) = (y :: ys) -> (x = y, xs = ys)

rts/idris_heap.c+2

@@ -110,12 +110,14 @@ void c_heap_destroy(CHeap * heap)

110void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)

111{

112 char * mem = malloc(heap_size);

113+

113 if (mem == NULL) {

114 if (mem == NULL) {

114 fprintf(stderr,

115 fprintf(stderr,

115 "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",

116 "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",

116 heap_size);

117 heap_size);

117 exit(EXIT_FAILURE);

118 exit(EXIT_FAILURE);

118 }

119 }

120+ memset(mem, 0, heap_size);

119

121

120 h->heap = mem;

122 h->heap = mem;

121 h->next = aligned_heap_pointer(h->heap);

123 h->next = aligned_heap_pointer(h->heap);

rts/idris_rts.c−2

@@ -209,7 +209,6 @@ void * allocate(size_t sz, int lock) {

209}

210

211void* iallocate(VM * vm, size_t isize, int outerlock) {

212−// return malloc(isize);

213 size_t size = aligned(isize);

212 size_t size = aligned(isize);

214

213

215#ifdef HAS_PTHREAD

214#ifdef HAS_PTHREAD

@@ -225,7 +224,6 @@ void* iallocate(VM * vm, size_t isize, int outerlock) {

225 char* ptr = vm->heap.next;

224 char* ptr = vm->heap.next;

226 vm->heap.next += size;

225 vm->heap.next += size;

227 assert(vm->heap.next <= vm->heap.end);

226 assert(vm->heap.next <= vm->heap.end);

228− memset(ptr, 0, size);

229 ((Hdr*)ptr)->sz = isize;

227 ((Hdr*)ptr)->sz = isize;

230

228

231#ifdef HAS_PTHREAD

229#ifdef HAS_PTHREAD

src/IRTS/Compiler.hs+1−1

@@ -533,7 +533,7 @@ irTree top args tree = do

533

534irSC :: Name -> Vars -> SC -> Idris LExp

535irSC top vs (STerm t) = irTerm top vs [] t

536−irSC top vs (UnmatchedCase str) = return $ LLazyExp $ LError str

536+irSC top vs (UnmatchedCase str) = return $ LError str

537

538irSC top vs (ProjCase tm alts) = do

539 tm' <- irTerm top vs [] tm

src/IRTS/JavaScript/AST.hs+1−1

@@ -202,7 +202,7 @@ jsStmt2Text (JsSwitchCase exp l d) =

202 default2Text Nothing = ""

203 default2Text (Just z) =

204 T.concat ["default:\n", indent $ T.concat [jsStmt2Text z, ";\nbreak;\n"]]

205−jsStmt2Text (JsError t) = T.concat ["throw new Error( ", jsAst2Text t, ");"]

205+jsStmt2Text (JsError t) = T.concat ["$JSRTS.die(", jsAst2Text t, ");\n"]

206jsStmt2Text (JsForever x) =

207 T.concat ["for(;;) {\n", indent $ jsStmt2Text x, "}\n"]

208jsStmt2Text JsContinue = "continue;"

src/Idris/Elab/Clause.hs+5−3

@@ -660,11 +660,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

660 i <- getIState

661 inf <- isTyInferred fname

662

663− -- Check if we have "with" patterns outside of "with" block

663+ -- Check if we have extra "with" patterns

664− when (isOutsideWith lhs_in && (not $ null withs)) $

664+ when (not $ null withs) $

665 ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)

666 (Elaborating "left hand side of " fname Nothing

667+ (Msg $ if isOutsideWith lhs_in

667− (Msg "unexpected patterns outside of \"with\" block")))

668+ then "unexpected patterns outside of \"with\" block"

669+ else "unexpected extra \"with\" patterns")))

668

670

669 -- get the parameters first, to pass through to any where block

671 -- get the parameters first, to pass through to any where block

670 let fn_ty = case lookupTy fname ctxt of

672 let fn_ty = case lookupTy fname ctxt of

src/Idris/IBC.hs+13−2

@@ -265,8 +265,9 @@ hashName i n = qhash (i * 5381) (show n)

265

266calculateHash :: IState -> IBCFile -> Int

267calculateHash ist f

268− = let acc = L.filter exported (ibc_access f) in

268+ = let acc = L.filter exported (ibc_access f)

269+ inl = L.filter (inlinable (map fst acc)) (ibc_flags f) in

269− mkHashFrom (map fst acc) (getDefs acc)

270+ mkHashFrom (map fst acc) (getDefs acc ++ L.concatMap getFullDef inl)

270 where

271 where

271 mkHashFrom :: [Name] -> [Term] -> Int

272 mkHashFrom :: [Name] -> [Term] -> Int

272 mkHashFrom ns tms = sum (L.zipWith hashName [1..] ns) +

273 mkHashFrom ns tms = sum (L.zipWith hashName [1..] ns) +

@@ -276,6 +277,10 @@ calculateHash ist f

276 exported (_, Frozen) = True

277 exported (_, Frozen) = True

277 exported _ = False

278 exported _ = False

278

279

280+ inlinable acc (n, opts)

281+ = n `elem` acc &&

282+ (Inlinable `elem` opts || PEGenerated `elem` opts)

283+

279 findTms :: [(a, Term, Term)] -> [Term]

284 findTms :: [(a, Term, Term)] -> [Term]

280 findTms = L.concatMap (\ (_, x, y) -> [x, y])

285 findTms = L.concatMap (\ (_, x, y) -> [x, y])

281

286

@@ -299,6 +304,12 @@ calculateHash ist f

299 Just ty -> ty : ts

304 Just ty -> ty : ts

300 getDefs (_ : ns) = getDefs ns

305 getDefs (_ : ns) = getDefs ns

301

306

307+ getFullDef :: (Name, [FnOpt]) -> [Term]

308+ getFullDef (n, _)

309+ = case lookupTyExact n (tt_ctxt ist) of

310+ Nothing -> []

311+ Just ty -> ty : patDef n

312+

302-- | Write a package index containing all the imports in the current

313-- | Write a package index containing all the imports in the current

303-- IState Used for ':search' of an entire package, to ensure

314-- IState Used for ':search' of an entire package, to ensure

304-- everything is loaded.

315-- everything is loaded.

src/Idris/Output.hs+4−3

@@ -75,9 +75,10 @@ instance Message SimpleWarning where

75formatMessage :: Message w => w -> Idris OutputDoc

76formatMessage w = do

77 i <- getIState

78− maybeSource <- case messageSource w of

78+ rs <- readSource fc

79+ let maybeSource = case rs of

79− Just src -> pure (Just src)

80+ Just src -> Just src

80− Nothing -> readSource fc

81+ Nothing -> messageSource w

81 let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))

82 let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))

82 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

83 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

83 where

84 where

src/Idris/Package/Parser.hs+11−7

@@ -13,9 +13,10 @@ import Idris.Imports

13import Idris.Options (Opt)

14import Idris.Package.Common

15import Idris.Parser (moduleName)

16−import Idris.Parser.Helpers (Parser, Parsing, eol, iName, identifier, isEol,

16+import Idris.Parser.Helpers (Parser, Parsing, eol, iName, identifier,

17+ identifierWithExtraChars, isEol, lchar,

17− lchar, packageName, parseErrorDoc, reserved,

18+ packageName, parseErrorDoc, reserved, runparser,

18− runparser, someSpace, stringLiteral)

19+ someSpace, stringLiteral)

19

20

20import Control.Applicative

21import Control.Applicative

21import Control.Monad.State.Strict

22import Control.Monad.State.Strict

@@ -26,14 +27,13 @@ import System.Exit

26import System.FilePath (isValid, takeExtension, takeFileName)

27import System.FilePath (isValid, takeExtension, takeFileName)

27import Text.Megaparsec ((<?>))

28import Text.Megaparsec ((<?>))

28import qualified Text.Megaparsec as P

29import qualified Text.Megaparsec as P

29−import qualified Text.Megaparsec.Char as P

30import qualified Text.PrettyPrint.ANSI.Leijen as PP

31

32type PParser = Parser PkgDesc

33

34parseDesc :: FilePath -> IO PkgDesc

35parseDesc fp = do

36− when (not $ takeExtension fp == ".ipkg") $ do

36+ unless (takeExtension fp == ".ipkg") $ do

37 putStrLn $ unwords ["The presented iPKG file does not have a '.ipkg' extension:", show fp]

38 exitWith (ExitFailure 1)

39 res <- doesFileExist fp

@@ -119,17 +119,20 @@ pOptions = do

119 Opts.Failure e -> fail $ fst $ Opts.renderFailure e ""

120 _ -> fail "Unexpected error"

121

122+libIdentifier :: Parsing m => m String

123+libIdentifier = identifierWithExtraChars "_'-."

124+

122pClause :: PParser ()

125pClause :: PParser ()

123pClause = clause "executable" filename (\st v -> st { execout = Just v })

126pClause = clause "executable" filename (\st v -> st { execout = Just v })

124 <|> clause "main" (iName []) (\st v -> st { idris_main = Just v })

127 <|> clause "main" (iName []) (\st v -> st { idris_main = Just v })

125− <|> clause "sourcedir" identifier (\st v -> st { sourcedir = v })

128+ <|> clause "sourcedir" (identifier <|> stringLiteral) (\st v -> st { sourcedir = v })

126 <|> clause "opts" pOptions (\st v -> st { idris_opts = v ++ idris_opts st })

129 <|> clause "opts" pOptions (\st v -> st { idris_opts = v ++ idris_opts st })

127 <|> clause "pkgs" (commaSep (pPkgName <* someSpace)) (\st ps ->

130 <|> clause "pkgs" (commaSep (pPkgName <* someSpace)) (\st ps ->

128 let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps

131 let pkgs = pureArgParser $ concatMap (\x -> ["-p", show x]) ps

129 in st { pkgdeps = ps `union` pkgdeps st

132 in st { pkgdeps = ps `union` pkgdeps st

130 , idris_opts = pkgs ++ idris_opts st })

133 , idris_opts = pkgs ++ idris_opts st })

131 <|> clause "modules" (commaSep moduleName) (\st v -> st { modules = modules st ++ v })

134 <|> clause "modules" (commaSep moduleName) (\st v -> st { modules = modules st ++ v })

132− <|> clause "libs" (commaSep identifier) (\st v -> st { libdeps = libdeps st ++ v })

135+ <|> clause "libs" (commaSep libIdentifier) (\st v -> st { libdeps = libdeps st ++ v })

133 <|> clause "objs" (commaSep identifier) (\st v -> st { objs = objs st ++ v })

136 <|> clause "objs" (commaSep identifier) (\st v -> st { objs = objs st ++ v })

134 <|> clause "makefile" (iName []) (\st v -> st { makefile = Just (show v) })

137 <|> clause "makefile" (iName []) (\st v -> st { makefile = Just (show v) })

135 <|> clause "tests" (commaSep (iName [])) (\st v -> st { idris_tests = idris_tests st ++ v })

138 <|> clause "tests" (commaSep (iName [])) (\st v -> st { idris_tests = idris_tests st ++ v })

@@ -142,3 +145,4 @@ pClause = clause "executable" filename (\st v -> st { execout = Just v })

142 <|> clause "brief" stringLiteral (\st v -> st { pkgbrief = Just v })

145 <|> clause "brief" stringLiteral (\st v -> st { pkgbrief = Just v })

143 <|> clause "author" textUntilEol (\st v -> st { pkgauthor = Just v })

146 <|> clause "author" textUntilEol (\st v -> st { pkgauthor = Just v })

144 <|> clause "maintainer" textUntilEol (\st v -> st { pkgmaintainer = Just v })

147 <|> clause "maintainer" textUntilEol (\st v -> st { pkgmaintainer = Just v })

148+

src/Idris/Parser.hs−1

@@ -60,7 +60,6 @@ import qualified System.Directory as Dir (doesFileExist, getModificationTime,

60import System.FilePath

61import Text.Megaparsec ((<?>))

62import qualified Text.Megaparsec as P

63−import qualified Text.Megaparsec.Char as P

64import qualified Text.PrettyPrint.ANSI.Leijen as PP

63import qualified Text.PrettyPrint.ANSI.Leijen as PP

65

64

66{-

65{-

src/Idris/Parser/Expr.hs+2−2

@@ -20,6 +20,7 @@ import Prelude hiding (pi)

20import Control.Applicative

21import Control.Arrow (left)

22import Control.Monad

23+import qualified Control.Monad.Combinators.Expr as P

23import Control.Monad.State.Strict

24import Control.Monad.State.Strict

24import Data.Function (on)

25import Data.Function (on)

25import Data.List

26import Data.List

@@ -27,7 +28,6 @@ import Data.Maybe

27import Text.Megaparsec ((<?>))

28import Text.Megaparsec ((<?>))

28import qualified Text.Megaparsec as P

29import qualified Text.Megaparsec as P

29import qualified Text.Megaparsec.Char as P

30import qualified Text.Megaparsec.Char as P

30−import qualified Text.Megaparsec.Expr as P

31

32-- | Allow implicit type declarations

33allowImp :: SyntaxInfo -> SyntaxInfo

@@ -1406,7 +1406,7 @@ VerbatimString_t ::=

1406 -}

1407verbatimStringLiteral :: Parsing m => m String

1408verbatimStringLiteral = token $ do P.try $ string "\"\"\""

1409− str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")

1409+ str <- P.manyTill P.anySingle $ P.try (string "\"\"\"")

1410 moreQuotes <- P.many $ P.char '"'

1411 return $ str ++ moreQuotes

1412

src/Idris/Parser/Helpers.hs+11−7

@@ -36,6 +36,7 @@ module Idris.Parser.Helpers

36 , iName

37 , name

38 , identifier

39+ , identifierWithExtraChars

39 , packageName

40 , packageName

40 -- * Access

41 -- * Access

41 , accessibility

42 , accessibility

@@ -269,10 +270,10 @@ reservedIdentifiers = HS.fromList

269 , "rewrite", "syntax", "then", "total", "using", "where", "with"

270 , "rewrite", "syntax", "then", "total", "using", "where", "with"

270 ]

271 ]

271

272

272−identifierOrReserved :: Parsing m => m String

273+identifierOrReservedWithExtraChars :: Parsing m => String -> m String

273−identifierOrReserved = token $ P.try $ do

274+identifierOrReservedWithExtraChars extraChars = token $ P.try $ do

274 c <- P.satisfy isAlpha <|> P.oneOf "_"

275 c <- P.satisfy isAlpha <|> P.oneOf "_"

275− cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf "_'.")

276+ cs <- P.many (P.satisfy isAlphaNum <|> P.oneOf extraChars)

276 return $ c : cs

277 return $ c : cs

277

278

278char :: Parsing m => Char -> m Char

279char :: Parsing m => Char -> m Char

@@ -295,13 +296,16 @@ reserved name = token $ P.try $ do

295 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

296 P.notFollowedBy (P.satisfy isAlphaNum <|> P.oneOf "_'.") <?> "end of " ++ name

296

297

297-- | Parses an identifier as a token

298-- | Parses an identifier as a token

298−identifier :: Parsing m => m String

299+identifierWithExtraChars :: Parsing m => String -> m String

299−identifier = P.try $ do

300+identifierWithExtraChars extraChars = P.try $ do

300− ident <- identifierOrReserved

301+ ident <- identifierOrReservedWithExtraChars extraChars

301 when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident

302 when (ident `HS.member` reservedIdentifiers) $ P.unexpected . P.Label . NonEmpty.fromList $ "reserved " ++ ident

302 when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"

303 when (ident == "_") $ P.unexpected . P.Label . NonEmpty.fromList $ "wildcard"

303 return ident

304 return ident

304

305

306+identifier :: Parsing m => m String

307+identifier = identifierWithExtraChars "_'."

308+

305-- | Parses an identifier with possible namespace as a name

309-- | Parses an identifier with possible namespace as a name

306iName :: Parsing m => [String] -> m Name

310iName :: Parsing m => [String] -> m Name

307iName bad = maybeWithNS identifier bad <?> "name"

311iName bad = maybeWithNS identifier bad <?> "name"

@@ -393,7 +397,7 @@ popIndent = do ist <- get

393

397

394-- | Gets current indentation

398-- | Gets current indentation

395indent :: Parsing m => m Int

399indent :: Parsing m => m Int

396−indent = P.unPos . P.sourceColumn <$> P.getPosition

400+indent = P.unPos . P.sourceColumn <$> P.getSourcePos

397

401

398-- | Gets last indentation

402-- | Gets last indentation

399lastIndent :: (MonadState IState m) => m Int

403lastIndent :: (MonadState IState m) => m Int

src/Idris/Parser/Ops.hs+1−2

@@ -17,14 +17,13 @@ import Prelude hiding (pi)

17

18import Control.Applicative

19import Control.Monad

20+import qualified Control.Monad.Combinators.Expr as P

20import Control.Monad.State.Strict

21import Control.Monad.State.Strict

21import Data.Char (isAlpha)

22import Data.Char (isAlpha)

22import Data.List

23import Data.List

23import Data.List.NonEmpty (fromList)

24import Data.List.NonEmpty (fromList)

24import Text.Megaparsec ((<?>))

25import Text.Megaparsec ((<?>))

25import qualified Text.Megaparsec as P

26import qualified Text.Megaparsec as P

26−import qualified Text.Megaparsec.Char as P

27−import qualified Text.Megaparsec.Expr as P

28

27

29-- | Creates table for fixity declarations to build expression parser

28-- | Creates table for fixity declarations to build expression parser

30-- using pre-build and user-defined operator/fixity declarations

29-- using pre-build and user-defined operator/fixity declarations

src/Idris/Parser/Stack.hs+20−9

@@ -57,23 +57,34 @@ type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)

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

58runparser p i inputname s =

59 case P.parse (runWriterT (evalStateT p i)) inputname s of

60− Left err -> Left $ ParseError s err

60+ Left err -> Left $ ParseError err

61 Right v -> Right $ fst v

62

63{- * Parse errors -}

64

65+newtype ParseError = ParseError { unParseError :: P.ParseErrorBundle String Void }

66+

65−data ParseError = ParseError String (P.ParseError (P.Token String) Void)

67+parseError :: ParseError -> P.ParseError String Void

68+parseError = NonEmpty.head . P.bundleErrors . unParseError

69+

70+parseErrorPosState :: ParseError -> P.PosState String

71+parseErrorPosState = P.bundlePosState . unParseError

72+

73+parseErrorOffset :: ParseError -> Int

74+parseErrorOffset = P.errorOffset . parseError

66

75

67instance Message ParseError where

76instance Message ParseError where

68− messageExtent (ParseError _ err) = sourcePositionFC pos

77+ messageExtent err = sourcePositionFC pos

78+ where

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

80+ messageText = PP.text . init . P.parseErrorTextPretty . parseError

81+ messageSource err = Just sline

69 where

82 where

70− (pos NonEmpty.:| _) = P.errorPos err

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

71− messageText (ParseError _ err) = PP.text . init . P.parseErrorTextPretty $ err

72− messageSource (ParseError src _) = Just src

73

84

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

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

75−prettyError :: ParseError -> String

86+prettyError :: ParseError -> String

76−prettyError (ParseError s err) = P.parseErrorPretty' s err

87+prettyError = P.errorBundlePretty . unParseError

77

88

78{- * Mark and restore -}

89{- * Mark and restore -}

79

90

@@ -104,7 +115,7 @@ sourcePositionFC (P.SourcePos name line column) =

104-- This is useful when the position is needed in a way unrelated to the

115-- This is useful when the position is needed in a way unrelated to the

105-- heirarchy of parsers. Prefer using @withExtent@ and friends.

116-- heirarchy of parsers. Prefer using @withExtent@ and friends.

106getFC :: Parsing m => m FC

117getFC :: Parsing m => m FC

107−getFC = sourcePositionFC <$> P.getPosition

118+getFC = sourcePositionFC <$> P.getSourcePos

108

119

109-- | Add an extent (widen) our current parsing context.

120-- | Add an extent (widen) our current parsing context.

110addExtent :: MonadWriter FC m => FC -> m ()

121addExtent :: MonadWriter FC m => FC -> m ()

src/Idris/REPL/Parser.hs+5−6

@@ -33,7 +33,6 @@ import Data.List.Split (splitOn)

33import System.Console.ANSI (Color(..))

34import System.FilePath ((</>))

35import qualified Text.Megaparsec as P

36−import qualified Text.Megaparsec.Char as P

37

36

38parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

37parseCmd :: IState -> String -> String -> Either IP.ParseError (Either String Command)

39parseCmd i inputname = IP.runparser pCmd i inputname . trim

38parseCmd i inputname = IP.runparser pCmd i inputname . trim

@@ -68,7 +67,7 @@ parserCommandsForHelp =

68 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

67 , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

69 , (["doc"], NameArg, "Show internal documentation", cmd_doc)

68 , (["doc"], NameArg, "Show internal documentation", cmd_doc)

70 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

69 , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

71− , genArg "namespace" (P.many P.anyChar) MakeDoc)

70+ , genArg "namespace" (P.many P.anySingle) MakeDoc)

72 , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

71 , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

73 , cmd_apropos)

72 , cmd_apropos)

74 , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

73 , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

@@ -198,7 +197,7 @@ pCmd = P.choice [ do c <- cmd names; parser c

198 where nop = do P.eof; return (Right NOP)

197 where nop = do P.eof; return (Right NOP)

199 unrecognized = do

198 unrecognized = do

200 IP.lchar ':'

199 IP.lchar ':'

201− cmd <- P.many P.anyChar

200+ cmd <- P.many P.anySingle

202 let cmd' = takeWhile (/=' ') cmd

201 let cmd' = takeWhile (/=' ') cmd

203 return (Left $ "Unrecognized command: " ++ cmd')

202 return (Left $ "Unrecognized command: " ++ cmd')

204

203

@@ -260,7 +259,7 @@ nameArg = genArg "name" IP.name

260fnNameArg = genArg "functionname" IP.fnName

259fnNameArg = genArg "functionname" IP.fnName

261

260

262strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

261strArg :: (String -> Command) -> String -> IP.IdrisParser (Either String Command)

263−strArg = genArg "string" (P.many P.anyChar)

262+strArg = genArg "string" (P.many P.anySingle)

264

263

265moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

264moduleArg :: (FilePath -> Command) -> String -> IP.IdrisParser (Either String Command)

266moduleArg = genArg "module" (fmap toPath IP.identifier)

265moduleArg = genArg "module" (fmap toPath IP.identifier)

@@ -342,7 +341,7 @@ cmd_execute name = do

342

341

343cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

342cmd_dynamic :: String -> IP.IdrisParser (Either String Command)

344cmd_dynamic name = do

343cmd_dynamic name = do

345− let optArg = do l <- P.many P.anyChar

344+ let optArg = do l <- P.many P.anySingle

346 if (l /= "")

345 if (l /= "")

347 then return $ Right (DynamicLink l)

346 then return $ Right (DynamicLink l)

348 else return $ Right ListDynamic

347 else return $ Right ListDynamic

@@ -440,7 +439,7 @@ cmd_unlet name = Right . Undefine <$> P.many IP.name

440cmd_loadto :: String -> IP.IdrisParser (Either String Command)

439cmd_loadto :: String -> IP.IdrisParser (Either String Command)

441cmd_loadto name = do

440cmd_loadto name = do

442 toline <- fromInteger <$> IP.natural

441 toline <- fromInteger <$> IP.natural

443− f <- P.many P.anyChar

442+ f <- P.many P.anySingle

444 return (Right (Load f (Just toline)))

443 return (Right (Load f (Just toline)))

445

444

446cmd_colour :: String -> IP.IdrisParser (Either String Command)

445cmd_colour :: String -> IP.IdrisParser (Either String Command)

stack.yaml+5−2

@@ -1,10 +1,13 @@

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

2−resolver: lts-11.14

2+resolver: lts-12.21

3

4packages:

5 - location: .

6

7−extra-deps: []

7+extra-deps:

8+ - megaparsec-7.0.4

9+ - parser-combinators-1.0.0

10+

8

11

9flags:

12flags:

10 idris:

13 idris:

test/TestRun.hs+20−14

@@ -11,6 +11,7 @@ import Data.Proxy

11import Data.Typeable

12import Options.Applicative

13import System.Directory

14+import System.Environment

14import System.Exit

15import System.Exit

15import System.FilePath ((</>))

16import System.FilePath ((</>))

16import System.Info

17import System.Info

@@ -103,20 +104,25 @@ runTest path flags = do

103 normalise (x : xs) = x : normalise xs

104 normalise (x : xs) = x : normalise xs

104 normalise [] = []

105 normalise [] = []

105

106

107+checkNode :: IO ()

108+checkNode = do

109+ nodePath <- findExecutable "node"

110+ nodejsPath <- findExecutable "nodejs"

111+ let node = nodePath <|> nodejsPath

112+ case node of

113+ Nothing -> do

114+ putStrLn "For running the test suite against Node, node must be installed."

115+ exitFailure

116+ Just _ -> return ()

117+

106main :: IO ()

118main :: IO ()

107main = do

119main = do

108− nodePath <- findExecutable "node"

120+ args <- getArgs

109− nodejsPath <- findExecutable "nodejs"

121+ when ("--node" `elem` args) checkNode

110− let node = nodePath <|> nodejsPath

111− case node of

112− Nothing -> do

113− putStrLn "For running the test suite against Node, node must be installed."

114− exitFailure

115− Just _ -> do

116− defaultMainWithIngredients ingredients $

122+ defaultMainWithIngredients ingredients $

117 askOption $ \(NodeOpt node) ->

123 askOption $ \(NodeOpt node) ->

118− let (codegen, flags) = if node then (JS, ["--codegen", "node"])

124+ let (codegen, flags) = if node then (JS, ["--codegen", "node"])

119− else (C , [])

125+ else (C , [])

120− in

126+ in

121− mkGoldenTests (testFamiliesForCodegen codegen)

127+ mkGoldenTests (testFamiliesForCodegen codegen) (flags ++ idrisFlags)

122− (flags ++ idrisFlags)

128+

test/error006/WithPatsNoWith.idr+11

@@ -4,3 +4,14 @@ foo : Int -> Bool

4foo 1 | 2 | 3 = True

5foo _ = False

6

7+foo2: Int -> Bool

8+foo2 n with (succ n)

9+ foo2 n | 1 | 2 = True

10+ foo2 _ | _ = False

11+

12+foo3: Int -> Int -> Bool

13+foo3 n m with (succ n)

14+ foo3 _ m | 2 with (succ m)

15+ foo3 _ _ | 2 | 3 | 4 = True

16+ foo3 _ _ | 2 | _ = False

17+ foo3 _ _ | _ = True

test/error006/expected+14

@@ -5,3 +5,17 @@ WithPatsNoWith.idr:4:1-13:

5When checking left hand side of foo:

6unexpected patterns outside of "with" block

7

8+WithPatsNoWith.idr:9:3-16:

9+ |

10+9 | foo2 n | 1 | 2 = True

11+ | ~~~~~~~~~~~~~~

12+When checking left hand side of with block in WithPatsNoWith.foo2:

13+unexpected extra "with" patterns

14+

15+WithPatsNoWith.idr:15:5-24:

16+ |

17+15 | foo3 _ _ | 2 | 3 | 4 = True

18+ | ~~~~~~~~~~~~~~~~~~~~

19+When checking left hand side of with block in with block in WithPatsNoWith.foo3:

20+unexpected extra "with" patterns

21+