{-# 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 NamedArg 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 Type -> Bool) -> Type -> TCMT IO (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
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
_ -> NamedArg a -> TCM (Telescope, Type) -> TCM (Telescope, Type)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg a
narg case NamedArg a -> [Dom (String, Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg a
narg ([Dom (String, Type)] -> ImplicitInsertion)
-> [Dom (String, Type)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel of
      ImplicitInsertion
BadImplicits   -> TypeError -> TCM (Telescope, Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongHidingInLHS
      NoSuchName String
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 -> String -> Bool)
-> Type
-> TCMT IO ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n (\ Hiding
h String
_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 -> String -> Bool)
-> Type
-> TCMT IO ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n Hiding -> String -> Bool
expand Type
t0 = do
  (ncas, t) <- Int
-> (Hiding -> String -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
n Hiding -> String -> 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
_  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
range Just{} ) = do
  Range -> TCMT IO Elim -> TCMT IO Elim
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
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
$ String -> TypeError
NotSupported (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
     String
"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 -> String -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
0 Hiding -> String -> 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 -> String -> 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 Type
dom@(Dom 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 :: String
x = String -> Dom Type -> String
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
String -> a -> String
bareNameWithDefault String
"_" Dom Type
dom, Hiding -> String -> Bool
expand (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)) String
x -> do
          kind <- if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
hidden (Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom 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
            String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
            String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> String
forall a. Show a => a -> String
show String
x)
              , TCMT IO Doc
"hiding = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Hiding -> String
forall a. Show a => a -> String
show (Hiding -> String) -> Hiding -> String
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom 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 Type -> TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a m.
(MonadTCEnv tcm, ExpandCase (tcm a), LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Dom 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 String -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged String -> NamedName) -> Ranged String -> NamedName
forall a b. (a -> b) -> a -> b
$ String -> Ranged String
forall a. a -> Ranged a
unranged String
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 Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo) Term
v), caRange :: Range
caRange = Range
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 Type
dom@(Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
a) Abs Type
_) -> do
      let
        x :: String
x  = String -> (NamedName -> String) -> Maybe NamedName -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"t" NamedName -> String
forall a. Pretty a => a -> String
prettyShow (Dom Type
dom Dom Type
-> Getting (Maybe NamedName) (Dom Type) (Maybe NamedName)
-> Maybe NamedName
forall s a. s -> Getting a s a -> a
^. Getting (Maybe NamedName) (Dom 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 Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom 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
$ String -> Constraint -> Abs Constraint
forall a. String -> a -> Abs a
Abs String
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 Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom 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
        String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.term.lock" Int
40 do
          Dom 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 Type -> m a -> m a
addContext (Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> Type -> Dom 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
-> String -> Comparison -> Dom Type -> TCMT IO (MetaId, Term)
newMetaArg MetaKind
kind String
x Comparison
cmp Dom 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 Type -> BlockT (TCMT IO) Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Dom 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 :: String -> MetaKind -> Type -> TCMT IO (MetaId, Term)
newMeta String
n = \case
      MetaKind
InstanceMeta    -> String -> Type -> TCMT IO (MetaId, Term)
newInstanceMeta String
n
      MetaKind
UnificationMeta -> RunMetaOccursCheck
-> String -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck String
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 -> String -> Comparison -> Type -> TCMT IO (MetaId, Term)
newInteractionMetaArg ArgInfo
info String
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
-> String -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck (String -> String
argNameToString String
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 -> String -> String
[ImplicitInsertion] -> String -> String
ImplicitInsertion -> String
(Int -> ImplicitInsertion -> String -> String)
-> (ImplicitInsertion -> String)
-> ([ImplicitInsertion] -> String -> String)
-> Show ImplicitInsertion
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ImplicitInsertion -> String -> String
showsPrec :: Int -> ImplicitInsertion -> String -> String
$cshow :: ImplicitInsertion -> String
show :: ImplicitInsertion -> String
$cshowList :: [ImplicitInsertion] -> String -> String
showList :: [ImplicitInsertion] -> String -> String
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 a]
doms = NamedArg e -> [Dom String] -> ImplicitInsertion
forall e. NamedArg e -> [Dom String] -> ImplicitInsertion
insertImplicit' NamedArg e
a ([Dom String] -> ImplicitInsertion)
-> [Dom String] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
  [Dom a] -> (Dom a -> Dom String) -> [Dom String]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom a]
doms ((Dom a -> Dom String) -> [Dom String])
-> (Dom a -> Dom String) -> [Dom String]
forall a b. (a -> b) -> a -> b
$ \ Dom a
dom ->
    Dom a
dom Dom a -> String -> Dom String
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> String -> Dom a -> String
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
String -> a -> String
bareNameWithDefault String
"_" 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 String] -> ImplicitInsertion
insertImplicit' NamedArg e
_ [] = ImplicitInsertion
BadImplicits
insertImplicit' NamedArg e
a [Dom String]
ts

  -- If @a@ is visible, then take the non-visible prefix of @ts@.
  | NamedArg e -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg 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 String -> Dom ()) -> [Dom String] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom String -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom String]
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 String
x <- NamedArg e -> Maybe String
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf NamedArg e
a = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> ImplicitInsertion
NoSuchName String
x) [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
      (Dom String -> Bool) -> [Dom String] -> Maybe [Dom ()]
takeHiddenUntil (\ Dom String
t -> String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Dom String -> String
forall t e. Dom' t e -> e
unDom Dom String
t Bool -> Bool -> Bool
&& NamedArg e -> Dom String -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a Dom String
t) [Dom String]
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 String -> Bool) -> [Dom String] -> Maybe [Dom ()]
takeHiddenUntil (NamedArg e -> Dom String -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding NamedArg e
a) [Dom String]
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 String -> Bool) -> [Dom String] -> Maybe [Dom ()]
takeHiddenUntil Dom String -> Bool
p [Dom String]
ts =
      case [Dom String]
ts2 of
        []      -> Maybe [Dom ()]
forall a. Maybe a
Nothing  -- Predicate was never true
        (Dom String
t : [Dom String]
_) -> if Dom String -> Bool
forall a. LensHiding a => a -> Bool
visible Dom String
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 String -> Dom ()) -> [Dom String] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom String -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom String]
ts1
      where
      (![Dom String]
ts1, ![Dom String]
ts2) = (Dom String -> Bool)
-> [Dom String] -> ([Dom String], [Dom String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break' (\ Dom String
t -> Dom String -> Bool
p Dom String
t Bool -> Bool -> Bool
|| Dom String -> Bool
forall a. LensHiding a => a -> Bool
visible Dom String
t) [Dom String]
ts