{-# LANGUAGE CPP #-}
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
implicitP :: ArgInfo -> NamedArg A.Pattern
implicitP info = Arg (setOrigin Inserted info) $ unnamed $ A.WildP $ PatRange $ noRange
insertImplicitPatterns :: ExpandHidden -> [NamedArg A.Pattern] ->
Telescope -> TCM [NamedArg A.Pattern]
insertImplicitPatterns exh ps tel =
insertImplicitPatternsT exh ps (telePi tel __DUMMY_TYPE__)
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 = takeWhile (not . visible) $ telToList tel
keep <- dropWhileEndM (not <.> isSizeLt . snd . unDom) ts
return $ map (implicitP . domInfo) 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 $
vcat [ "insertImplicitPatternsT"
, nest 2 $ "ps = " <+> do
brackets $ fsep $ punctuate comma $ map prettyA ps
, nest 2 $ "tel = " <+> prettyTCM tel
, nest 2 $ "b = " <+> addContext tel (prettyTCM b)
]
reportSDoc "tc.lhs.imp" 70 $
vcat [ "insertImplicitPatternsT"
, nest 2 $ "ps = " <+> (text . show) ps
, nest 2 $ "tel = " <+> (text . show) tel
, nest 2 $ "b = " <+> (text . show) b
]
case ps of
[] -> insImp dummy tel
p : _ -> do
let p' = applyWhen (isJust $ A.isProjP p) (setHiding NotHidden) p
hs <- insImp p' tel
let ps0@(~(p1 : ps1)) = hs ++ ps
reduce a >>= piOrPath >>= \case
Left (_, b) -> (p1 :) <$> insertImplicitPatternsT exh ps1 (absBody b)
Right{} -> return ps0
where
dummy = defaultNamedArg (A.VarP __IMPOSSIBLE__)
insImp p EmptyTel = return []
insImp p tel = case insertImplicit p $ telToList tel of
BadImplicits -> typeError WrongHidingInLHS
NoSuchName x -> typeError WrongHidingInLHS
ImpInsert n -> return $ map implicitArg n
implicitArg h = implicitP $ setHiding h $ defaultArgInfo