{-# OPTIONS_GHC -Wunused-imports #-}

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

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

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.SplitPattern ( 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

-- | 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'' Term Term -> TCM ()
ensureEmptyType Range
r Type'' Term Term
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'' Term Term -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
r Type'' Term Term
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'' Term Term -> Constraint
IsEmpty Range
r Type'' Term Term
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'' Term Term -> [DeBruijnPattern] -> TypeError
ShouldBeEmpty Type'' Term Term
t []

-- | Check whether a type is empty.
isEmptyType :: MonadTCM tcm => Type -> tcm Bool
isEmptyType :: forall (tcm :: * -> *).
MonadTCM tcm =>
Type'' Term Term -> tcm Bool
isEmptyType Type'' Term Term
ty = TCM Bool -> tcm Bool
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
forall a b. (a -> b) -> a -> b
$ 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'' Term Term -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
forall a. Range' a
noRange Type'' Term Term
ty

-- | Check whether some type in a telescope is empty.
isEmptyTel :: MonadTCM tcm => Telescope -> tcm Bool
isEmptyTel :: forall (tcm :: * -> *).
MonadTCM tcm =>
Tele (Dom' Term (Type'' Term Term)) -> tcm Bool
isEmptyTel Tele (Dom' Term (Type'' Term Term))
tel = TCM Bool -> tcm Bool
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Bool -> tcm Bool) -> TCM Bool -> tcm Bool
forall a b. (a -> b) -> a -> b
$ 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'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
forall a. Range' a
noRange Tele (Dom' Term (Type'' Term Term))
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'' Term Term -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
range Type'' Term Term
t = do
  mr <- Type'' Term Term
-> TCMT
     IO (Either (Blocked (Type'' Term Term)) (QName, Args, RecordData))
forall (m :: * -> *).
(HasCallStack, PureTCM m) =>
Type'' Term Term
-> m (Either
        (Blocked (Type'' Term Term)) (QName, Args, RecordData))
tryRecordType Type'' Term Term
t
  case mr of

    -- If t is blocked or a meta, we cannot decide emptiness now.  Postpone.
    Left (Blocked Blocker
b Type'' Term Term
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'' Term Term
t) -> do
      -- from the current context xs:ts, create a pattern list
      -- xs _ : ts t and try to split on _ (the last variable)
      tel0 <- TCMT IO (Tele (Dom' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
getContextTelescope
      let gamma = Tele (Dom' Term (Type'' Term Term))
-> [Dom ([Char], Type'' Term Term)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom' Term (Type'' Term Term))
tel0 [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
-> [Dom ([Char], Type'' Term Term)]
forall a. [a] -> [a] -> [a]
++ [Arg ([Char], Type'' Term Term) -> Dom ([Char], Type'' Term Term)
forall a. Arg a -> Dom a
domFromArg (Arg ([Char], Type'' Term Term) -> Dom ([Char], Type'' Term Term))
-> Arg ([Char], Type'' Term Term) -> Dom ([Char], Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ ([Char], Type'' Term Term) -> Arg ([Char], Type'' Term Term)
forall a. a -> Arg a
defaultArg ([Char]
forall a. Underscore a => a
underscore, Type'' Term Term
t)]
          tel   = [Dom ([Char], Type'' Term Term)]
-> Tele (Dom' Term (Type'' Term Term))
telFromList [Dom ([Char], Type'' Term Term)]
gamma
          ps    = Tele (Dom' Term (Type'' Term Term)) -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom' Term (Type'' Term Term))
tel

      dontAssignMetas $ do
        r <- splitLast Inductive tel ps
        case r of
          Left UnificationStuck{} -> do
            blocker <- Tele (Dom' Term (Type'' Term Term)) -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn (Tele (Dom' Term (Type'' Term Term)) -> Blocker)
-> TCMT IO (Tele (Dom' Term (Type'' Term Term))) -> TCMT IO Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO (Tele (Dom' Term (Type'' Term Term)))
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Tele (Dom' Term (Type'' Term Term))
tel -- TODO Jesper: get proper blocking information from unification
            return $ Left $ DontKnow 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'' Term Term -> [DeBruijnPattern] -> TypeError
ShouldBeEmpty Type'' Term Term
t [DeBruijnPattern]
ps

    -- If t is a record type, see if any of the field types is empty
    Right (QName
r, Args
pars, RecordData
def) -> do
      if Bool -> Bool
not (RecordData -> Bool
isEtaRecordDef RecordData
def) then 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 else
         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'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
range (Tele (Dom' Term (Type'' Term Term))
 -> TCMT IO (Either ErrorNonEmpty Int))
-> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ RecordData -> Tele (Dom' Term (Type'' Term Term))
_recTel RecordData
def Tele (Dom' Term (Type'' Term Term))
-> Args -> Tele (Dom' Term (Type'' Term Term))
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'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
r = Int
-> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
loop Int
0
  where
  loop :: Int
-> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
loop Int
i Tele (Dom' Term (Type'' Term Term))
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'' Term Term)
dom Abs (Tele (Dom' Term (Type'' Term Term)))
tel) = [TCMT IO (Either ErrorNonEmpty Int)]
-> TCMT IO (Either ErrorNonEmpty Int)
forall e (m :: * -> *) b.
(Monoid e, Monad 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'' Term Term -> TCMT IO (Either ErrorNonEmpty ())
checkEmptyType Range
r (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
dom)
    , Dom' Term (Type'' Term Term)
-> Abs (Tele (Dom' Term (Type'' Term Term)))
-> (Tele (Dom' Term (Type'' Term Term))
    -> TCMT IO (Either ErrorNonEmpty Int))
-> TCMT IO (Either ErrorNonEmpty Int)
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstraction Dom' Term (Type'' Term Term)
dom Abs (Tele (Dom' Term (Type'' Term Term)))
tel ((Tele (Dom' Term (Type'' Term Term))
  -> TCMT IO (Either ErrorNonEmpty Int))
 -> TCMT IO (Either ErrorNonEmpty Int))
-> (Tele (Dom' Term (Type'' Term Term))
    -> TCMT IO (Either ErrorNonEmpty Int))
-> TCMT IO (Either ErrorNonEmpty Int)
forall a b. (a -> b) -> a -> b
$ Int
-> Tele (Dom' Term (Type'' Term Term))
-> TCMT IO (Either ErrorNonEmpty Int)
loop (Int -> Int
forall a. Enum a => a -> a
succ Int
i)
    ]