{-# 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
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
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