1{-# LANGUAGE NondecreasingIndentation #-} 2 3module Agda.TypeChecking.Monad.Signature where 4 5import Prelude hiding (null) 6 7import qualified Control.Monad.Fail as Fail 8 9import Control.Arrow (first, second) 10import Control.Monad.Except 11import Control.Monad.State 12import Control.Monad.Reader 13import Control.Monad.Writer hiding ((<>)) 14import Control.Monad.Trans.Maybe 15import Control.Monad.Trans.Identity 16 17import Data.Foldable (for_) 18import qualified Data.List as List 19import Data.Set (Set) 20import qualified Data.Set as Set 21import qualified Data.Map as Map 22import qualified Data.HashMap.Strict as HMap 23import Data.Maybe 24import Data.Semigroup ((<>)) 25 26import Agda.Syntax.Abstract.Name 27import Agda.Syntax.Abstract (Ren, ScopeCopyInfo(..)) 28import Agda.Syntax.Common 29import Agda.Syntax.Internal as I 30import Agda.Syntax.Internal.Names 31import Agda.Syntax.Position 32import Agda.Syntax.Treeless (Compiled(..), TTerm, ArgUsage) 33 34import Agda.TypeChecking.Monad.Base 35import Agda.TypeChecking.Monad.Builtin 36import Agda.TypeChecking.Monad.Debug 37import Agda.TypeChecking.Monad.Context 38import Agda.TypeChecking.Monad.Env 39import Agda.TypeChecking.Monad.Mutual 40import Agda.TypeChecking.Monad.Open 41import Agda.TypeChecking.Monad.State 42import Agda.TypeChecking.Monad.Trace 43import Agda.TypeChecking.DropArgs 44import Agda.TypeChecking.Warnings 45import Agda.TypeChecking.Positivity.Occurrence 46import Agda.TypeChecking.Substitute 47import Agda.TypeChecking.CompiledClause 48import Agda.TypeChecking.Coverage.SplitTree 49import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile 50import {-# SOURCE #-} Agda.TypeChecking.Polarity 51import {-# SOURCE #-} Agda.TypeChecking.Pretty 52import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike 53import {-# SOURCE #-} Agda.TypeChecking.Reduce 54 55import {-# SOURCE #-} Agda.Compiler.Treeless.Erase 56import {-# SOURCE #-} Agda.Compiler.Builtin 57 58import Agda.Utils.Either 59import Agda.Utils.Functor 60import Agda.Utils.Lens 61import Agda.Utils.List 62import qualified Agda.Utils.List1 as List1 63import Agda.Utils.ListT 64import Agda.Utils.Maybe 65import Agda.Utils.Monad 66import Agda.Utils.Null 67import Agda.Utils.Pretty (prettyShow) 68import Agda.Utils.Singleton 69import Agda.Utils.Size 70import Agda.Utils.Update 71 72import Agda.Utils.Impossible 73 74-- | Add a constant to the signature. Lifts the definition to top level. 75addConstant :: QName -> Definition -> TCM () 76addConstant q d = do 77 reportSDoc "tc.signature" 20 $ "adding constant " <+> pretty q <+> " to signature" 78 tel <- getContextTelescope 79 let tel' = replaceEmptyName "r" $ killRange $ case theDef d of 80 Constructor{} -> fmap hideOrKeepInstance tel 81 Function{ funProjection = Just Projection{ projProper = Just{}, projIndex = n } } -> 82 let fallback = fmap hideOrKeepInstance tel in 83 if n > 0 then fallback else 84 -- if the record value is part of the telescope, its hiding should left unchanged 85 case initLast $ telToList tel of 86 Nothing -> fallback 87 Just (doms, dom) -> telFromList $ fmap hideOrKeepInstance doms ++ [dom] 88 _ -> tel 89 let d' = abstract tel' $ d { defName = q } 90 reportSDoc "tc.signature" 60 $ "lambda-lifted definition =" <?> pretty d' 91 modifySignature $ updateDefinitions $ HMap.insertWith (+++) q d' 92 i <- currentOrFreshMutualBlock 93 setMutualBlock i q 94 where 95 new +++ old = new { defDisplay = defDisplay new ++ defDisplay old 96 , defInstance = defInstance new `mplus` defInstance old } 97 98-- | Set termination info of a defined function symbol. 99setTerminates :: QName -> Bool -> TCM () 100setTerminates q b = modifySignature $ updateDefinition q $ updateTheDef $ \case 101 def@Function{} -> def { funTerminates = Just b } 102 def -> def 103 104-- | Set CompiledClauses of a defined function symbol. 105setCompiledClauses :: QName -> CompiledClauses -> TCM () 106setCompiledClauses q cc = modifySignature $ updateDefinition q $ updateTheDef $ setT 107 where 108 setT def@Function{} = def { funCompiled = Just cc } 109 setT def = def 110 111-- | Set SplitTree of a defined function symbol. 112setSplitTree :: QName -> SplitTree -> TCM () 113setSplitTree q st = modifySignature $ updateDefinition q $ updateTheDef $ setT 114 where 115 setT def@Function{} = def { funSplitTree = Just st } 116 setT def = def 117 118-- | Modify the clauses of a function. 119modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () 120modifyFunClauses q f = 121 modifySignature $ updateDefinition q $ updateTheDef $ updateFunClauses f 122 123-- | Lifts clauses to the top-level and adds them to definition. 124-- Also adjusts the 'funCopatternLHS' field if necessary. 125addClauses :: QName -> [Clause] -> TCM () 126addClauses q cls = do 127 tel <- getContextTelescope 128 modifySignature $ updateDefinition q $ 129 updateTheDef (updateFunClauses (++ abstract tel cls)) 130 . updateDefCopatternLHS (|| isCopatternLHS cls) 131 132mkPragma :: String -> TCM CompilerPragma 133mkPragma s = CompilerPragma <$> getCurrentRange <*> pure s 134 135-- | Add a compiler pragma `{-\# COMPILE <backend> <name> <text> \#-}` 136addPragma :: BackendName -> QName -> String -> TCM () 137addPragma b q s = ifM erased 138 {- then -} (warning $ PragmaCompileErased b q) 139 {- else -} $ do 140 pragma <- mkPragma s 141 modifySignature $ updateDefinition q $ addCompilerPragma b pragma 142 143 where 144 145 erased :: TCM Bool 146 erased = do 147 def <- theDef <$> getConstInfo q 148 case def of 149 -- If we have a defined symbol, we check whether it is erasable 150 Function{} -> 151 locallyTC eActiveBackendName (const $ Just b) $ 152 locallyTCState stBackends (const $ builtinBackends) $ 153 isErasable q 154 -- Otherwise (Axiom, Datatype, Record type, etc.) we keep it 155 _ -> pure False 156 157getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma) 158getUniqueCompilerPragma backend q = do 159 ps <- defCompilerPragmas backend <$> getConstInfo q 160 case ps of 161 [] -> return Nothing 162 [p] -> return $ Just p 163 (_:p1:_) -> 164 setCurrentRange p1 $ 165 genericDocError =<< do 166 hang (text ("Conflicting " ++ backend ++ " pragmas for") <+> pretty q <+> "at") 2 $ 167 vcat [ "-" <+> pretty (getRange p) | p <- ps ] 168 169setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM () 170setFunctionFlag flag val q = modifyGlobalDefinition q $ set (theDefLens . funFlag flag) val 171 172markStatic :: QName -> TCM () 173markStatic = setFunctionFlag FunStatic True 174 175markInline :: Bool -> QName -> TCM () 176markInline b = setFunctionFlag FunInline b 177 178markInjective :: QName -> TCM () 179markInjective q = modifyGlobalDefinition q $ \def -> def { defInjective = True } 180 181unionSignatures :: [Signature] -> Signature 182unionSignatures ss = foldr unionSignature emptySignature ss 183 where 184 unionSignature (Sig a b c) (Sig a' b' c') = 185 Sig (Map.union a a') 186 (HMap.union b b') -- definitions are unique (in at most one module) 187 (HMap.unionWith mappend c c') -- rewrite rules are accumulated 188 189-- | Add a section to the signature. 190-- 191-- The current context will be stored as the cumulative module parameters 192-- for this section. 193addSection :: ModuleName -> TCM () 194addSection m = do 195 tel <- getContextTelescope 196 let sec = Section tel 197 -- Make sure we do not overwrite an existing section! 198 whenJustM (getSection m) $ \ sec' -> do 199 -- At least not with different content! 200 if (sec == sec') then do 201 -- Andreas, 2015-12-02: test/Succeed/Issue1701II.agda 202 -- reports a "redundantly adding existing section". 203 reportSDoc "tc.section" 10 $ "warning: redundantly adding existing section" <+> pretty m 204 reportSDoc "tc.section" 60 $ "with content" <+> pretty sec 205 else do 206 reportSDoc "impossible" 10 $ "overwriting existing section" <+> pretty m 207 reportSDoc "impossible" 60 $ "of content " <+> pretty sec' 208 reportSDoc "impossible" 60 $ "with content" <+> pretty sec 209 __IMPOSSIBLE__ 210 -- Add the new section. 211 setModuleCheckpoint m 212 modifySignature $ over sigSections $ Map.insert m sec 213 214-- | Sets the checkpoint for the given module to the current checkpoint. 215setModuleCheckpoint :: ModuleName -> TCM () 216setModuleCheckpoint m = do 217 chkpt <- viewTC eCurrentCheckpoint 218 stModuleCheckpoints `modifyTCLens` Map.insert m chkpt 219 220-- | Get a section. 221-- 222-- Why Maybe? The reason is that we look up all prefixes of a module to 223-- compute number of parameters, and for hierarchical top-level modules, 224-- A.B.C say, A and A.B do not exist. 225{-# SPECIALIZE getSection :: ModuleName -> TCM (Maybe Section) #-} 226{-# SPECIALIZE getSection :: ModuleName -> ReduceM (Maybe Section) #-} 227getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section) 228getSection m = do 229 sig <- (^. stSignature . sigSections) <$> getTCState 230 isig <- (^. stImports . sigSections) <$> getTCState 231 return $ Map.lookup m sig `mplus` Map.lookup m isig 232 233-- | Lookup a section telescope. 234-- 235-- If it doesn't exist, like in hierarchical top-level modules, 236-- the section telescope is empty. 237{-# SPECIALIZE lookupSection :: ModuleName -> TCM Telescope #-} 238{-# SPECIALIZE lookupSection :: ModuleName -> ReduceM Telescope #-} 239lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope 240lookupSection m = maybe EmptyTel (^. secTelescope) <$> getSection m 241 242-- | Add display forms for a name @f@ copied by a module application. Essentially if @f@ can reduce to 243-- 244-- @ 245-- λ xs → A.B.C.f vs 246-- @ 247-- 248-- by unfolding module application copies (`defCopy`), then we add a display form 249-- 250-- @ 251-- A.B.C.f vs ==> f xs 252-- @ 253addDisplayForms :: QName -> TCM () 254addDisplayForms x = do 255 reportSDoc "tc.display.section" 20 $ "Computing display forms for" <+> pretty x 256 def <- theDef <$> getConstInfo x 257 let v = case def of 258 Constructor{conSrcCon = h} -> Con h{ conName = x } ConOSystem [] 259 _ -> Def x [] 260 261 -- Compute all unfoldings of x by repeatedly calling reduceDefCopy 262 vs <- unfoldings x v 263 reportSDoc "tc.display.section" 20 $ nest 2 $ vcat 264 [ "unfoldings:" <?> vcat [ "-" <+> pretty v | v <- vs ] ] 265 266 -- Turn unfoldings into display forms 267 npars <- subtract (projectionArgs def) <$> getContextSize 268 let dfs = catMaybes $ map (displayForm npars v) vs 269 reportSDoc "tc.display.section" 20 $ nest 2 $ vcat 270 [ "displayForms:" <?> vcat [ "-" <+> (pretty y <+> "-->" <?> pretty df) | (y, df) <- dfs ] ] 271 272 -- and add them 273 mapM_ (uncurry addDisplayForm) dfs 274 where 275 276 -- To get display forms for projections we need to unSpine here. 277 view :: Term -> ([Arg ArgName], Term) 278 view = second unSpine . lamView 279 280 -- Given an unfolding `top = λ xs → y es` generate a display form 281 -- `y es ==> top xs`. The first `npars` variables in `xs` are module parameters 282 -- and should not be pattern variables, but matched literally. 283 displayForm :: Nat -> Term -> Term -> Maybe (QName, DisplayForm) 284 displayForm npars top v = 285 case view v of 286 (xs, Def y es) -> (y,) <$> mkDisplay xs es 287 (xs, Con h i es) -> (conName h,) <$> mkDisplay xs es 288 _ -> __IMPOSSIBLE__ 289 where 290 mkDisplay xs es = Just (Display (n - npars) es $ DTerm $ top `apply` args) 291 where 292 n = length xs 293 args = zipWith (\ x i -> var i <$ x) xs (downFrom n) 294 295 -- Unfold a single defCopy. 296 unfoldOnce :: Term -> TCM (Reduced () Term) 297 unfoldOnce v = case view v of 298 (xs, Def f es) -> (fmap . fmap) (unlamView xs) (reduceDefCopyTCM f es) 299 (xs, Con c i es) -> (fmap . fmap) (unlamView xs) (reduceDefCopyTCM (conName c) es) 300 _ -> pure $ NoReduction () 301 302 -- Compute all reduceDefCopy unfoldings of `x`. Stop when we hit a non-copy. 303 unfoldings :: QName -> Term -> TCM [Term] 304 unfoldings x v = unfoldOnce v >>= \ case 305 NoReduction{} -> return [] 306 YesReduction _ v' -> do 307 let headSymbol = case snd $ view v' of 308 Def y _ -> Just y 309 Con y _ _ -> Just (conName y) 310 _ -> Nothing 311 case headSymbol of 312 Nothing -> return [] 313 Just y | x == y -> do 314 -- This should never happen, but if it does, getting an __IMPOSSIBLE__ is much better 315 -- than looping. 316 reportSDoc "impossible" 10 $ nest 2 $ vcat 317 [ "reduceDefCopy said YesReduction but the head symbol is the same!?" 318 , nest 2 $ "v =" <+> pretty v 319 , nest 2 $ "v' =" <+> pretty v' 320 ] 321 __IMPOSSIBLE__ 322 Just y -> do 323 ifM (defCopy <$> getConstInfo y) 324 ((v' :) <$> unfoldings y v') -- another copy so keep going 325 (return [v']) -- not a copy, we stop 326 327-- | Module application (followed by module parameter abstraction). 328applySection 329 :: ModuleName -- ^ Name of new module defined by the module macro. 330 -> Telescope -- ^ Parameters of new module. 331 -> ModuleName -- ^ Name of old module applied to arguments. 332 -> Args -- ^ Arguments of module application. 333 -> ScopeCopyInfo -- ^ Imported names and modules 334 -> TCM () 335applySection new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = rd } = do 336 rd <- closeConstructors rd 337 applySection' new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = rd } 338 where 339 -- If a datatype is being copied, all its constructors need to be copied, 340 -- and if a constructor is copied its datatype needs to be. 341 closeConstructors :: Ren QName -> TCM (Ren QName) 342 closeConstructors rd = do 343 ds <- nubOn id . catMaybes <$> traverse constructorData (Map.keys rd) 344 cs <- nubOn id . concat <$> traverse dataConstructors (Map.keys rd) 345 new <- Map.unionsWith (<>) <$> traverse rename (ds ++ cs) 346 reportSDoc "tc.mod.apply.complete" 30 $ 347 "also copying: " <+> pretty new 348 return $ Map.unionWith (<>) new rd 349 where 350 rename :: QName -> TCM (Ren QName) 351 rename x 352 | x `Map.member` rd = pure mempty 353 | otherwise = 354 Map.singleton x . pure . qnameFromList . singleton <$> freshName_ (prettyShow $ qnameName x) 355 356 constructorData :: QName -> TCM (Maybe QName) 357 constructorData x = do 358 (theDef <$> getConstInfo x) <&> \case 359 Constructor{ conData = d } -> Just d 360 _ -> Nothing 361 362 dataConstructors :: QName -> TCM [QName] 363 dataConstructors x = do 364 (theDef <$> getConstInfo x) <&> \case 365 Datatype{ dataCons = cs } -> cs 366 Record{ recConHead = h } -> [conName h] 367 _ -> [] 368 369applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM () 370applySection' new ptel old ts ScopeCopyInfo{ renNames = rd, renModules = rm } = do 371 do 372 noCopyList <- catMaybes <$> mapM getName' constrainedPrims 373 for_ (Map.keys rd) $ \ q -> 374 when (q `elem` noCopyList) $ typeError (TriedToCopyConstrainedPrim q) 375 376 reportSDoc "tc.mod.apply" 10 $ vcat 377 [ "applySection" 378 , "new =" <+> pretty new 379 , "ptel =" <+> pretty ptel 380 , "old =" <+> pretty old 381 , "ts =" <+> pretty ts 382 ] 383 _ <- Map.traverseWithKey (traverse . copyDef ts) rd 384 _ <- Map.traverseWithKey (traverse . copySec ts) rm 385 computePolarity (Map.elems rd >>= List1.toList) 386 where 387 -- Andreas, 2013-10-29 388 -- Here, if the name x is not imported, it persists as 389 -- old, possibly out-of-scope name. 390 -- This old name may used by the case split tactic, leading to 391 -- names that cannot be printed properly. 392 -- I guess it would make sense to mark non-imported names 393 -- as such (out-of-scope) and let splitting fail if it would 394 -- produce out-of-scope constructors. 395 -- 396 -- Taking 'List1.head' because 'Module.Data.cons' and 'Module.cons' are 397 -- equivalent valid names and either can be used. 398 copyName x = maybe x List1.head (Map.lookup x rd) 399 400 argsToUse x = do 401 let m = commonParentModule old x 402 reportSDoc "tc.mod.apply" 80 $ "Common prefix: " <+> pretty m 403 size <$> lookupSection m 404 405 copyDef :: Args -> QName -> QName -> TCM () 406 copyDef ts x y = do 407 def <- getConstInfo x 408 np <- argsToUse (qnameModule x) 409 -- Issue #3083: We need to use the hiding from the telescope of the 410 -- original module. This can be different than the hiding for the common 411 -- parent in the case of record modules. 412 hidings <- map getHiding . telToList <$> lookupSection (qnameModule x) 413 let ts' = zipWith setHiding hidings ts 414 commonTel <- lookupSection (commonParentModule old $ qnameModule x) 415 reportSDoc "tc.mod.apply" 80 $ vcat 416 [ "copyDef" <+> pretty x <+> "->" <+> pretty y 417 , "ts' = " <+> pretty ts' ] 418 copyDef' ts' np def 419 where 420 copyDef' ts np d = do 421 reportSDoc "tc.mod.apply" 60 $ "making new def for" <+> pretty y <+> "from" <+> pretty x <+> "with" <+> text (show np) <+> "args" <+> text (show $ defAbstract d) 422 reportSDoc "tc.mod.apply" 80 $ vcat 423 [ "args = " <+> text (show ts') 424 , "old type = " <+> pretty (defType d) ] 425 reportSDoc "tc.mod.apply" 80 $ 426 "new type = " <+> pretty t 427 addConstant y =<< nd y 428 makeProjection y 429 -- Issue1238: the copied def should be an 'instance' if the original 430 -- def is one. Skip constructors since the original constructor will 431 -- still work as an instance. 432 unless isCon $ whenJust inst $ \ c -> addNamedInstance y c 433 -- Set display form for the old name if it's not a constructor. 434{- BREAKS fail/Issue478 435 -- Andreas, 2012-10-20 and if we are not an anonymous module 436 -- unless (isAnonymousModuleName new || isCon || size ptel > 0) $ do 437-} 438 -- BREAKS fail/Issue1643a 439 -- -- Andreas, 2015-09-09 Issue 1643: 440 -- -- Do not add a display form for a bare module alias. 441 -- when (not isCon && size ptel == 0 && not (null ts)) $ do 442 when (size ptel == 0) $ do 443 addDisplayForms y 444 where 445 ts' = take np ts 446 t = defType d `piApply` ts' 447 pol = defPolarity d `apply` ts' 448 occ = defArgOccurrences d `apply` ts' 449 gen = defArgGeneralizable d `apply` ts' 450 inst = defInstance d 451 -- the name is set by the addConstant function 452 nd :: QName -> TCM Definition 453 nd y = for def $ \ df -> Defn 454 { defArgInfo = defArgInfo d 455 , defName = y 456 , defType = t 457 , defPolarity = pol 458 , defArgOccurrences = occ 459 , defArgGeneralizable = gen 460 , defGeneralizedParams = [] -- This is only needed for type checking data/record defs so no need to copy it. 461 , defDisplay = [] 462 , defMutual = -1 -- TODO: mutual block? 463 , defCompiledRep = noCompiledRep 464 , defInstance = inst 465 , defCopy = True 466 , defMatchable = Set.empty 467 , defNoCompilation = defNoCompilation d 468 , defInjective = False 469 , defCopatternLHS = isCopatternLHS [cl] 470 , defBlocked = defBlocked d 471 , theDef = df } 472 oldDef = theDef d 473 isCon = case oldDef of { Constructor{} -> True ; _ -> False } 474 mutual = case oldDef of { Function{funMutual = m} -> m ; _ -> Nothing } 475 extlam = case oldDef of { Function{funExtLam = e} -> e ; _ -> Nothing } 476 with = case oldDef of { Function{funWith = w} -> copyName <$> w ; _ -> Nothing } 477 -- Andreas, 2015-05-11, to fix issue 1413: 478 -- Even if we apply the record argument (must be @var 0@), we stay a projection. 479 -- This is because we may abstract the record argument later again. 480 -- See succeed/ProjectionNotNormalized.agda 481 isVar0 t = case unArg t of Var 0 [] -> True; _ -> False 482 proj = case oldDef of 483 Function{funProjection = Just p@Projection{projIndex = n}} 484 | size ts' < n || (size ts' == n && maybe True isVar0 (lastMaybe ts')) 485 -> Just $ p { projIndex = n - size ts' 486 , projLams = projLams p `apply` ts' 487 , projProper= copyName <$> projProper p 488 } 489 _ -> Nothing 490 def = 491 case oldDef of 492 Constructor{ conPars = np, conData = d } -> return $ 493 oldDef { conPars = np - size ts' 494 , conData = copyName d 495 } 496 Datatype{ dataPars = np, dataCons = cs } -> return $ 497 oldDef { dataPars = np - size ts' 498 , dataClause = Just cl 499 , dataCons = map copyName cs 500 } 501 Record{ recPars = np, recTel = tel } -> return $ 502 oldDef { recPars = np - size ts' 503 , recClause = Just cl 504 , recTel = apply tel ts' 505 } 506 GeneralizableVar -> return GeneralizableVar 507 _ -> do 508 (mst, _, cc) <- compileClauses Nothing [cl] -- Andreas, 2012-10-07 non need for record pattern translation 509 let newDef = 510 set funMacro (oldDef ^. funMacro) $ 511 set funStatic (oldDef ^. funStatic) $ 512 set funInline True $ 513 emptyFunction 514 { funClauses = [cl] 515 , funCompiled = Just cc 516 , funSplitTree = mst 517 , funMutual = mutual 518 , funProjection = proj 519 , funTerminates = Just True 520 , funExtLam = extlam 521 , funWith = with 522 } 523 reportSDoc "tc.mod.apply" 80 $ ("new def for" <+> pretty x) <?> pretty newDef 524 return newDef 525 526 cl = Clause { clauseLHSRange = getRange $ defClauses d 527 , clauseFullRange = getRange $ defClauses d 528 , clauseTel = EmptyTel 529 , namedClausePats = [] 530 , clauseBody = Just $ dropArgs pars $ case oldDef of 531 Function{funProjection = Just p} -> projDropParsApply p ProjSystem rel ts' 532 _ -> Def x $ map Apply ts' 533 , clauseType = Just $ defaultArg t 534 , clauseCatchall = False 535 , clauseExact = Just True 536 , clauseRecursive = Just False -- definitely not recursive 537 , clauseUnreachable = Just False -- definitely not unreachable 538 , clauseEllipsis = NoEllipsis 539 } 540 where 541 -- The number of remaining parameters. We need to drop the 542 -- lambdas corresponding to these from the clause body above. 543 pars = max 0 $ maybe 0 (pred . projIndex) proj 544 rel = getRelevance $ defArgInfo d 545 546 {- Example 547 548 module Top Θ where 549 module A Γ where 550 module M Φ where 551 module B Δ where 552 module N Ψ where 553 module O Ψ' where 554 open A public -- introduces only M --> A.M into the *scope* 555 module C Ξ = Top.B ts 556 557 new section C 558 tel = Ξ.(Θ.Δ)[ts] 559 560 calls 561 1. copySec ts Top.A.M C.M 562 2. copySec ts Top.B.N C.N 563 3. copySec ts Top.B.N.O C.N.O 564 with 565 old = Top.B 566 567 For 1. 568 Common prefix is: Top 569 totalArgs = |Θ| (section Top) 570 tel = Θ.Γ.Φ (section Top.A.M) 571 ts' = take totalArgs ts 572 Θ₂ = drop totalArgs Θ 573 new section C.M 574 tel = Θ₂.Γ.Φ[ts'] 575 -} 576 copySec :: Args -> ModuleName -> ModuleName -> TCM () 577 copySec ts x y = do 578 totalArgs <- argsToUse x 579 tel <- lookupSection x 580 let sectionTel = apply tel $ take totalArgs ts 581 reportSDoc "tc.mod.apply" 80 $ "Copying section" <+> pretty x <+> "to" <+> pretty y 582 reportSDoc "tc.mod.apply" 80 $ " ts = " <+> mconcat (List.intersperse "; " (map pretty ts)) 583 reportSDoc "tc.mod.apply" 80 $ " totalArgs = " <+> text (show totalArgs) 584 reportSDoc "tc.mod.apply" 80 $ " tel = " <+> text (unwords (map (fst . unDom) $ telToList tel)) -- only names 585 reportSDoc "tc.mod.apply" 80 $ " sectionTel = " <+> text (unwords (map (fst . unDom) $ telToList ptel)) -- only names 586 addContext sectionTel $ addSection y 587 588-- | Add a display form to a definition (could be in this or imported signature). 589addDisplayForm :: QName -> DisplayForm -> TCM () 590addDisplayForm x df = do 591 d <- makeOpen df 592 let add = updateDefinition x $ \ def -> def{ defDisplay = d : defDisplay def } 593 ifM (isLocal x) 594 {-then-} (modifySignature add) 595 {-else-} (stImportsDisplayForms `modifyTCLens` HMap.insertWith (++) x [d]) 596 whenM (hasLoopingDisplayForm x) $ 597 typeError . GenericDocError =<< do "Cannot add recursive display form for" <+> pretty x 598 599isLocal :: ReadTCState m => QName -> m Bool 600isLocal x = HMap.member x <$> useR (stSignature . sigDefinitions) 601 602getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm] 603getDisplayForms q = do 604 ds <- either (const []) defDisplay <$> getConstInfo' q 605 ds1 <- HMap.lookupDefault [] q <$> useR stImportsDisplayForms 606 ds2 <- HMap.lookupDefault [] q <$> useR stImportedDisplayForms 607 ifM (isLocal q) (return $ ds ++ ds1 ++ ds2) 608 (return $ ds1 ++ ds ++ ds2) 609 610-- | Find all names used (recursively) by display forms of a given name. 611chaseDisplayForms :: QName -> TCM (Set QName) 612chaseDisplayForms q = go Set.empty [q] 613 where 614 go :: Set QName -- Accumulator. 615 -> [QName] -- Work list. TODO: make work set to avoid duplicate chasing? 616 -> TCM (Set QName) 617 go used [] = pure used 618 go used (q : qs) = do 619 let rhs (Display _ _ e) = e -- Only look at names in the right-hand side (#1870) 620 let notYetUsed x = if x `Set.member` used then Set.empty else Set.singleton x 621 ds <- namesIn' notYetUsed . map (rhs . dget) 622 <$> (getDisplayForms q `catchError_` \ _ -> pure []) -- might be a pattern synonym 623 go (Set.union ds used) (Set.toList ds ++ qs) 624 625-- | Check if a display form is looping. 626hasLoopingDisplayForm :: QName -> TCM Bool 627hasLoopingDisplayForm q = Set.member q <$> chaseDisplayForms q 628 629canonicalName :: HasConstInfo m => QName -> m QName 630canonicalName x = do 631 def <- theDef <$> getConstInfo x 632 case def of 633 Constructor{conSrcCon = c} -> return $ conName c 634 Record{recClause = Just (Clause{ clauseBody = body })} -> can body 635 Datatype{dataClause = Just (Clause{ clauseBody = body })} -> can body 636 _ -> return x 637 where 638 can body = canonicalName $ extract $ fromMaybe __IMPOSSIBLE__ body 639 extract (Def x _) = x 640 extract _ = __IMPOSSIBLE__ 641 642sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName) 643sameDef d1 d2 = do 644 c1 <- canonicalName d1 645 c2 <- canonicalName d2 646 if (c1 == c2) then return $ Just c1 else return Nothing 647 648-- | Can be called on either a (co)datatype, a record type or a 649-- (co)constructor. 650whatInduction :: MonadTCM tcm => QName -> tcm Induction 651whatInduction c = liftTCM $ do 652 def <- theDef <$> getConstInfo c 653 mz <- getBuiltinName' builtinIZero 654 mo <- getBuiltinName' builtinIOne 655 case def of 656 Datatype{} -> return Inductive 657 Record{} | not (recRecursive def) -> return Inductive 658 Record{ recInduction = i } -> return $ fromMaybe Inductive i 659 Constructor{ conInd = i } -> return i 660 _ | Just c == mz || Just c == mo 661 -> return Inductive 662 _ -> __IMPOSSIBLE__ 663 664-- | Does the given constructor come from a single-constructor type? 665-- 666-- Precondition: The name has to refer to a constructor. 667singleConstructorType :: QName -> TCM Bool 668singleConstructorType q = do 669 d <- theDef <$> getConstInfo q 670 case d of 671 Record {} -> return True 672 Constructor { conData = d } -> do 673 di <- theDef <$> getConstInfo d 674 return $ case di of 675 Record {} -> True 676 Datatype { dataCons = cs } -> length cs == 1 677 _ -> __IMPOSSIBLE__ 678 _ -> __IMPOSSIBLE__ 679 680-- | Signature lookup errors. 681data SigError 682 = SigUnknown String -- ^ The name is not in the signature; default error message. 683 | SigAbstract -- ^ The name is not available, since it is abstract. 684 685-- | Standard eliminator for 'SigError'. 686sigError :: (String -> a) -> a -> SigError -> a 687sigError f a = \case 688 SigUnknown s -> f s 689 SigAbstract -> a 690 691class ( Functor m 692 , Applicative m 693 , Fail.MonadFail m 694 , HasOptions m 695 , MonadDebug m 696 , MonadTCEnv m 697 ) => HasConstInfo m where 698 -- | Lookup the definition of a name. The result is a closed thing, all free 699 -- variables have been abstracted over. 700 getConstInfo :: QName -> m Definition 701 getConstInfo q = getConstInfo' q >>= \case 702 Right d -> return d 703 Left (SigUnknown err) -> __IMPOSSIBLE_VERBOSE__ err 704 Left SigAbstract -> __IMPOSSIBLE_VERBOSE__ $ 705 "Abstract, thus, not in scope: " ++ prettyShow q 706 707 -- | Version that reports exceptions: 708 getConstInfo' :: QName -> m (Either SigError Definition) 709 -- getConstInfo' q = Right <$> getConstInfo q -- conflicts with default signature 710 711 -- | Lookup the rewrite rules with the given head symbol. 712 getRewriteRulesFor :: QName -> m RewriteRules 713 714 -- Lifting HasConstInfo through monad transformers: 715 716 default getConstInfo' 717 :: (HasConstInfo n, MonadTrans t, m ~ t n) 718 => QName -> m (Either SigError Definition) 719 getConstInfo' = lift . getConstInfo' 720 721 default getRewriteRulesFor 722 :: (HasConstInfo n, MonadTrans t, m ~ t n) 723 => QName -> m RewriteRules 724 getRewriteRulesFor = lift . getRewriteRulesFor 725 726{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-} 727 728defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules 729defaultGetRewriteRulesFor q = ifNotM (shouldReduceDef q) (return []) $ do 730 st <- getTCState 731 let sig = st^.stSignature 732 imp = st^.stImports 733 look s = HMap.lookup q $ s ^. sigRewriteRules 734 return $ mconcat $ catMaybes [look sig, look imp] 735 736-- | Get the original name of the projection 737-- (the current one could be from a module application). 738getOriginalProjection :: HasConstInfo m => QName -> m QName 739getOriginalProjection q = projOrig . fromMaybe __IMPOSSIBLE__ <$> isProjection q 740 741instance HasConstInfo (TCMT IO) where 742 getRewriteRulesFor = defaultGetRewriteRulesFor 743 getConstInfo' q = do 744 st <- getTC 745 env <- askTC 746 defaultGetConstInfo st env q 747 getConstInfo q = getConstInfo' q >>= \case 748 Right d -> return d 749 Left (SigUnknown err) -> fail err 750 Left SigAbstract -> notInScopeError $ qnameToConcrete q 751 752defaultGetConstInfo 753 :: (HasOptions m, MonadDebug m, MonadTCEnv m) 754 => TCState -> TCEnv -> QName -> m (Either SigError Definition) 755defaultGetConstInfo st env q = do 756 let defs = st^.(stSignature . sigDefinitions) 757 idefs = st^.(stImports . sigDefinitions) 758 case catMaybes [HMap.lookup q defs, HMap.lookup q idefs] of 759 [] -> return $ Left $ SigUnknown $ "Unbound name: " ++ prettyShow q ++ showQNameId q 760 [d] -> mkAbs env d 761 ds -> __IMPOSSIBLE_VERBOSE__ $ "Ambiguous name: " ++ prettyShow q 762 where 763 mkAbs env d 764 | treatAbstractly' q' env = 765 case makeAbstract d of 766 Just d -> return $ Right d 767 Nothing -> return $ Left SigAbstract 768 -- the above can happen since the scope checker is a bit sloppy with 'abstract' 769 | otherwise = return $ Right d 770 where 771 q' = case theDef d of 772 -- Hack to make abstract constructors work properly. The constructors 773 -- live in a module with the same name as the datatype, but for 'abstract' 774 -- purposes they're considered to be in the same module as the datatype. 775 Constructor{} -> dropLastModule q 776 _ -> q 777 778 dropLastModule q@QName{ qnameModule = m } = 779 q{ qnameModule = mnameFromList $ 780 initWithDefault __IMPOSSIBLE__ $ mnameToList m 781 } 782 783-- HasConstInfo lifts through monad transformers 784-- (see default signatures in HasConstInfo class). 785 786instance HasConstInfo m => HasConstInfo (ChangeT m) 787instance HasConstInfo m => HasConstInfo (ExceptT err m) 788instance HasConstInfo m => HasConstInfo (IdentityT m) 789instance HasConstInfo m => HasConstInfo (ListT m) 790instance HasConstInfo m => HasConstInfo (MaybeT m) 791instance HasConstInfo m => HasConstInfo (ReaderT r m) 792instance HasConstInfo m => HasConstInfo (StateT s m) 793instance (Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m) 794instance HasConstInfo m => HasConstInfo (BlockT m) 795 796{-# INLINE getConInfo #-} 797getConInfo :: HasConstInfo m => ConHead -> m Definition 798getConInfo = getConstInfo . conName 799 800-- | Look up the polarity of a definition. 801getPolarity :: HasConstInfo m => QName -> m [Polarity] 802getPolarity q = defPolarity <$> getConstInfo q 803 804-- | Look up polarity of a definition and compose with polarity 805-- represented by 'Comparison'. 806getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity] 807getPolarity' CmpEq q = map (composePol Invariant) <$> getPolarity q -- return [] 808getPolarity' CmpLeq q = getPolarity q -- composition with Covariant is identity 809 810-- | Set the polarity of a definition. 811setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m () 812setPolarity q pol = do 813 reportSDoc "tc.polarity.set" 20 $ 814 "Setting polarity of" <+> pretty q <+> "to" <+> pretty pol <> "." 815 modifySignature $ updateDefinition q $ updateDefPolarity $ const pol 816 817-- | Look up the forced arguments of a definition. 818getForcedArgs :: HasConstInfo m => QName -> m [IsForced] 819getForcedArgs q = defForced <$> getConstInfo q 820 821-- | Get argument occurrence info for argument @i@ of definition @d@ (never fails). 822getArgOccurrence :: QName -> Nat -> TCM Occurrence 823getArgOccurrence d i = do 824 def <- getConstInfo d 825 return $! case theDef def of 826 Constructor{} -> StrictPos 827 _ -> fromMaybe Mixed $ defArgOccurrences def !!! i 828 829-- | Sets the 'defArgOccurrences' for the given identifier (which 830-- should already exist in the signature). 831setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m () 832setArgOccurrences d os = modifyArgOccurrences d $ const os 833 834modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m () 835modifyArgOccurrences d f = 836 modifySignature $ updateDefinition d $ updateDefArgOccurrences f 837 838setTreeless :: QName -> TTerm -> TCM () 839setTreeless q t = 840 modifyGlobalDefinition q $ updateTheDef $ \case 841 fun@Function{} -> fun{ funTreeless = Just $ Compiled t Nothing } 842 _ -> __IMPOSSIBLE__ 843 844setCompiledArgUse :: QName -> [ArgUsage] -> TCM () 845setCompiledArgUse q use = 846 modifyGlobalDefinition q $ updateTheDef $ \case 847 fun@Function{} -> 848 fun{ funTreeless = funTreeless fun <&> \ c -> c { cArgUsage = Just use } } 849 _ -> __IMPOSSIBLE__ 850 851getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled) 852getCompiled q = do 853 (theDef <$> getConstInfo q) <&> \case 854 Function{ funTreeless = t } -> t 855 _ -> Nothing 856 857-- | Returns a list of length 'conArity'. 858-- If no erasure analysis has been performed yet, this will be a list of 'False's. 859getErasedConArgs :: HasConstInfo m => QName -> m [Bool] 860getErasedConArgs q = do 861 def <- getConstInfo q 862 case theDef def of 863 Constructor{ conArity, conErased } -> return $ 864 fromMaybe (replicate conArity False) conErased 865 _ -> __IMPOSSIBLE__ 866 867setErasedConArgs :: QName -> [Bool] -> TCM () 868setErasedConArgs q args = modifyGlobalDefinition q $ updateTheDef $ \case 869 def@Constructor{ conArity } 870 | length args == conArity -> def{ conErased = Just args } 871 | otherwise -> __IMPOSSIBLE__ 872 def -> def -- no-op for non-constructors 873 874getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm) 875getTreeless q = fmap cTreeless <$> getCompiled q 876 877getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage]) 878getCompiledArgUse q = (cArgUsage =<<) <$> getCompiled q 879 880-- | add data constructors to a datatype 881addDataCons :: QName -> [QName] -> TCM () 882addDataCons d cs = modifySignature $ updateDefinition d $ updateTheDef $ \ def -> 883 let !cs' = cs ++ dataCons def in 884 case def of 885 Datatype{} -> def {dataCons = cs' } 886 _ -> __IMPOSSIBLE__ 887 888-- | Get the mutually recursive identifiers of a symbol from the signature. 889getMutual :: QName -> TCM (Maybe [QName]) 890getMutual d = getMutual_ . theDef <$> getConstInfo d 891 892-- | Get the mutually recursive identifiers from a `Definition`. 893getMutual_ :: Defn -> Maybe [QName] 894getMutual_ = \case 895 Function { funMutual = m } -> m 896 Datatype { dataMutual = m } -> m 897 Record { recMutual = m } -> m 898 _ -> Nothing 899 900-- | Set the mutually recursive identifiers. 901setMutual :: QName -> [QName] -> TCM () 902setMutual d m = modifySignature $ updateDefinition d $ updateTheDef $ \ def -> 903 case def of 904 Function{} -> def { funMutual = Just m } 905 Datatype{} -> def {dataMutual = Just m } 906 Record{} -> def { recMutual = Just m } 907 _ -> if null m then def else __IMPOSSIBLE__ -- nothing to do 908 909-- | Check whether two definitions are mutually recursive. 910mutuallyRecursive :: QName -> QName -> TCM Bool 911mutuallyRecursive d d1 = (d `elem`) . fromMaybe __IMPOSSIBLE__ <$> getMutual d1 912 913-- | A function/data/record definition is nonRecursive if it is not even mutually 914-- recursive with itself. 915definitelyNonRecursive_ :: Defn -> Bool 916definitelyNonRecursive_ = maybe False null . getMutual_ 917 918-- | Get the number of parameters to the current module. 919getCurrentModuleFreeVars :: TCM Nat 920getCurrentModuleFreeVars = size <$> (lookupSection =<< currentModule) 921 922-- For annoying reasons the qnameModule of a pattern lambda is not correct 923-- (#2883), so make sure to grab the right module for those. 924getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName) 925getDefModule f = mapRight modName <$> getConstInfo' f 926 where 927 modName def = case theDef def of 928 Function{ funExtLam = Just (ExtLamInfo m _ _) } -> m 929 _ -> qnameModule f 930 931-- | Compute the number of free variables of a defined name. This is the sum of 932-- number of parameters shared with the current module and the number of 933-- anonymous variables (if the name comes from a let-bound module). 934getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat 935getDefFreeVars = getModuleFreeVars . qnameModule 936 937freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, 938 ReadTCState m, MonadTCEnv m, MonadDebug m) 939 => QName -> m Args 940freeVarsToApply q = do 941 vs <- moduleParamsToApply $ qnameModule q 942 t <- defType <$> getConstInfo q 943 let TelV tel _ = telView'UpTo (size vs) t 944 unless (size tel == size vs) __IMPOSSIBLE__ 945 return $ zipWith (\ arg dom -> unArg arg <$ argFromDom dom) vs $ telToList tel 946 947{-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-} 948{-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-} 949getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) 950 => ModuleName -> m Nat 951getModuleFreeVars m = do 952 m0 <- commonParentModule m <$> currentModule 953 (+) <$> getAnonymousVariables m <*> (size <$> lookupSection m0) 954 955-- | Compute the context variables to apply a definition to. 956-- 957-- We have to insert the module telescope of the common prefix 958-- of the current module and the module where the definition comes from. 959-- (Properly raised to the current context.) 960-- 961-- Example: 962-- @ 963-- module M₁ Γ where 964-- module M₁ Δ where 965-- f = ... 966-- module M₃ Θ where 967-- ... M₁.M₂.f [insert Γ raised by Θ] 968-- @ 969moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, 970 MonadTCEnv m, ReadTCState m, MonadDebug m) 971 => ModuleName -> m Args 972moduleParamsToApply m = do 973 974 traceSDoc "tc.sig.param" 90 ("computing module parameters of " <+> pretty m) $ do 975 976 -- Jesper, 2020-01-22: If the module parameter substitution for the 977 -- module cannot be found, that likely means we are within a call to 978 -- @inTopContext@. In that case we should provide no arguments for 979 -- the module parameters (see #4383). 980 caseMaybeM (getModuleParameterSub m) (return []) $ \sub -> do 981 982 traceSDoc "tc.sig.param" 60 (do 983 cxt <- getContext 984 nest 2 $ vcat 985 [ "cxt = " <+> prettyTCM (PrettyContext cxt) 986 , "sub = " <+> pretty sub 987 ]) $ do 988 989 -- Get the correct number of free variables (correctly raised) of @m@. 990 n <- getModuleFreeVars m 991 traceSDoc "tc.sig.param" 60 (nest 2 $ "n = " <+> text (show n)) $ do 992 tel <- take n . telToList <$> lookupSection m 993 traceSDoc "tc.sig.param" 60 (nest 2 $ "tel = " <+> pretty tel) $ do 994 unless (size tel == n) __IMPOSSIBLE__ 995 let args = applySubst sub $ zipWith (\ i a -> var i <$ argFromDom a) (downFrom n) tel 996 traceSDoc "tc.sig.param" 60 (nest 2 $ "args = " <+> prettyList_ (map pretty args)) $ do 997 998 -- Apply the original ArgInfo, as the hiding information in the current 999 -- context might be different from the hiding information expected by @m@. 1000 1001 getSection m >>= \case 1002 Nothing -> do 1003 -- We have no section for @m@. 1004 -- This should only happen for toplevel definitions, and then there 1005 -- are no free vars to apply, or? 1006 -- unless (null args) __IMPOSSIBLE__ 1007 -- No, this invariant is violated by private modules, see Issue1701a. 1008 return args 1009 Just (Section stel) -> do 1010 -- The section telescope of @m@ should be as least 1011 -- as long as the number of free vars @m@ is applied to. 1012 -- We still check here as in no case, we want @zipWith@ to silently 1013 -- drop some @args@. 1014 -- And there are also anonymous modules, thus, the invariant is not trivial. 1015 when (size stel < size args) __IMPOSSIBLE__ 1016 return $ zipWith (\ !dom (Arg _ v) -> v <$ argFromDom dom) (telToList stel) args 1017 1018-- | Unless all variables in the context are module parameters, create a fresh 1019-- module to capture the non-module parameters. Used when unquoting to make 1020-- sure generated definitions work properly. 1021inFreshModuleIfFreeParams :: TCM a -> TCM a 1022inFreshModuleIfFreeParams k = do 1023 msub <- getModuleParameterSub =<< currentModule 1024 if isNothing msub || msub == Just IdS then k else do 1025 m <- currentModule 1026 m' <- qualifyM m . mnameFromList1 . singleton <$> 1027 freshName_ ("_" :: String) 1028 addSection m' 1029 withCurrentModule m' k 1030 1031-- | Instantiate a closed definition with the correct part of the current 1032-- context. 1033{-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-} 1034instantiateDef 1035 :: ( Functor m, HasConstInfo m, HasOptions m 1036 , ReadTCState m, MonadTCEnv m, MonadDebug m ) 1037 => Definition -> m Definition 1038instantiateDef d = do 1039 vs <- freeVarsToApply $ defName d 1040 verboseS "tc.sig.inst" 30 $ do 1041 ctx <- getContext 1042 m <- currentModule 1043 reportSDoc "tc.sig.inst" 30 $ 1044 "instDef in" <+> pretty m <> ":" <+> pretty (defName d) <+> 1045 fsep (map pretty $ zipWith (<$) (reverse $ map (fst . unDom) ctx) vs) 1046 return $ d `apply` vs 1047 1048instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, 1049 ReadTCState m, MonadTCEnv m, MonadDebug m) 1050 => RewriteRule -> m RewriteRule 1051instantiateRewriteRule rew = do 1052 traceSDoc "rewriting" 95 ("instantiating rewrite rule" <+> pretty (rewName rew) <+> "to the local context.") $ do 1053 vs <- freeVarsToApply $ rewName rew 1054 let rew' = rew `apply` vs 1055 traceSLn "rewriting" 95 ("instantiated rewrite rule: ") $ do 1056 traceSLn "rewriting" 95 (show rew') $ do 1057 return rew' 1058 1059instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, 1060 ReadTCState m, MonadTCEnv m, MonadDebug m) 1061 => RewriteRules -> m RewriteRules 1062instantiateRewriteRules = mapM instantiateRewriteRule 1063 1064-- | Give the abstract view of a definition. 1065makeAbstract :: Definition -> Maybe Definition 1066makeAbstract d = 1067 case defAbstract d of 1068 ConcreteDef -> return d 1069 AbstractDef -> do 1070 def <- makeAbs $ theDef d 1071 return d { defArgOccurrences = [] -- no positivity info for abstract things! 1072 , defPolarity = [] -- no polarity info for abstract things! 1073 , theDef = def 1074 } 1075 where 1076 makeAbs d@Axiom{} = Just d 1077 makeAbs d@DataOrRecSig{} = Just d 1078 makeAbs d@GeneralizableVar{} = Just d 1079 makeAbs d@Datatype {} = Just $ AbstractDefn d 1080 makeAbs d@Function {} = Just $ AbstractDefn d 1081 makeAbs Constructor{} = Nothing 1082 -- Andreas, 2012-11-18: Make record constructor and projections abstract. 1083 -- Andreas, 2017-08-14: Projections are actually not abstract (issue #2682). 1084 -- Return the Defn under a wrapper to allow e.g. eligibleForProjectionLike 1085 -- to see whether the abstract thing is a record type or not. 1086 makeAbs d@Record{} = Just $ AbstractDefn d 1087 makeAbs Primitive{} = __IMPOSSIBLE__ 1088 makeAbs PrimitiveSort{} = __IMPOSSIBLE__ 1089 makeAbs AbstractDefn{}= __IMPOSSIBLE__ 1090 1091-- | Enter abstract mode. Abstract definition in the current module are transparent. 1092{-# SPECIALIZE inAbstractMode :: TCM a -> TCM a #-} 1093inAbstractMode :: MonadTCEnv m => m a -> m a 1094inAbstractMode = localTC $ \e -> e { envAbstractMode = AbstractMode } 1095 1096-- | Not in abstract mode. All abstract definitions are opaque. 1097{-# SPECIALIZE inConcreteMode :: TCM a -> TCM a #-} 1098inConcreteMode :: MonadTCEnv m => m a -> m a 1099inConcreteMode = localTC $ \e -> e { envAbstractMode = ConcreteMode } 1100 1101-- | Ignore abstract mode. All abstract definitions are transparent. 1102ignoreAbstractMode :: MonadTCEnv m => m a -> m a 1103ignoreAbstractMode = localTC $ \e -> e { envAbstractMode = IgnoreAbstractMode } 1104 1105-- | Enter concrete or abstract mode depending on whether the given identifier 1106-- is concrete or abstract. 1107{-# SPECIALIZE inConcreteOrAbstractMode :: QName -> (Definition -> TCM a) -> TCM a #-} 1108inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a 1109inConcreteOrAbstractMode q cont = do 1110 -- Andreas, 2015-07-01: If we do not ignoreAbstractMode here, 1111 -- we will get ConcreteDef for abstract things, as they are turned into axioms. 1112 def <- ignoreAbstractMode $ getConstInfo q 1113 case defAbstract def of 1114 AbstractDef -> inAbstractMode $ cont def 1115 ConcreteDef -> inConcreteMode $ cont def 1116 1117-- | Check whether a name might have to be treated abstractly (either if we're 1118-- 'inAbstractMode' or it's not a local name). Returns true for things not 1119-- declared abstract as well, but for those 'makeAbstract' will have no effect. 1120treatAbstractly :: MonadTCEnv m => QName -> m Bool 1121treatAbstractly q = asksTC $ treatAbstractly' q 1122 1123-- | Andreas, 2015-07-01: 1124-- If the @current@ module is a weak suffix of the identifier module, 1125-- we can see through its abstract definition if we are abstract. 1126-- (Then @treatAbstractly'@ returns @False@). 1127-- 1128-- If I am not mistaken, then we cannot see definitions in the @where@ 1129-- block of an abstract function from the perspective of the function, 1130-- because then the current module is a strict prefix of the module 1131-- of the local identifier. 1132-- This problem is fixed by removing trailing anonymous module name parts 1133-- (underscores) from both names. 1134treatAbstractly' :: QName -> TCEnv -> Bool 1135treatAbstractly' q env = case envAbstractMode env of 1136 ConcreteMode -> True 1137 IgnoreAbstractMode -> False 1138 AbstractMode -> not $ current `isLeChildModuleOf` m 1139 where 1140 current = dropAnon $ envCurrentModule env 1141 m = dropAnon $ qnameModule q 1142 dropAnon (MName ms) = MName $ List.dropWhileEnd isNoName ms 1143 1144-- | Get type of a constant, instantiated to the current context. 1145{-# SPECIALIZE typeOfConst :: QName -> TCM Type #-} 1146typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type 1147typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q) 1148 1149-- | Get relevance of a constant. 1150{-# SPECIALIZE relOfConst :: QName -> TCM Relevance #-} 1151relOfConst :: HasConstInfo m => QName -> m Relevance 1152relOfConst q = getRelevance <$> getConstInfo q 1153 1154-- | Get modality of a constant. 1155{-# SPECIALIZE modalityOfConst :: QName -> TCM Modality #-} 1156modalityOfConst :: HasConstInfo m => QName -> m Modality 1157modalityOfConst q = getModality <$> getConstInfo q 1158 1159-- | The number of dropped parameters for a definition. 1160-- 0 except for projection(-like) functions and constructors. 1161droppedPars :: Definition -> Int 1162droppedPars d = case theDef d of 1163 Axiom{} -> 0 1164 DataOrRecSig{} -> 0 1165 GeneralizableVar{} -> 0 1166 def@Function{} -> projectionArgs def 1167 Datatype {dataPars = _} -> 0 -- not dropped 1168 Record {recPars = _} -> 0 -- not dropped 1169 Constructor{conPars = n} -> n 1170 Primitive{} -> 0 1171 PrimitiveSort{} -> 0 1172 AbstractDefn{} -> __IMPOSSIBLE__ 1173 1174-- | Is it the name of a record projection? 1175{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-} 1176isProjection :: HasConstInfo m => QName -> m (Maybe Projection) 1177isProjection qn = isProjection_ . theDef <$> getConstInfo qn 1178 1179isProjection_ :: Defn -> Maybe Projection 1180isProjection_ def = 1181 case def of 1182 Function { funProjection = result } -> result 1183 _ -> Nothing 1184 1185-- | Is it a function marked STATIC? 1186isStaticFun :: Defn -> Bool 1187isStaticFun = (^. funStatic) 1188 1189-- | Is it a function marked INLINE? 1190isInlineFun :: Defn -> Bool 1191isInlineFun = (^. funInline) 1192 1193-- | Returns @True@ if we are dealing with a proper projection, 1194-- i.e., not a projection-like function nor a record field value 1195-- (projection applied to argument). 1196isProperProjection :: Defn -> Bool 1197isProperProjection d = caseMaybe (isProjection_ d) False $ \ isP -> 1198 (projIndex isP > 0) && isJust (projProper isP) 1199 1200-- | Number of dropped initial arguments of a projection(-like) function. 1201projectionArgs :: Defn -> Int 1202projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_ 1203 1204-- | Check whether a definition uses copatterns. 1205usesCopatterns :: (HasConstInfo m) => QName -> m Bool 1206usesCopatterns q = defCopatternLHS <$> getConstInfo q 1207 1208-- | Apply a function @f@ to its first argument, producing the proper 1209-- postfix projection if @f@ is a projection. 1210applyDef :: (HasConstInfo m) 1211 => ProjOrigin -> QName -> Arg Term -> m Term 1212applyDef o f a = do 1213 let fallback = return $ Def f [Apply a] 1214 caseMaybeM (isProjection f) fallback $ \ isP -> do 1215 if projIndex isP <= 0 then fallback else do 1216 -- Get the original projection, if existing. 1217 if isNothing (projProper isP) then fallback else do 1218 return $ unArg a `applyE` [Proj o $ projOrig isP] 1219