module Agda.TypeChecking.Datatypes where

import Control.Monad.Except

import Data.Maybe (fromMaybe)
import qualified Data.List as List

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (constructorForm)
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 :: 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 (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Record     { recConHead :: Defn -> ConHead
recConHead = ConHead
c' } -> ConHead -> ExceptT SigError m ConHead
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
    Defn
_ -> SigError -> ExceptT SigError m ConHead
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
$ String -> SigError
SigUnknown (String -> SigError) -> String -> SigError
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a constructor"

-- | 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 (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, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m Term
constructorForm (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
ch ConInfo
ConOCon [])
  Either SigError ConHead -> TCM (Either SigError ConHead)
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 :: 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 (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 :: QName -> TCM Bool
consOfHIT :: QName -> TCM Bool
consOfHIT QName
c = do
  QName
d <- QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
  Defn
def <- 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
  case Defn
def of
    Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM 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 (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
xs
    Record{} -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Defn
_  -> TCM 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
  :: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug 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 :: ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getConType ConHead
c Type
t = do
  String -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"tc.getConType" VerboseLevel
30 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
    [ TCM Doc
"getConType: constructor "
    , ConHead -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
    , TCM Doc
" at type "
    , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> 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@.
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.getConType" VerboseLevel
35 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"  target type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
prettyShow Type
t
  Substitution' Term
-> Maybe ((QName, Type, Args), Type)
-> Maybe ((QName, Type, Args), Type)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Empty -> VerboseLevel -> Substitution' Term
forall a. Empty -> VerboseLevel -> Substitution' a
strengthenS Empty
forall a. HasCallStack => a
__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
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 :: * -> *).
(HasConstInfo m, MonadReduce m, MonadDebug 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
  :: (HasConstInfo m, MonadReduce m, MonadDebug 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 :: ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t = do
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.getConType" VerboseLevel
35 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
" " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
    [ String
"getFullyAppliedConType", ConHead -> String
forall a. Pretty a => a -> String
prettyShow ConHead
c, Type -> String
forall a. Pretty a => a -> String
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
      String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.getConType" VerboseLevel
35 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
" " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
        [ String
"getFullyAppliedConType: case Def", QName -> String
forall a. Pretty a => a -> String
prettyShow QName
d, [Elim] -> String
forall a. Pretty a => a -> String
prettyShow [Elim]
es ]
      Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      let cont :: VerboseLevel -> f (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))
-> f Type -> f (Maybe ((QName, Type, Args), Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              (Type -> Args -> f Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Args
pars) (Type -> f Type) -> (Definition -> Type) -> Definition -> f Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> f Type) -> f Definition -> f Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConHead -> f 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
cs -> VerboseLevel -> m (Maybe ((QName, Type, Args), Type))
forall (f :: * -> *).
(MonadReduce f, HasConstInfo f) =>
VerboseLevel -> f (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))
forall (f :: * -> *).
(MonadReduce f, HasConstInfo f) =>
VerboseLevel -> f (Maybe ((QName, Type, Args), Type))
cont VerboseLevel
n
        Defn
_ ->  Maybe ((QName, Type, Args), Type)
-> m (Maybe ((QName, Type, Args), Type))
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 (m :: * -> *) a. Monad m => a -> m a
return Maybe ((QName, Type, Args), Type)
forall a. Maybe a
Nothing

data ConstructorInfo
  = DataCon Nat                  -- ^ Arity.
  | RecordCon 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 :: QName -> m 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 ConstructorInfo) -> m ConstructorInfo
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 } -> 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 (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 (m :: * -> *) a. Monad m => a -> m a
return (ConstructorInfo -> m ConstructorInfo)
-> ConstructorInfo -> m ConstructorInfo
forall a b. (a -> b) -> a -> b
$ HasEta -> [Dom QName] -> ConstructorInfo
RecordCon (Defn -> HasEta
recEtaEquality Defn
r) [Dom QName]
fs
        Datatype{} ->
           ConstructorInfo -> m ConstructorInfo
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
_ -> m ConstructorInfo
forall a. HasCallStack => a
__IMPOSSIBLE__

---------------------------------------------------------------------------
-- * 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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Record{recNamedCon :: Defn -> Bool
recNamedCon = Bool
namedC} -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
namedC
    Defn
_                            -> Bool -> TCM Bool
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
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  case Definition -> Defn
theDef Definition
def of
    Datatype{} -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
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
    Record{}   -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
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
IsRecord
    Defn
_          -> Maybe DataOrRecord -> TCM (Maybe DataOrRecord)
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 Term
v = do
  case Term
v of
    Def QName
d [Elim]
_ -> (DataOrRecord -> QName) -> Maybe DataOrRecord -> Maybe QName
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 (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

getNumberOfParameters :: QName -> TCM (Maybe Nat)
getNumberOfParameters :: QName -> TCM (Maybe VerboseLevel)
getNumberOfParameters 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{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
n }   -> Maybe VerboseLevel -> TCM (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCM (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCM (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 -> TCM (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCM (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCM (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 -> TCM (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe VerboseLevel -> TCM (Maybe VerboseLevel))
-> Maybe VerboseLevel -> TCM (Maybe VerboseLevel)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
n
    Defn
_                          -> Maybe VerboseLevel -> TCM (Maybe VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe VerboseLevel
forall a. Maybe a
Nothing

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

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

-- | 'Nothing' if not data or record type name.
getConHeads' :: QName -> TCM (Maybe [ConHead])
getConHeads' :: QName -> TCMT IO (Maybe [ConHead])
getConHeads' QName
d = 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 -> TCMT IO (Maybe [ConHead])) -> TCMT IO (Maybe [ConHead])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Record{recConHead :: Defn -> ConHead
recConHead = ConHead
h}  -> Maybe [ConHead] -> TCMT IO (Maybe [ConHead])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [ConHead] -> TCMT IO (Maybe [ConHead]))
-> Maybe [ConHead] -> TCMT IO (Maybe [ConHead])
forall a b. (a -> b) -> a -> b
$ [ConHead] -> Maybe [ConHead]
forall a. a -> Maybe a
Just [ConHead
h]
  Datatype{dataCons :: Defn -> [QName]
dataCons = [QName]
cs} -> [ConHead] -> Maybe [ConHead]
forall a. a -> Maybe a
Just ([ConHead] -> Maybe [ConHead])
-> TCM [ConHead] -> TCMT IO (Maybe [ConHead])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> TCMT IO ConHead) -> [QName] -> TCM [ConHead]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO ConHead
makeConHead [QName]
cs
  Defn
_                       -> Maybe [ConHead] -> TCMT IO (Maybe [ConHead])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [ConHead] -> TCMT IO (Maybe [ConHead]))
-> Maybe [ConHead] -> TCMT IO (Maybe [ConHead])
forall a b. (a -> b) -> a -> b
$ Maybe [ConHead]
forall a. Maybe a
Nothing

-- | Fills in the fields.
makeConHead :: QName -> TCM ConHead
makeConHead :: QName -> TCMT IO ConHead
makeConHead QName
c = do
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
  case Definition -> Defn
theDef Definition
def of
    Constructor{conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
n, conProj :: Defn -> Maybe [QName]
conProj = Just [QName]
fs} -> do
      TelV Tele (Dom Type)
tel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Definition -> Type
defType Definition
def)
      let ai :: [ArgInfo]
ai = (Dom (String, Type) -> ArgInfo)
-> [Dom (String, Type)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom (String, Type) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo ([Dom (String, Type)] -> [ArgInfo])
-> [Dom (String, Type)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n ([Dom (String, Type)] -> [Dom (String, Type)])
-> [Dom (String, Type)] -> [Dom (String, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel
      ConHead -> TCMT IO ConHead
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> TCMT IO ConHead) -> ConHead -> TCMT IO ConHead
forall a b. (a -> b) -> a -> b
$ QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
c Induction
Inductive ([Arg QName] -> ConHead) -> [Arg QName] -> ConHead
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> QName -> Arg QName)
-> [ArgInfo] -> [QName] -> [Arg QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ArgInfo -> QName -> Arg QName
forall e. ArgInfo -> e -> Arg e
Arg [ArgInfo]
ai [QName]
fs
    Constructor{conProj :: Defn -> Maybe [QName]
conProj = Maybe [QName]
Nothing} -> ConHead -> TCMT IO ConHead
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> TCMT IO ConHead) -> ConHead -> TCMT IO ConHead
forall a b. (a -> b) -> a -> b
$ QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
c Induction
Inductive []
    Defn
_ -> TCMT IO ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__

{- UNUSED
data DatatypeInfo = DataInfo
  { datatypeName   :: QName
  , datatypeParTel :: Telescope
  , datatypePars   :: Args
  , datatypeIxTel  :: Telescope
  , datatypeIxs    :: Args
  }

-- | Get the name and parameters from a type if it's a datatype or record type
--   with a named constructor.
getDatatypeInfo :: Type -> TCM (Maybe DatatypeInfo)
getDatatypeInfo t = do
  t <- reduce t
  case unEl t of
    Def d args -> do
      n          <- getDefFreeVars d
      args       <- return $ genericDrop n args
      def        <- instantiateDef =<< getConstInfo d
      TelV tel _ <- telView (defType def)
      let npars  = case theDef def of
            Datatype{dataPars = np} -> Just np
            Record{recPars = np, recNamedCon = True}
              | genericLength args == np -> Just np
              | otherwise                -> __IMPOSSIBLE__
            _                            -> Nothing
      return $ do
        np <- npars
        let (pt, it) = genericSplitAt np $ telToList tel
            parTel   = telFromList pt
            ixTel    = telFromList it
            (ps, is) = genericSplitAt np args
        return $ DataInfo { datatypeName = d
                          , datatypeParTel = parTel
                          , datatypePars   = ps
                          , datatypeIxTel  = ixTel
                          , datatypeIxs    = is
                          }
    _ -> return Nothing
-}