{-# LANGUAGE PatternSynonyms #-}

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

import Prelude hiding (null)

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

import Data.Bifunctor (first)
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

import Mikan.Syntax.Position (HasRange, beginningOf, getRange)
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Abstract (Binder, mkBinder_)
import Mikan.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta) )
import Mikan.Syntax.Internal as I

import {-# SOURCE #-} Mikan.TypeChecking.MetaVars
import {-# SOURCE #-} Mikan.TypeChecking.Rules.Term (unquoteTactic)
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Pretty.Constraint ()  -- PrettyTCM Constraint instance only
import Mikan.TypeChecking.Telescope

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

import Mikan.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 (ArgName, Type)] -> ImplicitInsertion
forall e a. NamedArg e -> [Dom a] -> ImplicitInsertion
insertImplicit NamedArg a
narg ([Dom (ArgName, Type)] -> ImplicitInsertion)
-> [Dom (ArgName, Type)] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel of
      ImplicitInsertion
BadImplicits   -> TypeError -> TCM (Telescope, Type)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM (Telescope, Type))
-> TypeError -> TCM (Telescope, Type)
forall a b. (a -> b) -> a -> b
$ Hiding -> TypeError
WrongHidingInLHS (Hiding -> TypeError) -> Hiding -> TypeError
forall a b. (a -> b) -> a -> b
$ NamedArg a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg a
narg
      NoSuchName ArgName
x   -> TypeError -> TCM (Telescope, Type)
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM (Telescope, Type))
-> TypeError -> TCM (Telescope, Type)
forall a b. (a -> b) -> a -> b
$ Hiding -> TypeError
WrongHidingInLHS (Hiding -> TypeError) -> Hiding -> TypeError
forall a b. (a -> b) -> a -> b
$ NamedArg a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg a
narg
      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 -> ArgName -> Bool)
-> Type
-> TCMT IO ([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 ::
     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 -> ArgName -> Bool)
-> Type
-> TCMT IO ([Arg (Named NamedName Term)], Type)
implicitNamedArgs Int
n Hiding -> ArgName -> Bool
expand Type
t0 = do
  (ncas, t) <- Int
-> (Hiding -> ArgName -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
n Hiding -> ArgName -> Bool
expand Type
t0
  let (ns, cas) = List.unzipWith (\ (Named Maybe NamedName
n CheckedArg
ca) -> (Maybe NamedName
n, CheckedArg
ca)) ncas
      es = (CheckedArg -> Elim) -> [CheckedArg] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map' CheckedArg -> Elim
caElim [CheckedArg]
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)

-- | @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 -> ArgName -> Bool)
-> Type
-> TCM ([Named_ CheckedArg], Type)
implicitCheckedArgs Int
0 Hiding -> ArgName -> 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 -> ArgName -> 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 :: ArgName
x = ArgName -> Dom Type -> ArgName
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"_" Dom Type
dom, Hiding -> ArgName -> 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)) ArgName
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
            VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
            VerboseKey -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"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
<+> VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (ArgName -> VerboseKey
forall a. Show a => a -> VerboseKey
show ArgName
x)
              , TCMT IO Doc
"hiding = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (Hiding -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Hiding -> VerboseKey) -> Hiding -> VerboseKey
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 a
          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
            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 ArgName -> NamedName
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> NamedName) -> Ranged ArgName -> NamedName
forall a b. (a -> b) -> a -> b
$ ArgName -> Ranged ArgName
forall a. a -> Ranged a
unranged ArgName
x
          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 }
          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')

-- | Create a metavariable of 'MetaKind'.

newMetaArg ::
     MetaKind          -- ^ Kind 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.
newMetaArg :: MetaKind -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newMetaArg MetaKind
kind ArgName
x Comparison
cmp Type
a = do
  ArgName -> MetaKind -> Type -> TCM (MetaId, Term)
newMeta (ArgName -> ArgName
argNameToString ArgName
x) MetaKind
kind Type
a
  where
    newMeta :: ShortText -> MetaKind -> Type -> TCM (MetaId, Term)
    newMeta :: ArgName -> MetaKind -> Type -> TCM (MetaId, Term)
newMeta ArgName
n = \case
      MetaKind
InstanceMeta    -> ArgName -> Type -> TCM (MetaId, Term)
newInstanceMeta ArgName
n
      MetaKind
UnificationMeta -> RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
RunMetaOccursCheck ArgName
n Comparison
cmp

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

newInteractionMetaArg
  :: 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 :: ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg ArgName
x Comparison
cmp Type
a = do
  RunMetaOccursCheck
-> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
RunMetaOccursCheck (ArgName -> ArgName
argNameToString ArgName
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 -> ShowS
[ImplicitInsertion] -> ShowS
ImplicitInsertion -> VerboseKey
(Int -> ImplicitInsertion -> ShowS)
-> (ImplicitInsertion -> VerboseKey)
-> ([ImplicitInsertion] -> ShowS)
-> Show ImplicitInsertion
forall a.
(Int -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ImplicitInsertion -> ShowS
showsPrec :: Int -> ImplicitInsertion -> ShowS
$cshow :: ImplicitInsertion -> VerboseKey
show :: ImplicitInsertion -> VerboseKey
$cshowList :: [ImplicitInsertion] -> ShowS
showList :: [ImplicitInsertion] -> ShowS
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 = NamedArg e -> [Dom ArgName] -> ImplicitInsertion
forall e. NamedArg e -> [Dom ArgName] -> ImplicitInsertion
insertImplicit' NamedArg e
a ([Dom ArgName] -> ImplicitInsertion)
-> [Dom ArgName] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
  [Dom a]
doms [Dom a] -> (Dom a -> Dom ArgName) -> [Dom ArgName]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Dom a
dom ->
    Dom a
dom Dom a -> ArgName -> Dom ArgName
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ArgName -> Dom a -> ArgName
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@.
  | 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 ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom ArgName -> Dom ()
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 <- NamedArg e -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg e
a = ImplicitInsertion
-> ([Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()]
-> ImplicitInsertion
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (ArgName -> ImplicitInsertion
NoSuchName ArgName
x) [Dom ()] -> ImplicitInsertion
ImpInsert (Maybe [Dom ()] -> ImplicitInsertion)
-> Maybe [Dom ()] -> ImplicitInsertion
forall a b. (a -> b) -> a -> b
$
      (Dom ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (\ Dom ArgName
t -> ArgName
x ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== Dom ArgName -> ArgName
forall t e. Dom' t e -> e
unDom Dom ArgName
t Bool -> Bool -> Bool
&& NamedArg e -> Dom ArgName -> 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 = 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 ArgName -> Bool) -> [Dom ArgName] -> Maybe [Dom ()]
takeHiddenUntil (NamedArg e -> Dom ArgName -> Bool
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
        []      -> Maybe [Dom ()]
forall a. Maybe a
Nothing  -- Predicate was never true
        (Dom ArgName
t : [Dom ArgName]
_) -> if Dom ArgName -> Bool
forall a. LensHiding a => a -> Bool
visible Dom ArgName
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 ArgName -> Dom ()) -> [Dom ArgName] -> [Dom ()]
forall a b. (a -> b) -> [a] -> [b]
map' Dom ArgName -> Dom ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void [Dom ArgName]
ts1
      where
      (![Dom ArgName]
ts1, ![Dom ArgName]
ts2) = (Dom ArgName -> Bool)
-> [Dom ArgName] -> ([Dom ArgName], [Dom ArgName])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break' (\ Dom ArgName
t -> Dom ArgName -> Bool
p Dom ArgName
t Bool -> Bool -> Bool
|| Dom ArgName -> Bool
forall a. LensHiding a => a -> Bool
visible Dom ArgName
t) [Dom ArgName]
ts