module Agda.TypeChecking.Rules.LHS.Implicit where

import Prelude hiding (null)

import Control.Monad.Except
import Control.Monad.IO.Class

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.TypeChecking.Monad
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad

import Agda.Utils.Impossible

implicitP :: ArgInfo -> NamedArg A.Pattern
implicitP :: ArgInfo -> NamedArg Pattern
implicitP ArgInfo
info = forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall e. PatInfo -> Pattern' e
A.WildP forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
PatRange forall a b. (a -> b) -> a -> b
$ forall a. Range' a
noRange

-- | Insert implicit patterns in a list of patterns.
--   Even if 'DontExpandLast', trailing SIZELT patterns are inserted.
insertImplicitPatterns
  :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
  => ExpandHidden -> [NamedArg A.Pattern]
  -> Telescope -> m [NamedArg A.Pattern]
insertImplicitPatterns :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
exh [NamedArg Pattern]
ps Telescope
tel =
  forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
exh [NamedArg Pattern]
ps (Telescope -> Type -> Type
telePi Telescope
tel HasCallStack => Type
__DUMMY_TYPE__)

-- | Insert trailing SizeLt patterns, if any.
insertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg A.Pattern]
insertImplicitSizeLtPatterns :: forall (m :: * -> *). PureTCM m => Type -> m [NamedArg Pattern]
insertImplicitSizeLtPatterns Type
t = do
  -- Testing for SizeLt.  In case of blocked type, we return no.
  -- We assume that on the LHS, we know the type.  (TODO: Sufficient?)
  Term -> Maybe BoundedSize
isSize <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  let isBounded :: BoundedSize -> Bool
isBounded BoundedSize
BoundedNo   = Bool
False
      isBounded BoundedLt{} = Bool
True
      isSizeLt :: Type -> m Bool
isSizeLt Type
t = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False BoundedSize -> Bool
isBounded forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
isSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t

  -- Search for the last SizeLt type among the hidden arguments.
  TelV Telescope
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let ts :: [Dom (ArgName, Type)]
ts = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
  [Dom (ArgName, Type)]
keep <- forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM (Bool -> Bool
not forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Type -> m Bool
isSizeLt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom (ArgName, Type)]
ts
  -- Insert implicit patterns upto (including) the last SizeLt type.
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (ArgInfo -> NamedArg Pattern
implicitP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> ArgInfo
domInfo) [Dom (ArgName, Type)]
keep

-- | Insert implicit patterns in a list of patterns.
--   Even if 'DontExpandLast', trailing SIZELT patterns are inserted.
insertImplicitPatternsT
  :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
  => ExpandHidden -> [NamedArg A.Pattern] -> Type
  -> m [NamedArg A.Pattern]
insertImplicitPatternsT :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
DontExpandLast [] Type
a = forall (m :: * -> *). PureTCM m => Type -> m [NamedArg Pattern]
insertImplicitSizeLtPatterns Type
a
insertImplicitPatternsT ExpandHidden
exh            [NamedArg Pattern]
ps Type
a = do
  TelV Telescope
tel Type
b <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensHiding a => a -> Bool
visible) Type
a
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
20 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"insertImplicitPatternsT"
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
             forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"b   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
         ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
70 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"insertImplicitPatternsT"
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Telescope
tel
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"b   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => ArgName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> ArgName
show) Type
b
         ]
  case [NamedArg Pattern]
ps of
    [] -> forall {m :: * -> *} {e} {t}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
insImp forall {e}. NamedArg (Pattern' e)
dummy Telescope
tel
    NamedArg Pattern
p : [NamedArg Pattern]
_ -> forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p forall a b. (a -> b) -> a -> b
$ do
      -- Andreas, 2015-05-11.
      -- If p is a projection pattern, make it visible for the purpose of
      -- calling insImp / insertImplicit, to get correct behavior.
      let p' :: NamedArg Pattern
p' = forall a. Bool -> (a -> a) -> a -> a
applyWhen (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p) (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) NamedArg Pattern
p
      [NamedArg Pattern]
hs <- forall {m :: * -> *} {e} {t}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
insImp NamedArg Pattern
p' Telescope
tel
      -- Continue with implicit patterns inserted before @p@.
      -- The list @hs ++ ps@ cannot be empty.
      let ps0 :: [NamedArg Pattern]
ps0@(~(NamedArg Pattern
p1 : [NamedArg Pattern]
ps1)) = [NamedArg Pattern]
hs forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps
      forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        -- If @a@ is a function (or path) type, continue inserting after @p1@.
        Left (Dom Type
dom, Abs Type
cod) -> forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
cod forall a b. (a -> b) -> a -> b
$ \Type
b ->
          (NamedArg Pattern
p1 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
exh [NamedArg Pattern]
ps1 Type
b
        -- Otherwise, we are done.
        Right{}     -> forall (m :: * -> *) a. Monad m => a -> m a
return [NamedArg Pattern]
ps0
  where
    dummy :: NamedArg (Pattern' e)
dummy = forall a. a -> NamedArg a
defaultNamedArg (forall e. BindName -> Pattern' e
A.VarP forall a. HasCallStack => a
__IMPOSSIBLE__)

    insImp :: NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
insImp NamedArg e
p Tele (Dom t)
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return []
    insImp NamedArg e
p Tele (Dom t)
tel = case forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg e
p forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom t)
tel of
      ImplicitInsertion
BadImplicits   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
      NoSuchName ArgName
x   -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
      ImpInsert [Dom ()]
n    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a}. LensArgInfo a => a -> NamedArg Pattern
implicitArg [Dom ()]
n

    implicitArg :: a -> NamedArg Pattern
implicitArg a
d = ArgInfo -> NamedArg Pattern
implicitP forall a b. (a -> b) -> a -> b
$ forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
d