module Agda.TypeChecking.Records where
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Function
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Datatypes
import Agda.Utils.Either
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import qualified Agda.Utils.HashMap as HMap
#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 = do
def <- theDef <$> getConstInfo r
case def of
Record{} -> return def
_ -> typeError $ ShouldBeRecordType (El Prop $ Def r [])
getRecordFieldNames :: QName -> TCM [Arg C.Name]
getRecordFieldNames r =
map (fmap (nameConcrete . qnameName)) . recFields <$> getRecordDef r
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 [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 QName
getRecordConstructor r = killRange <$> recCon <$> getRecordDef r
isRecord :: QName -> TCM (Maybe Defn)
isRecord r = do
def <- theDef <$> getConstInfo r
return $ case def of
Record{} -> Just def
_ -> Nothing
isEtaRecord :: QName -> TCM Bool
isEtaRecord r = maybe False recEtaEquality <$> isRecord r
isInductiveRecord :: QName -> TCM Bool
isInductiveRecord r = maybe False (\ d -> recInduction d == Inductive || not (recRecursive d)) <$> isRecord r
isEtaRecordType :: Type -> TCM (Maybe (QName, Args))
isEtaRecordType a = case ignoreSharing $ unEl a of
Def d ps -> ifM (isEtaRecord d) (return $ Just (d, ps)) (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__
etaExpandRecord :: QName -> Args -> Term -> TCM (Telescope, Args)
etaExpandRecord r pars u = do
Record{ recFields = xs, recTel = tel, recEtaEquality = eta } <- getRecordDef r
unless eta __IMPOSSIBLE__
let tel' = apply tel pars
case ignoreSharing u of
Con _ args -> return (tel', args)
_ -> do
let xs' = map (fmap (\ x -> Def x [defaultArg u])) xs
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', xs')
etaContractRecord :: QName -> QName -> Args -> TCM Term
etaContractRecord r c args = do
Record{ recPars = npars, recFields = xs } <- getRecordDef r
let check :: Arg Term -> Arg QName -> Maybe (Maybe Term)
check a ax = do
case (argRelevance a, ignoreSharing $ unArg a) of
(Irrelevant, _) -> Just Nothing
(_, Def f [arg]) | unArg ax == f
-> Just $ Just $ unArg arg
_ -> 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 do
reportSDoc "tc.record.eta" 15 $ vcat
[ text "record" <+> prettyTCM (Con c args)
, text "is eta-contracted to" <+> prettyTCM a
]
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
def <- getRecordDef r
emap (Con $ recCon def) <$> check (recTel def `apply` ps)
where
check :: Telescope -> TCM (Either MetaId (Maybe [Arg Term]))
check EmptyTel = return $ Right $ Just []
check (ExtendTel arg@(Dom h Irrelevant _) tel) | regardIrrelevance =
underAbstraction arg tel $ \ tel ->
emap (Arg h Irrelevant garbage :) <$> check tel
check (ExtendTel arg@(Dom h r t) tel) = do
isSing <- isSingletonType' regardIrrelevance t
case isSing of
Left mid -> return $ Left mid
Right Nothing -> return $ Right Nothing
Right (Just v) -> underAbstraction arg tel $ \ tel ->
emap (Arg h r 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
t <- reduceB $ unEl t
case ignoreSharing <$> t of
Blocked m _ -> return (Left m)
NotBlocked (MetaV m _) -> return (Left m)
NotBlocked (Def r ps) ->
ifM (isNothing <$> isRecord r) (return $ Right Nothing) $ 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