git.iko.soy/Idris-dev
on 08797ae help sign in
Idris-dev/src/Idris/Error.hs
62 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 Control.Monad.State
15import System.IO.Error(isUserError, ioeGetErrorString)
16import Data.Char
17import Data.Typeable
19iucheck :: Idris ()
20iucheck = do tit <- typeInType
21 when (not tit) $
22 do ist <- get
23 idrisCatch (tclift $ ucheck (idris_constraints ist))
24 (\e -> do let msg = show e
25 setErrLine (getErrLine msg)
26 iputStrLn msg)
28report :: IOError -> String
29report e
30 | isUserError e = ioeGetErrorString e
31 | otherwise = show e
33idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a
34idrisCatch = catch
36data IdrisErr = IErr String
37 deriving Typeable
39instance Show IdrisErr where
40 show (IErr s) = s
42instance Exception IdrisErr
44ifail :: String -> Idris ()
45ifail str = throwIO (IErr str)
47tclift :: TC a -> Idris a
48tclift tc = case tc of
49 OK v -> return v
50 Error err -> do i <- get
51 case err of
52 At (FC f l) e -> setErrLine l
53 _ -> return ()
54 throwIO (IErr $ pshow i err)
56getErrLine str
57 = case span (/=':') str of
58 (_, ':':rest) -> case span isDigit rest of
59 ([], _) -> 0
60 (num, _) -> read num
61 _ -> 0