git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Error.hs
72 lines 2.0 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 case (unwrap e) of
46 At fc e -> do setErrSpan fc
47 iWarn fc $ pprintErr ist e
48 _ -> do setErrSpan (getErrSpan e)
49 iWarn emptyFC $ pprintErr ist e
50 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
51 unwrap e = e
53ifail :: String -> Idris a
54ifail = throwError . Msg
56ierror :: Err -> Idris a
57ierror = throwError
59tclift :: TC a -> Idris a
60tclift (OK v) = return v
61tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
62tclift (Error err) = throwError err
64tctry :: TC a -> TC a -> Idris a
65tctry tc1 tc2
66 = case tc1 of
67 OK v -> return v
68 Error err -> tclift tc2
70getErrSpan :: Err -> FC
71getErrSpan (At fc _) = fc
72getErrSpan _ = emptyFC