{-# LANGUAGE PatternSynonyms #-}

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

import Prelude hiding (null)

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

import Data.Bifunctor (first)

import Agda.Syntax.Position (HasRange, beginningOf, getRange)
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Abstract (Binder, mkBinder_)
import Agda.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta) )
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.Pretty.Constraint ()  -- PrettyTCM Constraint instance only
import Agda.TypeChecking.Telescope

import Agda.Utils.Function (applyWhen, applyWhenJust)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List qualified as List
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List1 qualified as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Tuple

import Agda.Utils.Impossible

-- Cut and paste from insertImplicitPatternsT:

-- | Split a given Pi 'Type' until you reach the given named argument,
-- returning the number of arguments skipped to reach the right plicity
-- and name.
splitImplicitBinderT :: HasRange a => NamedArg a -> Type -> TCM (Telescope, Type)
splitImplicitBinderT :: forall a. HasRange a => NamedArg a -> Type -> TCM (Telescope, Type)
splitImplicitBinderT Arg (Named_ a)
narg Type
ty = do
  -- Split off any invisible arguments at the front (so if the first
  -- argument is visible, return tel = EmptyTel)
  TelV tel ty0 <- Int -> (Dom' Term Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom' Term Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool)
-> (Dom' Term Type -> Bool) -> Dom' Term Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
ty

  case tel of
    -- If we didn't lob off any arguments then we can use the original
    -- type and the empty telescope
    Telescope
EmptyTel -> (Telescope, Type) -> TCM (Telescope, Type)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Telescope
forall a. Tele a
EmptyTel, Type
ty)

    -- Otherwise we try inserting implicit arguments.
    Telescope
_ -> Arg (Named_ a) -> TCM (Telescope, Type) -> TCM (Telescope, Type)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Arg (Named_ a)
narg case Arg (Named_ a) -> [Dom ([Char], Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit Arg (Named_ a)
narg ([Dom ([Char], Type)] -> ImplicitInsertion)
-> [Dom ([Char], Type)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel of
      ImplicitInsertion
BadImplicits   -> TypeError -> TCM (Telescope, Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
      NoSuchName [Char]
x   -> TypeError -> TCM (Telescope, Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
      ImpInsert [Dom ()]
doms ->
        let (Telescope
here, Telescope
there) = Int -> Telescope -> (Telescope, Telescope)
splitTelescopeAt ([Dom ()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ()]
doms) Telescope
tel
        in (Telescope, Type) -> TCM (Telescope, Type)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Telescope
here, Telescope -> Type -> Type
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
there Type
ty0)

-- | @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 ::
     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.
  -> TCM (Args, Type)    -- ^ The eliminating arguments and the remaining type.
implicitArgs :: Int -> (Hiding -> Bool) -> Type -> TCM (Args, Type)
implicitArgs Int
n Hiding -> Bool
expand Type
t = ([Arg (Named NamedName Term)] -> Args)
-> ([Arg (Named NamedName Term)], Type) -> (Args, Type)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Arg (Named NamedName Term) -> Arg Term)
-> [Arg (Named NamedName Term)] -> Args
forall a b. (a -> b) -> [a] -> [b]
map' ((Named NamedName Term -> Term)
-> Arg (Named NamedName Term) -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Term -> Term
forall name a. Named name a -> a
namedThing)) (([Arg (Named NamedName Term)], Type) -> (Args, Type))
-> TCMT IO ([Arg (Named NamedName Term)], Type) -> TCM (Args, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  Int
-> (Hiding -> [Char] -> Bool)
-> Type
-> TCMT IO ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n (\ Hiding
h [Char]
_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 ::
     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.
  -> TCM (NamedArgs, Type)          -- ^ The eliminating arguments and the remaining type.
implicitNamedArgs :: Int
-> (Hiding -> [Char] -> Bool)
-> Type
-> TCMT IO ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n Hiding -> [Char] -> Bool
expand Type
t0 = do
  (ncas, t) <- Int
-> (Hiding -> [Char] -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
n Hiding -> [Char] -> Bool
expand Type
t0
  let (ns, cas) = List.unzipWith (\ (Named Maybe NamedName
n CheckedArg
ca) -> (Maybe NamedName
n, CheckedArg
ca)) ncas
  es <- liftTCM $ noHeadConstraints cas
  let nargs = (Maybe NamedName -> Arg Term -> Arg (Named NamedName Term))
-> [Maybe NamedName] -> Args -> [Arg (Named NamedName Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\ Maybe NamedName
n (Arg ArgInfo
ai Term
v) -> ArgInfo -> Named NamedName Term -> Arg (Named NamedName Term)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Maybe NamedName -> Term -> Named NamedName Term
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
n Term
v)) [Maybe NamedName]
ns ([Elim] -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims [Elim]
es)
  return (nargs, t)

-- | Make sure there are no head constraints attached to the eliminations
-- and just return the eliminations.
noHeadConstraints :: [CheckedArg] -> TCM [Elim]
noHeadConstraints :: [CheckedArg] -> TCM [Elim]
noHeadConstraints = (CheckedArg -> TCMT IO Elim) -> [CheckedArg] -> TCM [Elim]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CheckedArg -> TCMT IO Elim
noHeadConstraint

noHeadConstraint :: CheckedArg -> TCM Elim
noHeadConstraint :: CheckedArg -> TCMT IO Elim
noHeadConstraint (CheckedArg Elim
elim Range' SrcFile
_  Maybe (Abs Constraint)
Nothing) = Elim -> TCMT IO Elim
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Elim
elim
noHeadConstraint (CheckedArg Elim
_ Range' SrcFile
range Just{} ) = do
  Range' SrcFile -> TCMT IO Elim -> TCMT IO Elim
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range' SrcFile
range do
    TypeError -> TCMT IO Elim
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Elim) -> TypeError -> TCMT IO Elim
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
NotSupported ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
     [Char]
"Lock constraints are not (yet) supported in this position."

-- | @implicitCheckedArgs 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.

implicitCheckedArgs ::
     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.
  -> TCM ([Named_ CheckedArg], Type)-- ^ The eliminating arguments and the remaining type.
implicitCheckedArgs :: Int
-> (Hiding -> [Char] -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
0 Hiding -> [Char] -> Bool
expand Type
t0 = ([Named_ CheckedArg], Type) -> TCM ([Named_ CheckedArg], Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0)
implicitCheckedArgs Int
n Hiding -> [Char] -> Bool
expand Type
t0 = do
    t0' <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t0
    reportSDoc "tc.term.args" 30 $ "implicitCheckedArgs" <+> prettyTCM t0'
    reportSDoc "tc.term.args" 80 $ "implicitCheckedArgs" <+> text (show t0')
    case unEl t0' of
      Pi dom :: Dom' Term Type
dom@(Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Abs Type
b
      -- Pi dom@Dom{domInfo = info, domTactic = mtac, unDom = a} b
        | let x :: [Char]
x = [Char] -> Dom' Term Type -> [Char]
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
[Char] -> a -> [Char]
bareNameWithDefault [Char]
"_" Dom' Term Type
dom, Hiding -> [Char] -> Bool
expand (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)) [Char]
x -> do
          kind <- if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
hidden (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) then MetaKind -> TCMT IO MetaKind
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MetaKind
UnificationMeta else do
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args.ifs" Int
15 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
              TCMT IO Doc
"inserting instance meta for type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
            [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.args.ifs" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"x      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
x)
              , TCMT IO Doc
"hiding = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Hiding -> [Char]
forall a. Show a => a -> [Char]
show (Hiding -> [Char]) -> Hiding -> [Char]
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo))
              ]

            MetaKind -> TCMT IO MetaKind
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return MetaKind
InstanceMeta
          (_, v) <- newMetaArg kind x CmpLeq dom
          whenJust (dom ^. dTactic) \ Term
tac -> TCMT IO () -> TCMT IO ()
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM do
            -- We don't need to do a full 'applyDomToContext' here.
            -- 'newMetaArg' already adds the local rewrite rule constraint
            Dom' Term Type -> TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Dom' Term Type
dom (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Type -> TCMT IO ()
unquoteTactic Term
tac Term
v Type
a
          let name = NamedName -> Maybe NamedName
forall a. a -> Maybe a
Just (NamedName -> Maybe NamedName) -> NamedName -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged [Char] -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged [Char] -> NamedName) -> Ranged [Char] -> NamedName
forall a b. (a -> b) -> a -> b
$ [Char] -> Ranged [Char]
forall a. a -> Ranged a
unranged [Char]
x
          mc <- liftTCM $ makeLockConstraint t0' v
          let carg = CheckedArg{ caElim :: Elim
caElim = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Term
v), caRange :: Range' SrcFile
caRange = Range' SrcFile
forall a. Null a => a
empty, caConstraint :: Maybe (Abs Constraint)
caConstraint = Maybe (Abs Constraint)
mc }
          first (Named name carg :) <$> implicitCheckedArgs (n-1) expand (absApp b v)
      Term
_ -> ([Named_ CheckedArg], Type) -> TCM ([Named_ CheckedArg], Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
t0')

-- | @makeLockConstraint u funType@(El _ (Pi (Dom{ domInfo=info, unDom=a }) _))@
--   creates a @CheckLockedVars@ constraint for lock @u : a@
--   if @getLock info == IsLock _@.
--
--   Precondition: 'Type' is reduced.
makeLockConstraint :: Type -> Term -> TCM (Maybe (Abs Constraint))
makeLockConstraint :: Type -> Term -> TCM (Maybe (Abs Constraint))
makeLockConstraint Type
funType Term
u =
  case Type
funType of
    El Sort' Term
_ (Pi dom :: Dom' Term Type
dom@(Dom' Term Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Abs Type
_) -> do
      let
        x :: [Char]
x  = [Char] -> (NamedName -> [Char]) -> Maybe NamedName -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"t" NamedName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Dom' Term Type
dom Dom' Term Type
-> Getting (Maybe NamedName) (Dom' Term Type) (Maybe NamedName)
-> Maybe NamedName
forall s a. s -> Getting a s a -> a
^. Getting (Maybe NamedName) (Dom' Term Type) (Maybe NamedName)
forall t e (f :: * -> *).
Functor f =>
(Maybe NamedName -> f (Maybe NamedName))
-> Dom' t e -> f (Dom' t e)
dName)
        mc :: Maybe (Abs Constraint)
mc = case ArgInfo -> Lock
forall a. LensLock a => a -> Lock
getLock (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) of
          IsLock{} -> Abs Constraint -> Maybe (Abs Constraint)
forall a. a -> Maybe a
Just (Abs Constraint -> Maybe (Abs Constraint))
-> Abs Constraint -> Maybe (Abs Constraint)
forall a b. (a -> b) -> a -> b
$ [Char] -> Constraint -> Abs Constraint
forall a. [Char] -> a -> Abs a
Abs [Char]
x (Constraint -> Abs Constraint) -> Constraint -> Abs Constraint
forall a b. (a -> b) -> a -> b
$
            Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars (Int -> Term
var Int
0) (Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
funType) (Int -> Arg Term -> Arg Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg (Dom' Term Type
dom Dom' Term Type
-> Getting ArgInfo (Dom' Term Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Term
u) (Int -> Type -> Type
forall a. Subst a => Int -> a -> a
raise Int
1 Type
a)
          Lock
IsNotLock -> Maybe (Abs Constraint)
forall a. Maybe a
Nothing
      Maybe (Abs Constraint)
-> (Abs Constraint -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe (Abs Constraint)
mc \ Abs Constraint
c -> do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.term.lock" Int
40 do
          Dom' Term Type -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Dom' Term Type -> m a -> m a
addContext (Type -> Dom' Term Type
forall a. a -> Dom a
defaultDom (Type -> Dom' Term Type) -> Type -> Dom' Term Type
forall a b. (a -> b) -> a -> b
$ Type
funType) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Abs Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Abs Constraint -> m Doc
prettyTCM Abs Constraint
c
      Maybe (Abs Constraint) -> TCM (Maybe (Abs Constraint))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Abs Constraint)
mc
    Type
_ -> Maybe (Abs Constraint) -> TCM (Maybe (Abs Constraint))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Abs Constraint)
forall a. Maybe a
Nothing

-- | Create a metavariable of 'MetaKind'.

newMetaArg ::
     MetaKind          -- ^ Kind of meta.
  -> ArgName           -- ^ Name suggestion for meta.
  -> Comparison        -- ^ Check (@CmpLeq@) or infer (@CmpEq@) the type.
  -> Dom Type          -- ^ Type of meta plus relevance and local rewrite info.
  -> TCM (MetaId, Term)  -- ^ The created meta as id and as term.
newMetaArg :: MetaKind
-> [Char] -> Comparison -> Dom' Term Type -> TCMT IO (MetaId, Term)
newMetaArg MetaKind
kind [Char]
x Comparison
cmp Dom' Term Type
a = do
  prp <- BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall (m :: * -> *) a. BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool))
-> BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> BlockT (TCMT IO) Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Dom' Term Type
a
  let irrelevantIfProp =
        Bool
-> (TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term)
-> TCMT IO (MetaId, Term)
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Either Blocker Bool
prp Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True) ((TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
 -> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
-> (TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term)
-> TCMT IO (MetaId, Term)
forall a b. (a -> b) -> a -> b
$ Relevance -> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
irrelevant
  applyDomToContext a $ irrelevantIfProp $
    newMeta (argNameToString x) kind (unDom a)
  where
    newMeta :: String -> MetaKind -> Type -> TCM (MetaId, Term)
    newMeta :: [Char] -> MetaKind -> Type -> TCMT IO (MetaId, Term)
newMeta [Char]
n = \case
      MetaKind
InstanceMeta    -> [Char] -> Type -> TCMT IO (MetaId, Term)
newInstanceMeta [Char]
n
      MetaKind
UnificationMeta -> RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck [Char]
n Comparison
cmp

-- | Create a questionmark (always 'UnificationMeta').

newInteractionMetaArg
  :: ArgInfo    -- ^ 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 -> [Char] -> Comparison -> Type -> TCMT IO (MetaId, Term)
newInteractionMetaArg ArgInfo
info [Char]
x Comparison
cmp Type
a = do
  ArgInfo -> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
    RunMetaOccursCheck
-> [Char] -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck ([Char] -> [Char]
argNameToString [Char]
x) Comparison
cmp Type
a

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

-- | 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 -> [Char] -> [Char]
[ImplicitInsertion] -> [Char] -> [Char]
ImplicitInsertion -> [Char]
(Int -> ImplicitInsertion -> [Char] -> [Char])
-> (ImplicitInsertion -> [Char])
-> ([ImplicitInsertion] -> [Char] -> [Char])
-> Show ImplicitInsertion
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> ImplicitInsertion -> [Char] -> [Char]
showsPrec :: Int -> ImplicitInsertion -> [Char] -> [Char]
$cshow :: ImplicitInsertion -> [Char]
show :: ImplicitInsertion -> [Char]
$cshowList :: [ImplicitInsertion] -> [Char] -> [Char]
showList :: [ImplicitInsertion] -> [Char] -> [Char]
Show)

pattern NoInsertNeeded :: ImplicitInsertion
pattern $mNoInsertNeeded :: forall {r}. ImplicitInsertion -> ((# #) -> r) -> ((# #) -> r) -> r
$bNoInsertNeeded :: ImplicitInsertion
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' Term a]
doms = NamedArg e -> [Dom [Char]] -> ImplicitInsertion
forall e. NamedArg e -> [Dom [Char]] -> ImplicitInsertion
insertImplicit' NamedArg e
a ([Dom [Char]] -> ImplicitInsertion)
-> [Dom [Char]] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
  [Dom' Term a] -> (Dom' Term a -> Dom [Char]) -> [Dom [Char]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom' Term a]
doms ((Dom' Term a -> Dom [Char]) -> [Dom [Char]])
-> (Dom' Term a -> Dom [Char]) -> [Dom [Char]]
forall a b. (a -> b) -> a -> b
$ \ Dom' Term a
dom ->
    Dom' Term a
dom Dom' Term a -> [Char] -> Dom [Char]
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> [Char] -> Dom' Term a -> [Char]
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
[Char] -> a -> [Char]
bareNameWithDefault [Char]
"_" Dom' Term 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 [Char]] -> ImplicitInsertion
insertImplicit' Arg (Named_ e)
_ [] = ImplicitInsertion
BadImplicits
insertImplicit' Arg (Named_ e)
a [Dom [Char]]
ts

  -- If @a@ is visible, then take the non-visible prefix of @ts@.
  | Arg (Named_ e) -> Bool
forall a. LensHiding a => a -> Bool
visible Arg (Named_ e)
a = [Dom ()] -> ImplicitInsertion
ImpInsert ([Dom ()] -> ImplicitInsertion) -> [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$! (Dom () -> Bool) -> [Dom ()] -> [Dom ()]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile' Dom () -> Bool
forall a. LensHiding a => a -> Bool
notVisible ([Dom ()] -> [Dom ()]) -> [Dom ()] -> [Dom ()]
forall a b. (a -> b) -> a -> b
$ (Dom [Char] -> Dom ()) -> [Dom [Char]] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom [Char] -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom [Char]]
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 [Char]
x <- Arg (Named_ e) -> Maybe [Char]
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe [Char]
bareNameOf Arg (Named_ e)
a = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Char] -> ImplicitInsertion
NoSuchName [Char]
x) [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
      (Dom [Char] -> Bool) -> [Dom [Char]] -> Maybe [Dom ()]
takeHiddenUntil (\ Dom [Char]
t -> [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Dom [Char] -> [Char]
forall t e. Dom' t e -> e
unDom Dom [Char]
t Bool -> Bool -> Bool
&& Arg (Named_ e) -> Dom [Char] -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg (Named_ e)
a Dom [Char]
t) [Dom [Char]]
ts

  -- If @a@ is neither visible nor named, take prefix of @ts@ with different hiding than @a@.
  | Bool
otherwise = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ImplicitInsertion
BadImplicits [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
      (Dom [Char] -> Bool) -> [Dom [Char]] -> Maybe [Dom ()]
takeHiddenUntil (Arg (Named_ e) -> Dom [Char] -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Arg (Named_ e)
a) [Dom [Char]]
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 [Char] -> Bool) -> [Dom [Char]] -> Maybe [Dom ()]
takeHiddenUntil Dom [Char] -> Bool
p [Dom [Char]]
ts =
      case [Dom [Char]]
ts2 of
        []      -> Maybe [Dom ()]
forall a. Maybe a
Nothing  -- Predicate was never true
        (Dom [Char]
t : [Dom [Char]]
_) -> if Dom [Char] -> Bool
forall a. LensHiding a => a -> Bool
visible Dom [Char]
t then Maybe [Dom ()]
forall a. Maybe a
Nothing else [Dom ()] -> Maybe [Dom ()]
forall a. a -> Maybe a
Just ([Dom ()] -> Maybe [Dom ()]) -> [Dom ()] -> Maybe [Dom ()]
forall a b. (a -> b) -> a -> b
$! (Dom [Char] -> Dom ()) -> [Dom [Char]] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom [Char] -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom [Char]]
ts1
      where
      (![Dom [Char]]
ts1, ![Dom [Char]]
ts2) = (Dom [Char] -> Bool)
-> [Dom [Char]] -> ([Dom [Char]], [Dom [Char]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break' (\ Dom [Char]
t -> Dom [Char] -> Bool
p Dom [Char]
t Bool -> Bool -> Bool
|| Dom [Char] -> Bool
forall a. LensHiding a => a -> Bool
visible Dom [Char]
t) [Dom [Char]]
ts