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