ac33945 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Wrap Idris in an ErrorT

This is the first step in getting error reflection to work. The next is to centralize the error handlers.

commitac339455a8d756fd044874fa907e5aff2e238e16 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 14 Oct 2013, 18:09 (13 years ago) parent3544af3

10 files changed+51−46

compare with master

unifiedsplit

src/Core/Execute.hs+2−2 src/Core/TT.hs+4 src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/ElabDecls.hs+3−3 src/Idris/Error.hs+21−28 src/Idris/Parser.hs+5−4 src/Idris/REPL.hs+10−5 src/Main.hs+2−1 src/Pkg/Package.hs+1−1

src/Core/Execute.hs+2−2

@@ -159,8 +159,8 @@ debugThunks = do st <- getExecState

159159execute :: Term -> Idris Term

160160execute tm = do est <- initState

161161 ctxt <- getContext

162− res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

163− toTT res

162+ res <- lift . lift $ flip runExec est $ do res <- doExec [] ctxt tm

163+ toTT res

164164 case res of

165165 Left err -> fail err

166166 Right tm' -> return tm'

src/Core/TT.hs+4

@@ -21,6 +21,7 @@

2121module Core.TT where

2222

2323import Control.Monad.State

24+import Control.Monad.Trans.Error (Error(..))

2425import Debug.Trace

2526import qualified Data.Map as Map

2627import Data.Char

@@ -133,6 +134,9 @@ instance Pretty Err where

133134 pretty (ProviderError msg) = text msg

134135 pretty _ = text "Error"

135136

137+instance Error Err where

138+ strMsg = Msg

139+

136140data TC a = OK a

137141 | Error Err

138142 deriving (Eq, Functor)

src/Idris/AbsSyntax.hs+1−1

@@ -60,7 +60,7 @@ addDyLib libs = do i <- getIState

6060 case mapMaybe (findDyLib ls) libs of

6161 x:_ -> return (Left x)

6262 [] -> do

63− handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

63+ handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

6464 case msum handle of

6565 Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

6666 concat (intersperse "," libs) ++ "\"")

src/Idris/AbsSyntaxTree.hs+2−1

@@ -20,6 +20,7 @@ import System.Console.Haskeline

2020

2121

2222import Control.Monad.Trans.State.Strict

23+import Control.Monad.Trans.Error

2324

2425import Data.List

2526import Data.Char

@@ -187,7 +188,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

187188-- | The monad for the main REPL - reading and processing files and updating

188189-- global state (hence the IO inner monad).

189190--type Idris = WriterT [Either String (IO ())] (State IState a))

190−type Idris = StateT IState IO

191+type Idris = StateT IState (ErrorT Err IO)

191192

192193-- Commands in the REPL

193194

src/Idris/ElabDecls.hs+3−3

@@ -1467,9 +1467,9 @@ elabDecls info ds = do mapM_ (elabDecl EAll info) ds

14671467elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

14681468elabDecl what info d

14691469 = idrisCatch (elabDecl' what info d)

1470− (\e -> do let msg = show e

1471− setErrLine (getErrLine msg)

1472− iputStrLn msg)

1470+ (\e -> do setErrLine (getErrLine e)

1471+ ist <- getIState

1472+ iputStrLn $ pshow ist e)

14731473

14741474elabDecl' _ info (PFix _ _ _)

14751475 = return () -- nothing to elaborate

src/Idris/Error.hs+21−28

@@ -13,6 +13,7 @@ import Core.Constraints

1313import System.Console.Haskeline

1414import System.Console.Haskeline.MonadException

1515import Control.Monad.State

16+import Control.Monad.Error (throwError, catchError)

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

1718import Data.Char

1819import Data.Typeable

@@ -21,42 +22,36 @@ iucheck :: Idris ()

2122iucheck = do tit <- typeInType

2223 when (not tit) $

2324 do ist <- getIState

24− idrisCatch (tclift $ ucheck (idris_constraints ist))

25− (\e -> do let msg = show e

26− setErrLine (getErrLine msg)

27− iputStrLn msg)

25+ (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

26+ (\e -> do setErrLine (getErrLine e)

27+ iputStrLn (pshow ist e))

28+

29+showErr :: Err -> Idris String

30+showErr e = getIState >>= return . flip pshow e

31+

2832

2933report :: IOError -> String

3034report e

3135 | isUserError e = ioeGetErrorString e

3236 | otherwise = show e

3337

34−idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

35−idrisCatch = catch

38+--idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a

39+--idrisCatch = catch

3640

37−data IdrisErr = IErr String

38− deriving Typeable

41+idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a

42+idrisCatch = catchError

3943

40−instance Show IdrisErr where

41− show (IErr s) = s

42−

43−instance Exception IdrisErr

4444

4545ifail :: String -> Idris ()

46−ifail str = throwIO (IErr str)

46+ifail = throwError . Msg

4747

4848ierror :: Err -> Idris a

49−ierror err = do i <- getIState

50− throwIO (IErr $ pshow i err)

49+ierror = throwError

5150

5251tclift :: TC a -> Idris a

53−tclift tc = case tc of

54− OK v -> return v

55− Error err -> do i <- getIState

56− case err of

57− At (FC f l) e -> setErrLine l

58− _ -> return ()

59− throwIO (IErr $ pshow i err)

52+tclift (OK v) = return v

53+tclift (Error err@(At (FC f l) e)) = do setErrLine l ; throwError err

54+tclift (Error err) = throwError err

6055

6156tctry :: TC a -> TC a -> Idris a

6257tctry tc1 tc2

@@ -64,10 +59,8 @@ tctry tc1 tc2

6459 OK v -> return v

6560 Error err -> tclift tc2

6661

67−getErrLine str

68− = case span (/=':') str of

69− (_, ':':rest) -> case span isDigit rest of

70− ([], _) -> 0

71− (num, _) -> read num

72− _ -> 0

62+getErrLine :: Err -> Int

63+getErrLine (At (FC _ l) _) = l

64+getErrLine _ = 0

65+

7366

src/Idris/Parser.hs+5−4

@@ -941,8 +941,9 @@ loadModule f

941941 LIDR sfn -> loadSource True sfn)

942942 let (dir, fh) = splitFileName file

943943 return (dropExtension fh))

944− (\e -> do let msg = show e

945− setErrLine (getErrLine msg)

944+ (\e -> do setErrLine (getErrLine e)

945+ ist <- getIState

946+ msg <- showErr e

946947 iputStrLn msg

947948 return "")

948949

@@ -964,8 +965,8 @@ loadFromIFile (LIDR fn) = loadSource' True fn

964965loadSource' :: Bool -> FilePath -> Idris ()

965966loadSource' lidr r

966967 = idrisCatch (loadSource lidr r)

967− (\e -> do let msg = show e

968− setErrLine (getErrLine msg)

968+ (\e -> do setErrLine (getErrLine e)

969+ msg <- showErr e

969970 iputStrLn msg)

970971

971972{- | Load Idris source code-}

src/Idris/REPL.hs+10−5

@@ -56,6 +56,7 @@ import System.Process

5656import System.Directory

5757import System.IO

5858import Control.Monad

59+import Control.Monad.Trans.Error (ErrorT(..))

5960import Control.Monad.Trans.State.Strict ( StateT, execStateT, get, put )

6061import Control.Monad.Trans ( liftIO, lift )

6162import Data.Maybe

@@ -250,7 +251,7 @@ processInput cmd orig inputs

250251 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

251252 return Nothing

252253 Success cmd -> do idrisCatch (process fn cmd)

253− (\e -> iputStrLn (show e))

254+ (\e -> do msg <- showErr e ; iputStrLn msg)

254255 return (Just inputs)

255256

256257resolveProof :: Name -> Idris Name

@@ -541,7 +542,7 @@ process fn (Missing n)

541542 _ -> iFail $ "Ambiguous name"

542543process fn (DynamicLink l) = do i <- getIState

543544 let lib = trim l

544− handle <- lift $ tryLoadLib lib

545+ handle <- lift . lift $ tryLoadLib lib

545546 case handle of

546547 Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""

547548 Just x -> do let libs = idris_dynamic_libs i

@@ -686,8 +687,12 @@ replSettings hFile = setComplete replCompletion $ defaultSettings {

686687 }

687688

688689-- invoke as if from command line

689−idris :: [Opt] -> IO IState

690−idris opts = execStateT (idrisMain opts) idrisInit

690+idris :: [Opt] -> IO ()

691+idris opts = do res <- runErrorT $ execStateT (idrisMain opts) idrisInit

692+ case res of

693+ Left err -> putStrLn $ pshow idrisInit err

694+ Right ist -> return ()

695+

691696

692697loadInputs :: [FilePath] -> Idris ()

693698loadInputs inputs

@@ -888,7 +893,7 @@ initScript = do script <- getInitScript

888893 liftIO $ hClose h)

889894 (\e -> iFail $ "Error reading init file: " ++ show e)

890895 where runInit :: Handle -> Idris ()

891− runInit h = do eof <- lift (hIsEOF h)

896+ runInit h = do eof <- lift . lift $ hIsEOF h

892897 ist <- getIState

893898 unless eof $ do

894899 line <- liftIO $ hGetLine h

src/Main.hs+2−1

@@ -8,6 +8,7 @@ import System.FilePath ((</>), addTrailingPathSeparator)

99import Data.Maybe

1010import Data.Version

11+import Control.Monad.Trans.Error ( ErrorT(..) )

1112import Control.Monad.Trans.State.Strict ( execStateT, get, put )

1213import Control.Monad.Trans ( liftIO )

1314import Control.Monad ( when )

@@ -40,7 +41,7 @@ import Paths_idris

4041

4142main = do xs <- getArgs

4243 let opts = parseArgs xs

43− execStateT (runIdris opts) idrisInit

44+ runErrorT $ execStateT (runIdris opts) idrisInit

4445

4546runIdris :: [Opt] -> Idris ()

4647runIdris opts = do

src/Pkg/Package.hs+1−1

@@ -70,7 +70,7 @@ installPkg pkgdesc

7070buildMods :: [Opt] -> [Name] -> IO ()

7171buildMods opts ns = do let f = map (toPath . show) ns

7272-- putStrLn $ "MODULE: " ++ show f

73− idris (map Filename f ++ opts)

73+ idris (map Filename f ++ opts)

7474 return ()

7575 where toPath n = foldl1' (</>) $ splitOn "." n

7676