{-|
Module      : Idris.Error
Description : Utilities to deal with error reporting.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Idris.Error (getErrSpan, idrisCatch, ierror, ifail, iucheck, report,
                    setAndReport, showErr, tclift, tcliftAt, tctry, warnDisamb) where

import Idris.AbsSyntax
import Idris.Core.Constraints
import Idris.Core.Evaluate (ctxtAlist)
import Idris.Core.TT
import Idris.Delaborate
import Idris.Output

import Prelude hiding (catch)

import Control.Monad (when)
import qualified Data.Foldable as Foldable
import Data.List (intercalate, isPrefixOf)
import qualified Data.Set as S
import qualified Data.Text as T
import System.IO.Error (ioeGetErrorString, isUserError)

iucheck :: Idris ()
iucheck :: Idris ()
iucheck = do Bool
tit <- Idris Bool
typeInType
             IState
ist <- Idris IState
getIState
             let cs :: Set ConstraintFC
cs = IState -> Set ConstraintFC
idris_constraints IState
ist
             Int -> String -> Idris ()
logLvl Int
7 forall a b. (a -> b) -> a -> b
$ String
"ALL CONSTRAINTS: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Set a -> [a]
S.toList Set ConstraintFC
cs))
             forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit) forall a b. (a -> b) -> a -> b
$
                   (forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ Set ConstraintFC -> TC ()
ucheck (IState -> Set ConstraintFC
idris_constraints IState
ist)) forall a. Idris a -> (Err -> Idris a) -> Idris a
`idrisCatch`
                              (\Err
e -> do let fc :: FC
fc = Err -> FC
getErrSpan Err
e
                                        FC -> Idris ()
setErrSpan FC
fc
                                        FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
e)

showErr :: Err -> Idris String
showErr :: Err -> Idris String
showErr Err
e = Idris IState
getIState forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip IState -> Err -> String
pshow Err
e


report :: IOError -> String
report :: IOError -> String
report IOError
e
    | IOError -> Bool
isUserError IOError
e = IOError -> String
ioeGetErrorString IOError
e
    | Bool
otherwise     = forall a. Show a => a -> String
show IOError
e

idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
idrisCatch :: forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch = forall a. Idris a -> (Err -> Idris a) -> Idris a
catchError


setAndReport :: Err -> Idris ()
setAndReport :: Err -> Idris ()
setAndReport Err
e = do IState
ist <- Idris IState
getIState
                    case (forall {t}. Err' t -> Err' t
unwrap Err
e) of
                      At FC
fc Err
e -> do FC -> Idris ()
setErrSpan FC
fc
                                    FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
e
                      Err
_ -> do FC -> Idris ()
setErrSpan (Err -> FC
getErrSpan Err
e)
                              FC -> OutputDoc -> Idris ()
iWarn FC
emptyFC forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
e
  where unwrap :: Err' t -> Err' t
unwrap (ProofSearchFail Err' t
e) = Err' t
e -- remove bookkeeping constructor
        unwrap Err' t
e = Err' t
e

ifail :: String -> Idris a
ifail :: forall a. String -> Idris a
ifail = forall a. Err -> Idris a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg

ierror :: Err -> Idris a
ierror :: forall a. Err -> Idris a
ierror = forall a. Err -> Idris a
throwError

tclift :: TC a -> Idris a
tclift :: forall a. TC a -> Idris a
tclift (OK a
v) = forall (m :: * -> *) a. Monad m => a -> m a
return a
v
tclift (Error err :: Err
err@(At FC
fc Err
e)) = do FC -> Idris ()
setErrSpan FC
fc; forall a. Err -> Idris a
throwError Err
err
tclift (Error err :: Err
err@(UniverseError FC
fc UExp
_ (Int, Int)
_ (Int, Int)
_ [ConstraintFC]
_)) = do FC -> Idris ()
setErrSpan FC
fc; forall a. Err -> Idris a
throwError Err
err
tclift (Error Err
err) = forall a. Err -> Idris a
throwError Err
err

tcliftAt :: FC -> TC a -> Idris a
tcliftAt :: forall a. FC -> TC a -> Idris a
tcliftAt FC
fc (OK a
v) = forall (m :: * -> *) a. Monad m => a -> m a
return a
v
tcliftAt FC
fc (Error err :: Err
err@(At FC
_ Err
e)) = do FC -> Idris ()
setErrSpan FC
fc; forall a. Err -> Idris a
throwError Err
err
tcliftAt FC
fc (Error err :: Err
err@(UniverseError FC
_ UExp
_ (Int, Int)
_ (Int, Int)
_ [ConstraintFC]
_)) = do FC -> Idris ()
setErrSpan FC
fc; forall a. Err -> Idris a
throwError Err
err
tcliftAt FC
fc (Error Err
err) = do FC -> Idris ()
setErrSpan FC
fc; forall a. Err -> Idris a
throwError (forall t. FC -> Err' t -> Err' t
At FC
fc Err
err)

tctry :: TC a -> TC a -> Idris a
tctry :: forall a. TC a -> TC a -> Idris a
tctry TC a
tc1 TC a
tc2
    = case TC a
tc1 of
           OK a
v -> forall (m :: * -> *) a. Monad m => a -> m a
return a
v
           Error Err
err -> forall a. TC a -> Idris a
tclift TC a
tc2

getErrSpan :: Err -> FC
getErrSpan :: Err -> FC
getErrSpan (At FC
fc Err
_) = FC
fc
getErrSpan (UniverseError FC
fc UExp
_ (Int, Int)
_ (Int, Int)
_ [ConstraintFC]
_) = FC
fc
getErrSpan Err
_ = FC
emptyFC

--------------------------------------------------------------------
-- Specific warnings not included in elaborator
--------------------------------------------------------------------
-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
warnDisamb :: IState -> PTerm -> Idris ()
warnDisamb :: IState -> PTerm -> Idris ()
warnDisamb IState
ist (PQuote Raw
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PRef FC
_ [FC]
_ Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PInferRef FC
_ [FC]
_ Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PPatvar FC
_ Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PLam FC
_ Name
_ FC
_ PTerm
t PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb IState
ist (PPi Plicity
_ Name
_ FC
_ PTerm
t PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb IState
ist (PLet FC
_ RigCount
_ Name
_ FC
_ PTerm
x PTerm
t PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb IState
ist (PTyped PTerm
x PTerm
t) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t
warnDisamb IState
ist (PApp FC
_ PTerm
t [PArg]
args) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PArg' t -> t
getTm) [PArg]
args
warnDisamb IState
ist (PWithApp FC
_ PTerm
t PTerm
a) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
a
warnDisamb IState
ist (PAppBind FC
_ PTerm
f [PArg]
args) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
f forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                     forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PArg' t -> t
getTm) [PArg]
args
warnDisamb IState
ist (PMatchApp FC
_ Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PCase FC
_ PTerm
tm [(PTerm, PTerm)]
cases) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(PTerm
x,PTerm
y)-> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y) [(PTerm, PTerm)]
cases
warnDisamb IState
ist (PIfThenElse FC
_ PTerm
c PTerm
t PTerm
f) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist) [PTerm
c, PTerm
t, PTerm
f]
warnDisamb IState
ist (PTrue FC
_ PunInfo
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PResolveTC FC
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PRewrite FC
_ Maybe Name
_ PTerm
x PTerm
y Maybe PTerm
z) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Foldable.mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist) Maybe PTerm
z
warnDisamb IState
ist (PPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
warnDisamb IState
ist (PDPair FC
_ [FC]
_ PunInfo
_ PTerm
x PTerm
y PTerm
z) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
z
warnDisamb IState
ist (PAlternative [(Name, Name)]
_ PAltType
_ [PTerm]
tms) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist) [PTerm]
tms
warnDisamb IState
ist (PHidden PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PType FC
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PUniverse FC
_ Universe
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PGoal FC
_ PTerm
x Name
_ PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
warnDisamb IState
ist (PConstant FC
_ Const
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist PTerm
Placeholder = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PDoBlock [PDo]
steps) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PDo -> Idris ()
wStep [PDo]
steps
  where wStep :: PDo -> Idris ()
wStep (DoExp FC
_ PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
        wStep (DoBind FC
_ Name
_ FC
_ PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
        wStep (DoBindP FC
_ PTerm
x PTerm
y [(PTerm, PTerm)]
cs) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(PTerm
x,PTerm
y) -> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y) [(PTerm, PTerm)]
cs
        wStep (DoLet FC
_ RigCount
_ Name
_ FC
_ PTerm
x PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
        wStep (DoLetP FC
_ PTerm
x PTerm
y [(PTerm, PTerm)]
cs) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(PTerm
x,PTerm
y) -> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y) [(PTerm, PTerm)]
cs
        wStep (DoRewrite FC
_ PTerm
h) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
h
warnDisamb IState
ist (PIdiom FC
_ PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
warnDisamb IState
ist (PMetavar FC
_ Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PProof [PTactic]
tacs) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Foldable.mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist)) [PTactic]
tacs
warnDisamb IState
ist (PTactics [PTactic]
tacs) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Foldable.mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist)) [PTactic]
tacs
warnDisamb IState
ist (PElabError Err
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist PTerm
PImpossible = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PCoerced PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PDisamb [[Text]]
ds PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Text] -> Idris ()
warnEmpty [[Text]]
ds
  where warnEmpty :: [Text] -> Idris ()
warnEmpty [Text]
d =
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Text] -> Name -> Bool
isIn [Text]
d forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (Context -> [(Name, Def)]
ctxtAlist (IState -> Context
tt_ctxt IState
ist)))) forall a b. (a -> b) -> a -> b
$
            forall a. Err -> Idris a
ierror forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
              String
"Nothing found in namespace \"" forall a. [a] -> [a] -> [a]
++
              forall a. [a] -> [[a]] -> [a]
intercalate String
"." (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ [Text]
d) forall a. [a] -> [a] -> [a]
++
              String
"\"."
        isIn :: [Text] -> Name -> Bool
isIn [Text]
d (NS Name
_ [Text]
ns) = forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Text]
d [Text]
ns
        isIn [Text]
d Name
_ = Bool
False

warnDisamb IState
ist (PUnifyLog PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PNoImplicits PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PQuasiquote PTerm
tm Maybe PTerm
goal) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Foldable.mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist) Maybe PTerm
goal
warnDisamb IState
ist (PUnquote PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PQuoteName Name
_ Bool
_ FC
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PAs FC
_ Name
_ PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PAppImpl PTerm
tm [ImplicitInfo]
_) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PRunElab FC
_ PTerm
tm [String]
_) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb IState
ist (PConstSugar FC
_ PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm