module Agda.TypeChecking.Datatypes where
import Control.Monad.Except
import Data.Maybe (fromMaybe)
import qualified Data.List as List
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.TypeChecking.Pretty
import Agda.Utils.Either
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Impossible
getConHead :: (HasConstInfo m) => QName -> m (Either SigError ConHead)
getConHead c = runExceptT $ do
def <- ExceptT $ getConstInfo' c
case theDef def of
Constructor { conSrcCon = c' } -> return c'
Record { recConHead = c' } -> return c'
_ -> throwError $ SigUnknown $ prettyShow c ++ " is not a constructor"
getConForm :: QName -> TCM (Either SigError ConHead)
getConForm c = caseEitherM (getConHead c) (return . Left) $ \ ch -> do
Con con _ [] <- constructorForm (Con ch ConOCon [])
return $ Right con
getOrigConHead :: QName -> TCM (Either SigError ConHead)
getOrigConHead c = mapRight (setConName c) <$> getConHead c
{-# SPECIALIZE getConstructorData :: QName -> TCM QName #-}
getConstructorData :: HasConstInfo m => QName -> m QName
getConstructorData c = do
def <- getConstInfo c
case theDef def of
Constructor{conData = d} -> return d
_ -> __IMPOSSIBLE__
consOfHIT :: QName -> TCM Bool
consOfHIT c = do
d <- getConstructorData c
def <- theDef <$> getConstInfo d
case def of
Datatype {dataPathCons = xs} -> return $ not $ null xs
Record{} -> return False
_ -> __IMPOSSIBLE__
getConType
:: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m)
=> ConHead
-> Type
-> m (Maybe ((QName, Type, Args), Type))
getConType c t = do
reportSDoc "tc.getConType" 30 $ sep $
[ "getConType: constructor "
, prettyTCM c
, " at type "
, prettyTCM t
]
TelV tel t <- telView t
reportSLn "tc.getConType" 35 $ " target type: " ++ prettyShow t
applySubst (strengthenS __IMPOSSIBLE__ (size tel)) <$> do
addContext tel $ getFullyAppliedConType c t
getFullyAppliedConType
:: (HasConstInfo m, MonadReduce m, MonadDebug m)
=> ConHead
-> Type
-> m (Maybe ((QName, Type, Args), Type))
getFullyAppliedConType c t = do
reportSLn "tc.getConType" 35 $ List.intercalate " " $
[ "getFullyAppliedConType", prettyShow c, prettyShow t ]
c <- fromRight __IMPOSSIBLE__ <$> do getConHead $ conName c
case unEl t of
Def d es -> do
reportSLn "tc.getConType" 35 $ List.intercalate " " $
[ "getFullyAppliedConType: case Def", prettyShow d, prettyShow es ]
def <- getConstInfo d
let cont n = do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take n es
Just . ((d, defType def, pars),) <$> do
(`piApplyM` pars) . defType =<< getConInfo c
case theDef def of
Datatype { dataPars = n, dataCons = cs } | conName c `elem` cs -> cont n
Record { recPars = n, recConHead = con } | c == con -> cont n
_ -> return Nothing
_ -> return Nothing
data ConstructorInfo
= DataCon Nat
| RecordCon HasEta [Dom QName]
getConstructorInfo :: HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo c = do
(theDef <$> getConstInfo c) >>= \case
Constructor{ conData = d, conArity = n } -> do
(theDef <$> getConstInfo d) >>= \case
r@Record{ recFields = fs } ->
return $ RecordCon (recEtaEquality r) fs
Datatype{} ->
return $ DataCon 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
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 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
getConstructors :: QName -> TCM [QName]
getConstructors d = fromMaybe __IMPOSSIBLE__ <$>
getConstructors' d
getConstructors' :: QName -> TCM (Maybe [QName])
getConstructors' d = getConstructors_ . theDef <$> getConstInfo d
getConstructors_ :: Defn -> Maybe [QName]
getConstructors_ = \case
Datatype{dataCons = cs} -> Just cs
Record{recConHead = h} -> Just [conName h]
_ -> Nothing
getConHeads :: QName -> TCM [ConHead]
getConHeads d = fromMaybe __IMPOSSIBLE__ <$>
getConHeads' d
getConHeads' :: QName -> TCM (Maybe [ConHead])
getConHeads' d = theDef <$> getConstInfo d >>= \case
Record{recConHead = h} -> return $ Just [h]
Datatype{dataCons = cs} -> Just <$> mapM makeConHead cs
_ -> return $ Nothing
makeConHead :: QName -> TCM ConHead
makeConHead c = do
def <- getConstInfo c
case theDef def of
Constructor{conPars = n, conProj = Just fs} -> do
TelV tel _ <- telView (defType def)
let ai = map getArgInfo $ drop n $ telToList tel
return $ ConHead c Inductive $ zipWith Arg ai fs
Constructor{conProj = Nothing} -> return $ ConHead c Inductive []
_ -> __IMPOSSIBLE__