{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Records where

import Control.Applicative
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.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.Utils.List

#include "../undefined.h"
import Agda.Utils.Impossible

-- | Order the fields of a record construction.
--   Use the second argument for missing fields.
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
  -- shouldBeNull (xs \\ ys)     $ TooFewFields r
  return $ order xs fs
  where
    ys = map fst fs

    shouldBeNull [] err = return ()
    shouldBeNull xs err = typeError $ err xs

    -- invariant: the first list contains at least the fields of the second list
    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 ]

-- | The name of the module corresponding to a record.
recordModule :: QName -> ModuleName
recordModule = mnameFromList . qnameToList

-- | Get the definition for a record. Throws an exception if the name
--   does not refer to a record.
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 [])

-- | Get the field names of a record.
getRecordFieldNames :: MonadTCM tcm => QName -> tcm [C.Name]
getRecordFieldNames r = map (nameConcrete . qnameName) . recFields <$> getRecordDef r

-- | Get the field types of a record.
getRecordFieldTypes :: MonadTCM tcm => QName -> tcm Telescope
getRecordFieldTypes r = recTel <$> getRecordDef r

-- | Get the type of the record constructor.
getRecordConstructorType :: MonadTCM tcm => QName -> [Arg Term] -> tcm Type
getRecordConstructorType r pars = do
  Record{ recTel = tel, recSort = s} <- getRecordDef r
  return $ telePi (apply tel pars) $ El s $ Def r pars

-- | Check if a name refers to a record.
isRecord :: MonadTCM tcm => QName -> tcm Bool
isRecord r = do
  def <- theDef <$> getConstInfo r
  return $ case def of
    Record{} -> True
    _        -> False

{-| Compute the eta expansion of a record. The first argument should be
    the name of a record type. Given

    @record R : Set where x : A; y : B@

    and @r : R@, @etaExpand R [] r@ is @[R.x r, R.y r]@
-}
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 x = Arg NotHidden $ 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

-- | The fields should be eta contracted already.
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
  case sequence cs of
    Just (c:cs) -> do
      if all (c ==) cs
        then return c
        else fallBack
    _ -> fallBack
  where
    fallBack = return (Con r args)