{-|
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 7 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "ALL CONSTRAINTS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([ConstraintFC] -> 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`
                              (\e :: 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 e :: Err
e = Idris IState
getIState Idris IState -> (IState -> Idris String) -> Idris String
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Idris String
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 e :: 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 :: 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 e :: Err
e = do IState
ist <- Idris IState
getIState
                    case (Err -> Err
forall t. Err' t -> Err' t
unwrap Err
e) of
                      At fc :: FC
fc e :: 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
                      _ -> 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 e :: Err' t
e) = Err' t
e -- remove bookkeeping constructor
        unwrap e :: Err' t
e = Err' t
e

ifail :: String -> Idris a
ifail :: 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 :: Err -> Idris a
ierror = Err -> Idris a
forall a. Err -> Idris a
throwError

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

tcliftAt :: FC -> TC a -> Idris a
tcliftAt :: FC -> TC a -> Idris a
tcliftAt fc :: FC
fc (OK v :: a
v) = a -> Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
tcliftAt fc :: FC
fc (Error err :: Err
err@(At _ e :: Err
e)) = do FC -> Idris ()
setErrSpan FC
fc; Err -> Idris a
forall a. Err -> Idris a
throwError Err
err
tcliftAt fc :: FC
fc (Error err :: Err
err@(UniverseError _ _ _ _ _)) = do FC -> Idris ()
setErrSpan FC
fc; Err -> Idris a
forall a. Err -> Idris a
throwError Err
err
tcliftAt fc :: FC
fc (Error err :: Err
err) = do FC -> Idris ()
setErrSpan FC
fc; Err -> Idris 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 :: TC a -> TC a -> Idris a
tctry tc1 :: TC a
tc1 tc2 :: TC a
tc2
    = case TC a
tc1 of
           OK v :: a
v -> a -> Idris a
forall (m :: * -> *) a. Monad m => a -> m a
return a
v
           Error err :: 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
fc _) = FC
fc
getErrSpan (UniverseError fc :: FC
fc _ _ _ _) = FC
fc
getErrSpan _ = 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 ist :: IState
ist (PQuote _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PRef _ _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PInferRef _ _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PPatvar _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PLam _ _ _ t :: PTerm
t b :: PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb ist :: IState
ist (PPi _ _ _ t :: PTerm
t b :: PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb ist :: IState
ist (PLet _ _ _ _ x :: PTerm
x t :: PTerm
t b :: PTerm
b) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
b
warnDisamb ist :: IState
ist (PTyped x :: PTerm
x t :: PTerm
t) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t
warnDisamb ist :: IState
ist (PApp _ t :: PTerm
t args :: [PArg]
args) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
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 ist :: IState
ist (PWithApp _ t :: PTerm
t a :: PTerm
a) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
t Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
a
warnDisamb ist :: IState
ist (PAppBind _ f :: PTerm
f args :: [PArg]
args) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
f Idris () -> Idris () -> Idris ()
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 ist :: IState
ist (PMatchApp _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PCase _ tm :: PTerm
tm cases :: [(PTerm, PTerm)]
cases) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm Idris () -> Idris () -> Idris ()
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_ (\(x :: PTerm
x,y :: PTerm
y)-> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y) [(PTerm, PTerm)]
cases
warnDisamb ist :: IState
ist (PIfThenElse _ c :: PTerm
c t :: PTerm
t f :: 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 ist :: IState
ist (PTrue _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PResolveTC _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PRewrite _ _ x :: PTerm
x y :: PTerm
y z :: Maybe PTerm
z) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
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 ist :: IState
ist (PPair _ _ _ x :: PTerm
x y :: PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
warnDisamb ist :: IState
ist (PDPair _ _ _ x :: PTerm
x y :: PTerm
y z :: PTerm
z) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
z
warnDisamb ist :: IState
ist (PAlternative _ _ tms :: [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 ist :: IState
ist (PHidden tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PType _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PUniverse _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PGoal _ x :: PTerm
x _ y :: PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
warnDisamb ist :: IState
ist (PConstant _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist Placeholder = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PDoBlock steps :: [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 _ x :: PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
        wStep (DoBind _ _ _ x :: PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
        wStep (DoBindP _ x :: PTerm
x y :: PTerm
y cs :: [(PTerm, PTerm)]
cs) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
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_ (\(x :: PTerm
x,y :: PTerm
y) -> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
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 _ _ _ _ x :: PTerm
x y :: PTerm
y) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y
        wStep (DoLetP _ x :: PTerm
x y :: PTerm
y cs :: [(PTerm, PTerm)]
cs) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
y Idris () -> Idris () -> Idris ()
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_ (\(x :: PTerm
x,y :: PTerm
y) -> IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x Idris () -> Idris () -> Idris ()
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 _ h :: PTerm
h) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
h
warnDisamb ist :: IState
ist (PIdiom _ x :: PTerm
x) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
x
warnDisamb ist :: IState
ist (PMetavar _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PProof tacs :: [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 ist :: IState
ist (PTactics tacs :: [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 ist :: IState
ist (PElabError _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist PImpossible = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PCoerced tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PDisamb ds :: [[Text]]
ds tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm Idris () -> Idris () -> Idris ()
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 d :: [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
$
              "Nothing found in namespace \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++
              String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ((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]
++
              "\"."
        isIn :: [Text] -> Name -> Bool
isIn d :: [Text]
d (NS _ ns :: [Text]
ns) = [Text] -> [Text] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [Text]
d [Text]
ns
        isIn d :: [Text]
d _ = Bool
False

warnDisamb ist :: IState
ist (PUnifyLog tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PNoImplicits tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PQuasiquote tm :: PTerm
tm goal :: Maybe PTerm
goal) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm Idris () -> Idris () -> Idris ()
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 ist :: IState
ist (PUnquote tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PQuoteName _ _ _) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
warnDisamb ist :: IState
ist (PAs _ _ tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PAppImpl tm :: PTerm
tm _) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PRunElab _ tm :: PTerm
tm _) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm
warnDisamb ist :: IState
ist (PConstSugar _ tm :: PTerm
tm) = IState -> PTerm -> Idris ()
warnDisamb IState
ist PTerm
tm