{-# LANGUAGE CPP #-}

{-| Functions for inserting implicit arguments at the right places.
-}
module Agda.TypeChecking.Implicit where

import Agda.Syntax.Common

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

data ImplicitInsertion
      = ImpInsert Int	  -- ^ this many implicits have to be inserted
      | BadImplicits	  -- ^ hidden argument where there should have been a non-hidden arg
      | NoSuchName String -- ^ bad named argument
      | NoInsertNeeded
  deriving (Show)

impInsert :: Int -> ImplicitInsertion
impInsert 0 = NoInsertNeeded
impInsert n = ImpInsert n

-- | The list should be non-empty.
insertImplicit :: NamedArg e -> [Arg String] -> ImplicitInsertion
insertImplicit _		 [] = __IMPOSSIBLE__
insertImplicit (Arg NotHidden _) ts = impInsert $ nofHidden ts
  where
    nofHidden :: [Arg a] -> Int
    nofHidden = length . takeWhile ((Hidden ==) . argHiding)
insertImplicit (Arg _ e) ts@(t : _) =
  case argHiding t of
    NotHidden -> BadImplicits
    Hidden    -> case nameOf e of
      Nothing -> impInsert 0
      Just x  -> find 0 x ts
  where
    find i x (Arg Hidden y : ts)
      | x == y	  = impInsert i
      | otherwise = find (i + 1) x ts
    find i x (Arg NotHidden _ : _) = NoSuchName x
    find i x []			   = NoSuchName x