{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Rules.LHS.Implicit where

import Control.Applicative

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Info
import Agda.Syntax.Internal
import qualified Agda.Syntax.Abstract as A

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty

import Agda.TypeChecking.Rules.LHS.Problem

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

-- | Insert implicit patterns in a problem.
insertImplicitProblem :: Problem -> TCM Problem
insertImplicitProblem (Problem ps qs tel) = do
  reportSDoc "tc.lhs.imp" 15 $
    sep [ text "insertImplicits"
	, nest 2 $ brackets $ fsep $ punctuate comma $ map prettyA ps
	, nest 2 $ prettyTCM tel
	]
  ps' <- insertImplicitPatterns ps tel
  return $ Problem ps' qs tel

-- | Insert implicit patterns in a list of patterns.
insertImplicitPatterns :: [NamedArg A.Pattern] -> Telescope -> TCM [NamedArg A.Pattern]
insertImplicitPatterns ps EmptyTel = return ps
insertImplicitPatterns ps tel@(ExtendTel _ tel') = case ps of
  [] -> do
    i <- insImp dummy tel
    case i of
      Just n	-> return $ replicate n implicitP
      Nothing	-> return []
  p : ps -> do
    i <- insImp p tel
    case i of
      Just 0	-> __IMPOSSIBLE__
      Just n	-> insertImplicitPatterns (replicate n implicitP ++ p : ps) tel
      Nothing	-> (p :) <$> insertImplicitPatterns ps (absBody tel')
  where
    dummy = Arg NotHidden $ unnamed ()

    insImp x tel = case insertImplicit x $ map (fmap fst) $ telToList tel of
      BadImplicits   -> typeError $ WrongHidingInLHS (telePi tel $ sort Prop)
      NoSuchName x   -> typeError $ WrongHidingInLHS (telePi tel $ sort Prop)
      ImpInsert n    -> return $ Just n
      NoInsertNeeded -> return Nothing

    implicitP = Arg Hidden . unnamed . A.ImplicitP . PatRange $ noRange