1-- | Lenses for 'TCState' and more.
2
3module Agda.TypeChecking.Monad.State where
4
5
6import qualified Control.Exception as E
7
8import Control.Monad.State (void)
9import Control.Monad.Trans (MonadIO, liftIO)
10
11import Data.Maybe
12
13import qualified Data.Map as Map
14
15import qualified Data.List.NonEmpty as NonEmpty
16import Data.Set (Set)
17import qualified Data.Set as Set
18import qualified Data.HashMap.Strict as HMap
19
20import Agda.Benchmarking
21
22import Agda.Interaction.Response
23  (InteractionOutputCallback, Response)
24
25import Agda.Syntax.Common
26import Agda.Syntax.Scope.Base
27import qualified Agda.Syntax.Concrete.Name as C
28import Agda.Syntax.Abstract (PatternSynDefn, PatternSynDefns)
29import Agda.Syntax.Abstract.PatternSynonyms
30import Agda.Syntax.Abstract.Name
31import Agda.Syntax.Internal
32
33import Agda.TypeChecking.Monad.Base
34import Agda.TypeChecking.Warnings
35
36import Agda.TypeChecking.Monad.Debug (reportSDoc, reportSLn, verboseS)
37import Agda.TypeChecking.Positivity.Occurrence
38import Agda.TypeChecking.CompiledClause
39
40import Agda.Utils.Hash
41import Agda.Utils.Lens
42import Agda.Utils.Monad (bracket_)
43import Agda.Utils.Pretty
44import Agda.Utils.Tuple
45
46import Agda.Utils.Impossible
47
48-- | Resets the non-persistent part of the type checking state.
49
50resetState :: TCM ()
51resetState = do
52    pers <- getsTC stPersistentState
53    putTC $ initState { stPersistentState = pers }
54
55-- | Resets all of the type checking state.
56--
57--   Keep only 'Benchmark' and backend information.
58
59resetAllState :: TCM ()
60resetAllState = do
61    b <- getBenchmark
62    backends <- useTC stBackends
63    putTC $ updatePersistentState (\ s -> s { stBenchmark = b }) initState
64    stBackends `setTCLens` backends
65-- resetAllState = putTC initState
66
67-- | Restore 'TCState' after performing subcomputation.
68--
69--   In contrast to 'Agda.Utils.Monad.localState', the 'Benchmark'
70--   info from the subcomputation is saved.
71localTCState :: TCM a -> TCM a
72localTCState = bracket_ getTC (\ s -> do
73   b <- getBenchmark
74   putTC s
75   modifyBenchmark $ const b)
76
77-- | Same as 'localTCState' but also returns the state in which we were just
78--   before reverting it.
79localTCStateSaving :: TCM a -> TCM (a, TCState)
80localTCStateSaving compute = do
81  oldState <- getTC
82  result <- compute
83  newState <- getTC
84  do
85    b <- getBenchmark
86    putTC oldState
87    modifyBenchmark $ const b
88  return (result, newState)
89
90-- | Same as 'localTCState' but keep all warnings.
91localTCStateSavingWarnings :: TCM a -> TCM a
92localTCStateSavingWarnings compute = do
93  (result, newState) <- localTCStateSaving compute
94  modifyTC $ over stTCWarnings $ const $ newState ^. stTCWarnings
95  return result
96
97data SpeculateResult = SpeculateAbort | SpeculateCommit
98
99-- | Allow rolling back the state changes of a TCM computation.
100speculateTCState :: TCM (a, SpeculateResult) -> TCM a
101speculateTCState m = do
102  ((x, res), newState) <- localTCStateSaving m
103  case res of
104    SpeculateAbort  -> return x
105    SpeculateCommit -> x <$ putTC newState
106
107speculateTCState_ :: TCM SpeculateResult -> TCM ()
108speculateTCState_ m = void $ speculateTCState $ ((),) <$> m
109
110-- | A fresh TCM instance.
111--
112-- The computation is run in a fresh state, with the exception that
113-- the persistent state is preserved. If the computation changes the
114-- state, then these changes are ignored, except for changes to the
115-- persistent state. (Changes to the persistent state are also ignored
116-- if errors other than type errors or IO exceptions are encountered.)
117
118freshTCM :: TCM a -> TCM (Either TCErr a)
119freshTCM m = do
120  ps <- useTC lensPersistentState
121  let s = set lensPersistentState ps initState
122  r <- liftIO $ (Right <$> runTCM initEnv s m) `E.catch` (return . Left)
123  case r of
124    Right (a, s) -> do
125      setTCLens lensPersistentState $ s ^. lensPersistentState
126      return $ Right a
127    Left err -> do
128      case err of
129        TypeError { tcErrState = s } ->
130          setTCLens lensPersistentState $ s ^. lensPersistentState
131        IOException s _ _ ->
132          setTCLens lensPersistentState $ s ^. lensPersistentState
133        _ -> return ()
134      return $ Left err
135
136---------------------------------------------------------------------------
137-- * Lens for persistent states and its fields
138---------------------------------------------------------------------------
139
140lensPersistentState :: Lens' PersistentTCState TCState
141lensPersistentState f s =
142  f (stPersistentState s) <&> \ p -> s { stPersistentState = p }
143
144updatePersistentState
145  :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
146updatePersistentState f s = s { stPersistentState = f (stPersistentState s) }
147
148modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
149modifyPersistentState = modifyTC . updatePersistentState
150
151-- | Lens for 'stAccumStatistics'.
152
153lensAccumStatisticsP :: Lens' Statistics PersistentTCState
154lensAccumStatisticsP f s = f (stAccumStatistics s) <&> \ a ->
155  s { stAccumStatistics = a }
156
157lensAccumStatistics :: Lens' Statistics TCState
158lensAccumStatistics =  lensPersistentState . lensAccumStatisticsP
159
160---------------------------------------------------------------------------
161-- * Scope
162---------------------------------------------------------------------------
163
164-- | Get the current scope.
165getScope :: ReadTCState m => m ScopeInfo
166getScope = useR stScope
167
168-- | Set the current scope.
169setScope :: ScopeInfo -> TCM ()
170setScope scope = modifyScope (const scope)
171
172-- | Modify the current scope without updating the inverse maps.
173modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
174modifyScope_ f = stScope `modifyTCLens` f
175
176-- | Modify the current scope.
177modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
178modifyScope f = modifyScope_ (recomputeInverseScopeMaps . f)
179
180-- | Get a part of the current scope.
181useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
182useScope l = useR $ stScope . l
183
184-- | Run a computation in a modified scope.
185locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
186locallyScope l = locallyTCState $ stScope . l
187
188-- | Run a computation in a local scope.
189withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
190withScope s m = locallyTCState stScope (recomputeInverseScopeMaps . const s) $ (,) <$> m <*> getScope
191
192-- | Same as 'withScope', but discard the scope from the computation.
193withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
194withScope_ s m = fst <$> withScope s m
195
196-- | Discard any changes to the scope by a computation.
197localScope :: TCM a -> TCM a
198localScope m = do
199  scope <- getScope
200  x <- m
201  setScope scope
202  return x
203
204-- | Scope error.
205notInScopeError :: C.QName -> TCM a
206notInScopeError x = do
207  printScope "unbound" 5 ""
208  typeError $ NotInScope [x]
209
210notInScopeWarning :: C.QName -> TCM ()
211notInScopeWarning x = do
212  printScope "unbound" 5 ""
213  warning $ NotInScopeW [x]
214
215-- | Debug print the scope.
216printScope :: String -> Int -> String -> TCM ()
217printScope tag v s = verboseS ("scope." ++ tag) v $ do
218  scope <- getScope
219  reportSDoc ("scope." ++ tag) v $ return $ vcat [ text s, pretty scope ]
220
221---------------------------------------------------------------------------
222-- * Signature
223---------------------------------------------------------------------------
224
225-- ** Lens for 'stSignature' and 'stImports'
226
227modifySignature :: MonadTCState m => (Signature -> Signature) -> m ()
228modifySignature f = stSignature `modifyTCLens` f
229
230modifyImportedSignature :: MonadTCState m => (Signature -> Signature) -> m ()
231modifyImportedSignature f = stImports `modifyTCLens` f
232
233getSignature :: ReadTCState m => m Signature
234getSignature = useR stSignature
235
236-- | Update a possibly imported definition. Warning: changes made to imported
237--   definitions (during type checking) will not persist outside the current
238--   module. This function is currently used to update the compiled
239--   representation of a function during compilation.
240modifyGlobalDefinition :: MonadTCState m => QName -> (Definition -> Definition) -> m ()
241modifyGlobalDefinition q f = do
242  modifySignature         $ updateDefinition q f
243  modifyImportedSignature $ updateDefinition q f
244
245setSignature :: MonadTCState m => Signature -> m ()
246setSignature sig = modifySignature $ const sig
247
248-- | Run some computation in a different signature, restore original signature.
249withSignature :: (ReadTCState m, MonadTCState m) => Signature -> m a -> m a
250withSignature sig m = do
251  sig0 <- getSignature
252  setSignature sig
253  r <- m
254  setSignature sig0
255  return r
256
257-- ** Modifiers for rewrite rules
258addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
259addRewriteRulesFor f rews matchables =
260    over sigRewriteRules (HMap.insertWith mappend f rews)
261  . updateDefinition f (updateTheDef setNotInjective . setCopatternLHS)
262  . (setMatchableSymbols f matchables)
263    where
264      setNotInjective def@Function{} = def { funInv = NotInjective }
265      setNotInjective def            = def
266
267      setCopatternLHS =
268        updateDefCopatternLHS (|| any hasProjectionPattern rews)
269
270      hasProjectionPattern rew = any (isJust . isProjElim) $ rewPats rew
271
272setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
273setMatchableSymbols f matchables =
274  foldr ((.) . (\g -> updateDefinition g setMatchable)) id matchables
275    where
276      setMatchable def = def { defMatchable = Set.insert f $ defMatchable def }
277
278-- ** Modifiers for parts of the signature
279
280lookupDefinition :: QName -> Signature -> Maybe Definition
281lookupDefinition q sig = HMap.lookup q $ sig ^. sigDefinitions
282
283updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
284updateDefinitions = over sigDefinitions
285
286updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
287updateDefinition q f = updateDefinitions $ HMap.adjust f q
288
289updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
290updateTheDef f def = def { theDef = f (theDef def) }
291
292updateDefType :: (Type -> Type) -> (Definition -> Definition)
293updateDefType f def = def { defType = f (defType def) }
294
295updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> (Definition -> Definition)
296updateDefArgOccurrences f def = def { defArgOccurrences = f (defArgOccurrences def) }
297
298updateDefPolarity :: ([Polarity] -> [Polarity]) -> (Definition -> Definition)
299updateDefPolarity f def = def { defPolarity = f (defPolarity def) }
300
301updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
302updateDefCompiledRep f def = def { defCompiledRep = f (defCompiledRep def) }
303
304addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
305addCompilerPragma backend pragma = updateDefCompiledRep $ Map.insertWith (++) backend [pragma]
306
307updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
308updateFunClauses f def@Function{ funClauses = cs} = def { funClauses = f cs }
309updateFunClauses f _                              = __IMPOSSIBLE__
310
311updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
312updateCovering f def@Function{ funCovering = cs} = def { funCovering = f cs }
313updateCovering f _                               = __IMPOSSIBLE__
314
315updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
316updateCompiledClauses f def@Function{ funCompiled = cc} = def { funCompiled = f cc }
317updateCompiledClauses f _                              = __IMPOSSIBLE__
318
319updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
320updateDefCopatternLHS f def@Defn{ defCopatternLHS = b } = def { defCopatternLHS = f b }
321
322updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
323updateDefBlocked f def@Defn{ defBlocked = b } = def { defBlocked = f b }
324
325---------------------------------------------------------------------------
326-- * Top level module
327---------------------------------------------------------------------------
328
329-- | Set the top-level module. This affects the global module id of freshly
330--   generated names.
331
332-- TODO: Is the hash-function collision-free? If not, then the
333-- implementation of 'setTopLevelModule' should be changed.
334
335setTopLevelModule :: C.QName -> TCM ()
336setTopLevelModule x = stFreshNameId `setTCLens` NameId 0 (ModuleNameHash $ hashString $ prettyShow x)
337
338-- | Use a different top-level module for a computation. Used when generating
339--   names for imported modules.
340withTopLevelModule :: C.QName -> TCM a -> TCM a
341withTopLevelModule x m = do
342  next <- useTC stFreshNameId
343  setTopLevelModule x
344  y <- m
345  stFreshNameId `setTCLens` next
346  return y
347
348currentModuleNameHash :: ReadTCState m => m ModuleNameHash
349currentModuleNameHash = do
350  NameId _ h <- useTC stFreshNameId
351  return h
352
353---------------------------------------------------------------------------
354-- * Foreign code
355---------------------------------------------------------------------------
356
357addForeignCode :: BackendName -> String -> TCM ()
358addForeignCode backend code = do
359  r <- asksTC envRange  -- can't use TypeChecking.Monad.Trace.getCurrentRange without cycle
360  modifyTCLens (stForeignCode . key backend) $ Just . (ForeignCode r code :) . fromMaybe []
361
362---------------------------------------------------------------------------
363-- * Interaction output callback
364---------------------------------------------------------------------------
365
366getInteractionOutputCallback :: ReadTCState m => m InteractionOutputCallback
367getInteractionOutputCallback
368  = getsTC $ stInteractionOutputCallback . stPersistentState
369
370appInteractionOutputCallback :: Response -> TCM ()
371appInteractionOutputCallback r
372  = getInteractionOutputCallback >>= \ cb -> cb r
373
374setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
375setInteractionOutputCallback cb
376  = modifyPersistentState $ \ s -> s { stInteractionOutputCallback = cb }
377
378---------------------------------------------------------------------------
379-- * Pattern synonyms
380---------------------------------------------------------------------------
381
382getPatternSyns :: ReadTCState m => m PatternSynDefns
383getPatternSyns = useR stPatternSyns
384
385setPatternSyns :: PatternSynDefns -> TCM ()
386setPatternSyns m = modifyPatternSyns (const m)
387
388-- | Lens for 'stPatternSyns'.
389modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
390modifyPatternSyns f = stPatternSyns `modifyTCLens` f
391
392getPatternSynImports :: ReadTCState m => m PatternSynDefns
393getPatternSynImports = useR stPatternSynImports
394
395-- | Get both local and imported pattern synonyms
396getAllPatternSyns :: ReadTCState m => m PatternSynDefns
397getAllPatternSyns = Map.union <$> getPatternSyns <*> getPatternSynImports
398
399lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
400lookupPatternSyn (AmbQ xs) = do
401  defs <- traverse lookupSinglePatternSyn xs
402  case mergePatternSynDefs defs of
403    Just def   -> return def
404    Nothing    -> typeError $ CannotResolveAmbiguousPatternSynonym (NonEmpty.zip xs defs)
405
406lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
407lookupSinglePatternSyn x = do
408    s <- getPatternSyns
409    case Map.lookup x s of
410        Just d  -> return d
411        Nothing -> do
412            si <- getPatternSynImports
413            case Map.lookup x si of
414                Just d  -> return d
415                Nothing -> notInScopeError $ qnameToConcrete x
416
417---------------------------------------------------------------------------
418-- * Benchmark
419---------------------------------------------------------------------------
420
421-- | Lens getter for 'Benchmark' from 'TCState'.
422theBenchmark :: TCState -> Benchmark
423theBenchmark = stBenchmark . stPersistentState
424
425-- | Lens map for 'Benchmark'.
426updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
427updateBenchmark f = updatePersistentState $ \ s -> s { stBenchmark = f (stBenchmark s) }
428
429-- | Lens getter for 'Benchmark' from 'TCM'.
430getBenchmark :: TCM Benchmark
431getBenchmark = getsTC $ theBenchmark
432
433-- | Lens modify for 'Benchmark'.
434modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
435modifyBenchmark = modifyTC' . updateBenchmark
436
437---------------------------------------------------------------------------
438-- * Instance definitions
439---------------------------------------------------------------------------
440
441-- | Look through the signature and reconstruct the instance table.
442addImportedInstances :: Signature -> TCM ()
443addImportedInstances sig = do
444  let itable = Map.fromListWith Set.union
445               [ (c, Set.singleton i)
446               | (i, Defn{ defInstance = Just c }) <- HMap.toList $ sig ^. sigDefinitions ]
447  stImportedInstanceDefs `modifyTCLens` Map.unionWith Set.union itable
448
449-- | Lens for 'stInstanceDefs'.
450updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
451updateInstanceDefs = over stInstanceDefs
452
453modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
454modifyInstanceDefs = modifyTC . updateInstanceDefs
455
456getAllInstanceDefs :: TCM TempInstanceTable
457getAllInstanceDefs = do
458  (table,xs) <- useTC stInstanceDefs
459  itable <- useTC stImportedInstanceDefs
460  let !table' = Map.unionWith Set.union itable table
461  return (table', xs)
462
463getAnonInstanceDefs :: TCM (Set QName)
464getAnonInstanceDefs = snd <$> getAllInstanceDefs
465
466-- | Remove all instances whose type is still unresolved.
467clearAnonInstanceDefs :: TCM ()
468clearAnonInstanceDefs = modifyInstanceDefs $ mapSnd $ const Set.empty
469
470-- | Add an instance whose type is still unresolved.
471addUnknownInstance :: QName -> TCM ()
472addUnknownInstance x = do
473  reportSLn "tc.decl.instance" 10 $
474    "adding definition " ++ prettyShow x ++
475    " to the instance table (the type is not yet known)"
476  modifyInstanceDefs $ mapSnd $ Set.insert x
477
478-- | Add instance to some ``class''.
479addNamedInstance
480  :: QName  -- ^ Name of the instance.
481  -> QName  -- ^ Name of the class.
482  -> TCM ()
483addNamedInstance x n = do
484  reportSLn "tc.decl.instance" 10 $
485    "adding definition " ++ prettyShow x ++ " to instance table for " ++ prettyShow n
486  -- Mark x as instance for n.
487  modifySignature $ updateDefinition x $ \ d -> d { defInstance = Just n }
488  -- Add x to n's instances.
489  modifyInstanceDefs $ mapFst $ Map.insertWith Set.union n $ Set.singleton x
490