git.iko.soy/Idris-dev
on 35ec145 help sign in
Idris-dev/src/Idris/Error.hs
63 lines 1.6 kB history raw
1{-# LANGUAGE DeriveDataTypeable #-}
3module Idris.Error where
5import Prelude hiding (catch)
6import Idris.AbsSyntax
7import Idris.Delaborate
9import Core.TT
10import Core.Typecheck
11import Core.Constraints
13import System.Console.Haskeline
14import System.Console.Haskeline.MonadException
15import Control.Monad.State
16import System.IO.Error(isUserError, ioeGetErrorString)
17import Data.Char
18import Data.Typeable
20iucheck :: Idris ()
21iucheck = do tit <- typeInType
22 when (not tit) $
23 do ist <- get
24 idrisCatch (tclift $ ucheck (idris_constraints ist))
25 (\e -> do let msg = show e
26 setErrLine (getErrLine msg)
27 iputStrLn msg)
29report :: IOError -> String
30report e
31 | isUserError e = ioeGetErrorString e
32 | otherwise = show e
34idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a
35idrisCatch = catch
37data IdrisErr = IErr String
38 deriving Typeable
40instance Show IdrisErr where
41 show (IErr s) = s
43instance Exception IdrisErr
45ifail :: String -> Idris ()
46ifail str = throwIO (IErr str)
48tclift :: TC a -> Idris a
49tclift tc = case tc of
50 OK v -> return v
51 Error err -> do i <- get
52 case err of
53 At (FC f l) e -> setErrLine l
54 _ -> return ()
55 throwIO (IErr $ pshow i err)
57getErrLine str
58 = case span (/=':') str of
59 (_, ':':rest) -> case span isDigit rest of
60 ([], _) -> 0
61 (num, _) -> read num
62 _ -> 0