{-# OPTIONS_GHC -Wunused-imports #-}

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.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty

import Agda.Utils.Either
import Agda.Utils.Functor        ( (<.>) )
import Agda.Syntax.Common.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__

-- | @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
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
c)
  Definition
cdef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
  let ctype :: Type
ctype = Definition -> Type
defType Definition
cdef
      cdata :: QName
cdata = Defn -> QName
conData forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef
      npars :: VerboseLevel
npars = Defn -> VerboseLevel
conPars forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef
  case forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
d [Elim]
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
cdata -> 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 ]
      Type
dt <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      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
npars [Elim]
es
      Type
ctPars <- Type
ctype forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((QName
d, Type
dt, Args
pars), Type
ctPars)
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- | Make sure a constructor is fully applied and infer the type of the constructor.
--   Raises a type error if the constructor does not belong to the given type.
fullyApplyCon
  :: (PureTCM m, MonadBlock m, MonadTCError m)
  => ConHead -- ^ Constructor.
  -> Elims    -- ^ Constructor arguments.
  -> Type    -- ^ Type of the constructor application.
  -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
       -- ^ Name of the data/record type,
       --   type of the data/record type,
       --   reconstructed parameters,
       --   type of the constructor (applied to parameters),
       --   full application arguments,
       --   types of missing arguments (already added to context),
       --   type of the full application.
  -> m a
fullyApplyCon :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m, MonadTCError m) =>
ConHead
-> [Elim]
-> Type
-> (QName
    -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> m a
fullyApplyCon ConHead
c [Elim]
vs Type
t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret = forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
    -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
c [Elim]
vs Type
t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Type -> TypeError
DoesNotConstructAnElementOf (ConHead -> QName
conName ConHead
c)

-- | Like @fullyApplyCon@, but calls the given fallback function if
--   it encounters something other than a datatype.
fullyApplyCon'
  :: (PureTCM m, MonadBlock m)
  => ConHead -- ^ Constructor.
  -> Elims    -- ^ Constructor arguments.
  -> Type    -- ^ Type of the constructor application.
  -> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a) -- ^ See @fullyApplyCon@
  -> (Type -> m a) -- ^ Fallback function
  -> m a
fullyApplyCon' :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
    -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
c [Elim]
vs Type
t0 QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret Type -> m a
err = 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
"fullyApplyCon': constructor "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
    , TCMT IO Doc
" with arguments"
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Elim]
vs
    , TCMT IO Doc
" at type "
    , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
    ]
  (TelV Telescope
tel Type
t, Boundary
boundary) <- forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundaryP Type
t0
  -- The type of the constructor application may still be a function
  -- type.  In this case, we introduce the domains @tel@ into the context
  -- and apply the constructor to these fresh variables.
  forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
    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
    Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
    forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe ((QName, Type, Args), Type)
Nothing -> Type -> m a
err Type
t
      Just ((QName
d, Type
dt, Args
pars), Type
a) ->
        QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret QName
d Type
dt Args
pars Type
a (forall a. Subst a => VerboseLevel -> a -> a
raise (forall a. Sized a => a -> VerboseLevel
size Telescope
tel) [Elim]
vs forall a. [a] -> [a] -> [a]
++ forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
tel Boundary
boundary) Telescope
tel Type
t

-- | @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, MonadBlock 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, MonadBlock m) =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getConType ConHead
ch Type
t = do
  let c :: QName
c = ConHead -> QName
conName ConHead
ch
  -- Optimization: if the constructor has no parameters, there
  -- is no need to reduce the type.
  Maybe VerboseLevel
npars <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
c
  if | Maybe VerboseLevel
npars forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just VerboseLevel
0 -> do
      Type
ctype <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
      QName
d  <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
      Type
dtype <- Definition -> Type
defType 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. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((QName
d,Type
dtype,[]),Type
ctype)
     | Bool
otherwise -> forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
    -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
ch [] Type
t
      (\QName
d Type
dt Args
pars Type
ct [Elim]
es Telescope
tel Type
a -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
        -- Now @dt@, @pars@, and @ct@ live under @tel@,
        -- so we need to remove the dependency on @tel@.
        let escape :: ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
escape = 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 Telescope
tel)) in
        forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
escape ((QName
d, Type
dt, Args
pars), Type
ct))
      (\Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)

data ConstructorInfo
  = DataCon Arity
      -- ^ Arity of the data constructor.
  | RecordCon PatternOrCopattern HasEta
      Arity
      -- ^ Arity of the record constructor.
      [Dom QName]
      -- ^ List of field names. Has length 'Arity'.

-- | Return the number of non-parameter arguments to a constructor (arity).
--   In case of record constructors, also return the field names (plus other info).
--
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 -> VerboseLevel -> [Dom QName] -> ConstructorInfo
RecordCon (Defn -> PatternOrCopattern
recPatternMatching Defn
r) (Defn -> HasEta
recEtaEquality Defn
r) VerboseLevel
n [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{ EtaEquality
recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality', 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 forall a b. (a -> b) -> a -> b
$
      case PatternOrCopattern
recPatternMatching of
        -- If the user explicitly asked for @pattern@, pattern matching is allowed.
        p :: PatternOrCopattern
p@PatternOrCopattern
PatternMatching -> PatternOrCopattern
p
        -- Otherwise, 'recEtaEquality' might allow pattern matching.
        PatternOrCopattern
CopatternMatching ->
          if forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed EtaEquality
recEtaEquality' then PatternOrCopattern
PatternMatching else PatternOrCopattern
CopatternMatching
    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, DataOrRecord))
isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
isDataOrRecord = \case
    Def QName
d [Elim]
_ -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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
  forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall a. LensModality a => a -> Bool
usableModality forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM [QName]
getConstructors QName
d

-- | 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