ac33945 · Idris-dev · git.iko.soy

src/Core/Execute.hs+2−2

compare with master

unifiedsplit

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

159execute :: Term -> Idris Term

160execute tm = do est <- initState

161 ctxt <- getContext

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

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

163− toTT res

163+ toTT res

164 case res of

165 Left err -> fail err

166 Right tm' -> return tm'

src/Core/TT.hs+4

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

21module Core.TT where

22

23import Control.Monad.State

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

24import Debug.Trace

25import Debug.Trace

25import qualified Data.Map as Map

26import qualified Data.Map as Map

26import Data.Char

27import Data.Char

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

133 pretty (ProviderError msg) = text msg

134 pretty (ProviderError msg) = text msg

134 pretty _ = text "Error"

135 pretty _ = text "Error"

135

136

137+instance Error Err where

138+ strMsg = Msg

139+

136data TC a = OK a

140data TC a = OK a

137 | Error Err

141 | Error Err

138 deriving (Eq, Functor)

142 deriving (Eq, Functor)

src/Idris/AbsSyntax.hs+1−1

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

60 case mapMaybe (findDyLib ls) libs of

61 x:_ -> return (Left x)

62 [] -> do

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

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

64 case msum handle of

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

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

src/Idris/AbsSyntaxTree.hs+2−1

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

20

21

22import Control.Monad.Trans.State.Strict

23+import Control.Monad.Trans.Error

23

24

24import Data.List

25import Data.List

25import Data.Char

26import Data.Char

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

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

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

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

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

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

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

190−type Idris = StateT IState IO

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

191

192

192-- Commands in the REPL

193-- Commands in the REPL

193

194

src/Idris/ElabDecls.hs+3−3

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

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

1468elabDecl what info d

1469 = idrisCatch (elabDecl' what info d)

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

1471− setErrLine (getErrLine msg)

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

1471+ ist <- getIState

1472− iputStrLn msg)

1472+ iputStrLn $ pshow ist e)

1473

1474elabDecl' _ info (PFix _ _ _)

1475 = return () -- nothing to elaborate

src/Idris/Error.hs+21−28

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

13import System.Console.Haskeline

14import System.Console.Haskeline.MonadException

15import Control.Monad.State

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

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

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

17import Data.Char

18import Data.Char

18import Data.Typeable

19import Data.Typeable

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

21iucheck = do tit <- typeInType

22iucheck = do tit <- typeInType

22 when (not tit) $

23 when (not tit) $

23 do ist <- getIState

24 do ist <- getIState

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

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

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

26− setErrLine (getErrLine msg)

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

27− iputStrLn msg)

27+ iputStrLn (pshow ist e))

28+

29+showErr :: Err -> Idris String

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

31+

28

32

29report :: IOError -> String

33report :: IOError -> String

30report e

34report e

31 | isUserError e = ioeGetErrorString e

35 | isUserError e = ioeGetErrorString e

32 | otherwise = show e

36 | otherwise = show e

33

37

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

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

35−idrisCatch = catch

39+--idrisCatch = catch

36

40

37−data IdrisErr = IErr String

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

38− deriving Typeable

42+idrisCatch = catchError

39

43

40−instance Show IdrisErr where

41− show (IErr s) = s

42−

43−instance Exception IdrisErr

44

45ifail :: String -> Idris ()

46−ifail str = throwIO (IErr str)

46+ifail = throwError . Msg

47

48ierror :: Err -> Idris a

49−ierror err = do i <- getIState

49+ierror = throwError

50− throwIO (IErr $ pshow i err)

51

50

52tclift :: TC a -> Idris a

51tclift :: TC a -> Idris a

53−tclift tc = case tc of

54− OK v -> return v

52+tclift (OK v) = return v

55− Error err -> do i <- getIState

56− case err of

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

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

58− _ -> return ()

54+tclift (Error err) = throwError err

59− throwIO (IErr $ pshow i err)

60

55

61tctry :: TC a -> TC a -> Idris a

56tctry :: TC a -> TC a -> Idris a

62tctry tc1 tc2

57tctry tc1 tc2

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

64 OK v -> return v

59 OK v -> return v

65 Error err -> tclift tc2

60 Error err -> tclift tc2

66

61

67−getErrLine str

62+getErrLine :: Err -> Int

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

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

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

64+getErrLine _ = 0

70− ([], _) -> 0

65+

71− (num, _) -> read num

72− _ -> 0

73

66

src/Idris/Parser.hs+5−4

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

941 LIDR sfn -> loadSource True sfn)

942 let (dir, fh) = splitFileName file

943 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

946 iputStrLn msg

947 iputStrLn msg

947 return "")

948 return "")

948

949

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

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

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

965loadSource' lidr r

966loadSource' lidr r

966 = idrisCatch (loadSource lidr r)

967 = 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

969 iputStrLn msg)

970 iputStrLn msg)

970

971

971{- | Load Idris source code-}

972{- | Load Idris source code-}

src/Idris/REPL.hs+10−5

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

56import System.Directory

57import System.IO

58import Control.Monad

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

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

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

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

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

61import Data.Maybe

62import Data.Maybe

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

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

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

251 return Nothing

252 return Nothing

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

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

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

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

254 return (Just inputs)

255 return (Just inputs)

255

256

256resolveProof :: Name -> Idris Name

257resolveProof :: Name -> Idris Name

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

541 _ -> iFail $ "Ambiguous name"

542 _ -> iFail $ "Ambiguous name"

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

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

543 let lib = trim l

544 let lib = trim l

544− handle <- lift $ tryLoadLib lib

545+ handle <- lift . lift $ tryLoadLib lib

545 case handle of

546 case handle of

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

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

547 Just x -> do let libs = idris_dynamic_libs i

548 Just x -> do let libs = idris_dynamic_libs i

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

686 }

687 }

687

688

688-- invoke as if from command line

689-- invoke as if from command line

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

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

690−idris opts = execStateT (idrisMain opts) idrisInit

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+

691

696

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

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

693loadInputs inputs

698loadInputs inputs

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

888 liftIO $ hClose h)

893 liftIO $ hClose h)

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

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

890 where runInit :: Handle -> Idris ()

895 where runInit :: Handle -> Idris ()

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

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

892 ist <- getIState

897 ist <- getIState

893 unless eof $ do

898 unless eof $ do

894 line <- liftIO $ hGetLine h

899 line <- liftIO $ hGetLine h

src/Main.hs+2−1

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

8

9import Data.Maybe

10import Data.Version

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

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

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

12import Control.Monad.Trans ( liftIO )

13import Control.Monad.Trans ( liftIO )

13import Control.Monad ( when )

14import Control.Monad ( when )

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

40

41

41main = do xs <- getArgs

42main = do xs <- getArgs

42 let opts = parseArgs xs

43 let opts = parseArgs xs

43− execStateT (runIdris opts) idrisInit

44+ runErrorT $ execStateT (runIdris opts) idrisInit

44

45

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

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

46runIdris opts = do

47runIdris opts = do

src/Pkg/Package.hs+1−1

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

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

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

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

73− idris (map Filename f ++ opts)

73+ idris (map Filename f ++ opts)

74 return ()

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

76