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 = ExceptT SigError m ConHead -> m (Either SigError ConHead)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT SigError m ConHead -> m (Either SigError ConHead))
-> ExceptT SigError m ConHead -> m (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ do
  Definition
def <- m (Either SigError Definition) -> ExceptT SigError m Definition
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either SigError Definition) -> ExceptT SigError m Definition)
-> m (Either SigError Definition) -> ExceptT SigError m Definition
forall a b. (a -> b) -> a -> b
$ QName -> m (Either SigError Definition)
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' } -> ConHead -> ExceptT SigError m ConHead
forall a. a -> ExceptT SigError m a
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Record     { recConHead :: Defn -> ConHead
recConHead = ConHead
c' } -> ConHead -> ExceptT SigError m ConHead
forall a. a -> ExceptT SigError m a
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Defn
_ -> SigError -> ExceptT SigError m ConHead
forall a. SigError -> ExceptT SigError m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SigError -> ExceptT SigError m ConHead)
-> SigError -> ExceptT SigError m ConHead
forall a b. (a -> b) -> a -> b
$ [Char] -> SigError
SigUnknown ([Char] -> SigError) -> [Char] -> SigError
forall a b. (a -> b) -> a -> b
$ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
c [Char] -> [Char] -> [Char]
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 = Either SigError ConHead -> Bool
forall a b. Either a b -> Bool
isRight (Either SigError ConHead -> Bool)
-> m (Either SigError ConHead) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Either SigError ConHead)
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 = TCM (Either SigError ConHead)
-> (SigError -> TCM (Either SigError ConHead))
-> (ConHead -> TCM (Either SigError ConHead))
-> TCM (Either SigError ConHead)
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (QName -> TCM (Either SigError ConHead)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c) (Either SigError ConHead -> TCM (Either SigError ConHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError ConHead -> TCM (Either SigError ConHead))
-> (SigError -> Either SigError ConHead)
-> SigError
-> TCM (Either SigError ConHead)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SigError -> Either SigError ConHead
forall a b. a -> Either a b
Left) ((ConHead -> TCM (Either SigError ConHead))
 -> TCM (Either SigError ConHead))
-> (ConHead -> TCM (Either SigError ConHead))
-> TCM (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ \ ConHead
ch -> do
  Con ConHead
con ConInfo
_ [] <- Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
ch ConInfo
ConOCon [])
  Either SigError ConHead -> TCM (Either SigError ConHead)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError ConHead -> TCM (Either SigError ConHead))
-> Either SigError ConHead -> TCM (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ ConHead -> Either SigError ConHead
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 = (ConHead -> ConHead)
-> Either SigError ConHead -> Either SigError ConHead
forall b d a. (b -> d) -> Either a b -> Either a d
mapRight (QName -> ConHead -> ConHead
forall a. LensConName a => QName -> a -> a
setConName QName
c) (Either SigError ConHead -> Either SigError ConHead)
-> TCM (Either SigError ConHead) -> TCM (Either SigError ConHead)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Either SigError ConHead)
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 <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  case Definition -> Defn
theDef Definition
def of
    Constructor{conData :: Defn -> QName
conData = QName
d} -> QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
d
    Defn
_                        -> m QName
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 <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Defn
def of
    Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
xs
    Record{} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Defn
_  -> m Bool
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 <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Defn
def of
    Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ QName
c QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
xs
    Record{} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Defn
_  -> m Bool
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
  [Char] -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.getConType" VerboseLevel
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"getConType: constructor "
    , ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
    , TCMT IO Doc
" at type "
    , Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
    ]
  TelV Tele (Dom Type)
tel Type
t <- Type -> m (TelV Type)
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@.
  [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  target type: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t
  Substitution' (SubstArg (Maybe ((QName, Type, Args), Type)))
-> Maybe ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> VerboseLevel -> Substitution' Term
forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible (Tele (Dom Type) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom Type)
tel)) (Maybe ((QName, Type, Args), Type)
 -> Maybe ((QName, Type, Args), Type))
-> m (Maybe ((QName, Type, Args), Type))
-> m (Maybe ((QName, Type, Args), Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    Tele (Dom Type)
-> m (Maybe ((QName, Type, Args), Type))
-> m (Maybe ((QName, Type, Args), Type))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
tel (m (Maybe ((QName, Type, Args), Type))
 -> m (Maybe ((QName, Type, Args), Type)))
-> m (Maybe ((QName, Type, Args), Type))
-> m (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
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
  [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [ [Char]
"getFullyAppliedConType", ConHead -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow ConHead
c, Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t ]
  ConHead
c <- (SigError -> ConHead) -> Either SigError ConHead -> ConHead
forall a b. (a -> b) -> Either a b -> b
fromRight SigError -> ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__ (Either SigError ConHead -> ConHead)
-> m (Either SigError ConHead) -> m ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do QName -> m (Either SigError ConHead)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (QName -> m (Either SigError ConHead))
-> QName -> m (Either SigError ConHead)
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
  case Type -> Term
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
      [Char] -> VerboseLevel -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
        [ [Char]
"getFullyAppliedConType: case Def", QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
d, [Elim] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Elim]
es ]
      Definition
def <- QName -> m Definition
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 = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ [Elim] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims ([Elim] -> Maybe Args) -> [Elim] -> Maybe Args
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Elim] -> [Elim]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
n [Elim]
es
            ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
forall a. a -> Maybe a
Just (((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type))
-> (Type -> ((QName, Type, Args), Type))
-> Type
-> Maybe ((QName, Type, Args), Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName
d, Definition -> Type
defType Definition
def, Args
pars),) (Type -> Maybe ((QName, Type, Args), Type))
-> m Type -> m (Maybe ((QName, Type, Args), Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              (Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
`piApplyM` Args
pars) (Type -> m Type) -> (Definition -> Type) -> Definition -> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> m Type) -> m Definition -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConHead -> m Definition
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 QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
con            -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
cont VerboseLevel
n
        Defn
_ ->  Maybe ((QName, Type, Args), Type)
-> m (Maybe ((QName, Type, Args), Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ((QName, Type, Args), Type)
forall a. Maybe a
Nothing
    Term
_ -> Maybe ((QName, Type, Args), Type)
-> m (Maybe ((QName, Type, Args), Type))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ((QName, Type, Args), Type)
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 = ConstructorInfo -> Maybe ConstructorInfo -> ConstructorInfo
forall a. a -> Maybe a -> a
fromMaybe ConstructorInfo
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ConstructorInfo -> ConstructorInfo)
-> m (Maybe ConstructorInfo) -> m ConstructorInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe ConstructorInfo)
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 (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c) m Defn
-> (Defn -> m (Maybe ConstructorInfo)) -> m (Maybe ConstructorInfo)
forall a b. m a -> (a -> m b) -> m b
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 } -> ConstructorInfo -> Maybe ConstructorInfo
forall a. a -> Maybe a
Just (ConstructorInfo -> Maybe ConstructorInfo)
-> m ConstructorInfo -> m (Maybe ConstructorInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      (Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) m Defn -> (Defn -> m ConstructorInfo) -> m ConstructorInfo
forall a b. m a -> (a -> m b) -> m b
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 } ->
           ConstructorInfo -> m ConstructorInfo
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstructorInfo -> m ConstructorInfo)
-> ConstructorInfo -> m ConstructorInfo
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{} ->
           ConstructorInfo -> m ConstructorInfo
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstructorInfo -> m ConstructorInfo)
-> ConstructorInfo -> m ConstructorInfo
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ConstructorInfo
DataCon VerboseLevel
n
        Defn
_ -> m ConstructorInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> Maybe ConstructorInfo -> m (Maybe ConstructorInfo)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ConstructorInfo
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 <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Definition -> Defn
theDef Definition
def of
    Datatype{}                   -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Record{recNamedCon :: Defn -> Bool
recNamedCon = Bool
namedC} -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
namedC
    Defn
_                            -> Bool -> TCM Bool
forall a. a -> TCMT IO a
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 (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) TCMT IO Defn
-> (Defn -> TCM (Maybe DataOrRecord)) -> TCM (Maybe DataOrRecord)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Record{ PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching } -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
-> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a b. (a -> b) -> a -> b
$ DataOrRecord -> Maybe DataOrRecord
forall a. a -> Maybe a
Just (DataOrRecord -> Maybe DataOrRecord)
-> DataOrRecord -> Maybe DataOrRecord
forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> DataOrRecord
IsRecord PatternOrCopattern
recPatternMatching
    Datatype{} -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
-> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a b. (a -> b) -> a -> b
$ DataOrRecord -> Maybe DataOrRecord
forall a. a -> Maybe a
Just DataOrRecord
IsData
    Defn
_          -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DataOrRecord -> TCM (Maybe DataOrRecord))
-> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
forall a b. (a -> b) -> a -> b
$ Maybe DataOrRecord
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]
_ -> (DataOrRecord -> QName) -> Maybe DataOrRecord -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> DataOrRecord -> QName
forall a b. a -> b -> a
const QName
d) (Maybe DataOrRecord -> Maybe QName)
-> TCM (Maybe DataOrRecord) -> TCM (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
    Term
_       -> Maybe QName -> TCM (Maybe QName)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
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 <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Definition -> Defn
theDef Definition
def of
    Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
n }   -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
-> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n
    Record{ recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
n }      -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
-> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n
    Constructor{ conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
n } -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> m (Maybe VerboseLevel))
-> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n
    Defn
_                          -> Maybe VerboseLevel -> m (Maybe VerboseLevel)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe VerboseLevel
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 Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
d [Elim]
es -> do
      let ~(Just Args
args) = [Elim] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es
      Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
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) = VerboseLevel -> Args -> (Args, Args)
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
np Args
args
          Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args)))
-> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a b. (a -> b) -> a -> b
$ (QName, Args, Args) -> Maybe (QName, Args, Args)
forall a. a -> Maybe a
Just (QName
d,   Args
ps, Args
is)
        Record{} -> do
          Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args)))
-> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a b. (a -> b) -> a -> b
$ (QName, Args, Args) -> Maybe (QName, Args, Args)
forall a. a -> Maybe a
Just (QName
d, Args
args, [])
        Defn
_ -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, Args)
forall a. Maybe a
Nothing
    Term
_ -> Maybe (QName, Args, Args) -> m (Maybe (QName, Args, Args))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Args, Args)
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
  ((QName -> TCM Bool) -> [QName] -> TCM [QName])
-> [QName] -> (QName -> TCM Bool) -> TCM [QName]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (QName -> TCM Bool) -> [QName] -> TCM [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [QName]
cs ((QName -> TCM Bool) -> TCM [QName])
-> (QName -> TCM Bool) -> TCM [QName]
forall a b. (a -> b) -> a -> b
$ \ QName
c -> do
    Definition -> Bool
forall a. LensModality a => a -> Bool
usableModality (Definition -> Bool) -> TCMT IO Definition -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
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 = [QName] -> Maybe [QName] -> [QName]
forall a. a -> Maybe a -> a
fromMaybe [QName]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [QName] -> [QName])
-> TCMT IO (Maybe [QName]) -> TCM [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  QName -> TCMT IO (Maybe [QName])
getConstructors' QName
d

-- | 'Nothing' if not data or record type name.
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' :: QName -> TCMT IO (Maybe [QName])
getConstructors' QName
d = Defn -> Maybe [QName]
getConstructors_ (Defn -> Maybe [QName])
-> (Definition -> Defn) -> Definition -> Maybe [QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Maybe [QName])
-> TCMT IO Definition -> TCMT IO (Maybe [QName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
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} -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
cs
    Record{recConHead :: Defn -> ConHead
recConHead = ConHead
h}  -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [ConHead -> QName
conName ConHead
h]
    Defn
_                       -> Maybe [QName]
forall a. Maybe a
Nothing