    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    {- |  Non-linear matching of the lhs of a rewrite rule against a
          neutral term.

    Given a lhs

      Δ ⊢ lhs : B

    and a candidate term

      Γ ⊢ t : A

    we seek a substitution Γ ⊢ σ : Δ such that

      Γ ⊢ B[σ] = A   and
      Γ ⊢ lhs[σ] = t : A

    -}

    module Agda.TypeChecking.Rewriting.NonLinMatch where

    import Prelude hiding (null, sequence)

    import Control.Applicative  ( Alternative )
    import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
    import Control.Monad.State  ( MonadState, StateT, runStateT )

    import Data.Maybe
    import Data.IntMap (IntMap)
    import qualified Data.IntMap as IntMap
    import Data.IntSet (IntSet)
    import qualified Data.IntSet as IntSet

    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Conversion.Pure (pureEqualTermB)
    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Free.Reduce
    import Agda.TypeChecking.Irrelevance (isPropM)
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad hiding (constructorForm)
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Reduce.Monad
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Primitive.Cubical.Base

    import Agda.Utils.Either
    import Agda.Utils.Function (applyWhen)
    import Agda.Utils.Functor
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.Permutation
    import Agda.Utils.Size

    import Agda.Utils.Impossible

    -- | Monad for non-linear matching.
    newtype NLM a = NLM { forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
    unNLM :: ExceptT Blocked_ (StateT NLMState ReduceM) a }
      deriving ( (forall a b. (a -> b) -> NLM a -> NLM b)
    -> (forall a b. a -> NLM b -> NLM a) -> Functor NLM
    forall a b. a -> NLM b -> NLM a
    forall a b. (a -> b) -> NLM a -> NLM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> NLM a -> NLM b
    fmap :: forall a b. (a -> b) -> NLM a -> NLM b
    $c<$ :: forall a b. a -> NLM b -> NLM a
    <$ :: forall a b. a -> NLM b -> NLM a
    Functor, Functor NLM
    Functor NLM =>
    (forall a. a -> NLM a)
    -> (forall a b. NLM (a -> b) -> NLM a -> NLM b)
    -> (forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c)
    -> (forall a b. NLM a -> NLM b -> NLM b)
    -> (forall a b. NLM a -> NLM b -> NLM a)
    -> Applicative NLM
    forall a. a -> NLM a
    forall a b. NLM a -> NLM b -> NLM a
    forall a b. NLM a -> NLM b -> NLM b
    forall a b. NLM (a -> b) -> NLM a -> NLM b
    forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> NLM a
    pure :: forall a. a -> NLM a
    $c<*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
    <*> :: forall a b. NLM (a -> b) -> NLM a -> NLM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
    liftA2 :: forall a b c. (a -> b -> c) -> NLM a -> NLM b -> NLM c
    $c*> :: forall a b. NLM a -> NLM b -> NLM b
    *> :: forall a b. NLM a -> NLM b -> NLM b
    $c<* :: forall a b. NLM a -> NLM b -> NLM a
    <* :: forall a b. NLM a -> NLM b -> NLM a
    Applicative, Applicative NLM
    Applicative NLM =>
    (forall a b. NLM a -> (a -> NLM b) -> NLM b)
    -> (forall a b. NLM a -> NLM b -> NLM b)
    -> (forall a. a -> NLM a)
    -> Monad NLM
    forall a. a -> NLM a
    forall a b. NLM a -> NLM b -> NLM b
    forall a b. NLM a -> (a -> NLM b) -> NLM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
    >>= :: forall a b. NLM a -> (a -> NLM b) -> NLM b
    $c>> :: forall a b. NLM a -> NLM b -> NLM b
    >> :: forall a b. NLM a -> NLM b -> NLM b
    $creturn :: forall a. a -> NLM a
    return :: forall a. a -> NLM a
    Monad, Monad NLM
    Monad NLM => (forall a. String -> NLM a) -> MonadFail NLM
    forall a. String -> NLM a
    forall (m :: * -> *).
    Monad m =>
    (forall a. String -> m a) -> MonadFail m
    $cfail :: forall a. String -> NLM a
    fail :: forall a. String -> NLM a
    MonadFail
               , Applicative NLM
    Applicative NLM =>
    (forall a. NLM a)
    -> (forall a. NLM a -> NLM a -> NLM a)
    -> (forall a. NLM a -> NLM [a])
    -> (forall a. NLM a -> NLM [a])
    -> Alternative NLM
    forall a. NLM a
    forall a. NLM a -> NLM [a]
    forall a. NLM a -> NLM a -> NLM a
    forall (f :: * -> *).
    Applicative f =>
    (forall a. f a)
    -> (forall a. f a -> f a -> f a)
    -> (forall a. f a -> f [a])
    -> (forall a. f a -> f [a])
    -> Alternative f
    $cempty :: forall a. NLM a
    empty :: forall a. NLM a
    $c<|> :: forall a. NLM a -> NLM a -> NLM a
    <|> :: forall a. NLM a -> NLM a -> NLM a
    $csome :: forall a. NLM a -> NLM [a]
    some :: forall a. NLM a -> NLM [a]
    $cmany :: forall a. NLM a -> NLM [a]
    many :: forall a. NLM a -> NLM [a]
    Alternative, Monad NLM
    Alternative NLM
    (Alternative NLM, Monad NLM) =>
    (forall a. NLM a)
    -> (forall a. NLM a -> NLM a -> NLM a) -> MonadPlus NLM
    forall a. NLM a
    forall a. NLM a -> NLM a -> NLM a
    forall (m :: * -> *).
    (Alternative m, Monad m) =>
    (forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
    $cmzero :: forall a. NLM a
    mzero :: forall a. NLM a
    $cmplus :: forall a. NLM a -> NLM a -> NLM a
    mplus :: forall a. NLM a -> NLM a -> NLM a
    MonadPlus
               , MonadError Blocked_, MonadState NLMState
               , Monad NLM
    Functor NLM
    Applicative NLM
    (Functor NLM, Applicative NLM, Monad NLM) =>
    (SomeBuiltin -> NLM (Maybe (Builtin PrimFun))) -> HasBuiltins NLM
    SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (SomeBuiltin -> m (Maybe (Builtin PrimFun))) -> HasBuiltins m
    $cgetBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
    getBuiltinThing :: SomeBuiltin -> NLM (Maybe (Builtin PrimFun))
    HasBuiltins, Functor NLM
    Applicative NLM
    HasOptions NLM
    MonadTCEnv NLM
    MonadDebug NLM
    (Functor NLM, Applicative NLM, HasOptions NLM, MonadDebug NLM,
     MonadTCEnv NLM) =>
    (QName -> NLM Definition)
    -> (QName -> NLM (Either SigError Definition))
    -> (QName -> NLM RewriteRules)
    -> HasConstInfo NLM
    QName -> NLM RewriteRules
    QName -> NLM (Either SigError Definition)
    QName -> NLM Definition
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadDebug m,
     MonadTCEnv m) =>
    (QName -> m Definition)
    -> (QName -> m (Either SigError Definition))
    -> (QName -> m RewriteRules)
    -> HasConstInfo m
    $cgetConstInfo :: QName -> NLM Definition
    getConstInfo :: QName -> NLM Definition
    $cgetConstInfo' :: QName -> NLM (Either SigError Definition)
    getConstInfo' :: QName -> NLM (Either SigError Definition)
    $cgetRewriteRulesFor :: QName -> NLM RewriteRules
    getRewriteRulesFor :: QName -> NLM RewriteRules
    HasConstInfo, Monad NLM
    Functor NLM
    Applicative NLM
    NLM PragmaOptions
    NLM CommandLineOptions
    (Functor NLM, Applicative NLM, Monad NLM) =>
    NLM PragmaOptions -> NLM CommandLineOptions -> HasOptions NLM
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    m PragmaOptions -> m CommandLineOptions -> HasOptions m
    $cpragmaOptions :: NLM PragmaOptions
    pragmaOptions :: NLM PragmaOptions
    $ccommandLineOptions :: NLM CommandLineOptions
    commandLineOptions :: NLM CommandLineOptions
    HasOptions, Monad NLM
    NLM TCState
    Monad NLM =>
    NLM TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b)
    -> (forall a. (TCState -> TCState) -> NLM a -> NLM a)
    -> ReadTCState NLM
    forall a. (TCState -> TCState) -> NLM a -> NLM a
    forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
    forall (m :: * -> *).
    Monad m =>
    m TCState
    -> (forall a b. Lens' TCState a -> (a -> a) -> m b -> m b)
    -> (forall a. (TCState -> TCState) -> m a -> m a)
    -> ReadTCState m
    $cgetTCState :: NLM TCState
    getTCState :: NLM TCState
    $clocallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
    locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> NLM b -> NLM b
    $cwithTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
    withTCState :: forall a. (TCState -> TCState) -> NLM a -> NLM a
    ReadTCState
               , Monad NLM
    NLM TCEnv
    Monad NLM =>
    NLM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a) -> MonadTCEnv NLM
    forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    forall (m :: * -> *).
    Monad m =>
    m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a) -> MonadTCEnv m
    $caskTC :: NLM TCEnv
    askTC :: NLM TCEnv
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    localTC :: forall a. (TCEnv -> TCEnv) -> NLM a -> NLM a
    MonadTCEnv, Applicative NLM
    HasOptions NLM
    MonadTCEnv NLM
    ReadTCState NLM
    (Applicative NLM, MonadTCEnv NLM, ReadTCState NLM,
     HasOptions NLM) =>
    (forall a. ReduceM a -> NLM a) -> MonadReduce NLM
    forall a. ReduceM a -> NLM a
    forall (m :: * -> *).
    (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) =>
    (forall a. ReduceM a -> m a) -> MonadReduce m
    $cliftReduce :: forall a. ReduceM a -> NLM a
    liftReduce :: forall a. ReduceM a -> NLM a
    MonadReduce, MonadTCEnv NLM
    MonadTCEnv NLM =>
    (forall a. Name -> Dom Type -> NLM a -> NLM a)
    -> (forall a. Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a)
    -> (forall a.
        Substitution -> (Context -> Context) -> NLM a -> NLM a)
    -> (forall a. Range -> String -> (Name -> NLM a) -> NLM a)
    -> MonadAddContext NLM
    forall a. Range -> String -> (Name -> NLM a) -> NLM a
    forall a. Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
    forall a. Name -> Dom Type -> NLM a -> NLM a
    forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    forall (m :: * -> *).
    MonadTCEnv m =>
    (forall a. Name -> Dom Type -> m a -> m a)
    -> (forall a. Origin -> Name -> Term -> Dom Type -> m a -> m a)
    -> (forall a. Substitution -> (Context -> Context) -> m a -> m a)
    -> (forall a. Range -> String -> (Name -> m a) -> m a)
    -> MonadAddContext m
    $caddCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
    addCtx :: forall a. Name -> Dom Type -> NLM a -> NLM a
    $caddLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
    addLetBinding' :: forall a. Origin -> Name -> Term -> Dom Type -> NLM a -> NLM a
    $cupdateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    updateContext :: forall a. Substitution -> (Context -> Context) -> NLM a -> NLM a
    $cwithFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
    withFreshName :: forall a. Range -> String -> (Name -> NLM a) -> NLM a
    MonadAddContext, Monad NLM
    Functor NLM
    Applicative NLM
    NLM Bool
    NLM Verbosity
    NLM ProfileOptions
    (Functor NLM, Applicative NLM, Monad NLM) =>
    (String -> Key -> TCMT IO Doc -> NLM String)
    -> (forall a. String -> Key -> String -> NLM a -> NLM a)
    -> (forall a. String -> Key -> String -> NLM a -> NLM a)
    -> NLM Verbosity
    -> NLM ProfileOptions
    -> NLM Bool
    -> (forall a. NLM a -> NLM a)
    -> MonadDebug NLM
    String -> Key -> TCMT IO Doc -> NLM String
    forall a. String -> Key -> String -> NLM a -> NLM a
    forall a. NLM a -> NLM a
    forall (m :: * -> *).
    (Functor m, Applicative m, Monad m) =>
    (String -> Key -> TCMT IO Doc -> m String)
    -> (forall a. String -> Key -> String -> m a -> m a)
    -> (forall a. String -> Key -> String -> m a -> m a)
    -> m Verbosity
    -> m ProfileOptions
    -> m Bool
    -> (forall a. m a -> m a)
    -> MonadDebug m
    $cformatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
    formatDebugMessage :: String -> Key -> TCMT IO Doc -> NLM String
    $ctraceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
    traceDebugMessage :: forall a. String -> Key -> String -> NLM a -> NLM a
    $cverboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
    verboseBracket :: forall a. String -> Key -> String -> NLM a -> NLM a
    $cgetVerbosity :: NLM Verbosity
    getVerbosity :: NLM Verbosity
    $cgetProfileOptions :: NLM ProfileOptions
    getProfileOptions :: NLM ProfileOptions
    $cisDebugPrinting :: NLM Bool
    isDebugPrinting :: NLM Bool
    $cnowDebugPrinting :: forall a. NLM a -> NLM a
    nowDebugPrinting :: forall a. NLM a -> NLM a
    MonadDebug
               , MonadTCEnv NLM
    MonadReduce NLM
    ReadTCState NLM
    HasBuiltins NLM
    MonadAddContext NLM
    MonadDebug NLM
    HasConstInfo NLM
    (HasBuiltins NLM, HasConstInfo NLM, MonadAddContext NLM,
     MonadDebug NLM, MonadReduce NLM, MonadTCEnv NLM,
     ReadTCState NLM) =>
    PureTCM NLM
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m,
     MonadReduce m, MonadTCEnv m, ReadTCState m) =>
    PureTCM m
    PureTCM
               )

    instance MonadBlock NLM where
      patternViolation :: forall a. Blocker -> NLM a
    patternViolation Blocker
    b = Blocked_ -> NLM a
    forall a. Blocked_ -> NLM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Blocked_ -> NLM a) -> Blocked_ -> NLM a
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()
      catchPatternErr :: forall a. (Blocker -> NLM a) -> NLM a -> NLM a
    catchPatternErr Blocker -> NLM a
    h NLM a
    f = NLM a -> (Blocked_ -> NLM a) -> NLM a
    forall a. NLM a -> (Blocked_ -> NLM a) -> NLM a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    catchError NLM a
    f ((Blocked_ -> NLM a) -> NLM a) -> (Blocked_ -> NLM a) -> NLM a
    forall a b. (a -> b) -> a -> b
    $ \case
        Blocked Blocker
    b ()
    _      -> Blocker -> NLM a
    h Blocker
    b
        err :: Blocked_
    err@NotBlocked{} -> Blocked_ -> NLM a
    forall a. Blocked_ -> NLM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError Blocked_
    err

    data NLMState = NLMState
      { NLMState -> Sub
    _nlmSub   :: Sub
      , NLMState -> PostponedEquations
    _nlmEqs   :: PostponedEquations
      }

    instance Null NLMState where
      empty :: NLMState
    empty  = NLMState { _nlmSub :: Sub
    _nlmSub = Sub
    forall a. Null a => a
    empty , _nlmEqs :: PostponedEquations
    _nlmEqs = PostponedEquations
    forall a. Null a => a
    empty }
      null :: NLMState -> Bool
    null NLMState
    s = Sub -> Bool
    forall a. Null a => a -> Bool
    null (NLMState
    s NLMState -> Lens' NLMState Sub -> Sub
    forall o i. o -> Lens' o i -> i
    ^. (Sub -> f Sub) -> NLMState -> f NLMState
    Lens' NLMState Sub
    nlmSub) Bool -> Bool -> Bool
    && PostponedEquations -> Bool
    forall a. Null a => a -> Bool
    null (NLMState
    s NLMState -> Lens' NLMState PostponedEquations -> PostponedEquations
    forall o i. o -> Lens' o i -> i
    ^. (PostponedEquations -> f PostponedEquations)
    -> NLMState -> f NLMState
    Lens' NLMState PostponedEquations
    nlmEqs)

    nlmSub :: Lens' NLMState Sub
    nlmSub :: Lens' NLMState Sub
    nlmSub Sub -> f Sub
    f NLMState
    s = Sub -> f Sub
    f (NLMState -> Sub
    _nlmSub NLMState
    s) f Sub -> (Sub -> NLMState) -> f NLMState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \Sub
    x -> NLMState
    s {_nlmSub = x}

    nlmEqs :: Lens' NLMState PostponedEquations
    nlmEqs :: Lens' NLMState PostponedEquations
    nlmEqs PostponedEquations -> f PostponedEquations
    f NLMState
    s = PostponedEquations -> f PostponedEquations
    f (NLMState -> PostponedEquations
    _nlmEqs NLMState
    s) f PostponedEquations
    -> (PostponedEquations -> NLMState) -> f NLMState
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \PostponedEquations
    x -> NLMState
    s {_nlmEqs = x}

    runNLM :: (MonadReduce m) => NLM () -> m (Either Blocked_ NLMState)
    runNLM :: forall (m :: * -> *).
    MonadReduce m =>
    NLM () -> m (Either Blocked_ NLMState)
    runNLM NLM ()
    nlm = do
      (ok,out) <- ReduceM (Either Blocked_ (), NLMState)
    -> m (Either Blocked_ (), NLMState)
    forall a. ReduceM a -> m a
    forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
    liftReduce (ReduceM (Either Blocked_ (), NLMState)
     -> m (Either Blocked_ (), NLMState))
    -> ReduceM (Either Blocked_ (), NLMState)
    -> m (Either Blocked_ (), NLMState)
    forall a b. (a -> b) -> a -> b
    $ StateT NLMState ReduceM (Either Blocked_ ())
    -> NLMState -> ReduceM (Either Blocked_ (), NLMState)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ExceptT Blocked_ (StateT NLMState ReduceM) ()
    -> StateT NLMState ReduceM (Either Blocked_ ())
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT Blocked_ (StateT NLMState ReduceM) ()
     -> StateT NLMState ReduceM (Either Blocked_ ()))
    -> ExceptT Blocked_ (StateT NLMState ReduceM) ()
    -> StateT NLMState ReduceM (Either Blocked_ ())
    forall a b. (a -> b) -> a -> b
    $ NLM () -> ExceptT Blocked_ (StateT NLMState ReduceM) ()
    forall a. NLM a -> ExceptT Blocked_ (StateT NLMState ReduceM) a
    unNLM NLM ()
    nlm) NLMState
    forall a. Null a => a
    empty
      case ok of
        Left Blocked_
    block -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ NLMState -> m (Either Blocked_ NLMState))
    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Either Blocked_ NLMState
    forall a b. a -> Either a b
    Left Blocked_
    block
        Right ()
    _    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ NLMState -> m (Either Blocked_ NLMState))
    -> Either Blocked_ NLMState -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ NLMState -> Either Blocked_ NLMState
    forall a b. b -> Either a b
    Right NLMState
    out

    matchingBlocked :: Blocked_ -> NLM ()
    matchingBlocked :: Blocked_ -> NLM ()
    matchingBlocked = Blocked_ -> NLM ()
    forall a. Blocked_ -> NLM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError

    -- | Add substitution @i |-> v : a@ to result of matching.
    tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
    tellSub :: Relevance -> Key -> Type -> Term -> NLM ()
    tellSub Relevance
    r Key
    i Type
    a Term
    v = do
      old <- Key -> Sub -> Maybe (Relevance, Term)
    forall a. Key -> IntMap a -> Maybe a
    IntMap.lookup Key
    i (Sub -> Maybe (Relevance, Term))
    -> NLM Sub -> NLM (Maybe (Relevance, Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' NLMState Sub -> NLM Sub
    forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
    use (Sub -> f Sub) -> NLMState -> f NLMState
    Lens' NLMState Sub
    nlmSub
      case old of
        Maybe (Relevance, Term)
    Nothing -> (Sub -> f Sub) -> NLMState -> f NLMState
    Lens' NLMState Sub
    nlmSub Lens' NLMState Sub -> (Sub -> Sub) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' o i -> (i -> i) -> m ()
    %= Key -> (Relevance, Term) -> Sub -> Sub
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (Relevance
    r,Term
    v)
        Just (Relevance
    r',Term
    v')
          | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r  -> () -> NLM ()
    forall a. a -> NLM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
          | Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r' -> (Sub -> f Sub) -> NLMState -> f NLMState
    Lens' NLMState Sub
    nlmSub Lens' NLMState Sub -> (Sub -> Sub) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' o i -> (i -> i) -> m ()
    %= Key -> (Relevance, Term) -> Sub -> Sub
    forall a. Key -> a -> IntMap a -> IntMap a
    IntMap.insert Key
    i (Relevance
    r,Term
    v)
          | Bool
    otherwise       -> NLM (Maybe Blocked_) -> (Blocked_ -> NLM ()) -> NLM ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM (Type -> Term -> Term -> NLM (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    v Term
    v') Blocked_ -> NLM ()
    matchingBlocked

    tellEq :: Telescope -> Context -> Type -> Term -> Term -> NLM ()
    tellEq :: Telescope -> Context -> Type -> Term -> Term -> NLM ()
    tellEq Telescope
    gamma Context
    k Type
    a Term
    u Term
    v = do
      String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                   [ TCMT IO Doc
    "adding equality between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u)
                   , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
      (PostponedEquations -> f PostponedEquations)
    -> NLMState -> f NLMState
    Lens' NLMState PostponedEquations
    nlmEqs Lens' NLMState PostponedEquations
    -> (PostponedEquations -> PostponedEquations) -> NLM ()
    forall o (m :: * -> *) i.
    MonadState o m =>
    Lens' o i -> (i -> i) -> m ()
    %= (Context -> Type -> Term -> Term -> PostponedEquation
    PostponedEquation Context
    k Type
    a Term
    u Term
    vPostponedEquation -> PostponedEquations -> PostponedEquations
    forall a. a -> [a] -> [a]
    :)

    type Sub = IntMap (Relevance, Term)

    -- | Matching against a term produces a constraint
    --   which we have to verify after applying
    --   the substitution computed by matching.
    data PostponedEquation = PostponedEquation
      { PostponedEquation -> Context
    eqFreeVars :: Context -- ^ Context of free variables in the equation
      , PostponedEquation -> Type
    eqType :: Type    -- ^ Type of the equation, living in same context as the rhs.
      , PostponedEquation -> Term
    eqLhs :: Term     -- ^ Term from pattern, living in pattern context.
      , PostponedEquation -> Term
    eqRhs :: Term     -- ^ Term from scrutinee, living in context where matching was invoked.
      }
    type PostponedEquations = [PostponedEquation]

    -- | Match a non-linear pattern against a neutral term,
    --   returning a substitution.

    class Match a b where
      match :: Relevance  -- ^ Are we currently matching in an irrelevant context?
            -> Telescope  -- ^ The telescope of pattern variables
            -> Context    -- ^ The context of lambda-bound variables
            -> TypeOf b   -- ^ The type of the pattern
            -> a          -- ^ The pattern to match
            -> b          -- ^ The term to be matched against the pattern
            -> NLM ()

    instance Match a b => Match (Arg a) (Arg b) where
      match :: Relevance
    -> Telescope
    -> Context
    -> TypeOf (Arg b)
    -> Arg a
    -> Arg b
    -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf (Arg b)
    t Arg a
    p Arg b
    v = let r' :: Relevance
    r' = Relevance
    r Relevance -> Relevance -> Relevance
    `composeRelevance` Arg a -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Arg a
    p
                              in  Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r' Telescope
    gamma Context
    k (Dom' Term (TypeOf b) -> TypeOf b
    forall t e. Dom' t e -> e
    unDom TypeOf (Arg b)
    Dom' Term (TypeOf b)
    t) (Arg a -> a
    forall e. Arg e -> e
    unArg Arg a
    p) (Arg b -> b
    forall e. Arg e -> e
    unArg Arg b
    v)

    instance Match [Elim' NLPat] Elims where
      match :: Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    t, Elims -> Term
    hd) [] [] = () -> NLM ()
    forall a. a -> NLM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      match Relevance
    r Telescope
    gamma Context
    k (Type
    t, Elims -> Term
    hd) [] Elims
    _  = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
      match Relevance
    r Telescope
    gamma Context
    k (Type
    t, Elims -> Term
    hd) [Elim' NLPat]
    _  [] = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
      match Relevance
    r Telescope
    gamma Context
    k (Type
    t, Elims -> Term
    hd) (Elim' NLPat
    p:[Elim' NLPat]
    ps) (Elim
    v:Elims
    vs) =
       String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    50 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
         [ TCMT IO Doc
    "matching elimination " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Elim' NLPat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim' NLPat -> m Doc
    prettyTCM Elim' NLPat
    p)
         , TCMT IO Doc
    "  with               " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Elim -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Elim -> m Doc
    prettyTCM Elim
    v)
         , TCMT IO Doc
    "  eliminating head   " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (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) -> Term -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Elims -> Term
    hd []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    ":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t)]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do

       let no :: NLM ()
    no  = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
       case (Elim' NLPat
    p,Elim
    v) of
        (Apply Arg NLPat
    p, Apply Arg Term
    v) -> Context -> NLM Term -> NLM Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> NLM Type -> NLM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t) NLM Term -> (Term -> NLM ()) -> NLM ()
    forall a b. NLM a -> (a -> NLM b) -> NLM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          Pi Dom Type
    a Abs Type
    b -> do
            Relevance
    -> Telescope
    -> Context
    -> TypeOf (Arg Term)
    -> Arg NLPat
    -> Arg Term
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf (Arg Term)
    Dom Type
    a Arg NLPat
    p Arg Term
    v
            let t' :: Type
    t'  = Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    absApp Abs Type
    b (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    v)
                hd' :: Elims -> Term
    hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Arg Term
    vElim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
            Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    t',Elims -> Term
    hd') [Elim' NLPat]
    ps Elims
    vs
          Term
    t -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20
            (TCMT IO Doc
    "application at non-pi type (possible non-confluence?) " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t) NLM ()
    forall a. NLM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (IApply NLPat
    x NLPat
    y NLPat
    p , IApply Term
    u Term
    v Term
    i) -> Context -> NLM PathView -> NLM PathView
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Type -> NLM PathView
    forall (m :: * -> *). HasBuiltins m => Type -> m PathView
    pathView (Type -> NLM PathView) -> NLM Type -> NLM PathView
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t) NLM PathView -> (PathView -> NLM ()) -> NLM ()
    forall a b. NLM a -> (a -> NLM b) -> NLM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          PathType Sort
    s QName
    q Arg Term
    l Arg Term
    b Arg Term
    _u Arg Term
    _v -> do
            interval <- (TCErr -> Type) -> Either TCErr Type -> Type
    forall a b. (a -> b) -> Either a b -> b
    fromRight TCErr -> Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Either TCErr Type -> Type) -> NLM (Either TCErr Type) -> NLM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ExceptT TCErr NLM Type -> NLM (Either TCErr Type)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ExceptT TCErr NLM Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
            match r gamma k interval p i
            let t' = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> Term -> Type
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    b Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    i ]
            let hd' = Elims -> Term
    hd (Elims -> Term) -> (Elims -> Elims) -> Elims -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply Term
    u Term
    v Term
    iElim -> Elims -> Elims
    forall a. a -> [a] -> [a]
    :)
            match r gamma k (t',hd') ps vs
          PathView
    t -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20
            (TCMT IO Doc
    "interval application at non-pi type (possible non-confluence?) " 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 (PathView -> Type
    pathUnview PathView
    t)) NLM ()
    forall a. NLM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (Proj ProjOrigin
    o QName
    f, Proj ProjOrigin
    o' QName
    f') | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f' -> do
          Context -> NLM (Maybe Type) -> NLM (Maybe Type)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (QName -> Type -> NLM (Maybe Type)
    forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
    getDefType QName
    f (Type -> NLM (Maybe Type)) -> NLM Type -> NLM (Maybe Type)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> NLM Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t) NLM (Maybe Type) -> (Maybe Type -> NLM ()) -> NLM ()
    forall a b. NLM a -> (a -> NLM b) -> NLM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            Just (El Sort
    _ (Pi Dom Type
    a Abs Type
    b)) -> do
              let u :: Term
    u = Elims -> Term
    hd []
                  t' :: Type
    t' = Abs Type
    b Abs Type -> SubstArg Type -> Type
    forall a. Subst a => Abs a -> SubstArg a -> a
    `absApp` Term
    SubstArg Type
    u
              hd' <- Context -> NLM (Elims -> Term) -> NLM (Elims -> Term)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM (Elims -> Term) -> NLM (Elims -> Term))
    -> NLM (Elims -> Term) -> NLM (Elims -> Term)
    forall a b. (a -> b) -> a -> b
    $ Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    applyE (Term -> Elims -> Term) -> NLM Term -> NLM (Elims -> Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ProjOrigin -> QName -> Arg Term -> NLM Term
    forall (m :: * -> *).
    HasConstInfo m =>
    ProjOrigin -> QName -> Arg Term -> m Term
    applyDef ProjOrigin
    o QName
    f (Dom Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom Dom Type
    a Arg Type -> Term -> Arg Term
    forall (f :: * -> *) a b. Functor f => f a -> b -> f b
    $> Term
    u)
              match r gamma k (t',hd') ps vs
            Maybe Type
    _ -> NLM ()
    no

        (Proj ProjOrigin
    _ QName
    f, Proj ProjOrigin
    _ QName
    f') | Bool
    otherwise -> do
          String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    20 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "mismatch between projections " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f
            , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f' ]) NLM ()
    forall a. NLM a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero

        (Apply{}, Proj{} ) -> NLM ()
    no
        (Proj{} , Apply{}) -> NLM ()
    no

        (IApply{} , Elim
    _    ) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- TODO
        (Elim' NLPat
    _ , IApply{}    ) -> NLM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- TODO

    instance Match a b => Match (Dom a) (Dom b) where
      match :: Relevance
    -> Telescope
    -> Context
    -> TypeOf (Dom b)
    -> Dom a
    -> Dom b
    -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf (Dom b)
    t Dom a
    p Dom b
    v = Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf b
    TypeOf (Dom b)
    t (Dom a -> a
    forall t e. Dom' t e -> e
    unDom Dom a
    p) (Dom b -> b
    forall t e. Dom' t e -> e
    unDom Dom b
    v)

    instance Match NLPType Type where
      match :: Relevance
    -> Telescope -> Context -> TypeOf Type -> NLPType -> Type -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf Type
    _ (NLPType NLPSort
    sp NLPat
    p) (El Sort
    s Term
    a) = NLM () -> NLM ()
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    workOnTypes (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
        Relevance
    -> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k () NLPSort
    sp Sort
    s
        Relevance
    -> Telescope -> Context -> TypeOf Term -> NLPat -> Term -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Sort -> Type
    sort Sort
    s) NLPat
    p Term
    a

    instance Match NLPSort Sort where
      match :: Relevance
    -> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf Sort
    _ NLPSort
    p Sort
    s = do
        bs <- Context -> NLM (Blocked Sort) -> NLM (Blocked Sort)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM (Blocked Sort) -> NLM (Blocked Sort))
    -> NLM (Blocked Sort) -> NLM (Blocked Sort)
    forall a b. (a -> b) -> a -> b
    $ Sort -> NLM (Blocked Sort)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Sort
    s
        let b = Blocked Sort -> Blocked_
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void Blocked Sort
    bs
            s = Blocked Sort -> Sort
    forall t a. Blocked' t a -> a
    ignoreBlocking Blocked Sort
    bs
            yes = () -> NLM ()
    forall a. a -> NLM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            no  = Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()
        traceSDoc "rewriting.match" 30 (sep
          [ "matching pattern " <+> addContext gamma (addContext k $ prettyTCM p)
          , "  with sort      " <+> addContext k (prettyTCM s) ]) $ do
        case (p , s) of
          (PUniv Univ
    u NLPat
    lp    , Univ Univ
    u' Level' Term
    l) | Univ
    u Univ -> Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    == Univ
    u'          -> Relevance
    -> Telescope
    -> Context
    -> TypeOf (Level' Term)
    -> NLPat
    -> Level' Term
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k () NLPat
    lp Level' Term
    l
          (PInf Univ
    up Integer
    np    , Inf Univ
    u Integer
    n)   | Univ
    up Univ -> Univ -> Bool
    forall a. Eq a => a -> a -> Bool
    == Univ
    u, Integer
    np Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    n -> NLM ()
    yes
          (NLPSort
    PSizeUniv     , Sort
    SizeUniv)                     -> NLM ()
    yes
          (NLPSort
    PLockUniv     , Sort
    LockUniv)                     -> NLM ()
    yes
          (NLPSort
    PLevelUniv    , Sort
    LevelUniv)                    -> NLM ()
    yes
          (NLPSort
    PIntervalUniv , Sort
    IntervalUniv)                 -> NLM ()
    yes

          -- blocked cases
          (NLPSort
    _ , UnivSort{}) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , PiSort{}  ) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , FunSort{} ) -> Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
          (NLPSort
    _ , MetaS MetaId
    m Elims
    _ ) -> Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocked_
    forall t. MetaId -> Blocked' t ()
    blocked_ MetaId
    m

          -- all other cases do not match
          (NLPSort
    _ , Sort
    _) -> NLM ()
    no

    instance Match NLPat Level where
      match :: Relevance
    -> Telescope
    -> Context
    -> TypeOf (Level' Term)
    -> NLPat
    -> Level' Term
    -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k TypeOf (Level' Term)
    _ NLPat
    p Level' Term
    l = do
        t <- Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El (Integer -> Sort
    mkType Integer
    0) (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Type) -> NLM (Maybe Term) -> NLM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> NLM (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinLevel
        v <- reallyUnLevelView l
        match r gamma k t p v

    instance Match NLPat Term where
      match :: Relevance  -- Are we currently matching in an irrelevant context?
            -> Telescope  -- The telescope of pattern variables
            -> Context    -- The context of lambda-bound variables
            -> Type       -- The type of the pattern
            -> NLPat      -- The pattern to match
            -> Term       -- The term to be matched against the pattern
            -> NLM ()
      match :: Relevance
    -> Telescope -> Context -> Type -> NLPat -> Term -> NLM ()
    match Relevance
    r0 Telescope
    gamma Context
    k Type
    t NLPat
    p Term
    v = do
        vbt <- Context -> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type)))
    -> NLM (Blocked (Term, Type)) -> NLM (Blocked (Term, Type))
    forall a b. (a -> b) -> a -> b
    $ (Term, Type) -> NLM (Blocked (Term, Type))
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB (Term
    v,Type
    t)
        let n = Context -> Key
    forall a. Sized a => a -> Key
    size Context
    k
            b = Blocked (Term, Type) -> Blocked_
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void Blocked (Term, Type)
    vbt
            (v,t) = ignoreBlocking vbt
            prettyPat  = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ NLPat -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => NLPat -> m Doc
    prettyTCM NLPat
    p
            prettyTerm = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
            prettyType = TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a. ReadTCState m => m a -> m a
    withShowAllArguments (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Type -> m Doc
    prettyTCM Type
    t
        etaRecord <- addContext k $ isEtaRecordType t
        pview <- pathViewAsPi'whnf
        prop <- fromRight __IMPOSSIBLE__ <.> runBlocked . addContext k $ isPropM t
        let r = if Bool
    prop then Relevance
    irrelevant else Relevance
    r0
        traceSDoc "rewriting.match" 30 (sep
          [ "matching pattern " <+> prettyPat
          , "  with term      " <+> prettyTerm
          , "  of type        " <+> prettyType ]) $ do
        traceSDoc "rewriting.match" 80 (vcat
          [ "  raw pattern:  " <+> text (show p)
          , "  raw term:     " <+> text (show v)
          , "  raw type:     " <+> text (show t) ]) $ do
        traceSDoc "rewriting.match" 70 (vcat
          [ "pattern vars:   " <+> prettyTCM gamma
          , "bound vars:     " <+> prettyTCM k ]) $ do
        let yes = () -> NLM ()
    forall a. a -> NLM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
            no TCMT IO Doc
    msg = if Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r then NLM ()
    yes else do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "mismatch between" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyPat
                , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyTerm
                , TCMT IO Doc
    " of type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    prettyType
                , TCMT IO Doc
    msg ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b) ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Blocked_ -> NLM ()
    matchingBlocked Blocked_
    b
            block Blocked_
    b' = if Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    r then NLM ()
    yes else do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "matching blocked on meta"
                , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                [ TCMT IO Doc
    "blocking tag from reduction: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Blocked_ -> String
    forall a. Show a => a -> String
    show Blocked_
    b') ]) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
              Blocked_ -> NLM ()
    matchingBlocked (Blocked_
    b Blocked_ -> Blocked_ -> Blocked_
    forall a. Monoid a => a -> a -> a
    `mappend` Blocked_
    b')
            maybeBlock = \case
              MetaV MetaId
    m Elims
    es -> Blocked_ -> NLM ()
    matchingBlocked (Blocked_ -> NLM ()) -> Blocked_ -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Blocked_
    forall t. MetaId -> Blocked' t ()
    blocked_ MetaId
    m
              Term
    _          -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
        case p of
          PVar Key
    i [Arg Key]
    bvs -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PVar: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Key -> String
    forall a. Show a => a -> String
    show Key
    i)) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
            let vars :: [Key]
    vars = (Arg Key -> Key) -> [Arg Key] -> [Key]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Key -> Key
    forall e. Arg e -> e
    unArg [Arg Key]
    bvs
            let allowedVars :: IntSet
                allowedVars :: IntSet
    allowedVars = [Key] -> IntSet
    IntSet.fromList [Key]
    vars
                badVars :: IntSet
                badVars :: IntSet
    badVars = IntSet -> IntSet -> IntSet
    IntSet.difference ([Key] -> IntSet
    IntSet.fromList (Key -> [Key]
    forall a. Integral a => a -> [a]
    downFrom Key
    n)) IntSet
    allowedVars
                perm :: Permutation
                perm :: Permutation
    perm = Key -> [Key] -> Permutation
    Perm Key
    n ([Key] -> Permutation) -> [Key] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ [Key] -> [Key]
    forall a. [a] -> [a]
    reverse [Key]
    vars
                tel :: Telescope
                tel :: Telescope
    tel = Permutation -> Context -> Telescope
    permuteContext Permutation
    perm Context
    k
            ok <- Context
    -> NLM (Either Blocked_ (Maybe Term))
    -> NLM (Either Blocked_ (Maybe Term))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM (Either Blocked_ (Maybe Term))
     -> NLM (Either Blocked_ (Maybe Term)))
    -> NLM (Either Blocked_ (Maybe Term))
    -> NLM (Either Blocked_ (Maybe Term))
    forall a b. (a -> b) -> a -> b
    $ IntSet -> Term -> NLM (Either Blocked_ (Maybe Term))
    forall (m :: * -> *) a.
    (MonadReduce m, Reduce a, ForceNotFree a) =>
    IntSet -> a -> m (Either Blocked_ (Maybe a))
    reallyFree IntSet
    badVars Term
    v
            case ok of
              Left Blocked_
    b         -> Blocked_ -> NLM ()
    block Blocked_
    b
              Right Maybe Term
    Nothing  -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
              Right (Just Term
    v) ->
                let t' :: Type
    t' = Telescope -> Type -> Type
    telePi  Telescope
    tel (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Permutation -> Type -> Type
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible Permutation
    perm Type
    t
                    v' :: Term
    v' = Telescope -> Term -> Term
    teleLam Telescope
    tel (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    $ Impossible -> Permutation -> Term -> Term
    forall a. Subst a => Impossible -> Permutation -> a -> a
    renameP Impossible
    HasCallStack => Impossible
    impossible Permutation
    perm Term
    v
                in Relevance -> Key -> Type -> Term -> NLM ()
    tellSub Relevance
    r (Key
    iKey -> Key -> Key
    forall a. Num a => a -> a -> a
    -Key
    n) Type
    t' Term
    v'

          PDef QName
    f [Elim' NLPat]
    ps -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PDef: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    f) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $ do
            v <- Context -> NLM Term -> NLM Term
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM Term -> NLM Term) -> NLM Term -> NLM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> NLM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    constructorForm (Term -> NLM Term) -> NLM Term -> NLM Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> NLM Term
    forall (m :: * -> *). HasBuiltins m => Term -> m Term
    unLevel Term
    v
            case v of
              Def QName
    f' Elims
    es
                | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f'   -> do
                    ft <- Context -> NLM Type -> NLM Type
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM Type -> NLM Type) -> NLM Type -> NLM Type
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType (Definition -> Type) -> NLM Definition -> NLM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
                    match r gamma k (ft , Def f) ps es
              Con ConHead
    c ConInfo
    ci Elims
    vs
                | QName
    f QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ConHead -> QName
    conName ConHead
    c -> do
                    Context
    -> NLM (Maybe ((QName, Type, Args), Type))
    -> NLM (Maybe ((QName, Type, Args), Type))
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (ConHead -> Type -> NLM (Maybe ((QName, Type, Args), Type))
    forall (m :: * -> *).
    PureTCM m =>
    ConHead -> Type -> m (Maybe ((QName, Type, Args), Type))
    getFullyAppliedConType ConHead
    c Type
    t) NLM (Maybe ((QName, Type, Args), Type))
    -> (Maybe ((QName, Type, Args), Type) -> NLM ()) -> NLM ()
    forall a b. NLM a -> (a -> NLM b) -> NLM b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
                      Just ((QName, Type, Args)
    _ , Type
    ct) -> Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    ct , ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) [Elim' NLPat]
    ps Elims
    vs
                      Maybe ((QName, Type, Args), Type)
    Nothing -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
              Term
    _ | Pi Dom Type
    a Abs Type
    b <- Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -> do
                let ai :: ArgInfo
    ai    = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
                    pbody :: NLPat
    pbody = QName -> [Elim' NLPat] -> NLPat
    PDef QName
    f ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. Subst a => Key -> a -> a
    raise Key
    1 [Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NLPat -> Arg NLPat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                    body :: Term
    body  = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg (Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a) (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                k' <- Context -> String -> Dom Type -> NLM Context
    forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    k (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Dom Type
    a
                match r gamma k' (absBody b) pbody body
              Term
    _ | Just (QName
    d, Args
    pars) <- Maybe (QName, Args)
    etaRecord -> do
              -- If v is not of record constructor form but we are matching at record
              -- type, e.g., we eta-expand both v to (c vs) and
              -- the pattern (p = PDef f ps) to @c (p .f1) ... (p .fn)@.
                RecordDefn def <- Context -> NLM Defn -> NLM Defn
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
                (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
                addContext k (getFullyAppliedConType c t) >>= \case
                  Just ((QName, Type, Args)
    _ , Type
    ct) -> do
                    let flds :: [Arg QName]
    flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ RecordData -> [Dom QName]
    _recFields RecordData
    def
                        mkField :: QName -> NLPat
    mkField QName
    fld = QName -> [Elim' NLPat] -> NLPat
    PDef QName
    f ([Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld])
                        -- Issue #3335: when matching against the record constructor,
                        -- don't add projections but take record field directly.
                        ps' :: [Elim' NLPat]
    ps'
                          | ConHead -> QName
    conName ConHead
    c QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    f = [Elim' NLPat]
    ps
                          | Bool
    otherwise      = (Arg QName -> Elim' NLPat) -> [Arg QName] -> [Elim' NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat)
    -> (Arg QName -> Arg NLPat) -> Arg QName -> Elim' NLPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName -> NLPat) -> Arg QName -> Arg NLPat
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap QName -> NLPat
    mkField) [Arg QName]
    flds
                    Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    ct, ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) [Elim' NLPat]
    ps' ((Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    vs)
                  Maybe ((QName, Type, Args), Type)
    Nothing -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
              Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PLam ArgInfo
    i Abs NLPat
    p' -> case Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t of
            Pi Dom Type
    a Abs Type
    b -> do
              let body :: Term
    body = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    i (Key -> Term
    var Key
    0)]
              k' <- Context -> String -> Dom Type -> NLM Context
    forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    k (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Dom Type
    a
              match r gamma k' (absBody b) (absBody p') body
            Term
    _ | Left ((Dom Type
    a,Abs Type
    b),(Term
    x,Term
    y)) <- Type -> Either ((Dom Type, Abs Type), (Term, Term)) Type
    pview Type
    t -> do
              let body :: Term
    body = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ Term -> Term -> Term -> Elim
    forall a. a -> a -> a -> Elim' a
    IApply (Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    x) (Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    y) (Term -> Elim) -> Term -> Elim
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
              k' <- Context -> String -> Dom Type -> NLM Context
    forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    k String
    "i" Dom Type
    a
              match r gamma k' (absBody b) (absBody p') body
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PPi Dom NLPType
    pa Abs NLPType
    pb -> case Term
    v of
            Pi Dom Type
    a Abs Type
    b -> do
              Relevance
    -> Telescope
    -> Context
    -> TypeOf (Dom Type)
    -> Dom NLPType
    -> Dom Type
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k () Dom NLPType
    pa Dom Type
    a
              k' <- Context -> String -> Dom Type -> NLM Context
    forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    k (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Dom Type
    a
              match r gamma k' () (absBody pb) (absBody b)
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PSort NLPSort
    ps -> case Term
    v of
            Sort Sort
    s -> Relevance
    -> Telescope -> Context -> TypeOf Sort -> NLPSort -> Sort -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k () NLPSort
    ps Sort
    s
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PBoundVar Key
    i [Elim' NLPat]
    ps -> case Term
    v of
            Var Key
    i' Elims
    es | Key
    i Key -> Key -> Bool
    forall a. Eq a => a -> a -> Bool
    == Key
    i' -> do
              let ti :: Type
    ti = Type -> (ContextEntry -> Type) -> Maybe ContextEntry -> Type
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom (Dom Type -> Type)
    -> (ContextEntry -> Dom Type) -> ContextEntry -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ContextEntry -> Dom Type
    ctxEntryDom) (Maybe ContextEntry -> Type) -> Maybe ContextEntry -> Type
    forall a b. (a -> b) -> a -> b
    $ Key -> Context -> Maybe ContextEntry
    lookupBV_ Key
    i Context
    k
              Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    ti , Key -> Elims -> Term
    Var Key
    i) [Elim' NLPat]
    ps Elims
    es
            Term
    _ | Pi Dom Type
    a Abs Type
    b <- Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t -> do
              let ai :: ArgInfo
    ai    = Dom Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom Type
    a
                  pbody :: NLPat
    pbody = Key -> [Elim' NLPat] -> NLPat
    PBoundVar (Key
    1 Key -> Key -> Key
    forall a. Num a => a -> a -> a
    + Key
    i) ([Elim' NLPat] -> NLPat) -> [Elim' NLPat] -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. Subst a => Key -> a -> a
    raise Key
    1 [Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply (Arg NLPat -> Elim' NLPat) -> Arg NLPat -> Elim' NLPat
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> NLPat -> Arg NLPat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (NLPat -> Arg NLPat) -> NLPat -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ Term -> NLPat
    PTerm (Term -> NLPat) -> Term -> NLPat
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
                  body :: Term
    body  = Key -> Term -> Term
    forall a. Subst a => Key -> a -> a
    raise Key
    1 Term
    v Term -> Args -> Term
    forall t. Apply t => t -> Args -> t
    `apply` [ ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Key -> Term
    var Key
    0 ]
              k' <- Context -> String -> Dom Type -> NLM Context
    forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    k (Abs Type -> String
    forall a. Abs a -> String
    absName Abs Type
    b) Dom Type
    a
              match r gamma k' (absBody b) pbody body
            Term
    _ | Just (QName
    d, Args
    pars) <- Maybe (QName, Args)
    etaRecord -> do
              RecordDefn def <- Context -> NLM Defn -> NLM Defn
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (NLM Defn -> NLM Defn) -> NLM Defn -> NLM Defn
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef (Definition -> Defn) -> NLM Definition -> NLM Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> NLM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    d
              (tel, c, ci, vs) <- addContext k $ etaExpandRecord_ d pars def v
              addContext k (getFullyAppliedConType c t) >>= \case
                Just ((QName, Type, Args)
    _ , Type
    ct) -> do
                  let flds :: [Arg QName]
    flds = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Arg QName
    forall t a. Dom' t a -> Arg a
    argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
    forall a b. (a -> b) -> a -> b
    $ RecordData -> [Dom QName]
    _recFields RecordData
    def
                      ps' :: [Arg NLPat]
    ps'  = (Arg QName -> Arg NLPat) -> [Arg QName] -> [Arg NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map ((QName -> NLPat) -> Arg QName -> Arg NLPat
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((QName -> NLPat) -> Arg QName -> Arg NLPat)
    -> (QName -> NLPat) -> Arg QName -> Arg NLPat
    forall a b. (a -> b) -> a -> b
    $ \QName
    fld -> Key -> [Elim' NLPat] -> NLPat
    PBoundVar Key
    i ([Elim' NLPat]
    ps [Elim' NLPat] -> [Elim' NLPat] -> [Elim' NLPat]
    forall a. [a] -> [a] -> [a]
    ++ [ProjOrigin -> QName -> Elim' NLPat
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem QName
    fld])) [Arg QName]
    flds
                  Relevance
    -> Telescope
    -> Context
    -> TypeOf Elims
    -> [Elim' NLPat]
    -> Elims
    -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    r Telescope
    gamma Context
    k (Type
    ct, ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci) ((Arg NLPat -> Elim' NLPat) -> [Arg NLPat] -> [Elim' NLPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg NLPat -> Elim' NLPat
    forall a. Arg a -> Elim' a
    Apply [Arg NLPat]
    ps') ((Arg Term -> Elim) -> Args -> Elims
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> Elim
    forall a. Arg a -> Elim' a
    Apply Args
    vs)
                Maybe ((QName, Type, Args), Type)
    Nothing -> TCMT IO Doc -> NLM ()
    no TCMT IO Doc
    ""
            Term
    v -> Term -> NLM ()
    maybeBlock Term
    v
          PTerm Term
    u -> String -> Key -> TCMT IO Doc -> NLM () -> NLM ()
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    60 (TCMT IO Doc
    "matching a PTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    gamma (Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u)) (NLM () -> NLM ()) -> NLM () -> NLM ()
    forall a b. (a -> b) -> a -> b
    $
            Telescope -> Context -> Type -> Term -> Term -> NLM ()
    tellEq Telescope
    gamma Context
    k Type
    t Term
    u Term
    v

    extendContext :: MonadAddContext m => Context -> ArgName -> Dom Type -> m Context
    extendContext :: forall (m :: * -> *).
    MonadAddContext m =>
    Context -> String -> Dom Type -> m Context
    extendContext Context
    cxt String
    x Dom Type
    a = Range -> String -> (Name -> m Context) -> m Context
    forall a. Range -> String -> (Name -> m a) -> m a
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Range -> String -> (Name -> m a) -> m a
    withFreshName Range
    forall a. Null a => a
    empty String
    x \ Name
    y -> Context -> m Context
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Context -> m Context) -> Context -> m Context
    forall a b. (a -> b) -> a -> b
    $ Name -> Dom Type -> ContextEntry
    CtxVar Name
    y Dom Type
    a ContextEntry -> Context -> Context
    forall a. a -> [a] -> [a]
    : Context
    cxt

    makeSubstitution :: Telescope -> Sub -> Maybe Substitution
    makeSubstitution :: Telescope -> Sub -> Maybe Substitution
    makeSubstitution Telescope
    gamma Sub
    sub =
      [Term] -> Substitution
    forall a. DeBruijn a => [a] -> Substitution' a
    parallelS ([Term] -> Substitution) -> Maybe [Term] -> Maybe Substitution
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Key -> Maybe Term) -> [Key] -> Maybe [Term]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Key -> Maybe Term
    val [Key
    0 .. Telescope -> Key
    forall a. Sized a => a -> Key
    size Telescope
    gammaKey -> Key -> Key
    forall a. Num a => a -> a -> a
    -Key
    1]
        where
          val :: Key -> Maybe Term
    val Key
    i = Key -> Sub -> Maybe (Relevance, Term)
    forall a. Key -> IntMap a -> Maybe a
    IntMap.lookup Key
    i Sub
    sub Maybe (Relevance, Term)
    -> ((Relevance, Term) -> Term) -> Maybe Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ (Relevance
    rel, Term
    v) -> Bool -> (Term -> Term) -> Term -> Term
    forall b a. IsBool b => b -> (a -> a) -> a -> a
    applyWhen (Relevance -> Bool
    forall a. LensRelevance a => a -> Bool
    isIrrelevant Relevance
    rel) Term -> Term
    dontCare Term
    v

    {-# SPECIALIZE checkPostponedEquations :: Substitution -> PostponedEquations -> TCM (Maybe Blocked_) #-}
    checkPostponedEquations :: PureTCM m
                            => Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations :: forall (m :: * -> *).
    PureTCM m =>
    Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations Substitution
    sub PostponedEquations
    eqs = PostponedEquations
    -> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Applicative m, Monoid b) =>
    t a -> (a -> m b) -> m b
    forM' PostponedEquations
    eqs ((PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_))
    -> (PostponedEquation -> m (Maybe Blocked_)) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $
      \ (PostponedEquation Context
    k Type
    a Term
    lhs Term
    rhs) -> do
          let lhs' :: Term
    lhs' = Substitution' (SubstArg Term) -> Term -> Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Key -> Substitution -> Substitution
    forall a. Key -> Substitution' a -> Substitution' a
    liftS (Context -> Key
    forall a. Sized a => a -> Key
    size Context
    k) Substitution
    sub) Term
    lhs
          String
    -> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    30 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
            [ TCMT IO Doc
    "checking postponed equality between" , Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    lhs')
            , TCMT IO Doc
    " and " , Context -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    rhs) ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ do
          Context -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    forall (m :: * -> *) a. MonadAddContext m => Context -> m a -> m a
    addContext Context
    k (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Type -> Term -> Term -> m (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    lhs' Term
    rhs

    -- main function
    nonLinMatch :: (PureTCM m, Match a b)
                => Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch :: forall (m :: * -> *) a b.
    (PureTCM m, Match a b) =>
    Telescope -> TypeOf b -> a -> b -> m (Either Blocked_ Substitution)
    nonLinMatch Telescope
    gamma TypeOf b
    t a
    p b
    v = do
      let no :: String -> a -> m (Either a b)
    no String
    msg a
    b = String -> Key -> TCMT IO Doc -> m (Either a b) -> m (Either a b)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
                       [ TCMT IO Doc
    "matching failed during" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text String
    msg
                       , TCMT IO Doc
    "blocking: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (a -> String
    forall a. Show a => a -> String
    show a
    b) ]) (m (Either a b) -> m (Either a b))
    -> m (Either a b) -> m (Either a b)
    forall a b. (a -> b) -> a -> b
    $ Either a b -> m (Either a b)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Either a b
    forall a b. a -> Either a b
    Left a
    b)
      m (Either Blocked_ NLMState)
    -> (Blocked_ -> m (Either Blocked_ Substitution))
    -> (NLMState -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a b c.
    Monad m =>
    m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
    caseEitherM (NLM () -> m (Either Blocked_ NLMState)
    forall (m :: * -> *).
    MonadReduce m =>
    NLM () -> m (Either Blocked_ NLMState)
    runNLM (NLM () -> m (Either Blocked_ NLMState))
    -> NLM () -> m (Either Blocked_ NLMState)
    forall a b. (a -> b) -> a -> b
    $ Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    forall a b.
    Match a b =>
    Relevance -> Telescope -> Context -> TypeOf b -> a -> b -> NLM ()
    match Relevance
    relevant Telescope
    gamma Context
    forall a. Null a => a
    empty TypeOf b
    t a
    p b
    v) (String -> Blocked_ -> m (Either Blocked_ Substitution)
    forall {m :: * -> *} {a} {b}.
    (MonadDebug m, Show a) =>
    String -> a -> m (Either a b)
    no String
    "matching") ((NLMState -> m (Either Blocked_ Substitution))
     -> m (Either Blocked_ Substitution))
    -> (NLMState -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ \ NLMState
    s -> do
        let msub :: Maybe Substitution
    msub = Telescope -> Sub -> Maybe Substitution
    makeSubstitution Telescope
    gamma (Sub -> Maybe Substitution) -> Sub -> Maybe Substitution
    forall a b. (a -> b) -> a -> b
    $ NLMState
    s NLMState -> Lens' NLMState Sub -> Sub
    forall o i. o -> Lens' o i -> i
    ^. (Sub -> f Sub) -> NLMState -> f NLMState
    Lens' NLMState Sub
    nlmSub
            eqs :: PostponedEquations
    eqs = NLMState
    s NLMState -> Lens' NLMState PostponedEquations -> PostponedEquations
    forall o i. o -> Lens' o i -> i
    ^. (PostponedEquations -> f PostponedEquations)
    -> NLMState -> f NLMState
    Lens' NLMState PostponedEquations
    nlmEqs
        String
    -> Key
    -> TCMT IO Doc
    -> m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    90 (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "msub = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Maybe Substitution -> String
    forall a. Show a => a -> String
    show Maybe Substitution
    msub) (m (Either Blocked_ Substitution)
     -> m (Either Blocked_ Substitution))
    -> m (Either Blocked_ Substitution)
    -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ case Maybe Substitution
    msub of
          Maybe Substitution
    Nothing -> String -> Blocked_ -> m (Either Blocked_ Substitution)
    forall {m :: * -> *} {a} {b}.
    (MonadDebug m, Show a) =>
    String -> a -> m (Either a b)
    no String
    "checking that all variables are bound" Blocked_
    forall t. Blocked' t ()
    notBlocked_
          Just Substitution
    sub -> do
            ok <- Substitution -> PostponedEquations -> m (Maybe Blocked_)
    forall (m :: * -> *).
    PureTCM m =>
    Substitution -> PostponedEquations -> m (Maybe Blocked_)
    checkPostponedEquations Substitution
    sub PostponedEquations
    eqs
            case ok of
              Maybe Blocked_
    Nothing -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either Blocked_ Substitution -> m (Either Blocked_ Substitution))
    -> Either Blocked_ Substitution -> m (Either Blocked_ Substitution)
    forall a b. (a -> b) -> a -> b
    $ Substitution -> Either Blocked_ Substitution
    forall a b. b -> Either a b
    Right Substitution
    sub
              Just Blocked_
    b  -> String -> Blocked_ -> m (Either Blocked_ Substitution)
    forall {m :: * -> *} {a} {b}.
    (MonadDebug m, Show a) =>
    String -> a -> m (Either a b)
    no String
    "checking of postponed equations" Blocked_
    b

    -- | Typed βη-equality, also handles empty record types.
    --   Returns `Nothing` if the terms are equal, or `Just b` if the terms are not
    --   (where b contains information about possible metas blocking the comparison)
    equal :: PureTCM m => Type -> Term -> Term -> m (Maybe Blocked_)
    equal :: forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Maybe Blocked_)
    equal Type
    a Term
    u Term
    v = Type -> Term -> Term -> m (Either Blocker Bool)
    forall (m :: * -> *).
    PureTCM m =>
    Type -> Term -> Term -> m (Either Blocker Bool)
    pureEqualTermB Type
    a Term
    u Term
    v m (Either Blocker Bool)
    -> (Either Blocker Bool -> m (Maybe Blocked_))
    -> m (Maybe Blocked_)
    forall a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Left Blocker
    b      -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Blocked_ -> m (Maybe Blocked_))
    -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Maybe Blocked_
    forall a. a -> Maybe a
    Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
    forall a b. (a -> b) -> a -> b
    $ Blocker -> () -> Blocked_
    forall t a. Blocker -> a -> Blocked' t a
    Blocked Blocker
    b ()
      Right Bool
    True  -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Blocked_
    forall a. Maybe a
    Nothing
      Right Bool
    False -> String
    -> Key -> TCMT IO Doc -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall (m :: * -> *) a.
    MonadDebug m =>
    String -> Key -> TCMT IO Doc -> m a -> m a
    traceSDoc String
    "rewriting.match" Key
    10 ([TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ TCMT IO Doc
    "mismatch between " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    u
          , TCMT IO Doc
    " and " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    v
          ]) (m (Maybe Blocked_) -> m (Maybe Blocked_))
    -> m (Maybe Blocked_) -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ do
        Maybe Blocked_ -> m (Maybe Blocked_)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Blocked_ -> m (Maybe Blocked_))
    -> Maybe Blocked_ -> m (Maybe Blocked_)
    forall a b. (a -> b) -> a -> b
    $ Blocked_ -> Maybe Blocked_
    forall a. a -> Maybe a
    Just (Blocked_ -> Maybe Blocked_) -> Blocked_ -> Maybe Blocked_
    forall a b. (a -> b) -> a -> b
    $ NotBlocked' Term -> () -> Blocked_
    forall t a. NotBlocked' t -> a -> Blocked' t a
    NotBlocked NotBlocked' Term
    forall t. NotBlocked' t
    ReallyNotBlocked ()

    -- | Utility function for getting the name and type of a head term (i.e. a
    --   `Def` or `Con` with no arguments)
    getTypedHead :: PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead :: forall (m :: * -> *). PureTCM m => Term -> m (Maybe (QName, Type))
    getTypedHead = \case
      Def QName
    f []   -> (QName, Type) -> Maybe (QName, Type)
    forall a. a -> Maybe a
    Just ((QName, Type) -> Maybe (QName, Type))
    -> (Definition -> (QName, Type))
    -> Definition
    -> Maybe (QName, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QName
    f,) (Type -> (QName, Type))
    -> (Definition -> Type) -> Definition -> (QName, Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> Maybe (QName, Type))
    -> m Definition -> m (Maybe (QName, Type))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f
      Con (ConHead { conName :: ConHead -> QName
    conName = QName
    c }) ConInfo
    _ [] -> do
        -- Andreas, 2018-09-08, issue #3211:
        -- discount module parameters for constructor heads
        vs <- QName -> m Args
    forall (m :: * -> *).
    (Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
     MonadTCEnv m, MonadDebug m) =>
    QName -> m Args
    freeVarsToApply QName
    c
        -- Jesper, 2020-06-17, issue #4755: add dummy arguments in
        -- case we don't have enough parameters
        getNumberOfParameters c >>= \case
          Just Key
    npars -> do
            let ws :: Args
    ws = Key -> Arg Term -> Args
    forall a. Key -> a -> [a]
    replicate (Key
    npars Key -> Key -> Key
    forall a. Num a => a -> a -> a
    - Args -> Key
    forall a. Sized a => a -> Key
    size Args
    vs) (Arg Term -> Args) -> Arg Term -> Args
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall a. a -> Arg a
    defaultArg Term
    HasCallStack => Term
    __DUMMY_TERM__
            t0 <- Definition -> Type
    defType (Definition -> Type) -> m Definition -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    c
            t <- t0 `piApplyM` (vs ++ ws)
            return $ Just (c , t)
          Maybe Key
    Nothing -> Maybe (QName, Type) -> m (Maybe (QName, Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Type)
    forall a. Maybe a
    Nothing
      Term
    _ -> Maybe (QName, Type) -> m (Maybe (QName, Type))
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (QName, Type)
    forall a. Maybe a
    Nothing