{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.IApplyConfluence where

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

import Control.Monad.Except ( MonadError(..) )

import Data.Bifunctor (first, second)
import Data.DList (DList)
import Data.Foldable (toList)
import Data.IntMap (IntMap)
import Data.IntMap qualified as IntMap
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet

import Mikan.Syntax.Common
import Mikan.Syntax.Position
import Mikan.Syntax.Internal

import Mikan.Interaction.Options

import Mikan.TypeChecking.Primitive hiding (Nat)
import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Rules.LHS (buildLHSSubstitutions, LHSSubstitutionCase (..))
import Mikan.TypeChecking.Telescope.Path
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Conversion.Errors
import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.Substitute

import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Maybe
import Mikan.Utils.Singleton
import Mikan.Utils.Size
import Mikan.Utils.Impossible
import Mikan.Utils.Functor


checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ :: QName -> TCM ()
checkIApplyConfluence_ QName
f = do
  -- Andreas, 2019-03-27, iapply confluence should only be checked
  -- when --cubical[={full,erased}] is active. See
  -- test/Succeed/CheckIApplyConfluence.agda.
  -- We cannot reach the following crash point unless
  -- --cubical[={full,erased}] is active.
  VerboseKey -> Int -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadDebug m) =>
VerboseKey -> Int -> m ()
__CRASH_WHEN__ VerboseKey
"tc.cover.iapply.confluence.crash" Int
666
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Checking IApply confluence of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
  QName -> (Definition -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
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 -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.cover.iapply" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"length cls =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cls)
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when ([Clause] -> Bool
forall a. Null a => a -> Bool
null [Clause]
cls Bool -> Bool -> Bool
&& (Clause -> Bool) -> [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall a. Null a => a -> Bool
null ([Int] -> Bool) -> (Clause -> [Int]) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NAPs -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars (NAPs -> [Int]) -> (Clause -> NAPs) -> Clause -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats) [Clause]
cls') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (PragmaOptions -> Bool
optKeepCoveringClauses (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
$
        ASetter' TCState Defn -> (Defn -> Defn) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
modifyingTC ((Signature -> Identity Signature) -> TCState -> Identity TCState
Lens' TCState Signature
stSignature ((Signature -> Identity Signature) -> TCState -> Identity TCState)
-> ((Defn -> Identity Defn) -> Signature -> Identity Signature)
-> ASetter' TCState Defn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index Signature -> Traversal' Signature (IxValue Signature)
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index Signature
QName
f ((Definition -> Identity Definition)
 -> Signature -> Identity Signature)
-> ((Defn -> Identity Defn) -> Definition -> Identity Definition)
-> (Defn -> Identity Defn)
-> Signature
-> Identity Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defn -> Identity Defn) -> Definition -> Identity Definition
Lens' Definition Defn
lensTheDef) ((Defn -> Defn) -> TCM ()) -> (Defn -> Defn) -> TCM ()
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 a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> 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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | @checkIApplyConfluence 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 a. a -> TCMT IO a
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__
      -- Inserted clause, will respect boundaries whenever the
      -- user-written clauses do. Saves a ton of work!
      Clause {namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps} | NAPs -> Bool
forall a. HasDefP a => a -> Bool
hasDefP NAPs
ps -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      cl :: Clause
cl@Clause { clauseTel :: Clause -> Telescope
clauseTel = Telescope
clTel
                , namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
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 (Clause -> Range
clauseLHSRange Clause
cl) (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
          oldCall <- Lens' TCEnv (Maybe (Closure Call))
-> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe (Closure Call) -> f (Maybe (Closure Call)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Maybe (Closure Call))
eCall
          reportSDoc "tc.cover.iapply" 40 $ "tel =" <+> prettyTCM clTel
          reportSDoc "tc.cover.iapply" 40 $ "ps =" <+> pretty ps
          ps    <- normaliseProjP ps
          cxt   <- getContext
          clCxt <- inTopContext $ addContext clTel $ getContext
          let (_, clSub) = buildLHSSubstitutions cxt ps NormalFunSubst
          forM_ (iApplyVars ps) $ \ Int
i -> do
            unview <- TCMT IO (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
            let 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
$ Int -> Term
var Int
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
$ Int -> Term
var Int
i
            let es = NAPs -> [Elim]
patternsToElims NAPs
ps
            let lhs = QName -> [Elim] -> Term
Def QName
f [Elim]
es

            reportSDoc "tc.cover.iapply" 40 $ text "clause:" <+> pretty ps <+> "->" <+> pretty body
            reportSDoc "tc.cover.iapply" 20 $ "body =" <+> prettyTCM body
            inTopContext $ reportSDoc "tc.cover.iapply" 20 $ "Γ =" <+> prettyTCM clTel

            let
              k :: Substitution -> Comparison -> Type -> Term -> Term -> TCM ()
              -- TODO (Amy, 2023-07-08): Simplifying the LHS of a
              -- generated clause in its context is loopy, see #6722
              k Substitution
phi Comparison
cmp Type
ty Term
u Term
v | NAPs -> Bool
forall a. HasDefP a => a -> Bool
hasDefP NAPs
ps = Comparison -> Type -> Term -> Term -> TCM ()
compareTerm Comparison
cmp Type
ty Term
u Term
v
              k Substitution
phi Comparison
cmp Type
ty Term
u Term
v = do
                u_e   <- Term -> TCMT IO Term
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
u
                -- Issue #6725: Print these terms in their own TC state.
                -- If printing the values before entering the conversion
                -- checker is too expensive then we could save the TC
                -- state and print them when erroring instead, but that
                -- might cause space leaks.
                (u_p, v_p) <- (,) <$> prettyTCM u_e <*> (prettyTCM =<< simplify v)

                let
                  -- Make note of the context (literally): we're
                  -- checking that this specific clause in f is
                  -- confluent with IApply reductions. That way if we
                  -- can tell the user what the endpoints are.
                  why = Range -> QName -> Term -> Term -> Term -> Type -> Call
CheckIApplyConfluence
                    (Clause -> Range
forall a. HasRange a => a -> Range
getRange Clause
cl) QName
f
                    (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
phi Term
lhs)
                    Term
u_e Term
v Type
ty

                  -- But if the conversion checking failed really early, we drop the extra
                  -- information. In that case, it's just noise.
                  maybeDropCall e :: TCErr
e@(TypeError CallStack
loc TCState
s Closure SomeDiagnostic
err)
                    | Just (ConversionError Comparison
_ FailedCompareAs
_ Term
u' Term
v' ConversionErrorContext
_) <- SomeDiagnostic -> Maybe ConversionError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue Closure SomeDiagnostic
err) =
                      -- Issue #6725: restore the TC state from the
                      -- error before dealing with the stored terms.
                      (TCState -> TCState) -> TCM () -> TCM ()
forall a. (TCState -> TCState) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Closure SomeDiagnostic -> (SomeDiagnostic -> TCM ()) -> TCM ()
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure SomeDiagnostic
err ((SomeDiagnostic -> TCM ()) -> TCM ())
-> (SomeDiagnostic -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \SomeDiagnostic
e' -> do
                        u' <- Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify Term
u'
                        v' <- prettyTCM =<< simplify v'

                        -- Specifically, we compare how the things are pretty-printed, to avoid
                        -- double-printing, rather than a more refined heuristic, since the
                        -- “failure case” here is *at worst* accidentally reminding the user of how
                        -- IApplyConfluence works.
                        if (u_p == u' && v_p == v')
                          then localTC (set eCall oldCall) $ typeError e'
                          else throwError e
                  maybeDropCall TCErr
x = TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
x

                -- Note: Any postponed constraint with this call *will* have the extra
                -- information. This is a feature: if the constraint is woken up later,
                -- then it's probably a good idea to remind the user of what's going on,
                -- instead of presenting a mysterious error.
                traceCall why (compareTerm cmp ty u v `catchError` maybeDropCall)

            updateContext clSub (const clCxt) $
              compareTermOnFace' k CmpEq phi trhs lhs body

-- | 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 :: forall a.
Args -> Args -> (Substitution -> [(Term, Term)] -> TCM a) -> TCM a
unifyElims Args
vs Args
ts Substitution -> [(Term, Term)] -> TCM a
k = do
  dom <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  let (binds' , eqs' ) = candidate (map unArg vs) (map unArg ts)
      (binds'', eqss') =
        unzip $
        map (\(Int
j, DList Term
tts) -> case DList Term -> [Term]
forall a. DList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList DList Term
tts of
                Term
t : [Term]
ts -> ((Int
j, Term
t), (Term -> (Term, Term)) -> [Term] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (, Int -> Term
var Int
j) [Term]
ts)
                []     -> ((Int, Term), [(Term, Term)])
forall a. HasCallStack => a
__IMPOSSIBLE__) $
        IntMap.toList $ IntMap.fromListWith (<>) binds'
      cod'  = Substitution -> IntSet -> Context -> Context
codomain Substitution
s ([Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ ((Int, Term) -> Int) -> [(Int, Term)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Term) -> Int
forall a b. (a, b) -> a
fst [(Int, Term)]
binds'')
      cod   = Context -> Context
cod' Context
dom
      svs   = Args -> Int
forall a. Sized a => a -> Int
size Args
vs
      binds = [(Int, Term)] -> IntMap Term
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Term)] -> IntMap Term) -> [(Int, Term)] -> IntMap Term
forall a b. (a -> b) -> a -> b
$
              ((Int, Term) -> (Int, Term)) -> [(Int, Term)] -> [(Int, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> (Int, Term) -> (Int, Term)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Context -> Int
forall a. Sized a => a -> Int
size Context
cod Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
svs))) [(Int, Term)]
binds''
      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. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first  (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Context -> Int
forall a. Sized a => a -> Int
size Context
dom Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
svs))) ([(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     = IntMap Term -> Substitution
forall {a}. DeBruijn a => IntMap a -> Substitution' a
bindS IntMap Term
binds
  updateContext s cod' $ k s (s `applySubst` eqs)
  where
  candidate :: [Term] -> [Term] -> ([(Nat, DList Term)], [(Term, Term)])
  candidate :: [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts = case ([Term]
is, [Term]
ts) of
    (Term
i : [Term]
is, Var Int
j [] : [Term]
ts) -> ([(Int, DList Term)] -> [(Int, DList Term)])
-> ([(Int, DList Term)], [(Term, Term)])
-> ([(Int, DList Term)], [(Term, Term)])
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 ((Int
j, Term -> DList Term
forall el coll. Singleton el coll => el -> coll
singleton Term
i) (Int, DList Term) -> [(Int, DList Term)] -> [(Int, DList Term)]
forall a. a -> [a] -> [a]
:) (([(Int, DList Term)], [(Term, Term)])
 -> ([(Int, DList Term)], [(Term, Term)]))
-> ([(Int, DList Term)], [(Term, Term)])
-> ([(Int, DList Term)], [(Term, Term)])
forall a b. (a -> b) -> a -> b
$
                               [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts
    (Term
i : [Term]
is, Term
t : [Term]
ts)        -> ([(Term, Term)] -> [(Term, Term)])
-> ([(Int, DList Term)], [(Term, Term)])
-> ([(Int, DList Term)], [(Term, Term)])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Term
i, Term
t) (Term, Term) -> [(Term, Term)] -> [(Term, Term)]
forall a. a -> [a] -> [a]
:) (([(Int, DList Term)], [(Term, Term)])
 -> ([(Int, DList Term)], [(Term, Term)]))
-> ([(Int, DList Term)], [(Term, Term)])
-> ([(Int, DList Term)], [(Term, Term)])
forall a b. (a -> b) -> a -> b
$
                               [Term] -> [Term] -> ([(Int, DList Term)], [(Term, Term)])
candidate [Term]
is [Term]
ts
    ([],     [])            -> ([], [])
    ([Term], [Term])
_                       -> ([(Int, DList Term)], [(Term, Term)])
forall a. HasCallStack => a
__IMPOSSIBLE__

  bindS :: IntMap a -> Substitution' a
bindS IntMap a
binds = [a] -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([a] -> Substitution' a) -> [a] -> Substitution' a
forall a b. (a -> b) -> a -> b
$
    case IntMap a -> Maybe (Int, a)
forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMax IntMap a
binds of
      Maybe (Int, a)
Nothing       -> []
      Just (Int
max, a
_) -> [Int
0 .. Int
max] [Int] -> (Int -> a) -> [a]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Int
i ->
        a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (Int -> a
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i) (Int -> IntMap a -> Maybe a
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap a
binds)

  codomain
    :: Substitution
    -> IntSet  -- Support.
    -> Context -> Context
  codomain :: Substitution -> IntSet -> Context -> Context
codomain Substitution
s IntSet
vs = [ContextEntry] -> Context
forall a. [a] -> Context' a
Context ([ContextEntry] -> Context)
-> (Context -> [ContextEntry]) -> Context -> Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ((Int, ContextEntry) -> Maybe ContextEntry)
-> [(Int, ContextEntry)] -> [ContextEntry]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Int
i, ContextEntry
c) -> if Int
i Int -> IntSet -> Bool
`IntSet.member` IntSet
vs
                         then Maybe ContextEntry
forall a. Maybe a
Nothing
                         else ContextEntry -> Maybe ContextEntry
forall a. a -> Maybe a
Just ContextEntry
c) ([(Int, ContextEntry)] -> [ContextEntry])
-> (Context -> [(Int, ContextEntry)]) -> Context -> [ContextEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Int -> ContextEntry -> (Int, ContextEntry))
-> Context -> [(Int, ContextEntry)]
forall a. (Int -> ContextEntry -> a) -> Context -> [a]
cxWithIndex (\Int
i ContextEntry
c -> (Int
i, Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
dropS (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Substitution
s Substitution' (SubstArg ContextEntry)
-> ContextEntry -> ContextEntry
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` ContextEntry
c))

-- | Like @unifyElims@ but @Γ@ is from 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 :: forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
es_m Closure Constraint
cl [(Term, Term)] -> Constraint -> TCM a
k = do
  mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  enterClosure (getMetaInfo mv) $ \ Range
_ -> do -- mTel ⊢
  ty <- MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m
  mTel0 <- getContextTelescope
  unless (size mTel0 == size es_m) $ reportSDoc "tc.iapply.ip.meta" 20 $ "funny number of elims" <+> text (show (size mTel0, size es_m))
  unless (size mTel0 <= size es_m) $ __IMPOSSIBLE__ -- meta has at least enough arguments to fill its creation context.
  reportSDoc "tc.iapply.ip.meta" 20 $ "ty: " <+> prettyTCM ty

  -- if we have more arguments we extend the telescope accordingly.
  TelV mTel1 _ <- telViewUpToPath (size es_m) ty
  addContext (mTel1 `apply` teleArgs mTel0) $ do
  mTel <- getContextTelescope
  reportSDoc "tc.iapply.ip.meta" 20 $ "mTel: " <+> prettyTCM mTel

  es_m <- return $ take (size mTel) es_m
  -- invariant: size mTel == size es_m

  (c,cxt) <- enterClosure cl $ \ 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 :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope
  reportSDoc "tc.iapply.ip.meta" 20 $ prettyTCM cxt

  addContext cxt $ do

  reportSDoc "tc.iapply.ip.meta" 20 $ "es_m" <+> prettyTCM es_m

  reportSDoc "tc.iapply.ip.meta" 20 $ "trying unifyElims"

  unifyElims (teleArgs mTel) es_m $ \ Substitution
sigma [(Term, Term)]
eqs -> do

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

  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sigma:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Substitution -> m Doc
prettyTCM Substitution
sigma
  VerboseKey -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.iapply.ip.meta" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sigma:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO 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)