{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Monad.SizedTypes where
import qualified Data.Foldable as Fold
import qualified Data.Traversable as Trav
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
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty
import Agda.Utils.Singleton
#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 sizedTypesOption) (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 sizedTypesOption
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
sizedTypesOption
`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 <$> sizedTypesOption) (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 :: NonemptyList Term -> TCM Term
sizeMax vs = case vs of
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)
instance Pretty DeepSizeView where
pretty = \case
DSizeInf -> "∞"
DSizeVar n o -> text ("@" ++ show n) <+> "+" <+> pretty o
DSizeMeta x es o -> pretty (MetaV x es) <+> "+" <+> pretty o
DOtherSize t -> pretty t
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 = NonemptyList DeepSizeView
type SizeMaxView' = [DeepSizeView]
maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax v w = case (v,w) of
(DSizeInf :! _, _) -> singleton DSizeInf
(_, DSizeInf :! _) -> singleton DSizeInf
_ -> Fold.foldr maxViewCons w v
maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
maxViewCons _ (DSizeInf :! _) = singleton DSizeInf
maxViewCons DSizeInf _ = singleton DSizeInf
maxViewCons v ws = case sizeViewComparableWithMax v ws of
NotComparable -> consNe v ws
YesAbove _ ws' -> v :! ws'
YesBelow{} -> ws
sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView'
sizeViewComparableWithMax v (w :! ws) =
case (ws, sizeViewComparable v w) of
(w':ws', NotComparable) -> fmap (w:) $ sizeViewComparableWithMax v (w' :! ws')
(ws , r) -> fmap (const ws) r
maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ suc = fmap (sizeViewSuc_ suc)
unMaxView :: SizeMaxView -> TCM Term
unMaxView vs = sizeMax =<< Trav.mapM unDeepSizeView vs