{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternSynonyms #-}
module Agda.TypeChecking.Implicit where
import Control.Monad
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
implicitArgs
:: Int
-> (Hiding -> Bool)
-> Type
-> TCM (Args, Type)
implicitArgs n expand t = mapFst (map (fmap namedThing)) <$> do
implicitNamedArgs n (\ h x -> expand h) t
implicitNamedArgs
:: Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> TCM (NamedArgs, Type)
implicitNamedArgs 0 expand t0 = return ([], t0)
implicitNamedArgs n expand t0 = do
t0' <- reduce t0
reportSDoc "tc.term.args" 30 $ "implicitNamedArgs" <+> prettyTCM t0'
reportSDoc "tc.term.args" 80 $ "implicitNamedArgs" <+> text (show t0')
case unEl t0' of
Pi Dom{domInfo = info, domName = name, unDom = a} b
| let x = maybe "_" rangedThing name, expand (getHiding info) x -> do
info' <- if hidden info then return info else do
reportSDoc "tc.term.args.ifs" 15 $
"inserting instance meta for type" <+> prettyTCM a
reportSDoc "tc.term.args.ifs" 40 $ nest 2 $ vcat
[ "x = " <+> text (show x)
, "hiding = " <+> text (show $ getHiding info)
]
return $ makeInstance info
(_, v) <- newMetaArg info' x a
let narg = Arg info (Named (Just $ unranged x) v)
mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)
_ -> return ([], t0')
newMetaArg
:: ArgInfo
-> ArgName
-> Type
-> TCM (MetaId, Term)
newMetaArg info x a = do
applyModalityToContext info $
newMeta (getHiding info) (argNameToString x) a
where
newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
newMeta Instance{} = newInstanceMeta
newMeta Hidden = newNamedValueMeta RunMetaOccursCheck
newMeta NotHidden = newNamedValueMeta RunMetaOccursCheck
newInteractionMetaArg
:: ArgInfo
-> ArgName
-> Type
-> TCM (MetaId, Term)
newInteractionMetaArg info x a = do
applyModalityToContext info $
newMeta (getHiding info) (argNameToString x) a
where
newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
newMeta Instance{} = newInstanceMeta
newMeta Hidden = newNamedValueMeta' RunMetaOccursCheck
newMeta NotHidden = newNamedValueMeta' RunMetaOccursCheck
data ImplicitInsertion
= ImpInsert [Hiding]
| BadImplicits
| NoSuchName ArgName
deriving (Show)
pattern NoInsertNeeded :: ImplicitInsertion
pattern NoInsertNeeded = ImpInsert []
insertImplicit
:: NamedArg e
-> [Dom a]
-> ImplicitInsertion
insertImplicit a doms = insertImplicit' a $ map name doms
where
name dom = x <$ argFromDom dom
where x = maybe "_" rangedThing $ domName dom
insertImplicit'
:: NamedArg e
-> [Arg ArgName]
-> ImplicitInsertion
insertImplicit' _ [] = BadImplicits
insertImplicit' a ts
| visible a = ImpInsert $ takeWhile notVisible $ map getHiding ts
| Just x <- rangedThing <$> nameOf (unArg a) = maybe (NoSuchName x) ImpInsert $
takeHiddenUntil (\ t -> x == unArg t && sameHiding a t) ts
| otherwise = maybe BadImplicits ImpInsert $
takeHiddenUntil (sameHiding a) ts
where
takeHiddenUntil :: (Arg ArgName -> Bool) -> [Arg ArgName] -> Maybe [Hiding]
takeHiddenUntil p ts =
case ts2 of
[] -> Nothing
(t : _) -> if visible t then Nothing else Just $ map getHiding ts1
where
(ts1, ts2) = break (\ t -> p t || visible t) ts