git.iko.soy/Idris-dev
on cc9acda 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
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
38idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
39idrisCatch = catchError
41setAndReport :: Err -> Idris ()
42setAndReport e = do ist <- getIState
43 let h = idris_outh ist
44 case e of
45 At fc@(FC f l c) e -> do setErrLine l
46 ihWarn h fc $ pshow ist e
47 _ -> do setErrLine (getErrLine e)
48 ihputStrLn h $ pshow ist e
50ifail :: String -> Idris a
51ifail = throwError . Msg
53ierror :: Err -> Idris a
54ierror = throwError
56tclift :: TC a -> Idris a
57tclift (OK v) = return v
58tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err
59tclift (Error err) = throwError err
61tctry :: TC a -> TC a -> Idris a
62tctry tc1 tc2
63 = case tc1 of
64 OK v -> return v
65 Error err -> tclift tc2
67getErrLine :: Err -> Int
68getErrLine (At (FC _ l _) _) = l
69getErrLine _ = 0
71getErrColumn :: Err -> Int
72getErrColumn (At (FC _ _ c) _) = c
73getErrColumn _ = 0