git.iko.soy/Idris-dev
on 2dfba31 help sign in
Idris-dev/src/Idris/Error.hs
155 lines 6.4 kB history raw
1{-# LANGUAGE DeriveDataTypeable #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4module Idris.Error where
6import Prelude hiding (catch)
7import Idris.AbsSyntax
8import Idris.Delaborate
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 System.IO.Error(isUserError, ioeGetErrorString)
21import Data.Char
22import Data.List (intercalate, isPrefixOf)
23import qualified Data.Text as T
24import Data.Typeable
25import qualified Data.Traversable as Traversable
26import qualified Data.Foldable as Foldable
28iucheck :: Idris ()
29iucheck = do tit <- typeInType
30 ist <- getIState
31 let cs = idris_constraints ist
32 logLvl 7 $ "ALL CONSTRAINTS: " ++ show cs
33 when (not tit) $
34 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
35 (\e -> do let fc = getErrSpan e
36 setErrSpan fc
37 iWarn fc $ pprintErr 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@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err
72tclift (Error err) = throwError err
74tctry :: TC a -> TC a -> Idris a
75tctry tc1 tc2
76 = case tc1 of
77 OK v -> return v
78 Error err -> tclift tc2
80getErrSpan :: Err -> FC
81getErrSpan (At fc _) = fc
82getErrSpan (UniverseError fc _ _ _ _) = fc
83getErrSpan _ = emptyFC
85--------------------------------------------------------------------
86-- Specific warnings not included in elaborator
87--------------------------------------------------------------------
88-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
89warnDisamb :: IState -> PTerm -> Idris ()
90warnDisamb ist (PQuote _) = return ()
91warnDisamb ist (PRef _ _ _) = return ()
92warnDisamb ist (PInferRef _ _ _) = return ()
93warnDisamb ist (PPatvar _ _) = return ()
94warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
95warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
96warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
97warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
98warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
99 mapM_ (warnDisamb ist . getTm) args
100warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a
101warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
102 mapM_ (warnDisamb ist . getTm) args
103warnDisamb ist (PMatchApp _ _) = return ()
104warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
105 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
106warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]
107warnDisamb ist (PTrue _ _) = return ()
108warnDisamb ist (PResolveTC _) = return ()
109warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
110 Foldable.mapM_ (warnDisamb ist) z
111warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
112warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
113warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms
114warnDisamb ist (PHidden tm) = warnDisamb ist tm
115warnDisamb ist (PType _) = return ()
116warnDisamb ist (PUniverse _) = return ()
117warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
118warnDisamb ist (PConstant _ _) = return ()
119warnDisamb ist Placeholder = return ()
120warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
121 where wStep (DoExp _ x) = warnDisamb ist x
122 wStep (DoBind _ _ _ x) = warnDisamb ist x
123 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
124 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
125 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
126 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
127warnDisamb ist (PIdiom _ x) = warnDisamb ist x
128warnDisamb ist (PReturn _) = return ()
129warnDisamb ist (PMetavar _ _) = return ()
130warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
131warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
132warnDisamb ist (PElabError _) = return ()
133warnDisamb ist PImpossible = return ()
134warnDisamb ist (PCoerced tm) = warnDisamb ist tm
135warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
136 mapM_ warnEmpty ds
137 where warnEmpty d =
138 when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
139 ierror . Msg $
140 "Nothing found in namespace \"" ++
141 intercalate "." (map T.unpack d) ++
142 "\"."
143 isIn d (NS _ ns) = isPrefixOf d ns
144 isIn d _ = False
146warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
147warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
148warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
149 Foldable.mapM_ (warnDisamb ist) goal
150warnDisamb ist (PUnquote tm) = warnDisamb ist tm
151warnDisamb ist (PQuoteName _ _ _) = return ()
152warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
153warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
154warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
155warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm