    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' (ZonkAny 0))
    -> 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' (ZonkAny 0))
    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