module Agda.TypeChecking.Datatypes where
import Data.List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute
import Agda.Utils.Impossible
#include "../undefined.h"
getConstructorData :: QName -> TCM QName
getConstructorData c = do
def <- getConstInfo c
case theDef def of
Constructor{conData = d} -> return d
_ -> __IMPOSSIBLE__
isDatatype :: QName -> TCM Bool
isDatatype d = do
def <- getConstInfo d
case theDef def of
Datatype{} -> return True
Record{recNamedCon = namedC} -> return namedC
_ -> return False
isDataOrRecordType :: QName -> TCM Bool
isDataOrRecordType d = do
def <- getConstInfo d
case theDef def of
Datatype{} -> return True
Record{} -> return True
_ -> return False
data DatatypeInfo = DataInfo
{ datatypeName :: QName
, datatypeParTel :: Telescope
, datatypePars :: Args
, datatypeIxTel :: Telescope
, datatypeIxs :: Args
}
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