git.iko.soy/Idris-dev
on 175a735 help sign in
Idris-dev/src/Idris/Error.hs
71 lines 1.9 kB history raw
1{-# LANGUAGE DeriveDataTypeable #-}
3module Idris.Error where
5import Prelude hiding (catch)
6import Idris.AbsSyntax
7import Idris.Delaborate
8import Idris.Output
10import Idris.Core.TT
11import Idris.Core.Typecheck
12import Idris.Core.Constraints
14import System.Console.Haskeline
15import System.Console.Haskeline.MonadException
16import Control.Monad.State.Strict
17import Control.Monad.Error (throwError, catchError)
18import System.IO.Error(isUserError, ioeGetErrorString)
19import Data.Char
20import Data.Typeable
22iucheck :: Idris ()
23iucheck = do tit <- typeInType
24 when (not tit) $
25 do ist <- getIState
26 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
27 (\e -> do setErrSpan (getErrSpan e)
28 iputStrLn (pshow ist e))
30showErr :: Err -> Idris String
31showErr e = getIState >>= return . flip pshow e
34report :: IOError -> String
35report e
36 | isUserError e = ioeGetErrorString e
37 | otherwise = show e
39idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
40idrisCatch = catchError
43setAndReport :: Err -> Idris ()
44setAndReport e = do ist <- getIState
45 let h = idris_outh ist
46 case e of
47 At fc e -> do setErrSpan fc
48 ihWarn h fc $ pprintErr ist e
49 _ -> do setErrSpan (getErrSpan e)
50 ihputStrLn h $ pshow ist e
52ifail :: String -> Idris a
53ifail = throwError . Msg
55ierror :: Err -> Idris a
56ierror = throwError
58tclift :: TC a -> Idris a
59tclift (OK v) = return v
60tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
61tclift (Error err) = throwError err
63tctry :: TC a -> TC a -> Idris a
64tctry tc1 tc2
65 = case tc1 of
66 OK v -> return v
67 Error err -> tclift tc2
69getErrSpan :: Err -> FC
70getErrSpan (At fc _) = fc
71getErrSpan _ = emptyFC