{-# 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 = 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__

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

-- | 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 = ConHead
-> [Elim]
-> Type
-> (QName
    -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
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 ((Type -> m a) -> m a) -> (Type -> m a) -> m a
forall a b. (a -> b) -> a -> b
$
  TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> (Type -> TypeError) -> Type -> m a
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
  [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
"fullyApplyCon': 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
" with arguments"
    , [Elim] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Elim] -> m Doc
prettyTCM [Elim]
vs
    , 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
t0
    ]
  (TelV Telescope
tel Type
t, Boundary
boundary) <- Type -> m (TelView, 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.
  Telescope -> m a -> m a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ 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]
"  target type: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Type
t
    Type
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
    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 m (Maybe ((QName, Type, Args), Type))
-> (Maybe ((QName, Type, Args), Type) -> m a) -> m a
forall a b. m a -> (a -> m b) -> m b
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 (VerboseLevel -> [Elim] -> [Elim]
forall a. Subst a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel) [Elim]
vs [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++ Telescope -> Boundary -> [Elim]
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 <- QName -> m (Maybe VerboseLevel)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
c
  if | Maybe VerboseLevel
npars Maybe VerboseLevel -> Maybe VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
0 -> do
      Type
ctype <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
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
      QName
d  <- QName -> m QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
      Type
dtype <- Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
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
      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)
 -> m (Maybe ((QName, Type, Args), Type)))
-> Maybe ((QName, Type, Args), Type)
-> m (Maybe ((QName, Type, Args), Type))
forall a b. (a -> b) -> a -> b
$ ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
forall a. a -> Maybe a
Just ((QName
d,Type
dtype,[]),Type
ctype)
     | Bool
otherwise -> ConHead
-> [Elim]
-> Type
-> (QName
    -> Type
    -> Args
    -> Type
    -> [Elim]
    -> Telescope
    -> Type
    -> m (Maybe ((QName, Type, Args), Type)))
-> (Type -> m (Maybe ((QName, Type, Args), Type)))
-> m (Maybe ((QName, Type, Args), Type))
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 -> 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)
 -> m (Maybe ((QName, Type, Args), Type)))
-> Maybe ((QName, Type, Args), Type)
-> m (Maybe ((QName, Type, Args), Type))
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 = Substitution' (SubstArg ((QName, Type, Args), Type))
-> ((QName, Type, Args), Type) -> ((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 (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel)) in
        ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
forall a. a -> Maybe a
Just (((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type))
-> ((QName, Type, Args), Type) -> Maybe ((QName, Type, Args), Type)
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
_ -> 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 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 = 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 -> VerboseLevel -> [Dom QName] -> ConstructorInfo
RecordCon (Defn -> PatternOrCopattern
recPatternMatching Defn
r) (Defn -> HasEta
recEtaEquality Defn
r) VerboseLevel
n [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{ EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality' :: Defn -> EtaEquality
recEtaEquality', 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
forall p. p -> DataOrRecord' p
IsRecord (PatternOrCopattern -> DataOrRecord)
-> PatternOrCopattern -> DataOrRecord
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 EtaEquality -> Bool
forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed EtaEquality
recEtaEquality' then PatternOrCopattern
PatternMatching else PatternOrCopattern
CopatternMatching
    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
forall p. DataOrRecord' p
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, DataOrRecord))
isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
isDataOrRecord = \case
    Def QName
d [Elim]
_ -> (DataOrRecord -> (QName, DataOrRecord))
-> Maybe DataOrRecord -> Maybe (QName, DataOrRecord)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName
d,) (Maybe DataOrRecord -> Maybe (QName, DataOrRecord))
-> TCM (Maybe DataOrRecord) -> TCM (Maybe (QName, DataOrRecord))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
    Term
_       -> Maybe (QName, DataOrRecord) -> TCM (Maybe (QName, DataOrRecord))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, DataOrRecord)
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 -> TCM Bool) -> [QName] -> TCM [QName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Definition -> Bool
forall a. LensModality a => a -> Bool
usableModality (Definition -> Bool)
-> (QName -> TCMT IO Definition) -> QName -> TCM Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo) ([QName] -> TCM [QName]) -> TCM [QName] -> TCM [QName]
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 = [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