module Agda.TypeChecking.Rules.LHS.Implicit where
import Control.Applicative
import Control.Monad (forM)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Info
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Maybe
#include "undefined.h"
import Agda.Utils.Impossible
insertImplicitProblem :: Problem -> TCM Problem
insertImplicitProblem (Problem ps qs tel pr) = do
reportSDoc "tc.lhs.imp" 15 $
sep [ text "insertImplicits"
, nest 2 $ text "ps = " <+> do brackets $ fsep $ punctuate comma $ map prettyA ps
, nest 2 $ text "tel = " <+> prettyTCM tel
]
ps' <- insertImplicitPatterns ExpandLast ps tel
reportSDoc "tc.lhs.imp" 15 $
sep [ text "insertImplicits finished"
, nest 2 $ text "ps' = " <+> do brackets $ fsep $ punctuate comma $ map prettyA ps'
]
return $ Problem ps' qs tel pr
expandImplicitPattern :: Type -> A.NamedArg A.Pattern -> TCM (A.NamedArg A.Pattern)
expandImplicitPattern a p = maybe (return p) return =<< expandImplicitPattern' a p
expandImplicitPattern' :: Type -> A.NamedArg A.Pattern -> TCM (Maybe (A.NamedArg A.Pattern))
expandImplicitPattern' a p
| A.ImplicitP{} <- namedArg p, getHiding p /= Instance = do
caseMaybeM (isEtaRecordType =<< reduce a) (return Nothing) $ \ (d, _) -> do
def <- getRecordDef d
if not (recNamedCon def) then return Nothing else do
qs <- forM (recFields def) $ \ f -> flip Arg implicitP <$> reify (argInfo f)
let q = A.ConP (ConPatInfo True patNoRange) (A.AmbQ [recCon def]) qs
p' = updateNamedArg (const q) p
return $ Just p'
| otherwise = return Nothing
implicitP :: Named_ A.Pattern
implicitP = unnamed $ A.ImplicitP $ PatRange $ noRange
insertImplicitPatterns :: ExpandHidden -> [A.NamedArg A.Pattern] ->
Telescope -> TCM [A.NamedArg A.Pattern]
insertImplicitPatterns exh ps tel =
insertImplicitPatternsT exh ps (telePi tel typeDontCare)
insertImplicitPatternsT :: ExpandHidden -> [A.NamedArg A.Pattern] -> Type ->
TCM [A.NamedArg A.Pattern]
insertImplicitPatternsT DontExpandLast [] a = return []
insertImplicitPatternsT exh ps a = do
TelV tel b <- telViewUpTo' (1) (not . visible) a
case ps of
[] -> do
i <- insImp dummy tel
case i of
Just [] -> __IMPOSSIBLE__
Just hs -> return hs
Nothing -> return []
p : ps -> do
i <- insImp p tel
case i of
Just [] -> __IMPOSSIBLE__
Just hs -> insertImplicitPatternsT exh (hs ++ p : ps) (telePi tel b)
Nothing -> do
a <- reduce a
case ignoreSharing $ unEl a of
Pi arg b -> do
p <- expandImplicitPattern (unDom arg) p
(p :) <$> insertImplicitPatternsT exh ps (absBody b)
_ -> return (p : ps)
where
dummy = defaultNamedArg ()
insImp x EmptyTel
| visible x = return Nothing
| otherwise = typeError WrongHidingInLHS
insImp x tel = case insertImplicit x $ map (argFromDom . fmap fst) $ telToList tel of
BadImplicits -> typeError WrongHidingInLHS
NoSuchName x -> typeError WrongHidingInLHS
ImpInsert n -> return $ Just (map implicitArg n)
NoInsertNeeded -> return Nothing
implicitArg h = setHiding h $ defaultArg implicitP