    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

    -- | Check if a type is the 'primSize' type. The argument should be 'reduce'd.
    isSizeType :: MonadTCM tcm => Type -> tcm Bool
    isSizeType (El _ v) = liftTCM $
      ifM (not . optSizedTypes <$> commandLineOptions) (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 <$> commandLineOptions) (return Nothing) $ do
        Def x [] <- primSizeSuc
        return $ Just x
      `catchError` \_ -> return Nothing

    -- | A useful view on sizes.
    data SizeView = SizeInf | SizeSuc Term | OtherSize Term

    -- | Compute the size view of a term. The argument should be 'reduce'd.
    --   Precondition: sized types are enabled.
    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

    -- | Turn a size view into a term.
    unSizeView :: MonadTCM tcm => SizeView -> tcm Term
    unSizeView SizeInf       = primSizeInf
    unSizeView (SizeSuc v)   = flip apply [Arg NotHidden v] <$> primSizeSuc
    unSizeView (OtherSize v) = return v