1{-# LANGUAGE NondecreasingIndentation #-} 2 3module Agda.TypeChecking.Reduce where 4 5import Control.Monad.Reader 6 7import Data.Maybe 8import Data.Map (Map) 9import qualified Data.IntMap as IntMap 10import Data.Foldable 11import Data.Traversable 12import Data.HashMap.Strict (HashMap) 13import qualified Data.Set as Set 14 15import Agda.Interaction.Options 16 17import Agda.Syntax.Position 18import Agda.Syntax.Common 19import Agda.Syntax.Internal 20import Agda.Syntax.Internal.MetaVars 21import Agda.Syntax.Scope.Base (Scope) 22import Agda.Syntax.Literal 23 24import {-# SOURCE #-} Agda.TypeChecking.Irrelevance (workOnTypes, isPropM) 25import {-# SOURCE #-} Agda.TypeChecking.Level (reallyUnLevelView) 26import Agda.TypeChecking.Monad hiding ( enterClosure, constructorForm ) 27import Agda.TypeChecking.Substitute 28import Agda.TypeChecking.CompiledClause 29import Agda.TypeChecking.EtaContract 30 31import Agda.TypeChecking.Reduce.Monad 32 33import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Match 34import {-# SOURCE #-} Agda.TypeChecking.Patterns.Match 35import {-# SOURCE #-} Agda.TypeChecking.Pretty 36import {-# SOURCE #-} Agda.TypeChecking.Rewriting 37import {-# SOURCE #-} Agda.TypeChecking.Reduce.Fast 38 39import Agda.Utils.Functor 40import Agda.Utils.Lens 41import Agda.Utils.List 42import Agda.Utils.Maybe 43import qualified Agda.Utils.Maybe.Strict as Strict 44import Agda.Utils.Monad 45import Agda.Utils.Pretty (prettyShow) 46import Agda.Utils.Size 47import Agda.Utils.Tuple 48import qualified Agda.Utils.SmallSet as SmallSet 49 50import Agda.Utils.Impossible 51 52instantiate :: (Instantiate a, MonadReduce m) => a -> m a 53instantiate = liftReduce . instantiate' 54 55instantiateFull :: (InstantiateFull a, MonadReduce m) => a -> m a 56instantiateFull = liftReduce . instantiateFull' 57 58reduce :: (Reduce a, MonadReduce m) => a -> m a 59reduce = liftReduce . reduce' 60 61reduceB :: (Reduce a, MonadReduce m) => a -> m (Blocked a) 62reduceB = liftReduce . reduceB' 63 64-- Reduce a term and also produce a blocker signifying when 65-- this reduction should be retried. 66reduceWithBlocker :: (Reduce a, IsMeta a, MonadReduce m) => a -> m (Blocker, a) 67reduceWithBlocker a = ifBlocked a 68 (\b a' -> return (b, a')) 69 (\_ a' -> return (neverUnblock, a')) 70 71-- Reduce a term and call the continuation. If the continuation is 72-- blocked, the whole call is blocked either on what blocked the reduction 73-- or on what blocked the continuation (using `blockedOnEither`). 74withReduced 75 :: (Reduce a, IsMeta a, MonadReduce m, MonadBlock m) 76 => a -> (a -> m b) -> m b 77withReduced a cont = ifBlocked a (\b a' -> addOrUnblocker b $ cont a') (\_ a' -> cont a') 78 79normalise :: (Normalise a, MonadReduce m) => a -> m a 80normalise = liftReduce . normalise' 81 82-- | Normalise the given term but also preserve blocking tags 83-- TODO: implement a more efficient version of this. 84normaliseB :: (MonadReduce m, Reduce t, Normalise t) => t -> m (Blocked t) 85normaliseB = normalise >=> reduceB 86 87simplify :: (Simplify a, MonadReduce m) => a -> m a 88simplify = liftReduce . simplify' 89 90-- | Meaning no metas left in the instantiation. 91isFullyInstantiatedMeta :: MetaId -> TCM Bool 92isFullyInstantiatedMeta m = do 93 mv <- lookupMeta m 94 case mvInstantiation mv of 95 InstV _tel v -> noMetas <$> instantiateFull v 96 _ -> return False 97 98-- | Blocking on all blockers. 99blockAll :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a) 100blockAll bs = blockedOn block $ fmap ignoreBlocking bs 101 where block = unblockOnAll $ foldMap (Set.singleton . blocker) bs 102 blocker NotBlocked{} = alwaysUnblock 103 blocker (Blocked b _) = b 104 105-- | Blocking on any blockers. 106blockAny :: (Functor f, Foldable f) => f (Blocked a) -> Blocked (f a) 107blockAny bs = blockedOn block $ fmap ignoreBlocking bs 108 where block = case foldMap blocker bs of 109 [] -> alwaysUnblock -- no blockers 110 bs -> unblockOnAny $ Set.fromList bs 111 blocker NotBlocked{} = [] 112 blocker (Blocked b _) = [b] 113 114-- | Instantiate something. 115-- Results in an open meta variable or a non meta. 116-- Doesn't do any reduction, and preserves blocking tags (when blocking meta 117-- is uninstantiated). 118class Instantiate t where 119 instantiate' :: t -> ReduceM t 120 121 default instantiate' :: (t ~ f a, Traversable f, Instantiate a) => t -> ReduceM t 122 instantiate' = traverse instantiate' 123 124instance Instantiate t => Instantiate [t] 125instance Instantiate t => Instantiate (Map k t) 126instance Instantiate t => Instantiate (Maybe t) 127instance Instantiate t => Instantiate (Strict.Maybe t) 128 129instance Instantiate t => Instantiate (Abs t) 130instance Instantiate t => Instantiate (Arg t) 131instance Instantiate t => Instantiate (Elim' t) 132instance Instantiate t => Instantiate (Tele t) 133instance Instantiate t => Instantiate (IPBoundary' t) 134 135instance (Instantiate a, Instantiate b) => Instantiate (a,b) where 136 instantiate' (x,y) = (,) <$> instantiate' x <*> instantiate' y 137 138instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where 139 instantiate' (x,y,z) = (,,) <$> instantiate' x <*> instantiate' y <*> instantiate' z 140 141instance Instantiate Term where 142 instantiate' t@(MetaV x es) = do 143 blocking <- view stInstantiateBlocking <$> getTCState 144 145 mv <- lookupMeta x 146 let mi = mvInstantiation mv 147 148 case mi of 149 InstV tel v -> instantiate' inst 150 where 151 -- A slight complication here is that the meta might be underapplied, 152 -- in which case we have to build the lambda abstraction before 153 -- applying the substitution, or overapplied in which case we need to 154 -- fall back to applyE. 155 (es1, es2) = splitAt (length tel) es 156 vs1 = reverse $ map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es1 157 rho = vs1 ++# wkS (length vs1) idS 158 -- really should be .. ++# emptyS but using wkS makes it reduce to idS 159 -- when applicable 160 -- specification: inst == foldr mkLam v tel `applyE` es 161 inst = applySubst rho (foldr mkLam v $ drop (length es1) tel) `applyE` es2 162 _ | Just m' <- mvTwin mv, blocking -> do 163 instantiate' (MetaV m' es) 164 Open -> return t 165 OpenInstance -> return t 166 BlockedConst u | blocking -> instantiate' . unBrave $ BraveTerm u `applyE` es 167 | otherwise -> return t 168 PostponedTypeCheckingProblem _ -> return t 169 instantiate' (Level l) = levelTm <$> instantiate' l 170 instantiate' (Sort s) = Sort <$> instantiate' s 171 instantiate' t = return t 172 173instance Instantiate t => Instantiate (Type' t) where 174 instantiate' (El s t) = El <$> instantiate' s <*> instantiate' t 175 176instance Instantiate Level where 177 instantiate' (Max m as) = levelMax m <$> instantiate' as 178 179-- Use Traversable instance 180instance Instantiate t => Instantiate (PlusLevel' t) 181 182instance Instantiate a => Instantiate (Blocked a) where 183 instantiate' v@NotBlocked{} = return v 184 instantiate' v@(Blocked b u) = instantiate' b >>= \ case 185 b | b == alwaysUnblock -> notBlocked <$> instantiate' u 186 | otherwise -> return $ Blocked b u 187 188instance Instantiate Blocker where 189 instantiate' (UnblockOnAll bs) = unblockOnAll . Set.fromList <$> mapM instantiate' (Set.toList bs) 190 instantiate' (UnblockOnAny bs) = unblockOnAny . Set.fromList <$> mapM instantiate' (Set.toList bs) 191 instantiate' b@(UnblockOnMeta x) = 192 ifM (isInstantiatedMeta x) (return alwaysUnblock) (return b) 193 instantiate' b@UnblockOnProblem{} = return b 194 195instance Instantiate Sort where 196 instantiate' = \case 197 MetaS x es -> instantiate' (MetaV x es) >>= \case 198 Sort s' -> return s' 199 MetaV x' es' -> return $ MetaS x' es' 200 Def d es' -> return $ DefS d es' 201 _ -> __IMPOSSIBLE__ 202 s -> return s 203 204instance (Instantiate t, Instantiate e) => Instantiate (Dom' t e) where 205 instantiate' (Dom i fin n tac x) = Dom i fin n <$> instantiate' tac <*> instantiate' x 206 207instance Instantiate a => Instantiate (Closure a) where 208 instantiate' cl = do 209 x <- enterClosure cl instantiate' 210 return $ cl { clValue = x } 211 212instance Instantiate Constraint where 213 instantiate' (ValueCmp cmp t u v) = do 214 (t,u,v) <- instantiate' (t,u,v) 215 return $ ValueCmp cmp t u v 216 instantiate' (ValueCmpOnFace cmp p t u v) = do 217 ((p,t),u,v) <- instantiate' ((p,t),u,v) 218 return $ ValueCmpOnFace cmp p t u v 219 instantiate' (ElimCmp cmp fs t v as bs) = 220 ElimCmp cmp fs <$> instantiate' t <*> instantiate' v <*> instantiate' as <*> instantiate' bs 221 instantiate' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> instantiate' (u,v) 222 instantiate' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> instantiate' (a,b) 223 instantiate' (UnBlock m) = return $ UnBlock m 224 instantiate' (FindInstance m cs) = FindInstance m <$> mapM instantiate' cs 225 instantiate' (IsEmpty r t) = IsEmpty r <$> instantiate' t 226 instantiate' (CheckSizeLtSat t) = CheckSizeLtSat <$> instantiate' t 227 instantiate' c@CheckFunDef{} = return c 228 instantiate' (HasBiggerSort a) = HasBiggerSort <$> instantiate' a 229 instantiate' (HasPTSRule a b) = uncurry HasPTSRule <$> instantiate' (a,b) 230 instantiate' (CheckLockedVars a b c d) = 231 CheckLockedVars <$> instantiate' a <*> instantiate' b <*> instantiate' c <*> instantiate' d 232 instantiate' (UnquoteTactic t h g) = UnquoteTactic <$> instantiate' t <*> instantiate' h <*> instantiate' g 233 instantiate' c@CheckMetaInst{} = return c 234 instantiate' (UsableAtModality mod t) = UsableAtModality mod <$> instantiate' t 235 236instance Instantiate CompareAs where 237 instantiate' (AsTermsOf a) = AsTermsOf <$> instantiate' a 238 instantiate' AsSizes = return AsSizes 239 instantiate' AsTypes = return AsTypes 240 241instance Instantiate Candidate where 242 instantiate' (Candidate q u t ov) = Candidate q <$> instantiate' u <*> instantiate' t <*> pure ov 243 244instance Instantiate EqualityView where 245 instantiate' (OtherType t) = OtherType 246 <$> instantiate' t 247 instantiate' (IdiomType t) = IdiomType 248 <$> instantiate' t 249 instantiate' (EqualityType s eq l t a b) = EqualityType 250 <$> instantiate' s 251 <*> return eq 252 <*> mapM instantiate' l 253 <*> instantiate' t 254 <*> instantiate' a 255 <*> instantiate' b 256 257--------------------------------------------------------------------------- 258-- * Reduction to weak head normal form. 259--------------------------------------------------------------------------- 260 261-- | Is something (an elimination of) a meta variable? 262-- Does not perform any reductions. 263 264class IsMeta a where 265 isMeta :: a -> Maybe MetaId 266 267instance IsMeta Term where 268 isMeta (MetaV m _) = Just m 269 isMeta _ = Nothing 270 271instance IsMeta a => IsMeta (Sort' a) where 272 isMeta (MetaS m _) = Just m 273 isMeta _ = Nothing 274 275instance IsMeta a => IsMeta (Type'' t a) where 276 isMeta = isMeta . unEl 277 278instance IsMeta a => IsMeta (Elim' a) where 279 isMeta Proj{} = Nothing 280 isMeta IApply{} = Nothing 281 isMeta (Apply a) = isMeta a 282 283instance IsMeta a => IsMeta (Arg a) where 284 isMeta = isMeta . unArg 285 286instance IsMeta a => IsMeta (Level' a) where 287 isMeta (Max 0 [l]) = isMeta l 288 isMeta _ = Nothing 289 290instance IsMeta a => IsMeta (PlusLevel' a) where 291 isMeta (Plus 0 l) = isMeta l 292 isMeta _ = Nothing 293 294instance IsMeta CompareAs where 295 isMeta (AsTermsOf a) = isMeta a 296 isMeta AsSizes = Nothing 297 isMeta AsTypes = Nothing 298 299-- | Case on whether a term is blocked on a meta (or is a meta). 300-- That means it can change its shape when the meta is instantiated. 301ifBlocked 302 :: (Reduce t, IsMeta t, MonadReduce m) 303 => t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a 304ifBlocked t blocked unblocked = do 305 t <- reduceB t 306 case t of 307 Blocked m t -> blocked m t 308 NotBlocked nb t -> case isMeta t of -- #4899: MetaS counts as NotBlocked at the moment 309 Just m -> blocked (unblockOnMeta m) t 310 Nothing -> unblocked nb t 311 312-- | Throw pattern violation if blocked or a meta. 313abortIfBlocked :: (MonadReduce m, MonadBlock m, IsMeta t, Reduce t) => t -> m t 314abortIfBlocked t = ifBlocked t (const . patternViolation) (const return) 315 316isBlocked 317 :: (Reduce t, IsMeta t, MonadReduce m) 318 => t -> m (Maybe Blocker) 319isBlocked t = ifBlocked t (\m _ -> return $ Just m) (\_ _ -> return Nothing) 320 321class Reduce t where 322 reduce' :: t -> ReduceM t 323 reduceB' :: t -> ReduceM (Blocked t) 324 325 reduce' t = ignoreBlocking <$> reduceB' t 326 reduceB' t = notBlocked <$> reduce' t 327 328instance Reduce Type where 329 reduce' (El s t) = workOnTypes $ El s <$> reduce' t 330 reduceB' (El s t) = workOnTypes $ fmap (El s) <$> reduceB' t 331 332instance Reduce Sort where 333 reduce' s = do 334 s <- instantiate' s 335 case s of 336 PiSort a s1 s2 -> do 337 (s1' , s2') <- reduce' (s1 , s2) 338 maybe (return $ PiSort a s1' s2') reduce' $ piSort' a s1' s2' 339 FunSort s1 s2 -> do 340 (s1' , s2') <- reduce (s1 , s2) 341 maybe (return $ FunSort s1' s2') reduce' $ funSort' s1' s2' 342 UnivSort s' -> do 343 s' <- reduce' s' 344 caseMaybe (univSort' s') (return $ UnivSort s') reduce' 345 Prop s' -> Prop <$> reduce' s' 346 Type s' -> Type <$> reduce' s' 347 Inf f n -> return $ Inf f n 348 SSet s' -> SSet <$> reduce' s' 349 SizeUniv -> return SizeUniv 350 LockUniv -> return LockUniv 351 MetaS x es -> return s 352 DefS d es -> return s -- postulated sorts do not reduce 353 DummyS{} -> return s 354 355instance Reduce Elim where 356 reduce' (Apply v) = Apply <$> reduce' v 357 reduce' (Proj o f)= pure $ Proj o f 358 reduce' (IApply x y v) = IApply <$> reduce' x <*> reduce' y <*> reduce' v 359 360instance Reduce Level where 361 reduce' (Max m as) = levelMax m <$> mapM reduce' as 362 reduceB' (Max m as) = fmap (levelMax m) . blockAny <$> traverse reduceB' as 363 364instance Reduce PlusLevel where 365 reduceB' (Plus n l) = fmap (Plus n) <$> reduceB' l 366 367instance (Subst a, Reduce a) => Reduce (Abs a) where 368 reduce' b@(Abs x _) = Abs x <$> underAbstraction_ b reduce' 369 reduce' (NoAbs x v) = NoAbs x <$> reduce' v 370 371-- Lists are never blocked 372instance Reduce t => Reduce [t] where 373 reduce' = traverse reduce' 374 375instance Reduce t => Reduce (Arg t) where 376 reduce' a = case getRelevance a of 377 Irrelevant -> return a -- Don't reduce' irr. args!? 378 -- Andreas, 2018-03-03, caused #2989. 379 _ -> traverse reduce' a 380 381 reduceB' t = traverse id <$> traverse reduceB' t 382 383instance Reduce t => Reduce (Dom t) where 384 reduce' = traverse reduce' 385 reduceB' t = traverse id <$> traverse reduceB' t 386 387instance (Reduce a, Reduce b) => Reduce (a,b) where 388 reduce' (x,y) = (,) <$> reduce' x <*> reduce' y 389 reduceB' (x,y) = do 390 x <- reduceB' x 391 y <- reduceB' y 392 let blk = void x `mappend` void y 393 xy = (ignoreBlocking x , ignoreBlocking y) 394 return $ blk $> xy 395 396instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where 397 reduce' (x,y,z) = (,,) <$> reduce' x <*> reduce' y <*> reduce' z 398 reduceB' (x,y,z) = do 399 x <- reduceB' x 400 y <- reduceB' y 401 z <- reduceB' z 402 let blk = void x `mappend` void y `mappend` void z 403 xyz = (ignoreBlocking x , ignoreBlocking y , ignoreBlocking z) 404 return $ blk $> xyz 405 406reduceIApply :: ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term) 407reduceIApply = reduceIApply' reduceB' 408 409reduceIApply' :: (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term) -> [Elim] -> ReduceM (Blocked Term) 410reduceIApply' red d (IApply x y r : es) = do 411 view <- intervalView' 412 r <- reduceB' r 413 -- We need to propagate the blocking information so that e.g. 414 -- we postpone "someNeutralPath ?0 = a" rather than fail. 415 case view (ignoreBlocking r) of 416 IZero -> red (applyE x es) 417 IOne -> red (applyE y es) 418 _ -> fmap (<* r) (reduceIApply' red d es) 419reduceIApply' red d (_ : es) = reduceIApply' red d es 420reduceIApply' _ d [] = d 421 422instance Reduce DeBruijnPattern where 423 reduceB' (DotP o v) = fmap (DotP o) <$> reduceB' v 424 reduceB' p = return $ notBlocked p 425 426instance Reduce Term where 427 reduceB' = {-# SCC "reduce'<Term>" #-} maybeFastReduceTerm 428 429shouldTryFastReduce :: ReduceM Bool 430shouldTryFastReduce = (optFastReduce <$> pragmaOptions) `and2M` do 431 allowed <- asksTC envAllowedReductions 432 let optionalReductions = SmallSet.fromList [NonTerminatingReductions, UnconfirmedReductions] 433 requiredReductions = allReductions SmallSet.\\ optionalReductions 434 return $ (allowed SmallSet.\\ optionalReductions) == requiredReductions 435 436maybeFastReduceTerm :: Term -> ReduceM (Blocked Term) 437maybeFastReduceTerm v = do 438 let tryFast = case v of 439 Def{} -> True 440 Con{} -> True 441 MetaV{} -> True 442 _ -> False 443 if not tryFast then slowReduceTerm v 444 else 445 case v of 446 MetaV x _ -> ifM (isOpen x) (return $ blocked x v) (maybeFast v) 447 _ -> maybeFast v 448 where 449 isOpen x = isOpenMeta . mvInstantiation <$> lookupMeta x 450 maybeFast v = ifM shouldTryFastReduce (fastReduce v) (slowReduceTerm v) 451 452slowReduceTerm :: Term -> ReduceM (Blocked Term) 453slowReduceTerm v = do 454 v <- instantiate' v 455 let done | MetaV x _ <- v = return $ blocked x v 456 | otherwise = return $ notBlocked v 457 iapp = reduceIApply done 458 case v of 459-- Andreas, 2012-11-05 not reducing meta args does not destroy anything 460-- and seems to save 2% sec on the standard library 461-- MetaV x args -> notBlocked . MetaV x <$> reduce' args 462 MetaV x es -> iapp es 463 Def f es -> flip reduceIApply es $ unfoldDefinitionE False reduceB' (Def f []) f es 464 Con c ci es -> do 465 -- Constructors can reduce' when they come from an 466 -- instantiated module. 467 -- also reduce when they are path constructors 468 v <- flip reduceIApply es 469 $ unfoldDefinitionE False reduceB' (Con c ci []) (conName c) es 470 traverse reduceNat v 471 Sort s -> fmap Sort <$> reduceB' s 472 Level l -> ifM (SmallSet.member LevelReductions <$> asksTC envAllowedReductions) 473 {- then -} (fmap levelTm <$> reduceB' l) 474 {- else -} done 475 Pi _ _ -> done 476 Lit _ -> done 477 Var _ es -> iapp es 478 Lam _ _ -> done 479 DontCare _ -> done 480 Dummy{} -> done 481 where 482 -- NOTE: reduceNat can traverse the entire term. 483 reduceNat v@(Con c ci []) = do 484 mz <- getBuiltin' builtinZero 485 case v of 486 _ | Just v == mz -> return $ Lit $ LitNat 0 487 _ -> return v 488 reduceNat v@(Con c ci [Apply a]) | visible a && isRelevant a = do 489 ms <- getBuiltin' builtinSuc 490 case v of 491 _ | Just (Con c ci []) == ms -> inc <$> reduce' (unArg a) 492 _ -> return v 493 where 494 inc = \case 495 Lit (LitNat n) -> Lit $ LitNat $ n + 1 496 w -> Con c ci [Apply $ defaultArg w] 497 reduceNat v = return v 498 499-- Andreas, 2013-03-20 recursive invokations of unfoldCorecursion 500-- need also to instantiate metas, see Issue 826. 501unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim) 502unfoldCorecursionE (Proj o p) = notBlocked . Proj o <$> getOriginalProjection p 503unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) <$> 504 unfoldCorecursion v 505unfoldCorecursionE (IApply x y r) = do -- TODO check if this makes sense 506 [x,y,r] <- mapM unfoldCorecursion [x,y,r] 507 return $ IApply <$> x <*> y <*> r 508 509unfoldCorecursion :: Term -> ReduceM (Blocked Term) 510unfoldCorecursion v = do 511 v <- instantiate' v 512 case v of 513 Def f es -> unfoldDefinitionE True unfoldCorecursion (Def f []) f es 514 _ -> slowReduceTerm v 515 516-- | If the first argument is 'True', then a single delayed clause may 517-- be unfolded. 518unfoldDefinition :: 519 Bool -> (Term -> ReduceM (Blocked Term)) -> 520 Term -> QName -> Args -> ReduceM (Blocked Term) 521unfoldDefinition unfoldDelayed keepGoing v f args = 522 unfoldDefinitionE unfoldDelayed keepGoing v f (map Apply args) 523 524unfoldDefinitionE :: 525 Bool -> (Term -> ReduceM (Blocked Term)) -> 526 Term -> QName -> Elims -> ReduceM (Blocked Term) 527unfoldDefinitionE unfoldDelayed keepGoing v f es = do 528 r <- unfoldDefinitionStep unfoldDelayed v f es 529 case r of 530 NoReduction v -> return v 531 YesReduction _ v -> keepGoing v 532 533unfoldDefinition' :: 534 Bool -> (Simplification -> Term -> ReduceM (Simplification, Blocked Term)) -> 535 Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) 536unfoldDefinition' unfoldDelayed keepGoing v0 f es = do 537 r <- unfoldDefinitionStep unfoldDelayed v0 f es 538 case r of 539 NoReduction v -> return (NoSimplification, v) 540 YesReduction simp v -> keepGoing simp v 541 542unfoldDefinitionStep :: Bool -> Term -> QName -> Elims -> ReduceM (Reduced (Blocked Term) Term) 543unfoldDefinitionStep unfoldDelayed v0 f es = 544 {-# SCC "reduceDef" #-} do 545 traceSDoc "tc.reduce" 90 ("unfoldDefinitionStep v0" <+> pretty v0) $ do 546 info <- getConstInfo f 547 rewr <- instantiateRewriteRules =<< getRewriteRulesFor f 548 allowed <- asksTC envAllowedReductions 549 prp <- runBlocked $ isPropM $ defType info 550 defOk <- shouldReduceDef f 551 let def = theDef info 552 v = v0 `applyE` es 553 -- Non-terminating functions 554 -- (i.e., those that failed the termination check) 555 -- and delayed definitions 556 -- are not unfolded unless explicitly permitted. 557 dontUnfold = 558 (defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed) 559 || (defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed) 560 || (defDelayed info == Delayed && not unfoldDelayed) 561 || prp == Right True || isIrrelevant (defArgInfo info) 562 || not defOk 563 copatterns = defCopatternLHS info 564 case def of 565 Constructor{conSrcCon = c} -> do 566 let hd = Con (c `withRangeOf` f) ConOSystem 567 rewrite (NotBlocked ReallyNotBlocked ()) hd rewr es 568 Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do 569 pf <- fromMaybe __IMPOSSIBLE__ <$> getPrimitive' x 570 if FunctionReductions `SmallSet.member` allowed 571 then reducePrimitive x v0 f es pf dontUnfold 572 cls (defCompiled info) rewr 573 else noReduction $ notBlocked v 574 PrimitiveSort{ primSort = s } -> yesReduction NoSimplification $ Sort s `applyE` es 575 _ -> do 576 if (RecursiveReductions `SmallSet.member` allowed) || 577 (isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed) || -- includes projection-like 578 (isInlineFun def && InlineReductions `SmallSet.member` allowed) || 579 (definitelyNonRecursive_ def && copatterns && CopatternReductions `SmallSet.member` allowed) || 580 (definitelyNonRecursive_ def && FunctionReductions `SmallSet.member` allowed) 581 then 582 reduceNormalE v0 f (map notReduced es) dontUnfold 583 (defClauses info) (defCompiled info) rewr 584 else noReduction $ notBlocked v -- Andrea(s), 2014-12-05 OK? 585 586 where 587 noReduction = return . NoReduction 588 yesReduction s = return . YesReduction s 589 reducePrimitive x v0 f es pf dontUnfold cls mcc rewr 590 | length es < ar 591 = noReduction $ NotBlocked Underapplied $ v0 `applyE` es -- not fully applied 592 | otherwise = {-# SCC "reducePrimitive" #-} do 593 let (es1,es2) = splitAt ar es 594 args1 = fromMaybe __IMPOSSIBLE__ $ mapM isApplyElim es1 595 r <- primFunImplementation pf args1 (length es2) 596 case r of 597 NoReduction args1' -> do 598 let es1' = map (fmap Apply) args1' 599 if null cls && null rewr then do 600 noReduction $ applyE (Def f []) <$> do 601 blockAll $ map mredToBlocked es1' ++ map notBlocked es2 602 else 603 reduceNormalE v0 f (es1' ++ map notReduced es2) dontUnfold cls mcc rewr 604 YesReduction simpl v -> yesReduction simpl $ v `applyE` es2 605 where 606 ar = primFunArity pf 607 608 mredToBlocked :: IsMeta t => MaybeReduced t -> Blocked t 609 mredToBlocked (MaybeRed NotReduced e) = notBlocked e 610 mredToBlocked (MaybeRed (Reduced b) e) = e <$ b 611 612 reduceNormalE :: Term -> QName -> [MaybeReduced Elim] -> Bool -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> ReduceM (Reduced (Blocked Term) Term) 613 reduceNormalE v0 f es dontUnfold def mcc rewr = {-# SCC "reduceNormal" #-} do 614 traceSDoc "tc.reduce" 90 ("reduceNormalE v0 =" <+> pretty v0) $ do 615 case (def,rewr) of 616 _ | dontUnfold -> traceSLn "tc.reduce" 90 "reduceNormalE: don't unfold (non-terminating or delayed)" $ 617 defaultResult -- non-terminating or delayed 618 ([],[]) -> traceSLn "tc.reduce" 90 "reduceNormalE: no clauses or rewrite rules" $ do 619 -- no definition for head 620 blk <- defBlocked <$> getConstInfo f 621 noReduction $ blk $> vfull 622 (cls,rewr) -> do 623 ev <- appDefE_ f v0 cls mcc rewr es 624 debugReduce ev 625 return ev 626 where 627 defaultResult = noReduction $ NotBlocked ReallyNotBlocked vfull 628 vfull = v0 `applyE` map ignoreReduced es 629 debugReduce ev = verboseS "tc.reduce" 90 $ do 630 case ev of 631 NoReduction v -> do 632 reportSDoc "tc.reduce" 90 $ vcat 633 [ "*** tried to reduce " <+> pretty f 634 , " es = " <+> sep (map (pretty . ignoreReduced) es) 635 -- , "*** tried to reduce " <+> pretty vfull 636 , " stuck on" <+> pretty (ignoreBlocking v) 637 ] 638 YesReduction _simpl v -> do 639 reportSDoc "tc.reduce" 90 $ "*** reduced definition: " <+> pretty f 640 reportSDoc "tc.reduce" 95 $ " result" <+> pretty v 641 642-- | Specialized version to put in boot file. 643reduceDefCopyTCM :: QName -> Elims -> TCM (Reduced () Term) 644reduceDefCopyTCM = reduceDefCopy 645 646-- | Reduce a non-primitive definition if it is a copy linking to another def. 647reduceDefCopy :: forall m. PureTCM m => QName -> Elims -> m (Reduced () Term) 648reduceDefCopy f es = do 649 info <- getConstInfo f 650 case theDef info of 651 _ | not $ defCopy info -> return $ NoReduction () 652 Constructor{conSrcCon = c} -> return $ YesReduction YesSimplification (Con c ConOSystem es) 653 _ -> reduceDef_ info f es 654 where 655 reduceDef_ :: Definition -> QName -> Elims -> m (Reduced () Term) 656 reduceDef_ info f es = case defClauses info of 657 [cl] -> do -- proper copies always have a single clause 658 let v0 = Def f [] -- TODO: could be Con 659 ps = namedClausePats cl 660 nargs = length es 661 -- appDefE_ cannot handle underapplied functions, so we eta-expand here if that's the 662 -- case. We use this function to compute display forms from module applications and in 663 -- that case we don't always have saturated applications. 664 (lam, es') = (unlamView xs, newes) 665 where 666 etaArgs [] _ = [] 667 etaArgs (p : ps) [] 668 | VarP _ x <- namedArg p = Arg (getArgInfo p) (dbPatVarName x) : etaArgs ps [] 669 | otherwise = [] 670 etaArgs (_ : ps) (_ : es) = etaArgs ps es 671 xs = etaArgs ps es 672 n = length xs 673 newes = raise n es ++ [ Apply $ var i <$ x | (i, x) <- zip (downFrom n) xs ] 674 if (defDelayed info == Delayed) || (defNonterminating info) 675 then return $ NoReduction () 676 else do 677 ev <- liftReduce $ appDefE_ f v0 [cl] Nothing mempty $ map notReduced es' 678 case ev of 679 YesReduction simpl t -> return $ YesReduction simpl (lam t) 680 NoReduction{} -> return $ NoReduction () 681 [] -> return $ NoReduction () -- copies of generalizable variables have no clauses (and don't need unfolding) 682 _:_:_ -> __IMPOSSIBLE__ 683 684-- | Reduce simple (single clause) definitions. 685reduceHead :: PureTCM m => Term -> m (Blocked Term) 686reduceHead v = do -- ignoreAbstractMode $ do 687 -- Andreas, 2013-02-18 ignoreAbstractMode leads to information leakage 688 -- see Issue 796 689 690 -- first, possibly rewrite literal v to constructor form 691 v <- constructorForm v 692 traceSDoc "tc.inj.reduce" 30 (ignoreAbstractMode $ "reduceHead" <+> prettyTCM v) $ do 693 case v of 694 Def f es -> do 695 696 abstractMode <- envAbstractMode <$> askTC 697 isAbstract <- treatAbstractly f 698 traceSLn "tc.inj.reduce" 50 ( 699 "reduceHead: we are in " ++ show abstractMode++ "; " ++ prettyShow f ++ 700 " is treated " ++ if isAbstract then "abstractly" else "concretely" 701 ) $ do 702 let v0 = Def f [] 703 red = liftReduce $ unfoldDefinitionE False reduceHead v0 f es 704 def <- theDef <$> getConstInfo f 705 case def of 706 -- Andreas, 2012-11-06 unfold aliases (single clause terminating functions) 707 -- see test/succeed/Issue747 708 -- We restrict this to terminating functions to not make the 709 -- type checker loop here on non-terminating functions. 710 -- see test/fail/TerminationInfiniteRecord 711 Function{ funClauses = [ _ ], funDelayed = NotDelayed, funTerminates = Just True } -> do 712 traceSLn "tc.inj.reduce" 50 ("reduceHead: head " ++ prettyShow f ++ " is Function") $ do 713 red 714 Datatype{ dataClause = Just _ } -> red 715 Record{ recClause = Just _ } -> red 716 _ -> return $ notBlocked v 717 _ -> return $ notBlocked v 718 719-- | Unfold a single inlined function. 720unfoldInlined :: PureTCM m => Term -> m Term 721unfoldInlined v = do 722 inTypes <- viewTC eWorkingOnTypes 723 case v of 724 _ | inTypes -> return v -- Don't inline in types (to avoid unfolding of goals) 725 Def f es -> do 726 info <- getConstInfo f 727 let def = theDef info 728 irr = isIrrelevant $ defArgInfo info 729 case def of -- Only for simple definitions with no pattern matching (TODO: maybe copatterns?) 730 Function{ funCompiled = Just Done{}, funDelayed = NotDelayed } 731 | def ^. funInline , not irr -> liftReduce $ 732 ignoreBlocking <$> unfoldDefinitionE False (return . notBlocked) (Def f []) f es 733 _ -> return v 734 _ -> return v 735 736-- | Apply a definition using the compiled clauses, or fall back to 737-- ordinary clauses if no compiled clauses exist. 738appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) 739appDef_ f v0 cls mcc rewr args = appDefE_ f v0 cls mcc rewr $ map (fmap Apply) args 740 741appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) 742appDefE_ f v0 cls mcc rewr args = 743 localTC (\ e -> e { envAppDef = Just f }) $ 744 maybe (appDefE' v0 cls rewr args) 745 (\cc -> appDefE v0 cc rewr args) mcc 746 747 748-- | Apply a defined function to it's arguments, using the compiled clauses. 749-- The original term is the first argument applied to the third. 750appDef :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) 751appDef v cc rewr args = appDefE v cc rewr $ map (fmap Apply) args 752 753appDefE :: Term -> CompiledClauses -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) 754appDefE v cc rewr es = do 755 traceSDoc "tc.reduce" 90 ("appDefE v = " <+> pretty v) $ do 756 r <- matchCompiledE cc es 757 case r of 758 YesReduction simpl t -> return $ YesReduction simpl t 759 NoReduction es' -> rewrite (void es') (applyE v) rewr (ignoreBlocking es') 760 761-- | Apply a defined function to it's arguments, using the original clauses. 762appDef' :: Term -> [Clause] -> RewriteRules -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) 763appDef' v cls rewr args = appDefE' v cls rewr $ map (fmap Apply) args 764 765appDefE' :: Term -> [Clause] -> RewriteRules -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) 766appDefE' v cls rewr es = traceSDoc "tc.reduce" 90 ("appDefE' v = " <+> pretty v) $ do 767 goCls cls $ map ignoreReduced es 768 where 769 goCls :: [Clause] -> [Elim] -> ReduceM (Reduced (Blocked Term) Term) 770 goCls cl es = do 771 case cl of 772 -- Andreas, 2013-10-26 In case of an incomplete match, 773 -- we just do not reduce. This allows adding single function 774 -- clauses after they have been type-checked, to type-check 775 -- the remaining clauses (see Issue 907). 776 -- Andrea(s), 2014-12-05: We return 'MissingClauses' here, since this 777 -- is the most conservative reason. 778 [] -> rewrite (NotBlocked MissingClauses ()) (applyE v) rewr es 779 cl : cls -> do 780 let pats = namedClausePats cl 781 body = clauseBody cl 782 npats = length pats 783 nvars = size $ clauseTel cl 784 -- if clause is underapplied, skip to next clause 785 if length es < npats then goCls cls es else do 786 let (es0, es1) = splitAt npats es 787 (m, es0) <- matchCopatterns pats es0 788 let es = es0 ++ es1 789 case m of 790 No -> goCls cls es 791 DontKnow b -> rewrite b (applyE v) rewr es 792 Yes simpl vs -- vs is the subst. for the variables bound in body 793 | Just w <- body -> do -- clause has body? 794 -- TODO: let matchPatterns also return the reduced forms 795 -- of the original arguments! 796 -- Andreas, 2013-05-19 isn't this done now? 797 let sigma = buildSubstitution impossible nvars vs 798 return $ YesReduction simpl $ applySubst sigma w `applyE` es1 799 | otherwise -> rewrite (NotBlocked AbsurdMatch ()) (applyE v) rewr es 800 801instance Reduce a => Reduce (Closure a) where 802 reduce' cl = do 803 x <- enterClosure cl reduce' 804 return $ cl { clValue = x } 805 806instance Reduce Telescope where 807 reduce' EmptyTel = return EmptyTel 808 reduce' (ExtendTel a tel) = ExtendTel <$> reduce' a <*> reduce' tel 809 810instance Reduce Constraint where 811 reduce' (ValueCmp cmp t u v) = do 812 (t,u,v) <- reduce' (t,u,v) 813 return $ ValueCmp cmp t u v 814 reduce' (ValueCmpOnFace cmp p t u v) = do 815 ((p,t),u,v) <- reduce' ((p,t),u,v) 816 return $ ValueCmpOnFace cmp p t u v 817 reduce' (ElimCmp cmp fs t v as bs) = 818 ElimCmp cmp fs <$> reduce' t <*> reduce' v <*> reduce' as <*> reduce' bs 819 reduce' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> reduce' (u,v) 820 reduce' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> reduce' (a,b) 821 reduce' (UnBlock m) = return $ UnBlock m 822 reduce' (FindInstance m cs) = FindInstance m <$> mapM reduce' cs 823 reduce' (IsEmpty r t) = IsEmpty r <$> reduce' t 824 reduce' (CheckSizeLtSat t) = CheckSizeLtSat <$> reduce' t 825 reduce' c@CheckFunDef{} = return c 826 reduce' (HasBiggerSort a) = HasBiggerSort <$> reduce' a 827 reduce' (HasPTSRule a b) = uncurry HasPTSRule <$> reduce' (a,b) 828 reduce' (UnquoteTactic t h g) = UnquoteTactic <$> reduce' t <*> reduce' h <*> reduce' g 829 reduce' (CheckLockedVars a b c d) = 830 CheckLockedVars <$> reduce' a <*> reduce' b <*> reduce' c <*> reduce' d 831 reduce' c@CheckMetaInst{} = return c 832 reduce' (UsableAtModality mod t) = UsableAtModality mod <$> reduce' t 833 834instance Reduce CompareAs where 835 reduce' (AsTermsOf a) = AsTermsOf <$> reduce' a 836 reduce' AsSizes = return AsSizes 837 reduce' AsTypes = return AsTypes 838 839instance Reduce e => Reduce (Map k e) where 840 reduce' = traverse reduce' 841 842instance Reduce Candidate where 843 reduce' (Candidate q u t ov) = Candidate q <$> reduce' u <*> reduce' t <*> pure ov 844 845instance Reduce EqualityView where 846 reduce' (OtherType t) = OtherType 847 <$> reduce' t 848 reduce' (IdiomType t) = IdiomType 849 <$> reduce' t 850 reduce' (EqualityType s eq l t a b) = EqualityType 851 <$> reduce' s 852 <*> return eq 853 <*> mapM reduce' l 854 <*> reduce' t 855 <*> reduce' a 856 <*> reduce' b 857 858instance Reduce t => Reduce (IPBoundary' t) where 859 reduce' = traverse reduce' 860 reduceB' = fmap sequenceA . traverse reduceB' 861 862--------------------------------------------------------------------------- 863-- * Simplification 864--------------------------------------------------------------------------- 865 866-- | Only unfold definitions if this leads to simplification 867-- which means that a constructor/literal pattern is matched. 868-- We include reduction of IApply patterns, as `p i0` is akin to 869-- matcing on the `i0` constructor of interval. 870class Simplify t where 871 simplify' :: t -> ReduceM t 872 873 default simplify' :: (t ~ f a, Traversable f, Simplify a) => t -> ReduceM t 874 simplify' = traverse simplify' 875 876-- boring instances: 877 878instance Simplify t => Simplify [t] 879instance Simplify t => Simplify (Map k t) 880instance Simplify t => Simplify (Maybe t) 881instance Simplify t => Simplify (Strict.Maybe t) 882 883instance Simplify t => Simplify (Arg t) 884instance Simplify t => Simplify (Elim' t) 885instance Simplify t => Simplify (Named name t) 886instance Simplify t => Simplify (IPBoundary' t) 887 888instance (Simplify a, Simplify b) => Simplify (a,b) where 889 simplify' (x,y) = (,) <$> simplify' x <*> simplify' y 890 891instance (Simplify a, Simplify b, Simplify c) => Simplify (a,b,c) where 892 simplify' (x,y,z) = 893 do (x,(y,z)) <- simplify' (x,(y,z)) 894 return (x,y,z) 895 896instance Simplify Bool where 897 simplify' = return 898 899-- interesting instances: 900 901instance Simplify Term where 902 simplify' v = do 903 v <- instantiate' v 904 let iapp es m = ignoreBlocking <$> reduceIApply' (fmap notBlocked . simplify') (notBlocked <$> m) es 905 case v of 906 Def f vs -> iapp vs $ do 907 let keepGoing simp v = return (simp, notBlocked v) 908 (simpl, v) <- unfoldDefinition' False keepGoing (Def f []) f vs 909 traceSDoc "tc.simplify'" 90 ( 910 text ("simplify': unfolding definition returns " ++ show simpl) 911 <+> pretty (ignoreBlocking v)) $ do 912 case simpl of 913 YesSimplification -> simplifyBlocked' v -- Dangerous, but if @simpl@ then @v /= Def f vs@ 914 NoSimplification -> Def f <$> simplify' vs 915 MetaV x vs -> iapp vs $ MetaV x <$> simplify' vs 916 Con c ci vs-> iapp vs $ Con c ci <$> simplify' vs 917 Sort s -> Sort <$> simplify' s 918 Level l -> levelTm <$> simplify' l 919 Pi a b -> Pi <$> simplify' a <*> simplify' b 920 Lit l -> return v 921 Var i vs -> iapp vs $ Var i <$> simplify' vs 922 Lam h v -> Lam h <$> simplify' v 923 DontCare v -> dontCare <$> simplify' v 924 Dummy{} -> return v 925 926simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t 927simplifyBlocked' (Blocked _ t) = return t 928simplifyBlocked' (NotBlocked _ t) = simplify' t -- Andrea(s), 2014-12-05 OK? 929 930instance Simplify t => Simplify (Type' t) where 931 simplify' (El s t) = El <$> simplify' s <*> simplify' t 932 933instance Simplify Sort where 934 simplify' s = do 935 case s of 936 PiSort a s1 s2 -> piSort <$> simplify' a <*> simplify' s1 <*> simplify' s2 937 FunSort s1 s2 -> funSort <$> simplify' s1 <*> simplify' s2 938 UnivSort s -> univSort <$> simplify' s 939 Type s -> Type <$> simplify' s 940 Prop s -> Prop <$> simplify' s 941 Inf _ _ -> return s 942 SSet s -> SSet <$> simplify' s 943 SizeUniv -> return s 944 LockUniv -> return s 945 MetaS x es -> MetaS x <$> simplify' es 946 DefS d es -> DefS d <$> simplify' es 947 DummyS{} -> return s 948 949instance Simplify Level where 950 simplify' (Max m as) = levelMax m <$> simplify' as 951 952instance Simplify PlusLevel where 953 simplify' (Plus n l) = Plus n <$> simplify' l 954 955instance (Subst a, Simplify a) => Simplify (Abs a) where 956 simplify' a@(Abs x _) = Abs x <$> underAbstraction_ a simplify' 957 simplify' (NoAbs x v) = NoAbs x <$> simplify' v 958 959instance Simplify t => Simplify (Dom t) where 960 simplify' = traverse simplify' 961 962instance Simplify a => Simplify (Closure a) where 963 simplify' cl = do 964 x <- enterClosure cl simplify' 965 return $ cl { clValue = x } 966 967instance (Subst a, Simplify a) => Simplify (Tele a) where 968 simplify' EmptyTel = return EmptyTel 969 simplify' (ExtendTel a b) = uncurry ExtendTel <$> simplify' (a, b) 970 971instance Simplify ProblemConstraint where 972 simplify' (PConstr pid unblock c) = PConstr pid unblock <$> simplify' c 973 974instance Simplify Constraint where 975 simplify' (ValueCmp cmp t u v) = do 976 (t,u,v) <- simplify' (t,u,v) 977 return $ ValueCmp cmp t u v 978 simplify' (ValueCmpOnFace cmp p t u v) = do 979 ((p,t),u,v) <- simplify' ((p,t),u,v) 980 return $ ValueCmp cmp (AsTermsOf t) u v 981 simplify' (ElimCmp cmp fs t v as bs) = 982 ElimCmp cmp fs <$> simplify' t <*> simplify' v <*> simplify' as <*> simplify' bs 983 simplify' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> simplify' (u,v) 984 simplify' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> simplify' (a,b) 985 simplify' (UnBlock m) = return $ UnBlock m 986 simplify' (FindInstance m cs) = FindInstance m <$> mapM simplify' cs 987 simplify' (IsEmpty r t) = IsEmpty r <$> simplify' t 988 simplify' (CheckSizeLtSat t) = CheckSizeLtSat <$> simplify' t 989 simplify' c@CheckFunDef{} = return c 990 simplify' (HasBiggerSort a) = HasBiggerSort <$> simplify' a 991 simplify' (HasPTSRule a b) = uncurry HasPTSRule <$> simplify' (a,b) 992 simplify' (UnquoteTactic t h g) = UnquoteTactic <$> simplify' t <*> simplify' h <*> simplify' g 993 simplify' (CheckLockedVars a b c d) = 994 CheckLockedVars <$> simplify' a <*> simplify' b <*> simplify' c <*> simplify' d 995 simplify' c@CheckMetaInst{} = return c 996 simplify' (UsableAtModality mod t) = UsableAtModality mod <$> simplify' t 997 998instance Simplify CompareAs where 999 simplify' (AsTermsOf a) = AsTermsOf <$> simplify' a 1000 simplify' AsSizes = return AsSizes 1001 simplify' AsTypes = return AsTypes 1002 1003-- UNUSED 1004-- instance Simplify ConPatternInfo where 1005-- simplify' (ConPatternInfo mr mt) = ConPatternInfo mr <$> simplify' mt 1006 1007-- UNUSED 1008-- instance Simplify Pattern where 1009-- simplify' p = case p of 1010-- VarP _ -> return p 1011-- LitP _ -> return p 1012-- ConP c ci ps -> ConP c <$> simplify' ci <*> simplify' ps 1013-- DotP v -> DotP <$> simplify' v 1014-- ProjP _ -> return p 1015 1016instance Simplify DisplayForm where 1017 simplify' (Display n ps v) = Display n <$> simplify' ps <*> return v 1018 1019instance Simplify Candidate where 1020 simplify' (Candidate q u t ov) = Candidate q <$> simplify' u <*> simplify' t <*> pure ov 1021 1022instance Simplify EqualityView where 1023 simplify' (OtherType t) = OtherType 1024 <$> simplify' t 1025 simplify' (IdiomType t) = IdiomType 1026 <$> simplify' t 1027 simplify' (EqualityType s eq l t a b) = EqualityType 1028 <$> simplify' s 1029 <*> return eq 1030 <*> mapM simplify' l 1031 <*> simplify' t 1032 <*> simplify' a 1033 <*> simplify' b 1034 1035--------------------------------------------------------------------------- 1036-- * Normalisation 1037--------------------------------------------------------------------------- 1038 1039class Normalise t where 1040 normalise' :: t -> ReduceM t 1041 1042 default normalise' :: (t ~ f a, Traversable f, Normalise a) => t -> ReduceM t 1043 normalise' = traverse normalise' 1044 1045-- boring instances: 1046 1047instance Normalise t => Normalise [t] 1048instance Normalise t => Normalise (Map k t) 1049instance Normalise t => Normalise (Maybe t) 1050instance Normalise t => Normalise (Strict.Maybe t) 1051 1052-- Arg not included since we do not normalize irrelevant subterms 1053-- Elim' not included since it contains Arg 1054instance Normalise t => Normalise (Named name t) 1055instance Normalise t => Normalise (IPBoundary' t) 1056instance Normalise t => Normalise (WithHiding t) 1057 1058instance (Normalise a, Normalise b) => Normalise (a,b) where 1059 normalise' (x,y) = (,) <$> normalise' x <*> normalise' y 1060 1061instance (Normalise a, Normalise b, Normalise c) => Normalise (a,b,c) where 1062 normalise' (x,y,z) = 1063 do (x,(y,z)) <- normalise' (x,(y,z)) 1064 return (x,y,z) 1065 1066instance Normalise Bool where 1067 normalise' = return 1068 1069instance Normalise Char where 1070 normalise' = return 1071 1072instance Normalise Int where 1073 normalise' = return 1074 1075instance Normalise DBPatVar where 1076 normalise' = return 1077 1078-- interesting instances: 1079 1080instance Normalise Sort where 1081 normalise' s = do 1082 s <- reduce' s 1083 case s of 1084 PiSort a s1 s2 -> piSort <$> normalise' a <*> normalise' s1 <*> normalise' s2 1085 FunSort s1 s2 -> funSort <$> normalise' s1 <*> normalise' s2 1086 UnivSort s -> univSort <$> normalise' s 1087 Prop s -> Prop <$> normalise' s 1088 Type s -> Type <$> normalise' s 1089 Inf _ _ -> return s 1090 SSet s -> SSet <$> normalise' s 1091 SizeUniv -> return SizeUniv 1092 LockUniv -> return LockUniv 1093 MetaS x es -> return s 1094 DefS d es -> return s 1095 DummyS{} -> return s 1096 1097instance Normalise t => Normalise (Type' t) where 1098 normalise' (El s t) = El <$> normalise' s <*> normalise' t 1099 1100instance Normalise Term where 1101 normalise' v = ifM shouldTryFastReduce (fastNormalise v) (slowNormaliseArgs =<< reduce' v) 1102 1103slowNormaliseArgs :: Term -> ReduceM Term 1104slowNormaliseArgs = \case 1105 Var n vs -> Var n <$> normalise' vs 1106 Con c ci vs -> Con c ci <$> normalise' vs 1107 Def f vs -> Def f <$> normalise' vs 1108 MetaV x vs -> MetaV x <$> normalise' vs 1109 v@(Lit _) -> return v 1110 Level l -> levelTm <$> normalise' l 1111 Lam h b -> Lam h <$> normalise' b 1112 Sort s -> Sort <$> normalise' s 1113 Pi a b -> uncurry Pi <$> normalise' (a, b) 1114 v@DontCare{}-> return v 1115 v@Dummy{} -> return v 1116 1117-- Note: not the default instance for Elim' since we do something special for Arg. 1118instance Normalise t => Normalise (Elim' t) where 1119 normalise' (Apply v) = Apply <$> normalise' v -- invokes Normalise Arg here 1120 normalise' (Proj o f)= pure $ Proj o f 1121 normalise' (IApply x y v) = IApply <$> normalise' x <*> normalise' y <*> normalise' v 1122 1123instance Normalise Level where 1124 normalise' (Max m as) = levelMax m <$> normalise' as 1125 1126instance Normalise PlusLevel where 1127 normalise' (Plus n l) = Plus n <$> normalise' l 1128 1129instance (Subst a, Normalise a) => Normalise (Abs a) where 1130 normalise' a@(Abs x _) = Abs x <$> underAbstraction_ a normalise' 1131 normalise' (NoAbs x v) = NoAbs x <$> normalise' v 1132 1133instance Normalise t => Normalise (Arg t) where 1134 normalise' a 1135 | isIrrelevant a = return a -- Andreas, 2012-04-02: Do not normalize irrelevant terms!? 1136 | otherwise = traverse normalise' a 1137 1138instance Normalise t => Normalise (Dom t) where 1139 normalise' = traverse normalise' 1140 1141instance Normalise a => Normalise (Closure a) where 1142 normalise' cl = do 1143 x <- enterClosure cl normalise' 1144 return $ cl { clValue = x } 1145 1146instance (Subst a, Normalise a) => Normalise (Tele a) where 1147 normalise' EmptyTel = return EmptyTel 1148 normalise' (ExtendTel a b) = uncurry ExtendTel <$> normalise' (a, b) 1149 1150instance Normalise ProblemConstraint where 1151 normalise' (PConstr pid unblock c) = PConstr pid unblock <$> normalise' c 1152 1153instance Normalise Constraint where 1154 normalise' (ValueCmp cmp t u v) = do 1155 (t,u,v) <- normalise' (t,u,v) 1156 return $ ValueCmp cmp t u v 1157 normalise' (ValueCmpOnFace cmp p t u v) = do 1158 ((p,t),u,v) <- normalise' ((p,t),u,v) 1159 return $ ValueCmpOnFace cmp p t u v 1160 normalise' (ElimCmp cmp fs t v as bs) = 1161 ElimCmp cmp fs <$> normalise' t <*> normalise' v <*> normalise' as <*> normalise' bs 1162 normalise' (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> normalise' (u,v) 1163 normalise' (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> normalise' (a,b) 1164 normalise' (UnBlock m) = return $ UnBlock m 1165 normalise' (FindInstance m cs) = FindInstance m <$> mapM normalise' cs 1166 normalise' (IsEmpty r t) = IsEmpty r <$> normalise' t 1167 normalise' (CheckSizeLtSat t) = CheckSizeLtSat <$> normalise' t 1168 normalise' c@CheckFunDef{} = return c 1169 normalise' (HasBiggerSort a) = HasBiggerSort <$> normalise' a 1170 normalise' (HasPTSRule a b) = uncurry HasPTSRule <$> normalise' (a,b) 1171 normalise' (UnquoteTactic t h g) = UnquoteTactic <$> normalise' t <*> normalise' h <*> normalise' g 1172 normalise' (CheckLockedVars a b c d) = 1173 CheckLockedVars <$> normalise' a <*> normalise' b <*> normalise' c <*> normalise' d 1174 normalise' c@CheckMetaInst{} = return c 1175 normalise' (UsableAtModality mod t) = UsableAtModality mod <$> normalise' t 1176 1177instance Normalise CompareAs where 1178 normalise' (AsTermsOf a) = AsTermsOf <$> normalise' a 1179 normalise' AsSizes = return AsSizes 1180 normalise' AsTypes = return AsTypes 1181 1182instance Normalise ConPatternInfo where 1183 normalise' i = normalise' (conPType i) <&> \ t -> i { conPType = t } 1184 1185instance Normalise a => Normalise (Pattern' a) where 1186 normalise' p = case p of 1187 VarP o x -> VarP o <$> normalise' x 1188 LitP{} -> return p 1189 ConP c mt ps -> ConP c <$> normalise' mt <*> normalise' ps 1190 DefP o q ps -> DefP o q <$> normalise' ps 1191 DotP o v -> DotP o <$> normalise' v 1192 ProjP{} -> return p 1193 IApplyP o t u x -> IApplyP o <$> normalise' t <*> normalise' u <*> normalise' x 1194 1195instance Normalise DisplayForm where 1196 normalise' (Display n ps v) = Display n <$> normalise' ps <*> return v 1197 1198instance Normalise Candidate where 1199 normalise' (Candidate q u t ov) = Candidate q <$> normalise' u <*> normalise' t <*> pure ov 1200 1201instance Normalise EqualityView where 1202 normalise' (OtherType t) = OtherType 1203 <$> normalise' t 1204 normalise' (IdiomType t) = IdiomType 1205 <$> normalise' t 1206 normalise' (EqualityType s eq l t a b) = EqualityType 1207 <$> normalise' s 1208 <*> return eq 1209 <*> mapM normalise' l 1210 <*> normalise' t 1211 <*> normalise' a 1212 <*> normalise' b 1213 1214--------------------------------------------------------------------------- 1215-- * Full instantiation 1216--------------------------------------------------------------------------- 1217 1218-- | @instantiateFull'@ 'instantiate's metas everywhere (and recursively) 1219-- but does not 'reduce'. 1220class InstantiateFull t where 1221 instantiateFull' :: t -> ReduceM t 1222 1223 default instantiateFull' :: (t ~ f a, Traversable f, InstantiateFull a) => t -> ReduceM t 1224 instantiateFull' = traverse instantiateFull' 1225 1226-- Traversables (doesn't include binders like Abs, Tele): 1227 1228instance InstantiateFull t => InstantiateFull [t] 1229instance InstantiateFull t => InstantiateFull (HashMap k t) 1230instance InstantiateFull t => InstantiateFull (Map k t) 1231instance InstantiateFull t => InstantiateFull (Maybe t) 1232instance InstantiateFull t => InstantiateFull (Strict.Maybe t) 1233 1234instance InstantiateFull t => InstantiateFull (Arg t) 1235instance InstantiateFull t => InstantiateFull (Elim' t) 1236instance InstantiateFull t => InstantiateFull (Named name t) 1237instance InstantiateFull t => InstantiateFull (Open t) 1238instance InstantiateFull t => InstantiateFull (WithArity t) 1239instance InstantiateFull t => InstantiateFull (IPBoundary' t) 1240 1241-- Tuples: 1242 1243instance (InstantiateFull a, InstantiateFull b) => InstantiateFull (a,b) where 1244 instantiateFull' (x,y) = (,) <$> instantiateFull' x <*> instantiateFull' y 1245 1246instance (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a,b,c) where 1247 instantiateFull' (x,y,z) = 1248 do (x,(y,z)) <- instantiateFull' (x,(y,z)) 1249 return (x,y,z) 1250 1251instance (InstantiateFull a, InstantiateFull b, InstantiateFull c, InstantiateFull d) => InstantiateFull (a,b,c,d) where 1252 instantiateFull' (x,y,z,w) = 1253 do (x,(y,z,w)) <- instantiateFull' (x,(y,z,w)) 1254 return (x,y,z,w) 1255 1256-- Base types: 1257 1258instance InstantiateFull Bool where 1259 instantiateFull' = return 1260 1261instance InstantiateFull Char where 1262 instantiateFull' = return 1263 1264instance InstantiateFull Int where 1265 instantiateFull' = return 1266 1267instance InstantiateFull ModuleName where 1268 instantiateFull' = return 1269 1270instance InstantiateFull Name where 1271 instantiateFull' = return 1272 1273instance InstantiateFull QName where 1274 instantiateFull' = return 1275 1276instance InstantiateFull Scope where 1277 instantiateFull' = return 1278 1279instance InstantiateFull ConHead where 1280 instantiateFull' = return 1281 1282instance InstantiateFull DBPatVar where 1283 instantiateFull' = return 1284 1285-- Rest: 1286 1287instance InstantiateFull Sort where 1288 instantiateFull' s = do 1289 s <- instantiate' s 1290 case s of 1291 Type n -> Type <$> instantiateFull' n 1292 Prop n -> Prop <$> instantiateFull' n 1293 SSet n -> SSet <$> instantiateFull' n 1294 PiSort a s1 s2 -> piSort <$> instantiateFull' a <*> instantiateFull' s1 <*> instantiateFull' s2 1295 FunSort s1 s2 -> funSort <$> instantiateFull' s1 <*> instantiateFull' s2 1296 UnivSort s -> univSort <$> instantiateFull' s 1297 Inf _ _ -> return s 1298 SizeUniv -> return s 1299 LockUniv -> return s 1300 MetaS x es -> MetaS x <$> instantiateFull' es 1301 DefS d es -> DefS d <$> instantiateFull' es 1302 DummyS{} -> return s 1303 1304instance InstantiateFull t => InstantiateFull (Type' t) where 1305 instantiateFull' (El s t) = 1306 El <$> instantiateFull' s <*> instantiateFull' t 1307 1308instance InstantiateFull Term where 1309 instantiateFull' = instantiate' >=> recurse >=> etaOnce 1310 -- Andreas, 2010-11-12 DONT ETA!? eta-reduction breaks subject reduction 1311 -- but removing etaOnce now breaks everything 1312 where 1313 recurse = \case 1314 Var n vs -> Var n <$> instantiateFull' vs 1315 Con c ci vs -> Con c ci <$> instantiateFull' vs 1316 Def f vs -> Def f <$> instantiateFull' vs 1317 MetaV x vs -> MetaV x <$> instantiateFull' vs 1318 v@Lit{} -> return v 1319 Level l -> levelTm <$> instantiateFull' l 1320 Lam h b -> Lam h <$> instantiateFull' b 1321 Sort s -> Sort <$> instantiateFull' s 1322 Pi a b -> uncurry Pi <$> instantiateFull' (a,b) 1323 DontCare v -> dontCare <$> instantiateFull' v 1324 v@Dummy{} -> return v 1325 1326instance InstantiateFull Level where 1327 instantiateFull' (Max m as) = levelMax m <$> instantiateFull' as 1328 1329instance InstantiateFull PlusLevel where 1330 instantiateFull' (Plus n l) = Plus n <$> instantiateFull' l 1331 1332instance InstantiateFull Substitution where 1333 instantiateFull' sigma = 1334 case sigma of 1335 IdS -> return IdS 1336 EmptyS err -> return $ EmptyS err 1337 Wk n sigma -> Wk n <$> instantiateFull' sigma 1338 Lift n sigma -> Lift n <$> instantiateFull' sigma 1339 Strengthen bot sigma -> Strengthen bot <$> instantiateFull' sigma 1340 t :# sigma -> consS <$> instantiateFull' t 1341 <*> instantiateFull' sigma 1342 1343instance InstantiateFull ConPatternInfo where 1344 instantiateFull' i = instantiateFull' (conPType i) <&> \ t -> i { conPType = t } 1345 1346instance InstantiateFull a => InstantiateFull (Pattern' a) where 1347 instantiateFull' (VarP o x) = VarP o <$> instantiateFull' x 1348 instantiateFull' (DotP o t) = DotP o <$> instantiateFull' t 1349 instantiateFull' (ConP n mt ps) = ConP n <$> instantiateFull' mt <*> instantiateFull' ps 1350 instantiateFull' (DefP o q ps) = DefP o q <$> instantiateFull' ps 1351 instantiateFull' l@LitP{} = return l 1352 instantiateFull' p@ProjP{} = return p 1353 instantiateFull' (IApplyP o t u x) = IApplyP o <$> instantiateFull' t <*> instantiateFull' u <*> instantiateFull' x 1354 1355instance (Subst a, InstantiateFull a) => InstantiateFull (Abs a) where 1356 instantiateFull' a@(Abs x _) = Abs x <$> underAbstraction_ a instantiateFull' 1357 instantiateFull' (NoAbs x a) = NoAbs x <$> instantiateFull' a 1358 1359instance (InstantiateFull t, InstantiateFull e) => InstantiateFull (Dom' t e) where 1360 instantiateFull' (Dom i fin n tac x) = Dom i fin n <$> instantiateFull' tac <*> instantiateFull' x 1361 1362instance InstantiateFull a => InstantiateFull (Closure a) where 1363 instantiateFull' cl = do 1364 x <- enterClosure cl instantiateFull' 1365 return $ cl { clValue = x } 1366 1367instance InstantiateFull ProblemConstraint where 1368 instantiateFull' (PConstr p u c) = PConstr p u <$> instantiateFull' c 1369 1370instance InstantiateFull Constraint where 1371 instantiateFull' = \case 1372 ValueCmp cmp t u v -> do 1373 (t,u,v) <- instantiateFull' (t,u,v) 1374 return $ ValueCmp cmp t u v 1375 ValueCmpOnFace cmp p t u v -> do 1376 ((p,t),u,v) <- instantiateFull' ((p,t),u,v) 1377 return $ ValueCmpOnFace cmp p t u v 1378 ElimCmp cmp fs t v as bs -> 1379 ElimCmp cmp fs <$> instantiateFull' t <*> instantiateFull' v <*> instantiateFull' as <*> instantiateFull' bs 1380 LevelCmp cmp u v -> uncurry (LevelCmp cmp) <$> instantiateFull' (u,v) 1381 SortCmp cmp a b -> uncurry (SortCmp cmp) <$> instantiateFull' (a,b) 1382 UnBlock m -> return $ UnBlock m 1383 FindInstance m cs -> FindInstance m <$> mapM instantiateFull' cs 1384 IsEmpty r t -> IsEmpty r <$> instantiateFull' t 1385 CheckSizeLtSat t -> CheckSizeLtSat <$> instantiateFull' t 1386 c@CheckFunDef{} -> return c 1387 HasBiggerSort a -> HasBiggerSort <$> instantiateFull' a 1388 HasPTSRule a b -> uncurry HasPTSRule <$> instantiateFull' (a,b) 1389 UnquoteTactic t g h -> UnquoteTactic <$> instantiateFull' t <*> instantiateFull' g <*> instantiateFull' h 1390 CheckLockedVars a b c d -> 1391 CheckLockedVars <$> instantiateFull' a <*> instantiateFull' b <*> instantiateFull' c <*> instantiateFull' d 1392 c@CheckMetaInst{} -> return c 1393 UsableAtModality mod t -> UsableAtModality mod <$> instantiateFull' t 1394 1395instance InstantiateFull CompareAs where 1396 instantiateFull' (AsTermsOf a) = AsTermsOf <$> instantiateFull' a 1397 instantiateFull' AsSizes = return AsSizes 1398 instantiateFull' AsTypes = return AsTypes 1399 1400instance InstantiateFull Signature where 1401 instantiateFull' (Sig a b c) = uncurry3 Sig <$> instantiateFull' (a, b, c) 1402 1403instance InstantiateFull Section where 1404 instantiateFull' (Section tel) = Section <$> instantiateFull' tel 1405 1406instance (Subst a, InstantiateFull a) => InstantiateFull (Tele a) where 1407 instantiateFull' EmptyTel = return EmptyTel 1408 instantiateFull' (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull' (a, b) 1409 1410instance InstantiateFull Definition where 1411 instantiateFull' def@Defn{ defType = t ,defDisplay = df, theDef = d } = do 1412 (t, df, d) <- instantiateFull' (t, df, d) 1413 return $ def{ defType = t, defDisplay = df, theDef = d } 1414 1415instance InstantiateFull NLPat where 1416 instantiateFull' (PVar x y) = return $ PVar x y 1417 instantiateFull' (PDef x y) = PDef <$> instantiateFull' x <*> instantiateFull' y 1418 instantiateFull' (PLam x y) = PLam x <$> instantiateFull' y 1419 instantiateFull' (PPi x y) = PPi <$> instantiateFull' x <*> instantiateFull' y 1420 instantiateFull' (PSort x) = PSort <$> instantiateFull' x 1421 instantiateFull' (PBoundVar x y) = PBoundVar x <$> instantiateFull' y 1422 instantiateFull' (PTerm x) = PTerm <$> instantiateFull' x 1423 1424instance InstantiateFull NLPType where 1425 instantiateFull' (NLPType s a) = NLPType 1426 <$> instantiateFull' s 1427 <*> instantiateFull' a 1428 1429instance InstantiateFull NLPSort where 1430 instantiateFull' (PType x) = PType <$> instantiateFull' x 1431 instantiateFull' (PProp x) = PProp <$> instantiateFull' x 1432 instantiateFull' (PInf f n) = return $ PInf f n 1433 instantiateFull' PSizeUniv = return PSizeUniv 1434 instantiateFull' PLockUniv = return PLockUniv 1435 1436instance InstantiateFull RewriteRule where 1437 instantiateFull' (RewriteRule q gamma f ps rhs t c) = 1438 RewriteRule q 1439 <$> instantiateFull' gamma 1440 <*> pure f 1441 <*> instantiateFull' ps 1442 <*> instantiateFull' rhs 1443 <*> instantiateFull' t 1444 <*> pure c 1445 1446instance InstantiateFull DisplayForm where 1447 instantiateFull' (Display n ps v) = uncurry (Display n) <$> instantiateFull' (ps, v) 1448 1449instance InstantiateFull DisplayTerm where 1450 instantiateFull' (DTerm v) = DTerm <$> instantiateFull' v 1451 instantiateFull' (DDot v) = DDot <$> instantiateFull' v 1452 instantiateFull' (DCon c ci vs) = DCon c ci <$> instantiateFull' vs 1453 instantiateFull' (DDef c es) = DDef c <$> instantiateFull' es 1454 instantiateFull' (DWithApp v vs ws) = uncurry3 DWithApp <$> instantiateFull' (v, vs, ws) 1455 1456instance InstantiateFull Defn where 1457 instantiateFull' d = case d of 1458 Axiom{} -> return d 1459 DataOrRecSig{} -> return d 1460 GeneralizableVar{} -> return d 1461 AbstractDefn d -> AbstractDefn <$> instantiateFull' d 1462 Function{ funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv, funExtLam = extLam } -> do 1463 (cs, cc, cov, inv) <- instantiateFull' (cs, cc, cov, inv) 1464 extLam <- instantiateFull' extLam 1465 return $ d { funClauses = cs, funCompiled = cc, funCovering = cov, funInv = inv, funExtLam = extLam } 1466 Datatype{ dataSort = s, dataClause = cl } -> do 1467 s <- instantiateFull' s 1468 cl <- instantiateFull' cl 1469 return $ d { dataSort = s, dataClause = cl } 1470 Record{ recClause = cl, recTel = tel } -> do 1471 cl <- instantiateFull' cl 1472 tel <- instantiateFull' tel 1473 return $ d { recClause = cl, recTel = tel } 1474 Constructor{} -> return d 1475 Primitive{ primClauses = cs } -> do 1476 cs <- instantiateFull' cs 1477 return $ d { primClauses = cs } 1478 PrimitiveSort{} -> return d 1479 1480instance InstantiateFull ExtLamInfo where 1481 instantiateFull' e@(ExtLamInfo { extLamSys = sys}) = do 1482 sys <- instantiateFull' sys 1483 return $ e { extLamSys = sys} 1484 1485instance InstantiateFull System where 1486 instantiateFull' (System tel sys) = System <$> instantiateFull' tel <*> instantiateFull' sys 1487 1488instance InstantiateFull FunctionInverse where 1489 instantiateFull' NotInjective = return NotInjective 1490 instantiateFull' (Inverse inv) = Inverse <$> instantiateFull' inv 1491 1492instance InstantiateFull a => InstantiateFull (Case a) where 1493 instantiateFull' (Branches cop cs eta ls m b lz) = 1494 Branches cop 1495 <$> instantiateFull' cs 1496 <*> instantiateFull' eta 1497 <*> instantiateFull' ls 1498 <*> instantiateFull' m 1499 <*> pure b 1500 <*> pure lz 1501 1502instance InstantiateFull CompiledClauses where 1503 instantiateFull' (Fail xs) = return $ Fail xs 1504 instantiateFull' (Done m t) = Done m <$> instantiateFull' t 1505 instantiateFull' (Case n bs) = Case n <$> instantiateFull' bs 1506 1507instance InstantiateFull Clause where 1508 instantiateFull' (Clause rl rf tel ps b t catchall exact recursive unreachable ell) = 1509 Clause rl rf <$> instantiateFull' tel 1510 <*> instantiateFull' ps 1511 <*> instantiateFull' b 1512 <*> instantiateFull' t 1513 <*> return catchall 1514 <*> return exact 1515 <*> return recursive 1516 <*> return unreachable 1517 <*> return ell 1518 1519instance InstantiateFull Interface where 1520 instantiateFull' (Interface h s ft ms mod scope inside 1521 sig display userwarn importwarn b foreignCode 1522 highlighting libPragmas filePragmas usedOpts patsyns 1523 warnings partialdefs) = 1524 Interface h s ft ms mod scope inside 1525 <$> instantiateFull' sig 1526 <*> instantiateFull' display 1527 <*> return userwarn 1528 <*> return importwarn 1529 <*> instantiateFull' b 1530 <*> return foreignCode 1531 <*> return highlighting 1532 <*> return libPragmas 1533 <*> return filePragmas 1534 <*> return usedOpts 1535 <*> return patsyns 1536 <*> return warnings 1537 <*> return partialdefs 1538 1539instance InstantiateFull a => InstantiateFull (Builtin a) where 1540 instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t 1541 instantiateFull' (Prim x) = Prim <$> instantiateFull' x 1542 1543instance InstantiateFull Candidate where 1544 instantiateFull' (Candidate q u t ov) = 1545 Candidate q <$> instantiateFull' u <*> instantiateFull' t <*> pure ov 1546 1547instance InstantiateFull EqualityView where 1548 instantiateFull' (OtherType t) = OtherType 1549 <$> instantiateFull' t 1550 instantiateFull' (IdiomType t) = IdiomType 1551 <$> instantiateFull' t 1552 instantiateFull' (EqualityType s eq l t a b) = EqualityType 1553 <$> instantiateFull' s 1554 <*> return eq 1555 <*> mapM instantiateFull' l 1556 <*> instantiateFull' t 1557 <*> instantiateFull' a 1558 <*> instantiateFull' b 1559