1
{-# OPTIONS_GHC -Wunused-imports #-}
2
3
{-# LANGUAGE ViewPatterns #-}
4
5
module Agda.TypeChecking.Telescope where
6
7
import Prelude hiding (null)
8
9
import Control.Monad
10
11
import Data.Bifunctor (first)
12
import Data.Foldable (find)
13
import Data.IntSet (IntSet)
14
import qualified Data.IntSet as IntSet
15
import qualified Data.List as List
16
import Data.Maybe
17
import Data.Monoid
18
19
import Agda.Syntax.Common
20
import Agda.Syntax.Common.Pretty (prettyShow)
21
import Agda.Syntax.Internal
22
import Agda.Syntax.Internal.Pattern
23
24
import Agda.TypeChecking.Monad.Builtin
25
import Agda.TypeChecking.Monad
26
import Agda.TypeChecking.Reduce
27
import Agda.TypeChecking.Substitute
28
import Agda.TypeChecking.Free
29
30
import Agda.Utils.CallStack ( withCallerCallStack )
31
import Agda.Utils.Either
32
import Agda.Utils.Empty
33
import Agda.Utils.Functor
34
import Agda.Utils.List
35
import Agda.Utils.Null
36
import Agda.Utils.Permutation
37
import Agda.Utils.Singleton
38
import Agda.Utils.Size
39
import Agda.Utils.Tuple
40
import Agda.Utils.VarSet (VarSet)
41
import qualified Agda.Utils.VarSet as VarSet
42
43
import Agda.Utils.Impossible
44
45
-- | Flatten telescope: @(Γ : Tel) -> [Type Γ]@
46
flattenTel :: TermSubst a => Tele (Dom a) -> [Dom a]
47
flattenTel EmptyTel          = []
48
flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
49
50
{-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}
51
52
-- | Turn a context into a flat telescope: all entries live in the whole context.
53
-- @
54
--    (Γ : Context) -> [Type Γ]
55
-- @
56
flattenContext :: Context -> [ContextEntry]
57
flattenContext = loop 1 []
58
  where
59
    loop n tel []       = tel
60
    loop n tel (ce:ctx) = loop (n + 1) (raise n ce : tel) ctx
61
62
-- | Order a flattened telescope in the correct dependeny order: Γ ->
63
--   Permutation (Γ -> Γ~)
64
--
65
--   Since @reorderTel tel@ uses free variable analysis of type in @tel@,
66
--   the telescope should be 'normalise'd.
67
reorderTel :: [Dom Type] -> Maybe Permutation
68
reorderTel tel = topoSort comesBefore tel'
69
  where
70
    tel' = zip (downFrom $ size tel) tel
71
    (i, _) `comesBefore` (_, a) = i `freeIn` unEl (unDom a) -- a tiny bit unsafe
72
73
reorderTel_ :: [Dom Type] -> Permutation
74
reorderTel_ tel = fromMaybe __IMPOSSIBLE__ (reorderTel tel)
75
76
-- | Unflatten: turns a flattened telescope into a proper telescope. Must be
77
--   properly ordered.
78
unflattenTel :: [ArgName] -> [Dom Type] -> Telescope
79
unflattenTel xs tel = unflattenTel' (size tel) xs tel
80
81
-- | A variant of 'unflattenTel' which takes the size of the last
82
-- argument as an argument.
83
unflattenTel' :: Int -> [ArgName] -> [Dom Type] -> Telescope
84
unflattenTel' !n xs tel = case (xs, tel) of
85
  ([],     [])      -> EmptyTel
86
  (x : xs, a : tel) -> ExtendTel a' (Abs x tel')
87
    where
88
    tel' = unflattenTel' (n - 1) xs tel
89
    a'   = applySubst rho a
90
    rho  = parallelS $
91
           replicate n (withCallerCallStack impossibleTerm)
92
  ([],    _ : _) -> __IMPOSSIBLE__
93
  (_ : _, [])    -> __IMPOSSIBLE__
94
95
-- | Rename the variables in the telescope to the given names
96
--   Precondition: @size xs == size tel@.
97
renameTel :: [Maybe ArgName] -> Telescope -> Telescope
98
renameTel []           EmptyTel           = EmptyTel
99
renameTel (Nothing:xs) (ExtendTel a tel') = ExtendTel a $ renameTel xs <$> tel'
100
renameTel (Just x :xs) (ExtendTel a tel') = ExtendTel a $ renameTel xs <$> (tel' { absName = x })
101
renameTel []           (ExtendTel _ _   ) = __IMPOSSIBLE__
102
renameTel (_      :_ ) EmptyTel           = __IMPOSSIBLE__
103
104
-- | Get the suggested names from a telescope
105
teleNames :: Telescope -> [ArgName]
106
teleNames = map (fst . unDom) . telToList
107
108
teleArgNames :: Telescope -> [Arg ArgName]
109
teleArgNames = map (argFromDom . fmap fst) . telToList
110
111
teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
112
teleArgs = map argFromDom . teleDoms
113
114
teleDoms :: (DeBruijn a) => Tele (Dom t) -> [Dom a]
115
teleDoms tel = zipWith (\ i dom -> deBruijnVar i <$ dom) (downFrom $ size l) l
116
  where l = telToList tel
117
118
-- UNUSED
119
-- withNamedArgsFromTel :: [a] -> Telescope -> [NamedArg a]
120
-- xs `withNamedArgsFromTel` tel =
121
--   [ Arg info (Named (Just $ Ranged empty $ argNameToString name) x)
122
--   | (x, Dom {domInfo = info, unDom = (name,_)}) <- zip xs l ]
123
--   where l = telToList tel
124
125
teleNamedArgs :: (DeBruijn a) => Tele (Dom t) -> [NamedArg a]
126
teleNamedArgs = map namedArgFromDom . teleDoms
127
128
{-# INLINABLE tele2NamedArgs #-}
129
-- | A variant of `teleNamedArgs` which takes the argument names (and the argument info)
130
--   from the first telescope and the variable names from the second telescope.
131
--
132
--   Precondition: the two telescopes have the same length.
133
tele2NamedArgs :: (DeBruijn a) => Telescope -> Telescope -> [NamedArg a]
134
tele2NamedArgs tel0 tel =
135
  [ Arg info (Named (Just $ WithOrigin Inserted $ unranged $ argNameToString argName) (debruijnNamedVar varName i))
136
  | (i, Dom{domInfo = info, unDom = (argName,_)}, Dom{unDom = (varName,_)}) <- zip3 (downFrom $ size l) l0 l ]
137
  where
138
  l  = telToList tel
139
  l0 = telToList tel0
140
141
-- | Split the telescope at the specified position.
142
splitTelescopeAt :: Int -> Telescope -> (Telescope,Telescope)
143
splitTelescopeAt n tel
144
  | n <= 0    = (EmptyTel, tel)
145
  | otherwise = splitTelescopeAt' n tel
146
    where
147
      splitTelescopeAt' _ EmptyTel          = (EmptyTel,EmptyTel)
148
      splitTelescopeAt' 1 (ExtendTel a tel) = (ExtendTel a (tel $> EmptyTel), absBody tel)
149
      splitTelescopeAt' m (ExtendTel a tel) = (ExtendTel a (tel $> tel'), tel'')
150
        where
151
          (tel', tel'') = splitTelescopeAt (m - 1) $ absBody tel
152
153
-- | Permute telescope: permutes or drops the types in the telescope according
154
--   to the given permutation. Assumes that the permutation preserves the
155
--   dependencies in the telescope.
156
--
157
--   For example (Andreas, 2016-12-18, issue #2344):
158
--   @
159
--     tel                     = (A : Set) (X : _18 A) (i : Fin (_m_23 A X))
160
--     tel (de Bruijn)         = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0)
161
--     flattenTel tel          = 2:Set, 1:_18 @0, 0:Fin(_m_23 @1 @0) |- [ Set, _18 @2, Fin (_m_23 @2 @1) ]
162
--     perm                    = 0,1,2 -> 0,1  (picks the first two)
163
--     renaming _ perm         = [var 0, var 1, error]  -- THE WRONG RENAMING!
164
--     renaming _ (flipP perm) = [error, var 1, var 0]  -- The correct renaming!
165
--     apply to flattened tel  = ... |- [ Set, _18 @1, Fin (_m_23 @1 @0) ]
166
--     permute perm it         = ... |- [ Set, _18 @1 ]
167
--     unflatten (de Bruijn)   = 1:Set, 0: _18 @0
168
--     unflatten               = (A : Set) (X : _18 A)
169
--  @
170
permuteTel :: Permutation -> Telescope -> Telescope
171
permuteTel perm tel =
172
  let names = permute perm $ teleNames tel
173
      types = permute perm $ renameP impossible (flipP perm) $ flattenTel tel
174
  in  unflattenTel names types
175
176
-- | Like 'permuteTel', but start with a context.
177
--
178
permuteContext :: Permutation -> Context -> Telescope
179
permuteContext perm ctx = unflattenTel names types
180
  where
181
    flatTel = flattenContext ctx
182
    names   = permute perm $ map (prettyShow . fst . unDom) flatTel
183
    types   = permute perm $ renameP impossible (flipP perm) $ map (fmap snd) flatTel
184
185
-- | Recursively computes dependencies of a set of variables in a given
186
--   telescope. Any dependencies outside of the telescope are ignored.
187
varDependencies :: Telescope -> IntSet -> IntSet
188
varDependencies tel = addLocks . allDependencies IntSet.empty
189
  where
190
    addLocks s | IntSet.null s = s
191
               | otherwise = IntSet.union s $ IntSet.fromList $ filter (>= m) locks
192
      where
193
        locks = catMaybes [ deBruijnView (unArg a) | (a :: Arg Term) <- teleArgs tel, IsLock{} <- pure (getLock a)]
194
        m = IntSet.findMin s
195
    n  = size tel
196
    ts = flattenTel tel
197
198
    directDependencies :: Int -> IntSet
199
    directDependencies i = allFreeVars $ indexWithDefault __IMPOSSIBLE__ ts (n-1-i)
200
201
    allDependencies :: IntSet -> IntSet -> IntSet
202
    allDependencies =
203
      IntSet.foldr $ \j soFar ->
204
        if j >= n || j `IntSet.member` soFar
205
        then soFar
206
        else IntSet.insert j $ allDependencies soFar $ directDependencies j
207
208
-- | Computes the set of variables in a telescope whose type depend on
209
--   one of the variables in the given set (including recursive
210
--   dependencies). Any dependencies outside of the telescope are
211
--   ignored.
212
varDependents :: Telescope -> IntSet -> IntSet
213
varDependents tel = allDependents
214
  where
215
    n  = size tel
216
    ts = flattenTel tel
217
218
    directDependents :: IntSet -> IntSet
219
    directDependents is = IntSet.fromList
220
      [ j | j <- downFrom n
221
          , let tj = indexWithDefault __IMPOSSIBLE__ ts (n-1-j)
222
          , getAny $ runFree (Any . (`IntSet.member` is)) IgnoreNot tj
223
          ]
224
225
    allDependents :: IntSet -> IntSet
226
    allDependents is
227
     | null new  = empty
228
     | otherwise = new `IntSet.union` allDependents new
229
      where new = directDependents is
230
231
-- | A telescope split in two.
232
data SplitTel = SplitTel
233
  { firstPart  :: Telescope
234
  , secondPart :: Telescope
235
  , splitPerm  :: Permutation
236
    -- ^ The permutation takes us from the original telescope to
237
    --   @firstPart ++ secondPart@.
238
  }
239
240
-- | Split a telescope into the part that defines the given variables and the
241
--   part that doesn't.
242
--
243
--   See 'Agda.TypeChecking.Tests.prop_splitTelescope'.
244
splitTelescope
245
  :: VarSet     -- ^ A set of de Bruijn indices.
246
  -> Telescope  -- ^ Original telescope.
247
  -> SplitTel   -- ^ @firstPart@ mentions the given variables, @secondPart@ not.
248
splitTelescope fv tel = SplitTel tel1 tel2 perm
249
  where
250
    names = teleNames tel
251
    ts0   = flattenTel tel
252
    n     = size tel
253
254
    is    = varDependencies tel fv
255
    isC   = IntSet.fromList [0..(n-1)] `IntSet.difference` is
256
257
    perm  = Perm n $ map (n-1-) $ VarSet.toDescList is ++ VarSet.toDescList isC
258
259
    ts1   = renameP impossible (reverseP perm) (permute perm ts0)
260
261
    tel'  = unflattenTel (permute perm names) ts1
262
263
    m     = size is
264
    (tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
265
266
-- | As splitTelescope, but fails if any additional variables or reordering
267
--   would be needed to make the first part well-typed.
268
splitTelescopeExact
269
  :: [Int]          -- ^ A list of de Bruijn indices
270
  -> Telescope      -- ^ The telescope to split
271
  -> Maybe SplitTel -- ^ @firstPart@ mentions the given variables in the given order,
272
                    --   @secondPart@ contains all other variables
273
splitTelescopeExact is tel = guard ok $> SplitTel tel1 tel2 perm
274
  where
275
    names = teleNames tel
276
    ts0   = flattenTel tel
277
    n     = size tel
278
279
    checkDependencies :: IntSet -> [Int] -> Bool
280
    checkDependencies soFar []     = True
281
    checkDependencies soFar (j:js) = ok && checkDependencies (IntSet.insert j soFar) js
282
      where
283
        t   = indexWithDefault __IMPOSSIBLE__ ts0 (n-1-j)  -- ts0[n-1-j]
284
        -- Skip the construction of intermediate @IntSet@s in the check @ok@.
285
        -- ok  = (allFreeVars t `IntSet.intersection` IntSet.fromAscList [ 0 .. n-1 ])
286
        --       `IntSet.isSubsetOf` soFar
287
        good i = All $ (i < n) `implies` (i `IntSet.member` soFar) where implies = (<=)
288
        ok = getAll $ runFree good IgnoreNot t
289
290
    ok    = all (< n) is && checkDependencies IntSet.empty is
291
292
    isC   = downFrom n List.\\ is
293
294
    perm  = Perm n $ map (n-1-) $ is ++ isC
295
296
    ts1   = renameP impossible (reverseP perm) (permute perm ts0)
297
298
    tel'  = unflattenTel (permute perm names) ts1
299
300
    m     = size is
301
    (tel1, tel2) = telFromList -*- telFromList $ splitAt m $ telToList tel'
302
303
-- | Try to instantiate one variable in the telescope (given by its de Bruijn
304
--   level) with the given value, returning the new telescope and a
305
--   substitution to the old one. Returns Nothing if the given value depends
306
--   (directly or indirectly) on the variable.
307
instantiateTelescope
308
  :: Telescope -- ^ ⊢ Γ
309
  -> Int       -- ^ Γ ⊢ var k : A   de Bruijn _level_
310
  -> DeBruijnPattern -- ^ Γ ⊢ u : A
311
  -> Maybe (Telescope,           -- ⊢ Γ'
312
            PatternSubstitution, -- Γ' ⊢ σ : Γ
313
            Permutation)         -- Γ  ⊢ flipP ρ : Γ'
314
instantiateTelescope tel k p = guard ok $> (tel', sigma, rho)
315
  where
316
    names = teleNames tel
317
    ts0   = flattenTel tel
318
    n     = size tel
319
    j     = n-1-k
320
    u     = patternToTerm p
321
322
    -- Jesper, 2019-12-31: Previous implementation that does some
323
    -- unneccessary reordering but is otherwise correct (keep!)
324
    -- -- is0 is the part of Γ that is needed to type u
325
    -- is0   = varDependencies tel $ allFreeVars u
326
    -- -- is1 is the rest of Γ (minus the variable we are instantiating)
327
    -- is1   = IntSet.delete j $
328
    --           IntSet.fromAscList [ 0 .. n-1 ] `IntSet.difference` is0
329
    -- -- we work on de Bruijn indices, so later parts come first
330
    -- is    = IntSet.toAscList is1 ++ IntSet.toAscList is0
331
332
    -- -- if u depends on var j, we cannot instantiate
333
    -- ok    = not $ j `IntSet.member` is0
334
335
    -- is0 is the part of Γ that is needed to type u
336
    is0   = varDependencies tel $ allFreeVars u
337
    -- is1 is the part of Γ that depends on variable j
338
    is1   = varDependents tel $ singleton j
339
    -- lasti is the last (rightmost) variable of is0
340
    lasti = if null is0 then n else IntSet.findMin is0
341
    -- we move each variable in is1 to the right until it comes after
342
    -- all variables in is0 (i.e. after lasti)
343
    (as,bs) = List.partition (`IntSet.member` is1) [ n-1 , n-2 .. lasti ]
344
    is    = reverse $ List.delete j $ bs ++ as ++ downFrom lasti
345
346
    -- if u depends on var j, we cannot instantiate
347
    ok    = not $ j `IntSet.member` is0
348
349
    perm  = Perm n $ is    -- works on de Bruijn indices
350
    rho   = reverseP perm  -- works on de Bruijn levels
351
352
    p1    = renameP impossible perm p -- Γ' ⊢ p1 : A'
353
    us    = map (\i -> maybe p1 deBruijnVar (List.elemIndex i is)) [ 0 .. n-1 ]
354
    sigma = us ++# raiseS (n-1)
355
356
    ts1   = permute rho $ applyPatSubst sigma ts0
357
    tel'  = unflattenTel (permute rho names) ts1
358
359
-- | Try to eta-expand one variable in the telescope (given by its de Bruijn
360
--   level)
361
expandTelescopeVar
362
  :: Telescope  -- Γ = Γ₁(x : D pars)Γ₂
363
  -> Int        -- k = size Γ₁
364
  -> Telescope  -- Γ₁ ⊢ Δ
365
  -> ConHead    -- Γ₁ ⊢ c : Δ → D pars
366
  -> ( Telescope            -- Γ' = Γ₁ΔΓ₂[x ↦ c Δ]
367
     , PatternSubstitution) -- Γ' ⊢ ρ : Γ
368
expandTelescopeVar gamma k delta c = (tel', rho)
369
  where
370
    (ts1,xa:ts2) = fromMaybe __IMPOSSIBLE__ $
371
                    splitExactlyAt k $ telToList gamma
372
    a = raise (size delta) (snd <$> xa) -- Γ₁Δ ⊢ D pars
373
374
    cpi         = ConPatternInfo
375
      { conPInfo   = defaultPatternInfo
376
      , conPRecord = True
377
      , conPFallThrough
378
                   = False
379
      , conPType   = Just $ argFromDom a
380
      , conPLazy   = True
381
      }
382
    cargs       = map (setOrigin Inserted) $ teleNamedArgs delta
383
    cdelta      = ConP c cpi cargs                    -- Γ₁Δ ⊢ c Δ : D pars
384
    rho0        = consS cdelta $ raiseS (size delta)  -- Γ₁Δ ⊢ ρ₀ : Γ₁(x : D pars)
385
    rho         = liftS (size ts2) rho0               -- Γ₁ΔΓ₂ρ₀ ⊢ ρ : Γ₁(x : D pars)Γ₂
386
387
    gamma1      = telFromList ts1
388
    gamma2'     = applyPatSubst rho0 $ telFromList ts2
389
390
    tel'        = gamma1 `abstract` (delta `abstract` gamma2')
391
392
393
{-# INLINE telView #-}
394
-- | Gather leading Πs of a type in a telescope.
395
telView :: (MonadReduce m, MonadAddContext m) => Type -> m TelView
396
telView = telViewUpTo (-1)
397
398
{-# INLINE telViewUpTo #-}
399
-- | @telViewUpTo n t@ takes off the first @n@ function types of @t@.
400
-- Takes off all if @n < 0@.
401
telViewUpTo :: (MonadReduce m, MonadAddContext m) => Int -> Type -> m TelView
402
telViewUpTo n t = telViewUpTo' n (const True) t
403
404
{-# SPECIALIZE telViewUpTo' :: Int -> (Dom Type -> Bool) -> Type -> TCM TelView #-}
405
-- | @telViewUpTo' n p t@ takes off $t$
406
--   the first @n@ (or arbitrary many if @n < 0@) function domains
407
--   as long as they satify @p@.
408
telViewUpTo' :: (MonadReduce m, MonadAddContext m) => Int -> (Dom Type -> Bool) -> Type -> m TelView
409
telViewUpTo' 0 p t = return $ TelV EmptyTel t
410
telViewUpTo' n p t = do
411
  t <- reduce t
412
  case unEl t of
413
    Pi a b | p a ->
414
          -- Force the name to avoid retaining the rest of b.
415
      let !bn = absName b in
416
      absV a bn <$> do
417
        underAbstractionAbs a b $ \b -> telViewUpTo' (n - 1) p b
418
    _ -> return $ TelV EmptyTel t
419
420
{-# INLINE telViewPath #-}
421
telViewPath :: PureTCM m => Type -> m TelView
422
telViewPath = telViewUpToPath (-1)
423
424
{-# SPECIALIZE telViewUpToPath :: Int -> Type -> TCM TelView #-}
425
-- | @telViewUpToPath n t@ takes off $t$
426
--   the first @n@ (or arbitrary many if @n < 0@) function domains or Path types.
427
--
428
-- @telViewUpToPath n t = fst <$> telViewUpToPathBoundary'n t@
429
telViewUpToPath :: PureTCM m => Int -> Type -> m TelView
430
telViewUpToPath n t = if n == 0 then done t else do
431
  pathViewAsPi t >>= \case
432
    Left  (a, b)          -> recurse a b
433
    Right (El _ (Pi a b)) -> recurse a b
434
    Right t               -> done t
435
  where
436
    done t      = return $ TelV EmptyTel t
437
    recurse a b = absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
438
439
-- | [[ (i,(x,y)) ]] = [(i=0) -> x, (i=1) -> y]
440
type Boundary = Boundary' (Term,Term)
441
type Boundary' a = [(Term,a)]
442
443
444
{-# SPECIALIZE telViewUpToPathBoundary' :: Int -> Type -> TCM (TelView, Boundary) #-}
445
-- | Like @telViewUpToPath@ but also returns the @Boundary@ expected
446
-- by the Path types encountered. The boundary terms live in the
447
-- telescope given by the @TelView@.
448
-- Each point of the boundary has the type of the codomain of the Path type it got taken from, see @fullBoundary@.
449
telViewUpToPathBoundary' :: PureTCM m => Int -> Type -> m (TelView, Boundary)
450
telViewUpToPathBoundary' n t = if n == 0 then done t else do
451
  pathViewAsPi' t >>= \case
452
    Left ((a, b), xy)     -> addEndPoints xy <$> recurse a b
453
    Right (El _ (Pi a b)) -> recurse a b
454
    Right t               -> done t
455
  where
456
    done t      = return (TelV EmptyTel t, [])
457
    recurse a b = first (absV a (absName b)) <$> do
458
      underAbstractionAbs a b $ \b -> telViewUpToPathBoundary' (n - 1) b
459
    addEndPoints xy (telv@(TelV tel _), cs) =
460
      (telv, (var $ size tel - 1, raise (size tel) xy) : cs)
461
462
463
fullBoundary :: Telescope -> Boundary -> Boundary
464
fullBoundary tel bs =
465
      -- tel = Γ
466
      -- ΔΓ ⊢ b
467
      -- Δ ⊢ a = PiPath Γ bs b
468
      -- Δ.Γ ⊢ T is the codomain of the PathP at variable i
469
      -- Δ.Γ ⊢ i : I
470
      -- Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
471
      -- Δ.Γ | PiPath Γ bs A ⊢ teleElims tel bs : b
472
   let es = teleElims tel bs
473
       l  = size tel
474
   in map (\ (t@(Var i []), xy) -> (t, xy `applyE` (drop (l - i) es))) bs
475
476
{-# SPECIALIZE telViewUpToPathBoundary :: Int -> Type -> TCM (TelView, Boundary) #-}
477
-- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundary n a@
478
--  Input:  Δ ⊢ a
479
--  Output: ΔΓ ⊢ b
480
--          ΔΓ ⊢ i : I
481
--          ΔΓ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : b
482
telViewUpToPathBoundary :: PureTCM m => Int -> Type -> m (TelView,Boundary)
483
telViewUpToPathBoundary i a = do
484
   (telv@(TelV tel b), bs) <- telViewUpToPathBoundary' i a
485
   return $ (telv, fullBoundary tel bs)
486
487
{-# INLINE telViewUpToPathBoundaryP #-}
488
-- | @(TelV Γ b, [(i,t_i,u_i)]) <- telViewUpToPathBoundaryP n a@
489
--  Input:  Δ ⊢ a
490
--  Output: Δ.Γ ⊢ b
491
--          Δ.Γ ⊢ T is the codomain of the PathP at variable i
492
--          Δ.Γ ⊢ i : I
493
--          Δ.Γ ⊢ [ (i=0) -> t_i; (i=1) -> u_i ] : T
494
-- Useful to reconstruct IApplyP patterns after teleNamedArgs Γ.
495
telViewUpToPathBoundaryP :: PureTCM m => Int -> Type -> m (TelView,Boundary)
496
telViewUpToPathBoundaryP = telViewUpToPathBoundary'
497
498
{-# INLINE telViewPathBoundaryP #-}
499
telViewPathBoundaryP :: PureTCM m => Type -> m (TelView,Boundary)
500
telViewPathBoundaryP = telViewUpToPathBoundaryP (-1)
501
502
503
-- | @teleElimsB args bs = es@
504
--  Input:  Δ.Γ ⊢ args : Γ
505
--          Δ.Γ ⊢ T is the codomain of the PathP at variable i
506
--          Δ.Γ ⊢ i : I
507
--          Δ.Γ ⊢ bs = [ (i=0) -> t_i; (i=1) -> u_i ] : T
508
--  Output: Δ.Γ | PiPath Γ bs A ⊢ es : A
509
teleElims :: DeBruijn a => Telescope -> Boundary' (a,a) -> [Elim' a]
510
teleElims tel [] = map Apply $ teleArgs tel
511
teleElims tel boundary = recurse (teleArgs tel)
512
  where
513
    recurse = fmap updateArg
514
    matchVar x =
515
      snd <$> find (\case
516
        (Var i [],_) -> i == x
517
        _            -> __IMPOSSIBLE__) boundary
518
    updateArg a@(Arg info p) =
519
      case deBruijnView p of
520
        Just i | Just (t,u) <- matchVar i -> IApply t u p
521
        _                                 -> Apply a
522
523
{-# SPECIALIZE pathViewAsPi :: Type -> TCM (Either (Dom Type, Abs Type) Type) #-}
524
-- | Reduces 'Type'.
525
pathViewAsPi
526
  :: PureTCM m => Type -> m (Either (Dom Type, Abs Type) Type)
527
pathViewAsPi t = either (Left . fst) Right <$> pathViewAsPi' t
528
529
{-# SPECIALIZE pathViewAsPi' :: Type -> TCM (Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
530
-- | Reduces 'Type'.
531
pathViewAsPi'
532
  :: PureTCM m => Type -> m (Either ((Dom Type, Abs Type), (Term,Term)) Type)
533
pathViewAsPi' t = do
534
  pathViewAsPi'whnf <*> reduce t
535
536
{-# SPECIALIZE pathViewAsPi'whnf :: TCM (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type) #-}
537
pathViewAsPi'whnf
538
  :: (HasBuiltins m)
539
  => m (Type -> Either ((Dom Type, Abs Type), (Term,Term)) Type)
540
pathViewAsPi'whnf = do
541
  view <- pathView'
542
  minterval  <- getTerm' builtinInterval
543
  return $ \case
544
    (view -> PathType s l p a x y) | Just interval <- minterval ->
545
      let name | Lam _ (Abs n _) <- unArg a = n
546
               | otherwise = "i"
547
      in
548
        Left ( ( defaultDom $ El intervalSort interval
549
               , Abs name $ El (raise 1 s) $ raise 1 (unArg a) `apply` [defaultArg $ var 0]
550
               )
551
             , (unArg x, unArg y)
552
             )
553
554
    t    -> Right t
555
556
-- | Returns @Left (a,b)@ in case the type is @Pi a b@ or @PathP b _ _@.
557
--   Assumes the 'Type' is in whnf.
558
piOrPath :: HasBuiltins m => Type -> m (Either (Dom Type, Abs Type) Type)
559
piOrPath t = do
560
  (pathViewAsPi'whnf <*> pure t) <&> \case
561
    Left (p, _)           -> Left p
562
    Right (El _ (Pi a b)) -> Left (a,b)
563
    Right _               -> Right t
564
565
-- | Assumes 'Type' is in whnf.
566
telView'UpToPath :: Int -> Type -> TCM TelView
567
telView'UpToPath n t = if n == 0 then done else do
568
  piOrPath t >>= \case
569
    Left (a, b) -> absV a (absName b) <$> telViewUpToPath (n - 1) (absBody b)
570
    Right _     -> done
571
  where
572
    done = return $ TelV EmptyTel t
573
574
telView'Path :: Type -> TCM TelView
575
telView'Path = telView'UpToPath (-1)
576
577
isPath :: PureTCM m => Type -> m (Maybe (Dom Type, Abs Type))
578
isPath t = ifPath t (\a b -> return $ Just (a,b)) (const $ return Nothing)
579
580
ifPath :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
581
ifPath t yes no = ifPathB t yes $ no . ignoreBlocking
582
583
{-# SPECIALIZE ifPathB :: Type -> (Dom Type -> Abs Type -> TCM a) -> (Blocked Type -> TCM a) -> TCM a #-}
584
ifPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
585
ifPathB t yes no = ifBlocked t
586
  (\b t -> no $ Blocked b t)
587
  (\nb t -> caseEitherM (pathViewAsPi'whnf <*> pure t)
588
    (uncurry yes . fst)
589
    (no . NotBlocked nb))
590
591
ifNotPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
592
ifNotPathB = flip . ifPathB
593
594
ifPiOrPathB :: PureTCM m => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
595
ifPiOrPathB t yes no = ifPiTypeB t
596
  (\a b -> yes a b)
597
  (\bt -> caseEitherM (pathViewAsPi'whnf <*> pure (ignoreBlocking bt))
598
    (uncurry yes . fst)
599
    (no . (bt $>)))
600
601
ifNotPiOrPathB :: PureTCM m => Type -> (Blocked Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
602
ifNotPiOrPathB = flip . ifPiOrPathB
603
604
telePatterns :: DeBruijn a => Telescope -> Boundary -> [NamedArg (Pattern' a)]
605
telePatterns = telePatterns' teleNamedArgs
606
607
telePatterns' :: DeBruijn a =>
608
                (forall a. (DeBruijn a) => Telescope -> [NamedArg a]) -> Telescope -> Boundary -> [NamedArg (Pattern' a)]
609
telePatterns' f tel [] = f tel
610
telePatterns' f tel boundary = recurse $ f tel
611
  where
612
    recurse = (fmap . fmap . fmap) updateVar
613
    matchVar x =
614
      snd <$> find (\case
615
        (Var i [],_) -> i == x
616
        _            -> __IMPOSSIBLE__) boundary
617
    updateVar x =
618
      case deBruijnView x of
619
        Just i | Just (t,u) <- matchVar i -> IApplyP defaultPatternInfo t u x
620
        _                                 -> VarP defaultPatternInfo x
621
622
-- | Decomposing a function type.
623
624
mustBePi :: MonadReduce m => Type -> m (Dom Type, Abs Type)
625
mustBePi t = ifNotPiType t __IMPOSSIBLE__ $ curry return
626
627
-- | If the given type is a @Pi@, pass its parts to the first continuation.
628
--   If not (or blocked), pass the reduced type to the second continuation.
629
ifPi :: MonadReduce m => Term -> (Dom Type -> Abs Type -> m a) -> (Term -> m a) -> m a
630
ifPi t yes no = ifPiB t yes (no . ignoreBlocking)
631
632
ifPiB :: (MonadReduce m) => Term -> (Dom Type -> Abs Type -> m a) -> (Blocked Term -> m a) -> m a
633
ifPiB t yes no = ifBlocked t
634
  (\b t -> no $ Blocked b t) -- Pi type is never blocked
635
  (\nb t -> case t of
636
    Pi a b -> yes a b
637
    _      -> no $ NotBlocked nb t)
638
639
ifPiTypeB :: (MonadReduce m) => Type -> (Dom Type -> Abs Type -> m a) -> (Blocked Type -> m a) -> m a
640
ifPiTypeB (El s t) yes no = ifPiB t yes (\bt -> no $ El s <$> bt)
641
642
-- | If the given type is a @Pi@, pass its parts to the first continuation.
643
--   If not (or blocked), pass the reduced type to the second continuation.
644
ifPiType :: MonadReduce m => Type -> (Dom Type -> Abs Type -> m a) -> (Type -> m a) -> m a
645
ifPiType (El s t) yes no = ifPi t yes (no . El s)
646
647
-- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
648
--   If it is a @Pi@, pass its parts to the second continuation.
649
ifNotPi :: MonadReduce m => Term -> (Term -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
650
ifNotPi = flip . ifPi
651
652
-- | If the given type is blocked or not a @Pi@, pass it reduced to the first continuation.
653
--   If it is a @Pi@, pass its parts to the second continuation.
654
ifNotPiType :: MonadReduce m => Type -> (Type -> m a) -> (Dom Type -> Abs Type -> m a) -> m a
655
ifNotPiType = flip . ifPiType
656
657
ifNotPiOrPathType :: (MonadReduce tcm, HasBuiltins tcm) => Type -> (Type -> tcm a) -> (Dom Type -> Abs Type -> tcm a) -> tcm a
658
ifNotPiOrPathType t no yes = do
659
  ifPiType t yes (\ t -> either (uncurry yes . fst) (const $ no t) =<< (pathViewAsPi'whnf <*> pure t))
660
661
shouldBePath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
662
shouldBePath t = ifPathB t
663
  (curry return)
664
  (fromBlocked >=> \case
665
    El _ Dummy{} -> return (__DUMMY_DOM__, Abs "x" __DUMMY_TYPE__)
666
    t -> typeError $ ShouldBePath t)
667
668
shouldBePi :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
669
shouldBePi t = ifPiTypeB t
670
  (curry return)
671
  (fromBlocked >=> \case
672
    El _ Dummy{} -> return (__DUMMY_DOM__, Abs "x" __DUMMY_TYPE__)
673
    t -> typeError $ ShouldBePi t)
674
675
shouldBePiOrPath :: (PureTCM m, MonadBlock m, MonadTCError m) => Type -> m (Dom Type, Abs Type)
676
shouldBePiOrPath t = ifPiOrPathB t
677
  (curry return)
678
  (fromBlocked >=> \case
679
    El _ Dummy{} -> return (__DUMMY_DOM__, Abs "x" __DUMMY_TYPE__)
680
    t -> typeError $ ShouldBePi t) -- TODO: separate error
681
682
-- | A safe variant of 'piApply'.
683
684
class PiApplyM a where
685
  piApplyM' :: (MonadReduce m, HasBuiltins m) => m Empty -> Type -> a -> m Type
686
687
  piApplyM :: (MonadReduce m, HasBuiltins m) => Type -> a -> m Type
688
  piApplyM = piApplyM' __IMPOSSIBLE__
689
  {-# INLINE piApplyM #-}
690
691
instance PiApplyM Term where
692
  piApplyM' err t v = ifNotPiOrPathType t (\_ -> absurd <$> err) {-else-} $ \ _ b -> return $ absApp b v
693
  {-# INLINABLE piApplyM' #-}
694
695
{-# SPECIALIZE piApplyM' :: TCM Empty -> Type -> Term -> TCM Type #-}
696
697
instance PiApplyM a => PiApplyM (Arg a) where
698
  piApplyM' err t = piApplyM' err t . unArg
699
700
instance PiApplyM a => PiApplyM (Named n a) where
701
  piApplyM' err t = piApplyM' err t . namedThing
702
703
instance PiApplyM a => PiApplyM [a] where
704
  piApplyM' err t = foldl (\ mt v -> mt >>= \t -> (piApplyM' err t v)) (return t)
705
706
707
-- | Compute type arity
708
709
typeArity :: Type -> TCM Nat
710
typeArity t = do
711
  TelV tel _ <- telView t
712
  return (size tel)
713
714
-- | Fold a telescope into a monadic computation, adding variables to the
715
-- context at each step.
716
717
foldrTelescopeM
718
  :: MonadAddContext m
719
  => (Dom (ArgName, Type) -> m b -> m b)
720
  -> m b
721
  -> Telescope
722
  -> m b
723
foldrTelescopeM f b = go
724
  where
725
    go EmptyTel = b
726
    go (ExtendTel a tel) =
727
      f ((absName tel,) <$> a) $ underAbstraction a tel go