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