module Agda.TypeChecking.Datatypes where
import Control.Applicative ((<$>))
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.Size
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__
getConstructorArity :: QName -> TCM (Either Nat [Arg QName])
getConstructorArity c = do
Defn{ defType = t, theDef = def } <- getConstInfo c
case def of
Constructor{ conData = d, conPars = n } -> do
def <- theDef <$> getConstInfo d
case def of
Record{ recFields = fs } ->
return $ Right fs
Datatype{} -> do
TelV tel _ <- telView t
return $ Left $ size tel n
_ -> __IMPOSSIBLE__
_ -> __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
data DataOrRecord = IsData | IsRecord
deriving (Eq, Ord, Show)
isDataOrRecordType :: QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType d = do
def <- getConstInfo d
case theDef def of
Datatype{} -> return $ Just IsData
Record{} -> return $ Just IsRecord
_ -> return $ Nothing
isDataOrRecord :: Term -> TCM (Maybe QName)
isDataOrRecord (Def d _) = fmap (const d) <$> isDataOrRecordType d
isDataOrRecord (Shared p) = isDataOrRecord (derefPtr p)
isDataOrRecord _ = return Nothing
getNumberOfParameters :: QName -> TCM (Maybe Nat)
getNumberOfParameters d = do
def <- getConstInfo d
case theDef def of
Datatype{ dataPars = n} -> return $ Just n
Record{ recPars = n} -> return $ Just n
_ -> return Nothing