{-# 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
getConHead :: (HasConstInfo m) => QName -> m (Either SigError ConHead)
getConHead :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
Definition
def <- forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
c
case Definition -> Defn
theDef Definition
def of
Constructor { conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c' } -> forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
Record { recConHead :: Defn -> ConHead
recConHead = ConHead
c' } -> forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c'
Defn
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Char] -> SigError
SigUnknown forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow QName
c forall a. [a] -> [a] -> [a]
++ [Char]
" is not a constructor"
isConstructor :: (HasConstInfo m) => QName -> m Bool
isConstructor :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isConstructor QName
q = forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
q
getConForm :: QName -> TCM (Either SigError ConHead)
getConForm :: QName -> TCM (Either SigError ConHead)
getConForm QName
c = forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left) forall a b. (a -> b) -> a -> b
$ \ ConHead
ch -> do
Con ConHead
con ConInfo
_ [] <- forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
ch ConInfo
ConOCon [])
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ConHead
con
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getOrigConHead QName
c = forall b d a. (b -> d) -> Either a b -> Either a d
mapRight (forall a. LensConName a => QName -> a -> a
setConName QName
c) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead QName
c
{-# SPECIALIZE getConstructorData :: QName -> TCM QName #-}
getConstructorData :: HasConstInfo m => QName -> m QName
getConstructorData :: forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c = do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
case Definition -> Defn
theDef Definition
def of
Constructor{conData :: Defn -> QName
conData = QName
d} -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
d
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
consOfHIT :: HasConstInfo m => QName -> m Bool
consOfHIT :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT QName
c = do
QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Defn
def of
Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QName]
xs
Record{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
isPathCons :: HasConstInfo m => QName -> m Bool
isPathCons :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isPathCons QName
c = do
QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Defn
def of
Datatype {dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
xs} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
xs
Record{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
getFullyAppliedConType
:: PureTCM m
=> ConHead
-> Type
-> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType :: forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$
[ [Char]
"getFullyAppliedConType", forall a. Pretty a => a -> [Char]
prettyShow ConHead
c, forall a. Pretty a => a -> [Char]
prettyShow Type
t ]
ConHead
c <- forall a b. (a -> b) -> Either a b -> b
fromRight forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
c)
Definition
cdef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
let ctype :: Type
ctype = Definition -> Type
defType Definition
cdef
cdata :: QName
cdata = Defn -> QName
conData forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef
npars :: VerboseLevel
npars = Defn -> VerboseLevel
conPars forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef
case forall t a. Type'' t a -> a
unEl Type
t of
Def QName
d [Elim]
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
cdata -> do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$
[ [Char]
"getFullyAppliedConType: case Def", forall a. Pretty a => a -> [Char]
prettyShow QName
d, forall a. Pretty a => a -> [Char]
prettyShow [Elim]
es ]
Type
dt <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
let pars :: Args
pars = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall a b. (a -> b) -> a -> b
$ forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
npars [Elim]
es
Type
ctPars <- Type
ctype forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` Args
pars
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((QName
d, Type
dt, Args
pars), Type
ctPars)
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
fullyApplyCon
:: (PureTCM m, MonadBlock m, MonadTCError m)
=> ConHead
-> Elims
-> Type
-> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
-> m a
fullyApplyCon :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m, MonadTCError m) =>
ConHead
-> [Elim]
-> Type
-> (QName
-> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> m a
fullyApplyCon ConHead
c [Elim]
vs Type
t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret = forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
-> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
c [Elim]
vs Type
t QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Type -> TypeError
DoesNotConstructAnElementOf (ConHead -> QName
conName ConHead
c)
fullyApplyCon'
:: (PureTCM m, MonadBlock m)
=> ConHead
-> Elims
-> Type
-> (QName -> Type -> Args -> Type -> Elims -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' :: forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
-> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
c [Elim]
vs Type
t0 QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret Type -> m a
err = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.getConType" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"fullyApplyCon': constructor "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
, TCMT IO Doc
" with arguments"
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Elim]
vs
, TCMT IO Doc
" at type "
, forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0
]
(TelV Telescope
tel Type
t, Boundary
boundary) <- forall (m :: * -> *). PureTCM m => Type -> m (TelView, Boundary)
telViewPathBoundaryP Type
t0
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> [Char] -> m ()
reportSLn [Char]
"tc.getConType" VerboseLevel
35 forall a b. (a -> b) -> a -> b
$ [Char]
" target type: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Type
t
Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
forall (m :: * -> *).
PureTCM m =>
ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType ConHead
c Type
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe ((QName, Type, Args), Type)
Nothing -> Type -> m a
err Type
t
Just ((QName
d, Type
dt, Args
pars), Type
a) ->
QName -> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a
ret QName
d Type
dt Args
pars Type
a (forall a. Subst a => VerboseLevel -> a -> a
raise (forall a. Sized a => a -> VerboseLevel
size Telescope
tel) [Elim]
vs forall a. [a] -> [a] -> [a]
++ forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
tel Boundary
boundary) Telescope
tel Type
t
getConType
:: (PureTCM m, MonadBlock m)
=> ConHead
-> Type
-> m (Maybe ((QName, Type, Args), Type))
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
Maybe VerboseLevel
npars <- forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
c
if | Maybe VerboseLevel
npars forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just VerboseLevel
0 -> do
Type
ctype <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
QName
d <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getConstructorData QName
c
Type
dtype <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ((QName
d,Type
dtype,[]),Type
ctype)
| Bool
otherwise -> forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
ConHead
-> [Elim]
-> Type
-> (QName
-> Type -> Args -> Type -> [Elim] -> Telescope -> Type -> m a)
-> (Type -> m a)
-> m a
fullyApplyCon' ConHead
ch [] Type
t
(\QName
d Type
dt Args
pars Type
ct [Elim]
es Telescope
tel Type
a -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
let escape :: ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
escape = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS HasCallStack => Impossible
impossible (forall a. Sized a => a -> VerboseLevel
size Telescope
tel)) in
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ((QName, Type, Args), Type) -> ((QName, Type, Args), Type)
escape ((QName
d, Type
dt, Args
pars), Type
ct))
(\Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
data ConstructorInfo
= DataCon Arity
| RecordCon PatternOrCopattern HasEta
Arity
[Dom QName]
getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo :: forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo QName
c = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c
getConstructorInfo' :: HasConstInfo m => QName -> m (Maybe ConstructorInfo)
getConstructorInfo' :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c = do
(Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Constructor{ conData :: Defn -> QName
conData = QName
d, conArity :: Defn -> VerboseLevel
conArity = VerboseLevel
n } -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
(Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
r :: Defn
r@Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PatternOrCopattern
-> HasEta -> VerboseLevel -> [Dom QName] -> ConstructorInfo
RecordCon (Defn -> PatternOrCopattern
recPatternMatching Defn
r) (Defn -> HasEta
recEtaEquality Defn
r) VerboseLevel
n [Dom QName]
fs
Datatype{} ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ConstructorInfo
DataCon VerboseLevel
n
Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
isDatatype :: QName -> TCM Bool
isDatatype :: QName -> TCM Bool
isDatatype QName
d = do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Definition -> Defn
theDef Definition
def of
Datatype{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Record{recNamedCon :: Defn -> Bool
recNamedCon = Bool
namedC} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
namedC
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d = do
(Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Record{ EtaEquality
recEtaEquality' :: Defn -> EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality', PatternOrCopattern
recPatternMatching :: PatternOrCopattern
recPatternMatching :: Defn -> PatternOrCopattern
recPatternMatching } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ PatternOrCopattern -> DataOrRecord
IsRecord forall a b. (a -> b) -> a -> b
$
case PatternOrCopattern
recPatternMatching of
p :: PatternOrCopattern
p@PatternOrCopattern
PatternMatching -> PatternOrCopattern
p
PatternOrCopattern
CopatternMatching ->
if forall a. PatternMatchingAllowed a => a -> Bool
patternMatchingAllowed EtaEquality
recEtaEquality' then PatternOrCopattern
PatternMatching else PatternOrCopattern
CopatternMatching
Datatype{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just DataOrRecord
IsData
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
isDataOrRecord :: Term -> TCM (Maybe (QName, DataOrRecord))
isDataOrRecord = \case
Def QName
d [Elim]
_ -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName
d,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
getNumberOfParameters :: HasConstInfo m => QName -> m (Maybe Nat)
getNumberOfParameters :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe VerboseLevel)
getNumberOfParameters QName
d = do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Definition -> Defn
theDef Definition
def of
Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
n } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
Record{ recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
n } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
Constructor{ conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
n } -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just VerboseLevel
n
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
getDatatypeArgs :: HasConstInfo m => Type -> m (Maybe (QName, Args, Args))
getDatatypeArgs :: forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, Args, Args))
getDatatypeArgs Type
t = do
case forall t a. Type'' t a -> a
unEl Type
t of
Def QName
d [Elim]
es -> do
let ~(Just Args
args) = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case Defn
def of
Datatype{dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
np} -> do
let !(Args
ps, Args
is) = forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
np Args
args
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
d, Args
ps, Args
is)
Record{} -> do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
d, Args
args, [])
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
getNotErasedConstructors :: QName -> TCM [QName]
getNotErasedConstructors :: QName -> TCM [QName]
getNotErasedConstructors QName
d = do
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall a. LensModality a => a -> Bool
usableModality forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM [QName]
getConstructors QName
d
getConstructors :: QName -> TCM [QName]
getConstructors :: QName -> TCM [QName]
getConstructors QName
d = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
QName -> TCM (Maybe [QName])
getConstructors' QName
d
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' QName
d = Defn -> Maybe [QName]
getConstructors_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
getConstructors_ :: Defn -> Maybe [QName]
getConstructors_ :: Defn -> Maybe [QName]
getConstructors_ = \case
Datatype{dataCons :: Defn -> [QName]
dataCons = [QName]
cs} -> forall a. a -> Maybe a
Just [QName]
cs
Record{recConHead :: Defn -> ConHead
recConHead = ConHead
h} -> forall a. a -> Maybe a
Just [ConHead -> QName
conName ConHead
h]
Defn
_ -> forall a. Maybe a
Nothing