git.iko.soy/Idris-dev
on 3cb1f21 help sign in
Idris-dev/src/Idris/Error.hs
75 lines 2.0 kB history raw
1{-# LANGUAGE DeriveDataTypeable #-}
3module Idris.Error where
5import Prelude hiding (catch)
6import Idris.AbsSyntax
7import Idris.Delaborate
9import Idris.Core.TT
10import Idris.Core.Typecheck
11import Idris.Core.Constraints
13import System.Console.Haskeline
14import System.Console.Haskeline.MonadException
15import Control.Monad.State.Strict
16import Control.Monad.Error (throwError, catchError)
17import System.IO.Error(isUserError, ioeGetErrorString)
18import Data.Char
19import Data.Typeable
21iucheck :: Idris ()
22iucheck = do tit <- typeInType
23 when (not tit) $
24 do ist <- getIState
25 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
26 (\e -> do setErrLine (getErrLine e)
27 iputStrLn (pshow ist e))
29showErr :: Err -> Idris String
30showErr e = getIState >>= return . flip pshow e
33report :: IOError -> String
34report e
35 | isUserError e = ioeGetErrorString e
36 | otherwise = show e
38idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
39idrisCatch = catchError
42setAndReport :: Err -> Idris ()
43setAndReport e = do ist <- getIState
44 let h = idris_outh ist
45 case e of
46 At fc@(FC f l c) e -> do setErrLine l
47 ihWarn h fc $ pshow ist e
48 _ -> do setErrLine (getErrLine e)
49 ihputStrLn h $ pshow ist e
51ifail :: String -> Idris a
52ifail = throwError . Msg
54ierror :: Err -> Idris a
55ierror = throwError
57tclift :: TC a -> Idris a
58tclift (OK v) = return v
59tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err
60tclift (Error err) = throwError err
62tctry :: TC a -> TC a -> Idris a
63tctry tc1 tc2
64 = case tc1 of
65 OK v -> return v
66 Error err -> tclift tc2
68getErrLine :: Err -> Int
69getErrLine (At (FC _ l _) _) = l
70getErrLine _ = 0
72getErrColumn :: Err -> Int
73getErrColumn (At (FC _ _ c) _) = c
74getErrColumn _ = 0