{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.IApplyConfluence where

import Prelude hiding (null, (!!))  -- do not use partial functions like !!

import Control.Monad
import Control.Arrow (first,second)

import qualified Data.List as List
import qualified Data.Map as Map

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.Interaction.Options

import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Substitute

import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Maybe
import Agda.Utils.Size
import Agda.Utils.Impossible
import Agda.Utils.Functor


checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ QName
f = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool)
-> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  -- Andreas, 2019-03-27, iapply confluence should only be checked
  -- when --cubical or --erased-cubical is active. See
  -- test/Succeed/CheckIApplyConfluence.agda.
  -- We cannot reach the following crash point unless
  -- --cubical/--erased-cubical is active.
  VerboseKey -> VerboseLevel -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadTCM m, MonadDebug m) =>
VerboseKey -> VerboseLevel -> m ()
__CRASH_WHEN__ VerboseKey
"tc.cover.iapply.confluence.crash" VerboseLevel
666
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Checking IApply confluence of" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
  QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m) =>
QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode QName
f ((Definition -> TCM ()) -> TCM ())
-> (Definition -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Definition
d -> do
  case Definition -> Defn
theDef Definition
d of
    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cls', funCovering :: Defn -> [Clause]
funCovering = [Clause]
cls} -> do
      VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"length cls =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Clause] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Clause]
cls)
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Clause] -> Bool
forall a. Null a => a -> Bool
null [Clause]
cls Bool -> Bool -> Bool
&& Bool -> Bool
not ([VerboseLevel] -> Bool
forall a. Null a => a -> Bool
null ([VerboseLevel] -> Bool) -> [VerboseLevel] -> Bool
forall a b. (a -> b) -> a -> b
$ (Clause -> [VerboseLevel]) -> [Clause] -> [VerboseLevel]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NamedArg (Pattern' DBPatVar)] -> [VerboseLevel]
forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [VerboseLevel]
iApplyVars ([NamedArg (Pattern' DBPatVar)] -> [VerboseLevel])
-> (Clause -> [NamedArg (Pattern' DBPatVar)])
-> Clause
-> [VerboseLevel]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg (Pattern' DBPatVar)]
namedClausePats) [Clause]
cls')) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
f ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef
        ((Defn -> Defn) -> Definition -> Definition)
-> (Defn -> Defn) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering ([Clause] -> [Clause] -> [Clause]
forall a b. a -> b -> a
const [])

      Call -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [Clause] -> Bool -> Call
CheckFunDefCall (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
f) QName
f [] Bool
False) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        [Clause] -> (Clause -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Clause]
cls ((Clause -> TCM ()) -> TCM ()) -> (Clause -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> TCM ()
checkIApplyConfluence QName
f
    Defn
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | @addClause f (Clause {namedClausePats = ps})@ checks that @f ps@
-- reduces in a way that agrees with @IApply@ reductions.
checkIApplyConfluence :: QName -> Clause -> TCM ()
checkIApplyConfluence :: QName -> Clause -> TCM ()
checkIApplyConfluence QName
f Clause
cl = case Clause
cl of
      Clause {clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
Nothing} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Clause {clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
Nothing} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      cl :: Clause
cl@Clause { clauseTel :: Clause -> Telescope
clauseTel = Telescope
clTel
                , namedClausePats :: Clause -> [NamedArg (Pattern' DBPatVar)]
namedClausePats = [NamedArg (Pattern' DBPatVar)]
ps
                , clauseType :: Clause -> Maybe (Arg Type)
clauseType = Just Arg Type
t
                , clauseBody :: Clause -> Maybe Term
clauseBody = Just Term
body
                } -> Range -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
f) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          let
            trhs :: Type
trhs = Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
t
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
clTel
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ps =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg (Pattern' DBPatVar)] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg (Pattern' DBPatVar)]
ps
          [NamedArg (Pattern' DBPatVar)]
ps <- [NamedArg (Pattern' DBPatVar)]
-> TCMT IO [NamedArg (Pattern' DBPatVar)]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [NamedArg (Pattern' DBPatVar)]
ps
          [VerboseLevel] -> (VerboseLevel -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ ([NamedArg (Pattern' DBPatVar)] -> [VerboseLevel]
forall a. DeBruijn a => [NamedArg (Pattern' a)] -> [VerboseLevel]
iApplyVars [NamedArg (Pattern' DBPatVar)]
ps) ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i -> do
            IntervalView -> Term
unview <- TCMT IO (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
            let phi :: Term
phi = IntervalView -> Term
unview (IntervalView -> Term) -> IntervalView -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Arg Term -> IntervalView
IMax (Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ IntervalView -> Term
unview (Arg Term -> IntervalView
INeg (Arg Term -> IntervalView) -> Arg Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i)) (Arg Term -> IntervalView) -> Arg Term -> IntervalView
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i
            let es :: [Elim]
es = [NamedArg (Pattern' DBPatVar)] -> [Elim]
patternsToElims [NamedArg (Pattern' DBPatVar)]
ps
            let lhs :: Term
lhs = QName -> [Elim] -> Term
Def QName
f [Elim]
es

            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"clause:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg (Pattern' DBPatVar)] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg (Pattern' DBPatVar)]
ps TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"->" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
body
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"body =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
body

            Telescope -> TCM () -> TCM ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
clTel (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace Term
phi Type
trhs Term
lhs Term
body

            case Term
body of
              MetaV MetaId
m [Elim]
es_m' | Just [Arg Term]
es_m <- [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es_m' ->
                TCMT IO (Maybe InteractionId)
-> TCM () -> (InteractionId -> TCM ()) -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (MetaId -> TCMT IO (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((InteractionId -> TCM ()) -> TCM ())
-> (InteractionId -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii -> do
                [Closure (IPBoundary' Term)]
cs' <- do
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"clTel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
clTel
                  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
                  Closure Range
-> (Range -> TCMT IO [Closure (IPBoundary' Term)])
-> TCMT IO [Closure (IPBoundary' Term)]
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) ((Range -> TCMT IO [Closure (IPBoundary' Term)])
 -> TCMT IO [Closure (IPBoundary' Term)])
-> (Range -> TCMT IO [Closure (IPBoundary' Term)])
-> TCMT IO [Closure (IPBoundary' Term)]
forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do -- mTel ⊢
                  Type
ty <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m
                  Telescope
mTel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"size mTel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel)
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"size es_m =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseLevel -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m)

                  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"funny number of elims" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text ((VerboseLevel, VerboseLevel) -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel, [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m))
                  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
                  let over :: Overapplied
over = if Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m then Overapplied
NotOverapplied else Overapplied
Overapplied

                  -- extend telescope to handle extra elims
                  TelV Telescope
mTel1 Type
_ <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
PureTCM m =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpToPath ([Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) Type
ty
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"mTel1 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
mTel1

                  Telescope
-> TCMT IO [Closure (IPBoundary' Term)]
-> TCMT IO [Closure (IPBoundary' Term)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
mTel1 Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) (TCMT IO [Closure (IPBoundary' Term)]
 -> TCMT IO [Closure (IPBoundary' Term)])
-> TCMT IO [Closure (IPBoundary' Term)]
-> TCMT IO [Closure (IPBoundary' Term)]
forall a b. (a -> b) -> a -> b
$ do
                  Telescope
mTel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope

                  Telescope
-> TCMT IO [Closure (IPBoundary' Term)]
-> TCMT IO [Closure (IPBoundary' Term)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
clTel (TCMT IO [Closure (IPBoundary' Term)]
 -> TCMT IO [Closure (IPBoundary' Term)])
-> TCMT IO [Closure (IPBoundary' Term)]
-> TCMT IO [Closure (IPBoundary' Term)]
forall a b. (a -> b) -> a -> b
$ do -- mTel.clTel ⊢
                    () <- VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"mTel.clTel =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
                    Term
-> (Map VerboseLevel Bool
    -> Blocker -> Term -> TCMT IO (Closure (IPBoundary' Term)))
-> (Substitution -> TCMT IO (Closure (IPBoundary' Term)))
-> TCMT IO [Closure (IPBoundary' Term)]
forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (Map VerboseLevel Bool -> Blocker -> Term -> m a)
-> (Substitution -> m a)
-> m [a]
forallFaceMaps Term
phi Map VerboseLevel Bool
-> Blocker -> Term -> TCMT IO (Closure (IPBoundary' Term))
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Substitution -> TCMT IO (Closure (IPBoundary' Term)))
 -> TCMT IO [Closure (IPBoundary' Term)])
-> (Substitution -> TCMT IO (Closure (IPBoundary' Term)))
-> TCMT IO [Closure (IPBoundary' Term)]
forall a b. (a -> b) -> a -> b
$ \ Substitution
alpha -> do
                    -- mTel.clTel' ⊢
                    -- mTel.clTel  ⊢ alpha : mTel.clTel'
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"mTel.clTel' =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)

                    -- TelV tel _ <- telViewUpTo (size es) ty
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"i0S =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
alpha
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCM Doc
"es :", [Elim] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
es]
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCM Doc
"es_alpha :", [Elim] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Substitution
Substitution' (SubstArg [Elim])
alpha Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Elim]
es) ]

                    -- reducing path applications on endpoints in lhs
                    let
                       loop :: Term -> ReduceM Term
loop t :: Term
t@(Def QName
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
                       loop t :: Term
t@(Var VerboseLevel
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
                       loop t :: Term
t@(Con ConHead
_ ConInfo
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
                       loop t :: Term
t@(MetaV MetaId
_ [Elim]
es) = Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es
                       loop Term
t = Term -> ReduceM Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
                       loop' :: Term -> [Elim] -> ReduceM Term
loop' Term
t [Elim]
es = Blocked' Term Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked' Term Term -> Term)
-> ReduceM (Blocked' Term Term) -> ReduceM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> ReduceM (Blocked' Term Term))
-> ReduceM (Blocked' Term Term)
-> [Elim]
-> ReduceM (Blocked' Term Term)
reduceIApply' (Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> (Term -> Blocked' Term Term)
-> Term
-> ReduceM (Blocked' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked) (Blocked' Term Term -> ReduceM (Blocked' Term Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Blocked' Term Term -> ReduceM (Blocked' Term Term))
-> (Term -> Blocked' Term Term)
-> Term
-> ReduceM (Blocked' Term Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Blocked' Term Term
forall a t. a -> Blocked' t a
notBlocked (Term -> ReduceM (Blocked' Term Term))
-> Term -> ReduceM (Blocked' Term Term)
forall a b. (a -> b) -> a -> b
$ Term
t) [Elim]
es)
                    Term
lhs <- ReduceM Term -> TCMT IO Term
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM Term -> TCMT IO Term) -> ReduceM Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> ReduceM Term
loop (QName -> [Elim] -> Term
Def QName
f (Substitution
Substitution' (SubstArg [Elim])
alpha Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Elim]
es))

                    let
                        idG :: [Elim]
idG = VerboseLevel -> [Elim] -> [Elim]
forall a. Subst a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
clTel) ([Elim] -> [Elim]) -> [Elim] -> [Elim]
forall a b. (a -> b) -> a -> b
$ (Telescope -> Boundary' (Term, Term) -> [Elim]
forall a. DeBruijn a => Telescope -> Boundary' (a, a) -> [Elim' a]
teleElims Telescope
mTel [])

                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCM Doc
"lhs :", Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
lhs]
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"cxt1 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Constraint -> TCM Doc) -> Constraint -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Substitution
Substitution' (SubstArg Constraint)
alpha Substitution' (SubstArg Constraint) -> Constraint -> Constraint
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Comparison -> Term -> Type -> Term -> Term -> Constraint
ValueCmpOnFace Comparison
CmpEq Term
phi Type
trhs Term
lhs (MetaId -> [Elim] -> Term
MetaV MetaId
m [Elim]
idG)

                    [Arg Term]
-> [Arg Term]
-> (Substitution
    -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
-> TCMT IO (Closure (IPBoundary' Term))
forall a.
[Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims (Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) (Substitution
Substitution' (SubstArg [Arg Term])
alpha Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [Arg Term]
es_m) ((Substitution
  -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
 -> TCMT IO (Closure (IPBoundary' Term)))
-> (Substitution
    -> [(Term, Term)] -> TCMT IO (Closure (IPBoundary' Term)))
-> TCMT IO (Closure (IPBoundary' Term))
forall a b. (a -> b) -> a -> b
$ \ Substitution
sigma [(Term, Term)]
eqs -> do
                    -- mTel.clTel'' ⊢
                    -- mTel ⊢ clTel' ≃ clTel''.[eqs]
                    -- mTel.clTel'' ⊢ sigma : mTel.clTel'
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"cxt2 =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"sigma =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
sigma
                    VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"eqs =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Term, Term)] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Term, Term)]
eqs

                    IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term))
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term)))
-> IPBoundary' Term -> TCMT IO (Closure (IPBoundary' Term))
forall a b. (a -> b) -> a -> b
$ IPBoundary :: forall t. [(t, t)] -> t -> t -> Overapplied -> IPBoundary' t
IPBoundary
                       { ipbEquations :: [(Term, Term)]
ipbEquations = [(Term, Term)]
eqs
                       , ipbValue :: Term
ipbValue     = Substitution
Substitution' (SubstArg Term)
sigma Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
lhs
                       , ipbMetaApp :: Term
ipbMetaApp   = Substitution
Substitution' (SubstArg Term)
alpha Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` MetaId -> [Elim] -> Term
MetaV MetaId
m [Elim]
es_m'
                       , ipbOverapplied :: Overapplied
ipbOverapplied = Overapplied
over
                       }

                    -- WAS:
                    -- fmap (over,) $ buildClosure $ (eqs
                    --                , sigma `applySubst`
                    --                    (ValueCmp CmpEq (AsTermsOf (alpha `applySubst` trhs)) lhs (alpha `applySubst` MetaV m es_m)))

                let f :: InteractionPoint -> InteractionPoint
f InteractionPoint
ip = InteractionPoint
ip { ipClause :: IPClause
ipClause = case InteractionPoint -> IPClause
ipClause InteractionPoint
ip of
                                             ipc :: IPClause
ipc@IPClause{ipcBoundary :: IPClause -> [Closure (IPBoundary' Term)]
ipcBoundary = [Closure (IPBoundary' Term)]
b}
                                               -> IPClause
ipc {ipcBoundary :: [Closure (IPBoundary' Term)]
ipcBoundary = [Closure (IPBoundary' Term)]
b [Closure (IPBoundary' Term)]
-> [Closure (IPBoundary' Term)] -> [Closure (IPBoundary' Term)]
forall a. [a] -> [a] -> [a]
++ [Closure (IPBoundary' Term)]
cs'}
                                             ipc :: IPClause
ipc@IPNoClause{} -> IPClause
ipc}
                (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoint -> InteractionPoint)
-> InteractionId -> InteractionPoints -> InteractionPoints
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> v) -> k -> BiMap k v -> BiMap k v
BiMap.adjust InteractionPoint -> InteractionPoint
f InteractionId
ii)
              Term
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | current context is of the form Γ.Δ
unifyElims :: Args
              -- ^ variables to keep   Γ ⊢ x_n .. x_0 : Γ
           -> Args
              -- ^ variables to solve  Γ.Δ ⊢ ts : Γ
           -> (Substitution -> [(Term,Term)] -> TCM a)
              -- Γ.Δ' ⊢ σ : Γ.Δ
              -- Γ.Δ' new current context.
              -- Γ.Δ' ⊢ [(x = u)]
              -- Γ.Δ', [(x = u)] ⊢ id_g = ts[σ] : Γ
           -> TCM a
unifyElims :: [Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims [Arg Term]
vs [Arg Term]
ts Substitution -> [(Term, Term)] -> TCM a
k = do
                      [Dom (Name, Type)]
dom <- TCMT IO [Dom (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom (Name, Type)]
getContext
                      let ([(VerboseLevel, Term)]
binds' , [(Term, Term)]
eqs' ) = [Term] -> [Term] -> ([(VerboseLevel, Term)], [(Term, Term)])
candidate ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
vs) ((Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
ts)
                          ([(VerboseLevel, Term)]
binds'', [[(Term, Term)]]
eqss') =
                            [((VerboseLevel, Term), [(Term, Term)])]
-> ([(VerboseLevel, Term)], [[(Term, Term)]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((VerboseLevel, Term), [(Term, Term)])]
 -> ([(VerboseLevel, Term)], [[(Term, Term)]]))
-> [((VerboseLevel, Term), [(Term, Term)])]
-> ([(VerboseLevel, Term)], [[(Term, Term)]])
forall a b. (a -> b) -> a -> b
$ ((VerboseLevel, [Term]) -> ((VerboseLevel, Term), [(Term, Term)]))
-> [(VerboseLevel, [Term])]
-> [((VerboseLevel, Term), [(Term, Term)])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (VerboseLevel
j,Term
t:[Term]
ts) -> ((VerboseLevel
j,Term
t),(Term -> (Term, Term)) -> [Term] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (,VerboseLevel -> Term
var VerboseLevel
j) [Term]
ts)) ([(VerboseLevel, [Term])]
 -> [((VerboseLevel, Term), [(Term, Term)])])
-> [(VerboseLevel, [Term])]
-> [((VerboseLevel, Term), [(Term, Term)])]
forall a b. (a -> b) -> a -> b
$ Map VerboseLevel [Term] -> [(VerboseLevel, [Term])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map VerboseLevel [Term] -> [(VerboseLevel, [Term])])
-> Map VerboseLevel [Term] -> [(VerboseLevel, [Term])]
forall a b. (a -> b) -> a -> b
$ ([Term] -> [Term] -> [Term])
-> [(VerboseLevel, [Term])] -> Map VerboseLevel [Term]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
(++) (((VerboseLevel, Term) -> (VerboseLevel, [Term]))
-> [(VerboseLevel, Term)] -> [(VerboseLevel, [Term])]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> [Term]) -> (VerboseLevel, Term) -> (VerboseLevel, [Term])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[])) [(VerboseLevel, Term)]
binds')
                          cod :: [Dom (Name, Type)]
cod   = Substitution
-> [VerboseLevel] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
codomain Substitution
s (((VerboseLevel, Term) -> VerboseLevel)
-> [(VerboseLevel, Term)] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Term) -> VerboseLevel
forall a b. (a, b) -> a
fst [(VerboseLevel, Term)]
binds) [Dom (Name, Type)]
dom
                          binds :: [(VerboseLevel, Term)]
binds = ((VerboseLevel, Term) -> (VerboseLevel, Term))
-> [(VerboseLevel, Term)] -> [(VerboseLevel, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> (VerboseLevel, Term) -> (VerboseLevel, Term)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise ([Dom (Name, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (Name, Type)]
cod VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
vs))) [(VerboseLevel, Term)]
binds''
                          eqs :: [(Term, Term)]
eqs   = ((Term, Term) -> (Term, Term)) -> [(Term, Term)] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> (Term, Term) -> (Term, Term)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first  (VerboseLevel -> Term -> Term
forall a. Subst a => VerboseLevel -> a -> a
raise (VerboseLevel -> Term -> Term) -> VerboseLevel -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Dom (Name, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom (Name, Type)]
dom VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
vs)) ([(Term, Term)] -> [(Term, Term)])
-> [(Term, Term)] -> [(Term, Term)]
forall a b. (a -> b) -> a -> b
$ [(Term, Term)]
eqs' [(Term, Term)] -> [(Term, Term)] -> [(Term, Term)]
forall a. [a] -> [a] -> [a]
++ [[(Term, Term)]] -> [(Term, Term)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Term, Term)]]
eqss'
                          s :: Substitution
s     = [(VerboseLevel, Term)] -> Substitution
forall a. DeBruijn a => [(VerboseLevel, a)] -> Substitution' a
bindS [(VerboseLevel, Term)]
binds
                      Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution
-> ([Dom (Name, Type)] -> [Dom (Name, Type)]) -> m a -> m a
updateContext Substitution
s (Substitution
-> [VerboseLevel] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
codomain Substitution
s (((VerboseLevel, Term) -> VerboseLevel)
-> [(VerboseLevel, Term)] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Term) -> VerboseLevel
forall a b. (a, b) -> a
fst [(VerboseLevel, Term)]
binds)) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
                      Substitution -> [(Term, Term)] -> TCM a
k Substitution
s (Substitution
Substitution' (SubstArg [(Term, Term)])
s Substitution' (SubstArg [(Term, Term)])
-> [(Term, Term)] -> [(Term, Term)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [(Term, Term)]
eqs)
  where
    candidate :: [Term] -> [Term] -> ([(Nat,Term)],[(Term,Term)])
    candidate :: [Term] -> [Term] -> ([(VerboseLevel, Term)], [(Term, Term)])
candidate (Term
i:[Term]
is) (Var VerboseLevel
j []:[Term]
ts) = ([(VerboseLevel, Term)] -> [(VerboseLevel, Term)])
-> ([(VerboseLevel, Term)], [(Term, Term)])
-> ([(VerboseLevel, Term)], [(Term, Term)])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((VerboseLevel
j,Term
i)(VerboseLevel, Term)
-> [(VerboseLevel, Term)] -> [(VerboseLevel, Term)]
forall a. a -> [a] -> [a]
:) ([Term] -> [Term] -> ([(VerboseLevel, Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts)
    candidate (Term
i:[Term]
is) (Term
t:[Term]
ts)        = ([(Term, Term)] -> [(Term, Term)])
-> ([(VerboseLevel, Term)], [(Term, Term)])
-> ([(VerboseLevel, Term)], [(Term, Term)])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Term
i,Term
t)(Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
:) ([Term] -> [Term] -> ([(VerboseLevel, Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts)
    candidate [] [] = ([],[])
    candidate [Term]
_ [Term]
_ = ([(VerboseLevel, Term)], [(Term, Term)])
forall a. HasCallStack => a
__IMPOSSIBLE__


    bindS :: [(VerboseLevel, a)] -> Substitution' a
bindS [(VerboseLevel, a)]
binds = [a] -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([VerboseLevel] -> (VerboseLevel -> a) -> [a]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (-VerboseLevel
1VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. a -> [a] -> [a]
:((VerboseLevel, a) -> VerboseLevel)
-> [(VerboseLevel, a)] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, a) -> VerboseLevel
forall a b. (a, b) -> a
fst [(VerboseLevel, a)]
binds)] ((VerboseLevel -> a) -> [a]) -> (VerboseLevel -> a) -> [a]
forall a b. (a -> b) -> a -> b
$ (\ VerboseLevel
i -> a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (VerboseLevel -> a
forall a. DeBruijn a => VerboseLevel -> a
deBruijnVar VerboseLevel
i) (VerboseLevel -> [(VerboseLevel, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup VerboseLevel
i [(VerboseLevel, a)]
binds)))

    codomain :: Substitution
             -> [Nat]  -- support
             -> Context -> Context
    codomain :: Substitution
-> [VerboseLevel] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
codomain Substitution
s [VerboseLevel]
vs [Dom (Name, Type)]
cxt = ((VerboseLevel, Dom (Name, Type)) -> Dom (Name, Type))
-> [(VerboseLevel, Dom (Name, Type))] -> [Dom (Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel, Dom (Name, Type)) -> Dom (Name, Type)
forall a b. (a, b) -> b
snd ([(VerboseLevel, Dom (Name, Type))] -> [Dom (Name, Type)])
-> [(VerboseLevel, Dom (Name, Type))] -> [Dom (Name, Type)]
forall a b. (a -> b) -> a -> b
$ ((VerboseLevel, Dom (Name, Type)) -> Bool)
-> [(VerboseLevel, Dom (Name, Type))]
-> [(VerboseLevel, Dom (Name, Type))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (VerboseLevel
i,Dom (Name, Type)
c) -> VerboseLevel
i VerboseLevel -> [VerboseLevel] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`List.notElem` [VerboseLevel]
vs) ([(VerboseLevel, Dom (Name, Type))]
 -> [(VerboseLevel, Dom (Name, Type))])
-> [(VerboseLevel, Dom (Name, Type))]
-> [(VerboseLevel, Dom (Name, Type))]
forall a b. (a -> b) -> a -> b
$ [VerboseLevel]
-> [Dom (Name, Type)] -> [(VerboseLevel, Dom (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VerboseLevel
0..] [Dom (Name, Type)]
cxt'
     where
      cxt' :: [Dom (Name, Type)]
cxt' = (VerboseLevel -> Dom (Name, Type) -> Dom (Name, Type))
-> [VerboseLevel] -> [Dom (Name, Type)] -> [Dom (Name, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ VerboseLevel
n Dom (Name, Type)
d -> VerboseLevel -> Substitution -> Substitution
forall a. VerboseLevel -> Substitution' a -> Substitution' a
dropS VerboseLevel
n Substitution
s Substitution' (SubstArg (Dom (Name, Type)))
-> Dom (Name, Type) -> Dom (Name, Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Dom (Name, Type)
d) [VerboseLevel
1..] [Dom (Name, Type)]
cxt


-- | Like @unifyElims@ but @Γ@ is from the the meta's @MetaInfo@ and
-- the context extension @Δ@ is taken from the @Closure@.
unifyElimsMeta :: MetaId -> Args -> Closure Constraint -> ([(Term,Term)] -> Constraint -> TCM a) -> TCM a
unifyElimsMeta :: MetaId
-> [Arg Term]
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m [Arg Term]
es_m Closure Constraint
cl [(Term, Term)] -> Constraint -> TCM a
k = TCMT IO Bool -> TCM a -> TCM a -> TCM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Cubical -> Bool)
-> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (Closure Constraint -> (Constraint -> TCM a) -> TCM a
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl ((Constraint -> TCM a) -> TCM a) -> (Constraint -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ [(Term, Term)] -> Constraint -> TCM a
k []) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
                  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
                  Closure Range -> (Range -> TCM a) -> TCM a
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) ((Range -> TCM a) -> TCM a) -> (Range -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ Range
_ -> do -- mTel ⊢
                  Type
ty <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
m
                  Telescope
mTel0 <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
                  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel0 VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"funny number of elims" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text ((VerboseLevel, VerboseLevel) -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel0, [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m))
                  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel0 VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= [Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__ -- meta has at least enough arguments to fill its creation context.
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"ty: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ty

                  -- if we have more arguments we extend the telescope accordingly.
                  TelV Telescope
mTel1 Type
_ <- VerboseLevel -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
PureTCM m =>
VerboseLevel -> Type -> m (TelV Type)
telViewUpToPath ([Arg Term] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Arg Term]
es_m) Type
ty
                  Telescope -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Telescope
mTel1 Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel0) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
                  Telescope
mTel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"mTel: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
mTel

                  [Arg Term]
es_m <- [Arg Term] -> TCMT IO [Arg Term]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> TCMT IO [Arg Term])
-> [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Arg Term] -> [Arg Term]
forall a. VerboseLevel -> [a] -> [a]
take (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
mTel) [Arg Term]
es_m
                  -- invariant: size mTel == size es_m

                  (Constraint
c,Telescope
cxt) <- Closure Constraint
-> (Constraint -> TCMT IO (Constraint, Telescope))
-> TCMT IO (Constraint, Telescope)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl ((Constraint -> TCMT IO (Constraint, Telescope))
 -> TCMT IO (Constraint, Telescope))
-> (Constraint -> TCMT IO (Constraint, Telescope))
-> TCMT IO (Constraint, Telescope)
forall a b. (a -> b) -> a -> b
$ \ Constraint
c -> (Constraint
c,) (Telescope -> (Constraint, Telescope))
-> TCMT IO Telescope -> TCMT IO (Constraint, Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
cxt

                  Telescope -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
cxt (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do

                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"es_m" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
es_m

                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"trying unifyElims"

                  [Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
forall a.
[Arg Term]
-> [Arg Term] -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims (Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
mTel) [Arg Term]
es_m ((Substitution -> [(Term, Term)] -> TCM a) -> TCM a)
-> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ Substitution
sigma [(Term, Term)]
eqs -> do

                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"gotten a substitution"

                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"sigma:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution
sigma
                  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"sigma:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
sigma

                  [(Term, Term)] -> Constraint -> TCM a
k [(Term, Term)]
eqs (Substitution
Substitution' (SubstArg Constraint)
sigma Substitution' (SubstArg Constraint) -> Constraint -> Constraint
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Constraint
c)