module Agda.TypeChecking.Datatypes where
import Data.Maybe (fromMaybe)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (constructorForm)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Substitute
import Agda.Utils.Size
import Agda.Utils.Functor
#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 <$> do (`piApplyM` pars) . defType =<< getConInfo c
_ -> return Nothing
data HasEta = NoEta | YesEta
deriving (Eq)
data ConstructorInfo = DataCon Nat
| RecordCon HasEta [Arg QName]
getConstructorInfo :: QName -> TCM ConstructorInfo
getConstructorInfo 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
r@Record{ recFields = fs } ->
return $ RecordCon (if recEtaEquality r then YesEta else NoEta) fs
Datatype{} -> do
TelV tel _ <- telView t
return $ DataCon $ size tel n
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
getConstructorArity :: QName -> TCM Nat
getConstructorArity c =
for (getConstructorInfo c) $ \i ->
case i of
DataCon n -> n
RecordCon _ fs -> size fs
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
Constructor{ conPars = n } -> return $ Just n
_ -> return Nothing