module Agda.TypeChecking.SizedTypes where
import Control.Monad.Error
import Control.Monad
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 qualified Agda.Utils.Warshall as W
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Impossible
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Pretty (render)
#include "../undefined.h"
builtinSizeHook :: String -> QName -> Term -> Type -> TCM ()
builtinSizeHook s q e' t = do
when (s `elem` [builtinSizeLt, builtinSizeSuc]) $ do
modifySignature $ updateDefinition q
$ updateDefPolarity (const [Covariant])
. updateDefArgOccurrences (const [StrictPos])
when (s == builtinSizeMax) $ do
modifySignature $ updateDefinition q
$ updateDefPolarity (const [Covariant, Covariant])
. updateDefArgOccurrences (const [StrictPos, StrictPos])
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 [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 [u] | Just x == suc -> maxViewSuc_ (fromJust suc) <$> loop (unArg u)
Def x [u1,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
trySizeUniv :: Comparison -> Type -> Term -> Term
-> QName -> [Elim] -> QName -> [Elim] -> 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
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
]
]
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
isBounded :: Nat -> TCM BoundedSize
isBounded i = do
t <- reduce =<< typeOfBV i
case ignoreSharing $ unEl t of
Def x [u] -> do
sizelt <- getBuiltin' builtinSizeLt
return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
_ -> return BoundedNo
trivial :: Term -> Term -> TCM Bool
trivial u v = do
a <- sizeExpr u
b <- sizeExpr v
let triv = case (a, b) of
((e, n), (e', n')) -> e == e' && n <= n'
reportSDoc "tc.conv.size" 15 $
nest 2 $ sep [ if triv then text "trivial constraint" else empty
, text (show a) <+> text "<="
, text (show b)
]
return triv
`catchError` \_ -> return False
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 ()
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
cs <- getAllConstraints
test <- isSizeTypeTest
let sizeConstraint cl@Closure{ clValue = ValueCmp CmpLeq s _ _ }
| isJust (test s) = Just cl
sizeConstraint _ = Nothing
return $ mapMaybe (sizeConstraint . theConstraint) cs
getSizeMetas :: TCM [(MetaId, Int)]
getSizeMetas = do
ms <- getOpenMetas
test <- isSizeTypeTest
let sizeCon m = do
let nothing = return []
mi <- lookupMeta m
case mvJudgement mi of
HasType _ a -> do
TelV tel b <- telView =<< instantiateFull a
case test b of
Nothing -> nothing
Just _ -> return [(m, size tel)]
_ -> nothing
concat <$> mapM sizeCon ms
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 = do
scs <- mapM computeSizeConstraint leqs
return [ c | Just c <- scs ]
where
unClosure cl = (envContext $ clEnv cl, clValue cl)
(gammas, ls) = unzip $ map unClosure cs
gamma = maximumBy (compare `on` size) gammas
waterLevel = size gamma
leqs = zipWith raise (map ((waterLevel ) . size) gammas) 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 args | Just xs <- mapM isVar args, fastDistinct xs
-> return (SizeMeta m xs, 0)
_ -> patternViolation
where
isVar 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)]
haveSizedTypes :: TCM Bool
haveSizedTypes = do
Def _ [] <- ignoreSharing <$> primSize
Def _ [] <- ignoreSharing <$> primSizeInf
Def _ [] <- ignoreSharing <$> primSizeSuc
optSizedTypes <$> pragmaOptions
`catchError` \_ -> return False
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
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)
let metas0 :: [(MetaId, Int)]
metas0 = nub $ map (mapSnd length) $ concatMap flexibleVariables cs
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
found (m, _) = elem m $ map fst metas0
metas1 = filter (not . found) ms
let metas = metas0 ++ metas1
reportSLn "tc.size.solve" 15 $ "Metas: " ++ show metas0 ++ ", " ++ show metas1
verboseS "tc.size.solve" 20 $
forM_ metas $ \ (m, _) ->
reportSDoc "" 0 $ prettyTCM =<< mvJudgement <$> lookupMeta 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 = maybe __IMPOSSIBLE__ id $ lookup m metas
term (W.SizeConst W.Infinite) = infty
term (W.SizeVar j n) | j < ar = plus (var $ ar j 1) n
term _ = __IMPOSSIBLE__
lam _ v = Lam NotHidden $ Abs "s" v
v = flip (foldr lam) [0..ar1] $ 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 (isInteractionMeta m `and2M` return (isInf e)) $
assignTerm m v
mapM_ inst $ Map.toList sol
flip catchError (const cannotSolve) $
noConstraints $
forM_ cs0 $ \ cl -> enterClosure cl solveConstraint