git.iko.soy/Idris-dev
on ea65347 help sign in
Idris-dev/src/Idris/Error.hs
168 lines 6.9 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
82tcliftAt :: FC -> TC a -> Idris a
83tcliftAt fc (OK v) = return v
84tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err
85tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err
86tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc err)
88tctry :: TC a -> TC a -> Idris a
89tctry tc1 tc2
90 = case tc1 of
91 OK v -> return v
92 Error err -> tclift tc2
94getErrSpan :: Err -> FC
95getErrSpan (At fc _) = fc
96getErrSpan (UniverseError fc _ _ _ _) = fc
97getErrSpan _ = emptyFC
99--------------------------------------------------------------------
100-- Specific warnings not included in elaborator
101--------------------------------------------------------------------
102-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
103warnDisamb :: IState -> PTerm -> Idris ()
104warnDisamb ist (PQuote _) = return ()
105warnDisamb ist (PRef _ _ _) = return ()
106warnDisamb ist (PInferRef _ _ _) = return ()
107warnDisamb ist (PPatvar _ _) = return ()
108warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
109warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
110warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
111warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
112warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
113 mapM_ (warnDisamb ist . getTm) args
114warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a
115warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
116 mapM_ (warnDisamb ist . getTm) args
117warnDisamb ist (PMatchApp _ _) = return ()
118warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
119 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
120warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]
121warnDisamb ist (PTrue _ _) = return ()
122warnDisamb ist (PResolveTC _) = return ()
123warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
124 Foldable.mapM_ (warnDisamb ist) z
125warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
126warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
127warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms
128warnDisamb ist (PHidden tm) = warnDisamb ist tm
129warnDisamb ist (PType _) = return ()
130warnDisamb ist (PUniverse _ _) = return ()
131warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
132warnDisamb ist (PConstant _ _) = return ()
133warnDisamb ist Placeholder = return ()
134warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
135 where wStep (DoExp _ x) = warnDisamb ist x
136 wStep (DoBind _ _ _ x) = warnDisamb ist x
137 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
141warnDisamb ist (PIdiom _ x) = warnDisamb ist x
142warnDisamb ist (PMetavar _ _) = return ()
143warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
144warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
145warnDisamb ist (PElabError _) = return ()
146warnDisamb ist PImpossible = return ()
147warnDisamb ist (PCoerced tm) = warnDisamb ist tm
148warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
149 mapM_ warnEmpty ds
150 where warnEmpty d =
151 when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
152 ierror . Msg $
153 "Nothing found in namespace \"" ++
154 intercalate "." (map T.unpack . reverse $ d) ++
155 "\"."
156 isIn d (NS _ ns) = isPrefixOf d ns
157 isIn d _ = False
159warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
160warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
161warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
162 Foldable.mapM_ (warnDisamb ist) goal
163warnDisamb ist (PUnquote tm) = warnDisamb ist tm
164warnDisamb ist (PQuoteName _ _ _) = return ()
165warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
166warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
167warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
168warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm