git.iko.soy/Idris-dev
on 496cf41 help sign in
Idris-dev/src/Idris/Error.hs
73 lines 1.9 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)
48ierror :: Err -> Idris ()
49ierror err = do i <- get
50 throwIO (IErr $ pshow i err)
52tclift :: TC a -> Idris a
53tclift tc = case tc of
54 OK v -> return v
55 Error err -> do i <- get
56 case err of
57 At (FC f l) e -> setErrLine l
58 _ -> return ()
59 throwIO (IErr $ pshow i err)
61tctry :: TC a -> TC a -> Idris a
62tctry tc1 tc2
63 = case tc1 of
64 OK v -> return v
65 Error err -> tclift tc2
67getErrLine str
68 = case span (/=':') str of
69 (_, ':':rest) -> case span isDigit rest of
70 ([], _) -> 0
71 (num, _) -> read num
72 _ -> 0