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 (Blocker -> ErrorNonEmpty) -> Blocker -> ErrorNonEmpty
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 = 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 ()
failure () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
  where
  failure :: ErrorNonEmpty -> TCM ()
failure (DontKnow Blocker
u)      = Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
u (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Range -> Type -> Constraint
IsEmpty Range
r Type
t
  failure (FailBecause TCErr
err) = TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  failure ErrorNonEmpty
Fail              = TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
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 :: Tele (Dom' Term Type) -> TCM Bool
isEmptyTel Tele (Dom' Term Type)
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
-> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
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 -> 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 :: * -> *).
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) -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a. a -> TCMT IO a
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 (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 <- TCMT IO (Tele (Dom' Term Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom' Term Type))
getContextTelescope
      let gamma :: [Dom (ArgName, Type)]
gamma = Tele (Dom' Term Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom' Term Type)
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 :: Tele (Dom' Term Type)
tel   = [Dom (ArgName, Type)] -> Tele (Dom' Term Type)
telFromList [Dom (ArgName, Type)]
gamma
          ps :: [NamedArg DeBruijnPattern]
ps    = Tele (Dom' Term Type) -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom' Term Type)
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
-> 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 <- Tele (Dom' Term Type) -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn (Tele (Dom' Term Type) -> Blocker)
-> TCMT IO (Tele (Dom' Term Type)) -> TCMT IO Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom' Term Type) -> TCMT IO (Tele (Dom' Term Type))
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Tele (Dom' Term Type)
tel -- TODO Jesper: get proper blocking information from unification
            Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a. a -> TCMT IO a
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 -> Either ErrorNonEmpty ())
-> ErrorNonEmpty -> Either ErrorNonEmpty ()
forall a b. (a -> b) -> a -> b
$ Blocker -> ErrorNonEmpty
DontKnow Blocker
blocker
          Left SplitError
_                  -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a. a -> TCMT IO a
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] -> NamedArg DeBruijnPattern
forall a. a -> [a] -> a
lastWithDefault NamedArg DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__ ([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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DeBruijnPattern]
ps) then Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a. a -> TCMT IO a
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 :: * -> *).
(HasCallStack, 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 | NoEta{} <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
def -> Either ErrorNonEmpty () -> TCMT IO (Either ErrorNonEmpty ())
forall a. a -> TCMT IO a
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
         | Bool
otherwise -> 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
-> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
range (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
-> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ Defn -> Tele (Dom' Term Type)
recTel Defn
def Tele (Dom' Term Type) -> Args -> Tele (Dom' Term Type)
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) -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
r = Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
loop Int
0
  where
  loop :: Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
loop Int
i Tele (Dom' Term Type)
EmptyTel            = Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int))
-> Either ErrorNonEmpty Int -> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ ErrorNonEmpty -> Either ErrorNonEmpty Int
forall a b. a -> Either a b
Left ErrorNonEmpty
Fail
  loop Int
i (ExtendTel Dom' Term Type
dom Abs (Tele (Dom' Term Type))
tel) = [TCMT IO (Either ErrorNonEmpty Int)]
-> TCMT IO (Either ErrorNonEmpty Int)
forall e (m :: * -> *) b.
(Monoid e, Monad m, Functor m) =>
[m (Either e b)] -> m (Either e b)
orEitherM
    [ (Int
i Int -> Either ErrorNonEmpty () -> Either ErrorNonEmpty Int
forall a b. a -> Either ErrorNonEmpty b -> Either ErrorNonEmpty a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Either ErrorNonEmpty () -> Either ErrorNonEmpty Int)
-> TCMT IO (Either ErrorNonEmpty ())
-> TCMT IO (Either ErrorNonEmpty Int)
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 (Tele (Dom' Term Type))
-> (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
-> TCMT IO (Either ErrorNonEmpty Int)
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 ((Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
 -> TCMT IO (Either ErrorNonEmpty Int))
-> (Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int))
-> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ Int -> Tele (Dom' Term Type) -> TCMT IO (Either ErrorNonEmpty Int)
loop (Int -> Int
forall a. Enum a => a -> a
succ Int
i)
    ]