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_ 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_ Pattern -> NamedArg Pattern)
-> Named_ Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Named_ Pattern
forall a name. a -> Named name a
unnamed (Pattern -> Named_ Pattern) -> Pattern -> Named_ 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 :: 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 =
  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 :: 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?)
  isSize <- m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  let isBounded BoundedSize
BoundedNo   = Bool
False
      isBounded BoundedLt{} = Bool
True
      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 tel _ <- telView t
  let 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
  keep <- dropWhileEndM (not <.> isSizeLt . snd . unDom) ts
  -- Insert implicit patterns upto (including) the last SizeLt type.
  return $ map (implicitP . domInfo) 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 = 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 tel 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
  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
    [] -> 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 b a. IsBool b => b -> (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
      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@(~(p1 : ps1)) = hs ++ ps
      reduce a >>= piOrPath >>= \case
        -- If @a@ is a function (or path) type, continue inserting after @p1@.
        Left (Dom Type
dom, Abs Type
cod) -> Dom Type
-> Abs Type
-> (Type -> m [NamedArg Pattern])
-> m [NamedArg Pattern]
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction Dom Type
dom Abs Type
cod ((Type -> m [NamedArg Pattern]) -> m [NamedArg Pattern])
-> (Type -> m [NamedArg Pattern]) -> m [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ \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 Type
b
        -- Otherwise, we are done.
        Right{}     -> [NamedArg Pattern] -> m [NamedArg Pattern]
forall a. a -> m a
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 a. a -> m a
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 a. a -> m a
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