content: {-|
  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 = do tit <- typeInType
               ist <- getIState
               let cs = idris_constraints ist
               logLvl 7 $ "ALL CONSTRAINTS: " ++ show (length (S.toList cs))
               when (not tit) $
                     (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
                                (\e -> do let fc = getErrSpan e
                                          setErrSpan fc
                                          iWarn fc $ pprintErr ist e)
  
  showErr :: Err -> Idris String
  showErr e = getIState >>= return . flip pshow e
  
  
  report :: IOError -> String
  report e
      | isUserError e = ioeGetErrorString e
      | otherwise     = show e
  
  idrisCatch :: Idris a -> (Err -> Idris a) -> Idris a
  idrisCatch = catchError
  
  
  setAndReport :: Err -> Idris ()
  setAndReport e = do ist <- getIState
                      case (unwrap e) of
                        At fc e -> do setErrSpan fc
                                      iWarn fc $ pprintErr ist e
                        _ -> do setErrSpan (getErrSpan e)
                                iWarn emptyFC $ pprintErr ist e
    where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor
          unwrap e = e
  
  ifail :: String -> Idris a
  ifail = throwError . Msg
  
  ierror :: Err -> Idris a
  ierror = throwError
  
  tclift :: TC a -> Idris a
  tclift (OK v) = return v
  tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err
  tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err
  tclift (Error err) = throwError err
  
  tcliftAt :: FC -> TC a -> Idris a
  tcliftAt fc (OK v) = return v
  tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err
  tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err
  tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc err)
  
  tctry :: TC a -> TC a -> Idris a
  tctry tc1 tc2
      = case tc1 of
             OK v -> return v
             Error err -> tclift tc2
  
  getErrSpan :: Err -> FC
  getErrSpan (At fc _) = fc
  getErrSpan (UniverseError fc _ _ _ _) = fc
  getErrSpan _ = emptyFC
  
  --------------------------------------------------------------------
  -- Specific warnings not included in elaborator
  --------------------------------------------------------------------
  -- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
  warnDisamb :: IState -> PTerm -> Idris ()
  warnDisamb ist (PQuote _) = return ()
  warnDisamb ist (PRef _ _ _) = return ()
  warnDisamb ist (PInferRef _ _ _) = return ()
  warnDisamb ist (PPatvar _ _) = return ()
  warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
  warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b
  warnDisamb ist (PLet _ _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
  warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
  warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
                                   mapM_ (warnDisamb ist . getTm) args
  warnDisamb ist (PWithApp _ t a) = warnDisamb ist t >> warnDisamb ist a
  warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
                                       mapM_ (warnDisamb ist . getTm) args
  warnDisamb ist (PMatchApp _ _) = return ()
  warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
                                      mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
  warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]
  warnDisamb ist (PTrue _ _) = return ()
  warnDisamb ist (PResolveTC _) = return ()
  warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
                                        Foldable.mapM_ (warnDisamb ist) z
  warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
  warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
  warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms
  warnDisamb ist (PHidden tm) = warnDisamb ist tm
  warnDisamb ist (PType _) = return ()
  warnDisamb ist (PUniverse _ _) = return ()
  warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
  warnDisamb ist (PConstant _ _) = return ()
  warnDisamb ist Placeholder = return ()
  warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
    where wStep (DoExp _ x) = warnDisamb ist x
          wStep (DoBind _ _ _ x) = warnDisamb ist x
          wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
                                     mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
          wStep (DoLet _ _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y
          wStep (DoLetP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
                                    mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs
          wStep (DoRewrite _ h) = warnDisamb ist h
  warnDisamb ist (PIdiom _ x) = warnDisamb ist x
  warnDisamb ist (PMetavar _ _) = return ()
  warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
  warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
  warnDisamb ist (PElabError _) = return ()
  warnDisamb ist PImpossible = return ()
  warnDisamb ist (PCoerced tm) = warnDisamb ist tm
  warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
                                   mapM_ warnEmpty ds
    where warnEmpty d =
            when (not (any (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
              ierror . Msg $
                "Nothing found in namespace \"" ++
                intercalate "." (map T.unpack . reverse $ d) ++
                "\"."
          isIn d (NS _ ns) = isPrefixOf d ns
          isIn d _ = False
  
  warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
  warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
  warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
                                         Foldable.mapM_ (warnDisamb ist) goal
  warnDisamb ist (PUnquote tm) = warnDisamb ist tm
  warnDisamb ist (PQuoteName _ _ _) = return ()
  warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm
  warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm
  warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm
  warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm
  