a33905e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1 from idris-lang/master

Syncing from original

commita33905ee66e88a8b657a6935b8f9e04c8443e2b6 authorzenntenn <zenten@zenten.ca> dateFri 25 Jan 2019, 23:15 (8 years ago) parent1a7fa35 c060a88

32 files changed+239−87

compare with master

unifiedsplit

docs/effects/impleff.rst+1−1 docs/reference/ffi.rst+42−2 docs/reference/syntax-guide.rst+6 docs/st/state.rst+1−1 docs/tutorial/conclusions.rst+1−1 idris.cabal+8−7 jsrts/Runtime-javascript.js+6−2 jsrts/Runtime-node.js+10−1 libs/base/Data/Vect.idr+2−1 libs/contrib/Data/Nat.idr+17 libs/contrib/Data/SortedMap.idr+4 libs/contrib/Text/Lexer.idr+4−4 libs/prelude/Prelude/Bool.idr+1−1 libs/prelude/Prelude/List.idr+10−4 rts/idris_heap.c+2 rts/idris_rts.c−2 src/IRTS/Compiler.hs+1−1 src/IRTS/JavaScript/AST.hs+1−1 src/Idris/Elab/Clause.hs+5−3 src/Idris/IBC.hs+13−2 src/Idris/Output.hs+4−3 src/Idris/Package/Parser.hs+11−7 src/Idris/Parser.hs−1 src/Idris/Parser/Expr.hs+2−2 src/Idris/Parser/Helpers.hs+11−7 src/Idris/Parser/Ops.hs+1−2 src/Idris/Parser/Stack.hs+20−9 src/Idris/REPL/Parser.hs+5−6 stack.yaml+5−2 test/TestRun.hs+20−14 test/error006/WithPatsNoWith.idr+11 test/error006/expected+14

docs/effects/impleff.rst+1−1

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

144144

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

146146an ``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

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

149149

150150.. code-block:: idris

docs/reference/ffi.rst+42−2

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

115115 FFI_C : FFI

116116 FFI_C = MkFFI C_Types String String

117117

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+

118136Foreign calls

119137=============

120138

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

336354

337355 CData some_allocating_fun(int arg)

338356 {

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

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

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

340359 // ...

341− return cdata_manage(data, finalizer);

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

342361 }

343362

344363 int other_fun(CData cd, int arg)

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

347366 return result;

348367 }

349368

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+

350390FFI implementation

351391------------------

352392

docs/reference/syntax-guide.rst+6

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

390390 partial

391391 covering

392392

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+

393399Implicit Coercion

394400^^^^^^^^^^^^^^^^^

395401

docs/st/state.rst+1−1

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

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

165165 delete var

166166

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

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

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

169169of ``lift`` shortly.

170170

docs/tutorial/conclusions.rst+1−1

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

1111 questions on the mailing list.

1212

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

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

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

1515

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

1717 user provided information, in particular:

idris.cabal+8−7

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

100100

101101custom-setup

102102 setup-depends:

103− Cabal >= 1.10 && <2.3,

103+ Cabal >= 1.10 && <2.5,

104104 base >= 4 && <5,

105105 directory,

106106 filepath,

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

270270 , BuildFlags_idris

271271

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

273− , aeson >= 0.6 && < 1.4

273+ , aeson >= 0.6 && < 1.5

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

275275 , ansi-terminal < 0.9

276276 , ansi-wl-pprint < 0.7

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

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

282282 , bytestring < 0.11

283283 , cheapskate >= 0.1.1 && < 0.2

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

285− , containers >= 0.5 && < 0.6

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

285+ , containers >= 0.5 && < 0.7

286286 , deepseq < 1.5

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

288288 , filepath < 1.5

289289 , fingertree >= 0.1.4.1 && < 0.2

290290 , haskeline >= 0.7 && < 0.8

291291 , ieee754 >= 0.7 && < 0.9

292− , megaparsec >= 6.2 && < 7

292+ , megaparsec >= 7.0.4 && < 8

293293 , mtl >= 2.1 && < 2.3

294− , network < 2.8

294+ , network >= 2.7 && < 2.9

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

296+ , parser-combinators >= 1.0.0

296297 , pretty < 1.2

297298 , process < 1.7

298299 , regex-tdfa >= 1.2

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

307308 , utf8-string < 1.1

308309 , vector < 0.13

309310 , vector-binary-instances < 0.3

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

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

311312 , fsnotify >= 0.2 && < 2.2

312313 , async < 2.3

313314

jsrts/Runtime-javascript.js+6−2

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

77 }

88 return "";

99};

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

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

10+

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

12+

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

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

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

35$JSRTS.prim_systemInfo = function (index) {

46 switch (index) {

57 case 0:

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

911 }

1012 return "";

1113};

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

14+

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

16+

1317$JSRTS.prim_readStr = function () {

1418 var ret = '';

1519 var b = new Buffer(1024);

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

2832 }

2933 }

3034 return ret;

35+};

36+

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

38+ console.error(message);

39+ process.exit(-1);

3140};

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

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

315315

316316||| Foldr without seeding the accumulator

317317foldr1 : (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))

319320

320321||| Foldl without seeding the accumulator

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

libs/contrib/Data/Nat.idr+17

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

11module Data.Nat

33%default total

4+%access public export

56diff : Nat -> Nat -> Nat

67diff k Z = k

78diff Z j = j

89diff (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

287287mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v

288288mergeLeft = mergeWith const

289289

290+export

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

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

293+

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

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

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

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

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

161161hexDigits = some hexDigit

162162

163163||| Recognise a single octal digit

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

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

165165octDigit : Lexer

166−octDigit = pred isHexDigit

166+octDigit = pred isOctDigit

167167

168168||| Recognise one or more octal digits

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

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

170170octDigits : Lexer

171−octDigits = some hexDigit

171+octDigits = some octDigit

172172

173173||| Recognise a single alpha character

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

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

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

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

1313||| @ b the condition on the if

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

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

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

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

1717ifThenElse True t e = t

1818ifThenElse False t e = e

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

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

436436|||

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

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

439−|||

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

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

442440transpose [] = []

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

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

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

442+ spreadHeads [] tails = tails

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

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

445445

446446--------------------------------------------------------------------------------

447447-- Membership tests

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

861861-- Properties

862862--------------------------------------------------------------------------------

863863

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

865+ uninhabited Refl impossible

866+

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

868+ uninhabited Refl impossible

869+

864870||| (::) is injective

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

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

rts/idris_heap.c+2

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

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

111111{

112112 char * mem = malloc(heap_size);

113+

113114 if (mem == NULL) {

114115 fprintf(stderr,

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

116117 heap_size);

117118 exit(EXIT_FAILURE);

118119 }

120+ memset(mem, 0, heap_size);

119121

120122 h->heap = mem;

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

rts/idris_rts.c−2

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

209209}

210210

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

212−// return malloc(isize);

213212 size_t size = aligned(isize);

214213

215214#ifdef HAS_PTHREAD

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

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

226225 vm->heap.next += size;

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

228− memset(ptr, 0, size);

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

230228

231229#ifdef HAS_PTHREAD

src/IRTS/Compiler.hs+1−1

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

533533

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

535535irSC 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

537537

538538irSC top vs (ProjCase tm alts) = do

539539 tm' <- irTerm top vs [] tm

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

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

202202 default2Text Nothing = ""

203203 default2Text (Just z) =

204204 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"]

206206jsStmt2Text (JsForever x) =

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

208208jsStmt2Text 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

660660 i <- getIState

661661 inf <- isTyInferred fname

662662

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

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

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

664+ when (not $ null withs) $

665665 ierror (At (fromMaybe NoFC $ highestFC lhs_in_as)

666666 (Elaborating "left hand side of " fname Nothing

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

667+ (Msg $ if isOutsideWith lhs_in

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

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

668670

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

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

265265

266266calculateHash :: IState -> IBCFile -> Int

267267calculateHash ist f

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

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

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

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

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

270271 where

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

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

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

276277 exported (_, Frozen) = True

277278 exported _ = False

278279

280+ inlinable acc (n, opts)

281+ = n `elem` acc &&

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

283+

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

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

281286

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

299304 Just ty -> ty : ts

300305 getDefs (_ : ns) = getDefs ns

301306

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+

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

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

304315-- everything is loaded.

src/Idris/Output.hs+4−3

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

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

7676formatMessage w = do

7777 i <- getIState

78− maybeSource <- case messageSource w of

79− Just src -> pure (Just src)

80− Nothing -> readSource fc

78+ rs <- readSource fc

79+ let maybeSource = case rs of

80+ Just src -> Just src

81+ Nothing -> messageSource w

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

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

8384 where

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

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

1313import Idris.Options (Opt)

1414import Idris.Package.Common

1515import Idris.Parser (moduleName)

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

17− lchar, packageName, parseErrorDoc, reserved,

18− runparser, someSpace, stringLiteral)

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

17+ identifierWithExtraChars, isEol, lchar,

18+ packageName, parseErrorDoc, reserved, runparser,

19+ someSpace, stringLiteral)

1920

2021import Control.Applicative

2122import Control.Monad.State.Strict

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

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

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

2829import qualified Text.Megaparsec as P

29−import qualified Text.Megaparsec.Char as P

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

3131

3232type PParser = Parser PkgDesc

3333

3434parseDesc :: FilePath -> IO PkgDesc

3535parseDesc fp = do

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

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

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

3838 exitWith (ExitFailure 1)

3939 res <- doesFileExist fp

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

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

120120 _ -> fail "Unexpected error"

121121

122+libIdentifier :: Parsing m => m String

123+libIdentifier = identifierWithExtraChars "_'-."

124+

122125pClause :: PParser ()

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

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

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

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

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

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

130133 , idris_opts = pkgs ++ idris_opts st })

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

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

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

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

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

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

144147 <|> 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,

6060import System.FilePath

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

6262import qualified Text.Megaparsec as P

63−import qualified Text.Megaparsec.Char as P

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

6564

6665{-

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

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

2020import Control.Applicative

2121import Control.Arrow (left)

2222import Control.Monad

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

2324import Control.Monad.State.Strict

2425import Data.Function (on)

2526import Data.List

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

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

2829import qualified Text.Megaparsec as P

2930import qualified Text.Megaparsec.Char as P

30−import qualified Text.Megaparsec.Expr as P

3131

3232-- | Allow implicit type declarations

3333allowImp :: SyntaxInfo -> SyntaxInfo

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

14061406 -}

14071407verbatimStringLiteral :: Parsing m => m String

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

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

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

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

14111411 return $ str ++ moreQuotes

14121412

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

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

3636 , iName

3737 , name

3838 , identifier

39+ , identifierWithExtraChars

3940 , packageName

4041 -- * Access

4142 , accessibility

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

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

270271 ]

271272

272−identifierOrReserved :: Parsing m => m String

273−identifierOrReserved = token $ P.try $ do

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

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

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

276277 return $ c : cs

277278

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

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

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

296297

297298-- | Parses an identifier as a token

298−identifier :: Parsing m => m String

299−identifier = P.try $ do

300− ident <- identifierOrReserved

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

300+identifierWithExtraChars extraChars = P.try $ do

301+ ident <- identifierOrReservedWithExtraChars extraChars

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

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

303304 return ident

304305

306+identifier :: Parsing m => m String

307+identifier = identifierWithExtraChars "_'."

308+

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

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

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

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

393397

394398-- | Gets current indentation

395399indent :: Parsing m => m Int

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

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

397401

398402-- | Gets last indentation

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

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

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

1717

1818import Control.Applicative

1919import Control.Monad

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

2021import Control.Monad.State.Strict

2122import Data.Char (isAlpha)

2223import Data.List

2324import Data.List.NonEmpty (fromList)

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

2526import qualified Text.Megaparsec as P

26−import qualified Text.Megaparsec.Char as P

27−import qualified Text.Megaparsec.Expr as P

2827

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

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

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

5858runparser p i inputname s =

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

60− Left err -> Left $ ParseError s err

60+ Left err -> Left $ ParseError err

6161 Right v -> Right $ fst v

6262

6363{- * Parse errors -}

6464

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

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

66+

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

6675

6776instance 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

6982 where

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

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

72− messageSource (ParseError src _) = Just src

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

7384

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

75−prettyError :: ParseError -> String

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

86+prettyError :: ParseError -> String

87+prettyError = P.errorBundlePretty . unParseError

7788

7889{- * Mark and restore -}

7990

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

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

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

106117getFC :: Parsing m => m FC

107−getFC = sourcePositionFC <$> P.getPosition

118+getFC = sourcePositionFC <$> P.getSourcePos

108119

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

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

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

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

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

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

3535import qualified Text.Megaparsec as P

36−import qualified Text.Megaparsec.Char as P

3736

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

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

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

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

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

7069 , (["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)

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

7372 , cmd_apropos)

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

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

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

199198 unrecognized = do

200199 IP.lchar ':'

201− cmd <- P.many P.anyChar

200+ cmd <- P.many P.anySingle

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

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

204203

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

260259fnNameArg = genArg "functionname" IP.fnName

261260

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

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

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

264263

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

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

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

342341

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

344343cmd_dynamic name = do

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

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

346345 if (l /= "")

347346 then return $ Right (DynamicLink l)

348347 else return $ Right ListDynamic

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

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

441440cmd_loadto name = do

442441 toline <- fromInteger <$> IP.natural

443− f <- P.many P.anyChar

442+ f <- P.many P.anySingle

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

445444

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

stack.yaml+5−2

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

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

2−resolver: lts-11.14

2+resolver: lts-12.21

44packages:

55 - location: .

7−extra-deps: []

7+extra-deps:

8+ - megaparsec-7.0.4

9+ - parser-combinators-1.0.0

10+

811

912flags:

1013 idris:

test/TestRun.hs+20−14

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

1111import Data.Typeable

1212import Options.Applicative

1313import System.Directory

14+import System.Environment

1415import System.Exit

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

1617import System.Info

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

103104 normalise (x : xs) = x : normalise xs

104105 normalise [] = []

105106

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+

106118main :: IO ()

107119main = do

108− nodePath <- findExecutable "node"

109− nodejsPath <- findExecutable "nodejs"

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 $

120+ args <- getArgs

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

122+ defaultMainWithIngredients ingredients $

117123 askOption $ \(NodeOpt node) ->

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

119− else (C , [])

120− in

121− mkGoldenTests (testFamiliesForCodegen codegen)

122− (flags ++ idrisFlags)

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

125+ else (C , [])

126+ in

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

128+

test/error006/WithPatsNoWith.idr+11

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

44foo 1 | 2 | 3 = True

55foo _ = False

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:

55When checking left hand side of foo:

66unexpected patterns outside of "with" block

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+