git.iko.soy/Idris-dev
on 5ffef89 help sign in
Idris-dev/src/Idris/Error.hs
73 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 let h = idris_outh ist
46 case (unwrap e) of
47 At fc e -> do setErrSpan fc
48 ihWarn h fc $ pprintErr ist e
49 _ -> do setErrSpan (getErrSpan e)
50 ihWarn h emptyFC $ pprintErr ist e
51 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
52 unwrap e = e
54ifail :: String -> Idris a
55ifail = throwError . Msg
57ierror :: Err -> Idris a
58ierror = throwError
60tclift :: TC a -> Idris a
61tclift (OK v) = return v
62tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
63tclift (Error err) = throwError err
65tctry :: TC a -> TC a -> Idris a
66tctry tc1 tc2
67 = case tc1 of
68 OK v -> return v
69 Error err -> tclift tc2
71getErrSpan :: Err -> FC
72getErrSpan (At fc _) = fc
73getErrSpan _ = emptyFC