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

import Control.Monad        ( void )
import Control.Monad.Except ( MonadError(..) )

import Data.Semigroup
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
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.Reduce ( instantiateFull )
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

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

import Agda.Utils.Impossible

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

instance Semigroup ErrorNonEmpty where
  DontKnow Blocker
u1     <> :: ErrorNonEmpty -> ErrorNonEmpty -> ErrorNonEmpty
<> DontKnow Blocker
u2  = Blocker -> ErrorNonEmpty
DontKnow forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnBoth Blocker
u1 Blocker
u2  -- Both must unblock for this to proceed
  e :: ErrorNonEmpty
e@DontKnow{}    <> ErrorNonEmpty
_            = ErrorNonEmpty
e
  ErrorNonEmpty
_               <> e :: ErrorNonEmpty
e@DontKnow{} = ErrorNonEmpty
e
  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 = 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 = forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (Range -> Type -> TCM (Either ErrorNonEmpty ())
checkEmptyType Range
r Type
t) ErrorNonEmpty -> TCM ()
failure forall (m :: * -> *) a. Monad m => a -> m a
return
  where
  failure :: ErrorNonEmpty -> TCM ()
failure (DontKnow Blocker
u)      = forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
u forall a b. (a -> b) -> a -> b
$ Range -> Type -> Constraint
IsEmpty Range
r Type
t
  failure (FailBecause TCErr
err) = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  failure ErrorNonEmpty
Fail              = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError 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 = forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Type -> TCM (Either ErrorNonEmpty ())
checkEmptyType forall a. Range' a
noRange Type
ty

-- | Check whether some type in a telescope is empty.
isEmptyTel :: Telescope -> TCM Bool
isEmptyTel :: Tele (Dom' Term Type) -> TCM Bool
isEmptyTel Tele (Dom' Term Type)
tel = forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel forall a. Range' a
noRange Tele (Dom' Term Type)
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 -> TCM (Either ErrorNonEmpty ())
checkEmptyType Range
range Type
t = do
  Either (Blocked Type) (QName, Args, Defn)
mr <- forall (m :: * -> *).
PureTCM 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 Blocker
b Type
t) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (Blocker -> ErrorNonEmpty
DontKnow Blocker
b)

    -- If t is not a record type, try to split
    Left (NotBlocked NotBlocked' Term
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)
      Tele (Dom' Term Type)
tel0 <- forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom' Term Type))
getContextTelescope
      let gamma :: [Dom (ArgName, Type)]
gamma = forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom' Term Type)
tel0 forall a. [a] -> [a] -> [a]
++ [forall a. Arg a -> Dom a
domFromArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg (forall a. Underscore a => a
underscore, Type
t)]
          tel :: Tele (Dom' Term Type)
tel   = [Dom (ArgName, Type)] -> Tele (Dom' Term Type)
telFromList [Dom (ArgName, Type)]
gamma
          ps :: [NamedArg DeBruijnPattern]
ps    = forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom' Term Type)
tel

      forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ do
        Either SplitError Covering
r <- Induction
-> Tele (Dom' Term Type)
-> [NamedArg DeBruijnPattern]
-> TCM (Either SplitError Covering)
splitLast Induction
Inductive Tele (Dom' Term Type)
tel [NamedArg DeBruijnPattern]
ps
        case Either SplitError Covering
r of
          Left UnificationStuck{} -> do
            Blocker
blocker <- forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Tele (Dom' Term Type)
tel -- TODO Jesper: get proper blocking information from unification
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Blocker -> ErrorNonEmpty
DontKnow Blocker
blocker
          Left SplitError
_                  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
          Right Covering
cov -> do
            let ps :: [DeBruijnPattern]
ps = forall a b. (a -> b) -> [a] -> [b]
map (forall a. NamedArg a -> a
namedArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> a
lastWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov
            if (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DeBruijnPattern]
ps) then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right ()) else
              forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> ErrorNonEmpty
FailBecause forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *).
(HasCallStack, MonadTCEnv m, ReadTCState m) =>
TypeError -> m TCErr
typeError_ 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 | NoEta{} <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
         | Bool
otherwise -> forall (f :: * -> *) a. Functor f => f a -> f ()
void forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Range -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel Range
range forall a b. (a -> b) -> a -> b
$ Defn -> Tele (Dom' Term Type)
recTel Defn
def 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 -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel Range
r = Int -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
loop Int
0
  where
  loop :: Int -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
loop Int
i Tele (Dom' Term Type)
EmptyTel            = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
  loop Int
i (ExtendTel Dom' Term Type
dom Abs (Tele (Dom' Term Type))
tel) = forall e (m :: * -> *) b.
(Monoid e, Monad m, Functor m) =>
[m (Either e b)] -> m (Either e b)
orEitherM
    [ (Int
i forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> Type -> TCM (Either ErrorNonEmpty ())
checkEmptyType Range
r (forall t e. Dom' t e -> e
unDom Dom' Term Type
dom)
    , forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term Type
dom Abs (Tele (Dom' Term Type))
tel forall a b. (a -> b) -> a -> b
$ Int -> Tele (Dom' Term Type) -> TCM (Either ErrorNonEmpty Int)
loop (forall a. Enum a => a -> a
succ Int
i)
    ]