{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.SizedTypes where
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute ()
import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
#include "undefined.h"
import Agda.Utils.Impossible
data BoundedSize
= BoundedLt Term
| BoundedNo
deriving (Eq, Show)
class IsSizeType a where
isSizeType :: a -> TCM (Maybe BoundedSize)
instance IsSizeType a => IsSizeType (Dom a) where
isSizeType = isSizeType . unDom
instance IsSizeType a => IsSizeType (b,a) where
isSizeType = isSizeType . snd
instance IsSizeType a => IsSizeType (Type' a) where
isSizeType = isSizeType . unEl
instance IsSizeType Term where
isSizeType v = isSizeTypeTest <*> pure v
isSizeTypeTest :: TCM (Term -> Maybe BoundedSize)
isSizeTypeTest =
flip (ifM (optSizedTypes <$> pragmaOptions)) (return $ const Nothing) $ do
(size, sizelt) <- getBuiltinSize
let testType (Def d []) | Just d == size = Just BoundedNo
testType (Def d [Apply v]) | Just d == sizelt = Just $ BoundedLt $ unArg v
testType _ = Nothing
return testType
getBuiltinDefName :: String -> TCM (Maybe QName)
getBuiltinDefName s = fromDef <$> getBuiltin' s
where
fromDef (Just (Def d [])) = Just d
fromDef _ = Nothing
getBuiltinSize :: TCM (Maybe QName, Maybe QName)
getBuiltinSize = do
size <- getBuiltinDefName builtinSize
sizelt <- getBuiltinDefName builtinSizeLt
return (size, sizelt)
isSizeNameTest :: TCM (QName -> Bool)
isSizeNameTest = ifM (optSizedTypes <$> pragmaOptions)
isSizeNameTestRaw
(return $ const False)
isSizeNameTestRaw :: TCM (QName -> Bool)
isSizeNameTestRaw = do
(size, sizelt) <- getBuiltinSize
return $ (`elem` [size, sizelt]) . Just
haveSizedTypes :: TCM Bool
haveSizedTypes = do
Def _ [] <- primSize
Def _ [] <- primSizeInf
Def _ [] <- primSizeSuc
optSizedTypes <$> pragmaOptions
`catchError` \_ -> return False
haveSizeLt :: TCM Bool
haveSizeLt = isJust <$> getBuiltinDefName builtinSizeLt
builtinSizeHook :: String -> QName -> Type -> TCM ()
builtinSizeHook s q 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])
sizeSort :: Sort
sizeSort = mkType 0
sizeUniv :: Type
sizeUniv = sort $ sizeSort
sizeType_ :: QName -> Type
sizeType_ size = El sizeSort $ Def size []
sizeType :: TCM Type
sizeType = El sizeSort <$> primSize
sizeSucName :: TCM (Maybe QName)
sizeSucName = do
ifM (not . optSizedTypes <$> pragmaOptions) (return Nothing) $ tryMaybe $ do
Def x [] <- primSizeSuc
return x
sizeSuc :: Nat -> Term -> TCM Term
sizeSuc n v | n < 0 = __IMPOSSIBLE__
| n == 0 = return v
| otherwise = do
Def suc [] <- primSizeSuc
return $ case iterate (sizeSuc_ suc) v !!! n of
Nothing -> __IMPOSSIBLE__
Just t -> t
sizeSuc_ :: QName -> Term -> Term
sizeSuc_ suc v = Def suc [Apply $ defaultArg v]
sizeMax :: [Term] -> TCM Term
sizeMax vs = case vs of
[] -> __IMPOSSIBLE__
[v] -> return v
vs -> do
Def max [] <- primSizeMax
return $ foldr1 (\ u v -> Def max $ map (Apply . defaultArg) [u,v]) vs
data SizeView = SizeInf | SizeSuc Term | OtherSize Term
sizeView :: Term -> TCM SizeView
sizeView v = do
Def inf [] <- primSizeInf
Def suc [] <- primSizeSuc
case v of
Def x [] | x == inf -> return SizeInf
Def x [Apply u] | x == suc -> return $ SizeSuc (unArg u)
_ -> return $ OtherSize v
type Offset = Nat
data DeepSizeView
= DSizeInf
| DSizeVar Nat Offset
| DSizeMeta MetaId Elims Offset
| DOtherSize Term
deriving (Show)
data SizeViewComparable a
= NotComparable
| YesAbove DeepSizeView a
| YesBelow DeepSizeView a
deriving (Functor)
sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewComparable v w = case (v,w) of
(DSizeInf, _) -> YesAbove w ()
(_, DSizeInf) -> YesBelow w ()
(DSizeVar x n, DSizeVar y m) | x == y -> if n >= m then YesAbove w () else YesBelow w ()
_ -> NotComparable
sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ suc v = case v of
DSizeInf -> DSizeInf
DSizeVar i n -> DSizeVar i (n + 1)
DSizeMeta x vs n -> DSizeMeta x vs (n + 1)
DOtherSize u -> DOtherSize $ sizeSuc_ suc u
sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView
sizeViewPred 0 v = v
sizeViewPred k v = case v of
DSizeInf -> DSizeInf
DSizeVar i n | n >= k -> DSizeVar i (n - k)
DSizeMeta x vs n | n >= k -> DSizeMeta x vs (n - k)
_ -> __IMPOSSIBLE__
sizeViewOffset :: DeepSizeView -> Maybe Offset
sizeViewOffset v = case v of
DSizeInf -> Nothing
DSizeVar i n -> Just n
DSizeMeta x vs n -> Just n
DOtherSize u -> Just 0
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (v, w) = (sizeViewPred k v, sizeViewPred k w)
where k = case (sizeViewOffset v, sizeViewOffset w) of
(Just n, Just m) -> min n m
(Just n, Nothing) -> n
(Nothing, Just m) -> m
(Nothing, Nothing) -> 0
unSizeView :: SizeView -> TCM Term
unSizeView SizeInf = primSizeInf
unSizeView (SizeSuc v) = sizeSuc 1 v
unSizeView (OtherSize v) = return v
unDeepSizeView :: DeepSizeView -> TCM Term
unDeepSizeView v = case v of
DSizeInf -> primSizeInf
DSizeVar i n -> sizeSuc n $ var i
DSizeMeta x us n -> sizeSuc n $ MetaV x us
DOtherSize u -> return u
type SizeMaxView = [DeepSizeView]
maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax v w = case (v,w) of
(DSizeInf : _, _) -> [DSizeInf]
(_, DSizeInf : _) -> [DSizeInf]
_ -> foldr maxViewCons w v
maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
maxViewCons _ [DSizeInf] = [DSizeInf]
maxViewCons DSizeInf _ = [DSizeInf]
maxViewCons v ws = case sizeViewComparableWithMax v ws of
NotComparable -> v:ws
YesAbove _ ws' -> v:ws'
YesBelow{} -> ws
sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView
sizeViewComparableWithMax v ws = case ws of
[] -> __IMPOSSIBLE__
[w] -> fmap (const []) $ sizeViewComparable v w
(w:ws) -> case sizeViewComparable v w of
NotComparable -> fmap (w:) $ sizeViewComparableWithMax v ws
r -> fmap (const ws) r
maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ suc = map (sizeViewSuc_ suc)
unMaxView :: SizeMaxView -> TCM Term
unMaxView vs = sizeMax =<< mapM unDeepSizeView vs