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