module Agda.TypeChecking.Datatypes where
import Control.Applicative ((<$>))
import Data.Maybe (fromMaybe)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (constructorForm)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
getConHead :: QName -> TCM ConHead
getConHead c = conSrcCon . theDef <$> getConstInfo c
getConTerm :: QName -> TCM Term
getConTerm c = flip Con [] <$> getConHead c
getConForm :: QName -> TCM ConHead
getConForm c = do
Con con [] <- ignoreSharing <$> do constructorForm =<< getConTerm c
return con
getOrigConHead :: QName -> TCM ConHead
getOrigConHead c = setConName c <$> getConHead c
getOrigConTerm :: QName -> TCM Term
getOrigConTerm c = flip Con [] <$> getOrigConHead c
getConstructorData :: HasConstInfo m => QName -> m QName
getConstructorData c = do
def <- getConstInfo c
case theDef def of
Constructor{conData = d} -> return d
_ -> __IMPOSSIBLE__
getConType :: ConHead -> Type -> TCM (Maybe Type)
getConType c t = do
c <- getConHead $ conName c
case ignoreSharing $ unEl t of
Def d es -> do
def <- theDef <$> getConstInfo d
case def of
Datatype { dataPars = n, dataCons = cs } | conName c `elem` cs -> cont n
Record { recPars = n, recConHead = con } | c == con -> cont n
_ -> return Nothing
where
cont n = do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take n es
Just . (`apply` pars) . defType <$> getConInfo c
_ -> return Nothing
getConstructorArity :: QName -> TCM (Either Nat [I.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 v = do
case ignoreSharing v of
Def d _ -> fmap (const d) <$> isDataOrRecordType d
_ -> 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