git.iko.soy/Idris-dev
on 181dddb help sign in
Idris-dev/src/Idris/Error.hs
163 lines 6.6 kB history raw
1{-|
2Module : Idris.Error
3Description : Utilities to deal with error reporting.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE DeriveDataTypeable #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Error where
13import Prelude hiding (catch)
14import Idris.AbsSyntax
15import Idris.Delaborate
17import Idris.Core.Evaluate (ctxtAlist)
18import Idris.Core.TT
19import Idris.Core.Typecheck
20import Idris.Core.Constraints
21import Idris.Output
23import System.Console.Haskeline
24import System.Console.Haskeline.MonadException
25import Control.Monad (when)
26import Control.Monad.State.Strict
27import System.IO.Error(isUserError, ioeGetErrorString)
28import Data.Char
29import Data.List (intercalate, isPrefixOf)
30import qualified Data.Text as T
31import qualified Data.Set as S
32import Data.Typeable
33import qualified Data.Traversable as Traversable
34import qualified Data.Foldable as Foldable
36iucheck :: Idris ()
37iucheck = do tit <- typeInType
38 ist <- getIState
39 let cs = idris_constraints ist
40 logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))
41 when (not tit) $
42 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
43 (\e -> do let fc = getErrSpan e
44 setErrSpan fc
45 iWarn fc $ pprintErr ist e)
47showErr :: Err -> Idris String
48showErr e = getIState >>= return . flip pshow e
51report :: IOError -> String
52report e
53 | isUserError e = ioeGetErrorString e
54 | otherwise = show e
56idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
57idrisCatch = catchError
60setAndReport :: Err -> Idris ()
61setAndReport e = do ist <- getIState
62 case (unwrap e) of
63 At fc e -> do setErrSpan fc
64 iWarn fc $ pprintErr ist e
65 _ -> do setErrSpan (getErrSpan e)
66 iWarn emptyFC $ pprintErr ist e
67 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
68 unwrap e = e
70ifail :: String -> Idris a
71ifail = throwError . Msg
73ierror :: Err -> Idris a
74ierror = throwError
76tclift :: TC a -> Idris a
77tclift (OK v) = return v
78tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
79tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err
80tclift (Error err) = throwError err
82tctry :: TC a -> TC a -> Idris a
83tctry tc1 tc2
84 = case tc1 of
85 OK v -> return v
86 Error err -> tclift tc2
88getErrSpan :: Err -> FC
89getErrSpan (At fc _) = fc
90getErrSpan (UniverseError fc _ _ _ _) = fc
91getErrSpan _ = emptyFC
93--------------------------------------------------------------------
94-- Specific warnings not included in elaborator
95--------------------------------------------------------------------
96-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
97warnDisamb :: IState -> PTerm -> Idris ()
98warnDisamb ist (PQuote _) = return ()
99warnDisamb ist (PRef _ _ _) = return ()
100warnDisamb ist (PInferRef _ _ _) = return ()
101warnDisamb ist (PPatvar _ _) = return ()
102warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
103warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
104warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
105warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
106warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
107 mapM_ (warnDisamb ist . getTm) args
108warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a
109warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
110 mapM_ (warnDisamb ist . getTm) args
111warnDisamb ist (PMatchApp _ _) = return ()
112warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
113 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
114warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]
115warnDisamb ist (PTrue _ _) = return ()
116warnDisamb ist (PResolveTC _) = return ()
117warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
118 Foldable.mapM_ (warnDisamb ist) z
119warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
120warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
121warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms
122warnDisamb ist (PHidden tm) = warnDisamb ist tm
123warnDisamb ist (PType _) = return ()
124warnDisamb ist (PUniverse _) = return ()
125warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
126warnDisamb ist (PConstant _ _) = return ()
127warnDisamb ist Placeholder = return ()
128warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
129 where wStep (DoExp _ x) = warnDisamb ist x
130 wStep (DoBind _ _ _ x) = warnDisamb ist x
131 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
132 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
133 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
134 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
135warnDisamb ist (PIdiom _ x) = warnDisamb ist x
136warnDisamb ist (PReturn _) = return ()
137warnDisamb ist (PMetavar _ _) = return ()
138warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
139warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
140warnDisamb ist (PElabError _) = return ()
141warnDisamb ist PImpossible = return ()
142warnDisamb ist (PCoerced tm) = warnDisamb ist tm
143warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
144 mapM_ warnEmpty ds
145 where warnEmpty d =
146 when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
147 ierror . Msg $
148 "Nothing found in namespace \"" ++
149 intercalate "." (map T.unpack d) ++
150 "\"."
151 isIn d (NS _ ns) = isPrefixOf d ns
152 isIn d _ = False
154warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
155warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
156warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
157 Foldable.mapM_ (warnDisamb ist) goal
158warnDisamb ist (PUnquote tm) = warnDisamb ist tm
159warnDisamb ist (PQuoteName _ _ _) = return ()
160warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
161warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
162warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
163warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm