summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Trace.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Trace.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Trace.hs25
1 files changed, 23 insertions, 2 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Trace.hs b/src/full/Agda/TypeChecking/Monad/Trace.hs
index a1f7977..91f2d95 100644
--- a/src/full/Agda/TypeChecking/Monad/Trace.hs
+++ b/src/full/Agda/TypeChecking/Monad/Trace.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE CPP #-}
+
module Agda.TypeChecking.Monad.Trace where
import Prelude hiding (null)
@@ -9,11 +11,17 @@ import {-# SOURCE #-} Agda.Interaction.Highlighting.Generate
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Options
import Agda.Utils.Function
+import Agda.Utils.List
+import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
+#include "undefined.h"
+import Agda.Utils.Impossible
+
---------------------------------------------------------------------------
-- * Trace
---------------------------------------------------------------------------
@@ -36,6 +44,16 @@ traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm a -> tcm a
traceCall mkCall m = do
let call = mkCall Nothing
callRange = getRange call
+ -- Andreas, 2015-02-09 Make sure we do not set a range
+ -- outside the current file
+ unlessNull callRange $ \ (Range is) ->
+ unlessNull (mapMaybe srcFile $ map iStart is ++ map iEnd is) $ \ files -> do
+ whenJustM (asks envCurrentPath) $ \ currentFile -> do
+ unlessNull (filter (/= currentFile) files) $ \ wrongFiles -> do
+ reportSLn "impossible" 10 $
+ "Someone is trying to set the current range to " ++ show callRange ++
+ " which is outside of the current file " ++ show currentFile
+ __IMPOSSIBLE__
cl <- liftTCM $ buildClosure call
let trace = local $ foldr (.) id $
[ \e -> e { envCall = Just cl } | interestingCall cl ] ++
@@ -97,5 +115,8 @@ traceCallCPS_ mkCall ret cc =
getCurrentRange :: TCM Range
getCurrentRange = asks envRange
-setCurrentRange :: Range -> TCM a -> TCM a
-setCurrentRange r = applyUnless (null r) $ traceCall $ SetRange r
+-- | Sets the current range (for error messages etc.) to the range
+-- of the given object, if it has a range (i.e., its range is not 'noRange').
+setCurrentRange :: HasRange x => x -> TCM a -> TCM a
+setCurrentRange x = applyUnless (null r) $ traceCall $ SetRange r
+ where r = getRange x