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