a09a1bf · Idris-dev · git.iko.soy

.travis.yml+8

@@ -10,8 +10,10 @@ addons:

1010 - ghc-7.6.3

1111 - ghc-7.8.4

1212 - ghc-7.10.2

13+ - ghc-8.0.1

1314 - cabal-install-1.20

1415 - cabal-install-1.22

16+ - cabal-install-1.24

1517 # test dependencies

1618 - expect

1719 - cppcheck

@@ -35,6 +37,12 @@ matrix:

3537 compiler: ": #GHC 7.10.2"

3638 - env: CABALVER="1.22" GHCVER="7.10.2" TESTS="test_c"

3739 compiler: ": #GHC 7.10.2"

40+ - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="lib_doc doc"

41+ compiler: ": #GHC 8.0.1"

42+ - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_js"

43+ compiler: ": #GHC 8.0.1"

44+ - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"

45+ compiler: ": #GHC 8.0.1"

3846

3947cache:

4048 directories:

idris.cabal+5−5

@@ -1027,7 +1027,7 @@ Library

10271027 , ansi-terminal < 0.7

10281028 , ansi-wl-pprint < 0.7

10291029 , base64-bytestring < 1.1

1030− , binary >= 0.7 && < 0.8

1030+ , binary >= 0.7 && < 0.9

10311031 , blaze-html >= 0.6.1.3 && < 0.9

10321032 , blaze-markup >= 0.5.2.1 && < 0.8

10331033 , bytestring < 0.11

@@ -1044,14 +1044,14 @@ Library

10441044 , optparse-applicative >= 0.11 && < 0.13

10451045 , parsers >= 0.9 && < 0.13

10461046 , pretty < 1.2

1047− , process < 1.3

1047+ , process < 1.5

10481048 , split < 0.3

10491049 , terminal-size < 0.4

10501050 , text >=1.2.1.0 && < 1.3

1051− , time >= 1.4 && < 1.6

1052− , transformers < 0.5

1051+ , time >= 1.4 && < 1.7

1052+ , transformers < 0.6

10531053 , transformers-compat >= 0.3

1054− , trifecta >= 1.1 && < 1.6

1054+ , trifecta >= 1.6 && < 1.7

10551055 , uniplate >=1.6 && < 1.7

10561056 , unordered-containers < 0.3

10571057 , utf8-string < 1.1

src/Idris/Parser.hs+2−2

@@ -1569,7 +1569,7 @@ parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [Im

15691569parseImports fname input

15701570 = do i <- getIState

15711571 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

1572− Failure err -> fail (show err)

1572+ Failure (ErrInfo err _) -> fail (show err)

15731573 Success (x, annots, i) ->

15741574 do putIState i

15751575 fname' <- runIO $ Dir.makeAbsolute fname

@@ -1631,7 +1631,7 @@ parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->

16311631parseProg syn fname input mrk

16321632 = do i <- getIState

16331633 case runparser mainProg i fname input of

1634− Failure doc -> do -- FIXME: Get error location from trifecta

1634+ Failure (ErrInfo doc _) -> do -- FIXME: Get error location from trifecta

16351635 -- this can't be the solution!

16361636 -- Issue #1575 on the issue tracker.

16371637 -- https://github.com/idris-lang/Idris-dev/issues/1575

src/Idris/Parser/Helpers.hs+15

@@ -58,6 +58,21 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

5858

5959deriving instance Parsing IdrisInnerParser

6060

61+#if MIN_VERSION_base(4,9,0)

62+instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where

63+ line = lift line

64+ {-# INLINE line #-}

65+ position = lift position

66+ {-# INLINE position #-}

67+ slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

68+ {-# INLINE slicedWith #-}

69+ rend = lift rend

70+ {-# INLINE rend #-}

71+ restOfLine = lift restOfLine

72+ {-# INLINE restOfLine #-}

73+

74+#endif

75+

6176#if MIN_VERSION_base(4,8,0)

6277instance {-# OVERLAPPING #-} TokenParsing IdrisParser where

6378#else

src/Idris/Prover.hs+3−3

@@ -39,7 +39,7 @@ import qualified Idris.IdeMode as IdeMode

3939import Idris.Output

4040import Idris.TypeSearch (searchByType)

4141

42−import Text.Trifecta.Result(Result(..))

42+import Text.Trifecta.Result(Result(..), ErrInfo(..))

4343

4444import System.IO (Handle, stdin, stdout, hPutStrLn)

4545import System.Console.Haskeline

@@ -325,7 +325,7 @@ elabloop info fn d prompt prf e prev h env

325325 (d, prev', st, done, prf', env', res) <-

326326 idrisCatch

327327 (case cmd of

328− Failure err ->

328+ Failure (ErrInfo err _) ->

329329 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)

330330 Success (Left cmd') ->

331331 case cmd' of

@@ -440,7 +440,7 @@ ploop fn d prompt prf e h

440440 _ -> return ()

441441 (d, st, done, prf', res) <- idrisCatch

442442 (case cmd of

443− Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

443+ Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)

444444 Success Undo -> do (_, st) <- elabStep e loadState

445445 return (True, st, False, init prf, Right $ iPrintResult "")

446446 Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")

src/Idris/REPL.hs+10−10

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

8080import Data.List (groupBy)

8181import qualified Data.Text as T

8282

83−import Text.Trifecta.Result(Result(..))

83+import Text.Trifecta.Result(Result(..), ErrInfo(..))

8484

8585import System.Console.Haskeline as H

8686import System.FilePath

@@ -190,7 +190,7 @@ processNetCmd :: IState -> IState -> Handle -> FilePath -> String ->

190190 IO (IState, FilePath)

191191processNetCmd orig i h fn cmd

192192 = do res <- case parseCmd i "(net)" cmd of

193− Failure err -> return (Left (Msg " invalid command"))

193+ Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))

194194 Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i

195195 Success (Left err) -> return (Left (Msg err))

196196 case res of

@@ -307,7 +307,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

307307 do c <- colourise

308308 i <- getIState

309309 case parseCmd i "(input)" cmd of

310− Failure err -> iPrintError $ show (fixColour False err)

310+ Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)

311311 Success (Right (Prove mode n')) ->

312312 idrisCatch

313313 (do process fn (Prove mode n')

@@ -722,8 +722,8 @@ processInput cmd orig inputs efile

722722 let fn = fromMaybe "" (listToMaybe inputs)

723723 c <- colourise

724724 case parseCmd i "(input)" cmd of

725− Failure err -> do iputStrLn $ show (fixColour c err)

726− return (Just inputs)

725+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

726+ return (Just inputs)

727727 Success (Right Reload) ->

728728 reload orig inputs

729729 Success (Right Watch) ->

@@ -1787,8 +1787,8 @@ idrisMain opts =

17871787 mapM_ (\str -> do ist <- getIState

17881788 c <- colourise

17891789 case parseExpr ist str of

1790− Failure err -> do iputStrLn $ show (fixColour c err)

1791− runIO $ exitWith (ExitFailure 1)

1790+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

1791+ runIO $ exitWith (ExitFailure 1)

17921792 Success e -> process "" (Eval e))

17931793 exprs

17941794 runIO exitSuccess

@@ -1843,8 +1843,8 @@ execScript :: String -> Idris ()

18431843execScript expr = do i <- getIState

18441844 c <- colourise

18451845 case parseExpr i expr of

1846− Failure err -> do iputStrLn $ show (fixColour c err)

1847− runIO $ exitWith (ExitFailure 1)

1846+ Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)

1847+ runIO $ exitWith (ExitFailure 1)

18481848 Success term -> do ctxt <- getContext

18491849 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

18501850 res <- execute tm

@@ -1879,7 +1879,7 @@ initScript = do script <- getInitScript

18791879 runInit h

18801880 processLine i cmd input clr =

18811881 case parseCmd i input cmd of

1882− Failure err -> runIO $ print (fixColour clr err)

1882+ Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)

18831883 Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"

18841884 Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"

18851885 Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"

src/Pkg/PParser.hs+15−1

@@ -59,6 +59,20 @@ defaultPkg = PkgDesc "" Nothing Nothing Nothing Nothing

5959instance HasLastTokenSpan PParser where

6060 getLastTokenSpan = return Nothing

6161

62+#if MIN_VERSION_base(4,9,0)

63+instance {-# OVERLAPPING #-} DeltaParsing PParser where

64+ line = lift line

65+ {-# INLINE line #-}

66+ position = lift position

67+ {-# INLINE position #-}

68+ slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s

69+ {-# INLINE slicedWith #-}

70+ rend = lift rend

71+ {-# INLINE rend #-}

72+ restOfLine = lift restOfLine

73+ {-# INLINE restOfLine #-}

74+#endif

75+

6276#if MIN_VERSION_base(4,8,0)

6377instance {-# OVERLAPPING #-} TokenParsing PParser where

6478#else

@@ -71,7 +85,7 @@ parseDesc :: FilePath -> IO PkgDesc

7185parseDesc fp = do

7286 p <- readFile fp

7387 case runparser pPkg defaultPkg fp p of

74− Failure err -> fail (show $ PP.plain err)

88+ Failure (ErrInfo err _) -> fail (show $ PP.plain err)

7589 Success x -> return x

7690

7791pPkg :: PParser PkgDesc

stack.yaml+3−2

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

1−resolver: lts-6.4

1+resolver: lts-6.5

22

33packages:

4− - '.'

4+ - location: .

55

66flags:

77 idris:

@@ -10,6 +10,7 @@ flags:

1010

1111extra-deps:

1212 - libffi-0.1

13+ - trifecta-1.6

1314

1415nix:

1516 enable: false