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 = ArgInfo -> Named NamedName Pattern -> NamedArg Pattern
forall e. ArgInfo -> e -> Arg e
Arg (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) (Named NamedName Pattern -> NamedArg Pattern)
-> Named NamedName Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named NamedName Pattern)
-> Pattern -> Named NamedName Pattern
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern
forall e. PatInfo -> Pattern' e
A.WildP (PatInfo -> Pattern) -> PatInfo -> Pattern
forall a b. (a -> b) -> a -> b
$ Range -> PatInfo
PatRange (Range -> PatInfo) -> Range -> PatInfo
forall a b. (a -> b) -> a -> b
$ Range
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 :: ExpandHidden
-> [NamedArg Pattern] -> Telescope -> m [NamedArg Pattern]
insertImplicitPatterns ExpandHidden
exh [NamedArg Pattern]
ps Telescope
tel =
  ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
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 Type
HasCallStack => Type
__DUMMY_TYPE__)

-- | Insert trailing SizeLt patterns, if any.
insertImplicitSizeLtPatterns :: PureTCM m => Type -> m [NamedArg A.Pattern]
insertImplicitSizeLtPatterns :: 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 <- m (Term -> Maybe BoundedSize)
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 = Bool -> (BoundedSize -> Bool) -> Maybe BoundedSize -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False BoundedSize -> Bool
isBounded (Maybe BoundedSize -> Bool)
-> (Type -> Maybe BoundedSize) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
isSize (Term -> Maybe BoundedSize)
-> (Type -> Term) -> Type -> Maybe BoundedSize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Bool) -> m Type -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Type
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
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
  let ts :: [Dom (ArgName, Type)]
ts = (Dom (ArgName, Type) -> Bool)
-> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool)
-> (Dom (ArgName, Type) -> Bool) -> Dom (ArgName, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> Bool
forall a. LensHiding a => a -> Bool
visible) ([Dom (ArgName, Type)] -> [Dom (ArgName, Type)])
-> [Dom (ArgName, Type)] -> [Dom (ArgName, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
  [Dom (ArgName, Type)]
keep <- (Dom (ArgName, Type) -> m Bool)
-> [Dom (ArgName, Type)] -> m [Dom (ArgName, Type)]
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m [a]
dropWhileEndM (Bool -> Bool
not (Bool -> Bool)
-> (Dom (ArgName, Type) -> m Bool) -> Dom (ArgName, Type) -> m Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Type -> m Bool
isSizeLt (Type -> m Bool)
-> (Dom (ArgName, Type) -> Type) -> Dom (ArgName, Type) -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type)
-> (Dom (ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> (ArgName, Type)
forall t e. Dom' t e -> e
unDom) [Dom (ArgName, Type)]
ts
  -- Insert implicit patterns upto (including) the last SizeLt type.
  [NamedArg Pattern] -> m [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return ([NamedArg Pattern] -> m [NamedArg Pattern])
-> [NamedArg Pattern] -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ (Dom (ArgName, Type) -> NamedArg Pattern)
-> [Dom (ArgName, Type)] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map (ArgInfo -> NamedArg Pattern
implicitP (ArgInfo -> NamedArg Pattern)
-> (Dom (ArgName, Type) -> ArgInfo)
-> Dom (ArgName, Type)
-> NamedArg Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> ArgInfo
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 :: ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
insertImplicitPatternsT ExpandHidden
DontExpandLast [] Type
a = Type -> m [NamedArg Pattern]
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 <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
a
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"insertImplicitPatternsT"
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
             TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
brackets (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> [TCM Doc] -> [TCM Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCM Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCM Doc] -> [TCM Doc]) -> [TCM Doc] -> [TCM Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg Pattern -> TCM Doc) -> [NamedArg Pattern] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
ps
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"b   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b)
         ]
  ArgName -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.lhs.imp" Int
70 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCM Doc
"insertImplicitPatternsT"
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc)
-> ([NamedArg Pattern] -> ArgName) -> [NamedArg Pattern] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg Pattern] -> ArgName
forall a. Show a => a -> ArgName
show) [NamedArg Pattern]
ps
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc)
-> (Telescope -> ArgName) -> Telescope -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ArgName
forall a. Show a => a -> ArgName
show) Telescope
tel
         , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"b   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCM Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Type -> ArgName) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ArgName
forall a. Show a => a -> ArgName
show) Type
b
         ]
  case [NamedArg Pattern]
ps of
    [] -> NamedArg (Pattern' Any) -> Telescope -> m [NamedArg Pattern]
forall (m :: * -> *) e t.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
NamedArg e -> Tele (Dom t) -> m [NamedArg Pattern]
insImp NamedArg (Pattern' Any)
forall e. NamedArg (Pattern' e)
dummy Telescope
tel
    NamedArg Pattern
p : [NamedArg Pattern]
_ -> NamedArg Pattern -> m [NamedArg Pattern] -> m [NamedArg Pattern]
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Pattern
p (m [NamedArg Pattern] -> m [NamedArg Pattern])
-> m [NamedArg Pattern] -> m [NamedArg Pattern]
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' = Bool
-> (NamedArg Pattern -> NamedArg Pattern)
-> NamedArg Pattern
-> NamedArg Pattern
forall a. Bool -> (a -> a) -> a -> a
applyWhen (Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (ProjOrigin, AmbiguousQName) -> Bool)
-> Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
A.isProjP NamedArg Pattern
p) (Hiding -> NamedArg Pattern -> NamedArg Pattern
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden) NamedArg Pattern
p
      [NamedArg Pattern]
hs <- NamedArg Pattern -> Telescope -> m [NamedArg Pattern]
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 [NamedArg Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern]
ps
      Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a m Type
-> (Type -> m (Either (Dom Type, Abs Type) Type))
-> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> m (Either (Dom Type, Abs Type) Type)
forall (m :: * -> *).
HasBuiltins m =>
Type -> m (Either (Dom Type, Abs Type) Type)
piOrPath m (Either (Dom Type, Abs Type) Type)
-> (Either (Dom Type, Abs Type) Type -> m [NamedArg Pattern])
-> m [NamedArg Pattern]
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
_, Abs Type
b) -> (NamedArg Pattern
p1 NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
:) ([NamedArg Pattern] -> [NamedArg Pattern])
-> m [NamedArg Pattern] -> m [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpandHidden -> [NamedArg Pattern] -> Type -> m [NamedArg Pattern]
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 (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b)
        -- Otherwise, we are done.
        Right{}     -> [NamedArg Pattern] -> m [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return [NamedArg Pattern]
ps0
  where
    dummy :: NamedArg (Pattern' e)
dummy = Pattern' e -> NamedArg (Pattern' e)
forall a. a -> NamedArg a
defaultNamedArg (BindName -> Pattern' e
forall e. BindName -> Pattern' e
A.VarP BindName
forall a. HasCallStack => a
__IMPOSSIBLE__)

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

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