module Agda.TypeChecking.SizedTypes.Solve where
import Control.Monad.Error
import Data.Foldable (Foldable, foldMap)
import Data.Function
import Data.List
import Data.Monoid (mappend)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Traversable (Traversable)
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad as TCM
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 as C
import qualified Agda.TypeChecking.SizedTypes as S
import Agda.TypeChecking.SizedTypes.Syntax as Size
import Agda.TypeChecking.SizedTypes.Utils
import Agda.TypeChecking.SizedTypes.WarshallSolver as Size
import Agda.Utils.Cluster
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "../../undefined.h"
import Agda.Utils.Impossible
solveSizeConstraints :: TCM ()
solveSizeConstraints = do
cs0 <- S.getSizeConstraints
let
cannotSolve = typeError . GenericDocError =<<
vcat (text "Cannot solve size constraints" : map prettyTCM
cs0)
unless (null cs0) $ solveSizeConstraints_ cs0
ms <- S.getSizeMetas False
unless (null ms) $ do
inf <- primSizeInf
forM_ ms $ \ (m, t, tel) -> do
reportSDoc "tc.size.solve" 20 $
text "solution " <+> prettyTCM (MetaV m []) <+>
text " := " <+> prettyTCM inf
assignMeta 0 m t (downFrom $ size tel) inf
unless (null cs0 && null ms) $ do
flip catchError (const cannotSolve) $
noConstraints $
forM_ cs0 $ \ cl -> enterClosure cl solveConstraint
solveSizeConstraints_ :: [Closure TCM.Constraint] -> TCM ()
solveSizeConstraints_ cs0 = do
ccs <- catMaybes <$> do
forM cs0 $ \ c -> fmap (c,) <$> computeSizeConstraint c
cs <- concat <$> do
forM ccs $ \ (c, HypSizeConstraint cxt hids hs sc) -> do
case simplify1 (\ c -> Just [c]) sc of
Nothing -> typeError . GenericDocError =<< do
text "Contradictory size constraint" <+> prettyTCM c
Just cs -> return $ HypSizeConstraint cxt hids hs <$> cs
let (csNoM, csMs) = (`partitionMaybe` cs) $ \ c ->
fmap (c,) $ uncons $ map (metaId . sizeMetaId) $ Set.toList $ flexs c
css = cluster' csMs
unless (null csNoM) __IMPOSSIBLE__
forM_ css solveCluster
solveCluster :: [HypSizeConstraint] -> TCM ()
solveCluster [] = __IMPOSSIBLE__
solveCluster cs = do
let err reason = typeError . GenericDocError =<< do
vcat $
[ text $ "Cannot solve size constraints" ] ++ map prettyTCM cs ++
[ text $ "Reason: " ++ reason ]
reportSDoc "tc.size.solve" 20 $ vcat $
[ text "Solving constraint cluster" ] ++ map prettyTCM cs
let HypSizeConstraint gamma hids hs _ = maximumBy (compare `on` (length . sizeContext)) cs
let n = size gamma
csL = for cs $ \ (HypSizeConstraint cxt _ _ c) -> raise (n size cxt) c
csC :: [SizeConstraint]
csC = applyWhen (null hs) (mapMaybe canonicalizeSizeConstraint) csL
reportSDoc "tc.size.solve" 30 $ vcat $
[ text "Canonicalized constraints" ] ++
map (prettyTCM . HypSizeConstraint gamma hids hs) csC
let metas :: [SizeMeta]
metas = concat $ map (foldMap (:[])) csC
csF :: [Size.Constraint' NamedRigid Int]
csF = map (fmap (metaId . sizeMetaId)) csC
let hyps = map (fmap (metaId . sizeMetaId)) hs
let hg = fromMaybe __IMPOSSIBLE__ $ hypGraph (rigids csF) hyps
g <- maybe (err "Inconsistent constraints") return $ constraintGraph csF hg
reportSDoc "tc.size.solve" 40 $ vcat $
[ text "Constraint graph"
, text (show g)
]
sol :: Solution NamedRigid Int <- either err return $ solveGraph Map.empty hg g
either err return $ verifySolution hg csF sol
forM_ (Map.assocs sol) $ \ (m, a) -> do
unless (validOffset a) __IMPOSSIBLE__
u <- unSizeExpr $ fmap __IMPOSSIBLE__ a
let x = MetaId m
let SizeMeta _ xs = fromMaybe __IMPOSSIBLE__ $ find ((m==) . metaId . sizeMetaId) metas
let ys = rigidIndex <$> Set.toList (rigids a)
ok = all (`elem` xs) ys
u <- if ok then return u else primSizeInf
t <- getMetaType x
reportSDoc "tc.size.solve" 20 $ inTopContext $ modifyContext (const gamma) $ do
text "solution " <+> prettyTCM (MetaV x []) <+> text " := " <+> prettyTCM u
assignMeta n x t xs u
getSizeHypotheses :: Context -> TCM [(CtxId, SizeConstraint)]
getSizeHypotheses gamma = inTopContext $ modifyContext (const gamma) $ do
(_, msizelt) <- getBuiltinSize
caseMaybe msizelt (return []) $ \ sizelt -> do
catMaybes <$> do
forM (zip [0..] gamma) $ \ (i, ce) -> do
let xt = unDom $ ctxEntry ce
x = show $ fst xt
t <- reduce . raise (1 + i) . unEl . snd $ xt
case ignoreSharing t of
Def d [Apply u] | d == sizelt -> do
caseMaybeM (sizeExpr $ unArg u) (return Nothing) $ \ a ->
return $ Just $ (ctxId ce, Constraint (Rigid (NamedRigid x i) 0) Lt a)
_ -> return Nothing
canonicalizeSizeConstraint :: SizeConstraint -> Maybe (SizeConstraint)
canonicalizeSizeConstraint c@(Constraint a cmp b) =
case (a,b) of
(Flex (SizeMeta m xs) n, Flex (SizeMeta l ys) n')
| Just ys' <- mapM (\ y -> findIndex (==y) xs) ys ->
return $ Constraint (Flex (SizeMeta m [0..size xs1]) n)
cmp (Flex (SizeMeta l ys') n')
| Just xs' <- mapM (\ x -> findIndex (==x) ys) xs ->
return $ Constraint (Flex (SizeMeta m xs') n)
cmp (Flex (SizeMeta l [0..size ys1]) n')
| otherwise -> Nothing
(Flex (SizeMeta m xs) n, Rigid (NamedRigid x i) n') -> do
j <- findIndex (==i) xs
return $ Constraint (Flex (SizeMeta m [0..size xs1]) n) cmp (Rigid (NamedRigid x j) n')
(Rigid (NamedRigid x i) n, Flex (SizeMeta m xs) n') -> do
j <- findIndex (==i) xs
return $ Constraint (Rigid (NamedRigid x j) n) cmp (Flex (SizeMeta m [0..size xs1]) n')
(Flex (SizeMeta m xs) n, _) ->
return $ Constraint (Flex (SizeMeta m [0..size xs1]) n) cmp b
(_, Flex (SizeMeta m xs) n') -> do
return $ Constraint a cmp (Flex (SizeMeta m [0..size xs1]) n')
_ -> return c
data NamedRigid = NamedRigid
{ rigidName :: String
, rigidIndex :: Int
}
instance Eq NamedRigid where (==) = (==) `on` rigidIndex
instance Ord NamedRigid where compare = compare `on` rigidIndex
instance Show NamedRigid where show = rigidName
instance Plus NamedRigid Int NamedRigid where
plus (NamedRigid x i) j = NamedRigid x (i + j)
data SizeMeta = SizeMeta
{ sizeMetaId :: MetaId
, sizeMetaArgs :: [Int]
}
instance Eq SizeMeta where (==) = (==) `on` sizeMetaId
instance Ord SizeMeta where compare = compare `on` sizeMetaId
instance PrettyTCM SizeMeta where
prettyTCM (SizeMeta x es) = prettyTCM (MetaV x $ map (Apply . defaultArg . var) es)
instance Subst SizeMeta where
applySubst sigma (SizeMeta x es) = SizeMeta x (map raise es)
where
raise i =
case lookupS sigma i of
Var j [] -> j
_ -> __IMPOSSIBLE__
type DBSizeExpr = SizeExpr' NamedRigid SizeMeta
instance Subst (SizeExpr' NamedRigid SizeMeta) where
applySubst sigma a =
case a of
Infty -> a
Const{} -> a
Flex x n -> Flex (applySubst sigma x) n
Rigid r n ->
case lookupS sigma $ rigidIndex r of
Var j [] -> Rigid r{ rigidIndex = j } n
_ -> __IMPOSSIBLE__
type SizeConstraint = Constraint' NamedRigid SizeMeta
instance Subst (SizeConstraint) where
applySubst sigma (Constraint a cmp b) =
Constraint (applySubst sigma a) cmp (applySubst sigma b)
instance PrettyTCM (SizeConstraint) where
prettyTCM (Constraint a cmp b) = do
u <- unSizeExpr a
v <- unSizeExpr b
prettyTCM u <+> text (show cmp) <+> prettyTCM v
data HypSizeConstraint = HypSizeConstraint
{ sizeContext :: Context
, sizeHypIds :: [CtxId]
, sizeHypotheses :: [SizeConstraint]
, sizeConstraint :: SizeConstraint
}
instance Flexs SizeMeta HypSizeConstraint where
flexs (HypSizeConstraint _ _ hs c) = flexs hs `mappend` flexs c
instance PrettyTCM HypSizeConstraint where
prettyTCM (HypSizeConstraint cxt _ hs c) =
inTopContext $ modifyContext (const cxt) $ do
applyUnless (null hs)
(((hcat $ punctuate (text ", ") $ map prettyTCM hs) <+> text "|-") <+>)
(prettyTCM c)
computeSizeConstraint :: Closure TCM.Constraint -> TCM (Maybe HypSizeConstraint)
computeSizeConstraint c = do
let cxt = envContext $ clEnv c
inTopContext $ modifyContext (const cxt) $ do
case clValue c of
ValueCmp CmpLeq _ u v -> do
reportSDoc "tc.size.solve" 50 $ sep $
[ text "converting size constraint"
, prettyTCM c
]
ma <- sizeExpr u
mb <- sizeExpr v
(hids, hs) <- unzip <$> getSizeHypotheses cxt
let mk a b = HypSizeConstraint cxt hids hs $ Size.Constraint a Le b
return $ mk <$> ma <*> mb
_ -> __IMPOSSIBLE__
sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
sizeExpr u = do
u <- reduce u
reportSDoc "tc.conv.size" 60 $ text "sizeExpr:" <+> prettyTCM u
s <- sizeView u
case s of
SizeInf -> return $ Just Infty
SizeSuc u -> fmap (`plus` (1 :: Int)) <$> sizeExpr u
OtherSize u -> case ignoreSharing u of
Var i [] -> (\ x -> Just $ Rigid (NamedRigid x i) 0) . show <$> nameOfBV i
MetaV m es | Just xs <- mapM isVar es, fastDistinct xs
-> return $ Just $ Flex (SizeMeta m xs) 0
_ -> return Nothing
where
isVar (Proj{}) = Nothing
isVar (Apply v) = case ignoreSharing $ unArg v of
Var i [] -> Just i
_ -> Nothing
unSizeExpr :: DBSizeExpr -> TCM Term
unSizeExpr a =
case a of
Infty -> primSizeInf
Rigid r n -> do
unless (n >= 0) __IMPOSSIBLE__
sizeSuc n $ var $ rigidIndex r
Flex (SizeMeta x es) n -> do
unless (n >= 0) __IMPOSSIBLE__
sizeSuc n $ MetaV x $ map (Apply . defaultArg . var) es
Const{} -> __IMPOSSIBLE__