module Agda.TypeChecking.Rules.LHS.Implicit where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad (forM)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Info
import Agda.Syntax.Internal as I
import Agda.Syntax.Abstract (IsProjP(..))
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.Function
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
#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 -> NamedArg A.Pattern -> TCM (NamedArg A.Pattern)
expandImplicitPattern a p = maybe (return p) return =<< expandImplicitPattern' a p
expandImplicitPattern' :: Type -> NamedArg A.Pattern -> TCM (Maybe (NamedArg A.Pattern))
expandImplicitPattern' a p
| A.WildP{} <- namedArg p, getHiding p /= Instance = do
caseMaybeM (isEtaRecordType =<< reduce a) (return Nothing) $ \ (d, _) -> do
def <- getRecordDef d
do
let qs = for (recFields def) $ \ f -> Arg (argInfo f) implicitP
let q = A.ConP (ConPatInfo ConPImplicit patNoRange) (A.AmbQ [recCon def]) qs
p' = updateNamedArg (const q) p
return $ Just p'
| otherwise = return Nothing
implicitP :: Named_ A.Pattern
implicitP = unnamed $ A.WildP $ PatRange $ noRange
insertImplicitPatterns :: ExpandHidden -> [NamedArg A.Pattern] ->
Telescope -> TCM [NamedArg A.Pattern]
insertImplicitPatterns exh ps tel =
insertImplicitPatternsT exh ps (telePi tel typeDontCare)
insertImplicitSizeLtPatterns :: Type -> TCM [NamedArg A.Pattern]
insertImplicitSizeLtPatterns t = do
isSize <- isSizeTypeTest
let isBounded BoundedNo = False
isBounded BoundedLt{} = True
isSizeLt t = maybe False isBounded . isSize . unEl <$> reduce t
TelV tel _ <- telView t
let ts = reverse $ takeWhile (not . visible) $ telToList tel
keep <- reverse <$> dropWhileM (not <.> isSizeLt . snd . unDom) ts
return [ Arg ai implicitP | Dom ai _ <- keep ]
insertImplicitPatternsT :: ExpandHidden -> [NamedArg A.Pattern] -> Type ->
TCM [NamedArg A.Pattern]
insertImplicitPatternsT DontExpandLast [] a = insertImplicitSizeLtPatterns a
insertImplicitPatternsT exh ps a = do
TelV tel b <- telViewUpTo' (1) (not . visible) a
reportSDoc "tc.lhs.imp" 20 $
sep [ text "insertImplicitPatternsT"
, nest 2 $ text "ps = " <+> do
brackets $ fsep $ punctuate comma $ map prettyA ps
, nest 2 $ text "tel = " <+> prettyTCM tel
, nest 2 $ text "b = " <+> addCtxTel tel (prettyTCM b)
]
case ps of
[] -> insImp dummy tel
p : ps -> do
let p' = applyWhen (isJust $ isProjP p) (setHiding NotHidden) p
hs <- insImp p' tel
case hs of
[] -> do
a <- reduce a
case ignoreSharing $ unEl a of
Pi arg b -> do
(p :) <$> insertImplicitPatternsT exh ps (absBody b)
_ -> return (p : ps)
hs -> insertImplicitPatternsT exh (hs ++ p : ps) (telePi tel b)
where
dummy = defaultNamedArg (A.VarP __IMPOSSIBLE__)
insImp p EmptyTel = return []
insImp p tel = case insertImplicit p $ map (argFromDom . fmap fst) $ telToList tel of
BadImplicits -> typeError WrongHidingInLHS
NoSuchName x -> typeError WrongHidingInLHS
ImpInsert n -> return $ map implicitArg n
NoInsertNeeded -> return []
implicitArg h = setHiding h $ defaultArg implicitP