module Agda.TypeChecking.SizedTypes where
import Data.Function
import Data.List
import qualified Data.Map as Map
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.Warshall as W
#include "undefined.h"
import Agda.Utils.Impossible
isBounded :: MonadTCM tcm => Nat -> tcm BoundedSize
isBounded i = liftTCM $ do
t <- reduce =<< typeOfBV i
case ignoreSharing $ unEl t of
Def x [Apply u] -> do
sizelt <- getBuiltin' builtinSizeLt
return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
_ -> return BoundedNo
boundedSizeMetaHook :: Term -> Telescope -> Type -> TCM ()
boundedSizeMetaHook v tel0 a = do
res <- isSizeType a
case res of
Just (BoundedLt u) -> do
n <- getContextSize
let tel | n > 0 = telFromList $ genericDrop n $ telToList tel0
| otherwise = tel0
addCtxTel tel $ do
v <- sizeSuc 1 $ raise (size tel) v `apply` teleArgs tel
size <- sizeType
addConstraint $ ValueCmp CmpLeq size v u
_ -> return ()
trySizeUniv :: Comparison -> Type -> Term -> Term
-> QName -> Elims -> QName -> Elims -> TCM ()
trySizeUniv cmp t m n x els1 y els2 = do
let failure = typeError $ UnequalTerms cmp m n t
forceInfty u = compareSizes CmpEq (unArg u) =<< primSizeInf
(size, sizelt) <- flip catchError (const failure) $ do
Def size _ <- ignoreSharing <$> primSize
Def sizelt _ <- ignoreSharing <$> primSizeLt
return (size, sizelt)
case (cmp, els1, els2) of
(CmpLeq, [_], []) | x == sizelt && y == size -> return ()
(_, [Apply u], []) | x == sizelt && y == size -> forceInfty u
(_, [], [Apply u]) | x == size && y == sizelt -> forceInfty u
_ -> failure
deepSizeView :: Term -> TCM DeepSizeView
deepSizeView v = do
Def inf [] <- ignoreSharing <$> primSizeInf
Def suc [] <- ignoreSharing <$> primSizeSuc
let loop v = do
v <- reduce v
case ignoreSharing v of
Def x [] | x == inf -> return $ DSizeInf
Def x [Apply u] | x == suc -> sizeViewSuc_ suc <$> loop (unArg u)
Var i [] -> return $ DSizeVar i 0
MetaV x us -> return $ DSizeMeta x us 0
_ -> return $ DOtherSize v
loop v
sizeMaxView :: Term -> TCM SizeMaxView
sizeMaxView v = do
inf <- getBuiltinDefName builtinSizeInf
suc <- getBuiltinDefName builtinSizeSuc
max <- getBuiltinDefName builtinSizeMax
let loop v = do
v <- reduce v
case v of
Def x [] | Just x == inf -> return $ [DSizeInf]
Def x [Apply u] | Just x == suc -> maxViewSuc_ (fromJust suc) <$> loop (unArg u)
Def x [Apply u1, Apply u2] | Just x == max -> maxViewMax <$> loop (unArg u1) <*> loop (unArg u2)
Var i [] -> return $ [DSizeVar i 0]
MetaV x us -> return $ [DSizeMeta x us 0]
_ -> return $ [DOtherSize v]
loop v
compareSizes :: Comparison -> Term -> Term -> TCM ()
compareSizes cmp u v = do
reportSDoc "tc.conv.size" 10 $ vcat
[ text "Comparing sizes"
, nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
, prettyTCM v
]
]
verboseS "tc.conv.size" 60 $ do
u <- reduce u
v <- reduce v
reportSDoc "tc.conv.size" 60 $
nest 2 $ sep [ text (show u) <+> prettyTCM cmp
, text (show v)
]
us <- sizeMaxView u
vs <- sizeMaxView v
compareMaxViews cmp us vs
compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> TCM ()
compareMaxViews cmp us vs = case (cmp, us, vs) of
(CmpLeq, _, (DSizeInf : _)) -> return ()
(cmp, [u], [v]) -> compareSizeViews cmp u v
(CmpLeq, us, [v]) -> forM_ us $ \ u -> compareSizeViews cmp u v
(CmpLeq, us, vs) -> forM_ us $ \ u -> compareBelowMax u vs
(CmpEq, us, vs) -> compareMaxViews CmpLeq us vs >> compareMaxViews CmpLeq vs us
compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
compareBelowMax u vs =
alt (dontAssignMetas $ alts $ map (compareSizeViews CmpLeq u) vs) $ do
u <- unDeepSizeView u
v <- unMaxView vs
size <- sizeType
addConstraint $ ValueCmp CmpLeq size u v
where alt c1 c2 = c1 `catchError` const c2
alts [] = __IMPOSSIBLE__
alts [c] = c
alts (c:cs) = c `alt` alts cs
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
compareSizeViews cmp s1' s2' = do
size <- sizeType
let (s1, s2) = removeSucs (s1', s2')
withUnView cont = do
u <- unDeepSizeView s1
v <- unDeepSizeView s2
cont u v
failure = withUnView $ \ u v -> typeError $ UnequalTerms cmp u v size
continue cmp = withUnView $ compareAtom cmp size
case (cmp, s1, s2) of
(CmpLeq, _, DSizeInf) -> return ()
(CmpEq, DSizeInf, DSizeInf) -> return ()
(CmpEq, DSizeVar{}, DSizeInf) -> failure
(_ , DSizeInf, DSizeVar{}) -> failure
(_ , DSizeInf, _ ) -> continue CmpEq
(CmpLeq, DSizeVar i n, DSizeVar j m) | i == j -> unless (n <= m) failure
(CmpLeq, DSizeVar i n, DSizeVar j m) | i /= j -> do
res <- isBounded i
case res of
BoundedNo -> failure
BoundedLt u' -> do
v <- unDeepSizeView s2
if n > 0 then do
u'' <- sizeSuc (n 1) u'
compareSizes cmp u'' v
else compareSizes cmp u' =<< sizeSuc 1 v
(CmpLeq, s1, s2) -> withUnView $ \ u v -> do
unlessM (trivial u v) $ addConstraint $ ValueCmp CmpLeq size u v
(CmpEq, s1, s2) -> continue cmp
trivial :: Term -> Term -> TCM Bool
trivial u v = do
a@(e , n ) <- sizeExpr u
b@(e', n') <- sizeExpr v
let triv = e == e' && n <= n'
reportSDoc "tc.conv.size" 60 $
nest 2 $ sep [ if triv then text "trivial constraint" else empty
, text (show a) <+> text "<="
, text (show b)
]
return triv
`catchError` \_ -> return False
isSizeProblem :: ProblemId -> TCM Bool
isSizeProblem pid = andM . map (isSizeConstraint . theConstraint) =<< getConstraintsForProblem pid
isSizeConstraint :: Closure Constraint -> TCM Bool
isSizeConstraint Closure{ clValue = ValueCmp _ s _ _ } = isJust <$> isSizeType s
isSizeConstraint _ = return False
getSizeConstraints :: TCM [Closure Constraint]
getSizeConstraints = do
test <- isSizeTypeTest
let sizeConstraint cl@Closure{ clValue = ValueCmp CmpLeq s _ _ }
| isJust (test s) = Just cl
sizeConstraint _ = Nothing
mapMaybe (sizeConstraint . theConstraint) <$> getAllConstraints
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas interactionMetas = do
test <- isSizeTypeTest
catMaybes <$> do
getOpenMetas >>= do
mapM $ \ m -> do
let no = return Nothing
mi <- lookupMeta m
case mvJudgement mi of
HasType _ a -> do
TelV tel b <- telView a
caseMaybe (test b) no $ \ _ -> do
let yes = return $ Just (m, a, tel)
if interactionMetas then yes else do
ifM (isJust <$> isInteractionMeta m) no yes
_ -> no
data SizeExpr
= SizeMeta MetaId [Int]
| Rigid Int
deriving (Eq)
instance Show SizeExpr where
show (SizeMeta m _) = "X" ++ show (fromIntegral m :: Int)
show (Rigid i) = "c" ++ show i
data SizeConstraint
= Leq SizeExpr Int SizeExpr
instance Show SizeConstraint where
show (Leq a n b)
| n == 0 = show a ++ " =< " ++ show b
| n > 0 = show a ++ " =< " ++ show b ++ " + " ++ show n
| otherwise = show a ++ " + " ++ show (n) ++ " =< " ++ show b
computeSizeConstraints :: [Closure Constraint] -> TCM [SizeConstraint]
computeSizeConstraints [] = return []
computeSizeConstraints cs = catMaybes <$> mapM computeSizeConstraint leqs
where
gammas = map (envContext . clEnv) cs
ls = map clValue cs
ns = map size gammas
waterLevel = maximum ns
leqs = zipWith raise (map (waterLevel ) ns) ls
computeSizeConstraint :: Constraint -> TCM (Maybe SizeConstraint)
computeSizeConstraint c =
case c of
ValueCmp CmpLeq _ u v -> do
reportSDoc "tc.size.solve" 50 $ sep
[ text "converting size constraint"
, prettyTCM c
]
(a, n) <- sizeExpr u
(b, m) <- sizeExpr v
return $ Just $ Leq a (m n) b
`catchError` \ err -> case err of
PatternErr{} -> return Nothing
_ -> throwError err
_ -> __IMPOSSIBLE__
sizeExpr :: Term -> TCM (SizeExpr, Int)
sizeExpr u = do
u <- reduce u
reportSDoc "tc.conv.size" 60 $ text "sizeExpr:" <+> prettyTCM u
s <- sizeView u
case s of
SizeInf -> patternViolation
SizeSuc u -> mapSnd (+1) <$> sizeExpr u
OtherSize u -> case ignoreSharing u of
Var i [] -> return (Rigid i, 0)
MetaV m es | Just xs <- mapM isVar es, fastDistinct xs
-> return (SizeMeta m xs, 0)
_ -> patternViolation
where
isVar (Proj{}) = Nothing
isVar (Apply v) = case ignoreSharing $ unArg v of
Var i [] -> Just i
_ -> Nothing
flexibleVariables :: SizeConstraint -> [(MetaId, [Int])]
flexibleVariables (Leq a _ b) = flex a ++ flex b
where
flex (Rigid _) = []
flex (SizeMeta m xs) = [(m, xs)]
canonicalizeSizeConstraint :: SizeConstraint -> Maybe SizeConstraint
canonicalizeSizeConstraint c@(Leq a n b) =
case (a,b) of
(Rigid{}, Rigid{}) -> return c
(SizeMeta m xs, Rigid i) -> do
j <- findIndex (==i) xs
return $ Leq (SizeMeta m [0..size xs1]) n (Rigid j)
(Rigid i, SizeMeta m xs) -> do
j <- findIndex (==i) xs
return $ Leq (Rigid j) n (SizeMeta m [0..size xs1])
(SizeMeta m xs, SizeMeta l ys)
| Just ys' <- mapM (\ y -> findIndex (==y) xs) ys ->
return $ Leq (SizeMeta m [0..size xs1]) n (SizeMeta l ys')
| Just xs' <- mapM (\ x -> findIndex (==x) ys) xs ->
return $ Leq (SizeMeta m xs') n (SizeMeta l [0..size ys1])
| otherwise -> Nothing
solveSizeConstraints :: TCM ()
solveSizeConstraints = whenM haveSizedTypes $ do
reportSLn "tc.size.solve" 70 $ "Considering to solve size constraints"
cs0 <- getSizeConstraints
cs <- computeSizeConstraints cs0
ms <- getSizeMetas True
when (not (null cs) || not (null ms)) $ do
reportSLn "tc.size.solve" 10 $ "Solving size constraints " ++ show cs
cs <- return $ mapMaybe canonicalizeSizeConstraint cs
reportSLn "tc.size.solve" 10 $ "Canonicalized constraints: " ++ show cs
let
cannotSolve = typeError . GenericDocError =<<
vcat (text "Cannot solve size constraints" : map prettyTCM cs0)
metas0 :: [(MetaId, Int)]
metas0 = nub $ map (mapSnd length) $ concatMap flexibleVariables cs
metas1 :: [(MetaId, Int)]
metas1 = forMaybe ms $ \ (m, _, tel) ->
maybe (Just (m, size tel)) (const Nothing) $
lookup m metas0
metas = metas0 ++ metas1
reportSLn "tc.size.solve" 15 $ "Metas: " ++ show metas0 ++ ", " ++ show metas1
verboseS "tc.size.solve" 20 $
forM_ metas $ \ (m, _) ->
reportSDoc "tc.size.solve" 20 $ prettyTCM =<< mvJudgement <$> lookupMeta m
unlessM (oldSolver metas cs) cannotSolve
flip catchError (const cannotSolve) $
noConstraints $
forM_ cs0 $ \ cl -> enterClosure cl solveConstraint
oldSolver
:: [(MetaId, Int)]
-> [SizeConstraint]
-> TCM Bool
oldSolver metas cs = do
let cannotSolve = return False
mkFlex (m, ar) = W.NewFlex (fromIntegral m) $ \ i -> fromIntegral i < ar
mkConstr (Leq a n b) = W.Arc (mkNode a) n (mkNode b)
mkNode (Rigid i) = W.Rigid $ W.RVar i
mkNode (SizeMeta m _) = W.Flex $ fromIntegral m
case W.solve $ map mkFlex metas ++ map mkConstr cs of
Nothing -> cannotSolve
Just sol -> do
reportSLn "tc.size.solve" 10 $ "Solved constraints: " ++ show sol
s <- primSizeSuc
infty <- primSizeInf
let suc v = s `apply` [defaultArg v]
plus v 0 = v
plus v n = suc $ plus v (n 1)
inst (i, e) = do
let m = fromIntegral i
ar = fromMaybe __IMPOSSIBLE__ $ lookup m metas
term (W.SizeConst W.Infinite) = infty
term (W.SizeVar j n) | j < ar = plus (var $ ar j 1) n
term _ = __IMPOSSIBLE__
tel = replicate ar $ defaultArg "s"
v = term e
reportSDoc "tc.size.solve" 20 $ sep
[ text (show m) <+> text ":="
, nest 2 $ prettyTCM v
]
let isInf (W.SizeConst W.Infinite) = True
isInf _ = False
unlessM ((isJust <$> isInteractionMeta m) `and2M` return (isInf e)) $
assignTerm m tel v
mapM_ inst $ Map.toList sol
return True