1 2-- | Computing the free variables of a term lazily. 3-- 4-- We implement a reduce (traversal into monoid) over internal syntax 5-- for a generic collection (monoid with singletons). This should allow 6-- a more efficient test for the presence of a particular variable. 7-- 8-- Worst-case complexity does not change (i.e. the case when a variable 9-- does not occur), but best case-complexity does matter. For instance, 10-- see 'Agda.TypeChecking.Substitute.mkAbs': each time we construct 11-- a dependent function type, we check whether it is actually dependent. 12-- 13-- The distinction between rigid and strongly rigid occurrences comes from: 14-- Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper) 15-- 16-- The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly 17-- in t. It might have a solution if the occurrence is not strongly rigid, e.g. 18-- 19-- x = \f -> suc (f (x (\ y -> k))) has x = \f -> suc (f (suc k)) 20-- 21-- [Jason C. Reed, PhD thesis, page 106] 22-- 23-- Under coinductive constructors, occurrences are never strongly rigid. 24-- Also, function types and lambdas do not establish strong rigidity. 25-- Only inductive constructors do so. 26-- (See issue 1271). 27-- 28-- For further reading on semirings and semimodules for variable occurrence, 29-- see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016). 30-- There, he treats the "quantity" dimension of variable occurrences. 31-- 32-- The semiring has an additive operation for combining occurrences of subterms, 33-- and a multiplicative operation of representing function composition. E.g. 34-- if variable @x@ appears @o@ in term @u@, but @u@ appears in context @q@ in 35-- term @t@ then occurrence of variable @x@ coming from @u@ is accounted for 36-- as @q o@ in @t@. 37-- 38-- Consider example @(λ{ x → (x,x)}) y@: 39-- 40-- * Variable @x@ occurs once unguarded in @x@. 41-- 42-- * It occurs twice unguarded in the aggregation @x@ @x@ 43-- 44-- * Inductive constructor @,@ turns this into two strictly rigid occurrences. 45-- 46-- If @,@ is a record constructor, then we stay unguarded. 47-- 48-- * The function @({λ x → (x,x)})@ provides a context for variable @y@. 49-- This context can be described as weakly rigid with quantity two. 50-- 51-- * The final occurrence of @y@ is obtained as composing the context with 52-- the occurrence of @y@ in itself (which is the unit for composition). 53-- Thus, @y@ occurs weakly rigid with quantity two. 54-- 55-- It is not a given that the context can be described in the same way 56-- as the variable occurrence. However, for quantity it is the case 57-- and we obtain a semiring of occurrences with 0, 1, and even ω, which 58-- is an absorptive element for addition. 59 60module Agda.TypeChecking.Free.Lazy where 61 62import Control.Applicative hiding (empty) 63import Control.Monad.Reader 64 65 66import Data.IntMap (IntMap) 67import qualified Data.IntMap as IntMap 68import Data.IntSet (IntSet) 69import qualified Data.IntSet as IntSet 70import Data.Semigroup ( Semigroup, (<>) ) 71 72 73 74import Agda.Syntax.Common 75import Agda.Syntax.Internal 76 77import Agda.Utils.Functor 78import Agda.Utils.Lens 79import Agda.Utils.Monad 80import Agda.Utils.Null 81import Agda.Utils.Semigroup 82import Agda.Utils.Singleton 83import Agda.Utils.Size 84 85--------------------------------------------------------------------------- 86-- * Set of meta variables. 87 88-- | A set of meta variables. Forms a monoid under union. 89 90newtype MetaSet = MetaSet { theMetaSet :: IntSet } 91 deriving (Eq, Show, Null, Semigroup, Monoid) 92 93instance Singleton MetaId MetaSet where 94 singleton = MetaSet . singleton . metaId 95 96insertMetaSet :: MetaId -> MetaSet -> MetaSet 97insertMetaSet (MetaId m) (MetaSet ms) = MetaSet $ IntSet.insert m ms 98 99foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a 100foldrMetaSet f e ms = IntSet.foldr (f . MetaId) e $ theMetaSet ms 101 102--------------------------------------------------------------------------- 103-- * Flexible and rigid occurrences (semigroup) 104 105-- | Depending on the surrounding context of a variable, 106-- it's occurrence can be classified as flexible or rigid, 107-- with finer distinctions. 108-- 109-- The constructors are listed in increasing order (wrt. information content). 110data FlexRig' a 111 = Flexible a -- ^ In arguments of metas. 112 -- The set of metas is used by ''Agda.TypeChecking.Rewriting.NonLinMatch'' 113 -- to generate the right blocking information. 114 -- The semantics is that the status of a variable occurrence may change 115 -- if one of the metas in the set gets solved. We may say the occurrence 116 -- is tainted by the meta variables in the set. 117 | WeaklyRigid -- ^ In arguments to variables and definitions. 118 | Unguarded -- ^ In top position, or only under inductive record constructors (unit). 119 | StronglyRigid -- ^ Under at least one and only inductive constructors. 120 deriving (Eq, Show, Functor, Foldable) 121 122type FlexRig = FlexRig' MetaSet 123 124class LensFlexRig a o | o -> a where 125 lensFlexRig :: Lens' (FlexRig' a) o 126 127instance LensFlexRig a (FlexRig' a) where 128 lensFlexRig f x = f x 129 130isFlexible :: LensFlexRig a o => o -> Bool 131isFlexible o = case o ^. lensFlexRig of 132 Flexible {} -> True 133 _ -> False 134 135isUnguarded :: LensFlexRig a o => o -> Bool 136isUnguarded o = case o ^. lensFlexRig of 137 Unguarded -> True 138 _ -> False 139 140isWeaklyRigid :: LensFlexRig a o => o -> Bool 141isWeaklyRigid o = case o ^. lensFlexRig of 142 WeaklyRigid -> True 143 _ -> False 144 145isStronglyRigid :: LensFlexRig a o => o -> Bool 146isStronglyRigid o = case o ^. lensFlexRig of 147 StronglyRigid -> True 148 _ -> False 149 150-- | 'FlexRig' aggregation (additive operation of the semiring). 151-- For combining occurrences of the same variable in subterms. 152-- This is a refinement of the 'max' operation for 'FlexRig' 153-- which would work if 'Flexible' did not have the 'MetaSet' as an argument. 154-- Now, to aggregate two 'Flexible' occurrences, we union the involved 'MetaSet's. 155 156addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a 157addFlexRig = curry $ \case 158 -- StronglyRigid is dominant 159 (StronglyRigid, _) -> StronglyRigid 160 (_, StronglyRigid) -> StronglyRigid 161 -- Next is Unguarded 162 (Unguarded, _) -> Unguarded 163 (_, Unguarded) -> Unguarded 164 -- Then WeaklyRigid 165 (WeaklyRigid, _) -> WeaklyRigid 166 (_, WeaklyRigid) -> WeaklyRigid 167 -- Least is Flexible. We union the meta sets, as the variable 168 -- is tainted by all of the involved meta variable. 169 (Flexible ms1, Flexible ms2) -> Flexible $ ms1 <> ms2 170 171-- | Unit for 'addFlexRig'. 172zeroFlexRig :: Monoid a => FlexRig' a 173zeroFlexRig = Flexible mempty 174 175-- | Absorptive for 'addFlexRig'. 176omegaFlexRig :: FlexRig' a 177omegaFlexRig = StronglyRigid 178 179-- | 'FlexRig' composition (multiplicative operation of the semiring). 180-- For accumulating the context of a variable. 181-- 182-- 'Flexible' is dominant. Once we are under a meta, we are flexible 183-- regardless what else comes. We taint all variable occurrences 184-- under a meta by this meta. 185-- 186-- 'WeaklyRigid' is next in strength. Destroys strong rigidity. 187-- 188-- 'StronglyRigid' is still dominant over 'Unguarded'. 189-- 190-- 'Unguarded' is the unit. It is the top (identity) context. 191-- 192composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a 193composeFlexRig = curry $ \case 194 (Flexible ms1, Flexible ms2) -> Flexible $ ms1 <> ms2 195 (Flexible ms1, _) -> Flexible ms1 196 (_, Flexible ms2) -> Flexible ms2 197 (WeaklyRigid, _) -> WeaklyRigid 198 (_, WeaklyRigid) -> WeaklyRigid 199 (StronglyRigid, _) -> StronglyRigid 200 (_, StronglyRigid) -> StronglyRigid 201 (Unguarded, Unguarded) -> Unguarded 202 203-- | Unit for 'composeFlexRig'. 204oneFlexRig :: FlexRig' a 205oneFlexRig = Unguarded 206 207--------------------------------------------------------------------------- 208-- * Multi-dimensional feature vector for variable occurrence (semigroup) 209 210-- | Occurrence of free variables is classified by several dimensions. 211-- Currently, we have 'FlexRig' and 'Modality'. 212data VarOcc' a = VarOcc 213 { varFlexRig :: FlexRig' a 214 , varModality :: Modality 215 } 216 deriving (Show) 217type VarOcc = VarOcc' MetaSet 218 219-- | Equality up to origin. 220instance Eq a => Eq (VarOcc' a) where 221 VarOcc fr m == VarOcc fr' m' = fr == fr' && sameModality m m' 222 223instance LensModality (VarOcc' a) where 224 getModality = varModality 225 mapModality f (VarOcc x r) = VarOcc x $ f r 226 227instance LensRelevance (VarOcc' a) where 228instance LensQuantity (VarOcc' a) where 229 230-- | Access to 'varFlexRig' in 'VarOcc'. 231instance LensFlexRig a (VarOcc' a) where 232 lensFlexRig f (VarOcc fr m) = f fr <&> \ fr' -> VarOcc fr' m 233-- lensFlexRig :: Lens' (FlexRig' a) (VarOcc' a) 234-- lensFlexRig f (VarOcc fr m) = f fr <&> \ fr' -> VarOcc fr' m 235 236 237-- | The default way of aggregating free variable info from subterms is by adding 238-- the variable occurrences. For instance, if we have a pair @(t₁,t₂)@ then 239-- and @t₁@ has @o₁@ the occurrences of a variable @x@ 240-- and @t₂@ has @o₂@ the occurrences of the same variable, then 241-- @(t₁,t₂)@ has @mappend o₁ o₂@ occurrences of that variable. 242-- 243-- From counting 'Quantity', we extrapolate this to 'FlexRig' and 'Relevance': 244-- we care most about about 'StronglyRigid' 'Relevant' occurrences. 245-- E.g., if @t₁@ has a 'StronglyRigid' occurrence and @t₂@ a 'Flexible' occurrence, 246-- then @(t₁,t₂)@ still has a 'StronglyRigid' occurrence. 247-- Analogously, @Relevant@ occurrences count most, as we wish e.g. to forbid 248-- relevant occurrences of variables that are declared to be irrelevant. 249-- 250-- 'VarOcc' forms a semiring, and this monoid is the addition of the semiring. 251 252instance Semigroup a => Semigroup (VarOcc' a) where 253 VarOcc o m <> VarOcc o' m' = VarOcc (addFlexRig o o') (addModality m m') 254 255-- | The neutral element for variable occurrence aggregation is least serious 256-- occurrence: flexible, irrelevant. 257-- This is also the absorptive element for 'composeVarOcc', if we ignore 258-- the 'MetaSet' in 'Flexible'. 259instance (Semigroup a, Monoid a) => Monoid (VarOcc' a) where 260 mempty = VarOcc (Flexible mempty) zeroModality 261 mappend = (<>) 262 263-- | The absorptive element of variable occurrence under aggregation: 264-- strongly rigid, relevant. 265topVarOcc :: VarOcc' a 266topVarOcc = VarOcc StronglyRigid topModality 267 268-- | First argument is the outer occurrence (context) and second is the inner. 269-- This multiplicative operation is to modify an occurrence under a context. 270composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a 271composeVarOcc (VarOcc o m) (VarOcc o' m') = VarOcc (composeFlexRig o o') (composeModality m m') 272 -- We use the multipicative modality monoid (composition). 273 274oneVarOcc :: VarOcc' a 275oneVarOcc = VarOcc Unguarded unitModality 276 277--------------------------------------------------------------------------- 278-- * Storing variable occurrences (semimodule). 279 280-- | Any representation @c@ of a set of variables need to be able to be modified by 281-- a variable occurrence. This is to ensure that free variable analysis is 282-- compositional. For instance, it should be possible to compute `fv (v [u/x])` 283-- from `fv v` and `fv u`. 284-- 285-- In algebraic terminology, a variable set @a@ needs to be (almost) a left semimodule 286-- to the semiring 'VarOcc'. 287class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where 288 -- | Laws 289 -- * Respects monoid operations: 290 -- ``` 291 -- withVarOcc o mempty == mempty 292 -- withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y 293 -- ``` 294 -- * Respects VarOcc composition: 295 -- ``` 296 -- withVarOcc oneVarOcc = id 297 -- withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 298 -- ``` 299 -- * Respects VarOcc aggregation: 300 -- ``` 301 -- withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x 302 -- ``` 303 -- Since the corresponding unit law may fail, 304 -- ``` 305 -- withVarOcc mempty x = mempty 306 -- ``` 307 -- it is not quite a semimodule. 308 withVarOcc :: VarOcc' a -> c -> c 309 310-- | Representation of a variable set as map from de Bruijn indices 311-- to 'VarOcc'. 312type TheVarMap' a = IntMap (VarOcc' a) 313newtype VarMap' a = VarMap { theVarMap :: TheVarMap' a } 314 deriving (Eq, Show) 315 316type TheVarMap = TheVarMap' MetaSet 317type VarMap = VarMap' MetaSet 318 319-- | A "set"-style 'Singleton' instance with default/initial variable occurrence. 320instance Singleton Variable (VarMap' a) where 321 singleton i = VarMap $ IntMap.singleton i oneVarOcc 322 323mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b 324mapVarMap f = VarMap . f . theVarMap 325 326lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a) 327lookupVarMap i = IntMap.lookup i . theVarMap 328 329-- Andreas & Jesper, 2018-05-11, issue #3052: 330 331-- | Proper monoid instance for @VarMap@ rather than inheriting the broken one from IntMap. 332-- We combine two occurrences of a variable using 'mappend'. 333instance Semigroup a => Semigroup (VarMap' a) where 334 VarMap m <> VarMap m' = VarMap $ IntMap.unionWith (<>) m m' 335 336instance Semigroup a => Monoid (VarMap' a) where 337 mempty = VarMap IntMap.empty 338 mappend = (<>) 339 mconcat = VarMap . IntMap.unionsWith (<>) . map theVarMap 340 -- mconcat = VarMap . IntMap.unionsWith mappend . coerce -- ghc 8.6.5 does not seem to like this coerce 341 342instance (Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) where 343 withVarOcc o = mapVarMap $ fmap $ composeVarOcc o 344 345 346--------------------------------------------------------------------------- 347-- * Simple flexible/rigid variable collection. 348 349-- | Keep track of 'FlexRig' for every variable, but forget the involved meta vars. 350type TheFlexRigMap = IntMap (FlexRig' ()) 351newtype FlexRigMap = FlexRigMap { theFlexRigMap :: TheFlexRigMap } 352 deriving (Show, Singleton (Variable, FlexRig' ())) 353 354mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap 355mapFlexRigMap f = FlexRigMap . f . theFlexRigMap 356 357instance Semigroup FlexRigMap where 358 FlexRigMap m <> FlexRigMap m' = FlexRigMap $ IntMap.unionWith addFlexRig m m' 359 360instance Monoid FlexRigMap where 361 mempty = FlexRigMap IntMap.empty 362 mappend = (<>) 363 mconcat = FlexRigMap . IntMap.unionsWith addFlexRig . map theFlexRigMap 364 365-- | Compose everything with the 'varFlexRig' part of the 'VarOcc'. 366instance IsVarSet () FlexRigMap where 367 withVarOcc o = mapFlexRigMap $ fmap $ composeFlexRig $ () <$ varFlexRig o 368 369instance Singleton MetaId () where 370 singleton _ = () 371 372--------------------------------------------------------------------------- 373-- * Environment for collecting free variables. 374 375-- | Where should we skip sorts in free variable analysis? 376 377data IgnoreSorts 378 = IgnoreNot -- ^ Do not skip. 379 | IgnoreInAnnotations -- ^ Skip when annotation to a type. 380 | IgnoreAll -- ^ Skip unconditionally. 381 deriving (Eq, Show) 382 383-- | The current context. 384 385data FreeEnv' a b c = FreeEnv 386 { feExtra :: !b 387 -- ^ Additional context, e.g., whether to ignore free variables in sorts. 388 , feFlexRig :: !(FlexRig' a) 389 -- ^ Are we flexible or rigid? 390 , feModality :: !Modality 391 -- ^ What is the current relevance and quantity? 392 , feSingleton :: Maybe Variable -> c 393 -- ^ Method to return a single variable. 394 } 395 396type Variable = Int 397type SingleVar c = Variable -> c 398 399type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c 400 401-- | Ignore free variables in sorts. 402feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts 403feIgnoreSorts = feExtra 404 405instance LensFlexRig a (FreeEnv' a b c) where 406 lensFlexRig f e = f (feFlexRig e) <&> \ fr -> e { feFlexRig = fr } 407 408instance LensModality (FreeEnv' a b c) where 409 getModality = feModality 410 mapModality f e = e { feModality = f (feModality e) } 411 412instance LensRelevance (FreeEnv' a b c) where 413instance LensQuantity (FreeEnv' a b c) where 414 415-- | The initial context. 416 417initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c 418initFreeEnv e sing = FreeEnv 419 { feExtra = e 420 , feFlexRig = Unguarded 421 , feModality = unitModality -- multiplicative monoid 422 , feSingleton = maybe mempty sing 423 } 424 425type FreeT a b m c = ReaderT (FreeEnv' a b c) m c 426type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c 427 428-- | Run function for FreeM. 429runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c 430runFreeM single i m = runReader m $ initFreeEnv i single 431 432instance (Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) where 433 mempty = pure mempty 434 mappend = (<>) 435 mconcat = mconcat <.> sequence 436 437-- | Base case: a variable. 438variable :: (Monad m, IsVarSet a c) => Int -> FreeT a b m c 439variable n = do 440 o <- asks feFlexRig 441 r <- asks feModality 442 s <- asks feSingleton 443 return $ withVarOcc (VarOcc o r) (s $ Just n) 444 445-- | Subtract, but return Nothing if result is negative. 446subVar :: Int -> Maybe Variable -> Maybe Variable 447-- subVar n x = x >>= \ i -> (i - n) <$ guard (n <= i) 448subVar n x = do 449 i <- x 450 guard $ i >= n 451 return $ i - n 452 453-- | Going under a binder. 454underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z 455underBinder = underBinder' 1 456 457-- | Going under @n@ binders. 458underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z 459underBinder' n = local $ \ e -> e { feSingleton = feSingleton e . subVar n } 460 461-- | Changing the 'Modality'. 462underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z 463underModality = local . mapModality . composeModality . getModality 464 465-- | Changing the 'Relevance'. 466underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z 467underRelevance = local . mapRelevance . composeRelevance . getRelevance 468 469-- | Changing the 'FlexRig' context. 470underFlexRig :: (MonadReader r m, LensFlexRig a r, Semigroup a, LensFlexRig a o) => o -> m z -> m z 471underFlexRig = local . over lensFlexRig . composeFlexRig . view lensFlexRig 472 473-- | What happens to the variables occurring under a constructor? 474underConstructor :: (MonadReader r m, LensFlexRig a r, Semigroup a) => ConHead -> Elims -> m z -> m z 475underConstructor (ConHead _c _d i fs) es = 476 case i of 477 -- Coinductive (record) constructors admit infinite cycles: 478 CoInductive -> underFlexRig WeaklyRigid 479 -- Inductive constructors do not admit infinite cycles: 480 Inductive | size es == size fs -> underFlexRig StronglyRigid 481 | otherwise -> underFlexRig WeaklyRigid 482 -- Jesper, 2020-10-22: Issue #4995: treat occurrences in non-fully 483 -- applied constructors as weakly rigid. 484 -- Ulf, 2019-10-18: Now the termination checker treats inductive recursive records 485 -- the same as datatypes, so absense of infinite cycles can be proven in Agda, and thus 486 -- the unifier is allowed to do it too. Test case: test/Succeed/Issue1271a.agda 487 -- WAS: 488 -- -- Inductive record constructors do not admit infinite cycles, 489 -- -- but this cannot be proven inside Agda. 490 -- -- Thus, unification should not prove it either. 491 492--------------------------------------------------------------------------- 493-- * Recursively collecting free variables. 494 495-- | Gather free variables in a collection. 496class Free t where 497 -- Misplaced SPECIALIZE pragma: 498 -- {-# SPECIALIZE freeVars' :: a -> FreeM Any #-} 499 -- So you cannot specialize all instances in one go. :( 500 freeVars' :: IsVarSet a c => t -> FreeM a c 501 502 default freeVars' :: (t ~ f b, Foldable f, Free b) => IsVarSet a c => t -> FreeM a c 503 freeVars' = foldMap freeVars' 504 505 506instance Free Term where 507 -- SPECIALIZE instance does not work as well, see 508 -- https://ghc.haskell.org/trac/ghc/ticket/10434#ticket 509 -- {-# SPECIALIZE instance Free Term All #-} 510 -- {-# SPECIALIZE freeVars' :: Term -> FreeM Any #-} 511 -- {-# SPECIALIZE freeVars' :: Term -> FreeM All #-} 512 -- {-# SPECIALIZE freeVars' :: Term -> FreeM VarSet #-} 513 freeVars' t = case unSpine t of -- #4484: unSpine to avoid projected variables being treated as StronglyRigid 514 Var n ts -> variable n `mappend` do underFlexRig WeaklyRigid $ freeVars' ts 515 -- λ is not considered guarding, as 516 -- we cannot prove that x ≡ λy.x is impossible. 517 Lam _ t -> underFlexRig WeaklyRigid $ freeVars' t 518 Lit _ -> mempty 519 Def _ ts -> underFlexRig WeaklyRigid $ freeVars' ts -- because we are not in TCM 520 -- we cannot query whether we are dealing with a data/record (strongly r.) 521 -- or a definition by pattern matching (weakly rigid) 522 -- thus, we approximate, losing that x = List x is unsolvable 523 Con c _ ts -> underConstructor c ts $ freeVars' ts 524 -- Pi is not guarding, since we cannot prove that A ≡ B → A is impossible. 525 -- Even as we do not permit infinite type expressions, 526 -- we cannot prove their absence (as Set is not inductive). 527 -- Also, this is incompatible with univalence (HoTT). 528 Pi a b -> freeVars' (a,b) 529 Sort s -> freeVars' s 530 Level l -> freeVars' l 531 MetaV m ts -> underFlexRig (Flexible $ singleton m) $ freeVars' ts 532 DontCare mt -> underModality (Modality Irrelevant unitQuantity unitCohesion) $ freeVars' mt 533 Dummy{} -> mempty 534 535instance Free t => Free (Type' t) where 536 freeVars' (El s t) = 537 ifM (asks ((IgnoreNot ==) . feIgnoreSorts)) 538 {- then -} (freeVars' (s, t)) 539 {- else -} (freeVars' t) 540 541instance Free Sort where 542 freeVars' s = 543 ifM (asks ((IgnoreAll ==) . feIgnoreSorts)) mempty $ {- else -} 544 case s of 545 Type a -> freeVars' a 546 Prop a -> freeVars' a 547 Inf _ _ -> mempty 548 SSet a -> freeVars' a 549 SizeUniv -> mempty 550 LockUniv -> mempty 551 PiSort a s1 s2 -> underFlexRig (Flexible mempty) (freeVars' $ unDom a) `mappend` 552 underFlexRig WeaklyRigid (freeVars' (s1, s2)) 553 FunSort s1 s2 -> freeVars' s1 `mappend` freeVars' s2 554 UnivSort s -> underFlexRig WeaklyRigid $ freeVars' s 555 MetaS x es -> underFlexRig (Flexible $ singleton x) $ freeVars' es 556 DefS _ es -> underFlexRig WeaklyRigid $ freeVars' es 557 DummyS{} -> mempty 558 559instance Free Level where 560 freeVars' (Max _ as) = freeVars' as 561 562instance Free t => Free (PlusLevel' t) where 563 freeVars' (Plus _ l) = freeVars' l 564 565instance Free t => Free [t] where 566instance Free t => Free (Maybe t) where 567instance Free t => Free (WithHiding t) where 568instance Free t => Free (Named nm t) 569 570instance (Free t, Free u) => Free (t, u) where 571 freeVars' (t, u) = freeVars' t `mappend` freeVars' u 572 573instance (Free t, Free u, Free v) => Free (t, u, v) where 574 freeVars' (t, u, v) = freeVars' t `mappend` freeVars' u `mappend` freeVars' v 575 576instance Free t => Free (Elim' t) where 577 freeVars' (Apply t) = freeVars' t 578 freeVars' (Proj{} ) = mempty 579 freeVars' (IApply x y r) = freeVars' (x,y,r) 580 581instance Free t => Free (Arg t) where 582 freeVars' t = underModality (getModality t) $ freeVars' $ unArg t 583 584instance Free t => Free (Dom t) where 585 freeVars' d = freeVars' (domTactic d, unDom d) 586 587instance Free t => Free (Abs t) where 588 freeVars' (Abs _ b) = underBinder $ freeVars' b 589 freeVars' (NoAbs _ b) = freeVars' b 590 591instance Free t => Free (Tele t) where 592 freeVars' EmptyTel = mempty 593 freeVars' (ExtendTel t tel) = freeVars' (t, tel) 594 595instance Free Clause where 596 freeVars' cl = underBinder' (size $ clauseTel cl) $ freeVars' $ clauseBody cl 597 598instance Free EqualityView where 599 freeVars' = \case 600 OtherType t -> freeVars' t 601 IdiomType t -> freeVars' t 602 EqualityType s _eq l t a b -> freeVars' (s, l, [t, a, b]) 603