module Agda.TypeChecking.Monad.SizedTypes where
import Control.Applicative
import Control.Monad.Error
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.Utils.Monad
isSizeType :: Type -> TCM Bool
isSizeType v = isSizeTypeTest <*> pure v
isSizeNameTest :: TCM (QName -> Bool)
isSizeNameTest = liftTCM $
ifM (not . optSizedTypes <$> pragmaOptions) (return $ const False) $ do
Def size [] <- primSize
return (size ==)
`catchError` \_ -> return $ const False
isSizeTypeTest :: TCM (Type -> Bool)
isSizeTypeTest = do
testName <- isSizeNameTest
let testType (El _ (Def d [])) = testName d
testType _ = False
return testType
sizeType :: TCM Type
sizeType = El (mkType 0) <$> primSize
sizeSuc :: TCM (Maybe QName)
sizeSuc = liftTCM $
ifM (not . optSizedTypes <$> pragmaOptions) (return Nothing) $ do
Def x [] <- primSizeSuc
return $ Just x
`catchError` \_ -> return Nothing
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 [u] | x == suc -> return $ SizeSuc (unArg u)
_ -> return $ OtherSize v
unSizeView :: SizeView -> TCM Term
unSizeView SizeInf = primSizeInf
unSizeView (SizeSuc v) = flip apply [Arg NotHidden Relevant v] <$> primSizeSuc
unSizeView (OtherSize v) = return v