{-# LANGUAGE PatternSynonyms #-}

{-| Functions for inserting implicit arguments at the right places.
-}
module Agda.TypeChecking.Implicit where

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

import Agda.Syntax.Position (beginningOf, getRange)
import Agda.Syntax.Common
import Agda.Syntax.Abstract (Binder, mkBinder_)
import Agda.Syntax.Internal as I

import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (unquoteTactic)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Telescope

import Agda.Utils.Functor
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Tuple

-- Cut and paste from insertImplicitPatternsT:

-- | Insert implicit binders in a list of binders, but not at the end.
insertImplicitBindersT
  :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
  => [NamedArg Binder]     -- ^ Should be non-empty, otherwise nothing happens.
  -> Type                  -- ^ Function type eliminated by arguments given by binders.
  -> m [NamedArg Binder] -- ^ Padded binders.
insertImplicitBindersT :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
[NamedArg Binder] -> Type -> m [NamedArg Binder]
insertImplicitBindersT = \case
  []     -> \ Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
  NamedArg Binder
b : [NamedArg Binder]
bs -> forall l. IsList l => l -> [Item l]
List1.toList forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
insertImplicitBindersT1 (NamedArg Binder
b forall a. a -> [a] -> NonEmpty a
:| [NamedArg Binder]
bs)

-- | Insert implicit binders in a list of binders, but not at the end.
insertImplicitBindersT1
  :: (PureTCM m, MonadError TCErr m, MonadFresh NameId m, MonadTrace m)
  => List1 (NamedArg Binder)        -- ^ Non-empty.
  -> Type                           -- ^ Function type eliminated by arguments given by binders.
  -> m (List1 (NamedArg Binder))  -- ^ Padded binders.
insertImplicitBindersT1 :: forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
 MonadTrace m) =>
List1 (NamedArg Binder) -> Type -> m (List1 (NamedArg Binder))
insertImplicitBindersT1 bs :: List1 (NamedArg Binder)
bs@(NamedArg Binder
b :| [NamedArg Binder]
_) Type
a = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Binder
b forall a b. (a -> b) -> a -> b
$ do
  TelV Tele (Dom Type)
tel Type
ty0 <- 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.term.lambda.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
"insertImplicitBindersT"
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"bs  = " 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg Binder)
bs
         , 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 Tele (Dom Type)
tel
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ty  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty0)
         ]
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda.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
"insertImplicitBindersT"
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"bs  = " 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List1.toList) List1 (NamedArg Binder)
bs
         , 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) Tele (Dom Type)
tel
         , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ty  = " 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
ty0
         ]
  [NamedArg Binder]
hs <- forall {m :: * -> *} {e} {t}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m,
 MonadFresh NameId m, HasRange e) =>
NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
insImp NamedArg Binder
b Tele (Dom Type)
tel
  -- Continue with implicit binders inserted before @b@.
  let bs0 :: List1 (NamedArg Binder)
bs0@(NamedArg Binder
b1 :| [NamedArg Binder]
bs1) = forall a. [a] -> NonEmpty a -> NonEmpty a
List1.prependList [NamedArg Binder]
hs List1 (NamedArg Binder)
bs
  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 @b1@.
    Left (Dom Type
_, Abs Type
ty) -> (NamedArg Binder
b1 forall a. a -> [a] -> NonEmpty 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) =>
[NamedArg Binder] -> Type -> m [NamedArg Binder]
insertImplicitBindersT [NamedArg Binder]
bs1 (forall a. Subst a => Abs a -> a
absBody Abs Type
ty)
    -- Otherwise, we are done.
    Right{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return List1 (NamedArg Binder)
bs0
  where
  insImp :: NamedArg e -> Tele (Dom t) -> m [NamedArg Binder]
insImp NamedArg e
b Tele (Dom t)
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return []
  insImp NamedArg e
b Tele (Dom t)
tel = case forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg e
b 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 ()]
doms -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Dom () -> m (NamedArg Binder)
implicitArg [Dom ()]
doms
      where
      implicitArg :: Dom () -> m (NamedArg Binder)
implicitArg Dom ()
d = forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ArgInfo -> a -> NamedArg a
unnamedArg (forall t e. Dom' t e -> ArgInfo
domInfo Dom ()
d) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Binder
mkBinder_ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName forall a b. (a -> b) -> a -> b
$ Range -> Range
beginningOf forall a b. (a -> b) -> a -> b
$ forall a. HasRange a => a -> Range
getRange NamedArg e
b

-- | @implicitArgs n expand t@ generates up to @n@ implicit argument
--   metas (unbounded if @n<0@), as long as @t@ is a function type
--   and @expand@ holds on the hiding info of its domain.

implicitArgs
  :: (PureTCM m, MonadMetaSolver m, MonadTCM m)
  => Int               -- ^ @n@, the maximum number of implicts to be inserted.
  -> (Hiding -> Bool)  -- ^ @expand@, the predicate to test whether we should keep inserting.
  -> Type              -- ^ The (function) type @t@ we are eliminating.
  -> m (Args, Type)  -- ^ The eliminating arguments and the remaining type.
implicitArgs :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m (Args, Type)
implicitArgs Int
n Hiding -> Bool
expand Type
t = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n (\ Hiding
h ArgName
x -> Hiding -> Bool
expand Hiding
h) Type
t

-- | @implicitNamedArgs n expand t@ generates up to @n@ named implicit arguments
--   metas (unbounded if @n<0@), as long as @t@ is a function type
--   and @expand@ holds on the hiding and name info of its domain.

implicitNamedArgs
  :: (PureTCM m, MonadMetaSolver m, MonadTCM m)
  => Int                          -- ^ @n@, the maximum number of implicts to be inserted.
  -> (Hiding -> ArgName -> Bool)  -- ^ @expand@, the predicate to test whether we should keep inserting.
  -> Type                         -- ^ The (function) type @t@ we are eliminating.
  -> m (NamedArgs, Type)        -- ^ The eliminating arguments and the remaining type.
implicitNamedArgs :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
0 Hiding -> ArgName -> Bool
expand Type
t0 = forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0)
implicitNamedArgs Int
n Hiding -> ArgName -> Bool
expand Type
t0 = do
    Type
t0' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t0
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"implicitNamedArgs" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0'
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args" Int
80 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"implicitNamedArgs" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show Type
t0')
    case forall t a. Type'' t a -> a
unEl Type
t0' of
      Pi dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, domTactic :: forall t e. Dom' t e -> Maybe t
domTactic = Maybe Term
tac, unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Abs Type
b
        | let x :: ArgName
x = forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Dom Type
dom, Hiding -> ArgName -> Bool
expand (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) ArgName
x -> do
          ArgInfo
info' <- if forall a. LensHiding a => a -> Bool
hidden ArgInfo
info then forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info else do
            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.ifs" Int
15 forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"inserting instance meta for type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
            forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.ifs" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"x      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show ArgName
x)
              , TCMT IO Doc
"hiding = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info)
              ]

            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => a -> a
makeInstance ArgInfo
info
          (MetaId
_, Term
v) <- forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg ArgInfo
info' ArgName
x Comparison
CmpLeq Type
a
          forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Term
tac forall a b. (a -> b) -> a -> b
$ \ Term
tac -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$
            forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$ Term -> Term -> Type -> TCMT IO ()
unquoteTactic Term
tac Term
v Type
a
          let narg :: Arg (Named NamedName Term)
narg = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (forall name a. Maybe name -> a -> Named name a
Named (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged ArgName
x) Term
v)
          forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Arg (Named NamedName Term)
narg forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> m ([Arg (Named NamedName Term)], Type)
implicitNamedArgs (Int
nforall a. Num a => a -> a -> a
-Int
1) Hiding -> ArgName -> Bool
expand (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
v)
      Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0')

-- | Create a metavariable according to the 'Hiding' info.

newMetaArg
  :: (PureTCM m, MonadMetaSolver m)
  => ArgInfo    -- ^ Kind/relevance of meta.
  -> ArgName    -- ^ Name suggestion for meta.
  -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the type.
  -> Type       -- ^ Type of meta.
  -> m (MetaId, Term)  -- ^ The created meta as id and as term.
newMetaArg :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg ArgInfo
info ArgName
x Comparison
cmp Type
a = do
  Either Blocker Bool
prp <- forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
a
  let irrelevantIfProp :: m (MetaId, Term) -> m (MetaId, Term)
irrelevantIfProp =
        if Either Blocker Bool
prp forall a. Eq a => a -> a -> Bool
== forall a b. b -> Either a b
Right Bool
True
        then forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
Irrelevant
        else forall a. a -> a
id
  forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$ m (MetaId, Term) -> m (MetaId, Term)
irrelevantIfProp forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadMetaSolver m =>
Hiding -> ArgName -> Type -> m (MetaId, Term)
newMeta (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgName -> ArgName
argNameToString ArgName
x) Type
a
  where
    newMeta :: MonadMetaSolver m => Hiding -> String -> Type -> m (MetaId, Term)
    newMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Hiding -> ArgName -> Type -> m (MetaId, Term)
newMeta Instance{} ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
ArgName -> Type -> m (MetaId, Term)
newInstanceMeta ArgName
n
    newMeta Hiding
Hidden     ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
    newMeta Hiding
NotHidden  ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp

-- | Create a questionmark according to the 'Hiding' info.

newInteractionMetaArg
  :: ArgInfo    -- ^ Kind/relevance of meta.
  -> ArgName    -- ^ Name suggestion for meta.
  -> Comparison -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the type.
  -> Type       -- ^ Type of meta.
  -> TCM (MetaId, Term)  -- ^ The created meta as id and as term.
newInteractionMetaArg :: ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg ArgInfo
info ArgName
x Comparison
cmp Type
a = do
  forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info forall a b. (a -> b) -> a -> b
$
    Hiding -> ArgName -> Type -> TCM (MetaId, Term)
newMeta (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgName -> ArgName
argNameToString ArgName
x) Type
a
  where
    newMeta :: Hiding -> String -> Type -> TCM (MetaId, Term)
    newMeta :: Hiding -> ArgName -> Type -> TCM (MetaId, Term)
newMeta Instance{} ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
ArgName -> Type -> m (MetaId, Term)
newInstanceMeta ArgName
n
    newMeta Hiding
Hidden     ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp
    newMeta Hiding
NotHidden  ArgName
n = forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> m (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp

---------------------------------------------------------------------------

-- | Possible results of 'insertImplicit'.
data ImplicitInsertion
      = ImpInsert [Dom ()] -- ^ Success: this many implicits have to be inserted (list can be empty).
      | BadImplicits       -- ^ Error: hidden argument where there should have been a non-hidden argument.
      | NoSuchName ArgName -- ^ Error: bad named argument.
  deriving (Int -> ImplicitInsertion -> ArgName -> ArgName
[ImplicitInsertion] -> ArgName -> ArgName
ImplicitInsertion -> ArgName
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
showList :: [ImplicitInsertion] -> ArgName -> ArgName
$cshowList :: [ImplicitInsertion] -> ArgName -> ArgName
show :: ImplicitInsertion -> ArgName
$cshow :: ImplicitInsertion -> ArgName
showsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
$cshowsPrec :: Int -> ImplicitInsertion -> ArgName -> ArgName
Show)

pattern NoInsertNeeded :: ImplicitInsertion
pattern $bNoInsertNeeded :: ImplicitInsertion
$mNoInsertNeeded :: forall {r}. ImplicitInsertion -> ((# #) -> r) -> ((# #) -> r) -> r
NoInsertNeeded = ImpInsert []

-- | If the next given argument is @a@ and the expected arguments are @ts@
--   @insertImplicit' a ts@ returns the prefix of @ts@ that precedes @a@.
--
--   If @a@ is named but this name does not appear in @ts@, the 'NoSuchName' exception is thrown.
--
insertImplicit
  :: NamedArg e  -- ^ Next given argument @a@.
  -> [Dom a]     -- ^ Expected arguments @ts@.
  -> ImplicitInsertion
insertImplicit :: forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg e
a [Dom a]
doms = forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
insertImplicit' NamedArg e
a forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom a]
doms forall a b. (a -> b) -> a -> b
$ \ Dom a
dom ->
    Dom a
dom forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Dom a
dom

-- | If the next given argument is @a@ and the expected arguments are @ts@
--   @insertImplicit' a ts@ returns the prefix of @ts@ that precedes @a@.
--
--   If @a@ is named but this name does not appear in @ts@, the 'NoSuchName' exception is thrown.
--
insertImplicit'
  :: NamedArg e     -- ^ Next given argument @a@.
  -> [Dom ArgName]  -- ^ Expected arguments @ts@.
  -> ImplicitInsertion
insertImplicit' :: forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
insertImplicit' NamedArg e
_ [] = ImplicitInsertion
BadImplicits
insertImplicit' NamedArg e
a [Dom ArgName]
ts

  -- If @a@ is visible, then take the non-visible prefix of @ts@.
  | forall a. LensHiding a => a -> Bool
visible NamedArg e
a = [Dom ()] -> ImplicitInsertion
ImpInsert forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
takeWhile forall a. LensHiding a => a -> Bool
notVisible forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom ArgName]
ts

  -- If @a@ is named, take prefix of @ts@ until the name of @a@ (with correct hiding).
  -- If the name is not found, throw exception 'NoSuchName'.
  | Just ArgName
x <- forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg e
a = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArgName -> ImplicitInsertion
NoSuchName ArgName
x) [Dom ()] -> ImplicitInsertion
ImpInsert forall a b. (a -> b) -> a -> b
$
      (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (\ Dom ArgName
t -> ArgName
x forall a. Eq a => a -> a -> Bool
== forall t e. Dom' t e -> e
unDom Dom ArgName
t Bool -> Bool -> Bool
&& forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a Dom ArgName
t) [Dom ArgName]
ts

  -- If @a@ is neither visible nor named, take prefix of @ts@ with different hiding than @a@.
  | Bool
otherwise = forall b a. b -> (a -> b) -> Maybe a -> b
maybe ImplicitInsertion
BadImplicits [Dom ()] -> ImplicitInsertion
ImpInsert forall a b. (a -> b) -> a -> b
$
      (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a) [Dom ArgName]
ts

    where
    -- @takeHiddenUntil p ts@ returns the 'getHiding' of the prefix of @ts@
    -- until @p@ holds or a visible argument is encountered.
    -- If @p@ never holds, 'Nothing' is returned.
    --
    --   Precondition: @p@ should imply @not . visible@.
    takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
    takeHiddenUntil :: (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil Dom ArgName -> Bool
p [Dom ArgName]
ts =
      case [Dom ArgName]
ts2 of
        []      -> forall a. Maybe a
Nothing  -- Predicate was never true
        (Dom ArgName
t : [Dom ArgName]
_) -> if forall a. LensHiding a => a -> Bool
visible Dom ArgName
t then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom ArgName]
ts1
      where
      ([Dom ArgName]
ts1, [Dom ArgName]
ts2) = forall a. (a -> Bool) -> [a] -> ([a], [a])
break (\ Dom ArgName
t -> Dom ArgName -> Bool
p Dom ArgName
t Bool -> Bool -> Bool
|| forall a. LensHiding a => a -> Bool
visible Dom ArgName
t) [Dom ArgName]
ts