<commit_before>{-# LANGUAGE DeriveDataTypeable #-}

module Idris.Error where

import Prelude hiding (catch)
import Idris.AbsSyntax
import Idris.Delaborate
import Idris.Output

import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Constraints

import System.Console.Haskeline
import System.Console.Haskeline.MonadException
import Control.Monad.State.Strict
import Control.Monad.Error (throwError, catchError)
import System.IO.Error(isUserError, ioeGetErrorString)
import Data.Char
import Data.Typeable

iucheck :: Idris ()
iucheck = do tit <- typeInType
             when (not tit) $
                do ist <- getIState
                   (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
                              (\e -> do setErrSpan (getErrSpan e)
                                        iputStrLn (pshow 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
                    let h = idris_outh ist
                    case (e) of
                      At fc e -> do setErrSpan fc
                                    ihWarn h fc $ pprintErr ist e
                      _ -> do setErrSpan (getErrSpan e)
                              ihWarn h 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) = throwError err

tctry :: TC a -> TC a -> Idris a
tctry tc1 tc2
    = case tc1 of
           OK v -> return v<commit_msg>Fix missing function call from 723d972b2<commit_after>{-# LANGUAGE DeriveDataTypeable #-}

module Idris.Error where

import Prelude hiding (catch)
import Idris.AbsSyntax
import Idris.Delaborate
import Idris.Output

import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Constraints

import System.Console.Haskeline
import System.Console.Haskeline.MonadException
import Control.Monad.State.Strict
import Control.Monad.Error (throwError, catchError)
import System.IO.Error(isUserError, ioeGetErrorString)
import Data.Char
import Data.Typeable

iucheck :: Idris ()
iucheck = do tit <- typeInType
             when (not tit) $
                do ist <- getIState
                   (tclift $ ucheck (idris_constraints ist)) `idrisCatch`
                              (\e -> do setErrSpan (getErrSpan e)
                                        iputStrLn (pshow 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
                    let h = idris_outh ist
                    case (unwrap e) of
                      At fc e -> do setErrSpan fc
                                    ihWarn h fc $ pprintErr ist e
                      _ -> do setErrSpan (getErrSpan e)
                              ihWarn h 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) = throwError err

tctry :: TC a -> TC a -> Idris a
tctry tc1 tc2
    = case tc1 of
           OK v -> return v
{'fraction_non_alphanumeric': 0.08184143222506395, 'fraction_numerical': 0.0033248081841432226, 'mean_word_length': 2.111376292760541, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1503404', 'n_tokens_mistral': 1260, 'n_tokens_neox': 1219, 'n_words': 407}