git.iko.soy/Idris-dev
on cb005bc help sign in
Idris-dev/src/Idris/Error.hs
148 lines 6.0 kB history raw
1{-# LANGUAGE DeriveDataTypeable #-}
3module Idris.Error where
5import Prelude hiding (catch)
6import Idris.AbsSyntax
7import Idris.Delaborate
9import Idris.Core.Evaluate (ctxtAlist)
10import Idris.Core.TT
11import Idris.Core.Typecheck
12import Idris.Core.Constraints
13import Idris.Output
15import System.Console.Haskeline
16import System.Console.Haskeline.MonadException
17import Control.Monad (when)
18import Control.Monad.State.Strict
19import System.IO.Error(isUserError, ioeGetErrorString)
20import Data.Char
21import Data.List (intercalate, isPrefixOf)
22import qualified Data.Text as T
23import Data.Typeable
24import qualified Data.Traversable as Traversable
25import qualified Data.Foldable as Foldable
27iucheck :: Idris ()
28iucheck = do tit <- typeInType
29 ist <- getIState
30 let cs = idris_constraints ist
31 logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs
32 when (not tit) $
33 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
34 (\e -> do setErrSpan (getErrSpan e)
35 iputStrLn (pshow ist e))
37showErr :: Err -> Idris String
38showErr e = getIState >>= return . flip pshow e
41report :: IOError -> String
42report e
43 | isUserError e = ioeGetErrorString e
44 | otherwise = show e
46idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
47idrisCatch = catchError
50setAndReport :: Err -> Idris ()
51setAndReport e = do ist <- getIState
52 case (unwrap e) of
53 At fc e -> do setErrSpan fc
54 iWarn fc $ pprintErr ist e
55 _ -> do setErrSpan (getErrSpan e)
56 iWarn emptyFC $ pprintErr ist e
57 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
58 unwrap e = e
60ifail :: String -> Idris a
61ifail = throwError . Msg
63ierror :: Err -> Idris a
64ierror = throwError
66tclift :: TC a -> Idris a
67tclift (OK v) = return v
68tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
69tclift (Error err) = throwError err
71tctry :: TC a -> TC a -> Idris a
72tctry tc1 tc2
73 = case tc1 of
74 OK v -> return v
75 Error err -> tclift tc2
77getErrSpan :: Err -> FC
78getErrSpan (At fc _) = fc
79getErrSpan _ = emptyFC
81--------------------------------------------------------------------
82-- Specific warnings not included in elaborator
83--------------------------------------------------------------------
84-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
85warnDisamb :: IState -> PTerm -> Idris ()
86warnDisamb ist (PQuote _) = return ()
87warnDisamb ist (PRef _ _) = return ()
88warnDisamb ist (PInferRef _ _) = return ()
89warnDisamb ist (PPatvar _ _) = return ()
90warnDisamb ist (PLam _ _ t b) = warnDisamb ist t >> warnDisamb ist b
91warnDisamb ist (PPi _ _ t b) = warnDisamb ist t >> warnDisamb ist b
92warnDisamb ist (PLet _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
93warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
94warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
95 mapM_ (warnDisamb ist . getTm) args
96warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
97 mapM_ (warnDisamb ist . getTm) args
98warnDisamb ist (PMatchApp _ _) = return ()
99warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
100 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
101warnDisamb ist (PTrue _ _) = return ()
102warnDisamb ist (PRefl _ tm) = warnDisamb ist tm
103warnDisamb ist (PResolveTC _) = return ()
104warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>
105 warnDisamb ist x >> warnDisamb ist y
106warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
107 Foldable.mapM_ (warnDisamb ist) z
108warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y
109warnDisamb ist (PDPair _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
110warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms
111warnDisamb ist (PHidden tm) = warnDisamb ist tm
112warnDisamb ist PType = return ()
113warnDisamb ist (PUniverse _) = return ()
114warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
115warnDisamb ist (PConstant _) = return ()
116warnDisamb ist Placeholder = return ()
117warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
118 where wStep (DoExp _ x) = warnDisamb ist x
119 wStep (DoBind _ _ x) = warnDisamb ist x
120 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
121 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cs
122 wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y
123 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
124warnDisamb ist (PIdiom _ x) = warnDisamb ist x
125warnDisamb ist (PReturn _) = return ()
126warnDisamb ist (PMetavar _) = return ()
127warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
128warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
129warnDisamb ist (PElabError _) = return ()
130warnDisamb ist PImpossible = return ()
131warnDisamb ist (PCoerced tm) = warnDisamb ist tm
132warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
133 mapM_ warnEmpty ds
134 where warnEmpty d =
135 when (null (filter (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
136 ierror . Msg $
137 "Nothing found in namespace \"" ++
138 intercalate "." (map T.unpack d) ++
139 "\"."
140 isIn d (NS _ ns) = isPrefixOf d ns
141 isIn d _ = False
143warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
144warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
145warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
146 Foldable.mapM_ (warnDisamb ist) goal
147warnDisamb ist (PUnquote tm) = warnDisamb ist tm
148warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm