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

git.iko.soy/Idris-dev

Fix error recovery in repl

commit4ca34ff8764a0c0b1c06846310a6ac883cca8efd authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 20:16 (15 years ago) parent49e426a

6 files changed+28−13

compare with master

unifiedsplit

src/Idris/ElabDecls.hs+1−1 src/Idris/Error.hs+14−3 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+10−7 tutorial/examples/Makefile+1

src/Idris/ElabDecls.hs+1−1

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

553553

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

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

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

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

557557 setErrLine (getErrLine msg)

558558 iputStrLn msg)

559559

src/Idris/Error.hs+14−3

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

1+{-# LANGUAGE DeriveDataTypeable #-}

13module Idris.Error where

35import Prelude hiding (catch)

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

1214import Control.Monad.State

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

1416import Data.Char

17+import Data.Typeable

1518

1619iucheck :: Idris ()

1720iucheck = do tit <- typeInType

1821 when (not tit) $

1922 do ist <- get

2023 idrisCatch (tclift $ ucheck (idris_constraints ist))

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

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

2225 setErrLine (getErrLine msg)

2326 iputStrLn msg)

2427

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

2730 | isUserError e = ioeGetErrorString e

2831 | otherwise = show e

2932

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

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

3134idrisCatch = catch

3235

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+

3344tclift :: TC a -> Idris a

3445tclift tc = case tc of

3546 OK v -> return v

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

3748 case err of

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

3950 _ -> return ()

40− fail (pshow i err)

51+ throwIO (IErr $ pshow i err)

4152

4253getErrLine str

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

src/Idris/Parser.hs+1−1

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

7070 LIDR sfn -> loadSource True sfn)

7171 let (dir, fh) = splitFileName f

7272 return (dropExtension fh))

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

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

7474 setErrLine (getErrLine msg)

7575 iputStrLn msg

7676 return "")

src/Idris/Prover.hs+1−1

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

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

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

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

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

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

110110 return (False, e, False, prf))

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

112112 return (tm, prf')

src/Idris/REPL.hs+10−7

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

1919import Core.TT

2020import Core.Constraints

2121

22−import System.Console.Haskeline

22+import System.Console.Haskeline as H

2323import System.FilePath

2424import System.Environment

2525import System.Process

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

3737 case x of

3838 Nothing -> do iputStrLn "Bye bye"

3939 return ()

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

41− case ms of

42− Just mods -> repl orig mods

43− Nothing -> return ()

40+ Just input -> idrisCatch

41+ (do ms <- processInput input orig mods

42+ case ms of

43+ Just mods -> repl orig mods

44+ Nothing -> return ())

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

46+ repl orig mods)

4447

4548mkPrompt [] = "Idris"

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

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

6265 Right Edit -> do edit fn orig

6366 return (Just inputs)

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

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

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

6669 return (Just inputs)

6770 Right Quit -> do iputStrLn "Bye bye"

6871 return Nothing

6972 Right cmd -> do idrisCatch (process cmd)

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

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

7174 return (Just inputs)

7275

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

tutorial/examples/Makefile+1

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

11check: .PHONY

2+ rm *.ibc

23 for x in *.idr ; do \

34 echo "Checking $$x"; \

45 idris --check $$x; \