module Agda.TypeChecking.Records where
import Control.Monad
import Data.Function
import Data.List
import Data.Maybe
import qualified Data.Set as Set
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad ()
import Agda.TypeChecking.Telescope
import Agda.Utils.Either
import Agda.Utils.List
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
orderFields :: QName -> a -> [C.Name] -> [(C.Name, a)] -> TCM [a]
orderFields r def xs fs = do
shouldBeNull (ys \\ nub ys) $ DuplicateFields . nub
shouldBeNull (ys \\ xs) $ TooManyFields r
return $ order xs fs
where
ys = map fst fs
shouldBeNull [] err = return ()
shouldBeNull xs err = typeError $ err xs
order [] [] = []
order [] _ = __IMPOSSIBLE__
order (x : xs) ys = case lookup x (assocHoles ys) of
Just (e, ys') -> e : order xs ys'
Nothing -> def : order xs ys
assocHoles xs = [ (x, (v, xs')) | ((x, v), xs') <- holes xs ]
recordModule :: QName -> ModuleName
recordModule = mnameFromList . qnameToList
getRecordDef :: QName -> TCM Defn
getRecordDef r = maybe err return =<< isRecord r
where err = typeError $ ShouldBeRecordType (El Prop $ Def r [])
getRecordOfField :: QName -> TCM (Maybe QName)
getRecordOfField d = maybe Nothing fromP <$> isProjection d
where fromP Projection{ projProper = mp, projFromType = r} = mp $> r
getRecordFieldNames :: QName -> TCM [I.Arg C.Name]
getRecordFieldNames r = recordFieldNames <$> getRecordDef r
recordFieldNames :: Defn -> [I.Arg C.Name]
recordFieldNames = map (fmap (nameConcrete . qnameName)) . recFields
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords fields = do
defs <- (HMap.union `on` sigDefinitions) <$> getSignature <*> getImportedSignature
let possible def = case theDef def of
Record{ recFields = fs } -> Set.isSubsetOf given inrecord
where inrecord = Set.fromList $ map (nameConcrete . qnameName . unArg) fs
_ -> False
return [ defName d | d <- HMap.elems defs, possible d ]
where
given = Set.fromList fields
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes r = recTel <$> getRecordDef r
getRecordTypeFields :: Type -> TCM [I.Arg QName]
getRecordTypeFields t =
case ignoreSharing $ unEl t of
Def r _ -> do
rDef <- theDef <$> getConstInfo r
case rDef of
Record { recFields = fields } -> return fields
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
getRecordConstructorType :: QName -> TCM Type
getRecordConstructorType r = recConType <$> getRecordDef r
getRecordConstructor :: QName -> TCM ConHead
getRecordConstructor r = killRange <$> recConHead <$> getRecordDef r
isRecord :: HasConstInfo m => QName -> m (Maybe Defn)
isRecord r = do
def <- theDef <$> getConstInfo r
return $ case def of
Record{} -> Just def
_ -> Nothing
isRecordType :: Type -> TCM (Maybe (QName, Args, Defn))
isRecordType t = either (const Nothing) Just <$> tryRecordType t
tryRecordType :: Type -> TCM (Either (Maybe Type) (QName, Args, Defn))
tryRecordType t = ifBlockedType t (\ _ _ -> return $ Left Nothing) $ \ t -> do
let no = return $ Left $ Just t
case ignoreSharing $ unEl t of
Def r es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
caseMaybeM (isRecord r) no $ \ def -> return $ Right (r,vs,def)
_ -> no
projectType :: Type -> QName -> TCM (Maybe Type)
projectType t f = do
res <- isRecordType t
case res of
Nothing -> return Nothing
Just (_r, ps, _rdef) -> do
def <- getConstInfo f
if (isProperProjection $ theDef def)
then return $ Just $ defType def `apply` ps
else return Nothing
isEtaRecord :: HasConstInfo m => QName -> m Bool
isEtaRecord r = maybe False recEtaEquality <$> isRecord r
isEtaCon :: HasConstInfo m => QName -> m Bool
isEtaCon c = do
cdef <- theDef <$> getConstInfo c
case cdef of
Constructor {conData = r} -> isEtaRecord r
_ -> return False
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord r = maybe False (\ d -> recInduction d /= Just CoInductive || not (recRecursive d)) <$> isRecord r
isEtaRecordType :: Type -> TCM (Maybe (QName, Args))
isEtaRecordType a = case ignoreSharing $ unEl a of
Def d es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
ifM (isEtaRecord d) (return $ Just (d, vs)) (return Nothing)
_ -> return Nothing
isRecordConstructor :: QName -> TCM (Maybe (QName, Defn))
isRecordConstructor c = do
def <- theDef <$> getConstInfo c
case def of
Constructor{ conData = r } -> fmap (r,) <$> isRecord r
_ -> return Nothing
isGeneratedRecordConstructor :: QName -> TCM Bool
isGeneratedRecordConstructor c = do
def <- theDef <$> getConstInfo c
case def of
Constructor{ conData = r } -> do
def <- theDef <$> getConstInfo r
case def of
Record{ recNamedCon = False } -> return True
_ -> return False
_ -> return False
unguardedRecord :: QName -> TCM ()
unguardedRecord q = modifySignature $ updateDefinition q $ updateTheDef $ updateRecord
where updateRecord r@Record{} = r { recEtaEquality = False, recRecursive = True }
updateRecord _ = __IMPOSSIBLE__
recursiveRecord :: QName -> TCM ()
recursiveRecord q = modifySignature $ updateDefinition q $ updateTheDef $ updateRecord
where updateRecord r@Record{} = r { recRecursive = True }
updateRecord _ = __IMPOSSIBLE__
isRecursiveRecord :: QName -> TCM Bool
isRecursiveRecord q = recRecursive_ . theDef . fromMaybe __IMPOSSIBLE__ . lookupDefinition q <$> getSignature
recRecursive_ :: Defn -> Bool
recRecursive_ (Record { recRecursive = b }) = b
recRecursive_ _ = __IMPOSSIBLE__
etaExpandBoundVar :: Int -> TCM (Maybe (Telescope, Substitution, Substitution))
etaExpandBoundVar i = do
gamma <- getContext
let (gamma2, dom@(Dom ai (x, a)) : gamma1) = splitAt i gamma
let failure = do
reportSDoc "tc.meta.assign.proj" 25 $
text "failed to eta-expand variable " <+> prettyTCM x <+>
text " since its type " <+> prettyTCM a <+>
text " is not a record type"
return Nothing
caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> do
if not (recEtaEquality def) then return Nothing else Just <$> do
let tel = recTel def `apply` pars
m = size tel
fs = recFields def
ys = zipWith (\ f i -> f $> var i) fs $ downFrom m
u = Con (recConHead def) ys
tau0 = u :# raiseS m
tau = liftS (size gamma2) tau0
zs = for fs $ fmap $ \ f -> Var 0 [Proj f]
sigma0 = parallelS $ reverse $ map unArg zs
sigma = liftS (size gamma2) sigma0
rev = foldl (\ l (Dom ai (n, t)) -> Dom ai (nameToArgName n, t) : l) []
s = prettyShow x
tel' = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel
delta = telFromList $ rev gamma1 ++ telToList tel' ++ rev (applySubst tau0 gamma2)
return (delta, sigma, tau)
curryAt :: Type -> Int -> TCM (Term -> Term, Term -> Term, Type)
curryAt t n = do
TelV gamma core <- telViewUpTo n t
case ignoreSharing $ unEl core of
Pi (Dom ai a) b -> do
(r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
unless (recEtaEquality def) __IMPOSSIBLE__
let tel = recTel def `apply` pars
m = size tel
fs = recFields def
ys = zipWith (\ f i -> f $> var i) fs $ downFrom m
u = Con (recConHead def) ys
b' = raise m b `absApp` u
t' = gamma `telePi` (tel `telePi` b')
gammai = map domInfo $ telToList gamma
xs = reverse $ zipWith (\ ai i -> Arg ai $ var i) gammai [m..]
curry v = teleLam gamma $ teleLam tel $
raise (n+m) v `apply` (xs ++ [Arg ai u])
zs = for fs $ fmap $ \ f -> Var 0 [Proj f]
atel = sgTel $ Dom ai (absName b, a)
uncurry v = teleLam gamma $ teleLam atel $
raise (n + 1) v `apply` (xs ++ zs)
return (curry, uncurry, t')
_ -> __IMPOSSIBLE__
etaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)
etaExpandRecord r pars u = do
def <- getRecordDef r
(tel, _, args) <- etaExpandRecord_ r pars def u
return (tel, args)
etaExpandRecord_ :: QName -> Args -> Defn -> Term -> TCM (Telescope, ConHead, Args)
etaExpandRecord_ r pars def u = do
let Record{ recConHead = con
, recFields = xs
, recTel = tel
, recEtaEquality = eta
} = def
tel' = apply tel pars
unless eta __IMPOSSIBLE__
case ignoreSharing u of
Con con_ args -> do
when (con /= con_) __IMPOSSIBLE__
return (tel', con, args)
_ -> do
let xs' = for xs $ fmap $ \ x -> u `applyE` [Proj x]
reportSDoc "tc.record.eta" 20 $ vcat
[ text "eta expanding" <+> prettyTCM u <+> text ":" <+> prettyTCM r
, nest 2 $ vcat
[ text "tel' =" <+> prettyTCM tel'
, text "args =" <+> prettyTCM xs'
]
]
return (tel', con, xs')
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType t u = do
(r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType t
(tel, con, args) <- etaExpandRecord_ r pars def u
return (tel, Con con args)
etaContractRecord :: HasConstInfo m => QName -> ConHead -> Args -> m Term
etaContractRecord r c args = do
Just Record{ recFields = xs } <- isRecord r
let check :: I.Arg Term -> I.Arg QName -> Maybe (Maybe Term)
check a ax = do
case (getRelevance a, hasElims $ unArg a) of
(Irrelevant, _) -> Just Nothing
(_, Just (_, [])) -> Nothing
(_, Just (h, es)) | Proj f <- last es, unArg ax == f
-> Just $ Just $ h $ init es
_ -> Nothing
fallBack = return (Con c args)
case compare (length args) (length xs) of
LT -> fallBack
GT -> __IMPOSSIBLE__
EQ -> do
case zipWithM check args xs of
Just as -> case [ a | Just a <- as ] of
(a:as) ->
if all (a ==) as
then return a
else fallBack
_ -> fallBack
_ -> fallBack
isSingletonRecord :: QName -> Args -> TCM (Either MetaId Bool)
isSingletonRecord r ps = mapRight isJust <$> isSingletonRecord' False r ps
isSingletonRecordModuloRelevance :: QName -> Args -> TCM (Either MetaId Bool)
isSingletonRecordModuloRelevance r ps = mapRight isJust <$> isSingletonRecord' True r ps
isSingletonRecord' :: Bool -> QName -> Args -> TCM (Either MetaId (Maybe Term))
isSingletonRecord' regardIrrelevance r ps = do
reportSLn "tc.meta.eta" 30 $ "Is " ++ show r ++ " a singleton record type?"
def <- getRecordDef r
emap (Con $ recConHead def) <$> check (recTel def `apply` ps)
where
check :: Telescope -> TCM (Either MetaId (Maybe [I.Arg Term]))
check tel = do
reportSDoc "tc.meta.eta" 30 $
text "isSingletonRecord' checking telescope " <+> prettyTCM tel
case tel of
EmptyTel -> return $ Right $ Just []
ExtendTel dom tel
| isIrrelevant dom && regardIrrelevance -> do
underAbstraction dom tel $ \ tel ->
emap (Arg (domInfo dom) garbage :) <$> check tel
| otherwise -> do
isSing <- isSingletonType' regardIrrelevance $ unDom dom
case isSing of
Left mid -> return $ Left mid
Right Nothing -> return $ Right Nothing
Right (Just v) -> underAbstraction dom tel $ \ tel ->
emap (Arg (domInfo dom) v :) <$> check tel
garbage :: Term
garbage = Sort Prop
isSingletonType :: Type -> TCM (Either MetaId (Maybe Term))
isSingletonType = isSingletonType' False
isSingletonTypeModuloRelevance :: (MonadTCM tcm) => Type -> tcm (Either MetaId Bool)
isSingletonTypeModuloRelevance t = liftTCM $ do
mapRight isJust <$> isSingletonType' True t
isSingletonType' :: Bool -> Type -> TCM (Either MetaId (Maybe Term))
isSingletonType' regardIrrelevance t = do
TelV tel t <- telView t
ifBlockedType t (\ m _ -> return $ Left m) $ \ t -> do
res <- isRecordType t
case res of
Just (r, ps, def) | recEtaEquality def -> do
emap (abstract tel) <$> isSingletonRecord' regardIrrelevance r ps
_ -> return $ Right Nothing
emap :: (a -> b) -> Either c (Maybe a) -> Either c (Maybe b)
emap = mapRight . fmap