4ca34ff · Idris-dev · git.iko.soy

src/Idris/ElabDecls.hs+1−1

compare with master

unifiedsplit

@@ -553,7 +553,7 @@ pvars ist _ = []

553

554elabDecl :: ElabInfo -> PDecl -> Idris ()

555elabDecl info d = idrisCatch (elabDecl' info d)

556− (\e -> do let msg = report e

556+ (\e -> do let msg = show e

557 setErrLine (getErrLine msg)

558 iputStrLn msg)

559

src/Idris/Error.hs+14−3

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

1+{-# LANGUAGE DeriveDataTypeable #-}

2+

1module Idris.Error where

3module Idris.Error where

2

4

3import Prelude hiding (catch)

5import Prelude hiding (catch)

@@ -12,13 +14,14 @@ import System.Console.Haskeline

12import Control.Monad.State

14import Control.Monad.State

13import System.IO.Error(isUserError, ioeGetErrorString)

15import System.IO.Error(isUserError, ioeGetErrorString)

14import Data.Char

16import Data.Char

17+import Data.Typeable

15

18

16iucheck :: Idris ()

19iucheck :: Idris ()

17iucheck = do tit <- typeInType

20iucheck = do tit <- typeInType

18 when (not tit) $

21 when (not tit) $

19 do ist <- get

22 do ist <- get

20 idrisCatch (tclift $ ucheck (idris_constraints ist))

23 idrisCatch (tclift $ ucheck (idris_constraints ist))

21− (\e -> do let msg = report e

24+ (\e -> do let msg = show e

22 setErrLine (getErrLine msg)

25 setErrLine (getErrLine msg)

23 iputStrLn msg)

26 iputStrLn msg)

24

27

@@ -27,9 +30,17 @@ report e

27 | isUserError e = ioeGetErrorString e

30 | isUserError e = ioeGetErrorString e

28 | otherwise = show e

31 | otherwise = show e

29

32

30−idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a

33+idrisCatch :: Idris a -> (IdrisErr -> Idris a) -> Idris a

31idrisCatch = catch

34idrisCatch = catch

32

35

36+data IdrisErr = IErr String

37+ deriving Typeable

38+

39+instance Show IdrisErr where

40+ show (IErr s) = s

41+

42+instance Exception IdrisErr

43+

33tclift :: TC a -> Idris a

44tclift :: TC a -> Idris a

34tclift tc = case tc of

45tclift tc = case tc of

35 OK v -> return v

46 OK v -> return v

@@ -37,7 +48,7 @@ tclift tc = case tc of

37 case err of

48 case err of

38 At (FC f l) e -> setErrLine l

49 At (FC f l) e -> setErrLine l

39 _ -> return ()

50 _ -> return ()

40− fail (pshow i err)

51+ throwIO (IErr $ pshow i err)

41

52

42getErrLine str

53getErrLine str

43 = case span (/=':') str of

54 = case span (/=':') str of

src/Idris/Parser.hs+1−1

@@ -70,7 +70,7 @@ loadModule f

70 LIDR sfn -> loadSource True sfn)

71 let (dir, fh) = splitFileName f

72 return (dropExtension fh))

73− (\e -> do let msg = report e

73+ (\e -> do let msg = show e

74 setErrLine (getErrLine msg)

75 iputStrLn msg

76 return "")

src/Idris/Prover.hs+1−1

@@ -106,7 +106,7 @@ ploop d prompt prf e

106 Right tac -> do (_, e) <- elabStep e saveState

107 (_, st) <- elabStep e (runTac True i tac)

108 return (True, st, False, prf ++ [step]))

109− (\err -> do iputStrLn (report err)

109+ (\err -> do iputStrLn (show err)

110 return (False, e, False, prf))

111 if done then do (tm, _) <- elabStep st get_term

112 return (tm, prf')

src/Idris/REPL.hs+10−7

@@ -19,7 +19,7 @@ import Core.ProofShell

19import Core.TT

20import Core.Constraints

21

22−import System.Console.Haskeline

22+import System.Console.Haskeline as H

23import System.FilePath

24import System.Environment

25import System.Process

@@ -37,10 +37,13 @@ repl orig mods

37 case x of

38 Nothing -> do iputStrLn "Bye bye"

39 return ()

40+ Just input -> idrisCatch

40− Just input -> do ms <- processInput input orig mods

41+ (do ms <- processInput input orig mods

41− case ms of

42+ case ms of

42− Just mods -> repl orig mods

43+ Just mods -> repl orig mods

43− Nothing -> return ()

44+ Nothing -> return ())

45+ (\e -> do iputStrLn (show e)

46+ repl orig mods)

44

47

45mkPrompt [] = "Idris"

48mkPrompt [] = "Idris"

46mkPrompt [x] = "*" ++ dropExtension x

49mkPrompt [x] = "*" ++ dropExtension x

@@ -62,12 +65,12 @@ processInput cmd orig inputs

62 Right Edit -> do edit fn orig

65 Right Edit -> do edit fn orig

63 return (Just inputs)

66 return (Just inputs)

64 Right AddProof -> do idrisCatch (addProof fn orig)

67 Right AddProof -> do idrisCatch (addProof fn orig)

65− (\e -> iputStrLn (report e))

68+ (\e -> iputStrLn (show e))

66 return (Just inputs)

69 return (Just inputs)

67 Right Quit -> do iputStrLn "Bye bye"

70 Right Quit -> do iputStrLn "Bye bye"

68 return Nothing

71 return Nothing

69 Right cmd -> do idrisCatch (process cmd)

72 Right cmd -> do idrisCatch (process cmd)

70− (\e -> iputStrLn (report e))

73+ (\e -> iputStrLn (show e))

71 return (Just inputs)

74 return (Just inputs)

72

75

73edit :: FilePath -> IState -> Idris ()

76edit :: FilePath -> IState -> Idris ()

tutorial/examples/Makefile+1

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

1check: .PHONY

2+ rm *.ibc

2 for x in *.idr ; do \

3 for x in *.idr ; do \

3 echo "Checking $$x"; \

4 echo "Checking $$x"; \

4 idris --check $$x; \

5 idris --check $$x; \