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

CHANGELOG+6−1

compare with master

unifiedsplit

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

1New in 0.9.11:

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

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

3

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

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

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

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

9 same name.

10

11+Internal changes

12+

13+* Faster elaboration

14+* Smaller .ibc files

15+

11New in 0.9.10:

16New in 0.9.10:

12--------------

17--------------

13

18

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

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

162 ++ show e ++ " in " ++ show sc ++ " " ++ show i

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

164 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

166 show ProgramLineComment = "Program line next to comment"

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

168 show _ = "Error"

src/Idris/IBC.hs+2−1

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

8import Idris.AbsSyntax

9import Idris.Imports

10import Idris.Error

11+import Idris.Delaborate

11

12

12import Data.Binary

13import Data.Binary

13import Data.Vector.Binary

14import Data.Vector.Binary

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

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

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

80 runIO $ encodeFile f ibcf

81 runIO $ encodeFile f ibcf

81 iLOG "Written")

82 iLOG "Written")

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

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

83 return ()

84 return ()

84

85

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

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

src/Idris/Parser.hs+2−1

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

21import Idris.AbsSyntax

22import Idris.DSL

23import Idris.Imports

24+import Idris.Delaborate

24import Idris.Error

25import Idris.Error

25import Idris.ElabDecls

26import Idris.ElabDecls

26import Idris.ElabTerm hiding (namespace, params)

27import Idris.ElabTerm hiding (namespace, params)

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

1004 LIDR fn -> loadSource outh True fn

1005 LIDR fn -> loadSource outh True fn

1005 IBC fn src ->

1006 IBC fn src ->

1006 idrisCatch (loadIBC fn)

1007 idrisCatch (loadIBC fn)

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

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

1008 case src of

1009 case src of

1009 IDR sfn -> loadSource outh False sfn

1010 IDR sfn -> loadSource outh False sfn

1010 LIDR sfn -> loadSource outh True sfn)

1011 LIDR sfn -> loadSource outh True sfn)

src/Idris/REPL.hs+3−2

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

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

1102 _ -> return ()

1103 putIState inew)

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

1104− (\e -> do case e of

1105+ case e of

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

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

1106 iputStrLn (show e)

1107 iputStrLn (show e)

1107 ProgramLineComment -> return () -- fail elsewhere

1108 ProgramLineComment -> return () -- fail elsewhere

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

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

1109− iputStrLn (show e))

1110+ iputStrLn (pshow i e))

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

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

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

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

1112 tryLoad [] = return ()

1113 tryLoad [] = return ()