{-# 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 Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
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.Functor
import Agda.Utils.List as List
import Agda.Utils.Maybe
import Agda.Utils.Monad
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
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
ifBlocked 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 :: (MonadReduce m, MonadTCEnv m, HasBuiltins m)
=> Nat -> m BoundedSize
isBounded i = 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
:: ( MonadConstraint m
, MonadTCEnv m
, ReadTCState m
, MonadAddContext m
, HasOptions m
, HasBuiltins m
)
=> Term -> Telescope -> Type -> m ()
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
addConstraint $ ValueCmp CmpLeq AsSizes v u
_ -> return ()
trySizeUniv
:: MonadConversion m
=> Comparison -> CompareAs -> Term -> Term
-> QName -> Elims -> QName -> Elims -> m ()
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 :: (MonadReduce m, HasBuiltins m) => Term -> m 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 :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
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 :: (MonadConversion m) => Comparison -> SizeMaxView -> SizeMaxView -> m ()
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 :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
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 :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
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 AsSizes
continue cmp = withUnView $ compareAtom cmp AsSizes
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 :: (MonadConversion m) => Comparison -> Type -> Term -> Term -> m ()
giveUp cmp size u v =
ifM (asksTC envAssignMetas)
(addConstraint $ ValueCmp CmpLeq AsSizes u v)
(typeError $ UnequalTerms cmp u v AsSizes)
trivial :: (MonadConversion m) => Term -> Term -> m 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 :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
isSizeProblem pid = do
test <- isSizeTypeTest
all (mkIsSizeConstraint test (const True) . theConstraint) <$> getConstraintsForProblem pid
isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool
isSizeConstraint p c = isSizeTypeTest <&> \ test -> mkIsSizeConstraint test p c
mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint test = isSizeConstraint_ $ isJust . test . unEl
isSizeConstraint_
:: (Type -> Bool)
-> (Comparison -> Bool)
-> Closure Constraint
-> Bool
isSizeConstraint_ _isSizeType p Closure{ clValue = ValueCmp cmp AsSizes _ _ } = p cmp
isSizeConstraint_ isSizeType p Closure{ clValue = ValueCmp cmp (AsTermsOf s) _ _ } = p cmp && isSizeType s
isSizeConstraint_ _isSizeType _ _ = False
takeSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
takeSizeConstraints p = do
test <- isSizeTypeTest
map theConstraint <$> takeConstraints (mkIsSizeConstraint test p . theConstraint)
getSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
getSizeConstraints p = do
test <- isSizeTypeTest
filter (mkIsSizeConstraint test p) . 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 _ cmp 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 :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m)
=> Term -> m (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 (== CmpLeq)
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.nubOn id $ 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