770a3a7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Display errors properly on IBC load failure

commit770a3a7d9ebf1270d4c5cd0628b438e700bb7a59 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Jan 2014, 01:39 (13 years ago) parent5d8f805

5 files changed+14−6

compare with master

unifiedsplit

CHANGELOG+6−1 src/Idris/Core/TT.hs+1−1 src/Idris/IBC.hs+2−1 src/Idris/Parser.hs+2−1 src/Idris/REPL.hs+3−2

CHANGELOG+6−1

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

11New in 0.9.11:

2−-------------

2+--------------

44* Agda-style equational reasoning (in Syntax.PreorderReasoning)

55* 'case' construct now abstracts over the scrutinee in its type

@@ -8,6 +8,11 @@ New in 0.9.11:

88 valid identifier. Two labels are definitionally equal if they have the

99 same name.

1010

11+Internal changes

12+

13+* Faster elaboration

14+* Smaller .ibc files

15+

1116New in 0.9.10:

1217--------------

1318

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

@@ -162,7 +162,7 @@ instance Show Err where

162162 ++ show e ++ " in " ++ show sc ++ " " ++ show i

163163 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

164164 show (ProviderError msg) = "Type provider error: " ++ msg

165− show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ show e

165+ show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e

166166 show ProgramLineComment = "Program line next to comment"

167167 show (At f e) = show f ++ ":" ++ show e

168168 show _ = "Error"

src/Idris/IBC.hs+2−1

@@ -8,6 +8,7 @@ import Idris.Core.CaseTree

88import Idris.AbsSyntax

99import Idris.Imports

1010import Idris.Error

11+import Idris.Delaborate

1112

1213import Data.Binary

1314import Data.Vector.Binary

@@ -79,7 +80,7 @@ writeIBC src f

7980 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

8081 runIO $ encodeFile f ibcf

8182 iLOG "Written")

82− (\c -> do iLOG $ "Failed " ++ show c)

83+ (\c -> do iLOG $ "Failed " ++ pshow i c)

8384 return ()

8485

8586mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

src/Idris/Parser.hs+2−1

@@ -21,6 +21,7 @@ import Text.PrettyPrint.ANSI.Leijen (Doc, plain)

2121import Idris.AbsSyntax

2222import Idris.DSL

2323import Idris.Imports

24+import Idris.Delaborate

2425import Idris.Error

2526import Idris.ElabDecls

2627import Idris.ElabTerm hiding (namespace, params)

@@ -1004,7 +1005,7 @@ loadModule' outh f

10041005 LIDR fn -> loadSource outh True fn

10051006 IBC fn src ->

10061007 idrisCatch (loadIBC fn)

1007− (\c -> do iLOG $ fn ++ " failed " ++ show c

1008+ (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

10081009 case src of

10091010 IDR sfn -> loadSource outh False sfn

10101011 LIDR sfn -> loadSource outh True sfn)

src/Idris/REPL.hs+3−2

@@ -1101,12 +1101,13 @@ loadInputs h inputs

11011101 when (not loadCode) $ tryLoad $ nub (concat ifiles)

11021102 _ -> return ()

11031103 putIState inew)

1104− (\e -> do case e of

1104+ (\e -> do i <- getIState

1105+ case e of

11051106 At f _ -> do setErrLine (fc_line f)

11061107 iputStrLn (show e)

11071108 ProgramLineComment -> return () -- fail elsewhere

11081109 _ -> do setErrLine 3 -- FIXME! Propagate it

1109− iputStrLn (show e))

1110+ iputStrLn (pshow i e))

11101111 where -- load all files, stop if any fail

11111112 tryLoad :: [IFileType] -> Idris ()

11121113 tryLoad [] = return ()