git.iko.soy/Idris-dev
on cbbdb3e help sign in
Idris-dev/src/Idris/Error.hs
151 lines 6.1 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 setErrSpan (getErrSpan e)
36 iputStrLn (pshow ist e))
38showErr :: Err -> Idris String
39showErr e = getIState >>= return . flip pshow e
42report :: IOError -> String
43report e
44 | isUserError e = ioeGetErrorString e
45 | otherwise = show e
47idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
48idrisCatch = catchError
51setAndReport :: Err -> Idris ()
52setAndReport e = do ist <- getIState
53 case (unwrap e) of
54 At fc e -> do setErrSpan fc
55 iWarn fc $ pprintErr ist e
56 _ -> do setErrSpan (getErrSpan e)
57 iWarn emptyFC $ pprintErr ist e
58 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
59 unwrap e = e
61ifail :: String -> Idris a
62ifail = throwError . Msg
64ierror :: Err -> Idris a
65ierror = throwError
67tclift :: TC a -> Idris a
68tclift (OK v) = return v
69tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
70tclift (Error err) = throwError err
72tctry :: TC a -> TC a -> Idris a
73tctry tc1 tc2
74 = case tc1 of
75 OK v -> return v
76 Error err -> tclift tc2
78getErrSpan :: Err -> FC
79getErrSpan (At fc _) = fc
80getErrSpan _ = emptyFC
82--------------------------------------------------------------------
83-- Specific warnings not included in elaborator
84--------------------------------------------------------------------
85-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
86warnDisamb :: IState -> PTerm -> Idris ()
87warnDisamb ist (PQuote _) = return ()
88warnDisamb ist (PRef _ _) = return ()
89warnDisamb ist (PInferRef _ _) = return ()
90warnDisamb ist (PPatvar _ _) = return ()
91warnDisamb ist (PLam _ _ t b) = warnDisamb ist t >> warnDisamb ist b
92warnDisamb ist (PPi _ _ t b) = warnDisamb ist t >> warnDisamb ist b
93warnDisamb ist (PLet _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
94warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
95warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
96 mapM_ (warnDisamb ist . getTm) args
97warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
98 mapM_ (warnDisamb ist . getTm) args
99warnDisamb ist (PMatchApp _ _) = return ()
100warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
101 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
102warnDisamb ist (PTrue _ _) = return ()
103warnDisamb ist (PRefl _ tm) = warnDisamb ist tm
104warnDisamb ist (PResolveTC _) = return ()
105warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>
106 warnDisamb ist x >> warnDisamb ist y
107warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
108 Foldable.mapM_ (warnDisamb ist) z
109warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y
110warnDisamb ist (PDPair _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
111warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms
112warnDisamb ist (PHidden tm) = warnDisamb ist tm
113warnDisamb ist PType = return ()
114warnDisamb ist (PUniverse _) = return ()
115warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
116warnDisamb ist (PConstant _) = return ()
117warnDisamb ist Placeholder = return ()
118warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
119 where wStep (DoExp _ x) = warnDisamb ist x
120 wStep (DoBind _ _ x) = warnDisamb ist x
121 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
122 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cs
123 wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y
124 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
125warnDisamb ist (PIdiom _ x) = warnDisamb ist x
126warnDisamb ist (PReturn _) = return ()
127warnDisamb ist (PMetavar _) = return ()
128warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
129warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
130warnDisamb ist (PElabError _) = return ()
131warnDisamb ist PImpossible = return ()
132warnDisamb ist (PCoerced tm) = warnDisamb ist tm
133warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
134 mapM_ warnEmpty ds
135 where warnEmpty d =
136 when (null (filter (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
137 ierror . Msg $
138 "Nothing found in namespace \"" ++
139 intercalate "." (map T.unpack d) ++
140 "\"."
141 isIn d (NS _ ns) = isPrefixOf d ns
142 isIn d _ = False
144warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
145warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
146warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
147 Foldable.mapM_ (warnDisamb ist) goal
148warnDisamb ist (PUnquote tm) = warnDisamb ist tm
149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
150warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
151warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm