1 2module Agda.TypeChecking.Monad.Trace where 3 4import Prelude hiding (null) 5 6import Control.Monad.Except 7import Control.Monad.Reader 8import Control.Monad.State 9import Control.Monad.Trans.Identity 10import Control.Monad.Writer 11 12import qualified Data.Set as Set 13 14import Agda.Syntax.Position 15import qualified Agda.Syntax.Position as P 16 17import Agda.Interaction.Response 18import Agda.Interaction.Highlighting.Precise 19import Agda.Interaction.Highlighting.Range (rToR, minus) 20 21import Agda.TypeChecking.Monad.Base 22 hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype) 23import Agda.TypeChecking.Monad.Debug 24import Agda.TypeChecking.Monad.State 25 26import Agda.Utils.Function 27 28import qualified Agda.Utils.Maybe.Strict as Strict 29import Agda.Utils.Monad 30import Agda.Utils.Null 31import Agda.Utils.Pretty (prettyShow) 32 33--------------------------------------------------------------------------- 34-- * Trace 35--------------------------------------------------------------------------- 36 37interestingCall :: Call -> Bool 38interestingCall = \case 39 InferVar{} -> False 40 InferDef{} -> False 41 CheckArguments _ [] _ _ -> False 42 SetRange{} -> False 43 NoHighlighting{} -> False 44 -- Andreas, 2019-08-07, expanded catch-all pattern. 45 -- The previous presence of a catch-all raises the following question: 46 -- are all of the following really interesting? 47 CheckClause{} -> True 48 CheckLHS{} -> True 49 CheckPattern{} -> True 50 CheckPatternLinearityType{} -> True 51 CheckPatternLinearityValue{} -> True 52 CheckLetBinding{} -> True 53 InferExpr{} -> True 54 CheckExprCall{} -> True 55 CheckDotPattern{} -> True 56 IsTypeCall{} -> True 57 IsType_{} -> True 58 CheckArguments{} -> True 59 CheckMetaSolution{} -> True 60 CheckTargetType{} -> True 61 CheckDataDef{} -> True 62 CheckRecDef{} -> True 63 CheckConstructor{} -> True 64 CheckConstructorFitsIn{} -> True 65 CheckFunDefCall{} -> True 66 CheckPragma{} -> True 67 CheckPrimitive{} -> True 68 CheckIsEmpty{} -> True 69 CheckConfluence{} -> True 70 CheckWithFunctionType{} -> True 71 CheckSectionApplication{} -> True 72 CheckNamedWhere{} -> True 73 ScopeCheckExpr{} -> True 74 ScopeCheckDeclaration{} -> True 75 ScopeCheckLHS{} -> True 76 CheckProjection{} -> True 77 ModuleContents{} -> True 78 79class (MonadTCEnv m, ReadTCState m) => MonadTrace m where 80 81 -- | Record a function call in the trace. 82 traceCall :: Call -> m a -> m a 83 traceCall call m = do 84 cl <- buildClosure call 85 traceClosureCall cl m 86 87 traceCallM :: m Call -> m a -> m a 88 traceCallM call m = flip traceCall m =<< call 89 90 -- | Reset 'envCall' to previous value in the continuation. 91 -- 92 -- Caveat: if the last 'traceCall' did not set an 'interestingCall', 93 -- for example, only set the 'Range' with 'SetRange', 94 -- we will revert to the last interesting call. 95 traceCallCPS :: Call -> ((a -> m b) -> m b) -> ((a -> m b) -> m b) 96 traceCallCPS call k ret = do 97 mcall <- asksTC envCall 98 traceCall call $ k $ \ a -> do 99 maybe id traceClosureCall mcall $ ret a 100 101 traceClosureCall :: Closure Call -> m a -> m a 102 103 -- | Lispify and print the given highlighting information. 104 printHighlightingInfo :: RemoveTokenBasedHighlighting -> HighlightingInfo -> m () 105 106 default printHighlightingInfo 107 :: (MonadTrans t, MonadTrace n, t n ~ m) 108 => RemoveTokenBasedHighlighting -> HighlightingInfo -> m () 109 printHighlightingInfo r i = lift $ printHighlightingInfo r i 110 111instance MonadTrace m => MonadTrace (IdentityT m) where 112 traceClosureCall c f = IdentityT $ traceClosureCall c $ runIdentityT f 113 114instance MonadTrace m => MonadTrace (ReaderT r m) where 115 traceClosureCall c f = ReaderT $ \r -> traceClosureCall c $ runReaderT f r 116 117instance MonadTrace m => MonadTrace (StateT s m) where 118 traceClosureCall c f = StateT (traceClosureCall c . runStateT f) 119 120instance (MonadTrace m, Monoid w) => MonadTrace (WriterT w m) where 121 traceClosureCall c f = WriterT $ traceClosureCall c $ runWriterT f 122 123instance MonadTrace m => MonadTrace (ExceptT e m) where 124 traceClosureCall c f = ExceptT $ traceClosureCall c $ runExceptT f 125 126instance MonadTrace TCM where 127 traceClosureCall cl m = do 128 -- Andreas, 2016-09-13 issue #2177 129 -- Since the fix of #2092 we may report an error outside the current file. 130 -- (For instance, if we import a module which then happens to have the 131 -- wrong name.) 132 -- Thus, we no longer crash, but just report the alien range. 133 -- -- Andreas, 2015-02-09 Make sure we do not set a range 134 -- -- outside the current file 135 verboseS "check.ranges" 90 $ 136 Strict.whenJust (rangeFile callRange) $ \f -> do 137 currentFile <- asksTC envCurrentPath 138 when (currentFile /= Just f) $ do 139 reportSLn "check.ranges" 90 $ 140 prettyShow call ++ 141 " is setting the current range to " ++ show callRange ++ 142 " which is outside of the current file " ++ show currentFile 143 144 -- Compute update to 'Range' and 'Call' components of 'TCEnv'. 145 let withCall = localTC $ foldr (.) id $ concat $ 146 [ [ \e -> e { envCall = Just cl } | interestingCall call ] 147 , [ \e -> e { envHighlightingRange = callRange } 148 | callHasRange && highlightCall 149 || isNoHighlighting 150 ] 151 , [ \e -> e { envRange = callRange } | callHasRange ] 152 ] 153 154 -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked': 155 ifNotM (pure highlightCall `and2M` do (Interactive ==) . envHighlightingLevel <$> askTC) 156 {-then-} (withCall m) 157 {-else-} $ do 158 oldRange <- envHighlightingRange <$> askTC 159 highlightAsTypeChecked oldRange callRange $ 160 withCall m 161 where 162 call = clValue cl 163 callRange = getRange call 164 callHasRange = not $ null callRange 165 166 -- Should the given call trigger interactive highlighting? 167 highlightCall = case call of 168 CheckClause{} -> True 169 CheckLHS{} -> True 170 CheckPattern{} -> True 171 CheckPatternLinearityType{} -> False 172 CheckPatternLinearityValue{} -> False 173 CheckLetBinding{} -> True 174 InferExpr{} -> True 175 CheckExprCall{} -> True 176 CheckDotPattern{} -> True 177 IsTypeCall{} -> True 178 IsType_{} -> True 179 InferVar{} -> True 180 InferDef{} -> True 181 CheckArguments{} -> True 182 CheckMetaSolution{} -> False 183 CheckTargetType{} -> False 184 CheckDataDef{} -> True 185 CheckRecDef{} -> True 186 CheckConstructor{} -> True 187 CheckConstructorFitsIn{} -> False 188 CheckFunDefCall _ _ _ h -> h 189 CheckPragma{} -> True 190 CheckPrimitive{} -> True 191 CheckIsEmpty{} -> True 192 CheckConfluence{} -> False 193 CheckWithFunctionType{} -> True 194 CheckSectionApplication{} -> True 195 CheckNamedWhere{} -> False 196 ScopeCheckExpr{} -> False 197 ScopeCheckDeclaration{} -> False 198 ScopeCheckLHS{} -> False 199 NoHighlighting{} -> True 200 CheckProjection{} -> False 201 SetRange{} -> False 202 ModuleContents{} -> False 203 204 isNoHighlighting = case call of 205 NoHighlighting{} -> True 206 _ -> False 207 208 printHighlightingInfo remove info = do 209 modToSrc <- useTC stModuleToSource 210 method <- viewTC eHighlightingMethod 211 reportS "highlighting" 50 212 [ "Printing highlighting info:" 213 , show info 214 , " modToSrc = " ++ show modToSrc 215 ] 216 unless (null info) $ do 217 appInteractionOutputCallback $ 218 Resp_HighlightingInfo info remove method modToSrc 219 220 221getCurrentRange :: MonadTCEnv m => m Range 222getCurrentRange = asksTC envRange 223 224-- | Sets the current range (for error messages etc.) to the range 225-- of the given object, if it has a range (i.e., its range is not 'noRange'). 226setCurrentRange :: (MonadTrace m, HasRange x) => x -> m a -> m a 227setCurrentRange x = applyUnless (null r) $ traceCall $ SetRange r 228 where r = getRange x 229 230-- | @highlightAsTypeChecked rPre r m@ runs @m@ and returns its 231-- result. Additionally, some code may be highlighted: 232-- 233-- * If @r@ is non-empty and not a sub-range of @rPre@ (after 234-- 'P.continuousPerLine' has been applied to both): @r@ is 235-- highlighted as being type-checked while @m@ is running (this 236-- highlighting is removed if @m@ completes /successfully/). 237-- 238-- * Otherwise: Highlighting is removed for @rPre - r@ before @m@ 239-- runs, and if @m@ completes successfully, then @rPre - r@ is 240-- highlighted as being type-checked. 241 242highlightAsTypeChecked 243 :: (MonadTrace m) 244 => Range -- ^ @rPre@ 245 -> Range -- ^ @r@ 246 -> m a 247 -> m a 248highlightAsTypeChecked rPre r m 249 | r /= noRange && delta == rPre' = wrap r' highlight clear 250 | otherwise = wrap delta clear highlight 251 where 252 rPre' = rToR (P.continuousPerLine rPre) 253 r' = rToR (P.continuousPerLine r) 254 delta = rPre' `minus` r' 255 clear = mempty 256 highlight = parserBased { otherAspects = Set.singleton TypeChecks } 257 258 wrap rs x y = do 259 p rs x 260 v <- m 261 p rs y 262 return v 263 where 264 p rs x = printHighlightingInfo KeepHighlighting (singleton rs x) 265