module Agda.TypeChecking.Records where
import Control.Monad
import Data.Function
import Data.List
import Data.Maybe
import qualified Data.Set as Set
import Data.Traversable (traverse)
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (FieldAssignment'(..), nameFieldA)
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.TypeChecking.ProjectionLike (eligibleForProjectionLike)
import Agda.Utils.Either
import Agda.Utils.Functor (for, ($>))
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
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
unlessNull (ys \\ nub ys) $ typeError . DuplicateFields . nub
unlessNull (ys \\ xs) $ typeError . TooManyFields r
return $ order xs fs
where
ys = map fst fs
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 ]
insertMissingFields
:: QName
-> (C.Name -> a)
-> [FieldAssignment' a]
-> [Arg C.Name]
-> TCM [NamedArg a]
insertMissingFields r placeholder fs axs = do
let
xs = map unArg axs
let arg x e =
case [ a | a <- axs, unArg a == x ] of
[a] -> unnamed e <$ a
_ -> defaultNamedArg e
givenFields = [ (x, Just $ arg x e) | FieldAssignment x e <- fs ]
let missingExplicits =
[ (x, Just $ setOrigin Inserted $ unnamed . placeholder <$> a)
| a <- filter notHidden axs
, let x = unArg a
, x `notElem` map (view nameFieldA) fs
]
catMaybes <$> do
orderFields r Nothing xs $ givenFields ++ missingExplicits
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 = caseMaybeM (isProjection d) (return Nothing) $
\ Projection{ projProper = proper, projFromType = r} ->
return $ if proper then Just (unArg r) else Nothing
getRecordFieldNames :: QName -> TCM [Arg C.Name]
getRecordFieldNames r = recordFieldNames <$> getRecordDef r
recordFieldNames :: Defn -> [Arg C.Name]
recordFieldNames = map (fmap (nameConcrete . qnameName)) . recFields
findPossibleRecords :: [C.Name] -> TCM [QName]
findPossibleRecords fields = do
defs <- HMap.elems <$> use (stSignature . sigDefinitions)
idefs <- HMap.elems <$> use (stImports . sigDefinitions)
return $ cands defs ++ cands idefs
where
cands defs = [ defName d | d <- defs, possible d ]
possible def =
case theDef def of
Record{ recFields = fs } -> Set.isSubsetOf given $
Set.fromList $ map (nameConcrete . qnameName . unArg) fs
_ -> False
given = Set.fromList fields
getRecordFieldTypes :: QName -> TCM Telescope
getRecordFieldTypes r = recTel <$> getRecordDef r
getRecordTypeFields :: Type -> TCM [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__
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
origProjection :: HasConstInfo m => QName -> m (QName, Definition, Maybe Projection)
origProjection f = do
def <- getConstInfo f
let proj = isProjection_ $ theDef def
fallback = return (f, def, proj)
caseMaybe proj fallback $
\ p@Projection{ projProper = proper, projOrig = f' } ->
if not proper || f == f' then fallback else do
def <- getConstInfo f'
return (f', def, isProjection_ $ theDef def)
getDefType :: QName -> Type -> TCM (Maybe Type)
getDefType f t = do
(f, def, mp) <- origProjection f
let a = defType def
fallback = return $ Just a
reportSDoc "tc.deftype" 20 $ vcat
[ text "definition f = " <> prettyTCM f <+> text ("raw: " ++ show f)
, text "has type a = " <> prettyTCM a
, text "principal t = " <> prettyTCM t
]
caseMaybe mp fallback $
\ (Projection{ projIndex = n }) -> if n <= 0 then fallback else do
let npars | n == 0 = __IMPOSSIBLE__
| otherwise = n 1
reportSLn "tc.deftype" 20 $ "projIndex = " ++ show n
case ignoreSharing $ unEl t of
Def d es -> do
ifNotM (eligibleForProjectionLike d) failNotElig $ do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims $ take npars es
reportSDoc "tc.deftype" 20 $ vcat
[ text $ "head d = " ++ show d
, text "parameters =" <+> sep (map prettyTCM pars)
]
reportSLn "tc.deftype" 60 $ "parameters = " ++ show pars
if length pars < npars then failure "does not supply enough parameters"
else Just <$> a `piApplyM` pars
_ -> failNotDef
where
failNotElig = failure "is not eligible for projection-likeness"
failNotDef = failure "is not a Def."
failure reason = do
reportSDoc "tc.deftype" 25 $ sep
[ text "Def. " <+> prettyTCM f <+> text " is projection(like)"
, text "but the type "
, prettyTCM t
, text $ "of its argument " ++ reason
]
return Nothing
projectTyped :: Term -> Type -> ProjOrigin -> QName -> TCM (Maybe (Dom Type, Term, Type))
projectTyped v t o f = caseMaybeM (getDefType f t) (return Nothing) $ \ tf -> do
ifNotPiType tf (const $ return Nothing) $ \ dom b -> do
u <- applyDef o f (argFromDom dom $> v)
return $ Just (dom, u, b `absApp` v)
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 :: HasConstInfo m => QName -> m (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 $ \case
r@Record{} -> r { recEtaEquality' = setEtaEquality (recEtaEquality' r) False, recRecursive = True }
_ -> __IMPOSSIBLE__
recursiveRecord :: QName -> TCM ()
recursiveRecord q = do
ok <- etaEnabled
modifySignature $ updateDefinition q $ updateTheDef $ \case
r@Record{ recInduction = ind, recEtaEquality' = eta } ->
r { recRecursive = True, recEtaEquality' = eta' }
where
eta' | ok, eta == Inferred False, ind /= Just CoInductive = Inferred True
| otherwise = eta
_ -> __IMPOSSIBLE__
nonRecursiveRecord :: QName -> TCM ()
nonRecursiveRecord q = whenM etaEnabled $ do
modifySignature $ updateDefinition q $ updateTheDef $ \case
r@Record{ recInduction = ind, recEtaEquality' = Inferred False }
| ind /= Just CoInductive ->
r { recEtaEquality' = Inferred True }
r@Record{} -> r
_ -> __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 = fmap (\ (delta, sigma, tau, _) -> (delta, sigma, tau)) <$> do
expandRecordVar i =<< getContextTelescope
expandRecordVar :: Int -> Telescope -> TCM (Maybe (Telescope, Substitution, Substitution, Telescope))
expandRecordVar i gamma0 = do
let gamma = telToList gamma0
l = size gamma 1 i
let (gamma1, dom@(Dom ai (x, a)) : gamma2) = splitAt l gamma
let failure = do
reportSDoc "tc.meta.assign.proj" 25 $
text "failed to eta-expand variable " <+> pretty 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) ConOSystem ys
tau0 = consS u $ raiseS m
tau = liftS (size gamma2) tau0
zs = for fs $ fmap $ \ f -> Var 0 [Proj ProjSystem f]
sigma0 = reverse (map unArg zs) ++# raiseS 1
sigma = liftS (size gamma2) sigma0
s = prettyShow x
tel' = mapAbsNames (\ f -> stringToArgName $ argNameToString f ++ "(" ++ s ++ ")") tel
delta = telFromList $ gamma1 ++ telToList tel' ++ applySubst tau0 gamma2
return (delta, sigma, tau, tel)
expandRecordVarsRecursively :: [Int] -> Telescope -> TCM (Telescope, Substitution, Substitution)
expandRecordVarsRecursively [] gamma = return (gamma, idS, idS)
expandRecordVarsRecursively (i : is) gamma = do
caseMaybeM (expandRecordVar i gamma) (expandRecordVarsRecursively is gamma)
$ \ (gamma1, sigma1, tau1, tel) -> do
let n = size tel
newis = take n $ downFrom $ i + n
(gamma2, sigma2, tau2) <- expandRecordVarsRecursively (newis ++ is) gamma1
return (gamma2, applySubst sigma1 sigma2, applySubst tau2 tau1)
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) ConOSystem 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 ProjSystem 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 = etaExpandRecord' False
forceEtaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)
forceEtaExpandRecord = etaExpandRecord' True
etaExpandRecord' :: Bool -> QName -> Args -> Term -> TCM (Telescope, Args)
etaExpandRecord' forceEta r pars u = do
def <- getRecordDef r
(tel, _, _, args) <- etaExpandRecord'_ forceEta r pars def u
return (tel, args)
etaExpandRecord_ :: QName -> Args -> Defn -> Term -> TCM (Telescope, ConHead, ConInfo, Args)
etaExpandRecord_ = etaExpandRecord'_ False
etaExpandRecord'_ :: Bool -> QName -> Args -> Defn -> Term -> TCM (Telescope, ConHead, ConInfo, Args)
etaExpandRecord'_ forceEta r pars def u = do
let Record{ recConHead = con
, recFields = xs
, recTel = tel
} = def
eta = recEtaEquality def
tel' = apply tel pars
unless (eta || forceEta) __IMPOSSIBLE__
case ignoreSharing u of
Con con_ ci args -> do
when (con /= con_) $ do
reportSDoc "impossible" 10 $ vcat
[ text "etaExpandRecord_: the following two constructors should be identical"
, nest 2 $ text $ "con = " ++ show con
, nest 2 $ text $ "con_ = " ++ show con_
]
__IMPOSSIBLE__
return (tel', con, ci, args)
_ -> do
let xs' = for xs $ fmap $ \ x -> u `applyE` [Proj ProjSystem 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, ConOSystem, xs')
etaExpandAtRecordType :: Type -> Term -> TCM (Telescope, Term)
etaExpandAtRecordType t u = do
(r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType t
(tel, con, ci, args) <- etaExpandRecord_ r pars def u
return (tel, Con con ci args)
etaContractRecord :: HasConstInfo m => QName -> ConHead -> ConInfo -> Args -> m Term
etaContractRecord r c ci args = do
Just Record{ recFields = xs } <- isRecord r
let check :: Arg Term -> 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 _o f <- last es, unArg ax == f
-> Just $ Just $ h $ init es
_ -> Nothing
fallBack = return (Con c ci 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) ConOSystem) <$> check (recTel def `apply` ps)
where
check :: Telescope -> TCM (Either MetaId (Maybe [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
class NormaliseProjP a where
normaliseProjP :: HasConstInfo m => a -> m a
instance NormaliseProjP Clause where
normaliseProjP cl = do
ps <- normaliseProjP $ namedClausePats cl
return $ cl { namedClausePats = ps }
instance NormaliseProjP a => NormaliseProjP [a] where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Arg a) where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP a => NormaliseProjP (Named_ a) where
normaliseProjP = traverse normaliseProjP
instance NormaliseProjP (Pattern' x) where
normaliseProjP p@VarP{} = return p
normaliseProjP p@DotP{} = return p
normaliseProjP (ConP c cpi ps) = ConP c cpi <$> normaliseProjP ps
normaliseProjP p@LitP{} = return p
normaliseProjP (ProjP o d0) = ProjP o <$> getOriginalProjection d0