git.iko.soy/Idris-dev
on 4e326e4 help sign in
Idris-dev/src/Idris/Error.hs
162 lines 6.7 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.Delaborate
18import Idris.Output
20import Prelude hiding (catch)
22import Control.Monad (when)
23import qualified Data.Foldable as Foldable
24import Data.List (intercalate, isPrefixOf)
25import qualified Data.Set as S
26import qualified Data.Text as T
27import System.IO.Error (ioeGetErrorString, isUserError)
29iucheck :: Idris ()
30iucheck = do tit <- typeInType
31 ist <- getIState
32 let cs = idris_constraints ist
33 logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))
34 when (not tit) $
35 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
36 (\e -> do let fc = getErrSpan e
37 setErrSpan fc
38 iWarn fc $ pprintErr ist e)
40showErr :: Err -> Idris String
41showErr e = getIState >>= return . flip pshow e
44report :: IOError -> String
45report e
46 | isUserError e = ioeGetErrorString e
47 | otherwise = show e
49idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
50idrisCatch = catchError
53setAndReport :: Err -> Idris ()
54setAndReport e = do ist <- getIState
55 case (unwrap e) of
56 At fc e -> do setErrSpan fc
57 iWarn fc $ pprintErr ist e
58 _ -> do setErrSpan (getErrSpan e)
59 iWarn emptyFC $ pprintErr ist e
60 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
61 unwrap e = e
63ifail :: String -> Idris a
64ifail = throwError . Msg
66ierror :: Err -> Idris a
67ierror = throwError
69tclift :: TC a -> Idris a
70tclift (OK v) = return v
71tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
72tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err
73tclift (Error err) = throwError err
75tcliftAt :: FC -> TC a -> Idris a
76tcliftAt fc (OK v) = return v
77tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err
78tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err
79tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc err)
81tctry :: TC a -> TC a -> Idris a
82tctry tc1 tc2
83 = case tc1 of
84 OK v -> return v
85 Error err -> tclift tc2
87getErrSpan :: Err -> FC
88getErrSpan (At fc _) = fc
89getErrSpan (UniverseError fc _ _ _ _) = fc
90getErrSpan _ = emptyFC
92--------------------------------------------------------------------
93-- Specific warnings not included in elaborator
94--------------------------------------------------------------------
95-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
96warnDisamb :: IState -> PTerm -> Idris ()
97warnDisamb ist (PQuote _) = return ()
98warnDisamb ist (PRef _ _ _) = return ()
99warnDisamb ist (PInferRef _ _ _) = return ()
100warnDisamb ist (PPatvar _ _) = return ()
101warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
102warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
103warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
104warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
105warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
106 mapM_ (warnDisamb ist . getTm) args
107warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a
108warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
109 mapM_ (warnDisamb ist . getTm) args
110warnDisamb ist (PMatchApp _ _) = return ()
111warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
112 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
113warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]
114warnDisamb ist (PTrue _ _) = return ()
115warnDisamb ist (PResolveTC _) = return ()
116warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
117 Foldable.mapM_ (warnDisamb ist) z
118warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
119warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
120warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms
121warnDisamb ist (PHidden tm) = warnDisamb ist tm
122warnDisamb ist (PType _) = return ()
123warnDisamb ist (PUniverse _ _) = return ()
124warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
125warnDisamb ist (PConstant _ _) = return ()
126warnDisamb ist Placeholder = return ()
127warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
128 where wStep (DoExp _ x) = warnDisamb ist x
129 wStep (DoBind _ _ _ x) = warnDisamb ist x
130 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
131 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
132 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
133 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
134 wStep (DoRewrite _ h) = warnDisamb ist h
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