{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.SizedTypes where
import Prelude hiding (null)
import Control.Monad.Writer
import qualified Data.List as List
import qualified Data.Map as Map
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 {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.Constraints
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.List as List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.Warshall as W
#include "undefined.h"
import Agda.Utils.Impossible
checkSizeLtSat :: Term -> TCM ()
checkSizeLtSat t = whenM haveSizeLt $ do
reportSDoc "tc.size" 10 $ do
tel <- getContextTelescope
sep
[ text "checking that " <+> prettyTCM t <+> text " is not an empty type of sizes"
, if null tel then empty else do
text "in context " <+> inTopContext (prettyTCM tel)
]
reportSLn "tc.size" 60 $ "- raw type = " ++ show t
let postpone :: Term -> TCM ()
postpone t = do
reportSDoc "tc.size.lt" 20 $ sep
[ text "- postponing `not empty type of sizes' check for " <+> prettyTCM t ]
addConstraint $ CheckSizeLtSat t
let ok :: TCM ()
ok = reportSLn "tc.size.lt" 20 $ "- succeeded: not an empty type of sizes"
ifBlocked t (const postpone) $ \ _ t -> do
reportSLn "tc.size.lt" 20 $ "- type is not blocked"
caseMaybeM (isSizeType t) ok $ \ b -> do
reportSLn "tc.size.lt" 20 $ " - type is a size type"
case b of
BoundedNo -> ok
BoundedLt b -> do
reportSDoc "tc.size.lt" 20 $ text " - type is SIZELT" <+> prettyTCM b
ifBlocked b (\ _ _ -> postpone t) $ \ _ b -> do
reportSLn "tc.size.lt" 20 $ " - size bound is not blocked"
catchConstraint (CheckSizeLtSat t) $ do
unlessM (checkSizeNeverZero b) $ do
typeError . GenericDocError =<< do
text "Possibly empty type of sizes " <+> prettyTCM t
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero u = do
v <- sizeView u
case v of
SizeInf -> return True
SizeSuc{} -> return True
OtherSize u ->
case u of
Var i [] -> checkSizeVarNeverZero i
_ -> return False
checkSizeVarNeverZero :: Int -> TCM Bool
checkSizeVarNeverZero i = do
reportSDoc "tc.size" 20 $ text "checkSizeVarNeverZero" <+> prettyTCM (var i)
ts <- map (snd . unDom) . take i <$> getContext
(n, Any meta) <- runWriterT $ minSizeValAux ts $ repeat 0
if n > 0 then return True else
if meta then patternViolation else return False
where
minSizeValAux :: [Type] -> [Int] -> WriterT Any TCM Int
minSizeValAux _ [] = __IMPOSSIBLE__
minSizeValAux [] (n : _) = return n
minSizeValAux (t : ts) (n : ns) = do
reportSDoc "tc.size" 60 $
text ("minSizeVal (n:ns) = " ++ show (take (length ts + 2) $ n:ns) ++
" t =") <+> (text . show) t
let cont = minSizeValAux ts ns
perhaps = tell (Any True) >> cont
ifBlockedType t (\ _ _ -> perhaps) $ \ _ t -> do
caseMaybeM (liftTCM $ isSizeType t) cont $ \ b -> do
case b of
BoundedNo -> cont
BoundedLt u -> ifBlocked u (\ _ _ -> perhaps) $ \ _ u -> do
reportSLn "tc.size" 60 $ "minSizeVal upper bound u = " ++ show u
v <- liftTCM $ deepSizeView u
case v of
DSizeVar j m -> do
reportSLn "tc.size" 60 $ "minSizeVal upper bound v = " ++ show v
let ns' = List.updateAt j (max $ n+1-m) ns
reportSLn "tc.size" 60 $ "minSizeVal ns' = " ++ show (take (length ts + 1) ns')
minSizeValAux ts ns'
DSizeMeta{} -> perhaps
_ -> cont
isBounded :: MonadTCM tcm => Nat -> tcm BoundedSize
isBounded i = liftTCM $ do
t <- reduce =<< typeOfBV i
case 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 $ drop n $ telToList tel0
| otherwise = tel0
addContext 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 _ <- primSize
Def sizelt _ <- 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 [] <- primSizeInf
Def suc [] <- primSizeSuc
let loop v = do
v <- reduce v
case 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 = do
reportSDoc "tc.conv.size" 45 $ vcat
[ text "compareBelowMax"
]
alt (dontAssignMetas $ alts $ map (compareSizeViews CmpLeq u) vs) $ do
reportSDoc "tc.conv.size" 45 $ vcat
[ text "compareBelowMax: giving up"
]
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
reportSDoc "tc.conv.size" 45 $ hsep
[ text "compareSizeViews"
, text (show s1')
, text (show cmp)
, text (show s2')
]
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 ) <- oldSizeExpr u
b@(e', n') <- oldSizeExpr 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
takeSizeConstraints :: TCM [Closure Constraint]
takeSizeConstraints = do
test <- isSizeTypeTest
let sizeConstraint :: Closure Constraint -> Bool
sizeConstraint cl@Closure{ clValue = ValueCmp CmpLeq s _ _ }
| isJust (test $ unEl s) = True
sizeConstraint _ = False
cs <- filter sizeConstraint . map theConstraint <$> getAllConstraints
dropConstraints $ sizeConstraint . theConstraint
return cs
getSizeConstraints :: TCM [Closure Constraint]
getSizeConstraints = do
test <- isSizeTypeTest
let sizeConstraint :: Closure Constraint -> Bool
sizeConstraint cl@Closure{ clValue = ValueCmp CmpLeq s _ _ }
| isJust (test $ unEl s) = True
sizeConstraint _ = False
filter sizeConstraint . map 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
_ | BlockedConst{} <- mvInstantiation mi -> no
HasType _ a -> do
TelV tel b <- telView a
caseMaybe (test $ unEl b) no $ \ _ -> do
let yes = return $ Just (m, a, tel)
if interactionMetas then yes else do
ifM (isJust <$> isInteractionMeta m) no yes
_ -> no
data OldSizeExpr
= SizeMeta MetaId [Int]
| Rigid Int
deriving (Eq)
instance Show OldSizeExpr where
show (SizeMeta m _) = "X" ++ show (fromIntegral m :: Int)
show (Rigid i) = "c" ++ show i
data OldSizeConstraint
= Leq OldSizeExpr Int OldSizeExpr
instance Show OldSizeConstraint 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
oldComputeSizeConstraints :: [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = return []
oldComputeSizeConstraints cs = catMaybes <$> mapM oldComputeSizeConstraint 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
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint c =
case c of
ValueCmp CmpLeq _ u v -> do
reportSDoc "tc.size.solve" 50 $ sep
[ text "converting size constraint"
, prettyTCM c
]
(a, n) <- oldSizeExpr u
(b, m) <- oldSizeExpr v
return $ Just $ Leq a (m - n) b
`catchError` \ err -> case err of
PatternErr{} -> return Nothing
_ -> throwError err
_ -> __IMPOSSIBLE__
oldSizeExpr :: Term -> TCM (OldSizeExpr, Int)
oldSizeExpr u = do
u <- reduce u
reportSDoc "tc.conv.size" 60 $ text "oldSizeExpr:" <+> prettyTCM u
s <- sizeView u
case s of
SizeInf -> patternViolation
SizeSuc u -> mapSnd (+1) <$> oldSizeExpr u
OtherSize u -> case 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 unArg v of
Var i [] -> Just i
_ -> Nothing
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables (Leq a _ b) = flex a ++ flex b
where
flex (Rigid _) = []
flex (SizeMeta m xs) = [(m, xs)]
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint c@(Leq a n b) =
case (a,b) of
(Rigid{}, Rigid{}) -> return c
(SizeMeta m xs, Rigid i) -> do
j <- List.findIndex (==i) xs
return $ Leq (SizeMeta m [0..size xs-1]) n (Rigid j)
(Rigid i, SizeMeta m xs) -> do
j <- List.findIndex (==i) xs
return $ Leq (Rigid j) n (SizeMeta m [0..size xs-1])
(SizeMeta m xs, SizeMeta l ys)
| Just ys' <- mapM (\ y -> List.findIndex (==y) xs) ys ->
return $ Leq (SizeMeta m [0..size xs-1]) n (SizeMeta l ys')
| Just xs' <- mapM (\ x -> List.findIndex (==x) ys) xs ->
return $ Leq (SizeMeta m xs') n (SizeMeta l [0..size ys-1])
| otherwise -> Nothing
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints = whenM haveSizedTypes $ do
reportSLn "tc.size.solve" 70 $ "Considering to solve size constraints"
cs0 <- getSizeConstraints
cs <- oldComputeSizeConstraints 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 oldCanonicalizeSizeConstraint 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 = List.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)]
-> [OldSizeConstraint]
-> 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
suc <- primSizeSuc
infty <- primSizeInf
let plus v 0 = v
plus v n = suc `apply1` 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
[ pretty m <+> text ":="
, nest 2 $ prettyTCM v
]
let isInf (W.SizeConst W.Infinite) = True
isInf _ = False
unlessM (((isInf e &&) . isJust <$> isInteractionMeta m) `or2M` isFrozen m) $
assignTerm m tel v
mapM_ inst $ Map.toList sol
return True