module Agda.TypeChecking.Empty
  ( isEmptyType
  , isEmptyTel
  , ensureEmptyType
  , checkEmptyTel
  ) where

import Control.Monad.Except

import Data.Semigroup

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( fromSplitPatterns )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Either
import Agda.Utils.Monad

data ErrorNonEmpty
  = Fail              -- ^ Generic failure
  | FailBecause TCErr -- ^ Failure with informative error
  | DontKnow          -- ^ Emptyness check blocked

instance Semigroup ErrorNonEmpty where
  ErrorNonEmpty
DontKnow        <> :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
<> ErrorNonEmpty
_        = ErrorNonEmpty
DontKnow
  ErrorNonEmpty
_               <> ErrorNonEmpty
DontKnow = ErrorNonEmpty
DontKnow
  FailBecause TCErr
err <> ErrorNonEmpty
_        = TCErr -> ErrorNonEmpty
FailBecause TCErr
err
  ErrorNonEmpty
Fail            <> ErrorNonEmpty
err      = ErrorNonEmpty
err

instance Monoid ErrorNonEmpty where
  mempty :: ErrorNonEmpty
mempty  = ErrorNonEmpty
Fail
  mappend :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
mappend = ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
forall a. Semigroup a => a -> a -> a
(Data.Semigroup.<>)

-- | Ensure that a type is empty.
--   This check may be postponed as emptiness constraint.
ensureEmptyType
  :: Range -- ^ Range of the absurd pattern.
  -> Type  -- ^ Type that should be empty (empty data type or iterated product of such).
  -> TCM ()
ensureEmptyType :: Range -> Type -> TCM ()
ensureEmptyType Range
r Type
t = TCMT IO (Either ErrorNonEmpty ())
-> (ErrorNonEmpty -> TCM ()) -> (() -> TCM ()) -> TCM ()
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
r Type
t) ErrorNonEmpty -> TCM ()
forall (m :: * -> *). MonadConstraint m => ErrorNonEmpty -> m ()
failure () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return
  where
  failure :: ErrorNonEmpty -> m ()
failure ErrorNonEmpty
DontKnow          = Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Range -> Type -> Constraint
IsEmpty Range
r Type
t
  failure (FailBecause TCErr
err) = TCErr -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  failure ErrorNonEmpty
Fail              = TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> [DeBruijnPattern] -> TypeError
ShouldBeEmpty Type
t []

-- | Check whether a type is empty.
isEmptyType :: Type -> TCM Bool
isEmptyType :: Type -> TCM Bool
isEmptyType Type
ty = Either ErrorNonEmpty () -> Bool
forall a b. Either a b -> Bool
isRight (Either ErrorNonEmpty () -> Bool)
-> TCMT IO (Either ErrorNonEmpty ()) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
forall a. Range' a
noRange Type
ty

-- | Check whether some type in a telescope is empty.
isEmptyTel :: Telescope -> TCM Bool
isEmptyTel :: Telescope -> TCM Bool
isEmptyTel Telescope
tel = Either ErrorNonEmpty Int -> Bool
forall a b. Either a b -> Bool
isRight (Either ErrorNonEmpty Int -> Bool)
-> TCMT IO (Either ErrorNonEmpty Int) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
forall a. Range' a
noRange Telescope
tel

-- Either the type is possibly non-empty (Left err) or it is really empty
-- (Right ()).
checkEmptyType :: Range -> Type -> TCM (Either ErrorNonEmpty ())
checkEmptyType :: Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
range Type
t = do
  Either (Blocked Type) (QName, Args, Defn)
mr <- Type -> TCMT IO (Either (Blocked Type) (QName, Args, Defn))
forall (m :: * -> *).
(MonadReduce m, HasConstInfo m, HasBuiltins m) =>
Type -> m (Either (Blocked Type) (QName, Args, Defn))
tryRecordType Type
t
  case Either (Blocked Type) (QName, Args, Defn)
mr of

    -- If t is blocked or a meta, we cannot decide emptiness now.  Postpone.
    Left (Blocked MetaId
m Type
t) -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
-> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. a -> Either a b
Left ErrorNonEmpty
DontKnow

    -- If t is not a record type, try to split
    Left (NotBlocked NotBlocked
nb Type
t) -> do
      -- from the current context xs:ts, create a pattern list
      -- xs _ : ts t and try to split on _ (the last variable)
      Telescope
tel0 <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      let gamma :: [Dom (ArgName, Type)]
gamma = Telescope -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel0 [Dom (ArgName, Type)]
-> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a. [a] -> [a] -> [a]
++ [Arg (ArgName, Type) -> Dom (ArgName, Type)
forall a. Arg a -> Dom a
domFromArg (Arg (ArgName, Type) -> Dom (ArgName, Type))
-> Arg (ArgName, Type) -> Dom (ArgName, Type)
forall a b. (a -> b) -> a -> b
$ (ArgName, Type) -> Arg (ArgName, Type)
forall a. a -> Arg a
defaultArg (ArgName
forall a. Underscore a => a
underscore, Type
t)]
          tel :: Telescope
tel   = [Dom (ArgName, Type)] -> Telescope
telFromList [Dom (ArgName, Type)]
gamma
          ps :: [NamedArg DeBruijnPattern]
ps    = Telescope -> [NamedArg DeBruijnPattern]
forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
tel

      TCMT IO (Either ErrorNonEmpty ())
-> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCMT IO (Either ErrorNonEmpty ())
 -> TCMT IO (Either ErrorNonEmpty ()))
-> TCMT IO (Either ErrorNonEmpty ())
-> TCMT IO (Either ErrorNonEmpty ())
forall a b. (a -> b) -> a -> b
$ do
        Either SplitError Covering
r <- Induction
-> Telescope
-> [NamedArg DeBruijnPattern]
-> TCM (Either SplitError Covering)
splitLast Induction
Inductive Telescope
tel [NamedArg DeBruijnPattern]
ps
        case Either SplitError Covering
r of
          Left UnificationStuck{} -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
-> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. a -> Either a b
Left ErrorNonEmpty
DontKnow
          Left SplitError
_                  -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
-> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
          Right Covering
cov -> do
            let ps :: [DeBruijnPattern]
ps = (SplitClause -> DeBruijnPattern)
-> [SplitClause] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> (SplitClause -> NamedArg DeBruijnPattern)
-> SplitClause
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern
forall a. [a] -> a
last ([NamedArg DeBruijnPattern] -> NamedArg DeBruijnPattern)
-> (SplitClause -> [NamedArg DeBruijnPattern])
-> SplitClause
-> NamedArg DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns ([NamedArg SplitPattern] -> [NamedArg DeBruijnPattern])
-> (SplitClause -> [NamedArg SplitPattern])
-> SplitClause
-> [NamedArg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) ([SplitClause] -> [DeBruijnPattern])
-> [SplitClause] -> [DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov
            if ([DeBruijnPattern] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DeBruijnPattern]
ps) then Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either ErrorNonEmpty ()
forall a b. b -> Either a b
Right ()) else
              ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. a -> Either a b
Left (ErrorNonEmpty -> Either ErrorNonEmpty ())
-> (TCErr -> ErrorNonEmpty) -> TCErr -> Either ErrorNonEmpty ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> ErrorNonEmpty
FailBecause (TCErr -> Either ErrorNonEmpty ())
-> TCMT IO TCErr -> TCMT IO (Either ErrorNonEmpty ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TypeError -> TCMT IO TCErr
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
TypeError -> m TCErr
typeError_ (TypeError -> TCMT IO TCErr) -> TypeError -> TCMT IO TCErr
forall a b. (a -> b) -> a -> b
$ Type -> [DeBruijnPattern] -> TypeError
ShouldBeEmpty Type
t [DeBruijnPattern]
ps

    -- If t is a record type, see if any of the field types is empty
    Right (QName
r, Args
pars, Defn
def) -> do
      if Defn -> HasEta
recEtaEquality Defn
def HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
NoEta then Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ()))
-> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. a -> Either a b
Left ErrorNonEmpty
Fail else do
        Either ErrorNonEmpty Int -> Either ErrorNonEmpty ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either ErrorNonEmpty Int -> Either ErrorNonEmpty ())
-> TCMT IO (Either ErrorNonEmpty Int)
-> TCMT IO (Either ErrorNonEmpty ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Range -> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
range (Telescope -> TCMT IO (Either ErrorNonEmpty Int))
-> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ Defn -> Telescope
recTel Defn
def Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
`apply` Args
pars

-- | Check whether one of the types in the given telescope is constructor-less
--   and if yes, return its index in the telescope (0 = leftmost).
checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel :: Range -> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
r = Int -> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
forall b.
Enum b =>
b -> Telescope -> TCMT IO (Either ErrorNonEmpty b)
loop Int
0
  where
  loop :: b -> Telescope -> TCMT IO (Either ErrorNonEmpty b)
loop b
i Telescope
EmptyTel            = Either ErrorNonEmpty b -> TCMT IO (Either ErrorNonEmpty b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty b -> TCMT IO (Either ErrorNonEmpty b))
-> Either ErrorNonEmpty b -> TCMT IO (Either ErrorNonEmpty b)
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty b
forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
  loop b
i (ExtendTel Dom' Term Type
dom Abs Telescope
tel) = [TCMT IO (Either ErrorNonEmpty b)]
-> TCMT IO (Either ErrorNonEmpty b)
forall e (m :: * -> *) b.
(Monoid e, Monad m, Functor m) =>
[m (Either e b)] -> m (Either e b)
orEitherM
    [ (b
i b -> Either ErrorNonEmpty () -> Either ErrorNonEmpty b
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Either ErrorNonEmpty () -> Either ErrorNonEmpty b)
-> TCMT IO (Either ErrorNonEmpty ())
-> TCMT IO (Either ErrorNonEmpty b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Type -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
r (Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom Dom' Term Type
dom)
    , Dom' Term Type
-> Abs Telescope
-> (Telescope -> TCMT IO (Either ErrorNonEmpty b))
-> TCMT IO (Either ErrorNonEmpty b)
forall t a (m :: * -> *) b.
(Subst t a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term Type
dom Abs Telescope
tel ((Telescope -> TCMT IO (Either ErrorNonEmpty b))
 -> TCMT IO (Either ErrorNonEmpty b))
-> (Telescope -> TCMT IO (Either ErrorNonEmpty b))
-> TCMT IO (Either ErrorNonEmpty b)
forall a b. (a -> b) -> a -> b
$ b -> Telescope -> TCMT IO (Either ErrorNonEmpty b)
loop (b -> b
forall a. Enum a => a -> a
succ b
i)
    ]