{-# 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 {-# SOURCE #-} Agda.TypeChecking.Rules.Term (unquoteTactic)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Tuple
implicitArgs
:: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m)
=> Int
-> (Hiding -> Bool)
-> Type
-> m (Args, Type)
implicitArgs n expand t = mapFst (map (fmap namedThing)) <$> do
implicitNamedArgs n (\ h x -> expand h) t
implicitNamedArgs
:: (MonadReduce m, MonadMetaSolver m, MonadDebug m, MonadTCM m)
=> Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m (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@Dom{domInfo = info, domTactic = tac, unDom = a} b
| let x = bareNameWithDefault "_" dom, 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 CmpLeq a
whenJust tac $ \ tac -> liftTCM $ unquoteTactic tac v a
let narg = Arg info (Named (Just $ WithOrigin Inserted $ unranged x) v)
mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)
_ -> return ([], t0')
newMetaArg
:: MonadMetaSolver m
=> ArgInfo
-> ArgName
-> Comparison
-> Type
-> m (MetaId, Term)
newMetaArg info x cmp a = do
prp <- isPropM a
let irrelevantIfProp = if prp then applyRelevanceToContext Irrelevant else id
applyModalityToContext info $ irrelevantIfProp $
newMeta (getHiding info) (argNameToString x) a
where
newMeta :: MonadMetaSolver m => Hiding -> String -> Type -> m (MetaId, Term)
newMeta Instance{} n = newInstanceMeta n
newMeta Hidden n = newNamedValueMeta RunMetaOccursCheck n cmp
newMeta NotHidden n = newNamedValueMeta RunMetaOccursCheck n cmp
newInteractionMetaArg
:: ArgInfo
-> ArgName
-> Comparison
-> Type
-> TCM (MetaId, Term)
newInteractionMetaArg info x cmp a = do
applyModalityToContext info $
newMeta (getHiding info) (argNameToString x) a
where
newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
newMeta Instance{} n = newInstanceMeta n
newMeta Hidden n = newNamedValueMeta' RunMetaOccursCheck n cmp
newMeta NotHidden n = newNamedValueMeta' RunMetaOccursCheck n cmp
data ImplicitInsertion
= ImpInsert [Dom ()]
| BadImplicits
| NoSuchName ArgName
deriving (Show)
pattern NoInsertNeeded :: ImplicitInsertion
pattern NoInsertNeeded = ImpInsert []
insertImplicit
:: NamedArg e
-> [Dom a]
-> ImplicitInsertion
insertImplicit a doms = insertImplicit' a $
for doms $ \ dom ->
dom $> bareNameWithDefault "_" dom
insertImplicit'
:: NamedArg e
-> [Dom ArgName]
-> ImplicitInsertion
insertImplicit' _ [] = BadImplicits
insertImplicit' a ts
| visible a = ImpInsert $ takeWhile notVisible $ map void ts
| Just x <- bareNameOf a = maybe (NoSuchName x) ImpInsert $
takeHiddenUntil (\ t -> x == unDom t && sameHiding a t) ts
| otherwise = maybe BadImplicits ImpInsert $
takeHiddenUntil (sameHiding a) ts
where
takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil p ts =
case ts2 of
[] -> Nothing
(t : _) -> if visible t then Nothing else Just $ map void ts1
where
(ts1, ts2) = break (\ t -> p t || visible t) ts