{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.SizedTypes where
import Prelude hiding (null)
import Control.Monad.Writer
import qualified Data.Foldable as Fold
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.NonemptyList
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.Pretty as P
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
[ "checking that " <+> prettyTCM t <+> " is not an empty type of sizes"
, if null tel then empty else do
"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
[ "- 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 $ " - 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
"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 $ "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 $ singleton $ 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 $ singleton $ DSizeVar i 0
MetaV x us -> return $ singleton $ DSizeMeta x us 0
_ -> return $ singleton $ DOtherSize v
loop v
compareSizes :: Comparison -> Term -> Term -> TCM ()
compareSizes cmp u v = verboseBracket "tc.conv.size" 10 "compareSizes" $ do
reportSDoc "tc.conv.size" 10 $ vcat
[ "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 [ pretty u <+> prettyTCM cmp
, pretty 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:![]) -> Fold.forM_ us $ \ u -> compareSizeViews cmp u v
(CmpLeq, us, vs) -> Fold.forM_ us $ \ u -> compareBelowMax u vs
(CmpEq, us, vs) -> do
compareMaxViews CmpLeq us vs
compareMaxViews CmpLeq vs us
compareBelowMax :: DeepSizeView -> SizeMaxView -> TCM ()
compareBelowMax u vs = verboseBracket "tc.conv.size" 45 "compareBelowMax" $ do
reportSDoc "tc.conv.size" 45 $ sep
[ pretty u
, pretty CmpLeq
, pretty vs
]
alt (dontAssignMetas $ Fold.foldr1 alt $ fmap (compareSizeViews CmpLeq u) vs) $ do
reportSDoc "tc.conv.size" 45 $ vcat
[ "compareBelowMax: giving up"
]
u <- unDeepSizeView u
v <- unMaxView vs
size <- sizeType
giveUp CmpLeq size u v
where
alt c1 c2 = c1 `catchError` const c2
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
compareSizeViews cmp s1' s2' = do
reportSDoc "tc.conv.size" 45 $ hsep
[ "compareSizeViews"
, pretty s1'
, pretty cmp
, pretty 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) $ giveUp CmpLeq size u v
(CmpEq, s1, s2) -> continue cmp
giveUp :: Comparison -> Type -> Term -> Term -> TCM ()
giveUp cmp size u v =
ifM (asksTC envAssignMetas)
(addConstraint $ ValueCmp CmpLeq size u v)
(typeError $ UnequalTerms cmp u v size)
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 "trivial constraint" else empty
, pretty a <+> "<="
, pretty 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, Show)
instance Pretty OldSizeExpr where
pretty (SizeMeta m _) = P.text $ "X" ++ show (fromIntegral m :: Int)
pretty (Rigid i) = P.text $ "c" ++ show i
data OldSizeConstraint
= Leq OldSizeExpr Int OldSizeExpr
deriving (Show)
instance Pretty OldSizeConstraint where
pretty (Leq a n b)
| n == 0 = P.pretty a P.<+> "=<" P.<+> P.pretty b
| n > 0 = P.pretty a P.<+> "=<" P.<+> P.pretty b P.<+> "+" P.<+> P.text (show n)
| otherwise = P.pretty a P.<+> "+" P.<+> P.text (show (-n)) P.<+> "=<" P.<+> P.pretty 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
[ "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 $ "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 (IApply _ _ v) = isVar (Apply (defaultArg v))
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 ("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 <+> ":="
, 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