module Agda.TypeChecking.Datatypes where

import Control.Monad        ( filterM )
import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT )

import Data.Maybe (fromMaybe)

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty

import Agda.Utils.Either
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Constructors
---------------------------------------------------------------------------

-- | Get true constructor with record fields.
getConHead :: (HasConstInfo m) => QName -> m (Either SigError ConHead)
getConHead :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
  Definition
def <- forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c
  case Definition -> Defn
theDef Definition
def of
    Constructor { conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c' } -> forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Record     { recConHead :: Defn -> ConHead
recConHead = ConHead
c' } -> forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Defn
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Char] -> SigError
SigUnknown forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow QName
c forall a. [a] -> [a] -> [a]
++ [Char]
" is not a constructor"

isConstructor :: (HasConstInfo m) => QName -> m Bool
isConstructor :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isConstructor QName
q = forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
q

-- | Get true constructor with fields, expanding literals to constructors
--   if possible.
getConForm :: QName -> TCM (Either SigError ConHead)
getConForm :: QName -> TCM (Either SigError ConHead)
getConForm QName
c = forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left) forall a b. (a -> b) -> a -> b
$ \ ConHead
ch -> do
  Con ConHead
con ConInfo
_ [] <- forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
ch ConInfo
ConOCon [])
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ConHead
con

-- | Augment constructor with record fields (preserve constructor name).
--   The true constructor might only surface via 'reduce'.
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getOrigConHead QName
c = forall b d a. (b -> d) -> Either a b -> Either a d
mapRight (forall a. LensConName a => QName -> a -> a
setConName QName
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c

-- | Get the name of the datatype constructed by a given constructor.
--   Precondition: The argument must refer to a constructor
{-# SPECIALIZE getConstructorData :: QName -> TCM QName #-}
getConstructorData :: HasConstInfo m => QName -> m QName
getConstructorData :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c = do
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  case Definition -> Defn
theDef Definition
def of
    Constructor{conData :: Defn -> QName
conData = QName
d} -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
d
    Defn
_                        -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Is the datatype of this constructor a Higher Inductive Type?
--   Precondition: The argument must refer to a constructor of a datatype or record.
consOfHIT :: HasConstInfo m => QName -> m Bool
consOfHIT :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT QName
c = do
  QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Defn
def of
    Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
xs
    Record{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Defn
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__

isPathCons :: HasConstInfo m => QName -> m Bool
isPathCons :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
c = do
  QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Defn
def of
    Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
xs
    Record{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Defn
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @getConType c t@ computes the constructor parameters from type @t@
--   and returns them plus the instantiated type of constructor @c@.
--   This works also if @t@ is a function type ending in a data/record type;
--   the term from which @c@ comes need not be fully applied
--
--   @Nothing@ if @t@ is not a data/record type or does not have
--   a constructor @c@.
getConType
  :: PureTCM m
  => ConHead  -- ^ Constructor.
  -> Type     -- ^ Ending in data/record type.
  -> m (Maybe ((QName, Type, Args), Type))
       -- ^ @Nothing@ if not ends in data or record type.
       --
       --   @Just ((d, dt, pars), ct)@ otherwise, where
       --     @d@    is the data or record type name,
       --     @dt@   is the type of the data or record name,
       --     @pars@ are the reconstructed parameters,
       --     @ct@   is the type of the constructor instantiated to the parameters.
getConType :: forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getConType ConHead
c Type
t = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.getConType" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"getConType: constructor "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
    , TCMT IO Doc
" at type "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
    ]
  TelV Tele (Dom Type)
tel Type
t <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  -- Now @t@ lives under @tel@, we need to remove the dependency on @tel@.
  -- This will succeed if @t@ is indeed a data/record type that is the
  -- type of a constructor coming from a term
  -- (applied to at least the parameters).
  -- Note: @t@ will have some unbound deBruijn indices if view outside of @tel@.
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [Char]
"  target type: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t
  forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS HasCallStack => Impossible
impossible (forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
tel)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t
  -- Andreas, 2017-08-18, issue #2703:
  -- The original code
  --    getFullyAppliedConType c $ applySubst (strengthenS impossible (size tel)) t
  -- crashes because substitution into @Def@s is slightly too strict
  -- (see @defApp@ and @canProject@).
  -- Strengthening the parameters after the call to @getFullyAppliedConType@
  -- does not produce intermediate terms with __IMPOSSIBLE__s and this thus
  -- robust wrt. strictness/laziness of substitution.

-- | @getFullyAppliedConType c t@ computes the constructor parameters
--   from data type @t@ and returns them
--   plus the instantiated type of constructor @c@.
--
--   @Nothing@ if @t@ is not a data/record type or does not have
--   a constructor @c@.
--
--   Precondition: @t@ is reduced.
getFullyAppliedConType
  :: PureTCM m
  => ConHead  -- ^ Constructor.
  -> Type     -- ^ Reduced type of the fully applied constructor.
  -> m (Maybe ((QName, Type, Args), Type))
       -- ^ @Nothing@ if not data or record type.
       --
       --   @Just ((d, dt, pars), ct)@ otherwise, where
       --     @d@    is the data or record type name,
       --     @dt@   is the type of the data or record name,
       --     @pars@ are the reconstructed parameters,
       --     @ct@   is the type of the constructor instantiated to the parameters.
getFullyAppliedConType :: forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$
    [ [Char]
"getFullyAppliedConType", forall a. Pretty a => a -> [Char]
prettyShow ConHead
c, forall a. Pretty a => a -> [Char]
prettyShow Type
t ]
  ConHead
c <- forall a b. (a -> b) -> Either a b -> b
fromRight forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
  case forall t a. Type'' t a -> a
unEl Type
t of
    -- Note that if we come e.g. from getConType,
    -- then the non-parameter arguments of @es@ might contain __IMPOSSIBLE__
    -- coming from strengthening.  (Thus, printing them is not safe.)
    Def QName
d [Elim]
es -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$
        [ [Char]
"getFullyAppliedConType: case Def", forall a. Pretty a => a -> [Char]
prettyShow QName
d, forall a. Pretty a => a -> [Char]
prettyShow [Elim]
es ]
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      let cont :: VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
cont VerboseLevel
n = do
            -- At this point we can be sure that the parameters are well-scoped.
            let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall a b. (a -> b) -> a -> b
$ forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
n [Elim]
es
            forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName
d, Definition -> Type
defType Definition
def, Args
pars),) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              (forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
      case Definition -> Defn
theDef Definition
def of
        Datatype { dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
n, dataCons :: Defn -> [QName]
dataCons   = [QName]
cs  } | ConHead -> QName
conName ConHead
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
cs -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
cont VerboseLevel
n
        Record   { recPars :: Defn -> VerboseLevel
recPars  = VerboseLevel
n, recConHead :: Defn -> ConHead
recConHead = ConHead
con } | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
con            -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
cont VerboseLevel
n
        Defn
_ ->  forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

data ConstructorInfo
  = DataCon Nat
      -- ^ Arity.
  | RecordCon PatternOrCopattern HasEta [Dom QName]
      -- ^ List of field names.

-- | Return the number of non-parameter arguments to a data constructor,
--   or the field names of a record constructor.
--
--   For getting just the arity of constructor @c@,
--   use @either id size <$> getConstructorArity c@.
getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo :: forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo QName
c = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c

getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)
getConstructorInfo' :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c = do
  (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Constructor{ conData :: Defn -> QName
conData = QName
d, conArity :: Defn -> VerboseLevel
conArity = VerboseLevel
n } -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        r :: Defn
r@Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } ->
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> HasEta -> [Dom QName] -> ConstructorInfo
RecordCon (Defn -> PatternOrCopattern
recPatternMatching Defn
r) (Defn -> HasEta
recEtaEquality Defn
r) [Dom QName]
fs
        Datatype{} ->
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ConstructorInfo
DataCon VerboseLevel
n
        Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

---------------------------------------------------------------------------
-- * Data types
---------------------------------------------------------------------------

-- | Check if a name refers to a datatype or a record with a named constructor.
isDatatype :: QName -> TCM Bool
isDatatype :: QName -> TCM Bool
isDatatype QName
d = do
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Definition -> Defn
theDef Definition
def of
    Datatype{}                   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Record{recNamedCon :: Defn -> Bool
recNamedCon = Bool
namedC} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
namedC
    Defn
_                            -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Check if a name refers to a datatype or a record.
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d = do
  (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Record{ PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
recPatternMatching
    Datatype{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just DataOrRecord
IsData
    Defn
_          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing

-- | Precodition: 'Term' is 'reduce'd.
isDataOrRecord :: Term -> TCM (Maybe QName)
isDataOrRecord :: Term -> TCM (Maybe QName)
isDataOrRecord = \case
    Def QName
d [Elim]
_ -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const QName
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
    Term
_       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
getNumberOfParameters :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
d = do
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Definition -> Defn
theDef Definition
def of
    Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
n }   -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
    Record{ recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
n }      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
    Constructor{ conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
n } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
    Defn
_                          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- | This is a simplified version of @isDatatype@ from @Coverage@,
--   useful when we do not want to import the module.
getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))
getDatatypeArgs :: forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args, Args))
getDatatypeArgs Type
t = do
  case forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
d [Elim]
es -> do
      let ~(Just Args
args) = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      case Defn
def of
        Datatype{dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
np} -> do
          let !(Args
ps, Args
is) = forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
np Args
args
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
d,   Args
ps, Args
is)
        Record{} -> do
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
d, Args
args, [])
        Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

getNotErasedConstructors :: QName -> TCM [QName]
getNotErasedConstructors :: QName -> TCM [QName]
getNotErasedConstructors QName
d = do
  [QName]
cs <- QName -> TCM [QName]
getConstructors QName
d
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [QName]
cs forall a b. (a -> b) -> a -> b
$ \ QName
c -> do
    forall a. LensModality a => a -> Bool
usableModality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c

-- | Precondition: Name is a data or record type.
getConstructors :: QName -> TCM [QName]
getConstructors :: QName -> TCM [QName]
getConstructors QName
d = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  QName -> TCM (Maybe [QName])
getConstructors' QName
d

-- | 'Nothing' if not data or record type name.
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' QName
d = Defn -> Maybe [QName]
getConstructors_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d

-- | 'Nothing' if not data or record definition.
getConstructors_ :: Defn -> Maybe [QName]
getConstructors_ :: Defn -> Maybe [QName]
getConstructors_ = \case
    Datatype{dataCons :: Defn -> [QName]
dataCons = [QName]
cs} -> forall a. a -> Maybe a
Just [QName]
cs
    Record{recConHead :: Defn -> ConHead
recConHead = ConHead
h}  -> forall a. a -> Maybe a
Just [ConHead -> QName
conName ConHead
h]
    Defn
_                       -> forall a. Maybe a
Nothing