module Agda.TypeChecking.Records where
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad
import Data.List
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.Utils.List
#include "../undefined.h"
import Agda.Utils.Impossible
orderFields :: MonadTCM tcm => 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 :: MonadTCM tcm => QName -> tcm Defn
getRecordDef r = do
def <- theDef <$> getConstInfo r
case def of
Record{} -> return def
_ -> typeError $ ShouldBeRecordType (El Prop $ Def r [])
getRecordFieldNames :: MonadTCM tcm => QName -> tcm [(Hiding, C.Name)]
getRecordFieldNames r =
map (id *** nameConcrete . qnameName) . recFields <$> getRecordDef r
getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope
getRecordFieldTypes r = recTel <$> getRecordDef r
getRecordConstructorType :: MonadTCM tcm => QName -> tcm Type
getRecordConstructorType r = recConType <$> getRecordDef r
getRecordConstructor :: MonadTCM tcm => QName -> tcm QName
getRecordConstructor r = killRange <$> do
c <- recCon <$> getRecordDef r
case c of
Nothing -> return r
Just c -> return c
isRecord :: MonadTCM tcm => QName -> tcm Bool
isRecord r = do
def <- theDef <$> getConstInfo r
return $ case def of
Record{} -> True
_ -> False
etaExpandRecord :: MonadTCM tcm => QName -> Args -> Term -> tcm (Telescope, Args)
etaExpandRecord r pars u = do
Record{ recFields = xs, recTel = tel } <- getRecordDef r
let tel' = apply tel pars
proj (h, x) = Arg h $ Def x $ map hide pars ++ [Arg NotHidden u]
reportSDoc "tc.record.eta" 20 $ vcat
[ text "eta expanding" <+> prettyTCM u <+> text ":" <+> prettyTCM r
, nest 2 $ vcat
[ text "tel' =" <+> prettyTCM tel'
, text "args =" <+> prettyTCM (map proj xs)
]
]
return (tel', map proj xs)
where
hide (Arg _ x) = Arg Hidden x
etaContractRecord :: MonadTCM tcm => QName -> Args -> tcm Term
etaContractRecord r args = do
Record{ recFields = xs } <- getRecordDef r
let check (Arg _ v) (_, x) = do
case v of
Def y args@(_:_) | x == y -> return (Just $ unArg $ last args)
_ -> return Nothing
unless (length args == length xs) __IMPOSSIBLE__
cs <- zipWithM check args xs
let fallBack = Con <$> getRecordConstructor r <*> return args
case sequence cs of
Just (c:cs) -> do
if all (c ==) cs
then return c
else fallBack
_ -> fallBack