git.iko.soy/Idris-dev
on 0bc69fb help sign in
Idris-dev/src/Idris/Error.hs
51 lines 1.5 kB history raw
1module Idris.Error where
3import Idris.AbsSyntax
4import Idris.Delaborate
6import Core.TT
7import Core.Typecheck
8import Core.Constraints
10import Control.Monad.State
11import System.IO.Error
12import Data.Char
14iucheck :: Idris ()
15iucheck = do tit <- typeInType
16 when (not tit) $
17 do ist <- get
18 idrisCatch (tclift $ ucheck (idris_constraints ist))
19 (\e -> do let msg = report e
20 setErrLine (getErrLine msg)
21 iputStrLn msg)
23report :: IOError -> String
24report e
25 | isUserError e = ioeGetErrorString e
26 | otherwise = show e
28-- Taken from the library source code - for ghc 6.12/7 compatibility
29liftCatch :: (m (a,s) -> (e -> m (a,s)) -> m (a,s)) ->
30 StateT s m a -> (e -> StateT s m a) -> StateT s m a
31liftCatch catchError m h =
32 StateT $ \s -> runStateT m s `catchError` \e -> runStateT (h e) s
34idrisCatch :: Idris a -> (IOError -> Idris a) -> Idris a
35idrisCatch op handler = liftCatch catch op handler
37tclift :: Show a => TC a -> Idris a
38tclift tc = case tc of
39 OK v -> return v
40 Error err -> do i <- get
41 case err of
42 At (FC f l) e -> setErrLine l
43 _ -> return ()
44 fail (pshow i err)
46getErrLine str
47 = case span (/=':') str of
48 (_, ':':rest) -> case span isDigit rest of
49 (num, _) -> read num
50 _ -> 0