module Agda.TypeChecking.Implicit where
import Agda.Syntax.Common
#include "../undefined.h"
import Agda.Utils.Impossible
data ImplicitInsertion
= ImpInsert Int
| BadImplicits
| NoSuchName String
| NoInsertNeeded
deriving (Show)
impInsert :: Int -> ImplicitInsertion
impInsert 0 = NoInsertNeeded
impInsert n = ImpInsert n
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