1
{-# LANGUAGE CPP, PatternGuards #-}
2
2
module Agda.TypeChecking.SizedTypes where
4
4
import Control.Monad.Error
7
9
import qualified Data.Map as Map
9
11
import Agda.Interaction.Options
10
13
import Agda.Syntax.Common
11
14
import Agda.Syntax.Internal
12
16
import Agda.TypeChecking.Monad
13
17
import Agda.TypeChecking.Monad.Builtin
14
18
import Agda.TypeChecking.Pretty
15
19
import Agda.TypeChecking.Reduce
16
import Agda.TypeChecking.MetaVars
20
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
17
21
import Agda.TypeChecking.Substitute
18
22
import Agda.TypeChecking.Telescope
19
23
import {-# SOURCE #-} Agda.TypeChecking.Conversion
20
import Agda.TypeChecking.Constraints
24
import {-# SOURCE #-} Agda.TypeChecking.Constraints
21
26
import qualified Agda.Utils.Warshall as W
22
27
import Agda.Utils.List
28
import Agda.Utils.Maybe
23
29
import Agda.Utils.Monad
24
30
import Agda.Utils.Impossible
25
31
import Agda.Utils.Size
32
import Agda.Utils.Tuple
33
import Agda.Utils.Pretty (render)
27
35
#include "../undefined.h"
29
compareSizes :: Comparison -> Term -> Term -> TCM ()
30
compareSizes cmp u v = do
31
reportSDoc "tc.conv.size" 10 $ vcat
32
[ text "Comparing sizes"
33
, nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
39
reportSDoc "tc.conv.size" 15 $
40
nest 2 $ sep [ text (show u) <+> prettyTCM cmp
37
builtinSizeHook :: String -> QName -> Term -> Type -> TCM ()
38
builtinSizeHook s q e' t = do
39
when (s `elem` [builtinSizeLt, builtinSizeSuc]) $ do
40
modifySignature $ updateDefinition q
41
$ updateDefPolarity (const [Covariant])
42
. updateDefArgOccurrences (const [StrictPos])
43
when (s == builtinSizeMax) $ do
44
modifySignature $ updateDefinition q
45
$ updateDefPolarity (const [Covariant, Covariant])
46
. updateDefArgOccurrences (const [StrictPos, StrictPos])
48
. updateDefType (const tmax)
50
-- TODO: max : (i j : Size) -> Size< (suc (max i j))
54
-- | Compute the deep size view of a term.
55
-- Precondition: sized types are enabled.
56
deepSizeView :: Term -> TCM DeepSizeView
58
Def inf [] <- ignoreSharing <$> primSizeInf
59
Def suc [] <- ignoreSharing <$> primSizeSuc
62
case ignoreSharing v of
63
Def x [] | x == inf -> return $ DSizeInf
64
Def x [u] | x == suc -> sizeViewSuc_ suc <$> loop (unArg u)
65
Var i [] -> return $ DSizeVar i 0
66
MetaV x us -> return $ DSizeMeta x us 0
67
_ -> return $ DOtherSize v
70
sizeMaxView :: Term -> TCM SizeMaxView
72
inf <- getBuiltinDefName builtinSizeInf
73
suc <- getBuiltinDefName builtinSizeSuc
74
max <- getBuiltinDefName builtinSizeMax
78
Def x [] | Just x == inf -> return $ [DSizeInf]
79
Def x [u] | Just x == suc -> maxViewSuc_ (fromJust suc) <$> loop (unArg u)
80
Def x [u1,u2] | Just x == max -> maxViewMax <$> loop (unArg u1) <*> loop (unArg u2)
81
Var i [] -> return $ [DSizeVar i 0]
82
MetaV x us -> return $ [DSizeMeta x us 0]
83
_ -> return $ [DOtherSize v]
86
-- | Account for subtyping @Size< i =< Size@
88
-- @m = x els1@, @n = y els2@, @m@ and @n@ are not equal.
89
trySizeUniv :: Comparison -> Type -> Term -> Term
90
-> QName -> [Elim] -> QName -> [Elim] -> TCM ()
91
trySizeUniv cmp t m n x els1 y els2 = do
92
let failure = typeError $ UnequalTerms cmp m n t
93
forceInfty u = compareSizes CmpEq (unArg u) =<< primSizeInf
94
(size, sizelt) <- flip catchError (const failure) $ do
95
Def size _ <- ignoreSharing <$> primSize
96
Def sizelt _ <- ignoreSharing <$> primSizeLt
98
case (cmp, els1, els2) of
99
(CmpLeq, [_], []) | x == sizelt && y == size -> return ()
100
(_, [Apply u], []) | x == sizelt && y == size -> forceInfty u
101
(_, [], [Apply u]) | x == size && y == sizelt -> forceInfty u
104
-- | Compare two sizes. Only with --sized-types.
105
compareSizes :: Comparison -> Term -> Term -> TCM ()
106
compareSizes cmp u v = do
107
reportSDoc "tc.conv.size" 10 $ vcat
108
[ text "Comparing sizes"
109
, nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
116
reportSDoc "tc.conv.size" 15 $
117
nest 2 $ sep [ text (show u) <+> prettyTCM cmp
123
compareMaxViews cmp us vs
125
compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()
126
compareMaxViews cmp us vs = case (cmp, us, vs) of
127
(CmpLeq, _, (DSizeInf : _)) -> return ()
128
(cmp, [u], [v]) -> compareSizeViews cmp u v
129
(CmpLeq, us, [v]) -> forM_ us $ \ u -> compareSizeViews cmp u v
130
(CmpLeq, us, vs) -> forM_ us $ \ u -> compareBelowMax u vs
131
(CmpEq, us, vs) -> compareMaxViews CmpLeq us vs >> compareMaxViews CmpLeq vs us
132
-- _ -> typeError $ NotImplemented "compareMaxViews"
134
-- | @compareBelowMax u vs@ checks @u <= max vs@. Precondition: @size vs >= 2@
135
compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
136
compareBelowMax u vs =
137
alt (dontAssignMetas $ alts $ map (compareSizeViews CmpLeq u) vs) $ do
138
u <- unDeepSizeView u
141
addConstraint $ ValueCmp CmpLeq size u v
142
where alt c1 c2 = c1 `catchError` const c2
143
alts [] = __IMPOSSIBLE__
145
alts (c:cs) = c `alt` alts cs
147
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
148
compareSizeViews cmp s1' s2' = do
150
let (s1, s2) = removeSucs (s1', s2')
152
u <- unDeepSizeView s1
153
v <- unDeepSizeView s2
155
failure = withUnView $ \ u v -> typeError $ UnequalTerms cmp u v size
156
continue cmp = withUnView $ compareAtom cmp size
157
case (cmp, s1, s2) of
158
(CmpLeq, _, DSizeInf) -> return ()
159
(CmpEq, DSizeInf, DSizeInf) -> return ()
160
(CmpEq, DSizeVar{}, DSizeInf) -> failure
161
(_ , DSizeInf, DSizeVar{}) -> failure
162
(_ , DSizeInf, _ ) -> continue CmpEq
163
(CmpLeq, DSizeVar i n, DSizeVar j m) | i == j -> unless (n <= m) failure
164
(CmpLeq, DSizeVar i n, DSizeVar j m) | i /= j -> do
169
-- now we have i < u', in the worst case i+1 = u'
170
-- and we want to check i+n <= v
171
v <- unDeepSizeView s2
173
u'' <- sizeSuc (n - 1) u'
174
compareSizes cmp u'' v
175
else compareSizes cmp u' =<< sizeSuc 1 v
176
(CmpLeq, s1, s2) -> withUnView $ \ u v -> do
177
unlessM (trivial u v) $ addConstraint $ ValueCmp CmpLeq size u v
178
(CmpEq, s1, s2) -> continue cmp
181
-- | Compare two sizes. Only with --sized-types.
182
compareSizes :: Comparison -> Term -> Term -> TCM ()
183
compareSizes cmp u v = do
184
reportSDoc "tc.conv.size" 10 $ vcat
185
[ text "Comparing sizes"
186
, nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
192
reportSDoc "tc.conv.size" 15 $
193
nest 2 $ sep [ text (show u) <+> prettyTCM cmp
196
s1' <- deepSizeView u
197
s2' <- deepSizeView v
199
let failure = typeError $ UnequalTerms cmp u v size
200
(s1, s2) = removeSucs (s1', s2')
202
u <- unDeepSizeView s1
203
v <- unDeepSizeView s2
204
compareAtom cmp size u v
205
case (cmp, s1, s2) of
206
(CmpLeq, _, DSizeInf) -> return ()
207
(CmpEq, DSizeInf, DSizeInf) -> return ()
208
(CmpEq, DSizeVar{}, DSizeInf) -> failure
209
(_ , DSizeInf, DSizeVar{}) -> failure
210
(_ , DSizeInf, _ ) -> continue CmpEq
211
(CmpLeq, DSizeVar i n, DSizeVar j m) | i == j -> unless (n <= m) failure
212
(CmpLeq, DSizeVar i n, DSizeVar j m) | i /= j -> do
217
-- now we have i < u', in the worst case i+1 = u'
218
-- and we want to check i+n <= v
220
u'' <- sizeSuc (n - 1) u'
221
compareSizes cmp u'' v
222
else compareSizes cmp u' =<< sizeSuc 1 v
223
(CmpLeq, s1, s2) -> do
224
u <- unDeepSizeView s1
225
v <- unDeepSizeView s2
226
unlessM (trivial u v) $ addConstraint $ ValueCmp CmpLeq size u v
227
(CmpEq, s1, s2) -> continue cmp
51
237
(_, SizeInf, SizeSuc v) -> compareSizes CmpEq u v
52
238
(_, SizeSuc u, SizeSuc v) -> compareSizes cmp u v
54
ifM (trivial u v) (return ()) $
55
addConstraint $ ValueCmp CmpLeq size u v
240
unlessM (trivial u v) $ addConstraint $ ValueCmp CmpLeq size u v
56
241
_ -> compareAtom cmp size u v
244
isBounded :: Nat -> TCM BoundedSize
246
t <- reduce =<< typeOfBV i
247
case ignoreSharing $ unEl t of
249
sizelt <- getBuiltin' builtinSizeLt
250
return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
251
_ -> return BoundedNo
58
253
trivial :: Term -> Term -> TCM Bool
257
let triv = case (a, b) of
258
-- Andreas, 2012-02-24 filtering out more trivial constraints fixes
259
-- test/lib-succeed/SizeInconsistentMeta4.agda
260
((e, n), (e', n')) -> e == e' && n <= n'
262
((Rigid i, n), (Rigid j, m)) -> i == j && n <= m
62
265
reportSDoc "tc.conv.size" 15 $
63
nest 2 $ sep [ text (show a) <+> text "<="
266
nest 2 $ sep [ if triv then text "trivial constraint" else empty
267
, text (show a) <+> text "<="
66
return $ case (a, b) of
67
((Rigid i, n), (Rigid j, m)) -> i == j && n <= m
69
271
`catchError` \_ -> return False
273
-- | Whenever we create a bounded size meta, add a constraint
274
-- expressing the bound.
275
-- In @boundedSizeMetaHook v tel a@, @tel@ includes the current context.
276
boundedSizeMetaHook :: Term -> Telescope -> Type -> TCM ()
277
boundedSizeMetaHook v tel0 a = do
280
Just (BoundedLt u) -> do
282
let tel | n > 0 = telFromList $ genericDrop n $ telToList tel0
285
v <- sizeSuc 1 $ raise (size tel) v `apply` teleArgs tel
286
-- compareSizes CmpLeq v u
288
addConstraint $ ValueCmp CmpLeq size v u
291
-- | Test whether a problem consists only of size constraints.
292
isSizeProblem :: ProblemId -> TCM Bool
293
isSizeProblem pid = andM . map (isSizeConstraint . theConstraint) =<< getConstraintsForProblem pid
295
-- | Test is a constraint speaks about sizes.
296
isSizeConstraint :: Closure Constraint -> TCM Bool
297
isSizeConstraint (Closure{ clValue = ValueCmp _ s _ _ }) = isJust <$> isSizeType s
298
isSizeConstraint _ = return False
71
300
-- | Find the size constraints.
72
getSizeConstraints :: TCM [SizeConstraint]
301
getSizeConstraints :: TCM [Closure Constraint]
73
302
getSizeConstraints = do
74
303
cs <- getAllConstraints
76
let sizeConstraints cl@(Closure{ clValue = ValueCmp CmpLeq s _ _ })
78
sizeConstraints _ = []
79
scs <- mapM computeSizeConstraint $ concatMap (sizeConstraints . theConstraint) cs
80
return [ c | Just c <- scs ]
304
test <- isSizeTypeTest
305
let sizeConstraint cl@Closure{ clValue = ValueCmp CmpLeq s _ _ }
306
| isJust (test s) = Just cl
307
sizeConstraint _ = Nothing
308
return $ mapMaybe (sizeConstraint . theConstraint) cs
82
310
getSizeMetas :: TCM [(MetaId, Int)]
84
312
ms <- getOpenMetas
313
test <- isSizeTypeTest
86
314
let sizeCon m = do
315
let nothing = return []
87
316
mi <- lookupMeta m
88
317
case mvJudgement mi of
90
319
TelV tel b <- telView =<< instantiateFull a
93
else return [(m, size tel)]
322
Just _ -> return [(m, size tel)]
95
324
concat <$> mapM sizeCon ms
97
data SizeExpr = SizeMeta MetaId [CtxId]
327
getSizeMetas :: TCM ([(MetaId, Int)], [SizeConstraint])
330
test <- isSizeTypeTest
332
let nothing = return ([], [])
334
case mvJudgement mi of
336
TelV tel b <- telView =<< instantiateFull a
337
let noConstr = return ([(m, size tel)], [])
340
Just BoundedNo -> noConstr
341
Just (BoundedLt u) -> noConstr
343
Just (BoundedLt u) -> flip catchError (const $ noConstr) $ do
344
-- we assume the metavariable is used in an
345
-- extension of its creation context
346
ctxIds <- getContextId
347
let a = SizeMeta m $ take (size tel) $ reverse ctxIds
349
return ([(m, size tel)], [Leq a (n-1) b])
352
(mss, css) <- unzip <$> mapM sizeCon ms
353
return (concat mss, concat css)
100
data SizeConstraint = Leq SizeExpr Int SizeExpr
356
-- | Atomic size expressions.
358
= SizeMeta MetaId [Int] -- ^ A size meta applied to de Bruijn levels.
359
| Rigid Int -- ^ A de Bruijn level.
102
362
instance Show SizeExpr where
103
363
show (SizeMeta m _) = "X" ++ show (fromIntegral m :: Int)
104
show (Rigid i) = "c" ++ show (fromIntegral i :: Int)
364
show (Rigid i) = "c" ++ show i
366
-- | Size constraints we can solve.
368
= Leq SizeExpr Int SizeExpr -- ^ @Leq a +n b@ represents @a =< b + n@.
369
-- @Leq a -n b@ represents @a + n =< b@.
106
371
instance Show SizeConstraint where
110
374
| n > 0 = show a ++ " =< " ++ show b ++ " + " ++ show n
111
375
| otherwise = show a ++ " + " ++ show (-n) ++ " =< " ++ show b
113
computeSizeConstraint :: Closure Constraint -> TCM (Maybe SizeConstraint)
114
computeSizeConstraint cl =
115
enterClosure cl $ \c ->
377
-- | Compute a set of size constraints that all live in the same context
378
-- from constraints over terms of type size that may live in different
381
-- cf. 'Agda.TypeChecking.LevelConstraints.simplifyLevelConstraint'
382
computeSizeConstraints :: [Closure Constraint] -> TCM [SizeConstraint]
383
computeSizeConstraints [] = return [] -- special case to avoid maximum []
384
computeSizeConstraints cs = do
385
scs <- mapM computeSizeConstraint leqs
386
return [ c | Just c <- scs ]
388
-- get the constraints plus contexts they are defined in
389
unClosure cl = (envContext $ clEnv cl, clValue cl)
390
(gammas, ls) = unzip $ map unClosure cs
391
-- compute the longest context (common water level)
392
gamma = maximumBy (compare `on` size) gammas
393
waterLevel = size gamma
394
-- convert deBruijn indices to deBruijn levels to
395
-- enable comparing constraints under different contexts
396
leqs = zipWith raise (map ((waterLevel -) . size) gammas) ls
398
-- | Turn a constraint over de Bruijn levels into a size constraint.
399
computeSizeConstraint :: Constraint -> TCM (Maybe SizeConstraint)
400
computeSizeConstraint c = case c of
117
401
ValueCmp CmpLeq _ u v -> do
402
reportSDoc "tc.size.solve" 50 $ sep
403
[ text "converting size constraint"
118
406
(a, n) <- sizeExpr u
119
407
(b, m) <- sizeExpr v
120
408
return $ Just $ Leq a (m - n) b
121
`catchError` \err -> case errError err of
409
`catchError` \err -> case err of
122
410
PatternErr _ -> return Nothing
123
411
_ -> throwError err
124
412
_ -> __IMPOSSIBLE__
414
-- | Turn a term with de Bruijn levels into a size expression with offset.
416
-- Throws a 'patternViolation' if the term isn't a proper size expression.
126
417
sizeExpr :: Term -> TCM (SizeExpr, Int)
128
419
u <- reduce u -- Andreas, 2009-02-09.
129
420
-- This is necessary to surface the solutions of metavariables.
421
reportSDoc "tc.conv.size" 60 $ text "sizeExpr:" <+> prettyTCM u
135
SizeInf -> patternViolation
136
OtherSize u -> case u of
139
return (Rigid (cxt !! fromIntegral i), 0)
141
| all isVar args && distinct args -> do
143
return (SizeMeta m [ cxt !! fromIntegral i | Arg _ _ (Var i []) <- args ], 0)
424
SizeInf -> patternViolation
425
SizeSuc u -> mapSnd (+1) <$> sizeExpr u
426
OtherSize u -> case ignoreSharing u of
427
Var i [] -> return (Rigid i, 0) -- i is already a de Bruijn level.
428
MetaV m args | Just xs <- mapM isVar args, fastDistinct xs
429
-> return (SizeMeta m xs, 0)
144
430
_ -> patternViolation
146
isVar (Arg _ _ (Var _ [])) = True
432
isVar v = case ignoreSharing $ unArg v of
149
flexibleVariables :: SizeConstraint -> [(MetaId, [CtxId])]
436
-- | Compute list of size metavariables with their arguments
437
-- appearing in a constraint.
438
flexibleVariables :: SizeConstraint -> [(MetaId, [Int])]
150
439
flexibleVariables (Leq a _ b) = flex a ++ flex b
152
441
flex (Rigid _) = []
156
444
haveSizedTypes :: TCM Bool
157
445
haveSizedTypes = do
159
Def _ [] <- primSizeInf
160
Def _ [] <- primSizeSuc
446
Def _ [] <- ignoreSharing <$> primSize
447
Def _ [] <- ignoreSharing <$> primSizeInf
448
Def _ [] <- ignoreSharing <$> primSizeSuc
161
449
optSizedTypes <$> pragmaOptions
162
450
`catchError` \_ -> return False
452
-- | Convert size constraint into form where each meta is applied
453
-- to levels @0,1,..,n-1@ where @n@ is the arity of that meta.
455
-- @X[σ] <= t@ beomes @X[id] <= t[σ^-1]@
457
-- @X[σ] ≤ Y[τ]@ becomes @X[id] ≤ Y[τ[σ^-1]]@ or @X[σ[τ^1]] ≤ Y[id]@
458
-- whichever is defined. If none is defined, we give up.
460
canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
461
canonicalizeSizeConstraint c@(Leq a n b) =
463
(Rigid{}, Rigid{}) -> return c
464
(SizeMeta m xs, Rigid i) -> do
465
j <- findIndex (==i) xs
466
return $ Leq (SizeMeta m [0..size xs-1]) n (Rigid j)
467
(Rigid i, SizeMeta m xs) -> do
468
j <- findIndex (==i) xs
469
return $ Leq (Rigid j) n (SizeMeta m [0..size xs-1])
470
(SizeMeta m xs, SizeMeta l ys)
471
-- try to invert xs on ys
472
| Just ys' <- mapM (\ y -> findIndex (==y) xs) ys ->
473
return $ Leq (SizeMeta m [0..size xs-1]) n (SizeMeta l ys')
474
-- try to invert ys on xs
475
| Just xs' <- mapM (\ x -> findIndex (==x) ys) xs ->
476
return $ Leq (SizeMeta m xs') n (SizeMeta l [0..size ys-1])
478
| otherwise -> Nothing
164
480
solveSizeConstraints :: TCM ()
165
481
solveSizeConstraints = whenM haveSizedTypes $ do
166
cs <- getSizeConstraints
482
reportSLn "tc.size.solve" 70 $ "Considering to solve size constraints"
483
cs0 <- getSizeConstraints
484
cs <- computeSizeConstraints cs0
167
485
ms <- getSizeMetas
487
cs0 <- getSizeConstraints
488
cs1 <- computeSizeConstraints cs0
489
(ms,cs2) <- getSizeMetas
168
492
when (not (null cs) || not (null ms)) $ do
169
493
reportSLn "tc.size.solve" 10 $ "Solving size constraints " ++ show cs
171
let metas0 = map mkMeta $ groupOn fst $ concatMap flexibleVariables cs
495
cs <- return $ mapMaybe canonicalizeSizeConstraint cs
496
reportSLn "tc.size.solve" 10 $ "Canonicalized constraints: " ++ show cs
498
let -- Error for giving up
499
cannotSolve = typeError . GenericDocError =<<
500
vcat (text "Cannot solve size constraints" : map prettyTCM cs0)
502
{- OLD, before canonicalize
504
-- Ensure that each occurrence of a meta is applied to the same
505
-- arguments ("flexible variables").
506
-- Andreas, 2012-10-16 this is now redundant
507
mkMeta :: [(MetaId, [Int])] -> TCM (MetaId, [Int])
172
508
mkMeta ms@((m, xs) : _)
173
| allEqual (map snd ms) = (m, xs)
174
| otherwise = error $ "Inconsistent meta: " ++ show m ++ " " ++ show (map snd ms)
509
| allEqual (map snd ms) = return (m, xs)
511
reportSLn "tc.size.solve" 20 $
512
"Size meta variable " ++ show m ++ " not always applied to same arguments: " ++ show (nub (map snd ms))
175
514
mkMeta _ = __IMPOSSIBLE__
177
mkFlex (m, xs) = W.NewFlex (fromIntegral m) $ \i -> fromIntegral i `elem` xs
516
metas0 <- mapM mkMeta $ groupOn fst $ concatMap flexibleVariables cs
519
let mkFlex (m, xs) = W.NewFlex (fromIntegral m) $ \i -> fromIntegral i `elem` xs
522
let metas0 :: [(MetaId, Int)] -- meta id + arity
523
metas0 = nub $ map (mapSnd length) $ concatMap flexibleVariables cs
525
mkFlex (m, ar) = W.NewFlex (fromIntegral m) $ \i -> fromIntegral i < ar
179
527
mkConstr (Leq a n b) = W.Arc (mkNode a) n (mkNode b)
180
mkNode (Rigid i) = W.Rigid $ W.RVar $ fromIntegral i
528
mkNode (Rigid i) = W.Rigid $ W.RVar i
181
529
mkNode (SizeMeta m _) = W.Flex $ fromIntegral m
183
531
found (m, _) = elem m $ map fst metas0
533
-- Compute unconstrained metas
534
metas1 = filter (not . found) ms
536
{- OLD, before canonicalize
185
537
-- Compute unconstrained metas
186
538
let metas1 = map mkMeta' $ filter (not . found) ms
187
539
mkMeta' (m, n) = (m, [0..fromIntegral n - 1])
189
542
let metas = metas0 ++ metas1
191
544
reportSLn "tc.size.solve" 15 $ "Metas: " ++ show metas0 ++ ", " ++ show metas1
193
verboseS "tc.size.solve" 20 $ do
195
j <- mvJudgement <$> lookupMeta m
196
reportSDoc "" 0 $ prettyTCM j
546
verboseS "tc.size.solve" 20 $
547
-- debug print the type of all size metas
548
forM_ metas $ \ (m, _) ->
549
reportSDoc "" 0 $ prettyTCM =<< mvJudgement <$> lookupMeta m
551
-- run the Warshall solver
199
552
case W.solve $ map mkFlex metas ++ map mkConstr cs of
201
typeError $ GenericError $ "Unsolvable size constraints: " ++ show cs
553
Nothing -> cannotSolve
203
555
reportSLn "tc.size.solve" 10 $ "Solved constraints: " ++ show sol
206
558
let suc v = s `apply` [defaultArg v]
208
560
plus v n = suc $ plus v (n - 1)
211
let m = fromIntegral i
564
let m = fromIntegral i -- meta variable identifier
565
ar = maybe __IMPOSSIBLE__ id $ lookup m metas -- meta var arity
212
568
args = case lookup m metas of
214
570
Nothing -> __IMPOSSIBLE__
573
term (W.SizeConst W.Infinite) = infty
574
term (W.SizeVar j n) | j < ar = plus (var $ ar - j - 1) n
575
term _ = __IMPOSSIBLE__
216
578
term (W.SizeConst (W.Finite _)) = __IMPOSSIBLE__
217
term (W.SizeConst W.Infinite) = primSizeInf
218
579
term (W.SizeVar j n) = case findIndex (==fromIntegral j) $ reverse args of
219
Just x -> return $ plus (Var (fromIntegral x) []) n
580
Just x -> return $ plus (var x) n
220
581
Nothing -> __IMPOSSIBLE__
222
lam _ v = Lam NotHidden $ Abs "s" v
225
let v = foldr lam b args -- TODO: correct hiding
583
lam _ v = Lam NotHidden $ Abs "s" v -- hiding does not matter
585
-- convert size expression to term and abstract
586
v = flip (foldr lam) [0..ar-1] $ term e
227
588
reportSDoc "tc.size.solve" 20 $ sep
228
589
[ text (show m) <+> text ":="
229
590
, nest 2 $ prettyTCM v
593
-- Andreas, 2012-09-25: do not assign interaction metas to \infty
594
let isInf (W.SizeConst W.Infinite) = True
596
unlessM (isInteractionMeta m `and2M` return (isInf e)) $
234
599
mapM_ inst $ Map.toList sol
601
-- Andreas, 2012-09-19
602
-- The returned solution might not be consistent with
603
-- the hypotheses on rigid vars (j : Size< i).
604
-- Thus, we double check that all size constraints
605
-- have been solved correctly.
606
flip catchError (const cannotSolve) $
608
forM_ cs0 $ \ cl -> enterClosure cl solveConstraint
added
removed
src/full/Agda/TypeChecking/SizedTypes.hs
