git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Error.hs
164 lines 6.9 kB history raw
1{-|
2Module : Idris.Error
3Description : Utilities to deal with error reporting.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE DeriveDataTypeable #-}
9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
11module Idris.Error (getErrSpan, idrisCatch, ierror, ifail, iucheck, report,
12 setAndReport, showErr, tclift, tcliftAt, tctry, warnDisamb) where
14import Idris.AbsSyntax
15import Idris.Core.Constraints
16import Idris.Core.Evaluate (ctxtAlist)
17import Idris.Core.TT
18import Idris.Delaborate
19import Idris.Output
21import Prelude hiding (catch)
23import Control.Monad (when)
24import qualified Data.Foldable as Foldable
25import Data.List (intercalate, isPrefixOf)
26import qualified Data.Set as S
27import qualified Data.Text as T
28import System.IO.Error (ioeGetErrorString, isUserError)
30iucheck :: Idris ()
31iucheck = do tit <- typeInType
32 ist <- getIState
33 let cs = idris_constraints ist
34 logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))
35 when (not tit) $
36 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
37 (\e -> do let fc = getErrSpan e
38 setErrSpan fc
39 iWarn fc $ pprintErr ist e)
41showErr :: Err -> Idris String
42showErr e = getIState >>= return . flip pshow e
45report :: IOError -> String
46report e
47 | isUserError e = ioeGetErrorString e
48 | otherwise = show e
50idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
51idrisCatch = catchError
54setAndReport :: Err -> Idris ()
55setAndReport e = do ist <- getIState
56 case (unwrap e) of
57 At fc e -> do setErrSpan fc
58 iWarn fc $ pprintErr ist e
59 _ -> do setErrSpan (getErrSpan e)
60 iWarn emptyFC $ pprintErr ist e
61 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
62 unwrap e = e
64ifail :: String -> Idris a
65ifail = throwError . Msg
67ierror :: Err -> Idris a
68ierror = throwError
70tclift :: TC a -> Idris a
71tclift (OK v) = return v
72tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
73tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err
74tclift (Error err) = throwError err
76tcliftAt :: FC -> TC a -> Idris a
77tcliftAt fc (OK v) = return v
78tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err
79tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err
80tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc 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 cs) = warnDisamb ist x >> warnDisamb ist y >>
135 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
136 wStep (DoRewrite _ h) = warnDisamb ist h
137warnDisamb ist (PIdiom _ x) = warnDisamb ist x
138warnDisamb ist (PMetavar _ _) = return ()
139warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
140warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
141warnDisamb ist (PElabError _) = return ()
142warnDisamb ist PImpossible = return ()
143warnDisamb ist (PCoerced tm) = warnDisamb ist tm
144warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
145 mapM_ warnEmpty ds
146 where warnEmpty d =
147 when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
148 ierror . Msg $
149 "Nothing found in namespace \"" ++
150 intercalate "." (map T.unpack . reverse $ d) ++
151 "\"."
152 isIn d (NS _ ns) = isPrefixOf d ns
153 isIn d _ = False
155warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
156warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
157warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
158 Foldable.mapM_ (warnDisamb ist) goal
159warnDisamb ist (PUnquote tm) = warnDisamb ist tm
160warnDisamb ist (PQuoteName _ _ _) = return ()
161warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
162warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
163warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
164warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm