git.iko.soy/Idris-dev
on 5cf643e help sign in
Idris-dev/src/Idris/Error.hs
162 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 Idris.AbsSyntax
14import Idris.Core.Constraints
15import Idris.Core.Evaluate (ctxtAlist)
16import Idris.Core.TT
17import Idris.Core.Typecheck
18import Idris.Delaborate
19import Idris.Output
21import Prelude hiding (catch)
23import Control.Monad (when)
24import Control.Monad.State.Strict
25import Data.Char
26import qualified Data.Foldable as Foldable
27import Data.List (intercalate, isPrefixOf)
28import qualified Data.Set as S
29import qualified Data.Text as T
30import qualified Data.Traversable as Traversable
31import Data.Typeable
32import System.Console.Haskeline
33import System.Console.Haskeline.MonadException
34import System.IO.Error (ioeGetErrorString, isUserError)
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 (PMetavar _ _) = return ()
137warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
138warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
139warnDisamb ist (PElabError _) = return ()
140warnDisamb ist PImpossible = return ()
141warnDisamb ist (PCoerced tm) = warnDisamb ist tm
142warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
143 mapM_ warnEmpty ds
144 where warnEmpty d =
145 when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
146 ierror . Msg $
147 "Nothing found in namespace \"" ++
148 intercalate "." (map T.unpack . reverse $ d) ++
149 "\"."
150 isIn d (NS _ ns) = isPrefixOf d ns
151 isIn d _ = False
153warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
154warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
155warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
156 Foldable.mapM_ (warnDisamb ist) goal
157warnDisamb ist (PUnquote tm) = warnDisamb ist tm
158warnDisamb ist (PQuoteName _ _ _) = return ()
159warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
160warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
161warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
162warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm