module Agda.TypeChecking.Monad.SizedTypes where
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 :: MonadTCM tcm => Type -> tcm Bool
isSizeType (El _ v) = liftTCM $
ifM (not . optSizedTypes <$> pragmaOptions) (return False) $
case v of
Def x [] -> do
Def size [] <- primSize
return $ x == size
_ -> return False
`catchError` \_ -> return False
sizeType :: MonadTCM tcm => tcm Type
sizeType = El (mkType 0) <$> primSize
sizeSuc :: MonadTCM tcm => 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 :: MonadTCM tcm => 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 :: MonadTCM tcm => SizeView -> tcm Term
unSizeView SizeInf = primSizeInf
unSizeView (SizeSuc v) = flip apply [Arg NotHidden Relevant v] <$> primSizeSuc
unSizeView (OtherSize v) = return v