{-|
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"ALL CONSTRAINTS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([ConstraintFC] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Set ConstraintFC -> [ConstraintFC]
forall a. Set a -> [a]
S.toList Set ConstraintFC
cs))
             Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
                   (TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Set ConstraintFC -> TC ()
ucheck (IState -> Set ConstraintFC
idris_constraints IState
ist)) Idris () -> (Err -> Idris ()) -> Idris ()
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 (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
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 Idris IState -> (IState -> Idris String) -> Idris String
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Idris String
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Idris String)
-> (IState -> String) -> IState -> Idris String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IState -> Err -> String) -> Err -> IState -> String
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     = IOError -> String
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 = Idris a -> (Err -> Idris a) -> Idris a
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 (Err -> Err
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 (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
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 (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
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 = Err -> Idris a
forall a. Err -> Idris a
throwError (Err -> Idris a) -> (String -> Err) -> String -> Idris a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg

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

tclift :: TC a -> Idris a
tclift :: forall a. TC a -> Idris a
tclift (OK a
v) = a -> StateT IState (ExceptT Err IO) a
forall a. a -> StateT IState (ExceptT Err IO) a
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; Err -> StateT IState (ExceptT Err IO) a
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; Err -> StateT IState (ExceptT Err IO) a
forall a. Err -> Idris a
throwError Err
err
tclift (Error Err
err) = Err -> StateT IState (ExceptT Err IO) a
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) = a -> StateT IState (ExceptT Err IO) a
forall a. a -> StateT IState (ExceptT Err IO) a
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; Err -> StateT IState (ExceptT Err IO) a
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; Err -> StateT IState (ExceptT Err IO) a
forall a. Err -> Idris a
throwError Err
err
tcliftAt FC
fc (Error Err
err) = do FC -> Idris ()
setErrSpan FC
fc; Err -> StateT IState (ExceptT Err IO) a
forall a. Err -> Idris a
throwError (FC -> Err -> Err
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 -> a -> Idris a
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
           Error Err
err -> TC a -> Idris a
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PRef FC
_ [FC]
_ Name
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PInferRef FC
_ [FC]
_ Name
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PPatvar FC
_ Name
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                 (PArg -> Idris ()) -> [PArg] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist (PTerm -> Idris ()) -> (PArg -> PTerm) -> PArg -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                     (PArg -> Idris ()) -> [PArg] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IState -> PTerm -> Idris ()
warnDisamb IState
ist (PTerm -> Idris ()) -> (PArg -> PTerm) -> PArg -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PArg -> PTerm
forall t. PArg' t -> t
getTm) [PArg]
args
warnDisamb IState
ist (PMatchApp FC
_ Name
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                    ((PTerm, PTerm) -> Idris ()) -> [(PTerm, PTerm)] -> Idris ()
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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) = (PTerm -> Idris ()) -> [PTerm] -> Idris ()
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PResolveTC FC
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                      (PTerm -> Idris ()) -> Maybe PTerm -> Idris ()
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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) = (PTerm -> Idris ()) -> [PTerm] -> Idris ()
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PUniverse FC
_ Universe
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist PTerm
Placeholder = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PDoBlock [PDo]
steps) = (PDo -> Idris ()) -> [PDo] -> Idris ()
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                   ((PTerm, PTerm) -> Idris ()) -> [(PTerm, PTerm)] -> Idris ()
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                  ((PTerm, PTerm) -> Idris ()) -> [(PTerm, PTerm)] -> Idris ()
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist (PProof [PTactic]
tacs) = (PTactic -> Idris ()) -> [PTactic] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((PTerm -> Idris ()) -> PTactic -> Idris ()
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) = (PTactic -> Idris ()) -> [PTactic] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((PTerm -> Idris ()) -> PTactic -> Idris ()
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb IState
ist PTerm
PImpossible = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                 ([Text] -> Idris ()) -> [[Text]] -> Idris ()
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 =
          Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (((Name, Def) -> Bool) -> [(Name, Def)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Text] -> Name -> Bool
isIn [Text]
d (Name -> Bool) -> ((Name, Def) -> Name) -> (Name, Def) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Def) -> Name
forall a b. (a, b) -> a
fst) (Context -> [(Name, Def)]
ctxtAlist (IState -> Context
tt_ctxt IState
ist)))) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
            Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (String -> Err) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$
              String
"Nothing found in namespace \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++
              String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack ([Text] -> [String]) -> ([Text] -> [Text]) -> [Text] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall a. [a] -> [a]
reverse ([Text] -> [String]) -> [Text] -> [String]
forall a b. (a -> b) -> a -> b
$ [Text]
d) String -> String -> String
forall a. [a] -> [a] -> [a]
++
              String
"\"."
        isIn :: [Text] -> Name -> Bool
isIn [Text]
d (NS Name
_ [Text]
ns) = [Text] -> [Text] -> Bool
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 Idris () -> Idris () -> Idris ()
forall a b.
StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                       (PTerm -> Idris ()) -> Maybe PTerm -> Idris ()
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
_) = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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