git.iko.soy/Idris-dev
on 46256ab help sign in
Idris-dev/src/Idris/Error.hs
68 lines 1.7 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 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
38--idrisCatch :: Idris a -> (SomeException -> Idris a) -> Idris a
39--idrisCatch = catch
41idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
42idrisCatch = catchError
45ifail :: String -> Idris a
46ifail = throwError . Msg
48ierror :: Err -> Idris a
49ierror = throwError
51tclift :: TC a -> Idris a
52tclift (OK v) = return v
53tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err
54tclift (Error err) = throwError err
56tctry :: TC a -> TC a -> Idris a
57tctry tc1 tc2
58 = case tc1 of
59 OK v -> return v
60 Error err -> tclift tc2
62getErrLine :: Err -> Int
63getErrLine (At (FC _ l _) _) = l
64getErrLine _ = 0
66getErrColumn :: Err -> Int
67getErrColumn (At (FC _ _ c) _) = c
68getErrColumn _ = 0